Migrate to `Felix` namespaceHEADhotg

5 files changed, 4562 insertions, 0 deletions

diff --git a/source/Felix/Checking/Exact/Datatype.hs b/source/Felix/Checking/Exact/Datatype.hs
new file mode 100644
index 0000000..be943cd
--- /dev/null
+++ b/source/Felix/Checking/Exact/Datatype.hs
@@ -0,0 +1,751 @@
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | Exact preparation of deterministic datatype declarations.
+module Felix.Checking.Exact.Datatype
+    ( PreparedExactDatatype
+    , preparedExactDatatypeObjects
+    , preparedExactDatatypeBindings
+    , PreparedExactDatatypeFact
+    , preparedExactDatatypeFacts
+    , preparedExactDatatypeFactMarker
+    , preparedExactDatatypeFactTarget
+    , preparedExactDatatypeFactReference
+    , preparedExactDatatypeDescriptor
+    , prepareExactDatatype
+    , CheckedExactDatatypeAuthorization
+    , lowerPreparedExactDatatype
+    , authorizeCheckedExactDatatype
+    , ExactDatatypeError(..)
+    , exactDatatypeErrorLocation
+    , renderExactDatatypeError
+    ) where
+
+import Base hiding (Empty)
+import Felix.Checking.Authority
+import Felix.Checking.Core
+import Felix.Checking.Datatype qualified as Datatype
+import Felix.Checking.Declaration qualified as Declaration
+import Felix.Checking.Exact.Global qualified as ExactGlobal
+import Felix.Checking.Exact.Vocabulary
+import Felix.Checking.Identity
+import Felix.Checking.Semantic
+import Felix.Checking.Typed.Inductive qualified as Typed
+import Felix.Cache.Codec
+import Felix.Module
+import Felix.Meaning qualified as Meaning
+import Felix.Report.Location
+import Felix.Syntax.Abstract qualified as Raw
+import Felix.Syntax.Interface
+import Felix.Syntax.Internal qualified as Internal
+
+import Control.Monad (unless, when)
+import Control.Monad.Except (ExceptT)
+import Control.Monad.Except qualified as Except
+import Data.Bifunctor (first)
+import Data.ByteString (ByteString)
+import Data.List.NonEmpty qualified as NonEmpty
+import Data.Map.Strict qualified as Map
+import Data.Set qualified as Set
+import Data.Text qualified as Text
+import Numeric.Natural (Natural)
+
+
+data PreparedDatatypeObject = PreparedDatatypeObject
+    !Internal.Symbol
+    !SemanticGlobalKey
+    !CoreType
+    !ObjectId
+    !AssertedObject
+
+data PreparedExactDatatypeFact = PreparedExactDatatypeFact
+    !Internal.Marker
+    !(FrozenCheckedCore ObjectId)
+    !TheoremRef
+
+preparedExactDatatypeFactMarker
+    :: PreparedExactDatatypeFact
+    -> Internal.Marker
+preparedExactDatatypeFactMarker
+        (PreparedExactDatatypeFact marker _target _reference) =
+    marker
+
+preparedExactDatatypeFactTarget
+    :: PreparedExactDatatypeFact
+    -> FrozenCheckedCore ObjectId
+preparedExactDatatypeFactTarget
+        (PreparedExactDatatypeFact _marker target _reference) =
+    target
+
+preparedExactDatatypeFactReference
+    :: PreparedExactDatatypeFact
+    -> TheoremRef
+preparedExactDatatypeFactReference
+        (PreparedExactDatatypeFact _marker _target reference) =
+    reference
+
+data PreparedExactDatatype = PreparedExactDatatype
+    !Location
+    !DeclarationSyntaxId
+    !(NonEmpty PreparedDatatypeObject)
+    !(NonEmpty PreparedExactDatatypeFact)
+    !DatatypeCompilationDescriptor
+
+data CheckedExactDatatypeAuthorization =
+    CheckedExactDatatypeAuthorization
+        !DatatypeCompilationDescriptor
+        !ObjectId
+        !(NonEmpty ObjectId)
+
+preparedExactDatatypeObjects
+    :: PreparedExactDatatype
+    -> NonEmpty (ObjectId, CoreType)
+preparedExactDatatypeObjects
+        (PreparedExactDatatype _location _syntax objects _facts _descriptor) =
+    fmap
+        (\(PreparedDatatypeObject _symbol _key coreType identity _asserted) ->
+            (identity, coreType))
+        objects
+
+preparedExactDatatypeBindings
+    :: PreparedExactDatatype
+    -> NonEmpty (SemanticGlobalKey, SemanticGlobalTarget)
+preparedExactDatatypeBindings
+        (PreparedExactDatatype _location _syntax objects _facts _descriptor) =
+    fmap
+        (\(PreparedDatatypeObject _symbol key _coreType identity _asserted) ->
+            (key, GlobalReference identity))
+        objects
+
+preparedExactDatatypeFacts
+    :: PreparedExactDatatype
+    -> NonEmpty PreparedExactDatatypeFact
+preparedExactDatatypeFacts
+        (PreparedExactDatatype _location _syntax _objects facts _descriptor) =
+    facts
+
+preparedExactDatatypeDescriptor
+    :: PreparedExactDatatype
+    -> DatatypeCompilationDescriptor
+preparedExactDatatypeDescriptor
+        (PreparedExactDatatype _location _syntax _objects _facts descriptor) =
+    descriptor
+
+lowerPreparedExactDatatype
+    :: PreparedExactDatatype
+    -> Declaration.LoweringDriver
+        (Either
+            Declaration.DeclarationError
+            (Declaration.CheckedDeclaration
+                CheckedExactDatatypeAuthorization))
+lowerPreparedExactDatatype
+        (PreparedExactDatatype _location syntax objects facts descriptor) =
+    do
+        prepared <-
+            traverse
+                (\(PreparedExactDatatypeFact marker target _reference) ->
+                    Declaration.prepareFrozenCandidateSpecLowering
+                        assertedObjects
+                        target
+                        SearchEligible
+                        [markerAlias marker])
+                facts
+        pure (buildChecked <$> sequence prepared)
+  where
+    assertedObjects =
+        toList
+            (fmap
+                (\(PreparedDatatypeObject
+                        _symbol _key _coreType _identity asserted) -> asserted)
+                objects)
+    bindings =
+        toList
+            (fmap
+                (\(PreparedDatatypeObject
+                        _symbol key _coreType identity _asserted) ->
+                    semanticGlobalBinding key (GlobalReference identity))
+                objects)
+    carrier :| constructors = fmap objectIdentity objects
+    constructorIds =
+        case constructors of
+            firstConstructor : remainingConstructors ->
+                firstConstructor :| remainingConstructors
+            [] -> impossible "a prepared datatype has no constructor"
+    buildChecked specs =
+        Declaration.checkedCompiledDeclaration
+            syntax
+            assertedObjects
+            []
+            bindings
+            []
+            [ fmap
+                (\spec ->
+                    Declaration.checkedCandidate
+                        spec
+                        (Declaration.checkedDatatypePlanning descriptor))
+                specs
+            ]
+            (CheckedExactDatatypeAuthorization
+                descriptor carrier constructorIds)
+
+    markerAlias (Internal.Marker name) = semanticName name
+
+    objectIdentity
+            (PreparedDatatypeObject
+                _symbol _key _coreType identity _asserted) =
+        identity
+
+authorizeCheckedExactDatatype
+    :: CheckedExactDatatypeAuthorization
+    -> [NonEmpty Declaration.ReservedCandidate]
+    -> Declaration.Declaration ()
+authorizeCheckedExactDatatype
+        (CheckedExactDatatypeAuthorization descriptor carrier constructors) =
+    \case
+        [candidates] ->
+            Declaration.authorizeDatatypeCompilationCandidates
+                descriptor carrier constructors candidates
+        stages ->
+            Declaration.failDeclaration
+                (Declaration.CheckedAuthorizationCandidateShapeMismatch
+                    1 (length stages))
+
+data ExactDatatypeError
+    = ExactDatatypeUnsupportedBlock !Location
+    | ExactDatatypeOccurrenceCountMismatch !Location !Int !Int
+    | ExactDatatypeOccurrenceMismatch !Location
+    | ExactDatatypeGlossFailed !Location !Meaning.GlossError
+    | ExactDatatypeInvalid !Location !Text
+    | ExactDatatypeDuplicateGlobal !Location !SemanticGlobalKey
+    | ExactDatatypeFixedSemanticCollision !Location !SemanticGlobalKey
+    | ExactDatatypeGlobalAlreadyVisible !Location !SemanticGlobalKey
+    | ExactDatatypeObjectAlreadyAvailable !Location !ObjectId
+    | ExactDatatypeGlobalResolutionFailed
+        !Location
+        !ExactGlobal.ExactGlobalResolutionError
+    | ExactDatatypeLoweringFailed !Location !Typed.TypedInductiveError
+    | ExactDatatypeExpectedSet !Location !CoreType
+    | ExactDatatypeExpectedProposition !Location !CoreType
+    deriving stock (Show, Eq)
+
+exactDatatypeErrorLocation :: ExactDatatypeError -> Location
+exactDatatypeErrorLocation = \case
+    ExactDatatypeUnsupportedBlock location -> location
+    ExactDatatypeOccurrenceCountMismatch location _expected _actual -> location
+    ExactDatatypeOccurrenceMismatch location -> location
+    ExactDatatypeGlossFailed location _failure -> location
+    ExactDatatypeInvalid location _message -> location
+    ExactDatatypeDuplicateGlobal location _key -> location
+    ExactDatatypeFixedSemanticCollision location _key -> location
+    ExactDatatypeGlobalAlreadyVisible location _key -> location
+    ExactDatatypeObjectAlreadyAvailable location _identity -> location
+    ExactDatatypeGlobalResolutionFailed location _failure -> location
+    ExactDatatypeLoweringFailed location _failure -> location
+    ExactDatatypeExpectedSet location _actual -> location
+    ExactDatatypeExpectedProposition location _actual -> location
+
+renderExactDatatypeError :: ExactDatatypeError -> Text
+renderExactDatatypeError failure =
+    locationToText (exactDatatypeErrorLocation failure)
+        <> ": "
+        <> case failure of
+            ExactDatatypeUnsupportedBlock{} ->
+                "this datatype source form is not supported by the typed checker"
+            ExactDatatypeOccurrenceCountMismatch _location expected actual ->
+                "the datatype has " <> shown actual
+                    <> " syntax occurrences, but " <> shown expected
+                    <> " are required"
+            ExactDatatypeOccurrenceMismatch{} ->
+                "a datatype syntax occurrence does not match its declaration"
+            ExactDatatypeGlossFailed _location glossFailure ->
+                "datatype elaboration failed: " <> shown glossFailure
+            ExactDatatypeInvalid _location message ->
+                "invalid datatype declaration: " <> message
+            ExactDatatypeDuplicateGlobal _location key ->
+                "the datatype declares the semantic key more than once: "
+                    <> shown key
+            ExactDatatypeFixedSemanticCollision _location key ->
+                "the datatype collides with fixed semantics for " <> shown key
+            ExactDatatypeGlobalAlreadyVisible _location key ->
+                "the datatype global is already visible: " <> shown key
+            ExactDatatypeObjectAlreadyAvailable _location identity ->
+                "the datatype opaque object is already available: "
+                    <> shown identity
+            ExactDatatypeGlobalResolutionFailed _location resolution ->
+                "datatype global resolution failed: " <> shown resolution
+            ExactDatatypeLoweringFailed _location typedFailure ->
+                "typed datatype lowering failed: " <> shown typedFailure
+            ExactDatatypeExpectedSet _location actual ->
+                "a datatype premise domain has type " <> shown actual
+                    <> " instead of Set"
+            ExactDatatypeExpectedProposition _location actual ->
+                "a generated datatype fact has type " <> shown actual
+                    <> " instead of Prop"
+  where
+    shown :: Show value => value -> Text
+    shown = Text.pack . show
+
+type Prepare =
+    ExceptT ExactDatatypeError (Declaration.LoweringDriver)
+
+type SourceOccurrence = (Location, Raw.Marker, CanonicalLexicalEntry)
+
+exactDatatypeInvalid
+    :: Location
+    -> Datatype.DatatypeValidationError
+    -> ExactDatatypeError
+exactDatatypeInvalid declarationLocation failure =
+    ExactDatatypeInvalid
+        (fromMaybe
+            declarationLocation
+            (Datatype.datatypeValidationErrorLocation failure))
+        (Datatype.renderDatatypeValidationError failure)
+
+prepareExactDatatype
+    :: Raw.Block
+    -> [SourceOccurrence]
+    -> Declaration.LoweringDriver
+        (Either ExactDatatypeError PreparedExactDatatype)
+prepareExactDatatype block occurrences =
+    Except.runExceptT do
+        (location, marker, rawDatatype) <-
+            case block of
+                Raw.BlockData blockLocation _title blockMarker datatype ->
+                    pure (blockLocation, blockMarker, datatype)
+                _ ->
+                    Except.throwError
+                        (ExactDatatypeUnsupportedBlock (locate block))
+        keys <- validateOccurrences location marker rawDatatype occurrences
+        internal <-
+            case Meaning.meaning [block] of
+                Right
+                    [Internal.BlockData
+                        _internalLocation _internalMarker datatype] ->
+                            pure datatype
+                Left failure ->
+                    Except.throwError
+                        (ExactDatatypeGlossFailed location failure)
+                Right _ ->
+                    Except.throwError
+                        (ExactDatatypeUnsupportedBlock location)
+        checked <-
+            -- The new opaque carrier has no semantic binding while its
+            -- declaration is prepared, so premise recursion cannot depend on
+            -- abbreviation expansion. Revisit this if forward aliases become
+            -- available.
+            Except.lift
+                (Datatype.prepareCheckedDatatype pure internal)
+                >>= Except.liftEither
+                    . first (exactDatatypeInvalid location)
+        let symbols =
+                Datatype.checkedDatatypeHeadSymbol checked
+                    :| toList
+                        (Datatype.checkedDatatypeConstructorSymbols checked)
+            views = Datatype.checkedDatatypeClauseViews checked
+            arities =
+                0 :| (length
+                    . Datatype.checkedDatatypeClauseViewArguments
+                    <$> toList views)
+        unless (NonEmpty.length symbols == NonEmpty.length keys)
+            (Except.throwError
+                (ExactDatatypeOccurrenceCountMismatch
+                    location
+                    (NonEmpty.length symbols)
+                    (NonEmpty.length keys)))
+        validateKeys occurrences keys
+        slot <- Except.lift Declaration.nextDeclarationSlotLowering
+        theory <- Except.lift Declaration.currentTheoryLowering
+        objects <-
+            sequence
+                (NonEmpty.zipWith
+                    (\index (occurrenceLocation, symbol, key, arity) ->
+                        prepareObject
+                            occurrenceLocation
+                            slot theory index symbol key arity)
+                    (0 :| [1 ..])
+                    (NonEmpty.zipWith
+                        (\occurrenceLocation (symbol, key, arity) ->
+                            (occurrenceLocation, symbol, key, arity))
+                        (validatedOccurrenceLocations occurrences)
+                        (NonEmpty.zipWith
+                            (\(symbol, key) arity ->
+                                (symbol, key, arity))
+                            (NonEmpty.zip symbols keys)
+                            arities)))
+        let ownedSymbols = Set.fromList (toList symbols)
+            generated = Datatype.checkedDatatypeGeneratedFacts checked
+            externalSymbols =
+                (foldMap
+                    (Internal.mentionedSymbols . snd)
+                    generated
+                    <> foldMap premiseSymbols views)
+                    `Set.difference` ownedSymbols
+        external <-
+            Except.lift
+                (ExactGlobal.resolveExactSourceGlobals externalSymbols)
+                >>= Except.liftEither
+                    . first (ExactDatatypeGlobalResolutionFailed location)
+        let (externalGlobals, externalTypes) = external
+            ownedGlobals =
+                Map.fromList
+                    [ (symbol, Typed.SourceGlobal identity Nothing)
+                    | PreparedDatatypeObject
+                        symbol _key _coreType identity _asserted <-
+                            toList objects
+                    ]
+            ownedTypes =
+                Map.fromList
+                    [ (identity, coreType)
+                    | PreparedDatatypeObject
+                        _symbol _key coreType identity _asserted <-
+                            toList objects
+                    ]
+            sourceGlobals = Map.union ownedGlobals externalGlobals
+            globalTypes = Map.union ownedTypes externalTypes
+            resolveGlobal = (`Map.lookup` sourceGlobals)
+            globalType identity =
+                fromMaybe
+                    (impossible
+                        "prepared datatype global has no checked type")
+                    (Map.lookup identity globalTypes)
+        preparedClauses <-
+            Except.liftEither
+                (traverse
+                    (prepareClause location globalType resolveGlobal)
+                    views)
+        facts <-
+            Except.liftEither
+                (traverse
+                    (prepareFact location theory globalType resolveGlobal)
+                    generated)
+        let carrier = objectIdentity (NonEmpty.head objects)
+            constructors = objectIdentity <$> NonEmpty.tail objects
+            descriptor =
+                case NonEmpty.nonEmpty constructors of
+                    Nothing ->
+                        impossible
+                            "a checked datatype has no constructors"
+                    Just nonemptyConstructors ->
+                        datatypeCompilationDescriptor
+                            carrier
+                            nonemptyConstructors
+                            (preparedExactDatatypeFactReference
+                                <$> toList facts)
+            syntax =
+                declarationSyntaxId
+                    (encodePreparedDatatype
+                        objects
+                        preparedClauses
+                        facts
+                        descriptor)
+        pure
+            (PreparedExactDatatype
+                location
+                syntax
+                objects
+                facts
+                descriptor)
+  where
+    objectIdentity
+        (PreparedDatatypeObject _symbol _key _coreType identity _asserted) =
+        identity
+
+validateOccurrences
+    :: Location
+    -> Raw.Marker
+    -> Raw.Datatype
+    -> [SourceOccurrence]
+    -> Prepare (NonEmpty SemanticGlobalKey)
+validateOccurrences location marker datatype occurrences = do
+    expected <-
+        Except.liftEither
+            (expectedOccurrences location marker datatype)
+    unless (length occurrences == NonEmpty.length expected)
+        (Except.throwError
+            (ExactDatatypeOccurrenceCountMismatch
+                location
+                (NonEmpty.length expected)
+                (length occurrences)))
+    keys <-
+        sequence
+            (NonEmpty.zipWith validateOne expected
+                (case NonEmpty.nonEmpty occurrences of
+                    Just nonempty -> nonempty
+                    Nothing ->
+                        impossible
+                            "equal nonzero occurrence counts became empty"))
+    pure keys
+  where
+    validateOne
+            (expectedLocation, expectedMarker, expectedPattern)
+            (actualLocation, actualMarker, entry) =
+        case entry of
+            CanonicalExpressionFunction pat marker' _fixity
+                | actualMarker == expectedMarker
+                , marker' == expectedMarker
+                , pat == expectedPattern ->
+                    pure
+                        (SemanticExpressionFunction pat)
+            _ ->
+                Except.throwError
+                    (ExactDatatypeOccurrenceMismatch
+                        (bestLocation actualLocation expectedLocation))
+
+    bestLocation actual expected
+        | actual == Nowhere = expected
+        | otherwise = actual
+
+expectedOccurrences
+    :: Location
+    -> Raw.Marker
+    -> Raw.Datatype
+    -> Either
+        ExactDatatypeError
+        (NonEmpty (Location, Raw.Marker, Raw.Pattern))
+expectedOccurrences location blockMarker datatype = do
+    headOccurrence <-
+        expectedSymbol blockMarker (Raw.datatypeHeadExpr datatype)
+    clauses <-
+        traverse
+            (\clause ->
+                case Raw.datatypeClauseConstructorExpr clause of
+                    Raw.ExprOp constructorLocation symbol _arguments ->
+                        Right
+                            ( constructorLocation
+                            , Raw.mixfixMarker symbol
+                            , Raw.mixfixPattern symbol
+                            )
+                    expression ->
+                        Left
+                            (ExactDatatypeOccurrenceMismatch
+                                (locate expression)))
+            (Raw.datatypeClauses datatype)
+    pure (headOccurrence :| toList clauses)
+  where
+    expectedSymbol expectedMarker = \case
+        Raw.ExprOp symbolLocation symbol [] ->
+            Right
+                ( symbolLocation
+                , expectedMarker
+                , Raw.mixfixPattern symbol
+                )
+        expression ->
+            Left
+                (ExactDatatypeOccurrenceMismatch
+                    (case locate expression of
+                        Nowhere -> location
+                        expressionLocation -> expressionLocation))
+
+validateKeys
+    :: [SourceOccurrence]
+    -> NonEmpty SemanticGlobalKey
+    -> Prepare ()
+validateKeys occurrences keys = do
+    case duplicateWithLocation of
+        Just (duplicate, duplicateLocation) ->
+            Except.throwError
+                (ExactDatatypeDuplicateGlobal
+                    duplicateLocation
+                    duplicate)
+        Nothing -> pure ()
+    traverse_ validateOne (NonEmpty.zip locations keys)
+  where
+    locations = validatedOccurrenceLocations occurrences
+
+    duplicateWithLocation =
+        go Set.empty
+            [ (key, occurrenceLocation)
+            | (key, (occurrenceLocation, _marker, _entry)) <-
+                zip (toList keys) occurrences
+            ]
+
+    go _seen [] = Nothing
+    go seen ((key, occurrenceLocation) : remaining)
+        | key `Set.member` seen = Just (key, occurrenceLocation)
+        | otherwise = go (Set.insert key seen) remaining
+
+    validateOne (occurrenceLocation, key) = do
+        when (isJust (fixedSemanticMeaning key))
+            (Except.throwError
+                (ExactDatatypeFixedSemanticCollision occurrenceLocation key))
+        visible <-
+            Except.lift
+                (Declaration.resolveVisibleGlobalLowering key)
+        when (isJust visible)
+            (Except.throwError
+                (ExactDatatypeGlobalAlreadyVisible occurrenceLocation key))
+
+validatedOccurrenceLocations
+    :: [SourceOccurrence]
+    -> NonEmpty Location
+validatedOccurrenceLocations occurrences =
+    case NonEmpty.nonEmpty
+            [ occurrenceLocation
+            | (occurrenceLocation, _marker, _entry) <- occurrences
+            ] of
+        Just nonempty -> nonempty
+        Nothing ->
+            impossible "validated datatype occurrences are empty"
+
+prepareObject
+    :: Location
+    -> DeclarationSlot
+    -> TheoryId
+    -> Natural
+    -> Internal.Symbol
+    -> SemanticGlobalKey
+    -> Int
+    -> Prepare PreparedDatatypeObject
+prepareObject location slot theory index symbol key arity = do
+    let coreType =
+            foldr (const (TyArrow TySet)) TySet [1 .. arity]
+        seed =
+            opaqueDeclarationSeed
+                (declarationSlotModule slot)
+                (declarationSlotOrdinal slot)
+                DatatypeDeclaration
+                (generatedObjectSlot index)
+        content = OpaqueObjectContent theory seed coreType
+        identity = opaqueObjectId theory seed coreType
+    available <- Except.lift (Declaration.objectAvailableLowering identity)
+    when available
+        (Except.throwError
+            (ExactDatatypeObjectAlreadyAvailable location identity))
+    pure
+        (PreparedDatatypeObject
+            symbol
+            key
+            coreType
+            identity
+            (assertedObject identity content))
+
+data PreparedClause = PreparedClause
+    !Internal.FunctionSymbol
+    ![PreparedPremise]
+
+data PreparedPremise
+    = PreparedRecursivePremise !(FrozenCheckedCore ObjectId)
+    | PreparedNonRecursivePremise !(FrozenCheckedCore ObjectId)
+
+prepareClause
+    :: Location
+    -> (ObjectId -> CoreType)
+    -> (Internal.Symbol -> Maybe (Typed.SourceGlobal ObjectId))
+    -> Datatype.CheckedDatatypeClauseView
+    -> Either ExactDatatypeError PreparedClause
+prepareClause location globalType resolveGlobal view =
+    PreparedClause
+        (Datatype.checkedDatatypeClauseViewConstructor view)
+        <$> traverse preparePremise
+            (Datatype.checkedDatatypeClauseViewPremises view)
+  where
+    preparePremise = \case
+        Datatype.CheckedRecursiveDatatypePremise _variable domain ->
+            PreparedRecursivePremise
+                <$> prepareDomain domain
+        Datatype.CheckedNonRecursiveDatatypePremise _variable domain ->
+            PreparedNonRecursivePremise
+                <$> prepareDomain domain
+
+    prepareDomain domain = do
+        checked <-
+            first (ExactDatatypeLoweringFailed location)
+                (Typed.prepareTypedClosedTerm
+                    globalType
+                    resolveGlobal
+                    domain)
+        unless (frozenCoreType checked == TySet)
+            (Left
+                (ExactDatatypeExpectedSet
+                    location
+                    (frozenCoreType checked)))
+        pure checked
+
+prepareFact
+    :: Location
+    -> TheoryId
+    -> (ObjectId -> CoreType)
+    -> (Internal.Symbol -> Maybe (Typed.SourceGlobal ObjectId))
+    -> (Internal.Marker, Internal.Formula)
+    -> Either ExactDatatypeError PreparedExactDatatypeFact
+prepareFact location theory globalType resolveGlobal (marker, formula) = do
+    checked <-
+        first (ExactDatatypeLoweringFailed location)
+            (Typed.prepareTypedClosedFormula
+                globalType
+                resolveGlobal
+                formula)
+    unless (frozenCoreType checked == TyProp)
+        (Left
+            (ExactDatatypeExpectedProposition
+                location
+                (frozenCoreType checked)))
+    pure
+        (PreparedExactDatatypeFact
+            marker
+            checked
+            (theoremRef theory
+                (propositionIdOf (frozenCoreTerm checked))))
+
+premiseSymbols
+    :: Datatype.CheckedDatatypeClauseView
+    -> Set.Set Internal.Symbol
+premiseSymbols view =
+    foldMap symbols
+        (Datatype.checkedDatatypeClauseViewPremises view)
+  where
+    symbols = \case
+        Datatype.CheckedRecursiveDatatypePremise _variable domain ->
+            Internal.mentionedSymbols domain
+        Datatype.CheckedNonRecursiveDatatypePremise _variable domain ->
+            Internal.mentionedSymbols domain
+
+encodePreparedDatatype
+    :: NonEmpty PreparedDatatypeObject
+    -> NonEmpty PreparedClause
+    -> NonEmpty PreparedExactDatatypeFact
+    -> DatatypeCompilationDescriptor
+    -> ByteString
+encodePreparedDatatype objects clauses facts descriptor =
+    encodeCache do
+        putCacheTag 0x05
+        putCacheList putObject (toList objects)
+        putCacheList putClause (toList clauses)
+        putCacheList putFact (toList facts)
+        putDirectAuthorizationCache
+            (TrustedCompilation
+                (DatatypeCompilation descriptor))
+  where
+    putObject
+            (PreparedDatatypeObject
+                _symbol key coreType identity _asserted) = do
+        putSemanticGlobalKeyCache key
+        putCoreTypeCache coreType
+        putObjectIdCache identity
+
+    putClause (PreparedClause constructor premises) = do
+        putSemanticGlobalKeyCache
+            (SemanticExpressionFunction
+                (Raw.mixfixPattern constructor))
+        putCacheList putPremise premises
+
+    putPremise = \case
+        PreparedRecursivePremise domain -> do
+            putCacheTag 0x00
+            putCanonicalTermCache putObjectIdCache
+                (frozenCoreTerm domain)
+        PreparedNonRecursivePremise domain -> do
+            putCacheTag 0x01
+            putCanonicalTermCache putObjectIdCache
+                (frozenCoreTerm domain)
+
+    putFact fact = do
+        let Internal.Marker marker =
+                preparedExactDatatypeFactMarker fact
+        putCacheText marker
+        putCanonicalTermCache putObjectIdCache
+            (frozenCoreTerm
+                (preparedExactDatatypeFactTarget fact))
+        putTheoremRefCache
+            (preparedExactDatatypeFactReference fact)
diff --git a/source/Felix/Checking/Exact/Global.hs b/source/Felix/Checking/Exact/Global.hs
new file mode 100644
index 0000000..d4040e6
--- /dev/null
+++ b/source/Felix/Checking/Exact/Global.hs
@@ -0,0 +1,116 @@
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | Exact resolution of source symbols to checked semantic globals.
+module Felix.Checking.Exact.Global
+    ( ExactGlobalResolutionError(..)
+    , resolveExactSourceGlobals
+    ) where
+
+import Base
+import Felix.Checking.Core
+import Felix.Checking.Declaration qualified as Declaration
+import Felix.Checking.Exact.Vocabulary
+import Felix.Checking.Identity
+import Felix.Checking.Semantic
+import Felix.Checking.Typed.Inductive qualified as Typed
+import Felix.Syntax.Internal qualified as Internal
+
+import Control.Monad (foldM)
+import Control.Monad.Except
+    ( liftEither
+    , runExceptT
+    , throwError
+    )
+import Control.Monad.Trans.Class (lift)
+import Data.Bifunctor (first)
+import Data.Map.Strict qualified as Map
+import Data.Maybe (catMaybes)
+import Data.Set qualified as Set
+
+
+data ExactGlobalResolutionError
+    = ExactGlobalNotVisible !Internal.Symbol
+    | ExactGlobalAmbiguous !Internal.Symbol
+    | ExactGlobalUnsupported !Internal.Symbol
+    | ExactGlobalContextualUnsupported !Internal.Symbol
+    | ExactGlobalContentInvalid !CoreCheckError
+    deriving stock (Show, Eq)
+
+resolveExactSourceGlobals
+    :: Set.Set Internal.Symbol
+    -> Declaration.LoweringDriver
+        (Either
+            ExactGlobalResolutionError
+            ( Map.Map
+                Internal.Symbol
+                (Typed.SourceGlobal ObjectId)
+            , Map.Map ObjectId CoreType
+            ))
+resolveExactSourceGlobals symbols =
+    runExceptT
+        (foldM resolve (Map.empty, Map.empty)
+            (Set.toAscList symbols))
+  where
+    resolve (resolved, types) symbol =
+        case classifyExactSymbol symbol of
+            ExactClosedLiteral ->
+                pure (resolved, types)
+            ExactFixedPrimitive _meaning ->
+                pure (resolved, types)
+            ExactUnsupportedSymbol ->
+                throwError (ExactGlobalUnsupported symbol)
+            ExactSourceGlobal keys -> do
+                matches <-
+                    catMaybes
+                        <$> traverse
+                            (lift
+                                . Declaration.resolveVisibleGlobalContentLowering)
+                            (toList keys)
+                case matches of
+                    [] ->
+                        throwError (ExactGlobalNotVisible symbol)
+                    [match] -> do
+                        (source, sourceTypes) <-
+                            liftEither (prepareSourceGlobal symbol match)
+                        pure
+                            ( Map.insert symbol source resolved
+                            , Map.union sourceTypes types
+                            )
+                    _ ->
+                        throwError (ExactGlobalAmbiguous symbol)
+
+prepareSourceGlobal
+    :: Internal.Symbol
+    -> ( SemanticGlobalTarget
+       , ObjectContent
+       , Map.Map ObjectId CoreType
+       )
+    -> Either
+        ExactGlobalResolutionError
+        (Typed.SourceGlobal ObjectId, Map.Map ObjectId CoreType)
+prepareSourceGlobal symbol (target, content, dependencies) = do
+    body <-
+        case target of
+            GlobalReference _identity ->
+                Right Nothing
+            TransparentExpansion _identity ->
+                case content of
+                    TransparentObjectContent _theory _coreType canonical ->
+                        Just
+                            <$> first ExactGlobalContentInvalid
+                                (checkCanonicalCore
+                                    (`Map.lookup` dependencies)
+                                    canonical)
+                    _ ->
+                        impossible
+                            "validated transparent expansion has opaque content"
+            ContextualTransparentExpansion _identity _requirements ->
+                Left (ExactGlobalContextualUnsupported symbol)
+    let identity = semanticGlobalTargetObject target
+        types =
+            Map.insert
+                identity
+                (objectContentType content)
+                dependencies
+    pure (Typed.SourceGlobal identity body, types)
diff --git a/source/Felix/Checking/Exact/Inductive.hs b/source/Felix/Checking/Exact/Inductive.hs
new file mode 100644
index 0000000..5817b34
--- /dev/null
+++ b/source/Felix/Checking/Exact/Inductive.hs
@@ -0,0 +1,838 @@
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | Exact preparation and atomic publication of direct set inductives.
+module Felix.Checking.Exact.Inductive
+    ( PreparedExactInductive
+    , preparedExactInductiveCarrierId
+    , preparedExactInductiveCarrierType
+    , preparedExactInductiveCarrierBody
+    , preparedExactInductiveGuardTargets
+    , preparedExactInductiveFacts
+    , prepareExactInductive
+    , CheckedExactInductiveAuthorization
+    , lowerPreparedExactInductive
+    , authorizeCheckedExactInductive
+    , ExactInductiveError(..)
+    , exactInductiveErrorLocation
+    , renderExactInductiveError
+    ) where
+
+import Base hiding (Empty)
+import Felix.Checking.Authority
+import Felix.Checking.Core
+import Felix.Checking.Declaration qualified as Declaration
+import Felix.Checking.Exact.Global qualified as ExactGlobal
+import Felix.Checking.Exact.Vocabulary
+import Felix.Checking.Foundation
+import Felix.Checking.Identity
+import Felix.Checking.Semantic
+import Felix.Checking.Typed.Inductive qualified as Typed
+import Felix.Cache.Codec
+import Felix.Meaning qualified as Meaning
+import Felix.Report.Location
+import Felix.Syntax.Abstract qualified as Raw
+import Felix.Syntax.Interface
+import Felix.Syntax.Internal qualified as Internal
+
+import Control.Monad (unless, when)
+import Control.Monad.Except (ExceptT)
+import Control.Monad.Except qualified as Except
+import Data.Bifunctor (first)
+import Data.ByteString (ByteString)
+import Data.List qualified as List
+import Data.List.NonEmpty qualified as NonEmpty
+import Data.Map.Strict qualified as Map
+import Data.Set qualified as Set
+import Data.Text qualified as Text
+import Data.Vector qualified as Vector
+
+
+data PreparedExactInductive = PreparedExactInductive
+    !Location
+    !SemanticGlobalKey
+    !ObjectId
+    !(Maybe AssertedObject)
+    !SemanticName
+    !DeclarationSyntaxId
+    !(Typed.PreparedTypedInductive ObjectId)
+    ![SemanticFactOccurrenceFingerprint]
+
+data CheckedExactInductiveAuthorization =
+    CheckedExactInductiveAuthorization
+        !ObjectId
+        !(Typed.PreparedTypedInductive ObjectId)
+        ![SemanticFactOccurrenceFingerprint]
+        ![(Location, Declaration.PreparedVampireObligation Void ())]
+
+preparedExactInductiveCarrierId
+    :: PreparedExactInductive
+    -> ObjectId
+preparedExactInductiveCarrierId
+        (PreparedExactInductive
+            _location _key identity _asserted _alias _syntax _typed _guards) =
+    identity
+
+preparedExactInductiveCarrierType
+    :: PreparedExactInductive
+    -> CoreType
+preparedExactInductiveCarrierType
+        (PreparedExactInductive
+            _location _key _identity _asserted _alias _syntax typed _guards) =
+    Typed.typedInductiveCarrierType typed
+
+preparedExactInductiveCarrierBody
+    :: PreparedExactInductive
+    -> FrozenCheckedCore ObjectId
+preparedExactInductiveCarrierBody
+        (PreparedExactInductive
+            _location _key _identity _asserted _alias _syntax typed _guards) =
+    Typed.typedInductiveCarrierBody typed
+
+preparedExactInductiveGuardTargets
+    :: PreparedExactInductive
+    -> Vector.Vector (FrozenCheckedCore ObjectId)
+preparedExactInductiveGuardTargets
+        (PreparedExactInductive
+            _location _key _identity _asserted _alias _syntax typed _guards) =
+    Typed.typedInductiveGuardTargets typed
+
+preparedExactInductiveFacts
+    :: PreparedExactInductive
+    -> NonEmpty (Typed.PreparedTypedInductiveFact ObjectId)
+preparedExactInductiveFacts
+        (PreparedExactInductive
+            _location _key _identity _asserted _alias _syntax typed _guards) =
+    Typed.typedInductiveFacts typed
+
+data ExactInductiveError
+    = ExactInductiveUnsupportedBlock !Location
+    | ExactInductiveOccurrenceMissing !Location
+    | ExactInductiveOccurrenceAmbiguous !Location
+    | ExactInductiveHeadMismatch !Location
+    | ExactInductiveGlossFailed !Location !Meaning.GlossError
+    | ExactInductiveDuplicateParameter !Location !Internal.VarSymbol
+    | ExactInductiveDomainFreeVariable !Location !Internal.VarSymbol
+    | ExactInductiveDomainMentionsCarrier !Location
+    | ExactInductiveResultShape !Location
+    | ExactInductiveResultMentionsCarrier !Location
+    | ExactInductiveRecursiveTermMentionsCarrier !Location
+    | ExactInductiveRecursiveCarrierWrongArguments !Location
+    | ExactInductiveRecursiveCarrierOutsideMembership !Location
+    | ExactInductiveUnsupportedRecursiveCarrierContext !Location
+    | ExactInductiveFixedSemanticCollision !Location !SemanticGlobalKey
+    | ExactInductiveGlobalAlreadyVisible !Location !SemanticGlobalKey
+    | ExactInductiveGlobalNotVisible !Location !Internal.Symbol
+    | ExactInductiveGlobalAmbiguous !Location !Internal.Symbol
+    | ExactInductiveUnsupportedSymbol !Location !Internal.Symbol
+    | ExactInductiveGlobalContentInvalid !Location !CoreCheckError
+    | ExactInductivePreparationFailed
+        !Location
+        !Typed.TypedInductiveError
+    | ExactInductiveGuardMissing !Location
+    | ExactInductiveGuardAmbiguous !Location
+    deriving stock (Show, Eq)
+
+exactInductiveErrorLocation :: ExactInductiveError -> Location
+exactInductiveErrorLocation = \case
+    ExactInductiveUnsupportedBlock location -> location
+    ExactInductiveOccurrenceMissing location -> location
+    ExactInductiveOccurrenceAmbiguous location -> location
+    ExactInductiveHeadMismatch location -> location
+    ExactInductiveGlossFailed location _failure -> location
+    ExactInductiveDuplicateParameter location _parameter -> location
+    ExactInductiveDomainFreeVariable location _variable -> location
+    ExactInductiveDomainMentionsCarrier location -> location
+    ExactInductiveResultShape location -> location
+    ExactInductiveResultMentionsCarrier location -> location
+    ExactInductiveRecursiveTermMentionsCarrier location -> location
+    ExactInductiveRecursiveCarrierWrongArguments location -> location
+    ExactInductiveRecursiveCarrierOutsideMembership location -> location
+    ExactInductiveUnsupportedRecursiveCarrierContext location -> location
+    ExactInductiveFixedSemanticCollision location _key -> location
+    ExactInductiveGlobalAlreadyVisible location _key -> location
+    ExactInductiveGlobalNotVisible location _symbol -> location
+    ExactInductiveGlobalAmbiguous location _symbol -> location
+    ExactInductiveUnsupportedSymbol location _symbol -> location
+    ExactInductiveGlobalContentInvalid location _failure -> location
+    ExactInductivePreparationFailed location _failure -> location
+    ExactInductiveGuardMissing location -> location
+    ExactInductiveGuardAmbiguous location -> location
+
+renderExactInductiveError :: ExactInductiveError -> Text
+renderExactInductiveError failure =
+    locationToText (exactInductiveErrorLocation failure)
+        <> ": "
+        <> case failure of
+            ExactInductiveUnsupportedBlock{} ->
+                "this inductive source form is not supported by the typed checker"
+            ExactInductiveOccurrenceMissing{} ->
+                "the inductive declaration has no associated syntax occurrence"
+            ExactInductiveOccurrenceAmbiguous{} ->
+                "the inductive declaration has more than one semantic head"
+            ExactInductiveHeadMismatch{} ->
+                "the inductive head does not match its syntax occurrence"
+            ExactInductiveGlossFailed _location glossFailure ->
+                "inductive elaboration failed: " <> shown glossFailure
+            ExactInductiveDuplicateParameter _location parameter ->
+                "the inductive parameter is repeated: " <> shown parameter
+            ExactInductiveDomainFreeVariable _location variable ->
+                "the inductive domain contains an unbound variable: "
+                    <> shown variable
+            ExactInductiveDomainMentionsCarrier{} ->
+                "the inductive domain must be independent of its carrier"
+            ExactInductiveResultShape{} ->
+                "an inductive result must have the form t \\in F(args)"
+            ExactInductiveResultMentionsCarrier{} ->
+                "an inductive result term must not mention its carrier"
+            ExactInductiveRecursiveTermMentionsCarrier{} ->
+                "a recursive occurrence must be in the carrier of a membership premise"
+            ExactInductiveRecursiveCarrierWrongArguments{} ->
+                "the inductive carrier occurs with arguments other than its declared parameters"
+            ExactInductiveRecursiveCarrierOutsideMembership{} ->
+                "an inductive carrier occurrence must be in the set operand of a membership premise"
+            ExactInductiveUnsupportedRecursiveCarrierContext{} ->
+                "this recursive carrier context is outside the supported first-order set-term fragment"
+            ExactInductiveFixedSemanticCollision _location key ->
+                "the inductive carrier collides with fixed semantics for "
+                    <> shown key
+            ExactInductiveGlobalAlreadyVisible _location key ->
+                "the inductive carrier is already visible: " <> shown key
+            ExactInductiveGlobalNotVisible _location symbol ->
+                "an inductive source symbol is not visible: " <> shown symbol
+            ExactInductiveGlobalAmbiguous _location symbol ->
+                "an inductive source symbol has more than one meaning: "
+                    <> shown symbol
+            ExactInductiveUnsupportedSymbol _location symbol ->
+                "this inductive source symbol is not supported: "
+                    <> shown symbol
+            ExactInductiveGlobalContentInvalid _location coreFailure ->
+                "an inductive global has invalid checked content: "
+                    <> shown coreFailure
+            ExactInductivePreparationFailed _location typedFailure ->
+                "typed inductive preparation failed: " <> shown typedFailure
+            ExactInductiveGuardMissing{} ->
+                "an inductive domain guard has no visible authorized fact"
+            ExactInductiveGuardAmbiguous{} ->
+                "an inductive domain guard matches more than one visible fact"
+  where
+    shown :: Show value => value -> Text
+    shown = Text.pack . show
+
+type Prepare =
+    ExceptT
+        ExactInductiveError
+        (Declaration.LoweringDriver)
+
+prepareExactInductive
+    :: CheckedFoundation
+    -> Raw.Block
+    -> [CanonicalLexicalEntry]
+    -> Declaration.LoweringDriver
+        (Either ExactInductiveError PreparedExactInductive)
+prepareExactInductive foundation block entries =
+    Except.runExceptT do
+        (location, marker, rawInductive) <-
+            case block of
+                Raw.BlockInductive blockLocation _title blockMarker inductive ->
+                    pure (blockLocation, blockMarker, inductive)
+                _ ->
+                    Except.throwError
+                        (ExactInductiveUnsupportedBlock (locate block))
+        key <- validateOccurrence location rawInductive entries
+        when
+            (isJust (fixedSemanticMeaning key))
+            (Except.throwError
+                (ExactInductiveFixedSemanticCollision location key))
+        visible <-
+            Except.lift
+                (Declaration.resolveVisibleGlobalLowering key)
+        when (isJust visible)
+            (Except.throwError
+                (ExactInductiveGlobalAlreadyVisible location key))
+        internal <-
+            case Meaning.meaning [block] of
+                Right
+                    [Internal.BlockInductive
+                        _internalLocation _internalMarker inductive] ->
+                            pure inductive
+                Left failure ->
+                    Except.throwError
+                        (ExactInductiveGlossFailed location failure)
+                Right _ ->
+                    Except.throwError
+                        (ExactInductiveUnsupportedBlock location)
+        direct <-
+            Except.liftEither
+                (normalizeDirectInductive internal)
+        (sourceGlobals, globalTypes) <-
+            resolveSourceGlobals location internal direct
+        typed <-
+            Except.liftEither
+                (first
+                    (ExactInductivePreparationFailed location)
+                    (Typed.prepareTypedInductive
+                        (requireGlobalType globalTypes)
+                        foundation
+                        (`Map.lookup` sourceGlobals)
+                        marker
+                        direct))
+        guards <-
+            traverse
+                (resolveGuard location)
+                (Vector.toList
+                    (Typed.typedInductiveGuardTargets typed))
+        theory <- Except.lift Declaration.currentTheoryLowering
+        let carrierType = Typed.typedInductiveCarrierType typed
+            carrierBody = Typed.typedInductiveCarrierBody typed
+            carrierTerm = frozenCoreTerm carrierBody
+            identity =
+                transparentObjectId theory carrierType carrierTerm
+            content =
+                TransparentObjectContent theory carrierType carrierTerm
+            alias = case marker of
+                Raw.Marker name -> semanticName name
+        available <-
+            Except.lift
+                (Declaration.objectAvailableLowering identity)
+        let asserted
+                | available = Nothing
+                | otherwise = Just (assertedObject identity content)
+            syntax =
+                declarationSyntaxId
+                    (encodePreparedInductive key alias typed)
+        pure
+            (PreparedExactInductive
+                location
+                key
+                identity
+                asserted
+                alias
+                syntax
+                typed
+                guards)
+  where
+    requireGlobalType types identity =
+        fromMaybe
+            (impossible
+                "prepared inductive global has no checked type")
+            (Map.lookup identity types)
+
+validateOccurrence
+    :: Location
+    -> Raw.Inductive
+    -> [CanonicalLexicalEntry]
+    -> Prepare SemanticGlobalKey
+validateOccurrence location rawInductive entries = do
+    entry <-
+        case entries of
+            [] ->
+                Except.throwError
+                    (ExactInductiveOccurrenceMissing location)
+            [single] -> pure single
+            _ ->
+                Except.throwError
+                    (ExactInductiveOccurrenceAmbiguous location)
+    key <-
+        maybe
+            (Except.throwError
+                (ExactInductiveHeadMismatch location))
+            pure
+            (semanticGlobalKeyFromLexicalEntry entry)
+    let Raw.SymbolPattern headSymbol _parameters =
+            Raw.inductiveSymbolPattern rawInductive
+        expected =
+            SemanticExpressionFunction
+                (Raw.mixfixPattern headSymbol)
+    unless (key == expected)
+        (Except.throwError
+            (ExactInductiveHeadMismatch location))
+    pure key
+
+normalizeDirectInductive
+    :: Internal.Inductive
+    -> Either ExactInductiveError Typed.DirectInductive
+normalizeDirectInductive inductive = do
+    case firstDuplicate (Internal.inductiveParams inductive) of
+        Just duplicate ->
+            Left
+                (ExactInductiveDuplicateParameter
+                    (locate duplicate)
+                    duplicate)
+        Nothing -> pure ()
+    let parameters = Internal.inductiveParams inductive
+        parameterSet = Set.fromList parameters
+        domain = Internal.inductiveDomain inductive
+        carrier = Internal.inductiveSymbol inductive
+        domainVariables =
+            orderedUnique
+                (toList domain)
+    case find (`Set.notMember` parameterSet) domainVariables of
+        Just variable ->
+            Left
+                (ExactInductiveDomainFreeVariable
+                    (locate variable)
+                    variable)
+        Nothing -> pure ()
+    when
+        (Internal.SymbolMixfix carrier
+            `Set.member` Internal.mentionedSymbols domain)
+        (Left
+            (ExactInductiveDomainMentionsCarrier
+                (termLocation domain)))
+    clauses <-
+        traverse
+            (normalizeClause carrier parameters)
+            (Internal.inductiveIntros inductive)
+    pure
+        (Typed.DirectInductive
+            parameters
+            domain
+            clauses)
+
+normalizeClause
+    :: Internal.FunctionSymbol
+    -> [Internal.VarSymbol]
+    -> Internal.IntroRule
+    -> Either ExactInductiveError Typed.DirectInductiveClause
+normalizeClause carrier parameters rule = do
+    conditions <-
+        traverse
+            (normalizeCondition carrier parameters)
+            (Internal.introConditions rule)
+    result <-
+        normalizeResult
+            carrier
+            parameters
+            (Internal.introResult rule)
+    let parameterSet = Set.fromList parameters
+        variables =
+            List.filter (`Set.notMember` parameterSet)
+                (orderedUnique
+                    ( concatMap toList
+                        (Internal.introConditions rule)
+                      <> toList result
+                    ))
+    pure
+        (Typed.DirectInductiveClause
+            variables
+            conditions
+            result)
+
+normalizeResult
+    :: Internal.FunctionSymbol
+    -> [Internal.VarSymbol]
+    -> Internal.Formula
+    -> Either ExactInductiveError Internal.Term
+normalizeResult carrier parameters = \case
+    Internal.IsElementOf _location result target
+        | not (matchesCarrier carrier parameters target) ->
+            Left (ExactInductiveResultShape (termLocation target))
+        | Internal.SymbolMixfix carrier
+                `Set.member` Internal.mentionedSymbols result ->
+            Left
+                (ExactInductiveResultMentionsCarrier
+                    (termLocation result))
+        | otherwise ->
+            Right result
+    formula ->
+        Left (ExactInductiveResultShape (termLocation formula))
+
+normalizeCondition
+    :: Internal.FunctionSymbol
+    -> [Internal.VarSymbol]
+    -> Internal.Formula
+    -> Either ExactInductiveError Typed.DirectInductiveCondition
+normalizeCondition carrier parameters formula
+    | not
+        (Internal.SymbolMixfix carrier
+            `Set.member` Internal.mentionedSymbols formula) =
+        Right (Typed.DirectSideCondition formula)
+    | otherwise =
+        case formula of
+            Internal.IsElementOf _location recursiveTerm recursiveCarrier
+                | Internal.SymbolMixfix carrier
+                        `Set.member`
+                            Internal.mentionedSymbols recursiveTerm ->
+                    Left
+                        (ExactInductiveRecursiveTermMentionsCarrier
+                            (termLocation recursiveTerm))
+                | otherwise -> do
+                    context <-
+                        first recursiveCarrierContextError
+                            (Typed.prepareRecursiveCarrierContext
+                                carrier parameters recursiveCarrier)
+                    Right
+                        (Typed.DirectRecursiveCondition
+                            recursiveTerm context)
+            _ ->
+                Left
+                    (ExactInductiveRecursiveCarrierOutsideMembership
+                        (termLocation formula))
+
+recursiveCarrierContextError
+    :: Typed.RecursiveCarrierContextError
+    -> ExactInductiveError
+recursiveCarrierContextError = \case
+    Typed.RecursiveCarrierWrongArguments location ->
+        ExactInductiveRecursiveCarrierWrongArguments location
+    Typed.RecursiveCarrierUnsupportedContext location ->
+        ExactInductiveUnsupportedRecursiveCarrierContext location
+
+matchesCarrier
+    :: Internal.FunctionSymbol
+    -> [Internal.VarSymbol]
+    -> Internal.Term
+    -> Bool
+matchesCarrier carrier parameters = \case
+    Internal.TermSymbol _location (Internal.SymbolMixfix actual) arguments ->
+        actual == carrier
+            && length arguments == length parameters
+            && and
+                (zipWith
+                    (\argument parameter ->
+                        argument == Internal.TermVar parameter)
+                    arguments
+                    parameters)
+    _ -> False
+
+resolveSourceGlobals
+    :: Location
+    -> Internal.Inductive
+    -> Typed.DirectInductive
+    -> Prepare
+        ( Map.Map
+            Internal.Symbol
+            (Typed.SourceGlobal ObjectId)
+        , Map.Map ObjectId CoreType
+        )
+resolveSourceGlobals location internal direct =
+    Except.lift
+        (ExactGlobal.resolveExactSourceGlobals symbols)
+        >>= Except.liftEither
+            . first (exactGlobalError location)
+  where
+    carrier = Internal.SymbolMixfix (Internal.inductiveSymbol internal)
+    symbols =
+        Set.delete carrier (directSymbols direct)
+
+exactGlobalError
+    :: Location
+    -> ExactGlobal.ExactGlobalResolutionError
+    -> ExactInductiveError
+exactGlobalError location = \case
+    ExactGlobal.ExactGlobalNotVisible symbol ->
+        ExactInductiveGlobalNotVisible location symbol
+    ExactGlobal.ExactGlobalAmbiguous symbol ->
+        ExactInductiveGlobalAmbiguous location symbol
+    ExactGlobal.ExactGlobalUnsupported symbol ->
+        ExactInductiveUnsupportedSymbol location symbol
+    ExactGlobal.ExactGlobalContextualUnsupported symbol ->
+        ExactInductiveUnsupportedSymbol location symbol
+    ExactGlobal.ExactGlobalContentInvalid failure ->
+        ExactInductiveGlobalContentInvalid location failure
+
+resolveGuard
+    :: Location
+    -> FrozenCheckedCore ObjectId
+    -> Prepare SemanticFactOccurrenceFingerprint
+resolveGuard location target = do
+    matches <-
+        Except.lift
+            (Declaration.resolveVisibleFactTargetsLowering target)
+    case matches of
+        [] ->
+            Except.throwError (ExactInductiveGuardMissing location)
+        [fingerprint] ->
+            pure fingerprint
+        _ ->
+            Except.throwError (ExactInductiveGuardAmbiguous location)
+
+directSymbols :: Typed.DirectInductive -> Set.Set Internal.Symbol
+directSymbols direct =
+    Internal.mentionedSymbols (Typed.directInductiveDomain direct)
+        <> foldMap clauseSymbols
+            (Typed.directInductiveClauses direct)
+  where
+    clauseSymbols clause =
+        foldMap conditionSymbols
+                (Typed.directClauseConditions clause)
+            <> Internal.mentionedSymbols
+                (Typed.directClauseResult clause)
+    conditionSymbols = \case
+        Typed.DirectSideCondition formula ->
+            Internal.mentionedSymbols formula
+        Typed.DirectRecursiveCondition term context ->
+            Internal.mentionedSymbols term
+                <> Typed.recursiveCarrierContextSymbols context
+
+lowerPreparedExactInductive
+    :: PreparedExactInductive
+    -> Declaration.LoweringDriver
+        (Either
+            Declaration.DeclarationError
+            (Declaration.CheckedDeclaration
+                CheckedExactInductiveAuthorization))
+lowerPreparedExactInductive
+        (PreparedExactInductive
+            _location key identity asserted alias syntax typed guards) =
+    do
+        let facts = Typed.typedInductiveFacts typed
+            monotonicities =
+                Vector.toList
+                    (Typed.typedInductiveMonotonicities typed)
+            objects = maybeToList asserted
+        definition <-
+            Declaration.prepareDefinitionEquationSpecLowering
+                objects identity alias
+        preparedMonotonicities <-
+            traverse
+                (\monotonicity -> Except.runExceptT do
+                    let factLocation =
+                            Typed.typedInductiveMonotonicityLocation
+                                monotonicity
+                        target =
+                            Typed.typedInductiveMonotonicityTarget
+                                monotonicity
+                    spec <-
+                        Except.lift
+                            (Declaration.prepareFrozenCandidateSpecLowering
+                                objects target SearchIneligible [])
+                            >>= Except.liftEither
+                    obligation <-
+                        Except.lift
+                            (Declaration.prepareScopedVampireObligationLowering
+                                Vector.empty
+                                (embedClosedCore [] target)
+                                []
+                                []
+                                Declaration.VampireImplicitPremises)
+                            >>= either
+                                (Except.throwError
+                                    . Declaration.ProofObligationFailedAt
+                                        factLocation
+                                    . Declaration.CurrentCandidateVampirePreparationFailed)
+                                pure
+                    pure
+                        ( Declaration.checkedCandidate
+                            spec
+                            (Declaration.checkedSourceProofPlanning
+                                [ Declaration.checkedPlannedVampireRequest
+                                    factLocation obligation
+                                ]
+                                [])
+                        , (factLocation, obligation)
+                        ))
+                monotonicities
+        preparedCandidates <-
+            traverse
+                (\fact -> do
+                    prepared <-
+                        Declaration.prepareCandidateSpecLowering
+                            objects
+                            (embedClosedCore []
+                                (Typed.typedInductiveFactTarget fact))
+                            SearchEligible
+                            [markerAlias
+                                (Typed.typedInductiveFactMarker fact)]
+                    let descriptor =
+                            GuardedFoundationRules
+                                (guardedRuleSet
+                                    (Typed.typedInductiveFactRules fact))
+                        planning
+                            | null monotonicities =
+                                Declaration.checkedKernelPlanning
+                                    descriptor guards
+                            | otherwise =
+                                Declaration.checkedKernelPlanningWithStaged
+                                    descriptor
+                                    guards
+                                    (if Typed.typedInductiveFactRequiresMonotonicities
+                                            fact
+                                        then
+                                            [ Declaration.plannedEarlierCandidate
+                                                1 index
+                                            | (index, _target) <-
+                                                zip [0 ..] monotonicities
+                                            ]
+                                        else [])
+                    pure
+                        (fmap
+                            (\spec ->
+                                Declaration.checkedCandidate spec planning)
+                            prepared))
+                facts
+        pure do
+            definitionSpec <- definition
+            monotonicityCandidates <- sequence preparedMonotonicities
+            factCandidates <- sequence preparedCandidates
+            let stages
+                    | null monotonicityCandidates =
+                        [ Declaration.checkedCandidate definitionSpec
+                            (Declaration.checkedDefinitionEquationPlanning identity)
+                            :| toList factCandidates
+                        ]
+                    | otherwise =
+                        [ Declaration.checkedCandidate definitionSpec
+                            (Declaration.checkedDefinitionEquationPlanning identity)
+                            :| []
+                        , NonEmpty.fromList (fst <$> monotonicityCandidates)
+                        , factCandidates
+                        ]
+            pure
+                (Declaration.checkedCompiledDeclaration
+                    syntax
+                    objects
+                    []
+                    [semanticGlobalBinding key (GlobalReference identity)]
+                    []
+                    stages
+                    (CheckedExactInductiveAuthorization
+                        identity typed guards
+                        (snd <$> monotonicityCandidates)))
+  where
+    markerAlias (Raw.Marker name) =
+        semanticName name
+
+authorizeCheckedExactInductive
+    :: CheckedExactInductiveAuthorization
+    -> [NonEmpty Declaration.ReservedCandidate]
+    -> Declaration.Declaration ()
+authorizeCheckedExactInductive
+        (CheckedExactInductiveAuthorization
+            identity typed guards monotonicityObligations) = \case
+    [definitionCandidate :| candidates] -> do
+        unless (null monotonicityObligations)
+            (Declaration.failDeclaration
+                (Declaration.CheckedAuthorizationCandidateShapeMismatch 3 1))
+        Declaration.authorizeDefinitionEquationCandidate
+            identity definitionCandidate
+        let facts = Typed.typedInductiveFacts typed
+        case NonEmpty.nonEmpty candidates of
+            Just factCandidates
+                | NonEmpty.length factCandidates == NonEmpty.length facts ->
+                    sequence_
+                        (NonEmpty.zipWith
+                            (authorizeFact [])
+                            factCandidates
+                            facts)
+            _ ->
+                Declaration.failDeclaration
+                    (Declaration.CheckedAuthorizationCandidateShapeMismatch
+                        (1 + NonEmpty.length facts)
+                        (1 + length candidates))
+    [ definitionCandidate :| []
+      , monotonicityCandidates
+      , factCandidates
+      ]
+        | NonEmpty.length monotonicityCandidates
+                == length monotonicityObligations
+        , NonEmpty.length factCandidates
+                == NonEmpty.length (Typed.typedInductiveFacts typed) -> do
+            obligations <-
+                maybe
+                    (Declaration.failDeclaration
+                        (Declaration.CheckedAuthorizationCandidateShapeMismatch
+                            1 0))
+                    pure
+                    (NonEmpty.nonEmpty monotonicityObligations)
+            Declaration.authorizeDefinitionEquationCandidate
+                identity definitionCandidate
+            Declaration.authorizeVampireCandidateBatch
+                (NonEmpty.zipWith
+                    (\candidate (factLocation, obligation) ->
+                        (factLocation, candidate, pure obligation))
+                    monotonicityCandidates
+                    obligations)
+            sequence_
+                (NonEmpty.zipWith
+                    (\candidate fact ->
+                        authorizeFact
+                            (if Typed.typedInductiveFactRequiresMonotonicities
+                                    fact
+                                then NonEmpty.toList monotonicityCandidates
+                                else [])
+                            candidate
+                            fact)
+                    factCandidates
+                    (Typed.typedInductiveFacts typed))
+    stages ->
+        Declaration.failDeclaration
+            (Declaration.CheckedAuthorizationCandidateShapeMismatch
+                (if null monotonicityObligations then 1 else 3)
+                (length stages))
+  where
+    authorizeFact monotonicityCandidates candidate fact =
+        Declaration.authorizeKernelConstructionCandidate
+            (GuardedFoundationRules
+                (guardedRuleSet
+                    (Typed.typedInductiveFactRules fact)))
+            candidate do
+                traverse_ Declaration.useAuthorizedFact guards
+                traverse_
+                    Declaration.useStagedCandidate
+                    monotonicityCandidates
+                pure (Typed.typedInductiveFactDerivation fact)
+
+
+encodePreparedInductive
+    :: SemanticGlobalKey
+    -> SemanticName
+    -> Typed.PreparedTypedInductive ObjectId
+    -> ByteString
+encodePreparedInductive key alias typed =
+    encodeCache do
+        putCacheTag 0x04
+        putSemanticGlobalKeyCache key
+        putCoreTypeCache
+            (Typed.typedInductiveCarrierType typed)
+        putCanonicalTermCache putObjectIdCache
+            (frozenCoreTerm
+                (Typed.typedInductiveCarrierBody typed))
+        putCacheList putFrozenTerm
+            (Vector.toList
+                (Typed.typedInductiveContextInventory typed))
+        putCacheList
+            (putFrozenTerm
+                . Typed.typedInductiveMonotonicityTarget)
+            (Vector.toList
+                (Typed.typedInductiveMonotonicities typed))
+        putCacheText (semanticNameText alias)
+        putCacheList putFact
+            (toList (Typed.typedInductiveFacts typed))
+  where
+    putFrozenTerm =
+        putCanonicalTermCache putObjectIdCache . frozenCoreTerm
+
+    putFact fact = do
+        let Raw.Marker marker =
+                Typed.typedInductiveFactMarker fact
+        putCacheText marker
+        putCanonicalTermCache putObjectIdCache
+            (frozenCoreTerm
+                (Typed.typedInductiveFactTarget fact))
+        putCacheList
+            (putCacheBytes . encodeKernelRuleTag)
+            (toList (Typed.typedInductiveFactRules fact))
+
+firstDuplicate :: Ord value => [value] -> Maybe value
+firstDuplicate =
+    go Set.empty
+  where
+    go _seen [] = Nothing
+    go seen (value : remaining)
+        | value `Set.member` seen = Just value
+        | otherwise =
+            go (Set.insert value seen) remaining
+
+orderedUnique :: Ord value => [value] -> [value]
+orderedUnique =
+    reverse . snd . foldl' step (Set.empty, [])
+  where
+    step (seen, values) value
+        | value `Set.member` seen = (seen, values)
+        | otherwise =
+            (Set.insert value seen, value : values)
+
+termLocation :: Internal.Expr -> Location
+termLocation = Internal.exprLocation
diff --git a/source/Felix/Checking/Exact/Proof.hs b/source/Felix/Checking/Exact/Proof.hs
new file mode 100644
index 0000000..e2149c4
--- /dev/null
+++ b/source/Felix/Checking/Exact/Proof.hs
@@ -0,0 +1,2639 @@
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | Exact lowering for the first ordinary theorem/proof fragment.
+--
+-- This module is the trusted owner of structural local-proof composition.  Its
+-- private prepared tree controls when assumptions and proved local claims
+-- become available and executes discharges depth-first.  The declaration
+-- boundary validates typed tasks and authority; it does not reconstruct this
+-- derivation.
+module Felix.Checking.Exact.Proof
+    ( PreparedExactProof
+    , preparedExactProofSyntaxId
+    , preparedExactProofFirstOmission
+    , prepareExactProof
+    , CheckedExactProofAuthorization
+    , lowerPreparedExactProof
+    , authorizeCheckedExactProof
+    , PreparedFinalPreludeFoundationClaim
+    , prepareFinalPreludeFoundationClaim
+    , CheckedFinalPreludeFoundationAuthorization
+    , lowerPreparedFinalPreludeFoundationClaim
+    , authorizeCheckedFinalPreludeFoundationClaim
+    , ExactProofError(..)
+    , exactProofErrorLocation
+    , renderExactProofError
+    ) where
+
+import Base
+import Felix.Checking.Authority qualified as Authority
+import Felix.Checking.Backend.Problem qualified as Backend
+import Felix.Checking.Core
+import Felix.Checking.Declaration qualified as Declaration
+import Felix.Checking.Exact qualified as Exact
+import Felix.Checking.Foundation
+import Felix.Checking.Identity
+import Felix.Checking.Kernel.Derivation (foundationFactDerivation)
+import Felix.Checking.Kernel.Proof qualified as KernelProof
+import Felix.Checking.SetConstruction
+import Felix.Checking.Semantic
+import Felix.Cache.Codec
+import Felix.Report.Location
+import Felix.Syntax.Abstract qualified as Raw
+
+import Control.Monad.Except (ExceptT)
+import Control.Monad.Except qualified as Except
+import Control.Monad (foldM, unless, when)
+import Control.Monad.State.Strict (StateT)
+import Control.Monad.State.Strict qualified as State
+import Data.ByteString (ByteString)
+import Data.List.NonEmpty qualified as NonEmpty
+import Data.Map.Strict qualified as Map
+import Data.Set qualified as Set
+import Data.Text qualified as Text
+import Data.Vector (Vector)
+import Data.Vector qualified as Vector
+import Numeric.Natural (Natural)
+
+
+data ExactProofError
+    = ExactProofUnsupportedClaim !Location
+    | ExactProofUnsupportedStep !Location
+    | ExactProofSetInductionVariableRequired !Location
+    | ExactProofSetInductionVariableNotActive
+        !Location !Raw.VarSymbol
+    | ExactProofSetInductionFocusAmbiguous !Location
+    | ExactProofSetInductionActiveBinderIneligible
+        !Location !Raw.VarSymbol
+    | ExactProofSetInductionBinderConflict
+        !Location !Raw.VarSymbol
+    | ExactProofSetInductionGoalMismatch !Location
+    | ExactProofSetExtensionalityGoalMismatch !Location
+    | ExactProofSetExtensionalityDirectionsUnavailable !Location
+    | ExactProofExpectedUniversalGoal !Location
+    | ExactProofExpectedImplicationGoal !Location
+    | ExactProofGoalStatementMismatch !Location
+    | ExactProofEmptyCaseSplit !Location
+    | ExactProofStructuralCompositionFailed
+        !Location !KernelProof.KernelProofBuildError
+    | ExactProofLocalFunctionBinderMismatch !Location
+    | ExactProofLocalFunctionNameConflict !Location
+    | ExactProofUnknownReference !Location !Raw.Marker
+    | ExactProofElaborationFailed !Exact.ExactCompileError
+    | ExactProofObligationPreparationFailed
+        !Location
+        !(Declaration.VampireObligationPreparationError
+            Exact.ExactLocalId)
+    | ExactProofFoundationLeafRequiresImplicitAuto !Location
+    | ExactProofFoundationLeafTargetMismatch !Location
+    | ExactProofFoundationLeafTargetAmbiguous !Location
+    deriving stock (Show, Eq)
+
+exactProofErrorLocation :: ExactProofError -> Location
+exactProofErrorLocation = \case
+    ExactProofUnsupportedClaim location -> location
+    ExactProofUnsupportedStep location -> location
+    ExactProofSetInductionVariableRequired location -> location
+    ExactProofSetInductionVariableNotActive location _variable ->
+        location
+    ExactProofSetInductionFocusAmbiguous location -> location
+    ExactProofSetInductionActiveBinderIneligible location _variable ->
+        location
+    ExactProofSetInductionBinderConflict location _variable ->
+        location
+    ExactProofSetInductionGoalMismatch location -> location
+    ExactProofSetExtensionalityGoalMismatch location -> location
+    ExactProofSetExtensionalityDirectionsUnavailable location -> location
+    ExactProofExpectedUniversalGoal location -> location
+    ExactProofExpectedImplicationGoal location -> location
+    ExactProofGoalStatementMismatch location -> location
+    ExactProofEmptyCaseSplit location -> location
+    ExactProofStructuralCompositionFailed location _failure -> location
+    ExactProofLocalFunctionBinderMismatch location -> location
+    ExactProofLocalFunctionNameConflict location -> location
+    ExactProofUnknownReference location _marker -> location
+    ExactProofElaborationFailed failure ->
+        Exact.exactCompileErrorLocation failure
+    ExactProofObligationPreparationFailed location _failure -> location
+    ExactProofFoundationLeafRequiresImplicitAuto location -> location
+    ExactProofFoundationLeafTargetMismatch location -> location
+    ExactProofFoundationLeafTargetAmbiguous location -> location
+
+renderExactProofError :: ExactProofError -> Text
+renderExactProofError = \case
+    ExactProofUnsupportedClaim location ->
+        at location <> "this claim is not yet supported by the typed checker"
+    ExactProofUnsupportedStep location ->
+        at location <> "this proof step is not yet supported by the typed checker"
+    ExactProofSetInductionVariableRequired location ->
+        at location <> "exact set induction requires a named set variable"
+    ExactProofSetInductionVariableNotActive location variable ->
+        at location <> "the set-induction variable " <> shown variable
+            <> " is not an eligible exact focus"
+    ExactProofSetInductionFocusAmbiguous location ->
+        at location
+            <> "set induction without an explicit variable has no unique focus"
+    ExactProofSetInductionActiveBinderIneligible location variable ->
+        at location <> "the active binder " <> shown variable
+            <> " is not an eligible set-induction focus"
+    ExactProofSetInductionBinderConflict location variable ->
+        at location <> "the leading set-induction binder " <> shown variable
+            <> " conflicts with an active exact binder"
+    ExactProofSetInductionGoalMismatch location ->
+        at location <> "the set-induction variable does not belong to this goal"
+    ExactProofSetExtensionalityGoalMismatch location ->
+        at location <> "set extensionality requires a set-equality goal"
+    ExactProofSetExtensionalityDirectionsUnavailable location ->
+        at location
+            <> "set extensionality requires both directions as proved local claims"
+    ExactProofExpectedUniversalGoal location ->
+        at location <> "this fix step requires a universal goal"
+    ExactProofExpectedImplicationGoal location ->
+        at location <> "this assume step requires an implication goal"
+    ExactProofGoalStatementMismatch location ->
+        at location <> "the proof step does not match the current goal"
+    ExactProofEmptyCaseSplit location ->
+        at location <> "case analysis requires at least one case"
+    ExactProofStructuralCompositionFailed location failure ->
+        at location <> "invalid structural proof composition: " <> shown failure
+    ExactProofLocalFunctionBinderMismatch location ->
+        at location <> "the function argument must match its domain binder"
+    ExactProofLocalFunctionNameConflict location ->
+        at location <> "the function and argument names must be distinct"
+    ExactProofUnknownReference location marker ->
+        at location <> "the cited fact " <> shown marker <> " is not visible"
+    ExactProofElaborationFailed failure ->
+        Exact.renderExactCompileError failure
+    ExactProofObligationPreparationFailed location failure ->
+        at location <> "the exact proof obligation is invalid: " <> shown failure
+    ExactProofFoundationLeafRequiresImplicitAuto location ->
+        at location
+            <> "a confined foundation claim requires an implicit Auto proof"
+    ExactProofFoundationLeafTargetMismatch location ->
+        at location <> "the claim does not exactly match a foundation axiom"
+    ExactProofFoundationLeafTargetAmbiguous location ->
+        at location <> "the claim matches more than one foundation axiom"
+  where
+    at location = locationToText location <> ": "
+    shown :: Show value => value -> Text
+    shown = Text.pack . show
+
+data ExactLocalOrigin
+    = ExactAssumption
+    | ExactDerivedClaim
+    | ExactLocalDefinition
+    | ExactLocalConstructionExtensional
+    | ExactLocalConstructionEquation
+    deriving stock (Show, Eq, Ord)
+
+data PreparedLocal = PreparedLocal
+    !Backend.LocalPremiseOrdinal
+    !ExactLocalOrigin
+    !(Vector (Exact.ExactLocalId, CoreType))
+    !(ScopedCheckedCore ObjectId)
+
+data PreparedJustification
+    = PreparedAuto
+    | PreparedReferences
+        !(NonEmpty SemanticFactOccurrenceFingerprint)
+    | PreparedLocalOnly
+
+data PreparedDischarge
+    = PreparedVampireDischarge
+        !Location
+        !PreparedJustification
+        !(ScopedCheckedCore ObjectId)
+        !(Declaration.PreparedVampireObligation
+            Exact.ExactLocalId
+            ExactLocalOrigin)
+    | PreparedSetExtensionality
+        !Location
+        !(ScopedCheckedCore ObjectId)
+
+data PreparedCalculationLink = PreparedCalculationLink
+    !(ScopedCheckedCore ObjectId)
+    !PreparedDischarge
+
+-- The private constructor stores every destination with the discharge derived
+-- from its immediately preceding endpoint.  Planning and admission can
+-- therefore traverse one immutable sequence without re-associating shapes.
+data PreparedCalculation = PreparedCheckedCalculation
+    !CoreType
+    ![Exact.ExactLocalId]
+    !(Maybe (ScopedCheckedCore ObjectId))
+    !(ScopedCheckedCore ObjectId)
+    !(NonEmpty PreparedCalculationLink)
+    !(ScopedCheckedCore ObjectId)
+
+data PreparedSinceEvidence
+    = PreparedSinceExisting !PreparedLocal
+    | PreparedSinceDischarged !PreparedDischarge !PreparedLocal
+
+data PreparedCase = PreparedCase
+    !(ScopedCheckedCore ObjectId)
+    !PreparedProof
+
+data PreparedCaseAnalysis = PreparedCaseAnalysis
+    !(ScopedCheckedCore ObjectId)
+    !(NonEmpty PreparedCase)
+    !(ScopedCheckedCore ObjectId)
+    !PreparedDischarge
+
+data InitialSetInductionFocus = InitialSetInductionFocus
+    !Raw.VarSymbol
+    !Exact.ExactLocalId
+    !Natural
+
+data InitialSetInductionView = InitialSetInductionView
+    ![InitialSetInductionFocus]
+    !(Vector (Exact.ExactLocalId, CoreType))
+    !(ScopedCheckedCore ObjectId)
+    ![ScopedCheckedCore ObjectId]
+    !(ScopedCheckedCore ObjectId)
+    !(Maybe Raw.VarSymbol)
+
+data SetInductionBoundary
+    = InitialClaimInduction !InitialSetInductionView
+    -- A direct source-statement goal may retain only its leading binder name.
+    -- Recursive proof transformations deliberately discard this hint.
+    | SourceStatementInduction !(Maybe Raw.VarSymbol)
+    | RecursiveProofInduction
+
+data SelectedSetInductionFocus
+    = SelectedInitialSetInduction !InitialSetInductionFocus
+    | SelectedLeadingSetInduction !(Maybe Raw.VarSymbol)
+
+data PreparedSetInductionFocus
+    = PreparedInitialSetInductionFocus
+        !Exact.ExactLocalId
+        !Natural
+    | PreparedLeadingSetInductionFocus
+        !Exact.ExactLocalId
+
+data PreparedSetInduction = PreparedCheckedSetInduction
+    !PreparedSetInductionFocus
+    !(ScopedCheckedCore ObjectId)
+    ![ScopedCheckedCore ObjectId]
+    !(ScopedCheckedCore ObjectId)
+    !(ScopedCheckedCore ObjectId)
+    !(ScopedCheckedCore ObjectId)
+    !PreparedProof
+
+data PreparedProof
+    = PreparedImplicitAuto !PreparedDischarge
+    | PreparedQed !PreparedDischarge
+    | PreparedOmitted
+        !Location
+        !(ScopedCheckedCore ObjectId)
+    | PreparedFix ![Exact.ExactLocalId] !PreparedProof
+    | PreparedAssume
+        !(ScopedCheckedCore ObjectId)
+        !PreparedProof
+    | PreparedTake
+        ![Exact.ExactLocalId]
+        !(ScopedCheckedCore ObjectId)
+        !PreparedDischarge
+        !PreparedProof
+    | PreparedSetInduction !PreparedSetInduction
+    | PreparedHave
+        !(ScopedCheckedCore ObjectId)
+        !PreparedDischarge
+        !PreparedProof
+    | PreparedSuffices
+        !(ScopedCheckedCore ObjectId)
+        !(ScopedCheckedCore ObjectId)
+        !(ScopedCheckedCore ObjectId)
+        !PreparedDischarge
+        !PreparedProof
+    | PreparedCalculate
+        !PreparedCalculation
+        !PreparedProof
+    | PreparedSince
+        !(ScopedCheckedCore ObjectId)
+        !PreparedSinceEvidence
+        !(ScopedCheckedCore ObjectId)
+        !PreparedDischarge
+        !PreparedProof
+    | PreparedSubclaim
+        !(ScopedCheckedCore ObjectId)
+        !PreparedProof
+        !PreparedProof
+    | PreparedDefine
+        !Exact.ExactLocalId
+        !(ScopedCheckedCore ObjectId)
+        !(NonEmpty (ScopedCheckedCore ObjectId))
+        !PreparedProof
+    | PreparedDefineRelational
+        !Exact.ExactLocalId
+        !(ScopedCheckedCore ObjectId)
+        !PreparedDischarge
+        !(NonEmpty (ScopedCheckedCore ObjectId))
+        !PreparedProof
+    | PreparedDefineFunction
+        !Exact.ExactLocalId
+        !(ScopedCheckedCore ObjectId)
+        !(ScopedCheckedCore ObjectId)
+        !PreparedProof
+    | PreparedByCase !PreparedCaseAnalysis
+    | PreparedByContradiction
+        !(ScopedCheckedCore ObjectId)
+        !(ScopedCheckedCore ObjectId)
+        !(ScopedCheckedCore ObjectId)
+        !PreparedProof
+    | PreparedContradiction
+        !(ScopedCheckedCore ObjectId)
+        !(ScopedCheckedCore ObjectId)
+        !PreparedDischarge
+
+data PreparedExactProof = PreparedExactProof
+    !Location
+    !SemanticName
+    !(ScopedCheckedCore ObjectId)
+    !PreparedProof
+    !ProofSyntaxId
+
+data PreparedFinalPreludeFoundationClaim =
+    PreparedFinalPreludeFoundationClaim
+    !Location
+    !SemanticName
+    !(ScopedCheckedCore ObjectId)
+    !FoundationAxiomTag
+    !ProofSyntaxId
+
+preparedExactProofSyntaxId :: PreparedExactProof -> ProofSyntaxId
+preparedExactProofSyntaxId
+        (PreparedExactProof _location _alias _target _proof syntax) =
+    syntax
+
+preparedExactProofFirstOmission :: PreparedExactProof -> Maybe Location
+preparedExactProofFirstOmission
+        (PreparedExactProof _location _alias _target proof _syntax) =
+    preparedProofFirstOmission proof
+
+data PrepareState = PrepareState
+    { prepareNextLocal :: !Natural
+    , prepareNextPremise :: !Natural
+    }
+
+type Prepare =
+    StateT
+        PrepareState
+        (ExceptT ExactProofError (Declaration.LoweringDriver))
+
+prepareExactProof
+    :: Raw.Block
+    -> Maybe Raw.Proof
+    -> Declaration.LoweringDriver
+        (Either ExactProofError PreparedExactProof)
+prepareExactProof block explicitProof =
+    Except.runExceptT
+        (State.evalStateT prepare initialState)
+  where
+    initialState = PrepareState 0 0
+
+    prepare =
+        case block of
+            Raw.BlockClaim
+                    _kind location _title (Raw.Marker marker)
+                    (Raw.Claim assumptions statement) -> do
+                envelope <-
+                    liftDriver
+                        (Exact.prepareExactClaimEnvelope assumptions statement)
+                        >>= either
+                            (throwProof . ExactProofElaborationFailed)
+                            pure
+                let targetCore = Exact.preparedExactClaimTarget envelope
+                unless (null (scopedCoreContext targetCore))
+                    (throwProof
+                        (ExactProofUnsupportedClaim location))
+                (context, openedGoal, identities) <-
+                    openEnvelopeVariables
+                        targetCore
+                        (Exact.preparedExactClaimVariables envelope)
+                        (Exact.preparedExactClaimContext envelope)
+                (locals, bodyGoal, antecedents) <-
+                    openEnvelopeAntecedents
+                        context
+                        openedGoal
+                        (Exact.preparedExactClaimAntecedentCount envelope)
+                initialInduction <-
+                    prepareInitialSetInductionView
+                        statement
+                        context
+                        (Exact.preparedExactClaimVariables envelope)
+                        identities
+                        antecedents
+                        bodyGoal
+                bodyProof <-
+                    case explicitProof of
+                        Nothing ->
+                            PreparedImplicitAuto
+                                <$> prepareDischarge
+                                    location
+                                    context
+                                    locals
+                                    bodyGoal
+                                    Raw.JustificationEmpty
+                        Just sourceProof ->
+                            prepareProof
+                                location
+                                context
+                                locals
+                                (InitialClaimInduction initialInduction)
+                                bodyGoal
+                                sourceProof
+                let withAssumptions =
+                        foldr PreparedAssume bodyProof antecedents
+                    proof =
+                        case identities of
+                            [] -> withAssumptions
+                            _ -> PreparedFix identities withAssumptions
+                pure
+                    (PreparedExactProof
+                        location
+                        (semanticName marker)
+                        targetCore
+                        proof
+                        (proofSyntaxId
+                            (encodePreparedProof proof)))
+            _ ->
+                throwProof
+                    (ExactProofUnsupportedClaim (locate block))
+
+prepareFinalPreludeFoundationClaim
+    :: CheckedFoundation
+    -> Raw.Block
+    -> Maybe Raw.Proof
+    -> Declaration.LoweringDriver
+        (Either ExactProofError PreparedFinalPreludeFoundationClaim)
+prepareFinalPreludeFoundationClaim foundation block explicitProof =
+    Except.runExceptT do
+        case (block, explicitProof) of
+            ( Raw.BlockClaim
+                    _kind location _title (Raw.Marker marker)
+                    (Raw.Claim assumptions statement)
+              , Nothing
+              ) -> do
+                envelope <-
+                    Except.lift
+                        (Exact.prepareExactClaimEnvelope
+                            assumptions
+                            statement)
+                        >>= either
+                            (Except.throwError
+                                . ExactProofElaborationFailed)
+                            pure
+                unless
+                    ( null (Exact.preparedExactClaimVariables envelope)
+                        && Exact.preparedExactClaimAntecedentCount envelope
+                            == 0
+                    )
+                    (Except.throwError
+                        (ExactProofFoundationLeafRequiresImplicitAuto
+                            location))
+                let target = Exact.preparedExactClaimTarget envelope
+                    matches =
+                        [ tag
+                        | tag <- [minBound .. maxBound]
+                        , target == foundationTarget tag
+                        ]
+                tag <- case matches of
+                    [] ->
+                        Except.throwError
+                            (ExactProofFoundationLeafTargetMismatch location)
+                    [only] ->
+                        pure only
+                    _ ->
+                        Except.throwError
+                            (ExactProofFoundationLeafTargetAmbiguous location)
+                pure
+                    (PreparedFinalPreludeFoundationClaim
+                        location
+                        (semanticName marker)
+                        target
+                        tag
+                        (implicitAutoProofSyntaxId target))
+            (Raw.BlockClaim _kind location _title _marker _claim, Just{}) ->
+                Except.throwError
+                    (ExactProofFoundationLeafRequiresImplicitAuto location)
+            _ ->
+                Except.throwError
+                    (ExactProofUnsupportedClaim (locate block))
+  where
+    foundationTarget tag =
+        embedClosedCore []
+            (mapFrozenGlobals
+                absurd
+                (foundationAxiomFrozen foundation tag))
+
+openEnvelopeVariables
+    :: ScopedCheckedCore ObjectId
+    -> [Raw.VarSymbol]
+    -> Exact.ExactBinderContext
+    -> Prepare
+        ( Exact.ExactBinderContext
+        , ScopedCheckedCore ObjectId
+        , [Exact.ExactLocalId]
+        )
+openEnvelopeVariables target variables preparedContext =
+    case NonEmpty.nonEmpty variables of
+        Nothing ->
+            pure (preparedContext, target, [])
+        Just nonempty -> do
+            (_unannotated, opened, identities) <-
+                openFixedVariables
+                Exact.emptyExactBinderContext
+                target
+                nonempty
+            let expected =
+                    reverse
+                        (fst <$> toList
+                            (Exact.exactBinderContextSupport preparedContext))
+            unless
+                (identities == expected)
+                (impossible
+                    "prepared claim annotations do not match opened binders")
+            pure (preparedContext, opened, identities)
+
+openEnvelopeAntecedents
+    :: Exact.ExactBinderContext
+    -> ScopedCheckedCore ObjectId
+    -> Natural
+    -> Prepare
+        ( [PreparedLocal]
+        , ScopedCheckedCore ObjectId
+        , [ScopedCheckedCore ObjectId]
+        )
+openEnvelopeAntecedents context initialGoal initialCount =
+    go [] [] initialGoal initialCount
+  where
+    go locals antecedents goal 0 =
+        pure (locals, goal, antecedents)
+    go locals antecedents goal remaining = do
+        (antecedent, conclusion) <-
+            maybe
+                (impossible
+                    "a prepared claim envelope has too few implications")
+                pure
+                (openScopedImplication goal)
+        local <- allocateLocal ExactAssumption context antecedent
+        go
+            (locals <> [local])
+            (antecedents <> [antecedent])
+            conclusion
+            (remaining - 1)
+
+prepareInitialSetInductionView
+    :: Raw.Stmt
+    -> Exact.ExactBinderContext
+    -> [Raw.VarSymbol]
+    -> [Exact.ExactLocalId]
+    -> [ScopedCheckedCore ObjectId]
+    -> ScopedCheckedCore ObjectId
+    -> Prepare InitialSetInductionView
+prepareInitialSetInductionView
+        statement context variables identities antecedents bodyGoal = do
+    unless (length variables == length identities)
+        (impossible
+            "opened claim binders lost their source identity association")
+    foci <- traverse checkedFocus (zip variables identities)
+    let property = foldr implyChecked bodyGoal antecedents
+        support = Exact.exactBinderContextSupport context
+    unless
+        ( scopedCoreContext property
+            == (snd <$> Vector.toList support)
+        )
+        (impossible
+            "initial set-induction property changed its checked context")
+    pure
+        (InitialSetInductionView
+            foci support property antecedents bodyGoal
+            (claimLeadingUniversalName statement))
+  where
+    checkedFocus (variable, identity) = do
+        index <-
+            maybe
+                (impossible
+                    "an opened claim binder is absent from its exact context")
+                pure
+                (Exact.exactBinderContextIndex variable context)
+        case Exact.exactBinderContextSupport context
+                Vector.!? (fromIntegral index) of
+            Just (actualIdentity, TySet)
+                | actualIdentity == identity ->
+                    pure
+                        (InitialSetInductionFocus
+                            variable identity index)
+            _ ->
+                impossible
+                    "an initial set-induction focus changed identity or type"
+
+    implyChecked antecedent conclusion =
+        fromMaybe
+            (impossible
+                "an exact claim antecedent changed context")
+            (implyScopedCore antecedent conclusion)
+
+claimLeadingUniversalName :: Raw.Stmt -> Maybe Raw.VarSymbol
+claimLeadingUniversalName = \case
+    Raw.StmtFormula
+            (Raw.FormulaQuantified _location Raw.Universally
+                (variable :| _rest) _bound _formula) ->
+        Just variable
+    Raw.SymbolicForall _location (variable :| _rest)
+            _bound _suchThat _statement ->
+        Just variable
+    Raw.StmtQuantPhrase
+            _location
+            (Raw.QuantPhrase Raw.Universally
+                (Raw.NounPhrase _left _noun variables _right _suchThat))
+            _statement ->
+        listToMaybe variables
+    Raw.StmtVerbPhrase
+            (Raw.TermQuantified Raw.Universally _location
+                (Raw.NounPhrase _left _noun variable _right _suchThat)
+                :| [])
+            _verb ->
+        variable
+    Raw.StmtNoun
+            (Raw.TermQuantified Raw.Universally _location
+                (Raw.NounPhrase _left _noun variable _right _suchThat)
+                :| [])
+            _nounPhrase ->
+        variable
+    _statement ->
+        Nothing
+
+prepareProof
+    :: Location
+    -> Exact.ExactBinderContext
+    -> [PreparedLocal]
+    -> SetInductionBoundary
+    -> ScopedCheckedCore ObjectId
+    -> Raw.Proof
+    -> Prepare PreparedProof
+prepareProof fallback context locals inductionBoundary goal = \case
+    Raw.Omitted location ->
+        pure (PreparedOmitted location goal)
+    Raw.Qed maybeLocation justification ->
+        PreparedQed
+            <$> prepareDischarge
+                (fromMaybe fallback maybeLocation)
+                context
+                locals
+                goal
+                justification
+    Raw.FixSymbolic location variables bound continuation -> do
+        (context', goal', identities) <-
+            openFixedVariables context goal variables
+        case bound of
+            Raw.Unbounded ->
+                PreparedFix identities
+                    <$> prepareProof
+                        fallback
+                        context'
+                        locals
+                        RecursiveProofInduction
+                        goal'
+                        continuation
+            _ -> do
+                constraint <-
+                    prepareSymbolicBoundConstraints
+                        context' variables bound
+                prepareGuardedFix
+                    fallback location context' locals goal'
+                    identities constraint continuation
+    Raw.FixSuchThat location variables statement continuation -> do
+        (context', goal', identities) <-
+            openFixedVariables context goal variables
+        constraint <-
+            Exact.preparedExactPropositionCore
+                <$> prepareStatement context' statement
+        prepareGuardedFix
+            fallback location context' locals goal'
+            identities constraint continuation
+    Raw.Assume location statement continuation -> do
+        supplied <- prepareStatement context statement
+        when (isNothing (openScopedImplication goal))
+            (throwProof (ExactProofExpectedImplicationGoal location))
+        (assumption, conclusion) <-
+            maybe
+                (throwProof (ExactProofGoalStatementMismatch location))
+                pure
+                (openScopedAssumption
+                    (Exact.preparedExactPropositionCore supplied)
+                    goal)
+        local <- allocateLocal ExactAssumption context assumption
+        PreparedAssume assumption
+            <$> prepareProof
+                fallback
+                context
+                (locals <> [local])
+                RecursiveProofInduction
+                conclusion
+                continuation
+    Raw.TakeVar location variables bound statement justification continuation -> do
+        prepareSymbolicTake
+            fallback location context locals goal variables bound statement
+            justification continuation
+    Raw.TakeNoun location nounPhrase justification continuation ->
+        prepareNounTake
+            fallback location context locals goal nounPhrase
+            justification continuation
+    Raw.BySetInduction location variable continuation ->
+        prepareSetInduction
+            fallback location context locals inductionBoundary goal
+            variable continuation
+    Raw.Have location Nothing
+            (Raw.SymbolicExists _existential variables bound statement)
+            justification continuation ->
+        prepareSymbolicTake
+            fallback location context locals goal variables bound statement
+            justification continuation
+    Raw.Have location Nothing statement justification continuation -> do
+        claim <-
+            Exact.preparedExactPropositionCore
+                <$> prepareStatement context statement
+        discharge <-
+            prepareDischarge
+                location context locals claim justification
+        local <- allocateLocal ExactDerivedClaim context claim
+        PreparedHave claim discharge
+            <$> prepareProof
+                fallback
+                context
+                (locals <> [local])
+                RecursiveProofInduction
+                goal
+                continuation
+    Raw.Have location (Just sinceStatement)
+            statement justification continuation -> do
+        sinceProposition <-
+            Exact.preparedExactPropositionCore
+                <$> prepareStatement context sinceStatement
+        claim <-
+            Exact.preparedExactPropositionCore
+                <$> prepareStatement context statement
+        (evidence, sinceLocals) <-
+            case find (localMatches sinceProposition) locals of
+                Just existing ->
+                    pure (PreparedSinceExisting existing, locals)
+                Nothing -> do
+                    discharge <-
+                        prepareDischarge
+                            location
+                            context
+                            locals
+                            sinceProposition
+                            Raw.JustificationLocal
+                    local <-
+                        allocateLocal
+                            ExactDerivedClaim context sinceProposition
+                    pure
+                        ( PreparedSinceDischarged discharge local
+                        , locals <> [local]
+                        )
+        claimDischarge <-
+            prepareDischarge
+                location context sinceLocals claim justification
+        claimLocal <-
+            allocateLocal ExactDerivedClaim context claim
+        PreparedSince
+            sinceProposition evidence claim claimDischarge
+            <$> prepareProof
+                fallback
+                context
+                (sinceLocals <> [claimLocal])
+                RecursiveProofInduction
+                goal
+                continuation
+    Raw.Suffices location statement justification continuation -> do
+        reduction <-
+            Exact.preparedExactPropositionCore
+                <$> prepareStatement context statement
+        implication <-
+            maybe
+                (impossible
+                    "a checked suffices reduction changed lexical context")
+                pure
+                (implyScopedCore reduction goal)
+        discharge <-
+            prepareDischarge
+                location context locals implication justification
+        PreparedSuffices goal reduction implication discharge
+            <$> prepareProof
+                fallback
+                context
+                locals
+                (SourceStatementInduction
+                    (claimLeadingUniversalName statement))
+                reduction
+                continuation
+    Raw.Calc location quantifier calculation continuation -> do
+        prepared <-
+            prepareCalculation
+                location context locals quantifier calculation
+        local <-
+            allocateLocal
+                ExactDerivedClaim
+                context
+                (preparedCalculationResult prepared)
+        PreparedCalculate prepared
+            <$> prepareProof
+                fallback
+                context
+                (locals <> [local])
+                RecursiveProofInduction
+                goal
+                continuation
+    Raw.Subclaim location statement subproof continuation -> do
+        claim <-
+            Exact.preparedExactPropositionCore
+                <$> prepareStatement context statement
+        preparedSubproof <-
+            prepareProof
+                location
+                context
+                locals
+                (SourceStatementInduction
+                    (claimLeadingUniversalName statement))
+                claim
+                subproof
+        local <- allocateLocal ExactDerivedClaim context claim
+        PreparedSubclaim claim preparedSubproof
+            <$> prepareProof
+                fallback
+                context
+                (locals <> [local])
+                RecursiveProofInduction
+                goal
+                continuation
+    Raw.Define location variable expression continuation -> do
+        preparedBody <-
+            liftDriver
+                (Exact.prepareExactSetExpression context expression)
+                >>= either
+                    (throwProof . ExactProofElaborationFailed)
+                    pure
+        let body = Exact.preparedExactSetExpressionCore preparedBody
+        identity <- allocateLocalIdentity
+        context' <-
+            either
+                (throwProof . ExactProofElaborationFailed)
+                pure
+                (Exact.extendExactBinderContext
+                    ((identity, variable) :| [])
+                    context)
+        case Exact.preparedExactSetExpressionConstruction preparedBody of
+            Nothing -> do
+                separationCharacteristic <-
+                    liftDriver
+                        (Declaration.currentFoundationAxiomLowering
+                            SeparationCharacteristic)
+                definition <-
+                    maybe
+                        (impossible
+                            "an exact set expression did not form a local definition")
+                        pure
+                        (scopedSetDefinition separationCharacteristic body)
+                local <-
+                    allocateLocal ExactLocalDefinition context' definition
+                PreparedDefine identity body (definition :| [])
+                    <$> prepareProof
+                        fallback context' (locals <> [local])
+                        RecursiveProofInduction
+                        (weakenCheckedScopedCore TySet goal)
+                        continuation
+            Just (Exact.PreparedUnconditionalSetConstruction construction) -> do
+                characteristics <- prepareConstructionFoundation
+                (extensional, equation) <-
+                    maybe
+                        (impossible
+                            "a checked named construction has no definition views")
+                        pure
+                        (namedSetConstructionLocalViews
+                            characteristics construction)
+                extensionalLocal <-
+                    allocateLocal
+                        ExactLocalConstructionExtensional context' extensional
+                equationLocal <-
+                    allocateLocal
+                        ExactLocalConstructionEquation context' equation
+                PreparedDefine identity body (extensional :| [equation])
+                    <$> prepareProof
+                        fallback context'
+                        (locals <> [extensionalLocal, equationLocal])
+                        RecursiveProofInduction
+                        (weakenCheckedScopedCore TySet goal)
+                        continuation
+            Just (Exact.PreparedRelationalSetConstruction construction) -> do
+                characteristics <- prepareConstructionFoundation
+                let functionality =
+                        relationalSetConstructionFunctionality construction
+                discharge <-
+                    prepareDischarge
+                        location context locals functionality
+                        Raw.JustificationEmpty
+                (extensional, equation) <-
+                    maybe
+                        (impossible
+                            "a checked relational construction has no admitted definition views")
+                        pure
+                        (relationalSetConstructionLocalViews
+                            characteristics construction functionality)
+                extensionalLocal <-
+                    allocateLocal
+                        ExactLocalConstructionExtensional context' extensional
+                equationLocal <-
+                    allocateLocal
+                        ExactLocalConstructionEquation context' equation
+                PreparedDefineRelational
+                    identity body discharge (extensional :| [equation])
+                    <$> prepareProof
+                        fallback context'
+                        (locals <> [extensionalLocal, equationLocal])
+                        RecursiveProofInduction
+                        (weakenCheckedScopedCore TySet goal)
+                        continuation
+    Raw.DefineFunction
+            location function argument value bound domain continuation -> do
+        unless (argument == bound)
+            (throwProof
+                (ExactProofLocalFunctionBinderMismatch (locate bound)))
+        when (function == argument)
+            (throwProof
+                (ExactProofLocalFunctionNameConflict (locate function)))
+        argumentIdentity <- allocateLocalIdentity
+        argumentContext <-
+            either
+                (throwProof . ExactProofElaborationFailed)
+                pure
+                (Exact.extendExactBinderContext
+                    ((argumentIdentity, argument) :| [])
+                    context)
+        graph <-
+            liftDriver
+                (Exact.prepareExactLocalFunctionGraph
+                    location context argumentContext domain value)
+                >>= either
+                    (throwProof . ExactProofElaborationFailed)
+                    pure
+        functionIdentity <- allocateLocalIdentity
+        functionContext <-
+            either
+                (throwProof . ExactProofElaborationFailed)
+                pure
+                (Exact.extendExactBinderContext
+                    ((functionIdentity, function) :| [])
+                    context)
+        replacementCharacteristic <-
+            liftDriver
+                (Declaration.currentFoundationAxiomLowering
+                    ReplacementCharacteristic)
+        definition <-
+            maybe
+                (impossible
+                    "a checked replacement graph did not form a local definition")
+                pure
+                (scopedCharacteristicDefinition
+                    replacementCharacteristic
+                    (Exact.preparedExactLocalFunctionGraphCore graph)
+                    ( Exact.preparedExactLocalFunctionGraphDomain graph
+                        :| [Exact.preparedExactLocalFunctionGraphMap graph]
+                    ))
+        local <-
+            allocateLocal ExactLocalDefinition functionContext definition
+        PreparedDefineFunction
+            functionIdentity
+            (Exact.preparedExactLocalFunctionGraphCore graph)
+            definition
+            <$> prepareProof
+                fallback
+                functionContext
+                (locals <> [local])
+                RecursiveProofInduction
+                (weakenCheckedScopedCore TySet goal)
+                continuation
+    Raw.ByCase location sourceCases ->
+        prepareByCase
+            location context locals goal sourceCases
+    Raw.ByContradiction location continuation -> do
+        let falsum = falsumScopedCore (scopedCoreContext goal)
+        negation <-
+            maybe
+                (structuralFailure
+                    location
+                    "proof by contradiction requires a proposition goal")
+                pure
+                (negateScopedCore goal)
+        local <- allocateLocal ExactAssumption context negation
+        prepared <-
+            prepareProof
+                location
+                context
+                (locals <> [local])
+                RecursiveProofInduction
+                falsum
+                continuation
+        validateStructuralComposition
+            location [goal, negation, falsum]
+            (\foundation globalType ->
+                KernelProof.validateDoubleNegationComposition
+                    foundation globalType goal negation falsum)
+        pure
+            (PreparedByContradiction
+                goal negation falsum prepared)
+    Raw.Contradiction location justification -> do
+        let falsum = falsumScopedCore (scopedCoreContext goal)
+        discharge <-
+            prepareDischarge
+                location
+                context
+                locals
+                falsum
+                justification
+        validateStructuralComposition
+            location [goal, falsum]
+            (\foundation globalType ->
+                KernelProof.validateFalsumEliminationComposition
+                    foundation globalType goal falsum)
+        pure (PreparedContradiction goal falsum discharge)
+    proof ->
+        throwProof
+            (ExactProofUnsupportedStep
+                (proofLocation fallback proof))
+  where
+    localMatches proposition
+            (PreparedLocal _ordinal _origin _support local) =
+        local == proposition
+
+prepareSetInduction
+    :: Location
+    -> Location
+    -> Exact.ExactBinderContext
+    -> [PreparedLocal]
+    -> SetInductionBoundary
+    -> ScopedCheckedCore ObjectId
+    -> Maybe Raw.Term
+    -> Raw.Proof
+    -> Prepare PreparedProof
+prepareSetInduction
+        fallback location context locals boundary goal sourceFocus
+        continuation = do
+    selected <-
+        selectSetInductionFocus
+            location context boundary goal sourceFocus
+    case selected of
+        SelectedInitialSetInduction
+                (InitialSetInductionFocus _variable identity index) -> do
+            (foci, expectedSupport, property, antecedents, childTarget) <-
+                case boundary of
+                    InitialClaimInduction
+                            (InitialSetInductionView
+                                foundFoci support foundProperty
+                                foundAntecedents foundTarget _leadingName) ->
+                        pure
+                            ( foundFoci
+                            , support
+                            , foundProperty
+                            , foundAntecedents
+                            , foundTarget
+                            )
+                    RecursiveProofInduction ->
+                        impossible
+                            "an initial induction focus escaped its claim boundary"
+                    SourceStatementInduction _leadingName ->
+                        impossible
+                            "an initial induction focus escaped its claim boundary"
+            unless
+                ( Exact.exactBinderContextSupport context == expectedSupport
+                    && goal == childTarget
+                    && any (sameInitialFocus identity index) foci
+                )
+                (throwProof
+                    (ExactProofSetInductionGoalMismatch location))
+            PreparedSetInduction
+                <$> prepareCheckedSetInduction
+                    fallback location context locals
+                    (PreparedInitialSetInductionFocus identity index)
+                    index property antecedents childTarget continuation
+        SelectedLeadingSetInduction sourceName -> do
+            (binderType, property) <-
+                maybe
+                    (throwProof
+                        (ExactProofSetInductionGoalMismatch location))
+                    pure
+                    (openScopedForall goal)
+            unless (binderType == TySet)
+                (throwProof
+                    (ExactProofSetInductionGoalMismatch location))
+            identity <- allocateLocalIdentity
+            extendedContext <-
+                either
+                    (throwProof . ExactProofElaborationFailed)
+                    pure
+                    (case sourceName of
+                        Just variable ->
+                            Exact.extendExactBinderContext
+                                ((identity, variable) :| [])
+                                context
+                        Nothing ->
+                            Exact.extendExactAnonymousBinderContext
+                                identity context)
+            let expectedResult = weakenCheckedScopedCore TySet goal
+            prepared <- prepareCheckedSetInduction
+                fallback location extendedContext locals
+                (PreparedLeadingSetInductionFocus identity)
+                0 property [] property continuation
+            unless
+                (preparedSetInductionResult prepared == expectedResult)
+                (throwProof
+                    (ExactProofSetInductionGoalMismatch location))
+            pure (PreparedSetInduction prepared)
+  where
+    sameInitialFocus expectedIdentity expectedIndex
+            (InitialSetInductionFocus _variable identity index) =
+        identity == expectedIdentity && index == expectedIndex
+
+prepareCheckedSetInduction
+    :: Location
+    -> Location
+    -> Exact.ExactBinderContext
+    -> [PreparedLocal]
+    -> PreparedSetInductionFocus
+    -> Natural
+    -> ScopedCheckedCore ObjectId
+    -> [ScopedCheckedCore ObjectId]
+    -> ScopedCheckedCore ObjectId
+    -> Raw.Proof
+    -> Prepare PreparedSetInduction
+prepareCheckedSetInduction
+        fallback location context locals focus selected property antecedents
+        childTarget continuation = do
+    (_predicate, hypothesis, _step, result) <-
+        maybe
+            (throwProof
+                (ExactProofSetInductionGoalMismatch location))
+            pure
+            (scopedSetInductionInstance selected property)
+    validateStructuralComposition
+        location
+        (property : hypothesis : result : childTarget : antecedents)
+        (\foundation globalType ->
+            KernelProof.validateSetInductionComposition
+                foundation globalType selected property antecedents
+                childTarget hypothesis result)
+    local <- allocateLocal ExactAssumption context hypothesis
+    child <-
+        prepareProof
+            fallback
+            context
+            (locals <> [local])
+            RecursiveProofInduction
+            childTarget
+            continuation
+    pure
+        (PreparedCheckedSetInduction
+            focus property antecedents childTarget hypothesis result child)
+
+preparedSetInductionResult
+    :: PreparedSetInduction
+    -> ScopedCheckedCore ObjectId
+preparedSetInductionResult
+        (PreparedCheckedSetInduction
+            _focus _property _antecedents _target _hypothesis result _child) =
+    result
+
+selectSetInductionFocus
+    :: Location
+    -> Exact.ExactBinderContext
+    -> SetInductionBoundary
+    -> ScopedCheckedCore ObjectId
+    -> Maybe Raw.Term
+    -> Prepare SelectedSetInductionFocus
+selectSetInductionFocus location context boundary goal sourceFocus = do
+    explicit <- traverse simpleVariable sourceFocus
+    let (initialFoci, retainedLeadingName) =
+            case boundary of
+                InitialClaimInduction
+                        (InitialSetInductionView
+                            foci _support _property _antecedents _target
+                            leadingName) ->
+                    (foci, leadingName)
+                SourceStatementInduction leadingName ->
+                    ([], leadingName)
+                RecursiveProofInduction ->
+                    ([], Nothing)
+        leadingAvailable =
+            case openScopedForall goal of
+                Just (TySet, _body) -> True
+                _ -> False
+    case explicit of
+        Just variable ->
+            case find (initialNamed variable) initialFoci of
+                Just focus ->
+                    pure (SelectedInitialSetInduction focus)
+                Nothing
+                    | leadingAvailable
+                    , isJust
+                        (Exact.exactBinderContextIndex variable context) ->
+                        throwProof
+                            (ExactProofSetInductionBinderConflict
+                                location variable)
+                    | leadingAvailable ->
+                        pure
+                            (SelectedLeadingSetInduction
+                                (Just variable))
+                    | isJust
+                        (Exact.exactBinderContextIndex variable context) ->
+                        throwProof
+                            (ExactProofSetInductionActiveBinderIneligible
+                                location variable)
+                    | otherwise ->
+                        throwProof
+                            (ExactProofSetInductionVariableNotActive
+                                location variable)
+        Nothing ->
+            case
+                ( (SelectedInitialSetInduction <$> initialFoci)
+                    <> [ SelectedLeadingSetInduction retainedLeadingName
+                       | leadingAvailable
+                       ]
+                ) of
+                [only] -> pure only
+                _ ->
+                    throwProof
+                        (ExactProofSetInductionFocusAmbiguous location)
+  where
+    simpleVariable = \case
+        Raw.TermExpr (Raw.ExprVar variable) ->
+            pure variable
+        _term ->
+            throwProof
+                (ExactProofSetInductionVariableRequired location)
+
+    initialNamed variable
+            (InitialSetInductionFocus candidate _identity _index) =
+        candidate == variable
+
+prepareByCase
+    :: Location
+    -> Exact.ExactBinderContext
+    -> [PreparedLocal]
+    -> ScopedCheckedCore ObjectId
+    -> [Raw.Case]
+    -> Prepare PreparedProof
+prepareByCase location context locals goal sourceCases = do
+    cases <-
+        maybe
+            (throwProof (ExactProofEmptyCaseSplit location))
+            (traverse prepareCase)
+            (NonEmpty.nonEmpty sourceCases)
+    exhaustive <-
+        foldM disjoin
+            (preparedCaseAssumption (NonEmpty.head cases))
+            (preparedCaseAssumption <$> NonEmpty.tail cases)
+    discharge <-
+        prepareDischarge
+            location context locals exhaustive Raw.JustificationEmpty
+    validateStructuralComposition
+        location
+        (goal : exhaustive : (preparedCaseAssumption <$> toList cases))
+        (\foundation globalType ->
+            KernelProof.validateCaseAnalysisComposition
+                foundation
+                globalType
+                goal
+                (preparedCaseAssumption <$> cases)
+                exhaustive)
+    pure
+        (PreparedByCase
+            (PreparedCaseAnalysis goal cases exhaustive discharge))
+  where
+    prepareCase (Raw.Case statement child) = do
+        assumption <-
+            Exact.preparedExactPropositionCore
+                <$> prepareStatement context statement
+        local <- allocateLocal ExactAssumption context assumption
+        prepared <-
+            prepareProof
+                (locate statement)
+                context
+                (locals <> [local])
+                RecursiveProofInduction
+                goal
+                child
+        pure (PreparedCase assumption prepared)
+
+    disjoin left right =
+        maybe
+            (structuralFailure
+                location
+                "case assumptions changed type or lexical context")
+            pure
+            (disjoinScopedCore left right)
+
+preparedCaseAssumption
+    :: PreparedCase
+    -> ScopedCheckedCore ObjectId
+preparedCaseAssumption (PreparedCase assumption _proof) =
+    assumption
+
+preparedCaseProof :: PreparedCase -> PreparedProof
+preparedCaseProof (PreparedCase _assumption proof) =
+    proof
+
+prepareGuardedFix
+    :: Location
+    -> Location
+    -> Exact.ExactBinderContext
+    -> [PreparedLocal]
+    -> ScopedCheckedCore ObjectId
+    -> [Exact.ExactLocalId]
+    -> ScopedCheckedCore ObjectId
+    -> Raw.Proof
+    -> Prepare PreparedProof
+prepareGuardedFix
+        fallback location context locals goal identities constraint continuation = do
+    (antecedent, conclusion) <-
+        maybe
+            (throwProof (ExactProofExpectedImplicationGoal location))
+            pure
+            (openScopedImplication goal)
+    unless (constraint == antecedent)
+        (throwProof (ExactProofGoalStatementMismatch location))
+    local <- allocateLocal ExactAssumption context constraint
+    prepared <-
+        prepareProof
+            fallback
+            context
+            (locals <> [local])
+            RecursiveProofInduction
+            conclusion
+            continuation
+    pure (PreparedFix identities (PreparedAssume constraint prepared))
+
+prepareCalculation
+    :: Location
+    -> Exact.ExactBinderContext
+    -> [PreparedLocal]
+    -> Maybe Raw.CalcQuantifier
+    -> Raw.Calc
+    -> Prepare PreparedCalculation
+prepareCalculation location context locals quantifier calculation = do
+    (identities, calculationContext, calculationGuard) <-
+        prepareCalculationScope context quantifier
+    case calculation of
+        Raw.Equation first destinations -> do
+            firstChecked <- prepareSetEndpoint calculationContext first
+            checkedDestinations <-
+                traverse
+                    (\(destination, justification) -> do
+                        checked <-
+                            prepareSetEndpoint calculationContext destination
+                        pure
+                            ( locate destination
+                            , checked
+                            , justification
+                            ))
+                    destinations
+            finishCalculation
+                location context locals TySet identities calculationGuard
+                firstChecked checkedDestinations
+        Raw.Biconditionals first destinations -> do
+            firstChecked <- preparePropositionEndpoint calculationContext first
+            checkedDestinations <-
+                traverse
+                    (\(destination, justification) -> do
+                        checked <-
+                            preparePropositionEndpoint
+                                calculationContext destination
+                        pure
+                            ( locate destination
+                            , checked
+                            , justification
+                            ))
+                    destinations
+            finishCalculation
+                location context locals TyProp identities calculationGuard
+                firstChecked checkedDestinations
+  where
+    prepareSetEndpoint endpointContext expression =
+        Exact.preparedExactSetExpressionCore
+            <$> ( liftDriver
+                    (Exact.prepareExactSetExpression
+                        endpointContext expression)
+                    >>= either
+                        (throwProof . ExactProofElaborationFailed)
+                        pure
+                )
+
+    preparePropositionEndpoint endpointContext formula =
+        Exact.preparedExactPropositionCore
+            <$> prepareStatement endpointContext (Raw.StmtFormula formula)
+
+prepareCalculationScope
+    :: Exact.ExactBinderContext
+    -> Maybe Raw.CalcQuantifier
+    -> Prepare
+        ( [Exact.ExactLocalId]
+        , Exact.ExactBinderContext
+        , Maybe (ScopedCheckedCore ObjectId)
+        )
+prepareCalculationScope context = \case
+    Nothing ->
+        pure ([], context, Nothing)
+    Just (Raw.CalcQuantifier variables bound suchThat) -> do
+        identities <- traverse (const allocateLocalIdentity) variables
+        calculationContext <-
+            either
+                (throwProof . ExactProofElaborationFailed)
+                pure
+                (Exact.extendExactBinderContext
+                    (NonEmpty.zip identities variables)
+                    context)
+        boundGuard <-
+            prepareSymbolicBoundConstraints
+                calculationContext variables bound
+        suchThatGuard <-
+            traverse
+                (fmap Exact.preparedExactPropositionCore
+                    . prepareStatement calculationContext)
+                suchThat
+        calculationGuard <-
+            normalizeCalculationGuard
+                (boundGuard : maybeToList suchThatGuard)
+        pure (toList identities, calculationContext, calculationGuard)
+
+normalizeCalculationGuard
+    :: [ScopedCheckedCore ObjectId]
+    -> Prepare (Maybe (ScopedCheckedCore ObjectId))
+normalizeCalculationGuard guards =
+    foldM add Nothing guards
+  where
+    add accumulated constraint
+        | isScopedTruth constraint = pure accumulated
+        | otherwise =
+            case accumulated of
+                Nothing -> pure (Just constraint)
+                Just previous ->
+                    Just
+                        <$> maybe
+                            (impossible
+                                "checked calculation guards changed context")
+                            pure
+                            (conjoinScopedCore previous constraint)
+
+    isScopedTruth proposition =
+        scopedCoreType proposition == TyProp
+            && scopedCoreTerm proposition == CImp CFalsum CFalsum
+
+finishCalculation
+    :: Location
+    -> Exact.ExactBinderContext
+    -> [PreparedLocal]
+    -> CoreType
+    -> [Exact.ExactLocalId]
+    -> Maybe (ScopedCheckedCore ObjectId)
+    -> ScopedCheckedCore ObjectId
+    -> NonEmpty
+        ( Location
+        , ScopedCheckedCore ObjectId
+        , Raw.Justification
+        )
+    -> Prepare PreparedCalculation
+finishCalculation
+        fallback context locals operandType identities calculationGuard
+        first destinations = do
+    links <- prepareCalculationLinks first destinations
+    let finalEndpoint = preparedCalculationLinkDestination (NonEmpty.last links)
+    resultOpen <-
+        calculationEquality first finalEndpoint
+    result <-
+        closeCalculationProposition identities calculationGuard resultOpen
+    pure
+        (PreparedCheckedCalculation
+            operandType identities calculationGuard first links result)
+  where
+    prepareCalculationLinks previous (destination :| rest) = do
+        (next, firstLink) <- prepareCalculationLink previous destination
+        later <- prepareRemainingCalculationLinks next rest
+        pure (firstLink :| later)
+
+    prepareRemainingCalculationLinks _previous [] =
+        pure []
+    prepareRemainingCalculationLinks previous (destination : rest) = do
+        (next, link) <- prepareCalculationLink previous destination
+        (link :) <$> prepareRemainingCalculationLinks next rest
+
+    prepareCalculationLink previous
+            (destinationLocation, destination, justification) = do
+            linkOpen <- calculationEquality previous destination
+            link <- closeCalculationProposition
+                identities calculationGuard linkOpen
+            discharge <-
+                prepareDischarge
+                    (if destinationLocation == Nowhere
+                        then fallback
+                        else destinationLocation)
+                    context
+                    locals
+                    link
+                    justification
+            pure
+                ( destination
+                , PreparedCalculationLink destination discharge
+                )
+
+    calculationEquality left right =
+        maybe
+            (impossible
+                "checked calculation endpoints changed type or context")
+            pure
+            (equalScopedCore left right)
+
+closeCalculationProposition
+    :: [Exact.ExactLocalId]
+    -> Maybe (ScopedCheckedCore ObjectId)
+    -> ScopedCheckedCore ObjectId
+    -> Prepare (ScopedCheckedCore ObjectId)
+closeCalculationProposition identities calculationGuard proposition = do
+    guarded <-
+        case calculationGuard of
+            Nothing -> pure proposition
+            Just constraint ->
+                maybe
+                    (impossible
+                        "a checked calculation guard changed context")
+                    pure
+                    (implyScopedCore constraint proposition)
+    pure (closeBinders (length identities) guarded)
+  where
+    closeBinders 0 closed = closed
+    closeBinders remaining open =
+        closeBinders (remaining - 1)
+            (fromMaybe
+                (impossible
+                    "a checked calculation lost a quantified binder")
+                (closeScopedForall open))
+
+preparedCalculationResult
+    :: PreparedCalculation
+    -> ScopedCheckedCore ObjectId
+preparedCalculationResult
+        (PreparedCheckedCalculation
+            _operandType _identities _guard _first _links result) =
+    result
+
+preparedCalculationLinkDestination
+    :: PreparedCalculationLink
+    -> ScopedCheckedCore ObjectId
+preparedCalculationLinkDestination
+        (PreparedCalculationLink destination _discharge) =
+    destination
+
+preparedCalculationLinkDischarge
+    :: PreparedCalculationLink
+    -> PreparedDischarge
+preparedCalculationLinkDischarge
+        (PreparedCalculationLink _destination discharge) =
+    discharge
+
+preparedDischargeGoal
+    :: PreparedDischarge
+    -> ScopedCheckedCore ObjectId
+preparedDischargeGoal = \case
+    PreparedVampireDischarge _location _justification goal _obligation ->
+        goal
+    PreparedSetExtensionality _location goal ->
+        goal
+
+prepareSymbolicBoundConstraints
+    :: Exact.ExactBinderContext
+    -> NonEmpty Raw.VarSymbol
+    -> Raw.Bound
+    -> Prepare (ScopedCheckedCore ObjectId)
+prepareSymbolicBoundConstraints context variables bound =
+    Exact.preparedExactPropositionCore
+        <$> ( liftDriver
+                (Exact.prepareExactSymbolicBoundConstraints
+                    context variables bound)
+                >>= either
+                    (throwProof . ExactProofElaborationFailed)
+                    pure
+            )
+
+prepareSymbolicTake
+    :: Location
+    -> Location
+    -> Exact.ExactBinderContext
+    -> [PreparedLocal]
+    -> ScopedCheckedCore ObjectId
+    -> NonEmpty Raw.VarSymbol
+    -> Raw.Bound
+    -> Raw.Stmt
+    -> Raw.Justification
+    -> Raw.Proof
+    -> Prepare PreparedProof
+prepareSymbolicTake
+        fallback location context locals goal variables bound statement
+        justification continuation = do
+    identities <- traverse (const allocateLocalIdentity) variables
+    context' <-
+        either
+            (throwProof . ExactProofElaborationFailed)
+            pure
+            (Exact.extendExactBinderContext
+                (NonEmpty.zip identities variables)
+                context)
+    witness <-
+        Exact.preparedExactPropositionCore
+            <$> ( liftDriver
+                    (Exact.prepareExactSymbolicWitnessConstraints
+                        context' variables bound statement)
+                    >>= either
+                        (throwProof . ExactProofElaborationFailed)
+                        pure
+                )
+    prepareTake
+        fallback location context locals goal context'
+        (toList identities) witness justification continuation
+
+prepareNounTake
+    :: Location
+    -> Location
+    -> Exact.ExactBinderContext
+    -> [PreparedLocal]
+    -> ScopedCheckedCore ObjectId
+    -> Raw.NounPhrase []
+    -> Raw.Justification
+    -> Raw.Proof
+    -> Prepare PreparedProof
+prepareNounTake
+        fallback location context locals goal nounPhrase
+        justification continuation = do
+    (identities, context') <-
+        case nounPhrase of
+            Raw.NounPhrase _left _noun variables _right _suchThat ->
+                case NonEmpty.nonEmpty variables of
+                    Just binders -> do
+                        identities <-
+                            traverse (const allocateLocalIdentity) binders
+                        context' <-
+                            either
+                                (throwProof . ExactProofElaborationFailed)
+                                pure
+                                (Exact.extendExactBinderContext
+                                    (NonEmpty.zip identities binders)
+                                    context)
+                        pure (toList identities, context')
+                    Nothing -> do
+                        identity <- allocateLocalIdentity
+                        context' <-
+                            either
+                                (throwProof . ExactProofElaborationFailed)
+                                pure
+                                (Exact.extendExactAnonymousBinderContext
+                                    identity context)
+                        pure ([identity], context')
+    witness <-
+        Exact.preparedExactPropositionCore
+            <$> ( liftDriver
+                    (Exact.prepareExactNounWitnessConstraints
+                        context' nounPhrase)
+                    >>= either
+                        (throwProof . ExactProofElaborationFailed)
+                        pure
+                )
+    prepareTake
+        fallback location context locals goal context'
+        identities witness justification continuation
+
+prepareTake
+    :: Location
+    -> Location
+    -> Exact.ExactBinderContext
+    -> [PreparedLocal]
+    -> ScopedCheckedCore ObjectId
+    -> Exact.ExactBinderContext
+    -> [Exact.ExactLocalId]
+    -> ScopedCheckedCore ObjectId
+    -> Raw.Justification
+    -> Raw.Proof
+    -> Prepare PreparedProof
+prepareTake
+        fallback location context locals goal witnessContext
+        identities witness justification continuation = do
+    let witnessCount = length identities
+        existence = closeTakenWitnesses witnessCount witness
+        goal' = weakenForTakenWitnesses witnessCount goal
+    discharge <-
+        prepareDischarge
+            location context locals existence justification
+    local <- allocateLocal ExactAssumption witnessContext witness
+    PreparedTake identities witness discharge
+        <$> prepareProof
+            fallback
+            witnessContext
+            (locals <> [local])
+            RecursiveProofInduction
+            goal'
+            continuation
+
+-- The discharged existential and the opened witness premise are the same
+-- checked proposition viewed on opposite sides of existential elimination.
+closeTakenWitnesses
+    :: Int
+    -> ScopedCheckedCore ObjectId
+    -> ScopedCheckedCore ObjectId
+closeTakenWitnesses binderCount = go binderCount
+  where
+    go 0 proposition = proposition
+    go remaining proposition =
+        go (remaining - 1)
+            (fromMaybe
+                (impossible "a taken witness has no checked binder")
+                (closeScopedExists proposition))
+
+weakenForTakenWitnesses
+    :: Int
+    -> ScopedCheckedCore ObjectId
+    -> ScopedCheckedCore ObjectId
+weakenForTakenWitnesses binderCount = go binderCount
+  where
+    go 0 proposition = proposition
+    go remaining proposition =
+        go (remaining - 1)
+            (weakenCheckedScopedCore TySet proposition)
+
+openFixedVariables
+    :: Exact.ExactBinderContext
+    -> ScopedCheckedCore ObjectId
+    -> NonEmpty Raw.VarSymbol
+    -> Prepare
+        ( Exact.ExactBinderContext
+        , ScopedCheckedCore ObjectId
+        , [Exact.ExactLocalId]
+        )
+openFixedVariables initialContext initialGoal variables =
+    foldM openOne
+        (initialContext, initialGoal, [])
+        (toList variables)
+  where
+    openOne (context, goal, identities) variable = do
+        (binderType, body) <-
+            maybe
+                (throwProof
+                    (ExactProofExpectedUniversalGoal
+                        (locate variable)))
+                pure
+                (openScopedForall goal)
+        unless (binderType == TySet)
+            (throwProof
+                (ExactProofExpectedUniversalGoal
+                    (locate variable)))
+        identity <- allocateLocalIdentity
+        context' <-
+            either
+                (throwProof . ExactProofElaborationFailed)
+                pure
+                (Exact.extendExactBinderContext
+                    ((identity, variable) :| [])
+                    context)
+        pure (context', body, identities <> [identity])
+
+allocateLocalIdentity :: Prepare Exact.ExactLocalId
+allocateLocalIdentity = do
+    state <- State.get
+    State.put
+        state
+            { prepareNextLocal = prepareNextLocal state + 1
+            }
+    pure (Exact.exactLocalId (prepareNextLocal state))
+
+allocateLocal
+    :: ExactLocalOrigin
+    -> Exact.ExactBinderContext
+    -> ScopedCheckedCore ObjectId
+    -> Prepare PreparedLocal
+allocateLocal origin context proposition = do
+    state <- State.get
+    State.put
+        state
+            { prepareNextPremise = prepareNextPremise state + 1
+            }
+    pure
+        (PreparedLocal
+            (Backend.localPremiseOrdinal
+                (prepareNextPremise state))
+            origin
+            (Exact.exactBinderContextSupport context)
+            proposition)
+
+prepareConstructionFoundation
+    :: Prepare SetConstructionFoundation
+prepareConstructionFoundation = do
+    familyUnion <- foundation FamilyUnionCharacteristic
+    separation <- foundation SeparationCharacteristic
+    replacement <- foundation ReplacementCharacteristic
+    setChoose <- foundation SetChooseWitness
+    pure
+        (setConstructionFoundation
+            familyUnion separation replacement setChoose)
+  where
+    foundation tag =
+        liftDriver
+            (Declaration.currentFoundationAxiomLowering tag)
+
+prepareDischarge
+    :: Location
+    -> Exact.ExactBinderContext
+    -> [PreparedLocal]
+    -> ScopedCheckedCore ObjectId
+    -> Raw.Justification
+    -> Prepare PreparedDischarge
+prepareDischarge location context locals goal justification =
+    prepareDischargeWith
+        (dischargeModeFor goal)
+        [] Nothing location context locals goal justification
+
+-- A contradictory-axioms answer can establish falsum, but never an unrelated
+-- proposition directly. Derive that distinction from the checked target so
+-- every surface proof spelling reaches the same guarded request path.
+dischargeModeFor :: ScopedCheckedCore ObjectId -> DischargeMode
+dischargeModeFor goal
+    | scopedCoreType goal == TyProp
+    , scopedCoreTerm goal == CFalsum =
+        IndirectContradictionDischarge
+    | otherwise =
+        DirectDischarge
+
+data DischargeMode
+    = DirectDischarge
+    | IndirectContradictionDischarge
+
+prepareDischargeWith
+    :: DischargeMode
+    -> [FoundationAxiomTag]
+    -> Maybe Declaration.VampirePremiseSelection
+    -> Location
+    -> Exact.ExactBinderContext
+    -> [PreparedLocal]
+    -> ScopedCheckedCore ObjectId
+    -> Raw.Justification
+    -> Prepare PreparedDischarge
+prepareDischargeWith
+        dischargeMode auxiliaries selectionOverride
+        location context locals goal justification =
+    case justification of
+        Raw.JustificationSetExt -> do
+            (leftToRight, rightToLeft) <-
+                maybe
+                    (throwProof
+                        (ExactProofSetExtensionalityGoalMismatch location))
+                    pure
+                    (splitScopedSetEquality goal)
+            unless
+                ( hasDerivedLocal leftToRight
+                    && hasDerivedLocal rightToLeft
+                )
+                (throwProof
+                    (ExactProofSetExtensionalityDirectionsUnavailable
+                        location))
+            pure (PreparedSetExtensionality location goal)
+        _ -> do
+            preparedJustification <-
+                prepareJustification location justification
+            prepared <-
+                liftDriver
+                    (prepareObligation
+                        (Exact.exactBinderContextSupport context)
+                        goal
+                        (toScopedPremise <$> locals)
+                        auxiliaries
+                        (fromMaybe
+                            (vampirePremiseSelection preparedJustification)
+                            selectionOverride))
+                    >>= either
+                        (throwProof
+                            . ExactProofObligationPreparationFailed location)
+                        pure
+            pure
+                (PreparedVampireDischarge
+                    location
+                    preparedJustification
+                    goal
+                    prepared)
+  where
+    prepareObligation =
+        case dischargeMode of
+            DirectDischarge ->
+                Declaration.prepareScopedVampireObligationLowering
+            IndirectContradictionDischarge ->
+                Declaration.prepareScopedContradictionObligationLowering
+
+    hasDerivedLocal proposition =
+        any
+            (\case
+                PreparedLocal
+                        _ordinal ExactDerivedClaim _support local ->
+                    local == proposition
+                PreparedLocal{} ->
+                    False)
+            locals
+
+    toScopedPremise
+            (PreparedLocal ordinal origin support proposition) =
+        Declaration.scopedVampirePremise
+            ordinal origin support proposition
+
+prepareJustification
+    :: Location
+    -> Raw.Justification
+    -> Prepare PreparedJustification
+prepareJustification _location Raw.JustificationEmpty =
+    pure PreparedAuto
+prepareJustification location (Raw.JustificationRef markers) = do
+    resolved <- traverse (resolveReference location) (toList markers)
+    let unique = stableUnique resolved
+    case unique of
+        [] ->
+            impossible "a nonempty citation list resolved to no facts"
+        first : rest ->
+            pure (PreparedReferences (first :| rest))
+prepareJustification _location Raw.JustificationLocal =
+    pure PreparedLocalOnly
+prepareJustification location Raw.JustificationSetExt =
+    throwProof (ExactProofUnsupportedStep location)
+
+vampirePremiseSelection
+    :: PreparedJustification
+    -> Declaration.VampirePremiseSelection
+vampirePremiseSelection = \case
+    PreparedAuto ->
+        Declaration.VampireImplicitPremises
+    PreparedReferences fingerprints ->
+        Declaration.VampireExplicitPremises fingerprints
+    PreparedLocalOnly ->
+        Declaration.VampireLocalPremises
+
+resolveReference
+    :: Location
+    -> Raw.Marker
+    -> Prepare SemanticFactOccurrenceFingerprint
+resolveReference location marker@(Raw.Marker name) = do
+    resolved <-
+        liftDriver
+            (Declaration.resolveVisibleFactAliasLowering
+                (semanticName name))
+    maybe
+        (throwProof
+            (ExactProofUnknownReference location marker))
+        pure
+        resolved
+
+prepareStatement
+    :: Exact.ExactBinderContext
+    -> Raw.Stmt
+    -> Prepare Exact.PreparedExactProposition
+prepareStatement context statement =
+    liftDriver
+        (Exact.prepareExactProposition context statement)
+        >>= either
+            (throwProof . ExactProofElaborationFailed)
+            pure
+
+validateStructuralComposition
+    :: Location
+    -> [ScopedCheckedCore ObjectId]
+    -> ( CheckedFoundation
+         -> (ObjectId -> Maybe CoreType)
+         -> Either KernelProof.KernelProofBuildError ()
+       )
+    -> Prepare ()
+validateStructuralComposition location propositions validate = do
+    foundation <-
+        liftDriver Declaration.currentFoundationLowering
+    let identities =
+            Set.toAscList
+                (Set.unions
+                    ( canonicalTermGlobals . scopedCoreTerm
+                        <$> propositions
+                    ))
+    types <-
+        traverse
+            (\identity -> do
+                coreType <-
+                    liftDriver
+                        (Declaration.objectTypeLowering identity)
+                maybe
+                    (impossible
+                        "a checked structural proof lost a global object")
+                    (\availableType -> pure (identity, availableType))
+                    coreType)
+            identities
+    either
+        (throwProof
+            . ExactProofStructuralCompositionFailed location)
+        pure
+        (validate foundation
+            (\identity -> Map.lookup identity (Map.fromList types)))
+
+structuralFailure :: Location -> Text -> Prepare value
+structuralFailure location message =
+    throwProof
+        (ExactProofStructuralCompositionFailed
+            location
+            (KernelProof.ProofStructuralCompositionMismatch message))
+
+data CheckedExactProofAuthorization = CheckedExactProofAuthorization
+    !PreparedProof
+    !Bool
+
+lowerPreparedExactProof
+    :: PreparedExactProof
+    -> Declaration.LoweringDriver
+        (Either
+            Declaration.DeclarationError
+            (Declaration.CheckedDeclaration CheckedExactProofAuthorization))
+lowerPreparedExactProof
+        (PreparedExactProof _location alias target proof syntax) =
+    fmap checked
+        <$> Declaration.prepareCandidateSpecLowering
+            [] target SearchEligible [alias]
+  where
+    checked spec =
+        Declaration.checkedProofDeclaration
+            syntax [] [] [] []
+            [Declaration.checkedCandidate spec planning :| []]
+            (CheckedExactProofAuthorization
+                proof
+                (isJust (preparedProofFirstOmission proof)))
+      where
+        requests = plannedProofRequests proof
+        planning
+            | isJust (preparedProofFirstOmission proof) =
+                Declaration.checkedOmittedPlanning requests []
+            | otherwise =
+                Declaration.checkedSourceProofPlanning requests []
+
+authorizeCheckedExactProof
+    :: CheckedExactProofAuthorization
+    -> [NonEmpty Declaration.ReservedCandidate]
+    -> Declaration.Declaration ()
+authorizeCheckedExactProof
+        (CheckedExactProofAuthorization proof hasOmission) = \case
+    [candidate :| []]
+        | hasOmission ->
+            Declaration.authorizeOmittedCandidate
+                candidate
+                (executePreparedProof proof)
+        | otherwise ->
+            Declaration.authorizeVampireCandidate
+                candidate
+                (executePreparedProof proof)
+    stages ->
+        Declaration.failDeclaration
+            (Declaration.CheckedAuthorizationCandidateShapeMismatch
+                1 (length stages))
+
+data CheckedFinalPreludeFoundationAuthorization =
+    CheckedFinalPreludeFoundationAuthorization !FoundationAxiomTag
+
+lowerPreparedFinalPreludeFoundationClaim
+    :: PreparedFinalPreludeFoundationClaim
+    -> Declaration.LoweringDriver
+        (Either
+            Declaration.DeclarationError
+            (Declaration.CheckedDeclaration
+                CheckedFinalPreludeFoundationAuthorization))
+lowerPreparedFinalPreludeFoundationClaim
+        (PreparedFinalPreludeFoundationClaim
+            _location alias target tag syntax) =
+    fmap checked
+        <$> Declaration.prepareCandidateSpecLowering
+            [] target SearchEligible [alias]
+  where
+    checked spec =
+        Declaration.checkedProofDeclaration
+            syntax [] [] [] []
+            [ Declaration.checkedCandidate spec
+                (Declaration.checkedKernelPlanning
+                    (Authority.FoundationLeaf tag) [])
+                :| []
+            ]
+            (CheckedFinalPreludeFoundationAuthorization tag)
+
+authorizeCheckedFinalPreludeFoundationClaim
+    :: CheckedFinalPreludeFoundationAuthorization
+    -> [NonEmpty Declaration.ReservedCandidate]
+    -> Declaration.Declaration ()
+authorizeCheckedFinalPreludeFoundationClaim
+        (CheckedFinalPreludeFoundationAuthorization tag) = \case
+    [candidate :| []] ->
+        Declaration.authorizeKernelConstructionCandidate
+            (Authority.FoundationLeaf tag)
+            candidate
+            (pure (foundationFactDerivation tag))
+    stages ->
+        Declaration.failDeclaration
+            (Declaration.CheckedAuthorizationCandidateShapeMismatch
+                1 (length stages))
+
+preparedProofFirstOmission :: PreparedProof -> Maybe Location
+preparedProofFirstOmission = \case
+    PreparedImplicitAuto{} -> Nothing
+    PreparedQed{} -> Nothing
+    PreparedOmitted location _goal -> Just location
+    PreparedFix _identities continuation ->
+        preparedProofFirstOmission continuation
+    PreparedAssume _antecedent continuation ->
+        preparedProofFirstOmission continuation
+    PreparedTake _identities _witness _discharge continuation ->
+        preparedProofFirstOmission continuation
+    PreparedSetInduction
+            (PreparedCheckedSetInduction
+                _focus _property _antecedents _target
+                _hypothesis _result child) ->
+        preparedProofFirstOmission child
+    PreparedHave _claim _discharge continuation ->
+        preparedProofFirstOmission continuation
+    PreparedSuffices _goal _reduction _implication _discharge continuation ->
+        preparedProofFirstOmission continuation
+    PreparedCalculate _calculation continuation ->
+        preparedProofFirstOmission continuation
+    PreparedSince _since _evidence _claim _discharge continuation ->
+        preparedProofFirstOmission continuation
+    PreparedSubclaim _claim subproof continuation ->
+        preparedProofFirstOmission subproof
+            <|> preparedProofFirstOmission continuation
+    PreparedDefine _identity _body _definition continuation ->
+        preparedProofFirstOmission continuation
+    PreparedDefineRelational
+            _identity _body _functionality _definitions continuation ->
+        preparedProofFirstOmission continuation
+    PreparedDefineFunction _identity _graph _definition continuation ->
+        preparedProofFirstOmission continuation
+    PreparedByCase (PreparedCaseAnalysis _goal cases _exhaustive _discharge) ->
+        foldr
+            ((<|>) . preparedProofFirstOmission . preparedCaseProof)
+            Nothing
+            cases
+    PreparedByContradiction _goal _negation _falsum child ->
+        preparedProofFirstOmission child
+    PreparedContradiction{} -> Nothing
+
+plannedProofRequests
+    :: PreparedProof
+    -> [Declaration.CheckedPlannedVampireRequest]
+plannedProofRequests = \case
+    PreparedImplicitAuto discharge -> plannedDischargeRequests discharge
+    PreparedQed discharge -> plannedDischargeRequests discharge
+    PreparedOmitted{} -> []
+    PreparedFix _identities continuation ->
+        plannedProofRequests continuation
+    PreparedAssume _antecedent continuation ->
+        plannedProofRequests continuation
+    PreparedTake _identities _witness discharge continuation ->
+        plannedDischargeRequests discharge <> plannedProofRequests continuation
+    PreparedSetInduction
+            (PreparedCheckedSetInduction
+                _focus _property _antecedents _target
+                _hypothesis _result child) ->
+        plannedProofRequests child
+    PreparedHave _claim discharge continuation ->
+        plannedDischargeRequests discharge <> plannedProofRequests continuation
+    PreparedSuffices _goal _reduction _implication discharge continuation ->
+        plannedDischargeRequests discharge <> plannedProofRequests continuation
+    PreparedCalculate calculation continuation ->
+        plannedCalculationRequests calculation
+            <> plannedProofRequests continuation
+    PreparedSince _since evidence _claim discharge continuation ->
+        plannedSinceEvidenceRequests evidence
+            <> plannedDischargeRequests discharge
+            <> plannedProofRequests continuation
+    PreparedSubclaim _claim subproof continuation ->
+        plannedProofRequests subproof <> plannedProofRequests continuation
+    PreparedDefine _identity _body _definition continuation ->
+        plannedProofRequests continuation
+    PreparedDefineRelational
+            _identity _body functionality _definitions continuation ->
+        plannedDischargeRequests functionality
+            <> plannedProofRequests continuation
+    PreparedDefineFunction _identity _graph _definition continuation ->
+        plannedProofRequests continuation
+    PreparedByCase
+            (PreparedCaseAnalysis _goal cases _exhaustive discharge) ->
+        concatMap
+            (plannedProofRequests . preparedCaseProof)
+            (toList cases)
+            <> plannedDischargeRequests discharge
+    PreparedByContradiction _goal _negation _falsum child ->
+        plannedProofRequests child
+    PreparedContradiction _goal _falsum discharge ->
+        plannedDischargeRequests discharge
+
+plannedDischargeRequests
+    :: PreparedDischarge
+    -> [Declaration.CheckedPlannedVampireRequest]
+plannedDischargeRequests = \case
+    PreparedVampireDischarge location _justification _goal obligation ->
+        [Declaration.checkedPlannedVampireRequest location obligation]
+    PreparedSetExtensionality{} -> []
+
+plannedCalculationRequests
+    :: PreparedCalculation
+    -> [Declaration.CheckedPlannedVampireRequest]
+plannedCalculationRequests
+        (PreparedCheckedCalculation
+            _operandType _identities _guard _first links _result) =
+    concatMap
+        (plannedDischargeRequests . preparedCalculationLinkDischarge)
+        (toList links)
+
+plannedSinceEvidenceRequests
+    :: PreparedSinceEvidence
+    -> [Declaration.CheckedPlannedVampireRequest]
+plannedSinceEvidenceRequests = \case
+    PreparedSinceExisting{} -> []
+    PreparedSinceDischarged discharge _local ->
+        plannedDischargeRequests discharge
+
+executePreparedProof
+    :: PreparedProof
+    -> Declaration.CandidateProof ()
+executePreparedProof = \case
+    PreparedImplicitAuto discharge ->
+        executeDischarge discharge
+    PreparedQed discharge ->
+        executeDischarge discharge
+    PreparedOmitted _location _goal ->
+        Declaration.recordOmittedUse
+    PreparedFix _identities continuation ->
+        executePreparedProof continuation
+    PreparedAssume _antecedent continuation ->
+        executePreparedProof continuation
+    PreparedTake _identities _witness discharge continuation -> do
+        executeDischarge discharge
+        executePreparedProof continuation
+    PreparedSetInduction
+            (PreparedCheckedSetInduction
+                _focus _property _antecedents _target
+                _hypothesis _result child) ->
+        executePreparedProof child
+    PreparedHave _claim discharge continuation -> do
+        executeDischarge discharge
+        executePreparedProof continuation
+    PreparedSuffices goal reduction implication discharge continuation -> do
+        executeDischarge discharge
+        executePreparedProof continuation
+        unless
+            (implyScopedCore reduction goal == Just implication)
+            (impossible "a prepared suffices implication diverged")
+    PreparedCalculate calculation continuation -> do
+        executePreparedCalculation calculation
+        executePreparedProof continuation
+    PreparedSince sinceProposition evidence _claim discharge continuation -> do
+        executeSinceEvidence sinceProposition evidence
+        executeDischarge discharge
+        executePreparedProof continuation
+    PreparedSubclaim _claim subproof continuation -> do
+        executePreparedProof subproof
+        executePreparedProof continuation
+    PreparedDefine _identity _body _definition continuation ->
+        executePreparedProof continuation
+    PreparedDefineRelational
+            _identity _body functionality _definitions continuation -> do
+        executeDischarge functionality
+        executePreparedProof continuation
+    PreparedDefineFunction _identity _graph _definition continuation ->
+        executePreparedProof continuation
+    PreparedByCase
+            (PreparedCaseAnalysis _goal cases _exhaustive discharge) -> do
+        traverse_ (executePreparedProof . preparedCaseProof) cases
+        executeDischarge discharge
+    PreparedByContradiction _goal _negation _falsum child ->
+        executePreparedProof child
+    PreparedContradiction _goal _falsum discharge ->
+        executeDischarge discharge
+
+executeDischarge
+    :: PreparedDischarge
+    -> Declaration.CandidateProof ()
+executeDischarge
+        (PreparedVampireDischarge
+            location _justification _goal obligation) =
+    Declaration.locateProofObligation location
+        (Declaration.acceptPreparedVampireObligation obligation)
+executeDischarge PreparedSetExtensionality{} =
+    pure ()
+
+executePreparedCalculation
+    :: PreparedCalculation
+    -> Declaration.CandidateProof ()
+executePreparedCalculation
+        (PreparedCheckedCalculation
+            _operandType _identities _guard _first links _result) =
+    traverse_
+        (executeDischarge . preparedCalculationLinkDischarge)
+        links
+
+executeSinceEvidence
+    :: ScopedCheckedCore ObjectId
+    -> PreparedSinceEvidence
+    -> Declaration.CandidateProof ()
+executeSinceEvidence proposition = \case
+    PreparedSinceExisting local ->
+        unless (preparedLocalProposition local == proposition)
+            (impossible "a structural since premise diverged")
+    PreparedSinceDischarged discharge local -> do
+        executeDischarge discharge
+        unless
+            ( preparedDischargeGoal discharge == proposition
+                && preparedLocalProposition local == proposition
+            )
+            (impossible "a discharged since premise diverged")
+
+preparedLocalProposition
+    :: PreparedLocal
+    -> ScopedCheckedCore ObjectId
+preparedLocalProposition
+        (PreparedLocal _ordinal _origin _support proposition) =
+    proposition
+
+encodePreparedProof :: PreparedProof -> ByteString
+encodePreparedProof =
+    encodeCache . putPreparedProof
+
+putPreparedProof :: PreparedProof -> CachePut
+putPreparedProof = \case
+    PreparedImplicitAuto discharge -> do
+        putCacheTag 0x00
+        putPreparedDischarge discharge
+    PreparedQed discharge -> do
+        putCacheTag 0x01
+        putPreparedDischarge discharge
+    PreparedOmitted _location goal -> do
+        putCacheTag 0x06
+        putScopedProposition goal
+    PreparedFix identities continuation -> do
+        putCacheTag 0x02
+        putCacheList
+            (putCacheNatural . Exact.exactLocalIdValue)
+            identities
+        putPreparedProof continuation
+    PreparedAssume antecedent continuation -> do
+        putCacheTag 0x03
+        putScopedProposition antecedent
+        putPreparedProof continuation
+    PreparedTake identities witness discharge continuation -> do
+        putCacheTag 0x08
+        putCacheList
+            (putCacheNatural . Exact.exactLocalIdValue)
+            identities
+        putScopedProposition witness
+        putPreparedDischarge discharge
+        putPreparedProof continuation
+    PreparedSetInduction
+            (PreparedCheckedSetInduction
+                focus property antecedents target hypothesis result child) -> do
+        putCacheTag 0x07
+        putPreparedSetInductionFocus focus
+        putScopedProposition property
+        putCacheList putScopedProposition antecedents
+        putScopedProposition target
+        putScopedProposition hypothesis
+        putScopedProposition result
+        putPreparedProof child
+    PreparedHave claim discharge continuation -> do
+        putCacheTag 0x04
+        putScopedProposition claim
+        putPreparedDischarge discharge
+        putPreparedProof continuation
+    PreparedSuffices goal reduction implication discharge continuation -> do
+        putCacheTag 0x0c
+        putScopedProposition goal
+        putScopedProposition reduction
+        putScopedProposition implication
+        putPreparedDischarge discharge
+        putPreparedProof continuation
+    PreparedCalculate calculation continuation -> do
+        putCacheTag 0x0d
+        putPreparedCalculation calculation
+        putPreparedProof continuation
+    PreparedSince sinceProposition evidence claim discharge continuation -> do
+        putCacheTag 0x0e
+        putScopedProposition sinceProposition
+        putPreparedSinceEvidence evidence
+        putScopedProposition claim
+        putPreparedDischarge discharge
+        putPreparedProof continuation
+    PreparedSubclaim claim subproof continuation -> do
+        putCacheTag 0x05
+        putScopedProposition claim
+        putPreparedProof subproof
+        putPreparedProof continuation
+    PreparedDefine identity body definitions continuation -> do
+        putCacheTag 0x09
+        putCacheNatural (Exact.exactLocalIdValue identity)
+        putScopedTerm body
+        putCacheList putScopedProposition (toList definitions)
+        putPreparedProof continuation
+    PreparedDefineRelational
+            identity body functionality definitions continuation -> do
+        putCacheTag 0x11
+        putCacheNatural (Exact.exactLocalIdValue identity)
+        putScopedTerm body
+        putPreparedDischarge functionality
+        putCacheList putScopedProposition (toList definitions)
+        putPreparedProof continuation
+    PreparedByCase caseAnalysis -> do
+        putCacheTag 0x0f
+        putPreparedCaseAnalysis caseAnalysis
+    PreparedByContradiction goal negation falsum child -> do
+        putCacheTag 0x10
+        putScopedProposition goal
+        putScopedProposition negation
+        putScopedProposition falsum
+        putPreparedProof child
+    PreparedContradiction goal falsum discharge -> do
+        putCacheTag 0x0a
+        putScopedProposition goal
+        putScopedProposition falsum
+        putPreparedDischarge discharge
+    PreparedDefineFunction identity graph definition continuation -> do
+        putCacheTag 0x0b
+        putCacheNatural (Exact.exactLocalIdValue identity)
+        putScopedTerm graph
+        putScopedProposition definition
+        putPreparedProof continuation
+
+putPreparedSetInductionFocus
+    :: PreparedSetInductionFocus
+    -> CachePut
+putPreparedSetInductionFocus = \case
+    PreparedInitialSetInductionFocus identity index -> do
+        putCacheTag 0x00
+        putCacheNatural (Exact.exactLocalIdValue identity)
+        putCacheNatural index
+    PreparedLeadingSetInductionFocus identity -> do
+        putCacheTag 0x01
+        putCacheNatural (Exact.exactLocalIdValue identity)
+
+putPreparedDischarge :: PreparedDischarge -> CachePut
+putPreparedDischarge
+        (PreparedVampireDischarge
+            _location justification goal _obligation) = do
+    putPreparedDischargeSyntax justification goal
+putPreparedDischarge
+        (PreparedSetExtensionality _location goal) = do
+    putCacheTag 0x03
+    putScopedProposition goal
+
+putPreparedDischargeSyntax
+    :: PreparedJustification
+    -> ScopedCheckedCore ObjectId
+    -> CachePut
+putPreparedDischargeSyntax justification goal = do
+    putPreparedJustification justification
+    putScopedProposition goal
+
+putPreparedCalculation :: PreparedCalculation -> CachePut
+putPreparedCalculation
+        (PreparedCheckedCalculation
+            operandType identities calculationGuard first links result) = do
+    putCoreTypeCache operandType
+    putCacheList
+        (putCacheNatural . Exact.exactLocalIdValue)
+        identities
+    putCacheMaybe putScopedProposition calculationGuard
+    putCacheList putScopedTerm
+        (first : (preparedCalculationLinkDestination <$> toList links))
+    putCacheList putPreparedDischarge
+        (preparedCalculationLinkDischarge <$> toList links)
+    putScopedProposition result
+
+putPreparedSinceEvidence :: PreparedSinceEvidence -> CachePut
+putPreparedSinceEvidence = \case
+    PreparedSinceExisting local -> do
+        putCacheTag 0x00
+        putPreparedLocalEvidence local
+    PreparedSinceDischarged discharge local -> do
+        putCacheTag 0x01
+        putPreparedDischarge discharge
+        putPreparedLocalEvidence local
+
+putPreparedCaseAnalysis :: PreparedCaseAnalysis -> CachePut
+putPreparedCaseAnalysis
+        (PreparedCaseAnalysis goal cases exhaustive discharge) = do
+    putScopedProposition goal
+    putCacheList putPreparedCase (toList cases)
+    putScopedProposition exhaustive
+    putPreparedDischarge discharge
+
+putPreparedCase :: PreparedCase -> CachePut
+putPreparedCase (PreparedCase assumption proof) = do
+    putScopedProposition assumption
+    putPreparedProof proof
+
+putPreparedLocalEvidence :: PreparedLocal -> CachePut
+putPreparedLocalEvidence
+        (PreparedLocal ordinal _origin support proposition) = do
+    putCacheNatural (Backend.localPremiseOrdinalValue ordinal)
+    putCacheList
+        (\(identity, coreType) -> do
+            putCacheNatural (Exact.exactLocalIdValue identity)
+            putCoreTypeCache coreType)
+        (Vector.toList support)
+    putScopedProposition proposition
+
+implicitAutoProofSyntaxId
+    :: ScopedCheckedCore ObjectId
+    -> ProofSyntaxId
+implicitAutoProofSyntaxId goal =
+    proofSyntaxId
+        (encodeCache do
+            putCacheTag 0x00
+            putPreparedDischargeSyntax PreparedAuto goal)
+
+putPreparedJustification :: PreparedJustification -> CachePut
+putPreparedJustification = \case
+    PreparedAuto ->
+        putCacheTag 0x00
+    PreparedReferences fingerprints -> do
+        putCacheTag 0x01
+        putCacheList
+            putSemanticFactOccurrenceFingerprintCache
+            (toList fingerprints)
+    PreparedLocalOnly ->
+        putCacheTag 0x02
+
+putScopedProposition
+    :: ScopedCheckedCore ObjectId
+    -> CachePut
+putScopedProposition proposition = do
+    putCacheList putCoreTypeCache
+        (scopedCoreContext proposition)
+    putCanonicalTermCache putObjectIdCache
+        (scopedCoreTerm proposition)
+
+putScopedTerm
+    :: ScopedCheckedCore ObjectId
+    -> CachePut
+putScopedTerm term = do
+    putCacheList putCoreTypeCache
+        (scopedCoreContext term)
+    putCoreTypeCache (scopedCoreType term)
+    putCanonicalTermCache putObjectIdCache
+        (scopedCoreTerm term)
+
+proofLocation :: Location -> Raw.Proof -> Location
+proofLocation fallback = \case
+    Raw.Omitted location -> location
+    Raw.Qed maybeLocation _justification ->
+        fromMaybe fallback maybeLocation
+    Raw.Contradiction location _justification -> location
+    Raw.ByCase location _cases -> location
+    Raw.ByContradiction location _proof -> location
+    Raw.BySetInduction location _term _proof -> location
+    Raw.ByOrdInduction location _proof -> location
+    Raw.Assume location _statement _proof -> location
+    Raw.FixSymbolic location _variables _bound _proof -> location
+    Raw.FixSuchThat location _variables _statement _proof -> location
+    Raw.Calc location _quantifier _calculation _proof -> location
+    Raw.TakeVar location _variables _bound _statement _justification _proof ->
+        location
+    Raw.TakeNoun location _noun _justification _proof -> location
+    Raw.Have location _since _statement _justification _proof -> location
+    Raw.Suffices location _statement _justification _proof -> location
+    Raw.Subclaim location _statement _subproof _proof -> location
+    Raw.Define location _variable _expression _proof -> location
+    Raw.DefineFunction location _function _argument _value _bound _domain _proof ->
+        location
+    Raw.DefineFunctionLocal
+            location _function _argument _value _bound _target _rules _proof ->
+        location
+
+throwProof :: ExactProofError -> Prepare value
+throwProof =
+    State.lift . Except.throwError
+
+liftDriver
+    :: Declaration.LoweringDriver value
+    -> Prepare value
+liftDriver =
+    State.lift . Except.lift
+
+stableUnique :: Ord value => [value] -> [value]
+stableUnique =
+    reverse . snd
+        . foldl'
+            (\(seen, reversed) value ->
+                if value `Set.member` seen
+                    then (seen, reversed)
+                    else
+                        ( Set.insert value seen
+                        , value : reversed
+                        ))
+            (Set.empty, [])
diff --git a/source/Felix/Checking/Exact/Vocabulary.hs b/source/Felix/Checking/Exact/Vocabulary.hs
new file mode 100644
index 0000000..a712bf1
--- /dev/null
+++ b/source/Felix/Checking/Exact/Vocabulary.hs
@@ -0,0 +1,218 @@
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | Semantic classification shared by the exact source compilers.
+module Felix.Checking.Exact.Vocabulary
+    ( FixedSemanticMeaning(..)
+    , fixedSemanticMeaning
+    , lowerFixedEqualityPredicate
+    , ExactSymbolClass(..)
+    , classifyExactSymbol
+    , FixedSetTermDispatch(..)
+    , dispatchFixedSetTerm
+    ) where
+
+import Base hiding (Empty)
+import Felix.Checking.Core
+import Felix.Checking.Semantic
+import Felix.Syntax.Abstract qualified as Raw
+import Felix.Syntax.Internal qualified as Internal
+import Felix.Syntax.Lexicon qualified as Lexicon
+
+import Data.List.NonEmpty qualified as NonEmpty
+import Data.Map.Strict qualified as Map
+
+
+data FixedSemanticMeaning
+    = FixedEquality
+    | FixedDisequality
+    | FixedIntrinsic !CoreIntrinsicTag
+    | FixedNegatedIntrinsic !CoreIntrinsicTag
+    deriving stock (Show, Eq)
+
+fixedSemanticMeaning
+    :: SemanticGlobalKey
+    -> Maybe FixedSemanticMeaning
+fixedSemanticMeaning key =
+    Map.lookup key fixedSemanticVocabulary
+
+-- This inventory owns every exact source form that bypasses global lookup.
+fixedSemanticVocabulary
+    :: Map.Map SemanticGlobalKey FixedSemanticMeaning
+fixedSemanticVocabulary =
+    Map.fromList
+    [ ( relationKey Raw.EqSymbol
+      , FixedEquality
+      )
+    , ( SemanticRightAdjective
+            (Raw.lexicalItemPattern
+                Lexicon.builtinEqualityRightAdjective)
+      , FixedEquality
+      )
+    , ( verbKey Lexicon.builtinEqualityVerb
+      , FixedEquality
+      )
+    , ( relationKey Raw.ElementSymbol
+      , FixedIntrinsic Member
+      )
+    , ( relationKey Raw.NotElementSymbol
+      , FixedNegatedIntrinsic Member
+      )
+    , ( relationKey Raw.NeqSymbol
+      , FixedDisequality
+      )
+    , ( nounKey Lexicon.builtinElementNoun
+      , FixedIntrinsic Member
+      )
+    , ( expressionKey
+            (Raw.TokenCons (Raw.Command "emptyset") Raw.End)
+      , FixedIntrinsic Empty
+      )
+    , ( expressionKey (Raw.mixfixPattern Raw.UnionsSymbol)
+      , FixedIntrinsic FamilyUnion
+      )
+    , ( expressionKey (unaryCommandPattern "pow")
+      , FixedIntrinsic PowerSet
+      )
+    , ( expressionKey (unaryCommandPattern "cumul")
+      , FixedIntrinsic UnivOf
+      )
+    , ( expressionKey (Raw.mixfixPattern Raw.UpairSymbol)
+      , FixedIntrinsic PairSet
+      )
+    ]
+  where
+    relationKey relation =
+        SemanticRelation
+            (Raw.relationSymbolToken relation)
+            (Raw.relationSymbolParameterArity relation)
+    nounKey item =
+        let patterns = Raw.lexicalItemSgPlPattern item
+        in SemanticNoun (Raw.sg patterns) (Raw.pl patterns)
+    verbKey item =
+        let patterns = Raw.lexicalItemSgPlPattern item
+        in SemanticVerb (Raw.sg patterns) (Raw.pl patterns)
+    expressionKey = SemanticExpressionFunction
+
+-- | Lower the fixed proposition meanings shared by raw exact elaboration and
+-- the reusable internal-formula path. Membership deliberately retains its
+-- carrier-aware source lowering and is not handled here.
+lowerFixedEqualityPredicate
+    :: FixedSemanticMeaning
+    -> [CanonicalTerm global]
+    -> Maybe (CanonicalTerm global)
+lowerFixedEqualityPredicate meaning arguments =
+    case (meaning, arguments) of
+        (FixedEquality, [left, right]) ->
+            Just (CEq TySet left right)
+        (FixedDisequality, [left, right]) ->
+            Just (CImp (CEq TySet left right) CFalsum)
+        _ ->
+            Nothing
+
+unaryCommandPattern :: Text -> Raw.Pattern
+unaryCommandPattern command =
+    Raw.TokenCons (Raw.Command command)
+        (Raw.TokenCons Raw.InvisibleBraceL
+            (Raw.HoleCons
+                (Raw.TokenCons Raw.InvisibleBraceR Raw.End)))
+
+data ExactSymbolClass
+    = ExactClosedLiteral
+    | ExactFixedPrimitive !FixedSemanticMeaning
+    | ExactSourceGlobal !(NonEmpty SemanticGlobalKey)
+    | ExactUnsupportedSymbol
+    deriving stock (Show, Eq)
+
+classifyExactSymbol :: Internal.Symbol -> ExactSymbolClass
+classifyExactSymbol symbol =
+    case symbol of
+        Internal.SymbolInteger{} ->
+            ExactClosedLiteral
+        _ ->
+            case NonEmpty.nonEmpty (semanticKeys symbol) of
+                Nothing ->
+                    ExactUnsupportedSymbol
+                Just keys ->
+                    case firstFixed keys of
+                        Just meaning ->
+                            ExactFixedPrimitive meaning
+                        Nothing ->
+                            ExactSourceGlobal keys
+  where
+    firstFixed =
+        foldr
+            (\key found -> fixedSemanticMeaning key <|> found)
+            Nothing
+
+semanticKeys :: Internal.Symbol -> [SemanticGlobalKey]
+semanticKeys = \case
+    Internal.SymbolMixfix symbol ->
+        [SemanticExpressionFunction (Raw.mixfixPattern symbol)]
+    Internal.SymbolFun item ->
+        let patterns = Raw.lexicalItemSgPlPattern item
+        in [SemanticFunctionPhrase (Raw.sg patterns) (Raw.pl patterns)]
+    Internal.SymbolPredicate predicate ->
+        case predicate of
+            Internal.PredicateAdj item ->
+                [ SemanticLeftAdjective (Raw.lexicalItemPattern item)
+                , SemanticRightAdjective (Raw.lexicalItemPattern item)
+                ]
+            Internal.PredicateVerb item ->
+                let patterns = Raw.lexicalItemSgPlPattern item
+                in [SemanticVerb (Raw.sg patterns) (Raw.pl patterns)]
+            Internal.PredicateNoun item ->
+                let patterns = Raw.lexicalItemSgPlPattern item
+                in [SemanticNoun (Raw.sg patterns) (Raw.pl patterns)]
+            Internal.PredicateRelation relation ->
+                [ SemanticRelation
+                    (Raw.relationSymbolToken relation)
+                    (Raw.relationSymbolParameterArity relation)
+                ]
+            Internal.PredicateSymbol{} -> []
+            Internal.PredicateNounStruct{} -> []
+    Internal.SymbolInteger{} -> []
+
+-- | Result of interpreting a symbol already classified by the fixed exact
+-- vocabulary as a set-valued term.
+data FixedSetTermDispatch global
+    = NotFixedSetTerm
+    | LoweredFixedSetTerm !(CanonicalTerm global)
+    | RejectedFixedSetTerm
+    deriving stock (Show, Eq)
+
+-- | Interpret every fixed symbol that can occur in the reusable internal-term
+-- lowering. Fixed relations are handled by formula lowering.
+dispatchFixedSetTerm
+    :: Internal.Symbol
+    -> [CanonicalTerm global]
+    -> FixedSetTermDispatch global
+dispatchFixedSetTerm symbol arguments =
+    case classifyExactSymbol symbol of
+        ExactFixedPrimitive meaning ->
+            case meaning of
+                FixedIntrinsic intrinsic ->
+                    applyIntrinsic
+                        (CIntrinsic intrinsic)
+                        (coreIntrinsicType intrinsic)
+                        arguments
+                FixedNegatedIntrinsic _intrinsic ->
+                    RejectedFixedSetTerm
+                FixedEquality ->
+                    RejectedFixedSetTerm
+                FixedDisequality ->
+                    RejectedFixedSetTerm
+        _ ->
+            NotFixedSetTerm
+  where
+    applyIntrinsic term coreType remaining =
+        case (coreType, remaining) of
+            (TySet, []) ->
+                LoweredFixedSetTerm term
+            (TyArrow TySet resultType, argument : rest) ->
+                applyIntrinsic
+                    (CApp term argument)
+                    resultType
+                    rest
+            _ ->
+                RejectedFixedSetTerm