orbitPow_toNat
plain-language theorem explainer
Native orbit exponentiation on DistinctionNat agrees with ordinary natural-number power after reading off iteration counts. Anyone working period spectra, Euler residues, or prime-power coordinates cites this bridge. The proof is induction on the exponent, using the recovery theorems for multiplication and successor.
Claim. For distinction-native naturals $a$ and $k$, the iteration count of the native power $a^{\langle k\rangle}$ equals the ordinary power of the counts: $\mathrm{toNat}(a^{\langle k\rangle}) = \mathrm{toNat}(a)^{\mathrm{toNat}(k)}$.
background
DistinctionNat is the recognition-native copy of the naturals built from the logic orbit (identity and step). The map toNat reads off the iteration count into ordinary Nat. Multiplication and successor on DistinctionNat are already known to recover ordinary arithmetic under this map (toNat_mul, toNat_succ).
In the PeriodSpectrum module, orbitPow a k is δ-native exponentiation by an orbit exponent: it returns the unit at zero and multiplies by $a$ at each successor. Periods, unit residues, and factorization witnesses are all stated in this native layer, so one needs a clean bridge from native powers back to Nat powers.
The local setting is the factorization stack that turns period data (Euler exponents, even-period gaps, prime-power coordinates) into nontrivial factorizations of a modulus $N$.
proof idea
Induction on the exponent $k$.
Base case $k = 0$: orbitPow a 0 is the native unit, and toNat of the unit is $1$, matching $a^{0}$.
Successor step: rewrite orbitPow a (succ k) as orbitPow a k * a via orbitPow_succ, push toNat through multiplication with toNat_mul, apply the inductive hypothesis, and convert the successor exponent with toNat_succ. The remaining equality is ordinary Nat.pow_succ.
why it matters
This is the display lemma for native powers inside the period-spectrum certificate: period_spectrum_certificate records it as pow_display, and orbitPow_unitResidue uses it to push unit-residue closure through powers.
Downstream, Euler's theorem in the residue layer (eulerPeriod_returns_one) rewrites native powers to Nat powers before invoking ordinary coprimality arithmetic. Even-period-gap factoring (nontrivialFactorization_of_evenPeriodGapWitness) and the prime-coordinate uniqueness stack (coordinateFactorization_eq_factorization_product, primePowerValue_of_natPrime_toNat) likewise need native powers to match canonical Nat factorization.
In the Recognition foundation, this is arithmetic recovery for the factorization side of Primitive Recognition Calculus: periods live on the δ-orbit, while classical number theory lives on Nat. Without the bridge, period witnesses cannot export ordinary factors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.