Foundation Rhat Fixed Point Fixed Point Is Minimum

A fixed point and its cost

A fixed point of a map is an input the map sends to itself. If a process shrinks distances at every step, a theorem of analysis guarantees that repeated application drives any starting value toward a fixed point. The framework's machine-checked library of formal theorems proves this for a specific family of shrinking maps on positive real numbers: each step moves the current value closer to 1, and the error shrinks by a fixed factor less than 1 each time.

The framework also attaches a cost to each positive number. This cost, written J(x), measures how far the number sits from 1, the state of zero defect. The global minimum of this cost is unique: J(x) = 0 exactly when x = 1, and no other positive number achieves zero cost. That uniqueness is a proved theorem in the library.

In Recognition Science, the framework models a ledger, a discrete record of recognition events, and the cost is forced by five plain conditions rather than chosen freely. Within this account, a fixed point of the shrinking map is a state the process does not change, and the framework's declaration fixed_point_is_minimum states that such a fixed point is a local minimum of the cost. The statement is true, but it is true in a thin sense: the theorem's hypothesis already assumes that every step leaves the cost no higher, and the conclusion simply repeats that the cost at the fixed point is no greater than itself.

The declaration does not claim that every fixed point is a global minimum, nor that the cost decreases along every possible path. It does not claim that the shrinking map exists for every graph or that the fixed point is unique. Those are separate results in the library: the global minimum is unique, and graph topology can create multiple local minima, one per connected component. The fixed-point result is a local statement about a single state under a single map, and it earns its place by being part of a larger chain that ties contraction, cost, and graph structure together.

What the result changes is the picture of how a recognition process can settle. A process that shrinks distances will stop at a fixed point, and at that stopping place the cost is at a local floor. The uniqueness of the global floor at x = 1 gives the process a single deepest resting state, while the topology of the graph can supply other, shallower resting states. The fixed-point theorem is the hinge: it says the places where the process can stop are exactly the places where the cost is locally minimal.

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

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

What this page does not claim

The theorem does not claim that every fixed point is a global minimum. The theorem does not claim that the cost decreases along every possible path, only along steps of the shrinking map. The theorem does not claim that the shrinking map exists for every graph or that fixed points are unique.

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: