c_RS_lower
plain-language theorem explainer
This theorem proves the strict lower bound c_RS > 0.956 on the RS baryogenesis prefactor defined as (1 - phi^{-8})^2. Cosmologists deriving the eta_B prediction band in Recognition Science cite it to anchor the numerical interval that matches Planck data. The proof rewrites via the expanded definition and applies nlinarith to the companion bounds on (1 - phi^{-8}).
Claim. $c_{RS} := (1 - phi^{-8})^2 > 0.956$
background
In the Eta B Prefactor module the prefactor c_RS is defined as the square of (1 - phi^{-8}), encoding two independent washout channels for matter and antimatter sectors at the eight-tick scale. The module derives this from the integration-gap rung and Fibonacci identities for phi^8. Upstream, c_RS_expanded unfolds the definition to (1 - phi^{-8})^2 while one_minus_phi_neg8_lower and one_minus_phi_neg8_upper supply the interval (0.978, 0.979) for the inner term.
proof idea
The proof applies the rewrite from c_RS_expanded to express the claim in terms of (1 - phi^{-8})^2. It invokes one_minus_phi_neg8_lower and one_minus_phi_neg8_upper to obtain 0.978 < (1 - phi^{-8}) < 0.979. nlinarith then combines these inequalities to conclude the squared term exceeds 0.956.
why it matters
This bound feeds directly into eta_B_corrected_lower, which establishes eta_B_corrected > 6.0e-10, and into etaBPrefactorCert that packages the full prefactor band and observed match. It closes the numerical part of the module claim that c_RS lies in (0.956, 0.959), supporting the eight-tick octave structure and D = 3 spatial dimensions in the forcing chain. The interpretive 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.