orbitPow
plain-language theorem explainer
Defines native powering on the distinction orbit: raise a base residue a to an orbit exponent k by recursion (a^0 = 1, a^{k+1} = a^k · a). Anyone working period finding, Euler exponents, or even-period-gap factoring in the δ-layer cites this. The body is a plain recursive equation on DistinctionNat, not a proved theorem.
Claim. For a base $a$ in the distinction naturals, define the orbit power $a^{(\cdot)}$ by $a^{(0)} = 1$ and $a^{(k+1)} = a^{(k)} \cdot a$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with constructors zero and succ, the δ-native stand-in for ordinary natural numbers. Multiplication and the unit one live on the same type, so powering can be written without leaving the recognition layer.
Successor on this type is one more application of the generator, matching the Peano-style arithmetic built from logic elsewhere in the foundation. The PeriodSpectrum module uses this powering as the primitive that turns an exponent (an orbit length) into a residue, which is then compared modulo N via sameResidue and unitResidue.
Downstream period and factoring surfaces all phrase "return to the identity after k steps" as equality of orbitPow a k with one in the residue sense.
proof idea
No proof: this is a recursive definition by pattern match on the exponent. The zero case returns one; the successor case multiplies the recursive value by the fixed base a. Companion lemmas orbitPow_zero and orbitPow_succ are reflexivity wrappers; orbitPow_toNat is the bridge that identifies the native power with ordinary Nat exponentiation after toNat.
why it matters
This is the single powering primitive for the factorization stack. EvenPeriodGapWitness packages a unit base whose full period half+half returns to one under orbitPow while the half-power avoids 1 and -1, exactly the Shor configuration after period finding. nontrivialFactorization_of_evenPeriodGapWitness then turns that witness into a native nontrivial factorization of N.
On the existence side, eulerPeriod_returns_one states Euler's theorem in the δ residue layer as orbitPow a (periodExponent N) ≡ 1 mod N for unit residues, and PeriodExistenceCertificate records that surface. Sibling lemmas orbitPow_toNat and orbitPow_unitResidue make the Nat and unit-residue interfaces usable. In the broader Recognition chain this sits under primitive recognition calculus factorization, feeding period spectrum certificates rather than the T0–T8 forcing steps directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.