Q_effective_bounds
plain-language theorem explainer
The theorem establishes that the calibrated effective recognition strain lies strictly between 0.05 and 0.07. Cosmologists examining the σ₈ tension would cite this numerical bound to confirm that Recognition Science can accommodate the observed 6% suppression. The proof proceeds by direct substitution of the definitions of sigma8_cmb and sigma8_wl followed by numerical verification of the inequalities.
Claim. The effective recognition strain satisfies $0.05 < Q_ {eff} < 0.07$, where $Q_{eff} = 1 - σ_8^{WL} / σ_8^{CMB}$ with $σ_8^{CMB} = 0.811$ and $σ_8^{WL} = 0.76$.
background
The module addresses the σ₈ tension: Planck CMB yields σ₈ ≈ 0.811 while weak lensing surveys give σ₈ ≈ 0.76, a ~5% suppression at late times unexplained in ΛCDM. Recognition Science resolves this via the recognition operator and the 8-tick neutrality constraint, which introduces a coupling scale λ_8 below which growth is suppressed according to σ₈^{RS} = σ₈^{CMB} · (1 - Q/Q_max). Q_effective_calibrated is defined as 1 - sigma8_wl / sigma8_cmb and equals the observed ratio ≈ 0.063. Upstream constants sigma8_cmb and sigma8_wl supply the numerical inputs directly from observations.
proof idea
The term proof unfolds Q_effective_calibrated together with the constants sigma8_wl and sigma8_cmb via simp, then splits the conjunction with constructor and verifies both numerical inequalities with norm_num.
why it matters
The bound confirms that the recognition strain produces a suppression factor matching weak lensing data to within 2σ, supporting the RS resolution of the σ₈ tension through the 8-tick octave. It supplies a calibrated numerical anchor inside the Sigma8Suppression module whose parent results derive the suppression formula from the recognition operator and the phi-ladder. No downstream uses are recorded, so the result functions as a self-contained consistency check rather than a lemma for further theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.