primeCoordinateProduct_toNat_ne_zero
plain-language theorem explainer
The LogicNat product of any finite list of prime-power coordinates converts under toNat to a nonzero natural number. Coordinate-factorization uniqueness proofs cite this to justify Nat.factorization on the reconstructed product. Proof is list induction: the empty product is one, and each prime-power factor is a positive power of a prime base, so the product stays nonzero.
Claim. For every finite list of prime-power coordinates, if $N$ is the natural number read from the LogicNat product of those coordinates, then $N \neq 0$.
background
In the Primitive Recognition Calculus, arithmetic is carried by LogicNat (iteration counts of a step from identity) with a forward map to ordinary Nat that recovers successor and multiplication. Prime-power coordinates package a prime orbit base with an exponent; their values are orbit powers, and a list of them multiplies to a single LogicNat product.
The sibling lemma that a prime-orbit base converts to a Nat prime supplies positivity of each base. Orbit-power conversion then turns each coordinate into a positive Nat power. The local module builds uniqueness of factorization read from coordinates against the canonical Nat factorization of that reconstructed product; non-vanishing of the product is the first arithmetic hygiene step before factorization is well-defined on it.
proof idea
List induction on the coordinate list. Nil case: the empty product is the LogicNat unit, and one_toNat gives $1 \neq 0$. Cons case: rewrite the product as the head prime-power value times the recursive product, then apply toNat_mul so the Nat image is a product of two Nats. The head base is a Nat prime by natPrime_toNat_of_primeOrbit, hence positive; orbitPow_toNat plus pow_ne_zero shows the head power is nonzero. The inductive hypothesis handles the tail; Nat.mul_ne_zero closes.
why it matters
Feeds coordinateFactorization_eq_factorization_product, whose doc-comment states that factorization read off a coordinate list equals the canonical Nat factorization of the reconstructed product. Without non-vanishing, Nat.factorization on that product is undefined or vacuous, so uniqueness of prime-coordinate data against ordinary factorization cannot even be stated.
In the foundation stack this is arithmetic hygiene for the recognition-side factorization bridge: LogicNat products of prime orbits must land in the positive naturals where unique factorization lives. It sits under CoordinateUniqueness rather than the T0–T8 forcing chain, but it is required infrastructure for reading ordinary prime factorization back from recognition coordinates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.