Foundation Inequalities J Formula Pos

The positivity bound

The arithmetic mean of a positive number and its reciprocal is always at least 1. This is the AM-GM inequality, known since the nineteenth century, and it has a sharp edge: the mean equals 1 only when the number itself is 1. For any other positive number, the mean is strictly larger than 1.

The Recognition Science framework builds its cost function from this same pair. Its cost, a measure of how expensive a recognition event is, takes the form J(x) = (x + 1/x)/2 - 1 for a positive ratio x. The AM-GM inequality immediately gives J(x) ≥ 0, with equality exactly at x = 1. The framework's machine-checked library of formal theorems records this as the declaration J_formula_pos: for all positive x with x ≠ 1, J(x) > 0. The proof is a direct application of the strict AM-GM inequality, followed by a linear arithmetic step.

The content of J_formula_pos is therefore a positivity bound, not a claim about physics. It says the cost function is strictly positive whenever the ratio x is not 1, and it says nothing about what x represents or why that ratio matters. The declaration is one small lemma in a larger chain; its role is to guarantee that the cost function has a unique minimum at x = 1 and is strictly increasing as x moves away from 1 in either direction.

In Recognition Science, this bound supports the uniqueness of the golden ratio as the self-similar scaling. The golden ratio φ satisfies φ + 1/φ = √5, and the framework proves that J(φ) = (√5 - 2)/2, a positive number. The positivity lemma ensures that no other positive ratio achieves the minimum cost, clearing the path for φ to be the unique minimizer in the framework's derivation. The bound itself, however, is purely mathematical: it is a theorem about real numbers, proved without any physics assumptions.

What J_formula_pos does not claim is equally precise. It does not assert that the cost function is the only possible cost function, nor that the golden ratio is the only self-similar scaling in general mathematics. It does not claim that x = 1 is the only point where J is zero; that is a separate statement, J_formula_min_at_one, which says the minimum value is 0 at x = 1. The positivity bound is a lemma about a specific formula, and its proof is complete within the framework's library.

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

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

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

What this page does not claim

J_formula_pos does not assert that the cost function is the only possible cost function. The positivity bound does not claim that x = 1 is the only point where J is zero; that is a separate statement. The declaration does not claim anything about what x represents physically.

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: