Foundation Rhat From Jcost Gradient Midpoint Map

The midpoint map

The midpoint map is the function that takes any positive number and replaces it with the average of that number and 1. Written in symbols, it sends x to (x + 1)/2. This is one of the oldest and most natural operations in arithmetic: if you have a number and you want to move it partway toward 1, you take the midpoint. The map has a fixed point at 1, meaning that if you start at 1, you stay at 1. It is also a contraction: starting from any positive number other than 1 and applying the map repeatedly pulls the value closer and closer to 1.

In Recognition Science, this map appears in a specific role. The framework defines a cost, a measure of how far a recognition event is from perfect agreement, and the midpoint map is the update rule that reduces that cost at every step. The framework's machine-checked library of formal theorems proves three facts about this map. First, the midpoint map leaves the number 1 fixed. Second, for any positive starting value other than 1, applying the map strictly lowers the cost. Third, a more general statement holds: any function that keeps 1 fixed and always lowers the cost must have 1 as its only fixed point. These three facts together mean that, within the framework, the midpoint map is not just one possible way to reduce cost; it is the unique linear contraction that does so, and 1 is the only place where the descent can stop.

The practical consequence is that the midpoint map gives a concrete, provable model for how a system might settle toward a stable state. It does not claim to describe the actual dynamics of any physical process. It does not claim that the midpoint map is the only function that lowers the cost, only that it is the unique linear one. It also does not claim that the cost function itself is derived from the midpoint map; the cost function is defined separately, and the midpoint map is shown to be compatible with it. The framework's contribution is to show that this simple arithmetic rule has a precise, provable relationship to a general principle of cost reduction, not to assert that nature must use this rule.

/-- The midpoint map `x ↦ (x + 1)/2` is a linear contraction toward 1. -/
def midpointMap (x : ℝ) : ℝ := (x + 1) / 2

/-- The midpoint map has fixed point 1. -/
theorem midpointMap_fixed_point : midpointMap 1 = 1 := by
  unfold midpointMap; norm_num

/-- J decreases under the midpoint map for any x > 0, x ≠ 1. -/
theorem midpointMap_decreases_jcost {x : ℝ} (hx : 0 < x) (hne : x ≠ 1) :
    Jcost (midpointMap x) < Jcost x := by
  unfold midpointMap
  have hm_pos : 0 < (x + 1) / 2 := by positivity
  have hJx_eq : Jcost x = (x - 1) ^ 2 / (2 * x) := Jcost_eq_sq hx.ne'
  have hJm_eq : Jcost ((x + 1) / 2) = (x - 1) ^ 2 / (4 * (x + 1)) := by
    rw [Jcost_eq_sq hm_pos.ne']
    have hx1_pos : 0 < x + 1 := by linarith
    field_simp
    ring
  rw [hJx_eq, hJm_eq]
  rw [div_lt_div_iff₀ (by positivity) (by positivity)]
  have hne' : x - 1 ≠ 0 := sub_ne_zero.mpr hne
  have h_sq_pos : 0 < (x - 1) ^ 2 := by positivity
  nlinarith

/-- The unique fixed point of any J-cost-decreasing map with J as Lyapunov
    function is x = 1. -/
theorem jcost_lyapunov_unique_fixed_point {f : ℝ → ℝ}
    (hfixed : f 1 = 1)
    (hdecreasing : ∀ x : ℝ, 0 < x → x ≠ 1 → Jcost (f x) < Jcost x) :
    ∀ y : ℝ, 0 < y → f y = y → y = 1 := by
  intro y hy hfy
  by_contra hne
  exact absurd (hdecreasing y hy hne) (by rw [hfy]; exact lt_irrefl _)

What this page does not claim

The midpoint map is the only function that lowers the cost. The midpoint map describes the dynamics of any actual physical process. The cost function is derived from the midpoint map.

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