def
definition
Q_max
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cosmology.Sigma8Suppression on GitHub at line 80.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
77/-- The maximum strain from a single 8-tick cycle.
78
79 Q_max = J(φ) since the maximum stable ratio in a cycle is φ. -/
80noncomputable def Q_max : ℝ := Jcost phi
81
82/-! ## Suppression Factor Derivation -/
83
84/-- The growth suppression factor from recognition strain.
85
86 f_sup = 1 - Q/Q_max
87
88 where Q is the accumulated strain from structure formation. -/
89noncomputable def suppressionFactor (Q : ℝ) : ℝ := 1 - Q / Q_max
90
91/-- The predicted σ₈ after RS suppression. -/
92noncomputable def sigma8_predicted (Q : ℝ) : ℝ :=
93 sigma8_cmb * suppressionFactor Q
94
95/-! ## The Calibrated Strain -/
96
97/-- The maximum theoretical strain (normalized to 1 for convenience). -/
98noncomputable def Q_max_normalized : ℝ := 1
99
100/-- The suppression factor using normalized strain.
101 f_sup = 1 - Q/1 = 1 - Q -/
102noncomputable def suppressionFactorNorm (Q : ℝ) : ℝ := 1 - Q
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)