pith. sign in
theorem

integrationGap_factors

proved
show as:
module
IndisputableMonolith.Foundation.IntegrationGap
domain
Foundation
line
59 · github
papers citing
1 paper (below)

plain-language theorem explainer

The integration gap at the forced spatial dimension equals 45. Researchers closing the combinatorial side of dimension selection in Recognition Science cite this when they need the explicit integer value of D squared times (D plus 2) at D equals 3. The proof is a direct computational reduction that evaluates the product of parity count and configuration dimension at the concrete value of D.

Claim. At the forced spatial dimension $D=3$, the integration gap $D^2(D+2)$ equals $9 times 5$.

background

The integration gap is the product of parity count and configuration dimension for a spatial dimension d. Parity count at d equals d squared while configuration dimension equals d plus 2, yielding the integer d squared times (d plus 2). The module records that this integer is coprime to 2 to the power d exactly when d is odd, and it specializes the value at d equals 3 to 45. This supplies the concrete number required by the linking argument in Foundation.DimensionForcing that selects D equals 3 among odd candidates consistent with an orderly recognition cycle.

proof idea

The proof is a one-line wrapper that applies native_decide to evaluate the definitions of parityCount and configDim at the concrete value D equals 3.

why it matters

This pins the numerical value 45 of the integration gap at the dimension selected by the linking argument in Foundation.DimensionForcing. It completes the specialization needed for the coprimality claim in the same module, which restricts possible dimensions to D equals 3 among the odd candidates. Within the T0-T8 forcing chain it supplies the concrete integer that appears in the eight-tick octave structure at D equals 3.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.

papers checked against this theorem (showing 1 of 1)