`isw_driver_positive`

proved

show as: view math explainer →

module: IndisputableMonolith.ILG.ISWSign
domain: ILG
line: 68 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.ILG.ISWSign on GitHub at line 68.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  65    · repeat apply mul_nonneg <;> (try exact le_of_lt hC) <;> (try exact le_of_lt hXinv_pow)
  66
  67/-- Main Theorem (Target E): The ISW driver B(a,k) is strictly positive in ILG baseline. -/
  68theorem isw_driver_positive (P : KernelParams) (k a : ℝ) (ha : 0 < a) (hk : 0 < k)
  69    (halpha : 0 < P.alpha) (hC : 0 < P.C) :
  70    0 < isw_driver P k a := by
  71  unfold isw_driver
  72  have hf := f_growth_gt_one P k a ha hk halpha hC
  73  have hd := dlnw_pos P k a ha hk halpha hC
  74  linarith
  75
  76end ILG
  77end IndisputableMonolith

papers checked against this theorem

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