midpointMap
The midpoint map sends each real x to (x + 1)/2 and functions as the explicit linear contraction toward the fixed point at 1 on the J-cost landscape. Researchers formalizing the pre-Big-Bang emergence of the recognition operator R̂ cite this definition when establishing that J-cost serves as a strict Lyapunov function for gradient flow. The declaration is introduced as a direct algebraic expression with no lemmas or proof steps.
claimThe midpoint map is the function $m : ℝ → ℝ$ defined by $m(x) = (x + 1)/2$.
background
The module formalizes the structural claim from pre-Big-Bang paper §6 that the recognition operator R̂ emerges as the unique J-cost-minimizing update rule. J-cost is the function on positive reals whose value at x is (x - 1)^2 / (2x) and which attains its global minimum at x = 1. The midpoint map is the linear contraction that decreases this cost at every step away from 1 while fixing the point 1.
proof idea
This is a direct definition consisting of a single arithmetic expression. No lemmas are applied and no tactics are used.
why it matters in Recognition Science
The definition supplies the concrete map used by midpointMap_fixed_point and midpointMap_decreases_jcost, which in turn populate the RHatEmergenceCert structure. That structure certifies R̂ as the unique J-decreasing map with fixed point 1, converting the SCAFFOLD annotation in pre-Big-Bang §6 into theorem status. It realizes the gradient-flow uniqueness required by the J-uniqueness step (T5) of the forcing chain.
scope and limits
- Does not prove that the midpoint map is the only possible J-cost-decreasing contraction.
- Does not address nonlinear maps or maps on domains other than the positive reals.
- Does not derive the contraction rate away from the fixed point.
Lean usage
theorem midpoint_example : midpointMap 3 = 2 := by unfold midpointMap; norm_numformal statement (Lean)
40def midpointMap (x : ℝ) : ℝ := (x + 1) / 2
proof body
Definition body.
41
42/-- The midpoint map has fixed point 1. -/