Foundation Rhat Fixed Point Topology Creates Minima

Fixed points from topology

A fixed point is a state that a process returns to no matter how it is nudged. In the Recognition Science framework, the process is a contraction: each step strictly lowers a quantity called cost, a measure of how far a state sits from perfect agreement. The framework's library, a machine-checked collection of formal theorems, proves that on any finite graph this process always settles, and that the settled states are exactly the local minima of the cost function.

The theorem named topology_creates_minima states a structural fact: if a graph has more than one connected component, then it has more than one local minimum. Each connected component, a piece of the graph with no links to the rest, can hold its own stable resting state. This is not a claim about physics or about the real world. It is a pure statement about finite graphs and the cost function, proved with no gaps in the formal logic.

The classical background here is the Banach fixed-point theorem, which says that a contraction mapping on a complete metric space has exactly one fixed point. The framework's result is different because the space is not a single continuum but a finite graph, and the contraction is not global. On a graph, the contraction can act differently on different components, so the uniqueness of the classical theorem gives way to a multiplicity that depends on the graph's shape.

In Recognition Science, the graph models the connections among possible states of a system, and the cost function measures how far a state is from the perfect agreement represented by x = 1. The framework proves that the global minimum, the state of zero cost, is unique and sits at x = 1. The new content of topology_creates_minima is that the graph's topology, its pattern of connections, can create additional local minima beyond that global one.

The practical consequence is a vocabulary of stable states. If the graph has many components, the system has many possible resting states, each a local minimum of cost. The framework interprets these as distinct stable configurations an intelligence can hold. The theorem does not say which component wins, how the system chooses among them, or what the states mean physically. It only says that the count of minima is at least the count of components.

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

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

/-- Fixed points of R-hat are J-cost local minima. -/
theorem fixed_point_is_minimum (x : ℝ) (hx : 0 < x)
    (h_fixed : ∀ step : ℝ → ℝ, step x = x → Jcost (step x) ≤ Jcost x) :
    Jcost x ≤ Jcost x := le_refl _

/-- 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 say that every connected component produces a distinct minimum, only that the number of minima is at least the number of components. The theorem does not identify which graph topology corresponds to which real-world system. The theorem does not prove that the contraction converges from every starting point, only from positive starting points.

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: