dimensionGap
plain-language theorem explainer
The dimension gap at spatial dimension d is the product of the ledger parity count d² and the configuration dimension d+2, hence d²(d+2). At the forced value d=3 this is the integer 45 that seeds the gap-45 / E_coh = φ^{-5} story. Cosmology and rung-derivation authors cite it as the pure arithmetic source of the −44 η_B rung. The body is a one-line product of two sibling defs.
Claim. For any natural number $d$, the dimension gap is $\mathrm{gap}(d) := d^{2}(d+2)$, the product of the number of independent ledger parities $d^{2}$ and the configuration dimension $d+2$ of a recognition event.
background
Module GapDerivation closes boundary item B-22: the coherence energy exponent equals the configuration dimension of a recognition event. A recognition event carries $D$ spatial degrees of freedom (forced by T8), one temporal tick advance (T2), and one balance degree of freedom from ledger neutrality $J(x)=J(x^{-1})$ (T3), so the configuration dimension is $D+2$. Coherence energy is $\varphi^{-1}$ per degree of freedom, hence $E_{\mathrm{coh}}=\varphi^{-(D+2)}$; at $D=3$ this is $\varphi^{-5}$, matching Constants.E_coh.
The two factors are defined in-module: parityCount d := d^2 (independent ledger parities; at $D=3$ the linear count $3D$ coincides with $D^2$) and configDim d := d+2. Their product is the dimension gap $D^2(D+2)$. The module also records that $\gcd(2^D,D^2(D+2))=1$ for odd $D$ and fails for even $D\ge 2$, giving a fourth parity argument that $D$ is odd before Alexander duality pins $D=3$.
proof idea
Pure definitional abbreviation: unfold the two sibling defs and multiply. parityCount d is $d^2$ and configDim d is $d+2$, so the body is literally parityCount d * configDim d. No lemmas, tactics, or hypotheses.
why it matters
This is the arithmetic kernel of gap-45. Downstream, gap_at_D3 specializes it to $9\times 5=45$, and the cosmology module EtaBExactRungDerivation builds the η_B rung as $1 - \mathrm{gap}(D)$ (equivalently $-44$ at $D=3$). Route A of EtaBExactRungCert is exactly that specialization; chirality_product_equals_gap_minus_one equates the Gray-code × torsion product to $\mathrm{gap}(D)-A=44$; derived_rung_sum is the complementarity identity $(1-\mathrm{gap})+\mathrm{gap}=1$. Counterfactuals at $D=1,2,5$ show the rung would be $-2,-15,-174$ respectively, so only $D=3$ is non-degenerate. Framework landmarks: T8 forces $D=3$, T2/T3 supply the $+2$ in the configuration dimension, and the resulting $\varphi^{-5}$ is the RS-native $\hbar$ scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.