sigma8_cmb_err
plain-language theorem explainer
sigma8_cmb_err supplies the Planck CMB uncertainty on σ₈ as the constant 0.006. Cosmologists comparing RS structure-growth predictions to observations would reference this value when quantifying the tension with weak-lensing data. The definition is a direct numerical assignment.
Claim. The Planck CMB error on the amplitude of matter fluctuations is given by $0.006$.
background
The module treats the σ₈ tension between Planck CMB (≈0.811 ± 0.006) and weak-lensing surveys (≈0.76 ± 0.02). Recognition Science accounts for the ~5 % late-time suppression through the recognition operator and the 8-tick neutrality constraint that introduces a coupling scale below which growth is damped by cumulative strain Q. The upstream theorem from PrimitiveDistinction converts seven independent axioms into four structural conditions plus three definitional facts that justify the recognition operator used throughout the module.
proof idea
Direct numerical definition; no lemmas or tactics are applied.
why it matters
The constant fixes the CMB error bar for the suppression formula σ₈^{RS} = σ₈^{CMB} ⋅ (1 - Q/Q_max) that the module uses to match weak-lensing observations. It therefore anchors the quantitative test of the eight-tick octave and the recognition-strain mechanism inside the cosmology section. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.