primeCoordinateReadoutCommitment_recovers_prime_divisor
plain-language theorem explainer
Under the prime-coordinate readout commitment (existence of a δ-prime-coordinate transform), every nonzero non-unit distinction orbit admits a prime orbit divisor. Factorization work in the Primitive Recognition Calculus cites this as the theorem-level content of "solving becomes coordinate readout." The proof unpacks the nonempty commitment and hands the witness to the corresponding transform recovery lemma.
Claim. If a $\delta$-prime-coordinate transform exists, then for every distinction number $N$ that is nonzero and non-unit there exists a prime orbit position $p$ such that $p$ divides $N$.
background
The ambient setting is the Primitive Recognition Calculus factorization layer. Distinction numbers are the base-neutral finite orbits of repeated distinction (K2.12): an inductive type with zero and successor. Native divisibility says $a$ divides $b$ when some orbit position $k$ satisfies $a \cdot k = b$. A prime orbit position is nonzero, non-unit, and free of nontrivial factorization.
The hypothesis is the original D4 commitment: it is exactly the assertion that a $\delta$-prime-coordinate transform exists, not a weaker benchmark. That commitment is closed by classical transport of the transform. Upstream, any such transform already makes factor recovery immediate for every nonzero non-unit orbit number: the transform supplies, for each such $N$, coordinate data whose prime factor is recovered on the spot.
proof idea
One-line wrapper. Destructure the commitment hypothesis as a nonempty package to obtain a concrete $\delta$-prime-coordinate transform $T$, then apply deltaPrimeCoordinateTransform_recovers_prime_divisor to $T$. No extra arithmetic is done here; all recovery work lives in that upstream lemma.
why it matters
This is the theorem-level content of the slogan "solving becomes coordinate readout": once the D4 residual commitment is supplied, prime-divisor recovery is immediate rather than algorithmic search. Downstream it is wired into goal_closure_certificate as the residual_would_recover field, so the D4 closure certificate records that factor recovery is closed by a native noncomputable $\delta$-choice transform (classical transport remaining a separate proved path on the transform certificate). It sits in the Foundation factorization stack that turns orbit arithmetic into certified prime recovery, feeding the broader goal-closure story rather than a physical constant identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.