coordinateFactorization
plain-language theorem explainer
Maps a list of prime-power coordinates to the finitely supported Nat exponent function: each base^e contributes multiplicity e at the natural readout of the base. Downstream uniqueness and classical-transport theorems cite this as the factorization readout that must equal Nat.factorization. The body is a direct map-then-sum of singleton Finsupps.
Claim. Given a finite list of prime-power coordinates $(b_i, e_i)$, where each $b_i$ is a prime orbit and each $e_i$ is a nonzero orbit exponent, return the finitely supported function $\sum_i e_i\,\delta_{\mathrm{toNat}(b_i)}$ on $\mathbb{N}$.
background
In the Primitive Recognition Calculus, integers are carried as distinction orbits (DistinctionNat), not bare Lean Nat. A PrimePowerCoordinate packages one prime orbit base together with a nonzero exponent orbit, both still in the orbit language. The verifier maps toNat read those orbits as ordinary natural numbers.
Factorization in this layer is therefore not assumed a priori on orbits. One first builds a list of prime-power coordinates, reconstructs a product orbit, and only then compares the induced exponent function against Mathlib's canonical Nat.factorization. The present definition is exactly that induced exponent function: the Nat-side multiset of primes read off the coordinate list.
The ambient module develops coordinate uniqueness: that any two such coordinate presentations of the same orbit yield the same factorization, and that a computable classical-transport transform produces the canonical one.
proof idea
Pure definition, not a proof. Map each coordinate c to the singleton Finsupp single (c.base.toNat) (c.exponent.toNat), then take the list sum in the additive monoid of finitely supported functions Nat →₀ Nat. Empty list sums to zero; cons is singleton plus the recursive sum (unfolded later by the companion lemmas).
why it matters
This is the readout bridge between δ-coordinate data and classical arithmetic. Parent results include coordinateFactorization_eq_factorization_product (readout equals Nat.factorization of the reconstructed product), coordinateFactorization_eq_factorization_of_data (specialized to reconstruction data for a fixed orbit N), and classicalTransport_readout_is_canonical (the computable classical-transport transform yields exactly the canonical factorization). The certificate structure CoordinateUniquenessCertificate packages these equalities as the coordinate-uniqueness layer of the foundation.
In Recognition Science terms this is bookkeeping for the arithmetic-from-logic stack that underwrites later forcing and measurement layers: primes and exponents must display as ordinary Nat primes before mass ladders and constants can be stated in RS-native units. It does not itself invoke T5–T8 or the RCL; it supplies the unique prime decomposition language those later steps rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.