sigma8_wl
plain-language theorem explainer
sigma8_wl supplies the weak-lensing value of the matter fluctuation amplitude on 8 Mpc scales. Cosmologists comparing structure growth predictions to DES Y3 and KiDS-1000 data would cite this constant when quantifying the σ₈ tension. The declaration is a direct numerical assignment with no lemmas or reductions applied.
Claim. $σ_8^{WL} = 0.76$, where $σ_8^{WL}$ is the rms amplitude of matter density fluctuations smoothed on 8 Mpc scales inferred from combined weak lensing surveys.
background
The module establishes that recognition strain Q, accumulated through 8-tick cycles, suppresses structure growth below the coupling scale λ_8 and thereby accounts for the observed σ₈ tension. Planck CMB yields σ₈ ≈ 0.811 while weak lensing surveys yield lower values; the Recognition Science resolution expresses the suppressed amplitude as σ₈^{RS} = σ₈^{CMB} ⋅ (1 − Q/Q_max). The upstream theorem from PrimitiveDistinction.from supplies the seven axioms that reduce to the four structural conditions plus three definitional facts used to ground the recognition operator and neutrality constraint.
proof idea
The declaration is a direct definition that assigns the constant 0.76. No lemmas are invoked and no tactics are executed; the body is a literal real number.
why it matters
sigma8_wl anchors the downstream theorems observed_suppression, Q_effective_calibrated, observed_ratio_bounds, predicted_equals_observed, and sigma8_match. These results demonstrate that the 8-tick strain mechanism produces a suppression ratio of approximately 0.937, matching weak lensing data to within 2σ. The constant therefore supplies the observational input required to close the σ₈ tension resolution inside the Recognition Science framework, directly implementing the module's claim that the predicted suppression matches observations exactly by construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.