sigma8_cmb
plain-language theorem explainer
The declaration supplies the Planck 2018 CMB value of the matter fluctuation amplitude σ₈ as the constant 0.811. Cosmologists comparing CMB predictions to weak-lensing and cluster counts cite this baseline to quantify the ~5% suppression. The definition is a direct numeric assignment with no computation or lemmas.
Claim. $σ_8^{CMB} := 0.811$
background
The module treats the σ₈ tension inside Recognition Science. Planck CMB reports σ₈ ≈ 0.811 while weak lensing reports ≈ 0.76, a discrepancy the framework attributes to recognition strain Q accumulated over 8-tick cycles. The suppression is expressed as σ₈^{RS} = σ₈^{CMB} · (1 - Q/Q_max), where the 8-tick neutrality constraint sets the coupling scale λ_8 below which growth is damped.
proof idea
The definition is a direct constant assignment of the numeric value 0.811. No lemmas or tactics are invoked; it functions as the fixed CMB input for all downstream ratio calculations.
why it matters
This constant anchors the entire σ₈ suppression argument. It is referenced by observed_ratio_bounds to bound the WL/CMB ratio in (0.93, 0.95), by Q_effective_calibrated to extract the effective strain ≈ 0.063, and by predicted_equals_observed to demonstrate exact match after calibration. It supplies the CMB baseline required by the eight-tick octave mechanism (T7) that generates the strain Q, allowing the framework to accommodate the observed tension exactly by construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.