integrationGapCert
plain-language theorem explainer
The integration gap certificate at dimension three verifies that D squared times (D plus two) equals forty-five, with coprimality to powers of two holding precisely when D is odd. Researchers modeling recognition cycles cite this to confirm the combinatorial prerequisites for the phi-power balance identity at the forced dimension. The proof is a direct term-mode record construction that assembles the native-decide evaluations for each structural field.
Claim. At $D=3$ the integration gap $D^2(D+2)$ equals 45, the configuration dimension equals 5, the parity count equals 9, the gap minus one equals 44, and $2^D$ is coprime to the gap. For every natural number $k$ the product $(2k+1)^2(2k+3)$ is coprime to $2^{2k+1}$, while for every $k>0$ the product $(2k)^2(2k+2)$ shares a common factor with $2^{2k}$.
background
The module treats the integration gap as the integer $D^2(D+2)$, which equals 45 at $D=3$. This quantity enters the phi-power balance identity via the relation phi to the power of (A minus gap) times phi to the power of gap equals phi, with the gap minus one fixed at 44. The local setting is the combinatorial analysis that accompanies dimension forcing: the recognition period $2^D$ must remain coprime to the gap so that recognition cycles stay orderly. The module doc states that gcd of $2^D$ and the gap equals 1 if and only if D is odd, thereby restricting admissible dimensions once the linking argument selects D=3 among odd candidates.
proof idea
The proof is a term-mode construction of the IntegrationGapCert record. It supplies each field by direct reference to the specialized theorems configDim_at_D3, parityCount_at_D3, integrationGap_at_D3, gapMinusOne_at_D3, coprime_at_D3, coprimality_odd, and coprimality_even_fails. No further rewriting or induction is performed; the record syntax itself discharges the structure.
why it matters
This certificate consolidates the dimension-specific facts required to invoke the gap balance identity inside the phi-ladder. It supports the restriction to D=3 among odd dimensions through the coprimality condition and thereby feeds the dimension-forcing argument in Foundation.DimensionForcing. Within the Recognition Science framework it confirms the eight-tick octave and the selection of D=3 from T7 and T8, ensuring the integration gap of 45 satisfies the required phi-power identity without introducing common factors with the recognition period.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.