primeOrbit_of_natPrime_toNat
plain-language theorem explainer
If a distinction-orbit displays as a classical prime, then the orbit itself is prime in the δ-sense. Factorization and coordinate-uniqueness arguments cite this as the converse half of the δ-primality bridge. The proof applies the ofNat-direction lemma and rewrites by the ofNat/toNat round-trip identity.
Claim. Let $p$ be a finite distinction-orbit. If its verifier display $p^{\mathrm{toNat}}\in\mathbb{N}$ is a prime number, then $p$ is a prime orbit (no nontrivial factorization in the $\delta$-calculus).
background
DistinctionNat is the base-neutral finite orbit of repeated distinction: an inductive type with zero and successor, standing for pure iteration count before any radix is chosen. The map toNat reads that orbit as a Lean natural number (the verifier display); ofNat builds an orbit from a natural. Their composition is identity: ofNat(toNat n)=n.
A prime orbit is the δ-calculus notion of primality: the orbit is nonzero, non-unit, and admits no nontrivial factorization in the orbit monoid. Classical Nat.Prime is the ordinary arithmetic predicate on the display.
The sibling lemma primeOrbit_ofNat_of_natPrime already lifts a classical prime $p\in\mathbb{N}$ to primeOrbit(ofNat p). The present statement is the converse bridge for an arbitrary orbit whose display is prime, needed so that δ-primality and Nat-primality of the display become equivalent.
proof idea
Term-mode, two steps. From the hypothesis Nat.Prime(p.toNat), apply primeOrbit_ofNat_of_natPrime to obtain primeOrbit(ofNat(p.toNat)). Rewrite that conclusion with ofNat_toNat, which replaces ofNat(toNat p) by p, yielding primeOrbit p. No case analysis on the orbit structure is required.
why it matters
Feeds the biconditional primeOrbit_iff_natPrime_toNat, whose doc-comment states that "δ primality is exactly Nat primality of the display." That equivalence immediately yields a DecidablePred instance for primeOrbit, so primality of distinction-orbits is machine-checkable via the classical display.
In the CoordinateUniqueness module this closes the transport between classical factorization data and δ-factorization: unique prime-coordinate factorizations can be stated and proved by moving freely between Nat.Prime and primeOrbit. It sits in the Primitive Recognition Calculus factorization layer, where arithmetic is recovered from pure distinction orbits rather than assumed as a base type. No forcing-chain landmark (T5–T8) is touched directly; the result is infrastructure for unique factorization of recognition coordinates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.