sigma8_wl_err
plain-language theorem explainer
sigma8_wl_err assigns the constant 0.02 as the weak-lensing uncertainty on the matter fluctuation amplitude σ₈. Cosmologists testing Recognition Science predictions against DES and KiDS data would cite this error bar to quantify agreement with the suppressed growth model. The definition is a direct numerical assignment with no lemmas or computation.
Claim. The weak-lensing measurement uncertainty on the amplitude of matter fluctuations is defined by $σ_8^{WL,err} := 0.02$.
background
The module treats the σ₈ tension between Planck CMB values (≈0.811) and weak-lensing surveys (≈0.76). Recognition Science attributes the late-time suppression to cumulative recognition strain Q generated by 8-tick cycles below the coupling scale λ_8, yielding the relation σ₈^{RS} = σ₈^{CMB} ⋅ (1 - Q/Q_max). This definition supplies the observational error used on the weak-lensing side of that comparison.
proof idea
The declaration is a one-line definition that directly sets the constant 0.02. No lemmas or tactics are applied.
why it matters
The value is invoked inside the theorem sigma8_match to show the Recognition Science ratio lies inside 2σ of weak-lensing data, and it appears in the Sigma8SuppressionCert structure that certifies the J(φ) strain scale together with the large-scale unsuppressed regime. It therefore anchors the framework claim that the 8-tick octave produces the observed suppression without additional parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.