suppressionFactorNorm

formal source

  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)
 111
 112    The dilution factor accounts for cosmic expansion reducing
 113    the cumulative strain at the σ₈ scale. -/
 114noncomputable def Q_effective_calibrated : ℝ := 1 - sigma8_wl / sigma8_cmb
 115
 116/-- The predicted suppression ratio (calibrated to observations). -/
 117noncomputable def predicted_ratio : ℝ := suppressionFactorNorm Q_effective_calibrated
 118
 119/-! ## Verification Theorems -/
 120
 121/-- J(φ) bounds: J(φ) = (φ + 1/φ)/2 - 1 ≈ 0.118. -/
 122theorem Jcost_phi_bounds :
 123    (0.11 : ℝ) < Jcost phi ∧ Jcost phi < (0.12 : ℝ) := by
 124  have hφ : 1 < phi := one_lt_phi
 125  have hφ_pos : 0 < phi := phi_pos
 126  -- φ ≈ 1.618, so φ + 1/φ ≈ 2.236, and (φ + 1/φ)/2 - 1 ≈ 0.118
 127  have h_phi_upper : phi < 1.62 := phi_lt_two
 128  have h_phi_lower : (1.61 : ℝ) < phi := by
 129    have := phi_gt_one_and_half
 130    linarith
 131  have h_inv_lower : 1 / 1.62 < 1 / phi := by
 132    apply div_lt_div_of_pos_left zero_lt_one hφ_pos h_phi_upper