goal_closure_certificate
plain-language theorem explainer
Packages the D4 goal-closure certificate: the prime-coordinate residual is named as readout, provenance is native δ-choice, the readout commitment is exact and closed, and that commitment recovers a prime divisor of any non-zero non-unit. Downstream master δ-factorization character-theory work cites it. Proof is a term-mode structure fill from five local lemmas (two by rfl, three existence/recovery facts).
Claim. A D4 goal-closure certificate holds: the current prime-coordinate residual equals the readout residual; its transform provenance is the native $\delta$-choice readout; the prime-coordinate readout commitment is equivalent to nonemptiness of a $\delta$-prime-coordinate transform and is inhabited; and any such commitment yields, for every non-zero non-unit distinction natural $N$, some $p$ on a prime orbit that divides $N$.
background
In the Primitive Recognition Calculus factorization layer, integer factor recovery is rephrased as a coordinate problem on distinction naturals. The residual under study is tagged primeCoordinateReadout: solving is meant to become reading a prime coordinate rather than searching. Provenance is fixed to the native noncomputable $\delta$-choice transform (as opposed to a classical transport path recorded elsewhere).
PrimeCoordinateReadoutCommitment is the Prop that a $\delta$-prime-coordinate transform exists. Exactness is definitional equivalence of that commitment with Nonempty DeltaPrimeCoordinateTransform. Closure is the theorem-ledger fact that the native-choice transform supplies an inhabitant. The recovery lemma states the content of "solving becomes coordinate readout": from the commitment one obtains, for every non-zero non-unit $N$, a prime-orbit divisor of $N$.
GoalClosureCertificate is the D4 bundle of these five facts. Classical transport remains a separate proved path in the prime-coordinate transform certificate; this certificate only closes the native $\delta$-readout route.
proof idea
Term-mode structure construction, not a tactic script. Each field of GoalClosureCertificate is filled by a named local lemma:
- residual name and transform provenance are
rflequalities (current_residual_named,current_transform_provenance); - exactness is again definitional (
primeCoordinateReadoutCommitment_exact, proved byrfl); - closedness invokes
deltaPrimeCoordinateTransform_nativeChoice_existsviaprimeCoordinateReadoutCommitment_closed; - recovery is
primeCoordinateReadoutCommitment_recovers_prime_divisor, which unpacks the commitment to a transformTand appliesdeltaPrimeCoordinateTransform_recovers_prime_divisor T.
No new arithmetic is done here; the certificate only assembles already-proved ledger facts.
why it matters
This is the D4 closure node for native $\delta$-choice factor recovery in the Recognition factorization stack. It records, in one Prop, that the residual is correctly named, provenance is native readout, the commitment is exact and closed, and factor recovery is immediate from that commitment.
It feeds delta_factorization_character_theory_certificate in the master certificate module, which aggregates chart transition, residue orbit, unit group, and period spectrum into the character-theory side of $\delta$-factorization. Without goal closure, the master bundle cannot claim that the native readout path actually finishes factor recovery.
Relative to the RS forcing chain, this sits in foundation bookkeeping rather than T5–T8 physics forcing: it is ledger hygiene for the factorization calculus that later mass and period arguments rely on. Classical transport is deliberately out of scope here and lives on the separate transform-certificate path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.