integrationGap_at_D3
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not derive the value of D itself.
- Does not compute the gap for any dimension other than 3.
- Does not prove coprimality for general D.
- Does not connect the integer 45 to physical measurements.
Lean usage
have hgap : (integrationGap D : ℤ) = 45 := by exact_mod_cast integrationGap_at_D3formal statement (Lean)
57theorem integrationGap_at_D3 : integrationGap D = 45 := by native_decide
proof body
58