classicalTransport_readout_is_canonical
plain-language theorem explainer
For every nonzero nonunit distinction-orbit number N, the classical-transport δ prime-coordinate transform yields a coordinate list whose induced factorization equals the ordinary Nat.factorization of N's display. Anyone citing the computable δ transform as recovering the canonical prime decomposition needs this equality. The proof is a one-line application of the reconstruction-data specialization of coordinate factorization.
Claim. Let $N$ be a nonzero nonunit distinction-orbit number. Write $T(N)$ for the classical-transport $\delta$ prime-coordinate transform of $N$. Then the factorization read off the coordinate list of $T(N)$ equals the canonical factorization $\mathrm{Nat.factorization}(n)$, where $n$ is the natural-number display of $N$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor. Its display map toNat reads off the iteration count as an ordinary natural number. Nonzero nonunit orbits are those with display at least 2, so they admit a nontrivial prime factorization.
A prime-power coordinate is a pair (base, exponent) with prime base. The map coordinateFactorization turns a list of such coordinates into a finitely supported function $\mathbb{N}\to_0\mathbb{N}$ by summing Finsupp.single base exponent over the list: each coordinate contributes its exponent to its base prime.
The classical-transport transform deltaPrimeCoordinateTransform_classicalTransport is a theorem-level $\delta$ prime-coordinate transform obtained by carrying Mathlib's Nat.primeFactorsList across the established $\delta$/Nat display equivalence. Its doc states it "closes the transform as a classical transport theorem; it is not a new fast factoring algorithm." The upstream lemma coordinateFactorization_eq_factorization_of_data asserts that for any reconstruction data of $N$, the coordinate readout equals Nat.factorization N.toNat.
proof idea
One-line term proof. The classical-transport transform packages a PrimeCoordinateData N record (coordinates plus a reconstruction witness). Applying coordinateFactorization_eq_factorization_of_data to that record immediately yields
coordinateFactorization (data.coordinates) = Nat.factorization N.toNat.
The underscore lets Lean fill the data argument from the transform application. No further case analysis or arithmetic is required; the work sits in the reconstruction equality already proved for any such data.
why it matters
This certificate sits in the coordinate-uniqueness layer of the Primitive Recognition Calculus factorization stack. The module doc marks it as the certificate that the classical-transport readout is the canonical prime decomposition. Together with uniqueness of prime-coordinate factorizations (the sibling FTA-in-$\delta$-coordinates result), it shows there is a computable $\delta$ transform whose output is exactly Mathlib's factorization, not some exotic alternative basis.
In the Recognition framework this anchors arithmetic factorization inside the distinction-orbit calculus: primes and exponents are recovered from orbit structure via the display equivalence, rather than postulated externally. No downstream consumers are wired yet (used_by is empty), so the result is presently a leaf certificate for the factorization layer rather than an intermediate step in a larger proved chain. It does not touch the forcing chain T0–T8, RCL, or the mass ladder directly; its role is foundational bookkeeping for $\delta$-coordinate arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.