bottPeriodicity
plain-language theorem explainer
A concrete Bott-periodicity witness: the rank identity $2^{n+8}=2^n\cdot 2^8$ holds for all $n$, and every positive $k<8$ is a nonzero non-period residue mod 8. Anyone wiring the 8-tick Clifford bridge or the T8 spinor step cites this instance. Proof is a two-field structure fill-in via pow_add and elementary Nat modular arithmetic.
Claim. There is a Bott periodicity witness consisting of (i) the rank identity $2^{n+8} = 2^n \cdot 2^8$ for every $n \in \mathbb{N}$, and (ii) the minimality fact that every integer $k$ with $0 < k < 8$ satisfies $k \bmod 8 = k$, $k \neq 0$, and $k \neq 8$.
background
The CliffordBridge module links Recognition Science's eight-tick octave to classical Bott periodicity of real Clifford algebras: $\mathrm{Cl}_{n+8}(\mathbb{R}) \cong \mathrm{Cl}n(\mathbb{R}) \otimes M{16}(\mathbb{R})$, with $\mathrm{Cl}8(\mathbb{R}) \cong M{16}(\mathbb{R})$. The module frames the 8-tick DFT grading as the algebraic period that forces the RS evolution cycle.
The structure being inhabited packages two lightweight arithmetic stand-ins for that period-8 claim. The rank identity records that the dimension of the exterior algebra (or spinor space) multiplies by $2^8$ under $n \mapsto n+8$. The residue clause says no positive proper sub-tick is a full period: every $0<k<8$ is its own residue class mod 8 and is neither zero nor the period itself. Upstream, the RS tick $\tau_0=1$ and the eight-tick octave supply the physical period being matched; the structure statement itself notes that a full Clifford-isomorphism proof is deferred.
proof idea
Two short field proofs. For the rank identity, rewrite $2^{n+8}$ by pow_add to obtain $2^n \cdot 2^8$. For minimality, given $k<8$ and $k>0$, package the triple Nat.mod_eq_of_lt, Nat.ne_of_gt, and Nat.ne_of_lt to get $k\bmod 8=k$, $k\neq 0$, and $k\neq 8$. No Clifford algebra API is invoked; the witness is pure Nat arithmetic matching the structure's stated skeleton.
why it matters
This instance is the Bott field of complete8TickCliffordBridge, the packaged 8-tick $\leftrightarrow$ Clifford bridge (Bott witness, DFT bridge, $\mathrm{Cl}_3\cong M_2(\mathbb{C})$, $\mathrm{Spin}(3)\cong\mathrm{SU}(2)$, and $D=3$ spinor uniqueness). Downstream, the UnifiedForcingChain theorem t8_to_canonical_spinor_bridge_holds uses the bridge under T8 (spatial dimension forced to 3), so this definition is the arithmetic anchor that the eight-tick octave (primer T7) and $D=3$ (primer T8) share with classical Bott period 8.
It replaces an older existential placeholder (∃ _n, True) with an explicit period-8 API. The full $\mathrm{Cl}_{n+8}\cong\mathrm{Cl}n\otimes M{16}$ isomorphism remains outside the structure; only the rank and minimality skeleton are certified here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.