exp_factor_bounded

formal source

  68  exact mul_pos alpha_seed_positive (Real.exp_pos _)
  69
  70/-- The exponential factor is in (0, 1] since f_gap ≥ 0 (assuming w₈ > 0). -/
  71theorem exp_factor_bounded (hfg : 0 ≤ f_gap) :
  72    0 < Real.exp (-(f_gap / alpha_seed)) ∧ Real.exp (-(f_gap / alpha_seed)) ≤ 1 := by
  73  constructor
  74  · exact Real.exp_pos _
  75  · apply Real.exp_le_one_iff.mpr
  76    apply neg_nonpos_of_nonneg
  77    exact div_nonneg hfg (le_of_lt alpha_seed_positive)
  78
  79/-- The ratio alphaInv/alpha_seed equals the exponential factor. -/
  80theorem alphaInv_seed_ratio :
  81    alphaInv / alpha_seed = Real.exp (-(f_gap / alpha_seed)) := by
  82  unfold alphaInv
  83  field_simp
  84
  85/-! ## Part 2: The Logarithmic Structure
  86
  87Taking the natural log of α⁻¹/α_seed gives:
  88    ln(α⁻¹/α_seed) = -f_gap/α_seed
  89
  90This is the defining relation of the exponential form in log coordinates.
  91It says that the logarithm of the coupling ratio is LINEAR in f_gap with
  92slope -1/α_seed.
  93-/
  94
  95/-- The log of the ratio alphaInv/alpha_seed equals -f_gap/alpha_seed. -/
  96theorem log_alphaInv_seed_ratio :
  97    Real.log (alphaInv / alpha_seed) = -(f_gap / alpha_seed) := by
  98  rw [alphaInv_seed_ratio]
  99  exact Real.log_exp _
 100
 101/-- Equivalent: ln(α⁻¹) = ln(α_seed) - f_gap/α_seed. -/