Computational Extraction

C3-EXTRACT-001 — Judgment and eligible constructions

Extraction is the judgment E |- f : T ~~> A under X, where f is an accepted computational term, T is a data/function type in Type, A is a checked Algorithm artifact, and X identifies the extraction profile, representation mapping, formal contract, and preservation evidence. It is not a conversion from arbitrary propositions to programs. A request names both the construction and its associated contract theorem; both are checked in the exact environment.

The initial algorithm-structural/1 profile admits closed specializations of first-order inductive data, finite products, Nat, and first-order functions whose recursion has already elaborated to checked recursors. Functions may take erased proof parameters but not retained higher-order function arguments. Universe parameters and type arguments must be fixed before extraction. Dependent data is admitted only when proof/type erasure leaves a fixed checked layout; value-indexed layouts require an explicit checked representation mapping and are unsupported in this initial profile.

Nat uses arbitrary-precision nonnegative representation, not silent fixed-width arithmetic. Target allocation failure is an explicit runtime error outside the logical total-value theorem unless the contract includes a resource bound and its proof. A finite-width representation needs a separately checked range and operation-preservation proof. Unsupported mappings do not fall back to wrapping.

C3-EXTRACT-002 — Erasure and noncomputability

Erase propositions, proof arguments/fields, and type/universe arguments; retain computational values and their operational dependencies. The erased artifact must not inspect a proof or branch on its identity. Before erasure, the kernel must check the restricted Prop elimination rules; a serializer cannot mark a computational argument as a proof to remove it.

The retained computational closure must contain no axiom, uninterpreted constant, foreign evaluator, or opaque definition without an available checked computational body. Opaque computational definitions may be unfolded by the extractor from their checked bodies; this does not change kernel conversion. Noncomputable choice remains stuck and cannot be given arbitrary host behavior.

An existential proof in Prop, including one obtained classically, is not an executable witness. A Sigma value in Type can contain an executable witness and an erased proof. Classical assumptions occurring only in erased proofs may be retained in the contract footprint without preventing extraction, if policy admits them. They do not make retained classical choice computable.

C3-EXTRACT-003 — Preservation and execution tiers

The extraction record binds the source term, full environment, source contract, target signature/layout/ownership rules, Algorithm implementation, resource and error behavior, and a simulation/refinement obligation. Source and target observations must agree under the stated representation relation for the contract’s admitted inputs. Logical termination does not prove absence of finite-host resource exhaustion.

An extraction may be proposed without preservation evidence, but it cannot be admitted as proof-preserving until its certificate checks or a named extractor trust assumption is explicitly accepted. Such trust remains visible and is not called a checked preservation theorem. Interpreter/native/JIT/AOT lowering must likewise preserve the contract through certificates or named backend trust boundaries. No extraction receipt grants runtime capabilities.

C3-EXTRACT-004 — Failure and compatibility

Return unsupported for a type or layout outside the selected profile, rejected for malformed terms, invalid erasure, or mismatched contracts, and inconclusive for exhausted checking limits. Noncomputable retained axioms are rejected with their qualified names. Do not convert failure into a stub program, a fabricated witness, or a weaker contract.

The output uses the selected Algorithm edition and artifact format under their existing rules. Logical ZLM4 carries the extraction relation; it does not silently add Proof objects to ZLM1–3 or change how old loaders interpret bytes.