pith. machine review for the scientific record. sign in
theorem proved term proof high

integrationGapCert

show as:
view Lean formalization →

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.

claimAt $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 129theorem integrationGapCert : IntegrationGapCert where
 130  config_dim := configDim_at_D3

proof body

Term-mode proof.

 131  parity_count := parityCount_at_D3
 132  gap_value := integrationGap_at_D3
 133  gap_minus_one := gapMinusOne_at_D3
 134  coprime_at_3 := coprime_at_D3
 135  odd_coprime := coprimality_odd
 136  even_not_coprime := coprimality_even_fails
 137
 138end IntegrationGap
 139end Foundation
 140end IndisputableMonolith

depends on (8)

Lean names referenced from this declaration's body.