`phi_pow_102_interval`

definition

show as: view math explainer →

module: IndisputableMonolith.Numerics.Interval.GalacticBounds
domain: Numerics
line: 18 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Numerics.Interval.GalacticBounds on GitHub at line 18.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  15  unfold phi_pow_51_interval; norm_num
  16
  17/-- Interval for φ^102 = (φ^51)^2 -/
  18def phi_pow_102_interval : Interval :=
  19  mulPos phi_pow_51_interval phi_pow_51_interval phi_pow_51_lo_pos phi_pow_51_lo_pos
  20
  21/-- φ^16 lo > 0 -/
  22lemma phi_pow_16_lo_pos : (0 : ℚ) < phi_pow_16_interval.lo := by
  23  unfold phi_pow_16_interval; norm_num
  24
  25/-- φ^5 lo > 0 -/
  26lemma phi_pow_5_lo_pos : (0 : ℚ) < phi_pow_5_interval.lo := by
  27  unfold phi_pow_5_interval; norm_num
  28
  29/-- φ lo > 0 -/
  30lemma phi_lo_pos : (0 : ℚ) < phiInterval.lo := by
  31  unfold phiInterval; norm_num
  32
  33/-- Interval for φ^32 = (φ^16)^2 -/
  34def phi_pow_32_interval : Interval :=
  35  mulPos phi_pow_16_interval phi_pow_16_interval phi_pow_16_lo_pos phi_pow_16_lo_pos
  36
  37lemma phi_pow_32_lo_pos : (0 : ℚ) < phi_pow_32_interval.lo := by
  38  unfold phi_pow_32_interval mulPos; dsimp
  39  exact mul_pos phi_pow_16_lo_pos phi_pow_16_lo_pos
  40
  41/-- Interval for φ^37 = φ^32 * φ^5 -/
  42def phi_pow_37_interval : Interval :=
  43  mulPos phi_pow_32_interval phi_pow_5_interval phi_pow_32_lo_pos phi_pow_5_lo_pos
  44
  45lemma phi_pow_37_lo_pos : (0 : ℚ) < phi_pow_37_interval.lo := by
  46  unfold phi_pow_37_interval mulPos; dsimp
  47  exact mul_pos phi_pow_32_lo_pos phi_pow_5_lo_pos
  48

papers checked against this theorem

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