etaB_small
plain-language theorem explainer
The theorem proves that the Recognition Science baryon asymmetry etaB_RS satisfies etaB_RS times 10 to the 8 is less than 1, i.e., etaB less than 10 to the negative 8. Cosmologists modeling baryogenesis via the phi-ladder would cite this to confirm the predicted asymmetry lies below observational upper limits. The proof is a term-mode reduction that unfolds the definitions, rewrites via the positive inverse-multiplier inequality, simplifies the unit multiplication, and applies the prior phi to the 44 greater than 10 to the 8 bound.
Claim. $η_B < 10^{-8}$, where $η_B := φ^{-44}$ and $φ$ is the golden-ratio fixed point of the Recognition Science forcing chain.
background
The module Baryon Asymmetry From Phi Ladder derives the baryon asymmetry parameter from the phi-ladder in Recognition Science cosmology. Key definitions are baryonRung, which fixes the exponent at 44, and etaB_RS, which is the inverse of phi raised to baryonRung. An upstream theorem establishes phi to the 44 exceeds 10 to the 8, while an arithmetic lemma supplies the unit-multiplication identity. The local setting is the A3 Baryogenesis section, which states the RS prediction η_B ≈ φ^{-44} with zero axioms or sorrys.
proof idea
The term proof unfolds etaB_RS and baryonRung to obtain the concrete inequality. It rewrites using inv_mul_lt_iff₀ applied to the positivity of phi to the 44, converting the product bound into a direct comparison of phi to the 44 against 10 to the 8. Simplification via mul_one removes the unit factor, after which the proof concludes by exact application of the phi44_gt_1e8 theorem.
why it matters
This result supplies the final smallness component of the baryonAsymmetryCert definition, which packages the chosen rung, positivity of etaB, the phi44 largeness bound, and this upper bound. It realizes the A3 Baryogenesis step in the Recognition Science framework, where the phi fixed point (T6) and eight-tick octave (T7) generate the hierarchy that forces η_B to be small. The bound aligns the phi-ladder prediction with the observed baryon-to-photon ratio without additional parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.