orbitPow_succ
plain-language theorem explainer
Successor step for δ-native powering on DistinctionNat: raising a to the successor of k equals the product of a^k with a. Anyone inducting on orbit exponents or relating orbitPow to ordinary Nat powers cites this. The proof is pure definitional unfolding (rfl) of the recursive clause of orbitPow.
Claim. For any distinction-orbit naturals $a$ and $k$, the orbit power satisfies $a^{\mathrm{succ}(k)} = a^{k} \cdot a$, where successor is one further application of the distinction generator and multiplication is the monoid product on distinction naturals.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction: an inductive type with constructors zero and succ, standing in for a Peano-style counter built only from recognition steps (K2.12). Successor on this type is one more application of the generator, matching the ArithmeticFromLogic reading of succ as .step.
In the PeriodSpectrum factorization layer, orbitPow is δ-native exponentiation by an orbit exponent: it sends the zero exponent to the monoid unit one, and on succ k multiplies the previous power by the base a. This is the native powering used when periods and prime-coordinate transforms are expressed without leaving the distinction calculus.
The local module develops the period spectrum of factorization witnesses on these orbit naturals. The successor identity is the recursive hinge that lets induction on the exponent transfer statements about orbitPow to ordinary Nat exponentiation and divisibility.
proof idea
One-line definitional proof. The goal is exactly the succ clause in the recursive definition of orbitPow, so rfl closes it with no lemmas or rewriting. No case split or induction is required at this site; those appear only in consumers that induct on the exponent.
why it matters
This is the successor hinge for every induction on orbit exponents in the factorization stack. Downstream, orbitPow_toNat uses it (via the succ inductive case) to prove that the Nat image of orbitPow is ordinary exponentiation: $(a^k).\mathrm{toNat} = a.\mathrm{toNat}^{k.\mathrm{toNat}}$. The prime-coordinate transform theorem base_divides_orbitPow_of_exponent_nonzero likewise cases on the exponent and needs the succ multiplication form to show a nonzero power of p is divisible by p.
In the broader Recognition foundation, period spectrum and prime-coordinate work sit under PrimitiveRecognitionCalculus factorization: they turn orbit structure into arithmetic factorization data that later feeds forcing and spectrum arguments. The lemma itself is pure scaffolding algebra, not a T0–T8 forcing step, but without it the bridge from δ-native powers to Nat powers and divisibility does not open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.