coordinateFactorization_nil
plain-language theorem explainer
The empty list of prime-power coordinates yields the zero finitely supported exponent map. Anyone proving that coordinate-read factorizations match Nat.factorization cites this as the nil base case. The proof is a one-line simp unfolding of the sum-of-singles definition.
Claim. Reading prime exponents off the empty list of prime-power coordinates yields the zero map in $\mathbb{N}\to_0\mathbb{N}$: every prime has exponent $0$.
background
In the Primitive Recognition Calculus factorization layer, a prime-power coordinate packages a prime orbit base with a natural exponent. The coordinate factorization of a list is the finitely supported function on $\mathbb{N}$ obtained by summing, over each coordinate $c$, the singleton Finsupp that places exponent $c.\mathrm{exponent}$ at the natural number underlying $c.\mathrm{base}$.
That construction is the bridge between geometric prime-orbit data and ordinary unique factorization of natural numbers. The empty list is the unit for list concatenation and the zero of the Finsupp monoid, so its image must be the zero support map. Downstream uniqueness arguments induct on the coordinate list and need this nil identity as the base step.
proof idea
One-line wrapper: simp unfolds coordinateFactorization on []. The mapped list is empty, the Finsupp sum of an empty list is definitionally 0, and the goal closes.
why it matters
This is the nil base case for the induction proving that the factorization read off a coordinate list equals the canonical Nat.factorization of the reconstructed product. The same nil case anchors the support-membership lemma: nothing lies in the support of the empty factorization. Together those results feed coordinate uniqueness for prime-coordinate data, the algebraic backbone that lets Recognition Science treat geometric prime orbits as ordinary prime factors when reconstructing distinction naturals. No open scaffolding remains; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.