etaB_pos
plain-language theorem explainer
RS baryon asymmetry η_B^{RS} defined as φ^{-44} is strictly positive. Cosmologists modeling baryogenesis on the phi-ladder cite this to fix the sign of the predicted asymmetry. The proof is a one-line term application of inverse positivity to a positive power.
Claim. $0 < η_B^{RS}$ where $η_B^{RS} := φ^{-44}$ and $φ > 1$ is the golden-ratio fixed point with the baryon rung fixed at 44.
background
The Baryon Asymmetry from Phi-Ladder module fixes the baryon rung at 44 and defines etaB_RS as the reciprocal of phi raised to that power, yielding the RS prediction η_B ≈ φ^{-44}. This sits inside the broader phi-ladder construction where masses and asymmetries scale as yardstick times phi to a rung offset. The module states φ^{44} > 10^8 as a large-number bound and reports zero axioms or sorrys.
proof idea
The proof is a term-mode one-liner that applies inv_pos.mpr to pow_pos phi_pos baryonRung. It uses the upstream positivity of phi and the power lemma to obtain positivity of the inverse directly.
why it matters
This theorem supplies the eta_pos field inside baryonAsymmetryCert and the etaB_always_pos field inside baryogenesisCert. It fills the positivity requirement for the A3 Baryogenesis step, confirming the sign of η_B ≈ φ^{-44} that follows from the phi fixed point (T6) and the eight-tick octave (T7). It leaves open the precise numerical match to the observed asymmetry inside the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.