Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.CoordinateUniqueness

show as:
view Lean formalization →

δ-native prime orbits are forced to display as genuine natural primes, so coordinate readouts inherit Lean’s Nat.factorization uniqueness. The module builds the coordinate factorization map, proves it agrees with ordinary prime factorization of the product, and records uniqueness of prime-coordinate data. Anyone citing the factorization master certificate or uniqueness of RS coordinate factorizations needs this bridge. The argument is a short chain of equivalences plus inductive agreement with Mathlib factorization.

claimIf a coordinate orbit satisfies the $\delta$-native prime-orbit predicate, then its natural readout is a prime $p\in\mathbb{N}$. Conversely every natural prime arises this way. The coordinate factorization of a finite list of such orbits equals the Mathlib factorization of the product of their readouts, and that factorization data is unique.

background

In the Primitive Recognition Calculus, integers are not taken as primitive. Coordinates live in a $\delta$-native orbit language; the predicate primeOrbit marks those orbits that behave as primes under the recognition product. The upstream module PrimeCoordinateTransform supplies the readout map that sends an orbit to a natural number (and the inverse construction that lifts a natural prime back to an orbit).

This module sits in the Factorization layer: once orbits can be read as naturals, one wants the full strength of unique factorization in $\mathbb{N}$. Mathlib already provides Nat.factorization and its uniqueness theorems. The missing piece is a bridge theorem: prime-orbit display equals genuine primality of the readout, so lists of prime coordinates can be compared to ordinary prime factorizations of their product.

Sibling material defines the coordinate factorization of a list (nil and cons cases), shows the product of readouts is nonzero, and records that every coordinate base divides that product and is a prime divisor.

proof idea

The core is a two-way bridge: from prime-orbit to Nat.Prime of the readout, and the converse lift, packaged as an iff. Coordinate factorization is defined recursively on lists; agreement with Mathlib factorization of the product is proved by induction on that list structure, using the bridge at each cons step. Uniqueness of prime-coordinate data is then inherited from uniqueness of Nat.factorization once the two factorizations are identified. Supporting lemmas check nonzeroness of the product and the divisor/prime-divisor properties of each coordinate base.

why it matters in Recognition Science

Without this bridge, RS coordinate factorizations would be a parallel formal object with no link to classical unique factorization. The module is imported by MasterCertificate in the same Factorization tree, which packages the end-to-end certificate that recognition-side prime data is exactly ordinary prime factorization of the readout product.

In the broader Foundation stack this is bookkeeping rather than a forcing-chain step (not T5–T8), but it is the place where $\delta$-native language becomes eligible for every downstream argument that quotes uniqueness of factorization, multiplicity, or prime support. Closing the orbit-to-Nat.Prime equivalence is what lets later certificates cite Mathlib rather than re-prove unique factorization in orbit language.

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)