IndisputableMonolith.Foundation.IntegrationGap
The IntegrationGap module defines combinatorial quantities realizing the forced spatial dimension D=3 via the integration gap. Cosmologists deriving the baryon-to-photon ratio cite its D=3 specializations to obtain the rung integer -44. The module consists entirely of definitions and evaluations at D=3 with no theorems.
claimThe integration gap satisfies $I(D)-1=44$ at $D=3$, where the gap-from-dimension witness is $1-D^2(D+2)$ and parity and coprimality counts are evaluated at the same point.
background
The module imports the RS time quantum τ₀=1 tick from Constants. It introduces D as spatial dimension, configDim as configuration dimension, parityCount as the parity-state count, and integrationGap as the defect measure whose value at D=3 supplies the rung. Additional definitions cover gapMinusOne, integrationGap_factors, and coprimality checks that succeed only at D=3. The local setting is the forcing of D=3 by linking, cross-referenced to DimensionForcing.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the integrationGap infrastructure that feeds the master forcing-chain theorem in the root IndisputableMonolith module and the two η_B derivation modules. It realizes the three combinatorial witnesses for the -44 rung in the baryon-to-photon ratio, connecting directly to the T8 step that forces D=3.
scope and limits
- Does not prove the forcing of D=3; that resides in DimensionForcing.
- Does not derive physical constants or the η_B prefactor; those appear downstream.
- Does not evaluate the gap or parity counts for D other than 3.
- Does not contain any theorem statements or sorry placeholders.
used by (3)
depends on (1)
declarations in this module (18)
-
def
D -
def
configDim -
def
parityCount -
def
integrationGap -
theorem
configDim_at_D3 -
theorem
parityCount_at_D3 -
theorem
integrationGap_at_D3 -
theorem
integrationGap_factors -
theorem
coprimality_odd -
theorem
coprimality_even_fails -
theorem
coprime_at_D3 -
def
gapMinusOne -
theorem
gapMinusOne_at_D3 -
theorem
gapMinusOne_factor -
def
A -
theorem
gap_balance -
structure
IntegrationGapCert -
theorem
integrationGapCert