pith. machine review for the scientific record. sign in
def definition def or abbrev high

integrationGap

show as:
view Lean formalization →

The integration gap is defined as the product of the parity count (dimension squared) and the configuration dimension (dimension plus two). Researchers deriving exact baryon asymmetry rung values in the cosmology module cite this quantity when fixing the scale at dimension three, where the gap equals forty five. The definition is a direct algebraic product of the two component functions.

claimFor a natural number $d$, the integration gap is $d^2(d + 2)$.

background

The Integration Gap module introduces the integration gap as the integer $D^2(D + 2)$, which equals forty five at $D = 3$. The parity count is defined as the square of the dimension and counts the number of independent ledger parities. The configuration dimension is defined as the dimension plus two, incorporating the spatial degrees of freedom together with one temporal and one ledger balance term. The module also records the coprimality fact that the gap is coprime to $2^D$ precisely when $D$ is odd, which combines with the dimension selection argument in Foundation.DimensionForcing.

proof idea

This is a one-line definition that multiplies the result of parityCount d by the result of configDim d.

why it matters in Recognition Science

The definition supplies the integration gap value subtracted in eta_B_rung_from_dimension and witnessed in EtaBExactRungCert at dimension three. It anchors the numerical computations of chirality products and fermionic degrees of freedom in the EtaBExactRungDerivation module. The gap of forty five at the forced dimension three closes a combinatorial step that supports the eight-tick octave and the exact rung derivations in the Recognition Science framework.

scope and limits

formal statement (Lean)

  51def integrationGap (d : ℕ) : ℕ := parityCount d * configDim d

proof body

Definition body.

  52

used by (16)

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

depends on (4)

Lean names referenced from this declaration's body.