Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.CoordinateUniqueness

show as:
view Lean formalization →

δ-native prime orbits display as genuine natural primes, so coordinate factorizations inherit uniqueness from Nat.factorization. Anyone citing the prime-coordinate readout or MasterCertificate uniqueness needs this bridge. The argument pairs orbit-to-Nat roundtrips with inductive equality of coordinate and classical factorizations.

claimIf a coordinate orbit satisfies the $\delta$-native prime-orbit predicate, then its natural readout is a prime in $\mathbb{N}$, and conversely. The multiset of coordinate bases of a prime-coordinate datum therefore coincides with the unique $\mathrm{Nat.factorization}$ of the product readout.

background

In the Primitive Recognition Calculus factorization layer, primes first appear as orbits under $\delta$-native recognition dynamics, not as bare elements of $\mathbb{N}$. Upstream, PrimeCoordinateTransform supplies the readout map sending such orbits to natural numbers and back.

This module closes that loop. The module doc states that the $\delta$-native primeOrbit predicate forces the orbit display to be a genuine Nat prime, the bridge that lets the readout inherit Nat.factorization structure. Sibling material includes the iff between primeOrbit and natPrime after toNat, the recursive coordinateFactorization on nil/cons lists, product non-vanishing, and the uniqueness theorem for prime-coordinate data.

proof idea

Theorem-heavy module, not a pure definition dump. Roundtrip lemmas show that toNat of a prime orbit is a Nat prime and conversely, yielding an iff. coordinateFactorization is defined by recursion on the coordinate list (nil and cons). Equality with Nat.factorization of the product is proved inductively, using that each coordinate base is a prime divisor of the product and that list membership implies divisibility. Uniqueness of prime-coordinate factorization then follows from uniqueness of classical Nat.factorization.

why it matters in Recognition Science

MasterCertificate imports this module to certify that the $\delta$-native factorization readout is exactly the unique classical prime factorization. Without the primeOrbit $\leftrightarrow$ Nat.prime bridge, the coordinate layer could not inherit Mathlib factorization uniqueness. In the Recognition foundation stack this sits inside PrimitiveRecognitionCalculus.Factorization and feeds the master certificate that the coordinate presentation of integers is faithful. It is pure arithmetic scaffolding for later recognition readout, not a physics forcing step.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (18)