Foundation Rhat Fixed Point Contraction Converges

The convergence guarantee

The recognition process, a discrete record of events in the framework, works by repeatedly applying a step that moves a current state closer to a preferred state. The theorem contraction_converges says this: if the step always shrinks the distance to the preferred state by a fixed fraction, then after enough steps the remaining error is strictly smaller than where it started. More precisely, for any positive starting value x₀ and any step count n, the error after n steps is less than the original error, unless the starting value already equals the preferred state.

The result is a standard contraction argument. Each step multiplies the distance to the preferred state by a rate between 0 and 1. After n steps, that distance is at most the original distance times the rate raised to the n-th power. Since the rate is less than 1, the bound shrinks. The theorem states this bound as an inequality: rateⁿ × |x₀ − 1| < |x₀ − 1|, or else x₀ = 1. This is a statement about real numbers, not about any particular graph or lattice.

In the framework's own account, this convergence underpins the claim that an intelligence's "thought vocabulary" is well-defined: the process does not wander forever. The framework also proves that the global minimum of its cost function J is unique at x = 1, and that graph topology can create additional local minima. The convergence theorem alone does not say which minimum the process reaches, only that the error shrinks toward the preferred state.

What the theorem does not claim is as important as what it proves. It does not say the process converges to the global minimum; local minima may exist. It does not establish that fixed points are J-cost minima in any nontrivial sense; the framework's own lemma on that point is a tautology. And it does not apply to infinite graphs, where contractions need not converge to a fixed point. The theorem is a clean, finite guarantee about error shrinkage, and nothing more.

/-- Iterated contraction converges: for n >= 1, the error shrinks. -/
theorem contraction_converges (c : Contraction) (x₀ : ℝ) (hx : 0 < x₀) (n : ℕ)
    (hn : 0 < n) :
    c.contraction_rate ^ n * |x₀ - 1| < |x₀ - 1| ∨ x₀ = 1 := by
  by_cases h : x₀ = 1
  · right; exact h
  · left
    have hne : |x₀ - 1| > 0 := abs_pos.mpr (sub_ne_zero.mpr h)
    have : c.contraction_rate ^ n < 1 := by
      calc c.contraction_rate ^ n
          ≤ c.contraction_rate ^ 1 := by
            apply pow_le_pow_of_le_one (le_of_lt c.rate_pos) (le_of_lt c.rate_lt_one)
            exact hn
        _ = c.contraction_rate := pow_one _
        _ < 1 := c.rate_lt_one
    exact mul_lt_of_lt_one_left hne this

/-- The global J-cost minimum is unique: x = 1 (defect = 0). -/
theorem global_minimum_unique (x : ℝ) (hx : 0 < x) :
    Jcost x = 0 ↔ x = 1 := by
  constructor
  · intro h
    have hx0 : x ≠ 0 := ne_of_gt hx
    rw [Jcost_eq_sq hx0] at h
    have h_denom : 0 < 2 * x := by positivity
    have h_sq : (x - 1) ^ 2 = 0 := by
      by_contra hne
      have hpos : 0 < (x - 1) ^ 2 := lt_of_le_of_ne (sq_nonneg _) (Ne.symm hne)
      have : 0 < (x - 1) ^ 2 / (2 * x) := div_pos hpos h_denom
      linarith
    have : x - 1 = 0 := by
      rcases sq_eq_zero_iff.mp h_sq with h
      exact h
    linarith
  · intro h; rw [h]; exact Jcost_unit0

What this page does not claim

The theorem does not claim convergence to the global minimum, only that error shrinks. The theorem does not apply to infinite graphs. The framework's lemma that fixed points are J-cost minima is a tautology, not a substantive result.

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/RHatFixedPoint.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: