PrimeCoordinateReadoutCommitment
plain-language theorem explainer
The original D4 commitment is the proposition that a δ-prime-coordinate transform exists: every nonzero non-unit distinction natural carries prime-coordinate data. Factorization and goal-closure arguments cite it as the exact readout hypothesis, not a heuristic. It is definitionally the nonemptiness of that transform type, so exactness and recovery theorems reduce by unfolding.
Claim. The D4 readout commitment is the proposition that there exists a $\delta$-prime-coordinate transform: a map assigning prime-coordinate data to every nonzero non-unit distinction natural $N$.
background
In the primitive recognition calculus, factorization is framed as coordinate readout on distinction naturals. A $\delta$-prime-coordinate transform is the bold goal object: for every $N \neq 0$ that is not a unit, one obtains PrimeCoordinateData for $N$. Nonemptiness of that type is the mathematical content of having such a transform at all.
This module packages goal-closure bookkeeping for that claim. The D4 commitment is deliberately not a weaker benchmark: supplying it means supplying the full transform, not an external readout stub or a residual name alone. Upstream, the transform type is defined as the universal quantification over nonzero non-unit $N$; ledger-closure notions elsewhere (plaquette and domino parity) are separate holographic machinery and are not what this Prop asserts.
Locally, residual naming and transform provenance sit beside this commitment so a certificate can record both that the residual is the prime-coordinate readout and that the provenance is the native $\delta$-choice path.
proof idea
Definitional abbreviation only. The body is Nonempty DeltaPrimeCoordinateTransform, so the commitment is literally existence of an inhabitant of the bold transform type. No tactics; downstream exactness is rfl, and closedness is discharged by citing the native-choice existence theorem for the transform.
why it matters
This is the named D4 commitment that goal-closure certificates hang on. GoalClosureCertificate records residual naming and native $\delta$-readout provenance; the commitment itself is what primeCoordinateReadoutCommitment_closed proves via native-choice existence, and what primeCoordinateReadoutCommitment_exact equates with nonemptiness of the transform.
The payoff is primeCoordinateReadoutCommitment_recovers_prime_divisor: once the commitment is supplied, every nonzero non-unit $N$ has a prime-orbit divisor. That is the theorem-level content of "solving becomes coordinate readout." In the Recognition factorization stack it separates the bold existence claim from classical transport certificates kept on a parallel path.
It does not itself sit on the T0–T8 forcing chain; it is foundation-level bookkeeping that makes factor recovery a pure readout once the $\delta$-transform is present.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.