module module moderate

`IndisputableMonolith.Cosmology.Sigma8Suppression`

Sigma8Suppression module defines sigma8 values from Planck CMB 2018 and weak lensing, plus suppression factors and predicted sigma8 in the Recognition Science model. Researchers in cosmology comparing RS to observations would cite it for structure formation tests. It consists entirely of definitions importing Constants and Cost modules.

claim$σ_8^{CMB}$, $σ_8^{WL}$, observed suppression, $λ_8$, strain at scale, $Q_{max}$, suppression factor, $σ_8^{predicted}$ and normalized variants.

background

The module operates in the Recognition Science cosmology setting, where parameters derive from the fundamental time quantum $τ_0 = 1$ tick. It imports the Constants module for $τ_0$ and the Cost module for J-cost and defect calculations. Definitions here translate these into sigma8 suppression metrics for CMB and large-scale structure.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies sigma8 suppression data that anchors comparisons in the broader Recognition Science cosmology. It supports observable predictions for structure growth within the unified forcing chain.

scope and limits

Does not derive sigma8 from the Recognition Composition Law.
Does not specify the full phi-ladder for mass scales.
Does not include dynamic evolution equations for suppression.
Does not validate against other datasets beyond Planck 2018.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (23)

def sigma8_cmb L46
def sigma8_cmb_err L49
def sigma8_wl L52
def sigma8_wl_err L55
def observed_suppression L58
def lambda_8 L66
def strainAtScale L74
def Q_max L80
def suppressionFactor L89
def sigma8_predicted L92
def Q_max_normalized L98
def suppressionFactorNorm L102
def Q_effective_calibrated L114
def predicted_ratio L117
theorem Jcost_phi_bounds L122
theorem observed_ratio_bounds L149
theorem Q_effective_bounds L157
theorem predicted_equals_observed L166
theorem sigma8_match L176
def H_GrowthEquation L193
theorem growth_suppression_scale_separation L200
structure Sigma8SuppressionCert L208
def sigma8Suppression_verified L219