coordinate_uniqueness_certificate
plain-language theorem explainer
Bundles the full uniqueness package for prime-coordinate factorizations of distinction numbers: prime orbits display as ordinary primes, any reconstruction data recovers the canonical Nat factorization, that readout is unique, and divisibility by a prime orbit is exactly list membership among coordinate bases. Cited by the master δ-factorization character-theory certificate. Proof is a pure field-by-field assembly of six already-proved lemmas.
Claim. There exists a coordinate-uniqueness certificate asserting: (i) every prime orbit $p$ has $p.{\rm toNat}$ a natural prime; (ii) $p$ is a prime orbit if and only if $p.{\rm toNat}$ is prime; (iii) for any prime-coordinate reconstruction data of $N$, the coordinate factorization equals $\mathrm{Nat.factorization}(N.{\rm toNat})$; (iv) any two such data for the same $N$ induce the same factorization; (v) every coordinate base is a prime orbit dividing $N$; (vi) for $N\neq 0$ and prime orbit $q$, $q\mid N$ if and only if $q$ appears as a coordinate base.
background
In the Primitive Recognition Calculus, integers are carried as distinction numbers (DistinctionNat) whose display map toNat lands in ordinary naturals. A prime orbit is the δ-native notion of primality: an orbit with no nontrivial factor in the distinction monoid. Prime-power coordinates package a base orbit with an exponent; a list of such coordinates that multiplies back to $N$ is PrimeCoordinateData N.
The coordinate factorization of a list is the multiset of prime powers read off those coordinates. The module sits in the factorization layer of PRC, bridging δ-native structure to Mathlib's Nat.factorization so that the fundamental theorem of arithmetic is available on the display without leaving the recognition calculus.
Upstream, natPrime_toNat_of_primeOrbit shows prime orbits display as genuine Nat primes; primeOrbit_iff_natPrime_toNat gives the full equivalence; coordinateFactorization_eq_factorization_of_data identifies the readout with the canonical factorization; primeCoordinateData_factorization_unique is FTA in δ coordinates; coordinate_base_is_prime_divisor makes base extraction sound; and primeOrbit_divides_iff_mem_coordinate_bases equates divisibility with list membership.
proof idea
The proof constructs a term of the certificate structure by discharging each field with a one-line appeal to an existing lemma.
prime_orbit_displays_natPrime: intro on the orbit hypothesis, thennatPrime_toNat_of_primeOrbit.prime_orbit_iff_natPrime: direct assignment ofprimeOrbit_iff_natPrime_toNat.factorization_of_data: intro on $N$ and data, thencoordinateFactorization_eq_factorization_of_data.factorization_unique: intro on two data packages, thenprimeCoordinateData_factorization_unique.coordinate_base_sound: intro on membership, thencoordinate_base_is_prime_divisor.readout_complete: intro on nonzero $N$ and a prime orbit, thenprimeOrbit_divides_iff_mem_coordinate_bases.
No new arithmetic is proved here; the certificate is a packaging layer.
why it matters
This certificate is the uniqueness spine of δ-coordinate factorization. Downstream it is consumed by delta_factorization_character_theory_certificate in the MasterCertificate module, which assembles chart transition, residue orbit, unit group, and period spectrum into the full character-theory package for factorization in the recognition calculus.
In the broader Recognition Science forcing chain, unique prime readout on distinction numbers is the arithmetic substrate on which later cost and ladder constructions rest: once factorization is unique and recoverable by list membership, J-cost evaluations and phi-ladder mass assignments can treat prime support as canonical rather than choice-dependent. The certificate closes the coordinate-uniqueness layer so the master factorization certificate can cite a single Prop rather than six separate lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.