natPrime_toNat_of_primeOrbit
plain-language theorem explainer
If a distinction-native natural number lies on a prime orbit, its ordinary readout is a classical prime. Factorization and coordinate-uniqueness arguments cite this bridge so δ-native primality can inherit Mathlib's Nat.factorization API without baking Nat primes into the predicate. The proof rewrites the orbit predicate as absence of nontrivial factors, then matches Nat.prime_def by case analysis on putative factors.
Claim. Let $p$ be a distinction-native natural number. If $p$ satisfies the $\delta$-native prime-orbit predicate (no nontrivial factorization in the native arithmetic), then the ordinary natural-number display $p^{\mathrm{toNat}}$ is a classical prime.
background
In the Primitive Recognition Calculus, arithmetic is built from distinction orbits rather than from Mathlib naturals. DistinctionNat is the native carrier; toNat is the forward readout that counts iteration steps down to an ordinary Nat (the same pattern as the LogicNat display in ArithmeticFromLogic).
Native primality is the predicate primeOrbit: an orbit is prime when its display is neither $0$ nor $1$ and admits no nontrivial factorization in the native multiplication. The supporting rewrite primeOrbit_iff_toNat_no_nontrivial_factor packages exactly those three conditions on the readout. Classical primality is Mathlib's Nat.Prime.
This lemma is the one-way bridge from the $\delta$-native predicate to Nat.Prime. A sibling in Factorization.CoordinateUniqueness records the same statement for the coordinate-uniqueness certificate; the present copy lives in the native-cost uniqueness module so cost and factorization arguments can share the bridge without circular imports of Nat prime theory into the predicate itself.
proof idea
Rewrite the hypothesis with primeOrbit_iff_toNat_no_nontrivial_factor, obtaining $p^{\mathrm{toNat}} \neq 0$, $\neq 1$, and a no-nontrivial-factor clause. Unfold Nat.prime_def: the lower bound $p^{\mathrm{toNat}} \ge 2$ is immediate by omega.
For the divisor clause, take any $m$ with $m \mid p^{\mathrm{toNat}}$, written $p^{\mathrm{toNat}} = m \cdot k$. If $m = 1$, done. Otherwise argue $k = 1$ (hence $m = p^{\mathrm{toNat}}$): if both $m$ and $k$ differ from $1$, neither can be $0$ (else zero_mul / mul_zero would force the product to $0$, contradicting the nonzero clause), so the pair is a forbidden nontrivial factorization, contradicting the orbit hypothesis. The identity $m \cdot 1 = m$ uses mul_one.
why it matters
Coordinate uniqueness and native-cost certificates need Mathlib factorization on readouts while keeping primality defined only in $\delta$-native language. Downstream, primeOrbit_iff_natPrime_toNat upgrades this one-way map to an equivalence (so primeOrbit becomes decidable), coordinate_uniqueness_certificate installs it as the field prime_orbit_displays_natPrime, and prime_divisor_is_coordinate_base uses it to prove every native prime divisor appears as a coordinate base.
That completeness feeds coordinateFactorization_eq_factorization_product and the nonvanishing of prime-coordinate products. On the cost side, the Liouville-twist and RCL-spike native-cost certificates invoke the same bridge when stripping auxiliary hypotheses. In the Recognition stack this is foundation plumbing: unique prime-axis coordinates on the display are what let later J-cost and doubled-trace arguments treat prime axes as well-defined parameters, not a forcing-chain landmark (T5–T8) by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.