alphaInv_seed_ratio

formal source

  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. -/
 102theorem log_alphaInv_eq :
 103    Real.log alphaInv = Real.log alpha_seed - f_gap / alpha_seed := by
 104  have h := log_alphaInv_seed_ratio
 105  rw [Real.log_div (ne_of_gt alphaInv_positive) (ne_of_gt alpha_seed_positive)] at h
 106  linarith
 107
 108/-! ## Part 3: The Differential Equation
 109
 110The exponential form α⁻¹ = α_seed · exp(-f_gap/α_seed) satisfies the ODE