PrimeCoordinateTransformCertificate
plain-language theorem explainer
Certificate packaging the prime-coordinate transform interface on distinction orbits: reconstruction of N from its prime-power list, existence of a δ-transform, nonempty coordinates for non-units, and recovery of a prime divisor. Factorization goal-closure and the character-theory master ledger cite it. Pure Prop structure; the companion instance theorem fills each field from local lemmas.
Claim. A certificate asserting: (i) every prime-coordinate datum for an orbit number $N$ multiplies back to $N$; (ii) a $\delta$-prime-coordinate transform exists (both classical-transport and native-choice witnesses); (iii) if $N$ is not a unit then its coordinate list is nonempty; (iv) any such transform yields, for every nonzero non-unit $N$, a prime orbit position $p$ that divides $N$.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12). Native divisibility says $a$ divides $b$ when some orbit $k$ satisfies $a\cdot k=b$; the only multiplicative unit is the one-step orbit. A prime orbit position is nonzero, non-unit, and free of nontrivial factorization.
Prime-coordinate data for $N$ is a list of prime-power coordinates whose product (via successive primePowerValue multiplications, empty product = one) equals $N$. The bold goal object is a $\delta$-prime-coordinate transform: a map sending every nonzero non-unit $N$ to such data.
This module sits in the factorization lane under Foundation, importing physical period readout. The certificate is the Prop-level interface that later goal-closure and master ledgers demand before claiming "solving becomes coordinate readout."
proof idea
No proof body: this is a structure-as-Prop bundling five fields. Reconstruction is the field already stored on PrimeCoordinateData. The two existence fields are Nonempty wrappers around the same transform type (classical transport vs native choice). Nonunit-nonempty forces the coordinate list off [] when $N$ is not a unit. The recovery field is an implication: given any transform, every nonzero non-unit $N$ admits a prime orbit divisor. The companion theorem prime_coordinate_transform_certificate discharges the bundle by pointing each field at local lemmas (primeCoordinateData_reconstructs, existence proofs, etc.).
why it matters
This is the interface contract for the prime-coordinate transform lane inside factorization character theory. Downstream, prime_coordinate_transform_certificate builds a concrete instance; primeCoordinateReadoutCommitment_recovers_prime_divisor then shows that once a named residual commitment supplies a transform, factor recovery is immediate ("solving becomes coordinate readout"). The master ledger DeltaFactorizationCharacterTheoryCertificate aggregates chart transition, residue orbit, unit group, period spectrum, and finite multiplicative character certificates; this transform certificate is the factorization-facing hinge those lanes close against.
In Recognition terms it is scaffolding for native prime factorization on distinction orbits, not yet a forcing-chain (T0–T8) step. It does not touch J-uniqueness, $\varphi$, the eight-tick octave, or $D=3$; it only organizes how orbit numbers split into prime-power coordinates so later physical readout can name a divisor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.