etaB
plain-language theorem explainer
etaB(k) supplies the baryon asymmetry parameter at rung k on the φ-ladder trajectory in RS cosmology. Modelers of dynamical baryogenesis from GUT to electroweak scales cite it to track the exact φ-multiplication per temperature step. The implementation is a direct one-line definition etaB(k) = phi^k / phi^44.
Claim. The baryon asymmetry at temperature rung $k$ is given by $η_B(k) = φ^{k-44}$.
background
The module sets the local setting for baryogenesis as a φ-ladder on the temperature axis: $T_k = T_{GUT} · φ^{-k}$ with $η_B(T_k) = φ^{k-44}$. RS predicts the late-time value $η_B = φ^{-44}$ reached at the electroweak scale when $k=44$ (gap-45), while the asymmetry remains negligible at $k=0$ (GUT scale). The trajectory is monotone: $η_B(T_{k+1}) / η_B(T_k) = φ$ so the asymmetry grows by exactly φ per rung as the universe cools.
proof idea
This is a one-line definition that directly sets etaB(k) to phi^k / phi^44.
why it matters
The definition supplies the core expression referenced by BaryogenesisCert (which asserts the rung ratio equals phi, completeness at rung 44, strict positivity, and five B-violation channels) together with the supporting theorems etaB_at_gap45, etaB_pos and etaB_ratio. It realizes the φ-ladder step in the cosmology module and connects to the Recognition Science prediction of η_B = φ^{-44} at the electroweak scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.