integrationGap
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.