primeOrbit_iff_natPrime_toNat
plain-language theorem explainer
δ-primality of a finite distinction orbit is equivalent to ordinary Nat primality of its display value. Coordinate-factorization and uniqueness-certificate proofs cite this to move freely between the native primeOrbit predicate and Mathlib's Nat.Prime. The proof is a one-line Iff pairing of the two already-proved one-way bridges in the same module.
Claim. For every finite distinction orbit $p$, $p$ is a prime orbit if and only if its natural-number display is a prime: $\mathrm{primeOrbit}(p) \leftrightarrow \mathrm{Prime}(p^{\mathrm{toNat}})$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor, the δ-native stand-in for the naturals. Its verifier readout toNat sends zero to 0 and successor to Nat.succ, so every orbit has a canonical Nat display.
The predicate primeOrbit is the δ-native notion of primality on these orbits (from OrbitDivisibility): no nontrivial factor in the orbit sense. The two one-way bridges already in this module state that a prime orbit forces a Nat-prime display, and conversely that a Nat-prime display lifts to a prime orbit (via ofNat and the ofNat/toNat round-trip).
Local setting is CoordinateUniqueness inside PrimitiveRecognitionCalculus factorization: the goal is to inherit Mathlib's Nat.factorization structure on coordinate lists by identifying δ-primes with ordinary primes.
proof idea
Pure term-mode Iff constructor. Left-to-right is natPrime_toNat_of_primeOrbit (primeOrbit implies Nat.Prime of the display, via the no-nontrivial-factor characterization and Nat.prime_def_lt). Right-to-left is primeOrbit_of_natPrime_toNat (Nat.Prime of the display lifts through primeOrbit_ofNat_of_natPrime and ofNat_toNat). No extra tactics or rewriting at this site.
why it matters
This biconditional is the clean interface that lets the rest of the factorization stack treat δ-primes as ordinary primes. Downstream, coordinate_uniqueness_certificate records it as the field prime_orbit_iff_natPrime, and uses the forward direction for prime_orbit_displays_natPrime. That certificate packages the claim that coordinate lists induce unique Nat factorizations.
In the Recognition foundation layer this is bookkeeping rather than a forcing-chain step (T5–T8), but it is the bridge that makes prime-power coordinates machine-checkable: the next declaration installs DecidablePred primeOrbit by transporting Nat.Prime decidability across this iff. Without the equivalence, coordinate uniqueness would stay stuck on a native predicate with no Mathlib factorization API.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.