pith. machine review for the scientific record. sign in
theorem scaffolding sorry stub

omega_lambda_lt_11_16

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  34theorem omega_lambda_lt_11_16 : 11/16 - (alpha / Real.pi) < 11/16 := by

proof body

Body contains sorry. Scaffold only; not proved.

  35  have h1 : alpha / Real.pi > 0 := by
  36    have ha : alpha > 0 := by
  37      unfold alpha
  38      have h2 : alphaInv > 0 := by unfold alphaInv alpha_seed; positivity
  39      positivity
  40    have hp : Real.pi > 0 := Real.pi_pos
  41    positivity
  42  linarith
  43
  44/-- Key structural lemma: alphaInv ≥ alpha_seed - f_gap > 2.
  45
  46    This follows from:
  47    1. exp(-t) ≥ 1 - t (standard inequality)
  48    2. alphaInv = alpha_seed * exp(-t) ≥ alpha_seed - f_gap
  49    3. alpha_seed - f_gap > 2 (numerical: ~135 - 1.2 ≈ 133.8 > 2)
  50
  51    The single sorry is for the numerical bound f_gap < alpha_seed - 2.
  52    This is clear from f_gap ≈ 1.197 and alpha_seed ≈ 137, but requires
  53    interval arithmetic infrastructure to prove rigorously in Lean. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (16)

Lean names referenced from this declaration's body.