IndisputableMonolith.Foundation.Inequalities

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Inequalities — Fundamental Mathematical Lemmas
   6-/
   7
   8namespace IndisputableMonolith
   9namespace Foundation
  10namespace Inequalities
  11
  12open Constants
  13
  14/-! ## AM-GM Inequality for Reciprocals -/
  15
  16/-- The AM-GM inequality for x and 1/x: for all x > 0, x + 1/x ≥ 2.
  17
  18    This is the fundamental inequality that forces J-cost ≥ 0.
  19
  20    **Proof**: Use Mathlib's `add_div_two_ge_sqrt_mul_self_of_sq_le_sq` or direct algebra. -/
  21theorem am_gm_reciprocal {x : ℝ} (hx : x > 0) : x + 1/x ≥ 2 := by
  22  have h1 : x * (1/x) = 1 := by field_simp
  23  have h2 : (x - 1/x)^2 ≥ 0 := sq_nonneg _
  24  -- (x - 1/x)² = x² - 2 + 1/x²
  25  -- So x² + 1/x² ≥ 2
  26  -- We need: x + 1/x ≥ 2
  27  -- Use: (x + 1/x)² = x² + 2 + 1/x² ≥ 4, so x + 1/x ≥ 2 (since both positive)
  28  have hx_inv_pos : 1/x > 0 := by positivity
  29  have h_sum_pos : x + 1/x > 0 := by linarith
  30  -- Alternative: direct Mathlib lemma
  31  have h3 : x + 1/x = x + x⁻¹ := by rw [one_div]
  32  rw [h3]
  33  -- Use add_inv_le_iff or similar
  34  nlinarith [sq_nonneg (x - 1), sq_nonneg (x - x⁻¹), sq_nonneg x, sq_nonneg x⁻¹,
  35             mul_pos hx hx_inv_pos]
  36
  37/-- Equality in AM-GM holds iff x = 1. -/
  38theorem am_gm_reciprocal_eq {x : ℝ} (hx : x > 0) : x + 1/x = 2 ↔ x = 1 := by
  39  constructor
  40  · intro h
  41    have h1 : (x - 1)^2 = x^2 - 2*x + 1 := by ring
  42    have h2 : x^2 + 1 = 2*x := by
  43      have hx_ne : x ≠ 0 := ne_of_gt hx
  44      field_simp at h
  45      linarith
  46    have h3 : (x - 1)^2 = 0 := by nlinarith [sq_nonneg x]
  47    have h4 : x - 1 = 0 := by
  48      rwa [sq_eq_zero_iff] at h3
  49    linarith
  50  · intro h
  51    rw [h]
  52    norm_num
  53
  54/-- Strengthened AM-GM: x + 1/x > 2 when x ≠ 1. -/
  55theorem am_gm_reciprocal_strict {x : ℝ} (hx : x > 0) (hne : x ≠ 1) : x + 1/x > 2 := by
  56  have h := am_gm_reciprocal hx
  57  have hne' : ¬(x + 1/x = 2) := by
  58    intro heq
  59    exact hne ((am_gm_reciprocal_eq hx).mp heq)
  60  exact lt_of_le_of_ne h (Ne.symm hne')
  61
  62/-! ## J-cost Derived Bounds -/
  63
  64/-- J-cost is non-negative: J(x) = (x + 1/x)/2 - 1 ≥ 0 for x > 0.
  65
  66    This follows directly from AM-GM. -/
  67theorem J_formula_nonneg {x : ℝ} (hx : x > 0) : (x + 1/x) / 2 - 1 ≥ 0 := by
  68  have h := am_gm_reciprocal hx
  69  linarith
  70
  71/-- J-cost achieves minimum 0 at x = 1. -/
  72theorem J_formula_min_at_one : (1 + 1/(1 : ℝ)) / 2 - 1 = 0 := by norm_num
  73
  74/-- J-cost is strictly positive away from x = 1. -/
  75theorem J_formula_pos {x : ℝ} (hx : x > 0) (hne : x ≠ 1) : (x + 1/x) / 2 - 1 > 0 := by
  76  have h := am_gm_reciprocal_strict hx hne
  77  linarith
  78
  79/-! ## Golden Ratio Properties -/
  80
  81/-- Re-export phi for local convenience. -/
  82noncomputable abbrev φ : ℝ := Constants.phi
  83
  84/-- φ is positive -/
  85theorem phi_pos : φ > 0 := Constants.phi_pos
  86
  87/-- φ > 1 -/
  88theorem phi_gt_one : φ > 1 := Constants.one_lt_phi
  89
  90/-- 1/φ = φ - 1 (the golden ratio property) -/
  91theorem phi_inv : 1 / φ = φ - 1 := by
  92  have hsq : φ ^ 2 = φ + 1 := Constants.phi_sq_eq
  93  have hpos : 0 < φ := Constants.phi_pos
  94  have hne : φ ≠ 0 := hpos.ne'
  95  have hmul : φ * (φ - 1) = 1 := by
  96    calc
  97      φ * (φ - 1) = φ ^ 2 - φ := by ring
  98      _ = (φ + 1) - φ := by simp [hsq]
  99      _ = 1 := by ring
 100  have hdiv : φ - 1 = 1 / φ := by
 101    apply (eq_div_iff hne).2
 102    simpa [mul_comm, mul_left_comm, mul_assoc] using hmul
 103  exact hdiv.symm
 104
 105/-- φ² = φ + 1 (the defining equation) -/
 106theorem phi_sq : φ^2 = φ + 1 := Constants.phi_sq_eq
 107
 108/-- φ + 1/φ = √5 -/
 109theorem phi_plus_inv : φ + 1/φ = Real.sqrt 5 := by
 110  unfold φ Constants.phi
 111  have hroot_pos : (0 : ℝ) < 5 := by norm_num
 112  have hroot_ne : Real.sqrt 5 + 1 ≠ 0 := by
 113    have := Real.sqrt_nonneg 5
 114    linarith
 115  field_simp
 116  ring_nf
 117  rw [Real.sq_sqrt (le_of_lt hroot_pos)]
 118  ring
 119
 120/-- J-cost of φ -/
 121theorem J_cost_phi : (φ + 1/φ) / 2 - 1 = (Real.sqrt 5 - 2) / 2 := by
 122  rw [phi_plus_inv]
 123  ring
 124
 125end Inequalities
 126end Foundation
 127end IndisputableMonolith
 128