structural_growth_suppression
plain-language theorem explainer
The definition supplies the exponential suppression factor for sigma-8 structure growth in terms of recognition strain Q. Cosmologists modeling ILG corrections to the FRW metric cite this when adjusting growth rates for the Hubble tension. It is implemented as a direct one-line assignment to the real exponential of negative Q.
Claim. The sigma-8 structural growth suppression factor equals $e^{-Q}$ where $Q$ denotes the recognition strain.
background
The Cosmology.HubbleResolution module formalizes Induced Light Gravity (ILG) corrections to the Friedmann-Robertson-Walker metric and shows how the C_lag constant resolves the Hubble tension. The doc-comment identifies this definition as the Sigma-8 Suppression arising from recognition strain Q. No upstream lemmas are referenced in the dependency graph.
proof idea
The declaration is a one-line definition that sets the suppression factor to the real exponential of the negative input strain.
why it matters
This definition supplies the suppression mechanism for structural growth within the ILG framework for Hubble tension resolution. It directly implements the doc-comment's statement that structural growth is suppressed by the recognition strain Q. The module context ties it to FRW metric corrections, though no parent theorems or downstream applications are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.