available_ticks_fermion
plain-language theorem explainer
Defines the fermion-available tick count as one less than the eight-tick period: 2^D − 1. At D = 3 this is 7, the numerator of the standard Fermi–Dirac thermal weight 7/8. Downstream arithmetic identities cite it to equate the combinatorial tick fraction (8−1)/8 with the imported fermionic weight, without deriving that weight from first principles.
Claim. The number of fermion-available ticks is $2^D - 1$, i.e. the eight-tick period minus one (the identity tick excluded by the gloss).
background
This module records exact arithmetic identities that re-express Standard Model degree-of-freedom counts in D-flavored notation. Per the module status note, the SM representations, the minimal-neutrino convention $g_f = 90$, and the Fermi–Dirac integral giving the $7/8$ weight are imported physics; only the numerical identities are proved here.
Upstream, $D = 3$ is forced (T8 / DimensionForcing) and the fundamental cadence of the recognition operator is the eight-tick period $2^D = 8$ (EightTick). The local definition eightTick is exactly that power: $2^D$. The present quantity subtracts one tick, matching the gloss that fermions are excluded from the identity tick of the octave.
The companion weight identity written in the module is $\mathrm{fermi_dirac_weight} = (2^D - 1)/2^D$, which at $D = 3$ is the familiar $7/8$.
proof idea
One-line definitional abbreviation: unfold to eightTick - 1, and eightTick itself is 2 ^ D. No tactics, lemmas, or proof obligations; the kernel reduces the expression by unfolding.
why it matters
Feeds two local theorems that close the §7 gloss of the fermion DOF bridge. fermion_missing_identity_tick records that this count equals the eight-tick period minus the identity-tick count (both sides reduce to 7). fermi_weight_is_tick_fraction then shows the rational equality $(2^D-1)/2^D$ equals the imported Fermi–Dirac weight at $D$, by norm_num after unfolding.
In the Recognition framework this sits under the eight-tick octave (T7) and $D = 3$ (T8): the combinatorial fraction $(8-1)/8$ is the RS-side re-expression of the thermal weight that enters $g_\star = 28 + (7/8)\times 90 = 106.75$. The module is explicit that this is a numerical coincidence recorded after the target is known, not a derivation of spin-statistics thermal integrals or the SM spectrum from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.