natPrime_toNat_of_primeOrbit
plain-language theorem explainer
If a distinction-natural lies on a prime orbit, its ordinary natural readout is a genuine Nat prime. Anyone wiring δ-native factorization to Mathlib's Nat.factorization cites this one-way bridge. The proof rewrites the orbit predicate as absence of nontrivial factors and matches Mathlib's prime_def_lt characterization by a short contradiction on proper divisors.
Claim. Let $p$ be a distinction-natural. If $p$ satisfies the $\delta$-native prime-orbit predicate, then the ordinary natural number displayed by $p$ is prime: $\mathrm{Nat.Prime}(p^{\downarrow})$.
background
In the Primitive Recognition Calculus, distinction-naturals carry a $\delta$-native arithmetic whose readout map sends each object to an ordinary natural number. A prime orbit is the $\delta$-side primality predicate: the display is nonzero, not one, and admits no nontrivial factor pair in ordinary arithmetic.
The module CoordinateUniqueness lives under Factorization and imports the prime-coordinate transform. Its role is to identify when $\delta$-coordinate data recover ordinary unique factorization on the readout. The present result is the one-way bridge from the orbit predicate to Mathlib primality, so that Nat.factorization becomes available on displays.
Sibling material includes the converse lift (a Nat prime display returns a prime orbit), the resulting iff, and uniqueness lemmas for prime-coordinate factorization data.
proof idea
Rewrite the hypothesis with the characterization that a prime orbit means the display is nonzero, not equal to one, and has no nontrivial factor pair. Unpack that triple. Switch to Mathlib's Nat.prime_def_lt: the display is at least 2 (omega from the nonzero/not-one facts), and every proper positive divisor must be 1.
Given $m < p^{\downarrow}$ dividing the display, take the cofactor $k$. Assume for contradiction $m \neq 1$. Feed $(m,k)$ into the no-nontrivial-factor clause: neither factor can be zero (else the product is zero, contradicting the nonzero display), and $k$ cannot be 1 (else the display equals $m$, contradicting the strict size bound). That closes the contradiction.
why it matters
Per the doc-comment, this is the bridge that lets the $\delta$-readout inherit Nat.factorization structure. Sibling targets in the same module (the converse lift, the iff form, coordinate-factorization product identities, and uniqueness of prime-coordinate data) all need ordinary primality of displays before Mathlib's factorization API can be transferred back into $\delta$-coordinates.
In the Recognition foundation layer this keeps the primitive recognition calculus aligned with classical unique factorization without re-proving primality from scratch on the $\delta$ side. It does not itself invoke the forcing chain T0–T8, the Recognition Composition Law, or the $J$-cost; it supports the arithmetic substrate on which later coordinate and rung constructions sit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.