observed_suppression
plain-language theorem explainer
The observed suppression factor is the ratio of weak-lensing σ₈ to CMB σ₈. Cosmologists examining the σ₈ tension within Recognition Science cite this definition to quantify the empirical discrepancy between Planck and DES/KiDS data. The definition is a direct division of the two fixed empirical constants supplied by the module.
Claim. The observed suppression factor is defined as the ratio $0.76 / 0.811$, where $0.811$ is the CMB value of σ₈ and $0.76$ is the weak-lensing value of σ₈.
background
The module addresses the σ₈ tension: Planck CMB reports σ₈ ≈ 0.811 while weak lensing and cluster counts give σ₈ ≈ 0.76, a roughly 5% suppression at late times unexplained in ΛCDM. Recognition Science resolves the discrepancy by introducing recognition strain Q that accumulates over 8-tick cycles below the coupling scale λ₈ ≈ 8 Mpc, yielding the model σ₈^{RS} = σ₈^{CMB} · (1 - Q/Q_max). Upstream constants supply the two σ₈ values directly: sigma8_cmb is fixed at 0.811 and sigma8_wl at 0.76. The tick definition from Constants supplies the fundamental time quantum τ₀ = 1 used to derive the 8-tick octave elsewhere in the framework.
proof idea
This is a one-line definition that returns the quotient of the two module-level constants sigma8_wl and sigma8_cmb.
why it matters
The definition supplies the empirical target that the recognition-strain model must reproduce. It sits inside the module's resolution of the σ₈ tension via the 8-tick neutrality constraint and the suppression formula given in the module documentation. No downstream theorems depend on it yet, leaving it as the observational anchor for future comparisons with the predicted suppressionFactor and Q_max.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.