midpointMap_fixed_point
The midpoint map, given by averaging its argument with 1, fixes the value 1. Researchers formalizing J-cost gradient descent for recognition-operator emergence cite this fixed-point fact to anchor the attractor. The proof is a one-line wrapper that unfolds the map definition and simplifies the resulting arithmetic.
claimLet $m(x) = (x + 1)/2$. Then $m(1) = 1$.
background
The midpoint map is the explicit linear contraction $m(x) := (x + 1)/2$ toward 1. This module converts the pre-Big-Bang §6 scaffold into theorems by showing that any smooth map decreasing J-cost and fixing a point must contract toward 1, with the midpoint map supplying the canonical example. The upstream definition states that the midpoint map is a linear contraction toward 1.
proof idea
The proof is a one-line wrapper that unfolds the midpoint map definition and applies numerical normalization to verify the equality at 1.
why it matters in Recognition Science
This fixed-point result populates the midpoint_fixed field of the R̂ emergence certificate, which records the structural properties required for the recognition operator to arise as the unique J-cost-minimizing update. It completes one of the three key facts listed in the module doc-comment, advancing the conversion of the §6 SCAFFOLD tag to theorem status. The certificate also draws on the J-cost decrease and Lyapunov uniqueness lemmas proved in the same file.
scope and limits
- Does not prove that J-cost decreases under the midpoint map.
- Does not establish uniqueness of the fixed point at 1.
- Does not derive the contraction coefficient from the first-order Taylor expansion of J.
formal statement (Lean)
43theorem midpointMap_fixed_point : midpointMap 1 = 1 := by
proof body
Term-mode proof.
44 unfold midpointMap; norm_num
45
46/-- J decreases under the midpoint map for any x > 0, x ≠ 1. -/