baryogenesisCert
plain-language theorem explainer
RS cosmology assembles this definition to certify the baryon asymmetry trajectory along the phi-ladder. It supplies the four fields of BaryogenesisCert by direct reference to etaB_ratio, etaB_at_gap45, etaB_pos, and bViolationChannel_count. Cosmologists working on early-universe asymmetry would cite it to confirm that eta_B grows by exactly phi per cooling rung and reaches the recognition-complete value at rung 44. The construction is a record update with no additional reasoning steps.
Claim. The baryogenesis certificate is the structure asserting that the baryon asymmetry satisfies $η_B(k+1)/η_B(k)=φ$ for every natural number $k$, that $η_B(44)=1$, that $η_B(k)>0$ for all $k$, and that the number of B-violation channels equals five.
background
The module defines the phi-ladder trajectory for baryogenesis: temperature scales as $T_k=T_{GUT}·φ^{-k}$ and the asymmetry as $η_B(T_k)=φ^{k-44}$. The target structure BaryogenesisCert packages four properties: the rung ratio equals phi, completion at rung 44, strict positivity, and exactly five channels. An upstream certificate in BaryogenesisFromJCost uses a different structure with five mechanisms, J-cost equilibrium at 1, and positive J-cost for r not equal to 1. The local setting is the A3 dynamic closure that closes the trajectory without axioms or sorrys.
proof idea
This is a direct record construction. It supplies etaB_rung_ratio by etaB_ratio, etaB_complete by etaB_at_gap45, etaB_always_pos by etaB_pos, and five_channels by bViolationChannel_count. No tactics or reductions occur beyond the field assignments.
why it matters
The definition supplies the trajectory certificate imported by baryogenesisCert in BaryogenesisFromJCost. It realizes the Recognition Science prediction that eta_B reaches φ^{-44} at the electroweak scale via monotone growth by phi per rung. The five-channel count aligns with configDim D=3 in the forcing chain. It closes the phi-ladder part of the baryogenesis argument and leaves open only the derivation of the initial GUT-scale conditions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.