c_RS_upper
plain-language theorem explainer
The upper bound establishes that the Recognition Science baryogenesis prefactor c_RS, given by (1 - φ^{-8})^2, lies strictly below 0.959. Modelers of the baryon asymmetry would cite the result to close the upper end of the predicted η_B interval. The proof rewrites to the expanded form then applies linear arithmetic on the two supplied bounds for the base term (1 - φ^{-8}).
Claim. The washout prefactor satisfies $c_{RS} < 0.959$, where $c_{RS} = (1 - φ^{-8})^2$.
background
The module treats the order-one prefactor in the baryogenesis formula η_B = c × (integration-gap algebraic content). It defines c_RS as (1 − φ^{-8})^2 to capture two independent washout channels, each tied to one rung at the eight-tick scale in three spatial dimensions. Upstream results supply the definition c_RS := correctionFactor ^ 2, the expansion theorem equating it to (1 - φ^{-8})^2, and the companion bounds 0.978 < (1 - φ^{-8}) < 0.979 obtained from the Fibonacci identity for φ^8.
proof idea
The proof first rewrites the goal via the expansion theorem to reach (1 - φ^{-8})^2 < 0.959. It then introduces the lower bound on (1 - φ^{-8}) from one_minus_phi_neg8_lower and the upper bound from one_minus_phi_neg8_upper. Linear arithmetic on these two facts closes the inequality.
why it matters
The bound supplies the upper endpoint of the prefactor band used by eta_B_corrected_upper to cap the corrected η_B prediction below 6.2 × 10^{-10} and by etaBPrefactorCert to certify the full band. It completes the numerical verification of the 8-tick washout model, aligning with the eight-tick octave and D = 3 from the forcing chain. The squared form remains hypothesis-grade pending a first-principles Boltzmann derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.