fermion_missing_identity_tick
plain-language theorem explainer
Available fermion ticks equal the eight-tick octave minus one reserved identity tick, i.e. 8 − 1. Anyone assembling the combinatorial 7/8 Fermi–Dirac re-expression in this module cites it. The proof is a pure definitional unfold followed by reflexivity.
Claim. The count of ticks available to fermions equals the eight-tick period minus the identity-tick count: $N^{\mathrm{f}}_{\mathrm{avail}} = 2^{3} - N_{\mathrm{id}}$. With the standard assignments this is $8 - 1$.
background
This module records exact arithmetic identities that relate imported Standard Model degree-of-freedom counts to D = 3 combinatorial quantities. It does not derive the SM spectrum. Upstream RS results used as fixed inputs are D = 3 (T8 / DimensionForcing), the eight-tick octave period $2^{D} = 8$ (T7 / EightTick), and the generation count 3.
The eight-tick period is the fundamental evolution window in RS-native units (one tick $\tau_0 = 1$). The identity tick is the single reserved slot that is not available to fermionic posting; subtracting it leaves seven active slots. The Fermi–Dirac thermal weight $7/8$ is imported from the standard spin-statistics integral; only the combinatorial rewrite $(2^{D}-1)/2^{D}$ is checked here.
Sibling definitions in the same file fix eightTick = 8, the dimension gap at D = 3, and the per-generation and total fermionic DOF counts that later assemble into $g_* = 106.75$.
proof idea
One-line definitional proof. Unfold the two named constants available_ticks_fermion and identity_tick_count on either side of the equality; both sides reduce to the same closed numeral expression in eightTick, so rfl closes the goal. No lemmas are applied.
why it matters
This identity is the numerator step behind the module's central numerical coincidence $(8-1)/8 = 7/8$, which the file header explicitly treats as a re-expression of already-known counts rather than an RS derivation of the thermal weight. It sits on the T7 eight-tick octave and T8 D = 3 landmarks: once the period is $2^{3}$, removing one identity slot forces the factor seven that matches the imported Fermi–Dirac weight.
No downstream theorems currently depend on it (used_by is empty); its role is local bookkeeping inside the FermionDOFGapBridge arithmetic chain that also records $90 = 2 \times$ dimensionGap(3) and $28 + (7/8)\times 90 = 106.75$. The module status note (post Thapa review) stresses that closing a true RS derivation of $g_*$ would still require deriving gauge representations, the Higgs doublet, chiral neutrinos, and the thermal integral from RS premises—none of which is claimed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.