midpointMap_decreases_jcost
plain-language theorem explainer
The midpoint map strictly decreases J-cost for every positive real x distinct from 1. Researchers modeling the recognition operator as gradient descent on the J-cost landscape cite this to confirm that the midpoint update serves as a strict Lyapunov function. The proof substitutes the squared expression for J-cost from the upstream lemma, clears the resulting rational inequality, and resolves it by nlinarith.
Claim. For every real number $x > 0$ with $x ≠ 1$, the J-cost satisfies $J((x + 1)/2) < J(x)$, where $J$ is the J-cost function.
background
J-cost is the function $J(x) = (x + x^{-1})/2 - 1$, equivalently expressed as $J(x) = (x-1)^2/(2x)$ for $x ≠ 0$ by the lemma Jcost_eq_sq. The midpoint map is the function sending $x$ to $(x + 1)/2$. This theorem belongs to the module on R̂ emergence from J-cost gradient, which formalizes the structural claim from the pre-Big-Bang paper §6 that the recognition operator is the unique cost-minimizing update rule with fixed point at unity. It relies on the squared-ratio expression of J-cost from upstream lemmas in the Cost module and on the definition of recognition events whose cost is J-cost.
proof idea
The tactic proof unfolds the midpoint map definition, invokes Jcost_eq_sq twice to replace both J-cost terms with squared-ratio expressions, rewrites using div_lt_div_iff after establishing positivity, and concludes the strict inequality with nlinarith using positivity of $(x-1)^2$ together with the assumption $x ≠ 1$.
why it matters
This supplies the strict decrease property assembled into the rHatEmergenceCert definition, which certifies that the recognition operator R̂ arises as the unique J-cost-decreasing map with fixed point at 1. It converts the scaffold annotation in the pre-Big-Bang paper §6 into proved status by establishing J as a Lyapunov function for the midpoint contraction, directly supporting the gradient flow uniqueness argument and connecting to the forcing chain fixed point at unity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.