fermi_dirac_weight_D3
plain-language theorem explainer
At spatial dimension D = 3 the combinatorial Fermi–Dirac weight (2^D − 1)/2^D equals exactly 7/8. Cosmologists and RS auditors cite it when assembling the high-T effective relativistic DOF count g_*. The proof is a two-step unfold of the weight definition and of D, discharged by exact rational arithmetic.
Claim. With spatial dimension fixed at $D = 3$, the weight $(2^D - 1)/2^D$ equals $7/8$ exactly.
background
This module records kernel-checked arithmetic identities that re-express imported Standard Model degree-of-freedom counts in D-flavored notation. It does not derive the SM spectrum, the Fermi–Dirac thermal integral, or the high-T value g_* = 106.75; those are imported physics. What is RS-derived upstream is D = 3 (T8 / DimensionForcing) and the eight-tick period 2^D = 8.
Locally, D is the constant natural number 3, and eightTick is defined as 2^D. The weight fermi_dirac_weight_D d is the rational expression (2^d − 1)/2^d: the standard fermionic thermal factor written as a pure function of dimension. The module status note is explicit that the 7/8 factor itself comes from the usual Fermi/Bose integral ratio, not from spin-statistics sign theorems elsewhere in the repo.
The honest split is therefore: RS supplies D = 3 and the 8-tick cadence; the SM supplies the matter content and the thermal weight convention; this file only checks that the numbers line up under exact arithmetic.
proof idea
Term-mode proof in two unfolds. First unfold the weight definition fermi_dirac_weight_D, which is the map d ↦ (2^d − 1)/2^d as a real. Then unfold the constant D to the literal 3. The goal becomes (2^3 − 1)/2^3 = 7/8, which norm_num closes by exact rational computation. No external lemmas are required beyond the local definitions.
why it matters
This is the D = 3 specialization of the weight identity that feeds three downstream results in the same module. fermi_dirac_from_eight_tick rewrites the same 7/8 as (eightTick − 1)/eightTick, pure bookkeeping once eightTick := 2^D. g_star_D3_eq assembles the imported identity 28 + (7/8)×90 = 106.75. The certificate fermion_dof_gap_certificate packages both with the dimension-gap arithmetic (dimensionGap(3) = 45, fermionic_dof = 90) into a single conjunction.
In the broader RS chain this sits under T8 (D = 3) and the eight-tick octave (period 2^3), but only as notation: the module itself warns that matching 7/8 after the target is known is not a derivation of the Fermi–Dirac factor from RS premises. The open gap remains deriving gauge representations, Higgs content, and the thermal integral from first principles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.