Foundation Inequalities

The inequalities behind the cost

The classical AM-GM inequality states that for any positive number x, the sum of x and its reciprocal is at least 2: x + 1/x ≥ 2. Equality holds only when x equals 1. This is a standard result in algebra, taught wherever means are compared. Its proof is a matter of expanding (x - 1)² ≥ 0.

The framework's ledger, a discrete record of recognition events, assigns a cost to each event. The cost function, written J(x), is defined as (x + 1/x)/2 - 1. The AM-GM inequality immediately shows this cost is never negative: since x + 1/x is at least 2, the expression (x + 1/x)/2 - 1 is at least 0. The cost reaches its minimum value of zero only when x = 1, and it is strictly positive for any other positive x.

This library of formal theorems proves these facts. It establishes that the cost is non-negative, that its minimum is zero at x = 1, and that it is strictly positive elsewhere. These are the foundational inequalities from which the framework's later results, including the golden ratio and the forcing chain, are built.

The library also records standard properties of the golden ratio φ, which satisfies φ² = φ + 1 and 1/φ = φ - 1. It proves that φ + 1/φ = √5, and consequently that the cost of φ is (√5 - 2)/2. This connects the classical constant to the framework's cost function.

In plain terms, the library guarantees that the framework's cost function behaves sensibly: it never goes negative, it has a unique minimum, and it penalizes any departure from that minimum. These inequalities are the groundwork for the framework's claim that cost is forced, not chosen.

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

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

What this page does not claim

This library does not prove the uniqueness of the cost function J. This library does not derive the golden ratio as the self-similar scaling; it only records its algebraic properties. This library does not establish any physical constants or empirical predictions.

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: