eightTick
plain-language theorem explainer
Defines the eight-tick period as 2^D with D the forced spatial dimension, so the natural number is 8. It is the fundamental cadence of the recognition operator and the combinatorial period of the D-cube. Downstream fermion/boson tick counts and the 7/8 Fermi–Dirac weight identities cite it. The body is a one-line definitional abbreviation of the power of two.
Claim. Let $D=3$ be the spatial dimension forced by the dimension-forcing chain. The eight-tick period is the natural number $2^D$ (hence equal to $8$).
background
This module records exact arithmetic identities that re-express Standard Model degree-of-freedom counts in $D=3$ combinatorial notation. It does not derive the SM spectrum: gauge representations, neutrino conventions, and the thermal Fermi/Bose integrals are imported; what is RS-derived upstream is $D=3$ (T8 / DimensionForcing), the eight-tick period $2^D=8$ (T7 / EightTick), and the generation count 3.
Locally, $D$ is the constant natural number 3 ("spatial dimension forced by T8"). The eight-tick period is the vertex count of the $D$-cube and the fundamental cadence of the recognition operator $\hat R$. Sibling and upstream copies of $D$ in AlphaDerivation and GapDerivation carry the same forced value 3, sometimes glossed as linking or configuration dimension.
The Fermi–Dirac weight side of the bridge is the imported ratio $7/8$, rewritten here as $(2^D-1)/2^D$ once the period is named.
proof idea
Definitional, not a proof: eightTick is the abbreviation $2^D$ with the in-module constant $D:=3$. No tactics or lemmas fire at the definition site. The immediate companion theorem eightTick_eq discharges eightTick = 8 by native_decide after unfolding.
why it matters
Names the T7 eight-tick octave inside the fermion DOF bridge so later identities can speak in ticks rather than bare powers of two. Downstream, bosons get all eightTick ticks and fermions get eightTick - 1; fermion_missing_identity_tick packages that exclusion, and fermi_dirac_from_eight_tick equates the $D$-flavored weight $(2^D-1)/2^D$ to the tick fraction (eightTick-1)/eightTick (bookkeeping once eightTick := 2^D). Together with fermi_dirac_weight_D3 ($=7/8$) this feeds the assembled $g_\star$ arithmetic $28+(7/8)\times 90=106.75$.
Framework landmark: T7 forces period $2^3=8$; T8 forces $D=3$. The module status note is explicit that these are kernel-checked re-expressions, not a first-principles derivation of $g_\star$ from RS premises alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.