c_RS_upper
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}).
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the squared washout form from the Recognition Composition Law.
- Does not compute the full η_B without the integration-gap rung content.
- Does not fold Planck measurement errors into the bound.
- Does not address the matching lower bound on the prefactor.
formal statement (Lean)
138theorem c_RS_upper : c_RS < 0.959 := by
proof body
Term-mode proof.
139 rw [c_RS_expanded]
140 have hl : (1 - phi ^ (-8 : ℤ)) > 0.978 := one_minus_phi_neg8_lower
141 have hu : (1 - phi ^ (-8 : ℤ)) < 0.979 := one_minus_phi_neg8_upper
142 nlinarith [hl, hu]
143
144/-! ## φ^(−44) bounds via the Fibonacci identity -/
145
146/-- `φ^(n+1) = F(n+1) · φ + F(n)`. (Standard Fibonacci-φ identity.) -/