primePowerValue_of_natPrime_toNat
plain-language theorem explainer
A natural prime p, packaged as a unit-exponent prime-power coordinate and evaluated as an orbit, reads back as p under the verifier map toNat. Factorization and period-spectrum arguments cite this to connect Lean primes to DistinctionNat prime powers. The proof is a short simp unfolding the coordinate constructor and applying orbitPow_toNat with the ofNat round-trip.
Claim. For every natural number $p$ that is prime, if one forms the prime-power coordinate with base the $\delta$-orbit of $p$ and exponent $1$, then the verifier reading $\mathrm{toNat}$ of that coordinate's orbit value equals $p$.
background
In the Primitive Recognition Calculus, integers appear as DistinctionNat orbits (zero/succ structure) with a verifier map toNat that recovers ordinary Nat. The inverse ofNat embeds a Lean Nat into that orbit; toNat_ofNat states the round-trip identity toNat(ofNat n) = n.
A PrimePowerCoordinate is a pair (base, exponent) of DistinctionNat data with base a prime orbit and exponent nonzero. Its value is orbitPow base exponent, the orbit analogue of ordinary exponentiation. The theorem orbitPow_toNat records that this matches Nat power: (orbitPow a k).toNat = a.toNat ^ k.toNat.
primePowerCoordinateOfNatPrime packages a Lean prime p as the coordinate with base ofNat p and exponent one (the unit orbit). This module builds the prime-coordinate transform that factors orbits into such coordinates and reads periods back as ordinary products.
proof idea
Term-mode proof by a single simp. Unfolding primePowerValue and primePowerCoordinateOfNatPrime reduces the left-hand side to (orbitPow (ofNat p) one).toNat. orbitPow_toNat rewrites that as (ofNat p).toNat ^ one.toNat. one_toNat and toNat_ofNat collapse the power to p^1 = p.
why it matters
This is the single-prime base case for transporting Lean prime lists into DistinctionNat factorization data. Downstream, primeCoordinateProduct_fromNatList_toNat inducts on a list of primes and needs exactly this identity on each head: the product of unit-exponent prime-power coordinates reads back as the ordinary product of the primes.
In the Recognition foundation stack, arithmetic is rebuilt from logic/orbit structure before physical period readout. Closing the toNat bridge for prime powers keeps factorization native to DistinctionNat while remaining compatible with Mathlib's Nat.Prime. It does not itself invoke the forcing chain (T5–T8) or the J-cost; it is pure arithmetic scaffolding under PrimitiveRecognitionCalculus factorization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.