dimensionGap
plain-language theorem explainer
Defines the dimension-gap polynomial gap(d) = d²(d+2) on natural numbers. At the forced spatial dimension d = 3 this is 45, the integer that later appears as half the imported fermionic DOF count and as the offset in η_B rung arithmetic. Anyone citing the D-flavored re-expression of g_* or the gap-from-dimension route to the −44 rung uses this abbreviation. The body is a one-line arithmetic definition.
Claim. For each natural number $d$, the dimension gap is the natural number $\mathrm{gap}(d) := d^{2}(d+2)$. In particular, at the forced spatial dimension $D = 3$ one has $\mathrm{gap}(3) = 9 \cdot 5 = 45$.
background
This module sits in the Unification layer and, after the 2026-06-25 rescope, only proves arithmetic identities that relate imported Standard Model degree-of-freedom counts to combinatorial quantities built from $D = 3$. It does not derive the SM spectrum. Upstream RS results used as fixed inputs are $D = 3$ (T8 / DimensionForcing), the eight-tick period $2^{D} = 8$, and the generation count 3.
The local constant $D$ is defined as $3$. The same polynomial appears upstream in Foundation.GapDerivation as the product of a parity count and a configuration dimension, documented there as "(parity count) × (coherence exponent) = $D^{2}(D+2)$". This module re-exports the closed form $d^{2}(d+2)$ for use in fermion-DOF and cosmology identities.
Sibling facts in the file include dimensionGap_at_D3 (evaluating to 45), positivity, and the identity that the imported fermionic DOF count equals $2 \times \mathrm{gap}(3)$.
proof idea
Pure definition: the body is the term $d^{2} \cdot (d+2)$ with no proof obligations. Downstream lemmas unfold this abbreviation and discharge equalities by rfl, decide, or ring. The upstream GapDerivation form factors the same polynomial as parityCount × configDim; the two definitions agree on values but this bridge file uses the expanded monomial.
why it matters
The integer 45 is the shared kernel of several routes in Cosmology.EtaBExactRungDerivation. Route A sets the η_B rung from dimension to $1 - \mathrm{gap}(D)$ (hence −44 at $D = 3$). The complementarity identity derived_rung_sum is exactly $(1 - \mathrm{gap}(D)) + \mathrm{gap}(D) = 1$. Chirality × torsion is proved equal to $\mathrm{gap}(D) - A$, both sides 44 at $D = 3$. Counterfactuals at $D \in {1,2,5}$ show the rung would be −2, −15, −174, so only $D = 3$ is non-degenerate for this assignment.
In the fermion-DOF bridge itself, the proved arithmetic is $90 = 2 \times \mathrm{gap}(3)$ and the assembled $g_*$ identity $28 + (7/8)\cdot 90 = 106.75$. Per the module docstring these are machine-checked re-expressions of already-known counts, not an RS derivation of the gauge content. The landmark link is T8 ($D = 3$); the eight-tick $2^{3}$ enters the companion Fermi–Dirac weight $(2^{D}-1)/2^{D}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.