natPrimeFactorCoordinates
plain-language theorem explainer
Maps a natural number to its list of prime-power coordinates by reading Mathlib's multiset of prime factors and packaging each factor as a prime orbit with unit exponent. Factorization and classical-transport arguments cite it as the concrete coordinate readout on ordinary Nat. The body is a thin wrapper that feeds primeFactorsList into the list converter with the standard primality certificate.
Claim. For every natural number $n$, return the finite list of prime-power coordinates obtained from the multiset of prime factors of $n$: each prime $p$ appearing in that multiset becomes one coordinate whose base is the corresponding prime orbit and whose exponent is the unit (nonzero) distinction integer.
background
In the Primitive Recognition Calculus factorization layer, ordinary natural numbers are displayed as products of prime-power coordinates. A prime-power coordinate is a pair (base, exponent) where the base is a DistinctionNat lying on a prime orbit and the exponent is a nonzero DistinctionNat. The product of such coordinates reconstructs the original integer in the $\delta$/Nat display.
Mathlib already supplies Nat.primeFactorsList, the nondecreasing list of prime factors of $n$ counted with multiplicity. The sibling converter primeCoordinatesFromNatList turns any list of ordinary primes (with a primality proof for each entry) into a list of PrimePowerCoordinate values, one coordinate per list entry, each carrying unit exponent.
This definition simply specialises that converter to the canonical factor list of $n$, so the coordinate readout is classical rather than a new arithmetic algorithm.
proof idea
One-line definitional wrapper. Apply primeCoordinatesFromNatList to n.primeFactorsList, discharging the required hypothesis $\forall p\in L,,\mathrm{Nat.Prime},p$ by Nat.prime_of_mem_primeFactorsList on each membership proof. No further arithmetic is performed.
why it matters
Supplies the concrete Nat-side coordinate list used by the classical-transport construction of the $\delta$ prime-coordinate transform. Downstream, deltaPrimeCoordinateTransform_classicalTransport sets coordinates := natPrimeFactorCoordinates N.toNat and then proves reconstruction, closing the transform as transport of Mathlib factorisation rather than a new factoring method. The companion identity primeCoordinateProduct_natPrimeFactorCoordinates_toNat shows that the product of these coordinates recovers n.primeFactorsList.prod, tying the RS coordinate product back to ordinary unique factorisation. In the broader foundation stack this is bookkeeping that lets prime-orbit geometry talk to classical Nat without inventing new number theory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.