orbitPow_zero
plain-language theorem explainer
Orbit exponentiation sends the zero orbit exponent to the multiplicative unit, for every base in the distinction naturals. Anyone building period-spectrum certificates or divisor-to-factorization maps needs this base case. The proof is pure definitional equality (rfl) against the recursive clause of orbit power.
Claim. For every distinction-natural $a$, the $\delta$-native orbit power satisfies $a^{0} = 1$, where $0$ and $1$ are the zero and unit of the distinction-natural monoid.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction: an inductive type with constructors zero and succ, playing the role of a Peano carrier stripped of any preferred radix. It is the K2.12 object used wherever Recognition calculus needs a pure counting orbit rather than a numeral system.
Orbit power is the $\delta$-native exponentiation map on that carrier. By definition it returns the multiplicative unit at the zero exponent and multiplies by the base on successors: $a^{0} := 1$ and $a^{k+1} := a^{k}\cdot a$. The surrounding module develops the period spectrum of such powers, linking proper divisors of periods to nontrivial factorizations in the unit group of the recognition monoid.
The local setting is the factorization layer of Primitive Recognition Calculus: periods of orbit powers are the raw data from which spectrum certificates and nontrivial factorizations are extracted.
proof idea
One-line definitional proof. The recursive equation for orbit power has the clause orbitPow a zero = one by construction, so rfl closes the goal immediately. No lemmas are invoked.
why it matters
This is the zero-exponent base case for the orbit-power recursion used throughout the PeriodSpectrum development. Sibling results (successor step, conversion to ordinary naturals, unit-residue reduction, PeriodWitness, and the divisor-to-nontrivial-factorization map) all rest on a well-defined power map; without $a^{0}=1$ the inductive scaffolding for period divisors collapses.
In the broader Recognition chain, period structure on distinction orbits feeds the eight-tick octave story (T7): discrete periods of the recognition monoid are the combinatorial substrate from which the $2^{3}$ tick and the spatial dimension count are later forced. The declaration itself is elementary bookkeeping, but it anchors every later certificate that reads off a period from an orbit power.
No downstream consumers are recorded yet in the dependency graph; the lemma is infrastructure for the spectrum certificate and factorization theorems in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.