eta_B_corrected_two_sided_pos
plain-language theorem explainer
The corrected baryon-to-photon ratio η_B^RS = (1 − φ^(−8))^2 · φ^(−44) is strictly positive. Cosmologists assembling the RS η_B band cite this as the sign gate before interval arithmetic. The proof unfolds the product definition and multiplies the two existing positivity lemmas for the prefactor and the bare φ-scale.
Claim. The corrected RS prediction satisfies $0 < c_{\mathrm{RS}}\cdot\varphi^{-44}$, where $c_{\mathrm{RS}}=(1-\varphi^{-8})^2$ is the selected order-one prefactor and $\varphi$ is the golden ratio.
background
In RS cosmology the bare baryon asymmetry sits on the φ-ladder at rung −44: η_B^scale = φ^(−44). This module multiplies that scale by an order-one prefactor c_RS = (1 − φ^(−8))^2 to form the corrected prediction. The module docstring is explicit that c_RS is a selected ansatz, not a Boltzmann-derived washout; only algebra and numerical bounds are claimed as theorems.
Upstream, eta_B_phi_scale_pos shows 0 < φ^(−44) by zpow_pos and positivity of φ. Independently, c_RS_pos shows 0 < c_RS by squaring the positive correction factor (1 − φ^(−8)). The corrected quantity is defined simply as their product.
proof idea
Term-mode one-liner after unfold. Unfold the corrected prediction to the product c_RS · η_B^scale, then apply mul_pos to the pair of positivity lemmas c_RS_pos and eta_B_phi_scale_pos. Both factors are already known positive, so the product is positive.
why it matters
Positivity is the first algebraic gate on the corrected η_B prediction. The module then proves c_RS < 1 and the interval inclusion c_RS · φ^(−44) ∈ (6.0, 6.2)×10^(−10); those steps need a strictly positive base. No downstream users are recorded yet. Framework landmarks: φ is forced at T6, and the eight-tick octave (T7) supplies the heuristic scale δ = φ^(−8) in the two-sided washout story retained only as motivation. The module leaves open a genuine Γ/H rate derivation of the squared prefactor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.