nativePrimeCoordinateData_exists
plain-language theorem explainer
Every nonzero non-unit distinction number admits a finite list of prime-power coordinates whose product recovers it. Builders of a native δ-prime-coordinate transform cite this existence result before choosing a witness. The argument is strong induction on the Nat display: prime orbits are single-coordinate base cases; otherwise a native nontrivial factorization splits into strictly smaller factors that the inductive hypothesis handles, and the coordinate lists concatenate.
Claim. For every distinction number $N$ with $N \neq 0$ and $N$ not a unit, there exists prime-coordinate data for $N$: a finite list of prime-power coordinates whose product equals $N$.
background
In the Primitive Recognition Calculus factorization layer, orbit numbers are values of DistinctionNat, equipped with a display map toNat into ordinary naturals (the forward iteration-count map from the arithmetic-from-logic bridge). Prime-coordinate data for such an $N$ is a structure packing a list of prime-power coordinates together with a reconstruction proof that their product equals $N$.
The module's bold goal object is a δ-prime-coordinate transform: a total assignment of such data to every nonzero non-unit $N$. Two routes are developed. One transports Mathlib's Nat.primeFactorsList through the δ/Nat display equivalence. The other, treated here, stays native: it splits on whether $N$ lies on a prime orbit and otherwise uses a nontrivial factorization into smaller factors.
Supporting facts already in the module: if $a\cdot b=N$ with both factors nonzero and the complementary factor non-unit, then each factor has strictly smaller toNat than $N$; and every nonzero non-unit non-prime-orbit number admits such a nontrivial factorization.
proof idea
An auxiliary statement is proved by strong induction on $n\in\mathbb{N}$: every $N$ with $N.\mathrm{toNat}=n$ that is nonzero and non-unit has nonempty prime-coordinate data.
At stage $n$, case-split on whether $N$ is a prime orbit. If yes, the single-prime constructor supplies the witness. If no, the native nontrivial-factorization lemma yields $a\cdot b=N$ with both factors nonzero and non-unit. The left/right factor-size lemmas give $a.\mathrm{toNat}<n$ and $b.\mathrm{toNat}<n$, so the inductive hypothesis produces data for $a$ and for $b$. Concatenate the two coordinate lists; reconstruction follows from the append-product lemma, the two reconstruction fields, and $a\cdot b=N$.
The outer proof specializes the auxiliary statement at $n=N.\mathrm{toNat}$.
why it matters
This theorem is the existence engine for the native-choice transform. Downstream, deltaPrimeCoordinateTransform_nativeChoice inhabits the bold goal type DeltaPrimeCoordinateTransform by classical choice on the nonempty type proved here, using the δ-native prime-orbit / nontrivial-factorization split and well-founded descent on the Nat display.
It therefore closes the native half of the prime-coordinate program in the foundation factorization module, as the counterpart to the classical-transport construction that routes through Mathlib's prime-factor list. Within Recognition Science this sits in the arithmetic layer that underwrites later mass and period readouts: factorization of orbit numbers into prime-power coordinates is the bookkeeping that lets rung data be written multiplicatively. The result is pure existence, not a complexity claim, and it does not replace the classical transport path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.