Pith. sign in
module module high

IndisputableMonolith.Cosmology.EtaBExactRungDerivation

show as:
view Lean formalization →

Derives the baryon-to-photon rung η_B = −44 by three independent structural routes: dimension gap, Gray-code chirality, and fermionic degrees of freedom. Shows the three routes agree exactly. Cosmologists and RS auditors cite it to pin η_B on the φ-ladder before interval certification. The argument is algebraic identity plus specialization at D = 3.

claimThe baryon asymmetry rung is obtained three ways: (A) from the dimension gap, $r_A(d) = 1 - d^2(d+2)$, so $r_A(3) = -44$; (B) from Gray-code chirality products; (C) from the fermionic DOF gap. The module proves $r_A = r_B = r_C = -44$ and the identity linking chirality product to gap-minus-one.

background

Recognition Science places the baryon-to-photon ratio $\eta_B$ on the $\varphi$-ladder. The companion module BaryonAsymmetryExact closes that $\eta_B$ sits at rung $-44$ with the balance $\eta_B \times \varphi^{45} = \varphi$. EtaBIntervalCert then certifies $\varphi^{-44} \in (5.5\times 10^{-10}, 7.5\times 10^{-10})$, containing the Planck 2018 value.

GapDerivation supplies the dimension-gap formula: the coherence exponent equals $D+2$ (configuration dimension of a recognition event), so at $D=3$ one recovers $E_{\mathrm{coh}}=\varphi^{-5}$ and the integer gap $d^2(d+2)=45$. GrayCodeChirality and CKMFromCube supply the chiral 3-bit Gray walk on $Q_3$ as the geometric source of CP violation; FermionDOFGapBridge ties the same integer to fermionic counting.

This module is the cross-check layer: it defines the three rung expressions and proves they coincide, so the $-44$ assignment is not route-dependent.

proof idea

Route A is definitional: $\eta_B$ rung from dimension is $1 - d^2(d+2)$, specialized at $d=3$ to $-44$, with a factored form for algebraic reuse. Route B builds the rung from the Gray-code chirality product and proves equality to the named constant $-44$. Route C does the same from the fermionic DOF gap.

Agreement lemmas then show routes A/B, A/C, and B/C return identical integers. A final identity equates the chirality product to gap-minus-one, tying the CP-geometric count back to the dimension gap. No analytic estimates: pure integer and ring algebra over the imported gap and chirality definitions.

why it matters in Recognition Science

Track4ACert imports this module as the exact-rung leg of the Track 4.A master certificate ($\eta_B$ rung + $\Omega_\Lambda$ band + Planck consistency), status structural with zero sorry. UnifiedForcingChain also imports it, folding the cosmology rung into the T0–T8 inevitability spine from the cost foundation.

Without route agreement, the claim that $\eta_B$ is forced to rung $-44$ would rest on a single counting story. The three-way match (dimension gap from T8's $D=3$, Gray chirality, fermionic DOF) makes the rung a structural invariant rather than a fit parameter, and feeds the interval certificate that confronts Planck data.

scope and limits

used by (2)

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

depends on (7)

Lean names referenced from this declaration's body.

declarations in this module (21)