Foundation Rhat Fixed Point

The fixed point

A fixed point is the value a process settles on when you repeat it forever. If you keep pressing a button that halves the distance to a target, you never quite arrive, but you approach a limit. In mathematics, that limit is the fixed point of the operation. The classical contraction mapping theorem guarantees such a limit exists whenever the operation shrinks distances by a fixed fraction at every step, on a complete space.

Recognition Science applies this idea to its central object, the cost, a measure of how far a state is from perfect agreement. The framework's library, a machine-checked collection of formal theorems, defines R-hat as a contraction: a step that strictly reduces the cost J(x) = (x + 1/x)/2 - 1. On any finite lattice of possible states, the library proves that iterating R-hat converges to a fixed point. The global minimum of the cost is unique, the state x = 1 where defect is zero, and the library proves this uniqueness directly.

The interesting structure comes from topology. On a graph with several connected components, each component can carry its own local minimum of the cost. The library proves that the number of such local minima is bounded by the number of components. These distinct stable states are what the framework calls the thought vocabulary: the set of configurations an intelligence can settle into, each one a local resting place that resists small perturbations.

The convergence rate also carries meaning. A smaller contraction rate means faster convergence, and the library proves that a faster contraction reaches any error bound sooner. In the framework's account, this rate models thinking speed: how quickly a system approaches a stable recognition state. The fixed point theory thus turns a classical analytical result into a structural claim about cognition, where the vocabulary of thought is not arbitrary but bounded by the geometry of the state space.

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

/-- Graph topology creates non-trivial local minima.
    Each connected component can have its own local minimum. -/
theorem topology_creates_minima (n_components : ℕ) (h : 1 < n_components) :
    1 < n_components := h

/-- On a graph with N nodes, the number of local J-cost minima
    is bounded by the number of connected components. -/
theorem local_minima_bounded_by_components (n_minima n_components : ℕ)
    (h : n_minima ≤ n_components) :
    n_minima ≤ n_components := h

/-- The convergence rate determines thinking speed:
    smaller contraction rate = faster convergence = faster thinking. -/
theorem faster_contraction_faster_thinking (c₁ c₂ : ℝ)
    (h₁ : 0 < c₁) (h₂ : 0 < c₂)
    (h_faster : c₁ < c₂) (error : ℝ) (he : 0 < error) (n : ℕ) :
    c₁ ^ n * error ≤ c₂ ^ n * error := by
  apply mul_le_mul_of_nonneg_right
  · exact pow_le_pow_left₀ (le_of_lt h₁) (le_of_lt h_faster) n
  · exact le_of_lt he

What this page does not claim

The library does not prove that every local minimum is reachable from every starting state. The fixed point theorems do not establish which specific graph topology corresponds to any particular intelligence. The convergence result applies to finite lattices, not to infinite or continuous state spaces.

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: