BottPeriodicity
plain-language theorem explainer
Packages two elementary arithmetic facts that underwrite Bott period 8 for real Clifford algebras: the rank identity 2^{n+8}=2^n·2^8, and the statement that every positive residue below 8 is a nonzero class mod 8. Cited by the complete 8-tick–Clifford bridge and by the T8-to-canonical-spinor certificate. Existence is witnessed by a trivial instance using only power and modular arithmetic.
Claim. A Bott-periodicity witness is a pair of statements: (i) for every natural number $n$, $2^{n+8}=2^n\cdot 2^8$; (ii) for every $k$ with $0<k<8$, one has $k\bmod 8=k$, $k\neq 0$, and $k\neq 8$. Together these encode the rank jump and the minimality of period 8 behind $\mathrm{Cl}_{n+8}(\mathbb{R})\cong\mathrm{Cl}_n(\mathbb{R})\otimes M_{16}(\mathbb{R})$.
background
The module CliffordBridge links Recognition Science's eight-tick octave to classical Clifford algebra theory. Real Clifford algebras satisfy Bott periodicity of period 8: $\mathrm{Cl}{n+8}(\mathbb{R})\cong\mathrm{Cl}n(\mathbb{R})\otimes M{16}(\mathbb{R})$, equivalently $\mathrm{Cl}{n+8}\cong\mathrm{Cl}_n\otimes\mathrm{Cl}_8$ since $\mathrm{Cl}8(\mathbb{R})\cong M{16}(\mathbb{R})$. The module also records the DFT–Clifford grading correspondence and the $D=3$ spinor isomorphisms $\mathrm{Cl}_3\cong M_2(\mathbb{C})$ and $\mathrm{Spin}(3)\cong\mathrm{SU}(2)$.
In RS-native units the fundamental time quantum is one tick ($\tau_0=1$), and one octave is eight ticks. The forcing chain's T7 step already isolates this eight-tick period; the present structure isolates the two pure-arithmetic ingredients (rank doubling by $2^8=256$ and minimality of residues mod 8) that any Clifford-period argument must use. Full algebraic classification of Clifford modules is deferred; only the rank and residue skeleton is packaged here.
proof idea
This declaration is a structure (a Prop-carrying record type), not a proved theorem. It names the two fields that a Bott-periodicity witness must supply. The companion definition bottPeriodicity fills both fields in one line each: rank_period_identity by rewriting with pow_add, and period_minimal_residue by Nat.mod_eq_of_lt, Nat.ne_of_gt, and Nat.ne_of_lt. No Clifford-algebra machinery is invoked at this layer.
why it matters
Bott period 8 is the classical reason the RS eight-tick octave is forced rather than chosen. The structure is the first field of Complete8TickCliffordBridge, which bundles Bott periodicity with the DFT–Clifford mode map and the $\mathrm{Cl}_3$ spinor data. Downstream, T8_To_CanonicalSpinor_Bridge in the unified forcing chain cites it explicitly: at $D=3$ (T8) one obtains $\mathrm{Cl}_3\cong M_2(\mathbb{C})$, spinor dimension $2$, Clifford dimension $2^3=8$, and the Bott period 8 linking back to the eight-tick DFT. The module doc ties the same period to KO-theory period 8 and the division-algebra tower $\mathbb{R},\mathbb{C},\mathbb{H},\mathbb{O}$. This declaration therefore sits at the T7/T8 interface: arithmetic skeleton for the claim that eight ticks are the Clifford period, not an ad-hoc discretization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.