suppressionFactorNorm
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.