c_RS_pos
plain-language theorem explainer
The theorem establishes that the RS baryogenesis prefactor c_RS = (1 - φ^{-8})^2 is strictly positive. Cosmologists deriving the corrected η_B band in Recognition Science cite it to guarantee the prefactor does not cancel the φ^{-44} term. The term proof unfolds the definition to the square of the correction factor, imports the lower bound (1 - φ^{-8}) > 0.978, and applies the positivity tactic.
Claim. 0 < (1 - φ^{-8})^2, where φ is the golden ratio and the expression is the two-sided 8-tick washout prefactor in the η_B formula.
background
The module derives the order-one prefactor c in η_B = c × (algebraic content from the integration-gap rung). The single-tick correction factor is defined as 1 - φ^{-8}, and c_RS is its square, encoding independent washout channels for matter and antimatter sectors at the eight-tick octave (T7). Upstream, one_minus_phi_neg8_lower supplies the concrete bound (1 - φ^{-8}) > 0.978 obtained from the upper estimate on φ^{-8}. Separate c_RS definitions appear in gravity modules (leading-log coefficient -log φ / 2 and propagation speed 1), but the present declaration uses the cosmology version.
proof idea
The proof is a term-mode one-liner. It unfolds c_RS and correctionFactor to expose the square, obtains the strict lower bound on the base via one_minus_phi_neg8_lower, and hands the expression to the positivity tactic, which concludes the square is positive.
why it matters
The result is invoked directly by eta_B_corrected_pos, eta_B_corrected_lower, and eta_B_corrected_upper to bound the corrected η_B prediction inside (6.0 × 10^{-10}, 6.2 × 10^{-10}), matching the Planck 2018 interval. It supplies the positivity leg of etaBPrefactorCert and closes the positivity requirement inside the eight-tick washout construction of the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.