integrationGap_at_D3
plain-language theorem explainer
The declaration fixes the integration gap at 45 when the spatial dimension equals 3. Cosmology and foundation modules cite it to close rung derivations and phi-power identities. The proof is a one-line native_decide that evaluates the product of parity count and configuration dimension at the concrete value D=3.
Claim. For spatial dimension $D=3$, the integration gap defined by parity count times configuration dimension equals 45.
background
The integration gap is the product parityCount d * configDim d. At D=3 the parity count is D squared (9) and the configuration dimension is D+2 (5), so the product is 45. The module also records that gcd(2^D, D^2(D+2))=1 precisely when D is odd, restricting possible dimensions once 2^D is taken as the recognition period. D itself is the spatial dimension forced by linking in Foundation.DimensionForcing. Upstream the definition integrationGap d := parityCount d * configDim d supplies the combinatorial quantity used throughout the framework.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic. After integrationGap unfolds to parityCount D * configDim D and D is substituted by its definition 3, the arithmetic 9*5 reduces directly to 45.
why it matters
This anchors downstream results in EtaBExactRungDerivation: chirality_product_equals_gap_minus_one (4*11=44), eta_B_rung_from_dimension_at_D3 (-44), fermionicDOF_eq (90), and fermionic_half_equals_gap. It also supplies the concrete value for gap_balance, which rewrites phi^(-44)*phi^45=phi. Within the Recognition Science chain it confirms the combinatorial value at the dimension forced by T8 and supplies the integer needed for the phi-ladder mass formula and alpha-band constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.