pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.Foundation.IntegrationGap

show as:
view Lean formalization →

The IntegrationGap module supplies the dimension-forcing infrastructure that pins spatial dimension to three via the integration gap. Cosmologists deriving the baryon asymmetry η_B cite it for the three combinatorial witnesses that all reduce to integrationGap D − 1 = 44 at D = 3. The module consists of definitions for D, configDim, parityCount, integrationGap and supporting coprimality lemmas that evaluate the gap at the forced dimension.

claimLet $D$ denote spatial dimension. Define configDim$(D)$, parityCount$(D)$, and integrationGap$(D) = 1 - D^2(D+2)$. Then gapMinusOne$(D) = -1 + D^2(D+2)$, with integrationGap$(3) = -44$ and gapMinusOne$(3) = 44$. Coprimality holds for the odd case at $D=3$.

background

The module resides in the Foundation layer and imports only the RS time quantum τ₀ = 1 tick from Constants. Its doc-comment states that it concerns the spatial dimension forced by linking, referencing the DimensionForcing surface. It introduces D as the forced dimension, configDim and parityCount as auxiliary counts, integrationGap as the explicit defect 1 − D²(D+2), and gapMinusOne as its positive counterpart at D = 3. Coprimality lemmas (odd and even cases) are included to support the combinatorial witnesses.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the integrationGap infrastructure required by the master forcing-chain theorem in the root IndisputableMonolith and by the two η_B worked-example modules. EtaBExactRungDerivation uses it to realize the rung integer −44 via the gap-from-dimension witness 1 − D²(D+2) at D = 3. EtaBPrefactorDerivation uses the same gap to fix the algebraic content of the prefactor. It thereby closes the T8 step that forces D = 3 in the unified forcing chain.

scope and limits

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (18)