GoalClosureCertificate
plain-language theorem explainer
D4 closure certificate: a Prop record that residual naming, native δ-transform provenance, exactness and closure of the prime-coordinate readout commitment, and prime-divisor recovery all hold together. Factorization auditors cite it to pin that factor recovery is discharged by a native noncomputable δ-choice (classical transport stays a separate path). The structure itself is definitional; the inhabiting theorem packs five sibling lemmas.
Claim. A D4 goal-closure certificate is the proposition that (i) the current residual label is prime-coordinate readout; (ii) transform provenance is native $\delta$-readout; (iii) the prime-coordinate readout commitment is equivalent to nonemptiness of a $\delta$-prime-coordinate transform $N\mapsto$ prime-coordinate data on every nonzero non-unit distinction-orbit $N$; (iv) that commitment holds; and (v) under the commitment, every such $N$ admits a prime orbit $p$ with $p\mid N$.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): zero and successor, with native multiplication and divisibility. A unit is the one-step orbit; divides means existence of a multiplier orbit. The bold goal object is a $\delta$-prime-coordinate transform: a (possibly noncomputable) map sending every nonzero non-unit orbit $N$ to prime-coordinate data on $N$.
The original D4 commitment is exactly nonemptiness of that transform, not a weaker benchmark. Module docs fix the residual name to prime-coordinate readout and the provenance to native $\delta$ choice by prime/factorization descent. Classical transport of the same transform is tracked on a separate certificate path.
This module packages those status facts into one Prop structure so downstream ledgers can demand a single closed residual rather than ad-hoc equalities.
proof idea
Definitional Prop structure, not a proved theorem. Five fields pin: residual name equality to prime-coordinate readout; provenance equality to native $\delta$-readout; biconditional of the readout commitment with Nonempty of the $\delta$-prime-coordinate transform; assertion of the commitment; and the recovery implication (commitment implies every nonzero non-unit orbit has a prime divisor under native divides).
No tactics here. The sibling theorem goal_closure_certificate inhabits the structure by feeding five local lemmas (current_residual_named, current_transform_provenance, exactness, closedness, and recover-prime-divisor).
why it matters
Closes the D4 residual in the factorization lane: factor recovery is recorded as closed by a native noncomputable $\delta$-choice transform, while classical transport remains the separate proved path named in the doc-comment. Downstream, goal_closure_certificate is the concrete inhabitant, and the master ledger DeltaFactorizationCharacterTheoryCertificate sits in the same factorization character-theory stack (chart transition, residue orbit, unit group, period spectrum, finite multiplicative characters).
In Recognition terms this is bookkeeping for the primitive orbit calculus that underwrites later forcing and mass-ladder work: without a closed prime-coordinate readout, prime factorization on distinction orbits stays an open residual. The certificate does not itself invoke T5–T8 or the RCL; it clears a foundation obligation those layers assume is settled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.