Sigma8SuppressionCert
plain-language theorem explainer
The Sigma8SuppressionCert structure certifies that the recognition strain J(φ) lies in (0.11, 0.12), that strain vanishes for all wavenumbers k below the 8-tick scale k8, that the weak-lensing to CMB σ8 ratio lies in (0.93, 0.95), and that the RS-predicted ratio matches observation inside twice the weak-lensing error. Cosmologists addressing the σ8 tension would cite this certificate as the quantitative check that Recognition Science strain reproduces the observed suppression. It is assembled as a structure that bundles four independently-verif
Claim. A certificate asserting four properties: (i) $0.11 < J(φ) < 0.12$, (ii) strainAtScale$(k,k_8)=0$ whenever $0<k_8$ and $k≤k_8$, (iii) $0.93 < σ_8^{WL}/σ_8^{CMB} < 0.95$, and (iv) $|σ_8^{WL}/σ_8^{CMB} - r_{pred}| < 2·(σ_8^{WL,err}/σ_8^{CMB})$, where $r_{pred}$ is the normalized suppression factor from the 8-tick strain.
background
In the Recognition Science module on σ8 suppression, structure growth is governed by the recognition operator whose 8-tick neutrality constraint introduces a coupling scale λ8. The auxiliary function strainAtScale(k,k8) returns zero for k≤k8 (large-scale, unsuppressed growth) and Jcost(k/k8) otherwise, with Jcost the J-function J(x)=(x+1/x)/2−1. Upstream constants fix σ8_CMB=0.811 (Planck) and σ8_WL=0.76 (DES+KiDS), while predicted_ratio is obtained from the normalized suppressionFactorNorm applied to the effective calibrated strain Q.
proof idea
The declaration is a structure definition with an empty proof body. It packages four fields whose values are supplied by separate lemmas in the same module: Jcost_phi_bounds for the strain-scale interval, growth_suppression_scale_separation for the universal quantification over k and k8, observed_ratio_bounds for the ratio interval, and sigma8_match for the absolute-difference bound. No further tactics are applied.
why it matters
Sigma8SuppressionCert is the type of the instance sigma8Suppression_verified, which constructs it from the four supporting lemmas. It supplies the concrete certificate that the 8-tick octave (T7) produces a suppression factor matching weak-lensing data to within 2σ, thereby implementing the Recognition Science resolution of the σ8 tension stated in the module doc-comment. The J(φ) interval anchors the phi-ladder prediction for the coupling scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.