Foundation Inequalities Am Gm Reciprocal Eq

The equality case

The arithmetic mean of a positive number and its reciprocal is always at least 1. For any x greater than 0, the inequality x + 1/x ≥ 2 holds, with equality precisely when x = 1. This is a special case of the classical AM-GM inequality, which states that the arithmetic mean of nonnegative numbers is at least their geometric mean; for two numbers x and 1/x, the geometric mean is 1, so the arithmetic mean (x + 1/x)/2 must be at least 1.

The equality condition is the part the framework's library pins down. The theorem am_gm_reciprocal_eq states that for x > 0, the equation x + 1/x = 2 holds if and only if x = 1. The proof is short: from the inequality, if the sum equals 2, then the arithmetic mean equals the geometric mean, which forces the two numbers to be equal, so x = 1/x, and with x positive this gives x = 1. The converse, that x = 1 gives the sum 2, is immediate arithmetic.

This equality case carries the framework's cost function. In Recognition Science, the cost of a recognition event, a discrete record of a comparison, is defined as J(x) = (x + 1/x)/2 − 1. The AM-GM inequality directly shows J(x) ≥ 0 for all positive x, and the equality case shows J(x) = 0 exactly when x = 1. The framework's library records this as a theorem: the cost is nonnegative, and its minimum value 0 occurs only at the unit ratio.

The strict version follows immediately. For any x > 0 with x ≠ 1, the sum x + 1/x is strictly greater than 2, so the cost J(x) is strictly positive. This gives the framework a clean statement: the cost of recognition is zero only when the two quantities being compared are equal, and any mismatch carries a positive cost. The golden ratio φ, which satisfies φ + 1/φ = √5, gives a cost of (√5 − 2)/2, a positive value the library computes explicitly.

What the declaration does not claim is just as precise. It does not say anything about the cost function's uniqueness, about why the cost takes this particular form, or about any physical interpretation of the cost. Those are separate theorems in the framework's chain. The declaration only establishes the algebraic fact about the sum of a positive number and its reciprocal, together with its equality case, and the immediate consequence for the cost's nonnegativity and minimum.

/-- 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

/-- Strengthened AM-GM: x + 1/x > 2 when x ≠ 1. -/
theorem am_gm_reciprocal_strict {x : ℝ} (hx : x > 0) (hne : x ≠ 1) : x + 1/x > 2 := by
  have h := am_gm_reciprocal hx
  have hne' : ¬(x + 1/x = 2) := by
    intro heq
    exact hne ((am_gm_reciprocal_eq hx).mp heq)
  exact lt_of_le_of_ne h (Ne.symm hne')

/-- 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

What this page does not claim

The declaration does not prove that the cost function must have the form J(x) = (x + 1/x)/2 − 1. The declaration does not assign any physical meaning to the cost or its minimum. The declaration does not address the uniqueness of the golden ratio as a scaling factor.

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: