module module moderate

`IndisputableMonolith.Cosmology.EtaBExactRungDerivation`

The module derives the exact rung for η_B in Recognition Science cosmology along three paths. Dimension at D=3, chirality via Gray code flips on the 3-cube, and fermionic degrees of freedom all yield the same rung. Equality lemmas confirm the routes agree. The work uses the integration gap of 45 at D=3.

claimDerivations of the exact rung for the baryon asymmetry parameter $η_B$ at spatial dimension $D=3$, obtained from the integration gap, from the Gray code chirality flip count on the 3-cube, and from the count of fermionic degrees of freedom, together with proofs that the three values coincide.

background

This module operates within the cosmology sector of the Recognition Science framework. It imports the base time quantum $τ_0 = 1$ tick and the integration gap $D^2(D+2)$ which evaluates to 45 when $D=3$. The module introduces the Gray code chirality flip count on the 3-cube for axis 0, equal to four on the canonical cycle [0,1,3,2,6,7,5,4]. It then constructs separate derivations of the $η_B$ rung from dimension, from chirality, and from fermionic DOF.

proof idea

The module is built from a sequence of definitions and equality theorems. The dimension route applies the integration gap directly at D=3. The chirality route counts bit flips in the Gray code cycle. The fermionic route uses the fermionicDOF count. Agreement is established by explicit equality lemmas such as witnesses_AB_agree and witnesses_AC_agree. No single master theorem; rather a set of cross-checks.

why it matters in Recognition Science

This module supplies one of the two $η_B$ worked-example modules referenced in the companion paper. It is imported by the root IndisputableMonolith module, which assembles the master forcing-chain theorem and the T0-T8 landmarks. The derivations illustrate how the framework fixes cosmological parameters from the D=3 requirement and the phi-ladder structure.

scope and limits

Does not compute the numerical value of $η_B$.
Does not model the dynamical generation of the asymmetry.
Does not extend beyond the three listed derivation routes.
Does not address higher-dimensional or non-integer D cases.

used by (1)

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

IndisputableMonolith module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.IntegrationGap module_import

declarations in this module (20)

def bitFlipCount0 L43
def torsionGap01 L47
def fermionicDOF L50
theorem fermionicDOF_eq L52
def eta_B_rung_from_dimension L59
theorem eta_B_rung_from_dimension_at_D3 L62
def eta_B_rung_from_chirality L69
theorem eta_B_rung_from_chirality_eq L72
def eta_B_rung_from_fermionic L77
theorem eta_B_rung_from_fermionic_eq L80
theorem witnesses_AB_agree L88
theorem witnesses_AC_agree L93
theorem witnesses_BC_agree L98
theorem chirality_product_equals_gap_minus_one L106
theorem fermionic_half_equals_gap L115
theorem D1_counterfactual_rung L124
theorem D2_counterfactual_rung L128
theorem D5_counterfactual_rung L132
structure EtaBExactRungCert L138
theorem etaBExactRungCert L159