pith. machine review for the scientific record. sign in
def

Q_max

definition
show as:
view math explainer →
module
IndisputableMonolith.Cosmology.Sigma8Suppression
domain
Cosmology
line
80 · github
papers citing
none yet

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

A cached Ask Recognition explainer exists for this declaration.

open explainer

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)