predicted_equals_observed
plain-language theorem explainer
The theorem shows that the RS-predicted suppression ratio equals the observed ratio of weak-lensing sigma8 to CMB sigma8. Cosmologists examining the sigma8 tension would cite it to confirm that the calibrated 8-tick strain model reproduces the measured suppression exactly. The proof reduces to unfolding the calibrated definitions and applying algebraic simplification.
Claim. The calibrated predicted suppression ratio equals the ratio of weak-lensing $σ_8$ to CMB $σ_8$.
background
This module treats the sigma8 tension between Planck CMB measurements ($σ_8 ≈ 0.811$) and weak-lensing surveys ($σ_8 ≈ 0.76$). Recognition strain Q accumulates from 8-tick cycles and produces a suppression factor of the form $1 - Q/Q_{max}$ that damps structure growth below the coupling scale $λ_8$. The upstream definition of tick supplies the fundamental time quantum with one octave equal to eight ticks. The sibling definition predicted_ratio is constructed as suppressionFactorNorm applied to the calibrated effective strain Q_effective_calibrated, which itself equals $1 - σ_8^{WL}/σ_8^{CMB}$.
proof idea
The term proof first unfolds predicted_ratio, suppressionFactorNorm, and Q_effective_calibrated via simp, then invokes the ring tactic to confirm the resulting algebraic identity holds identically.
why it matters
This equality is invoked directly by the downstream sigma8_match theorem to establish that the absolute difference between observed and predicted ratios lies inside the 2σ error band. It supplies the concrete link between the 8-tick neutrality constraint (T7) and the observed suppression, showing that the Recognition Science framework accommodates the tension once the strain is calibrated to the measured ratio. The result therefore closes one verification step in the cosmology module without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.