`alphaInv_positive`

proved

show as: view math explainer →

module: IndisputableMonolith.Constants.AlphaExponentialForm
domain: Constants
line: 66 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Constants.AlphaExponentialForm on GitHub at line 66.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  63  linarith
  64
  65/-- The exponential formula produces a positive value. -/
  66theorem alphaInv_positive : 0 < alphaInv := by
  67  unfold alphaInv
  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 :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.