Foundation Inequalities Am Gm Reciprocal

The reciprocal bound

The AM-GM inequality is a classical result: for any nonnegative numbers, the arithmetic mean is at least the geometric mean. Applied to a positive number x and its reciprocal 1/x, it yields x + 1/x ≥ 2, with equality exactly when x = 1. This is the statement of the framework's declaration am_gm_reciprocal.

In Recognition Science, this inequality is the foundation for the cost function J(x) = (x + 1/x)/2 - 1. The declaration proves that J(x) ≥ 0 for all x > 0, that it reaches its minimum value 0 at x = 1, and that it is strictly positive for any other positive x. The cost is never negative, and it is zero only when the two quantities being compared are equal.

The framework's machine-checked library of formal theorems records these results. The declarations am_gm_reciprocal, am_gm_reciprocal_eq, and am_gm_reciprocal_strict establish the inequality, its equality condition, and its strict version. From these, J_formula_nonneg, J_formula_min_at_one, and J_formula_pos derive the corresponding properties of the cost function.

The declaration also connects to the golden ratio φ, which satisfies φ + 1/φ = √5, so its cost is (√5 - 2)/2 ≈ 0.118. This is a concrete instance of the general bound.

What the declaration does not claim: it does not prove that this cost function is the only possible one, nor does it establish any physical law. It is a mathematical lemma about real numbers, not a statement about the world.

/-- The AM-GM inequality for x and 1/x: for all x > 0, x + 1/x ≥ 2.

    This is the fundamental inequality that forces J-cost ≥ 0.

    **Proof**: Use Mathlib's `add_div_two_ge_sqrt_mul_self_of_sq_le_sq` or direct algebra. -/
theorem am_gm_reciprocal {x : ℝ} (hx : x > 0) : x + 1/x ≥ 2 := by
  have h1 : x * (1/x) = 1 := by field_simp
  have h2 : (x - 1/x)^2 ≥ 0 := sq_nonneg _
  -- (x - 1/x)² = x² - 2 + 1/x²
  -- So x² + 1/x² ≥ 2
  -- We need: x + 1/x ≥ 2
  -- Use: (x + 1/x)² = x² + 2 + 1/x² ≥ 4, so x + 1/x ≥ 2 (since both positive)
  have hx_inv_pos : 1/x > 0 := by positivity
  have h_sum_pos : x + 1/x > 0 := by linarith
  -- Alternative: direct Mathlib lemma
  have h3 : x + 1/x = x + x⁻¹ := by rw [one_div]
  rw [h3]
  -- Use add_inv_le_iff or similar
  nlinarith [sq_nonneg (x - 1), sq_nonneg (x - x⁻¹), sq_nonneg x, sq_nonneg x⁻¹,
             mul_pos hx hx_inv_pos]

/-- Equality in AM-GM holds iff x = 1. -/
theorem am_gm_reciprocal_eq {x : ℝ} (hx : x > 0) : x + 1/x = 2 ↔ x = 1 := by
  constructor
  · intro h
    have h1 : (x - 1)^2 = x^2 - 2*x + 1 := by ring
    have h2 : x^2 + 1 = 2*x := by
      have hx_ne : x ≠ 0 := ne_of_gt hx
      field_simp at h
      linarith
    have h3 : (x - 1)^2 = 0 := by nlinarith [sq_nonneg x]
    have h4 : x - 1 = 0 := by
      rwa [sq_eq_zero_iff] at h3
    linarith
  · intro h
    rw [h]
    norm_num

/-- J-cost is non-negative: J(x) = (x + 1/x)/2 - 1 ≥ 0 for x > 0.

    This follows directly from AM-GM. -/
theorem J_formula_nonneg {x : ℝ} (hx : x > 0) : (x + 1/x) / 2 - 1 ≥ 0 := by
  have h := am_gm_reciprocal hx
  linarith

/-- J-cost achieves minimum 0 at x = 1. -/
theorem J_formula_min_at_one : (1 + 1/(1 : ℝ)) / 2 - 1 = 0 := by norm_num

/-- J-cost is strictly positive away from x = 1. -/
theorem J_formula_pos {x : ℝ} (hx : x > 0) (hne : x ≠ 1) : (x + 1/x) / 2 - 1 > 0 := by
  have h := am_gm_reciprocal_strict hx hne
  linarith

/-- φ + 1/φ = √5 -/
theorem phi_plus_inv : φ + 1/φ = Real.sqrt 5 := by
  unfold φ Constants.phi
  have hroot_pos : (0 : ℝ) < 5 := by norm_num
  have hroot_ne : Real.sqrt 5 + 1 ≠ 0 := by
    have := Real.sqrt_nonneg 5
    linarith
  field_simp
  ring_nf
  rw [Real.sq_sqrt (le_of_lt hroot_pos)]
  ring

/-- J-cost of φ -/
theorem J_cost_phi : (φ + 1/φ) / 2 - 1 = (Real.sqrt 5 - 2) / 2 := by
  rw [phi_plus_inv]
  ring

What this page does not claim

This declaration does not prove that J is the only possible cost function satisfying the framework's axioms. It does not establish any physical law or empirical prediction about the world. It does not derive the golden ratio as a consequence of the inequality.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/Inequalities.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: