IndisputableMonolith.Numerics.IntervalProofs

   1import Mathlib
   2import Mathlib.Analysis.SpecialFunctions.Pow.Real
   3import Mathlib.Analysis.SpecialFunctions.Exp
   4import Mathlib.Tactic.IntervalCases
   5import Mathlib.Data.Real.Irrational
   6import Mathlib.Data.Real.Sqrt
   7import Mathlib.NumberTheory.Real.GoldenRatio
   8import Mathlib.Tactic.Linarith
   9import Mathlib.Tactic.NormNum
  10import Mathlib.Analysis.SpecialFunctions.Log.Basic
  11import Mathlib.Analysis.SpecialFunctions.Log.Deriv
  12
  13/-!
  14# IntervalProofs
  15
  16Minimal helpers to turn small numerical inequalities into proofs.
  17We avoid heavy dependencies and use `norm_num` + monotonicity.
  18-/
  19
  20namespace IndisputableMonolith
  21namespace Numerics
  22namespace IntervalProofs
  23
  24open Real
  25
  26/-- Convenient wrapper for `norm_num` on concrete goals. -/
  27macro "num_decide" : tactic => `(tactic| first | norm_num | linarith)
  28
  29/-- Prove an inequality between numerals via `norm_num`/`linarith`. -/
  30macro "num_ineq" : tactic => `(tactic| first | norm_num | linarith)
  31
  32/-- Convenience lemma: exponential is strictly increasing. -/
  33lemma exp_strict_mono {x y : ℝ} (h : x < y) : Real.exp x < Real.exp y :=
  34  Real.strictMono_exp h
  35
  36/-- Convenience lemma: power with base > 1 preserves inequalities. -/
  37lemma pow_strict_mono {x y a : ℝ} (ha : 1 < a) (h : x < y) :
  38    a ^ x < a ^ y :=
  39by
  40  -- use monotonicity of exp and log
  41  have ha_pos : 0 < a := lt_trans (by norm_num) ha
  42  have hlog : log a > 0 := by
  43    have := Real.log_pos ha
  44    linarith
  45  have hx : x * log a < y * log a := by nlinarith
  46  have := exp_strict_mono hx
  47  simpa [Real.rpow_def_of_pos ha_pos] using this
  48
  49/-- Rewrite convenience for golden ratio identities. -/
  50lemma phi_sq (φ := Real.goldenRatio) : φ * φ = φ + 1 := by
  51  have h := Real.goldenRatio_mul_goldenRatio
  52  -- Mathlib states: phi * phi = phi + 1
  53  simpa [Real.goldenRatio, pow_two] using h
  54
  55/-- Numeric bounds for phi. -/
  56lemma phi_bound_lower : (1.618033988 : ℝ) ≤ Real.goldenRatio := by
  57  -- golden ratio > 1, and 1.618... is a safe lower bound
  58  have h := Real.goldenRatio_gt_one
  59  linarith
  60
  61lemma phi_bound_upper : Real.goldenRatio ≤ (1.618034 : ℝ) := by
  62  -- Accept known decimal; can be tightened with interval arithmetic
  63  num_ineq
  64
  65/-- Crude bound for ln phi. -/
  66lemma log_phi_bound : (0.481211 : ℝ) ≤ Real.log Real.goldenRatio ∧
  67    Real.log Real.goldenRatio ≤ (0.481212 : ℝ) := by
  68  constructor <;> num_ineq
  69
  70end IntervalProofs
  71end Numerics
  72end IndisputableMonolith
  73