coordinateFactorization_cons
plain-language theorem explainer
Prepending one prime-power coordinate to a list adds exactly that base-exponent pair into the Finsupp factorization of the list. Anyone proving uniqueness or support facts for coordinate factorizations cites this cons law. The proof is a one-line simp unfolding the list-sum definition.
Claim. For any prime-power coordinate $c$ (prime orbit base with nonzero exponent) and any list $L$ of such coordinates, the Nat factorization read from $c::L$ equals the finitely supported function that places $\mathrm{exp}(c)$ at the Nat image of the base of $c$, plus the factorization of $L$.
background
In the primitive recognition calculus, integers arise as orbits under a distinction step. A PrimePowerCoordinate packages one prime orbit base together with a nonzero exponent orbit; both are DistinctionNat values, read into ordinary Nat by the orbit toNat map (iteration count from zero).
The list-level map coordinateFactorization turns a list of such coordinates into a finitely supported function $\mathbb{N}\to_0\mathbb{N}$: each coordinate contributes a singleton Finsupp at base.toNat with multiplicity exponent.toNat, and the list is summed. This is the bridge from RS prime-orbit data to classical Nat factorization support.
The module sits under factorization uniqueness: one wants the factorization read off coordinates to match Nat.factorization of the reconstructed product, and to know that support points are exactly the bases that appear.
proof idea
One-line wrapper. Unfold coordinateFactorization, then apply List.map_cons and List.sum_cons so the head singleton Finsupp separates from the sum over the tail. No arithmetic lemmas are needed beyond the definitional sum.
why it matters
This is the inductive step fuel for the uniqueness pipeline in the same module. Downstream, coordinateFactorization_eq_factorization_product inducts on the coordinate list and uses the cons law to match Nat.factorization of the reconstructed product; mem_support_coordinateFactorization likewise inducts and reads support membership off the head-or-tail split.
In the broader Recognition foundation, prime-orbit coordinates are the RS-native encoding of prime powers before classical arithmetic is recovered. Getting list factorization to behave under cons is the elementary bookkeeping that lets uniqueness of prime-coordinate data land on standard unique factorization, rather than an ad-hoc RS product. It does not itself invoke the forcing chain (T5–T8) or the J-cost; it is pure arithmetic scaffolding under PrimitiveRecognitionCalculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.