primeOrbit_ofNat_of_natPrime
plain-language theorem explainer
Classical Nat primes embed as prime orbit positions under the δ-orbit embedding ofNat. Anyone building prime-power coordinates or uniqueness bridges from Lean Nat primes into DistinctionNat cites this. The proof rewrites the native prime-orbit predicate to a no-nontrivial-factor statement on the display, then uses Nat.Prime divisibility.
Claim. If $p\in\mathbb{N}$ is prime, then the orbit position $\mathrm{ofNat}(p)$ is a prime orbit: nonzero, non-unit, and free of nontrivial factorization in the $\delta$-orbit monoid.
background
In the Primitive Recognition Calculus, orbit positions live in DistinctionNat, built from zero and successor. The map ofNat sends a Lean natural number into that orbit type; toNat is the inverse display, and toNat_ofNat records that the round-trip is the identity (K4.5).
A prime orbit is the native primality predicate on orbit positions: nonzero, not a unit, and with no nontrivial factorization. The bridge lemma primeOrbit_iff_toNat_no_nontrivial_factor says this is equivalent to the display natural being nonzero, not 1, and admitting no factorization $a\cdot b$ with both factors outside ${0,1}$. The module section is classical factorization transport back into $\delta$: moving Nat primes and factorizations into orbit language without importing Nat primality as the definition of orbit primality.
proof idea
Rewrite the goal with primeOrbit_iff_toNat_no_nontrivial_factor, then apply toNat_ofNat so the claim is about $p$ itself. The first two conjuncts are hp.ne_zero and hp.ne_one. For the factorization clause, take a putative $a,b$ with $a\cdot b=p$ and both outside ${0,1}$. Then $a\mid p$; Nat.Prime gives $a=1$ or $a=p$. The first case contradicts $a\neq 1$. The second forces $b=1$ by nlinarith with hp.pos, contradicting $b\neq 1$.
why it matters
This is the forward half of the Nat-prime / $\delta$-prime bridge. Downstream, primeOrbit_of_natPrime_toNat uses it (with ofNat_toNat) for the converse: Nat.Prime on the display lifts to a prime orbit. The same fact supplies the base_prime field of primePowerCoordinateOfNatPrime, which packages a classical prime as a single prime-power coordinate of exponent one.
In the Recognition factorization stack this is the entry point that lets classical unique factorization feed PrimeCoordinateData and assisted transforms without defining orbit primality by importing Nat.Prime. It sits under classical factorization transport into $\delta$, supporting coordinate uniqueness and reconstruction of orbit numbers from prime-power lists.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.