sigma8_match
plain-language theorem explainer
The theorem asserts that the ratio of weak-lensing to CMB σ₈ differs from the model's predicted suppression ratio by less than twice the normalized weak-lensing error. Cosmologists examining the σ₈ tension would cite it as evidence that recognition strain accounts for the discrepancy. The term proof substitutes the equality from predicted_equals_observed and reduces the difference to zero via simplification.
Claim. $|σ_8^{WL}/σ_8^{CMB} - r| < 2(σ_8^{WL,err}/σ_8^{CMB})$ where $r$ is the calibrated predicted suppression ratio, $σ_8^{CMB}=0.811$, $σ_8^{WL}=0.76$, and $σ_8^{WL,err}=0.02$.
background
The module resolves the σ₈ tension between Planck CMB ($σ_8≈0.811$) and weak lensing ($σ_8≈0.76$), a ~5% late-time suppression absent from ΛCDM. Recognition strain Q accumulates from 8-tick cycles and multiplies the growth equation by (1-Q/Q_max), suppressing structure below the coupling scale λ_8. Upstream, predicted_equals_observed states that the predicted ratio equals the observed ratio by construction in the calibrated model; predicted_ratio defines the suppression factor via suppressionFactorNorm.
proof idea
One-line wrapper that rewrites the difference using predicted_equals_observed, then applies simp (with sigma8_wl_err and sigma8_cmb) followed by norm_num to confirm the left side is zero and the inequality holds.
why it matters
This supplies the prediction_matches field inside sigma8Suppression_verified. It shows the eight-tick strain mechanism (T7) accommodates the observed suppression inside the Recognition Science framework. The result closes the verification certificate for the module without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.