CoordinateUniquenessCertificate
plain-language theorem explainer
Bundles six Prop fields that certify uniqueness of prime-power coordinate factorizations on DistinctionNat orbits. Anyone citing the coordinate-uniqueness layer or the factorization character-theory master ledger needs this package. It is a pure interface structure; the inhabiting theorem fills each field from sibling lemmas equating prime orbits with Nat primes and coordinate lists with classical factorization.
Claim. A certificate asserting: (i) every prime orbit $p$ has $\mathrm{toNat}(p)$ a natural prime; (ii) $p$ is a prime orbit iff $\mathrm{toNat}(p)$ is prime; (iii) for any prime-coordinate datum of $N$, the Finsupp read from its coordinate list equals $\mathrm{Nat.factorization}(\mathrm{toNat}(N))$; (iv) any two such data for the same $N$ yield the same factorization; (v) every listed base is a prime orbit dividing $N$; (vi) if $N\neq 0$, a prime orbit divides $N$ exactly when it appears as a coordinate base.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive zero/succ type with verifier map $\mathrm{toNat}$ into Lean $\mathbb{N}$. Prime orbits are the orbit-level primes; divisibility is the orbit divisibility relation.
A PrimePowerCoordinate is a pair (base, exponent) with base a prime orbit and exponent nonzero. PrimeCoordinateData for $N$ is a list of such coordinates whose prime-coordinate product reconstructs $N$. The coordinate factorization of a list is the Finsupp sum of singles $\mathrm{base.toNat}\mapsto\mathrm{exponent.toNat}$.
This module sits in the Primitive Recognition Calculus factorization lane, after the prime-coordinate transform. The certificate packages the uniqueness and soundness claims that make the orbit factorization match classical Nat factorization.
proof idea
No proof body: this is a Prop-valued structure (certificate interface). Each field is a named hypothesis to be discharged by an inhabiting theorem. Downstream, coordinate_uniqueness_certificate fills the fields by applying sibling lemmas: natPrime_toNat_of_primeOrbit and primeOrbit_iff_natPrime_toNat for the prime-display and iff clauses; coordinateFactorization_eq_factorization_of_data and primeCoordinateData_factorization_unique for factorization identity and uniqueness; coordinate_base_is_prime_divisor and related membership lemmas for base soundness and readout completeness.
why it matters
This is the coordinate-uniqueness layer certificate in the factorization stack. Its inhabiting theorem coordinate_uniqueness_certificate is the concrete proof that the interface is realized. Downstream, DeltaFactorizationCharacterTheoryCertificate (the factorization character-theory master ledger) depends on this uniqueness package among chart transition, residue orbit, unit group, period spectrum, and finite multiplicative character certificates.
In the Recognition foundation, orbit arithmetic must recover classical unique factorization so later forcing and character-theoretic steps can treat prime-power coordinates as genuine primes. The certificate is definitional scaffolding for that bridge; it does not itself invoke T5–T8 or the RCL, but it underwrites the arithmetic substrate those landmarks sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.