BaryogenesisCert
plain-language theorem explainer
The BaryogenesisCert structure encodes the φ-ladder trajectory for the baryon asymmetry η_B, requiring a constant ratio φ per rung, completion at rung 44, positivity for all rungs, and exactly five B-violation channels. Cosmologists working in Recognition Science would cite it to connect the J-cost asymmetry to the observed η_B ≈ 6×10^{-10} at the electroweak scale. The declaration is a pure structure definition that packages these four properties with no proof obligations or computational content.
Claim. A baryogenesis certificate on the φ-ladder consists of an asymmetry function η_B : ℕ → ℝ such that η_B(k+1)/η_B(k) = φ for every natural number k, η_B(44) = 1, η_B(k) > 0 for all k, and the inductive type of B-violation channels (sphaleron, electroweak, QCD, leptogenesis, neutrino mass) has cardinality 5.
background
In the Recognition Science framework the baryon asymmetry evolves along a φ-ladder as the universe cools according to T_k = T_GUT · φ^{-k} and η_B(T_k) = φ^{k-44}. The sibling definition etaB(k) := φ^k / φ^44 directly implements this trajectory, so that the ratio property and positivity follow at once from the algebraic properties of φ. The module states that the asymmetry grows by exactly φ per temperature rung and reaches its observed late-time value at rung 44 (gap-45).
proof idea
This declaration is a structure definition that directly records the four required properties. It references the etaB definition from the same module for the rung-ratio, completion, and positivity fields, and the BViolationChannel inductive type for the channel-count field. No lemmas or tactics are applied; the structure simply packages the upstream etaB properties and the five-channel enumeration.
why it matters
This structure supplies the φ-ladder trajectory that is instantiated by baryogenesisCert in BaryogenesisFromJCost and by the corresponding certificate in RSBaryogenesis. It realizes the RS prediction η_B = φ^{-44} at the electroweak scale, closing the dynamical part of baryogenesis within the eight-tick octave and D = 3. The five channels align with configDim D from the forcing chain (T8). It touches the open mapping from J-uniqueness (T5) onto the observed asymmetry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.