primeCoordinateReadoutCommitment_exact
plain-language theorem explainer
The D4 prime-coordinate readout commitment is definitionally the same proposition as existence of a δ-prime-coordinate transform. Factorization goal-closure work cites this to pin the residual name to the bold transform object, not a weaker benchmark. The proof is pure reflexivity from the commitment's definitional unfolding.
Claim. The original D4 prime-coordinate readout commitment holds if and only if there exists a $\delta$-prime-coordinate transform: a map that, for every nonzero non-unit distinction natural $N$, supplies prime-coordinate data for $N$.
background
In the Primitive Recognition Calculus factorization layer, the bold goal object is a $\delta$-prime-coordinate transform: for every distinction natural $N$ that is neither zero nor a unit, one must produce prime-coordinate data on $N$. The D4 readout commitment is the ledger name for that goal. By definition it is exactly the proposition that such a transform exists (as a nonempty type of total maps), not a heuristic score or external oracle.
The surrounding GoalClosure module packages residual naming, transform provenance, and recovery of prime divisors into a single certificate. Upstream, DeltaPrimeCoordinateTransform is documented as "the bold goal object"; the commitment doc states that supplying it "is exactly supplying the $\delta$-prime-coordinate transform, not a weaker benchmark or heuristic," and that it is closed by the classical-transport construction of the transform.
proof idea
One-line reflexivity. The commitment is defined by def as Nonempty DeltaPrimeCoordinateTransform, so the biconditional is definitional equality and rfl closes it with no lemmas or case splits.
why it matters
This pins the residual slot in the factorization goal-closure certificate. Downstream, goal_closure_certificate records residual_exact := primeCoordinateReadoutCommitment_exact alongside residual naming, transform provenance, closure, and prime-divisor recovery. Without the exactness link, the ledger could treat the D4 commitment as a looser benchmark; with it, certificate consumers know the residual is literally existence of the $\delta$-prime transform. In the Recognition foundation stack this is bookkeeping for the factorization goal, not a forcing-chain step (T5–T8), but it keeps the commitment honest relative to the native-choice transform that closes it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.