DeltaPrimeCoordinateTransform
plain-language theorem explainer
The δ-prime-coordinate transform is the type of assignments that, for every nonzero non-unit finite distinction orbit, supply prime-power coordinates whose product recovers that orbit. Factorization and D4 goal-closure work cite it as the bold readout goal object. The declaration is a pure type definition: a universal quantifier over nontrivial orbits, not a constructed map.
Claim. A $\delta$-prime-coordinate transform is any rule that, given a finite distinction orbit $N$ that is nonzero and not the multiplicative unit (the one-step orbit), returns prime-power coordinate data whose product equals $N$.
background
In the primitive recognition calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction: an inductive copy of the naturals built from zero and successor. Multiplicative structure on these orbits has a native unit predicate: the only unit is the one-step orbit. Nontrivial factorization therefore concerns orbits that are neither zero nor that unit.
Prime-coordinate data for an orbit $N$ is a list of prime-power coordinates together with a reconstruction equality: the product of those coordinates equals $N$. The present declaration packages the claim that every nontrivial orbit admits such data.
The surrounding module sits in the factorization layer of the foundation stack (importing the physical-period readout). Upstream anchors such as active edge count $A=1$ and the forcing of $D=3$ with eight-tick period fix the broader RS setting, but this type itself is purely about orbit factorization.
proof idea
Definitional, not a proof. The body is the type of total functions sending each nonzero non-unit distinction orbit to a PrimeCoordinateData package (coordinate list plus reconstruction proof). No tactics or lemmas are applied; later declarations inhabit the type by classical transport from Mathlib prime-factor lists or by noncomputable native descent.
why it matters
This is the bold D4 goal object for prime-coordinate readout. Downstream, the original commitment is exactly nonemptiness of this type, and that equivalence is recorded as an identity. Goal-closure certificates require provenance that the residual is closed by a native $\delta$-choice transform of this shape.
Concrete inhabitants include classical transport through the $\delta$/Nat display equivalence (using Mathlib factor lists, not a new factoring algorithm) and a noncomputable native-choice transform via prime-orbit / nontrivial-factorization descent. Existence of the type as a nonempty Prop is what closes the readout commitment in the theorem ledger. It does not itself force $D=3$ or the eight-tick octave; those live in the unified forcing chain and only frame why factorization of distinction orbits matters for physical period readout.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.