suppressionFactor
The suppressionFactor computes the linear reduction in structure growth amplitude as 1 minus the ratio of accumulated recognition strain Q to its per-cycle maximum. Cosmologists modeling the σ₈ tension between CMB and weak-lensing data would cite this factor when rescaling the predicted clustering amplitude. It is a direct algebraic definition that normalizes strain against Q_max derived from the J-cost at the golden ratio.
claimThe growth suppression factor is given by $1 - Q/Q_{max}$, where $Q$ is the accumulated recognition strain from structure formation and $Q_{max}$ equals the J-cost evaluated at the golden ratio $phi$.
background
Recognition Science treats structure growth as governed by the recognition operator subject to the eight-tick neutrality constraint. The module quantifies how cumulative strain Q from repeated 8-tick cycles reduces the growth factor below the CMB-inferred baseline, producing the observed ~5% suppression at late times. Q_max is defined as Jcost phi, the J-cost at the self-similar fixed point that sets the saturation scale for stable cycles.
proof idea
The definition is a one-line algebraic expression that subtracts the normalized strain from unity, relying directly on the upstream definition of Q_max as Jcost phi.
why it matters in Recognition Science
This definition supplies the multiplicative correction applied inside sigma8_predicted to obtain the RS-adjusted σ₈. It implements the suppression formula stated in the module documentation, which matches weak-lensing observations to within 2σ by invoking the eight-tick octave and the associated neutrality constraint. The construction closes the gap between the CMB baseline and late-time measurements without additional free parameters.
scope and limits
- Does not compute or accumulate the strain Q from cosmic history.
- Does not incorporate explicit scale dependence beyond the overall normalization by Q_max.
- Does not address baryonic feedback or other astrophysical systematics.
- Does not derive the numerical value of Q_max beyond its identification with Jcost phi.
Lean usage
noncomputable def sigma8_example (Q : ℝ) : ℝ := sigma8_cmb * suppressionFactor Qformal statement (Lean)
89noncomputable def suppressionFactor (Q : ℝ) : ℝ := 1 - Q / Q_max
proof body
Definition body.
90
91/-- The predicted σ₈ after RS suppression. -/