eightTick_eq
plain-language theorem explainer
The eight-tick combinatorial period equals 8 as a natural number. Unification and thermal-weight identities that rewrite Fermi–Dirac factors in tick language cite this equality. The proof is a one-line native evaluation of the concrete definition (period 2^D at D = 3).
Claim. The eight-tick period equals $8$: if the tick count is $2^D$ with spatial dimension $D = 3$, then that count is exactly $8$.
background
This module records kernel-checked arithmetic identities that relate imported Standard Model degree-of-freedom counts to D = 3 combinatorial quantities. It does not derive the SM spectrum; it only re-expresses known counts in D-flavored notation.
Upstream, spatial dimension is fixed at D = 3 (T8 / DimensionForcing; also AlphaDerivation and GapDerivation). The Recognition eight-tick octave is the hypercube period 2^D (T7), so at D = 3 one expects period 8. The local definition eightTick packages that period; the dimension-gap side of the same file uses dimensionGap(d) = D²(D+2), which equals 45 at D = 3.
The Fermi–Dirac thermal weight 7/8 is the standard integral ratio (imported), rewritten here as (2^D − 1)/2^D once the tick count is identified with 2^D.
proof idea
Term-mode proof by native_decide. The definition of the eight-tick period is a closed natural-number expression in the forced D = 3 (equivalently 2^3), so the kernel evaluates both sides and discharges equality by computation. No lemmas are invoked.
why it matters
Feeds fermi_dirac_from_eight_tick, which states the bookkeeping identity fermi_dirac_weight_D(D) = (eightTick − 1)/eightTick at D = 3. That parent rewrites the imported 7/8 Fermi–Dirac weight as (2^D − 1)/2^D once eightTick is known to be 8, then assembles into the larger g_star arithmetic (28 + (7/8)×90 = 106.75) proved elsewhere in the module.
In the forcing chain this is the numerical shadow of T7 (eight-tick octave, period 2^3) together with T8 (D = 3). The module status note is explicit: the identity is exact and machine-checked, but a re-expression after the target number is known is not an RS derivation of the SM DOF content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.