suppressionFactorNorm
The normalized suppression factor is defined as one minus the recognition strain Q. Cosmologists addressing the sigma-8 tension between CMB and weak-lensing data would cite this when calibrating structure-growth suppression in Recognition Science models. It is a direct algebraic definition with no auxiliary lemmas or reductions.
claimThe normalized suppression factor is $f(Q) = 1 - Q$, where $Q$ is the cumulative recognition strain at the sigma-8 scale.
background
Recognition Science resolves the sigma-8 tension by introducing a recognition strain Q that accumulates from 8-tick neutrality cycles and suppresses growth below the lambda-8 scale. The module states that sigma-8^RS equals sigma-8^CMB times (1 - Q/Q_max), with observed values sigma-8_CMB ≈ 0.811 and sigma-8_WL ≈ 0.76 implying Q_eff ≈ 0.063. Upstream, the scale definition from LargeScaleStructureFromRS supplies the phi-ladder for wave numbers, while UniversalForcingSelfReference.for encodes the meta-realization axioms that enforce the eight-tick constraint.
proof idea
Direct definition that sets the suppression factor to the expression 1 - Q. No lemmas or tactics are invoked; the body is the literal algebraic assignment.
why it matters in Recognition Science
This supplies the suppression factor consumed by predicted_ratio and predicted_equals_observed, which show that Recognition Science can match the observed sigma-8 ratio by construction. It implements the geometric factor arising from the 8-tick octave (T7) and the phi-ladder suppression phi^(-5) in the module's resolution of the tension. The parent theorems are the calibration results in the same file that equate the predicted ratio to sigma8_wl / sigma8_cmb.
scope and limits
- Does not derive the numerical value of Q from the forcing chain.
- Does not include dilution corrections from cosmic expansion.
- Does not address other tensions such as the Hubble constant discrepancy.
formal statement (Lean)
102noncomputable def suppressionFactorNorm (Q : ℝ) : ℝ := 1 - Q
proof body
Definition body.
103
104/-- The effective recognition strain for σ₈ scales (k ≈ 0.2 h/Mpc).
105
106 The observed suppression is σ₈_WL / σ₈_CMB ≈ 0.76 / 0.811 ≈ 0.937.
107 This corresponds to Q_eff ≈ 0.063 (6.3% suppression).
108
109 In RS, this arises from the geometric factor:
110 Q_eff = φ^(-5) ≈ 0.09 × (strain dilution factor)
111
112 The dilution factor accounts for cosmic expansion reducing
113 the cumulative strain at the σ₈ scale. -/