Pith. sign in
module module high

IndisputableMonolith.Cosmology.BaryonAsymmetryDerivation

show as:
view Lean formalization →

Packages the RS derivation of the baryon-to-photon ratio from ledger Sakharov conditions, Gray-code CP violation, three generations, and the Jarlskog invariant. Cosmologists citing the structural form of η_B or the high-T g_★ = 106.75 bookkeeping land here. The module wires imported foundation and SM results into a certified chain ending at the φ-ladder rung for η_B.

claimThe module assembles high-temperature SM relativistic degrees of freedom $g_\star = 106.75$, a structural baryon-to-photon ratio $\eta_B$ on the $\varphi$-ladder (with positivity, smallness, and saturation factors), and a completeness certificate that the chain from Sakharov conditions through CP violation reaches that $\eta_B$.

background

Baryogenesis needs the three Sakharov conditions: baryon-number violation, C and CP violation, and departure from thermal equilibrium. Upstream, SakharovFromLedger states those conditions in RS ledger language. GrayCodeChirality supplies the geometric origin of CP violation: the canonical 3-bit Gray-code cycle on the cube $Q_3$ is chiral, so directed face walks distinguish orientation. ParticleGenerations fixes exactly three fermion families (P-001). CKMFromCube and JarlskogInvariant turn cube geometry, generation torsion, and that chirality into the quark mixing phase and the rephasing-invariant $J_{CP}$.

At $T > T_{EW}$ the SM relativistic DOF are the standard count $g_\star = g_b + (7/8)g_f = 28 + (7/8)\cdot 90 = 106.75$ (minimal-neutrino convention). The module treats this as imported SM bookkeeping with RS-sourced gauge group and generation count, not a free new RS number. Constants supply the RS tick $\tau_0$ used in cosmological normalizations.

proof idea

Definition-and-assembly module, not a single deep proof. It records $g_\star$ and a three-generation DOF inclusion fact, then defines the structural $\eta_B$ (rung, saturation exponent, product with saturation) together with positivity and smallness lemmas. A derivation-chain-complete flag and a BaryonAsymmetryCert bundle assert that the imported Sakharov, chirality, generation, CKM, and Jarlskog pieces close the path to that structural $\eta_B$. Individual equalities lean on upstream modules; this file is the wiring and certificate layer.

why it matters in Recognition Science

Direct parent of EtaBIntervalCert, which proves the interval prediction $\varphi^{-44}\in(5.5\times10^{-10},7.5\times10^{-10})$ containing the Planck 2018 value $\eta_B\approx6.1\times10^{-10}$. Also imported by GStarDerivation, which re-derives $g_\star=106.75$ from $Q_3$-forced SM content. In the broader RS chain this is where ledger Sakharov conditions, Gray-code CP violation, and three generations become a quantitative baryon asymmetry on the $\varphi$-ladder, ready for interval certification rather than left as qualitative Sakharov talk.

scope and limits

used by (2)

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

depends on (6)

Lean names referenced from this declaration's body.

declarations in this module (11)