lambda_8

formal source

  63
  64    This is the scale below which recognition strain becomes significant.
  65    Derived from: λ_8 = 8 · τ_0 · c / H_0 ≈ 8 Mpc. -/
  66noncomputable def lambda_8 : ℝ := 8
  67
  68/-- The recognition strain Q at a given scale k.
  69
  70    Q(k) = J(k/k_8) where k_8 = 2π/λ_8 is the 8-tick wavenumber.
  71
  72    For k ≪ k_8: Q ≈ 0 (large scales, no suppression)
  73    For k ≫ k_8: Q ≈ J_max (small scales, maximum suppression) -/
  74noncomputable def strainAtScale (k k8 : ℝ) : ℝ :=
  75  if k ≤ k8 then 0 else Jcost (k / k8)
  76
  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