Foundation Rhat From Jcost Gradient Midpoint Map Decreases Jcost

The midpoint step

The midpoint map is the rule that replaces any positive number x by the average of x and 1, written (x + 1)/2. Applied once, it moves x halfway toward 1. Applied again, it moves the result halfway again, and so on. The sequence 2, 1.5, 1.25, 1.125 approaches 1 without ever overshooting. This is the simplest possible contraction toward a fixed point, and it has a classical pedigree: it is the arithmetic mean of a number and its target.

The Recognition Science framework attaches a cost to each positive number x, written J(x), which measures how far x sits from the balanced value 1. The framework proves that J is uniquely forced by five plain conditions, and its formula is J(x) = (x + 1/x)/2 - 1. This cost is zero exactly at x = 1 and positive everywhere else. The midpoint map, it turns out, always reduces this cost. The theorem midpointMap_decreases_jcost states it precisely: for any positive x that is not 1, the cost of (x + 1)/2 is strictly less than the cost of x. The framework's machine-checked library of formal theorems verifies this inequality with no unproved assumptions.

This single fact does real work. Because the midpoint map lowers the cost at every step, the cost acts as a Lyapunov function: a quantity that strictly decreases along the dynamics and therefore guarantees the dynamics settles somewhere. The framework proves a stronger structural claim: any smooth update rule that (i) lowers J at every step and (ii) has a fixed point exactly at x = 1 must be a contraction toward 1, and the unique linear contraction with J as its Lyapunov function is the midpoint map itself. This is the formal content of the pre-Big-Bang paper's section 6, which argued that the recognition operator emerges as gradient-descent on the J-cost surface. The framework's library upgrades that annotation to a proved theorem.

What the declaration does not claim is equally important. It does not say that the midpoint map is the only map that decreases J; the uniqueness theorem concerns linear contractions, and other nonlinear maps could also lower the cost. It does not say that starting from any positive number, repeated midpoint steps reach 1 in finite time; the approach is asymptotic, not exact. And it does not claim that the midpoint map is the recognition operator itself. The recognition operator is a separate object, and the certificate structure in the library assembles these three facts as evidence that the operator emerges from the cost dynamics, not as a definition of it.

/-- 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 map that decreases J-cost. Repeated midpoint steps reach the fixed point in finite time. The midpoint map is identical to the recognition operator.

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: