Foundation Rhat From Jcost Gradient Midpoint Map Fixed Point

The midpoint map's fixed point

The midpoint map is the rule that takes any positive number and replaces it with the average of that number and 1. Written in symbols, the rule is x ↦ (x + 1)/2. If you start with 3, the map sends it to 2; then 2 goes to 1.5; then 1.5 goes to 1.25; and so on, each step halving the distance to 1. The single number that the map leaves unchanged is 1 itself, because (1 + 1)/2 = 1. This is the fixed point of the map.

The declaration midpointMap_fixed_point establishes this fact as a theorem in the framework's machine-checked library of formal theorems: applying the midpoint map to 1 returns 1. The proof is immediate from the definition and the arithmetic of real numbers. The theorem is part of a larger structural claim about how the recognition operator, the framework's term for the update rule that reduces recognition cost, emerges from gradient descent on the cost function J. The surrounding theorems show that J strictly decreases under the midpoint map for every positive input other than 1, and that any map which decreases J and fixes 1 must have 1 as its unique fixed point on positive inputs.

What the theorem does not claim is broader. It does not assert that the midpoint map is the only map that decreases J; the uniqueness result applies to maps that also fix 1, and the midpoint map is one example, not the whole class. It does not claim that starting from any positive number, repeated application of the midpoint map reaches 1 in finitely many steps; the map approaches 1 asymptotically, never landing on it except from 1 itself. It does not claim that the midpoint map is the recognition operator; it is a concrete instance that satisfies the structural conditions, and the framework's certificate bundles the fixed-point, decrease, and uniqueness facts together as evidence for that identification.

/-- 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 not asserted to be the only J-decreasing map. Repeated midpoint application does not reach 1 in finitely many steps from any positive start. The midpoint map is not claimed to be identical to the recognition operator, only an instance satisfying its structural conditions.

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: