`phi_ne_zero`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Constants on GitHub at line 40.

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

  37  simpa [phi] using hone_lt
  38
  39lemma phi_ge_one : 1 ≤ phi := le_of_lt one_lt_phi
  40lemma phi_ne_zero : phi ≠ 0 := ne_of_gt phi_pos
  41lemma phi_ne_one : phi ≠ 1 := ne_of_gt one_lt_phi
  42
  43lemma phi_lt_two : phi < 2 := by
  44  have hsqrt5_lt : Real.sqrt 5 < 3 := by
  45    have h5_lt_9 : (5 : ℝ) < 9 := by norm_num
  46    have h9_eq : Real.sqrt 9 = 3 := by
  47      rw [show (9 : ℝ) = 3^2 by norm_num, Real.sqrt_sq (by norm_num : (3 : ℝ) ≥ 0)]
  48    have : Real.sqrt 5 < Real.sqrt 9 := Real.sqrt_lt_sqrt (by norm_num) h5_lt_9
  49    rwa [h9_eq] at this
  50  have hnum_lt : 1 + Real.sqrt 5 < 4 := by linarith
  51  have : (1 + Real.sqrt 5) / 2 < 4 / 2 := div_lt_div_of_pos_right hnum_lt (by norm_num)
  52  simp only [phi]
  53  linarith
  54
  55/-! ### φ irrationality -/
  56
  57/-- φ is irrational (degree 2 algebraic, not rational).
  58
  59    Proof: Our φ equals Mathlib's golden ratio, which is proven irrational
  60    via the irrationality of √5 (5 is prime, hence not a perfect square). -/
  61theorem phi_irrational : Irrational phi := by
  62  -- Our phi equals Mathlib's goldenRatio
  63  have h_eq : phi = Real.goldenRatio := rfl
  64  rw [h_eq]
  65  exact Real.goldenRatio_irrational
  66
  67/-! ### φ power bounds -/
  68
  69/-- Key identity: φ² = φ + 1 (from the defining equation x² - x - 1 = 0). -/
  70lemma phi_sq_eq : phi^2 = phi + 1 := by

papers checked against this theorem

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