jcost_lyapunov_unique_fixed_point
plain-language theorem explainer
Any map f from the positive reals to the reals that fixes 1 and strictly decreases J-cost away from 1 has 1 as its sole fixed point. Pre-Big-Bang modelers constructing the recognition operator as gradient flow on the J-cost landscape cite the result for uniqueness. The term proof assumes a second fixed point y, applies the decrease hypothesis to reach Jcost y < Jcost y, and obtains an immediate contradiction from order irreflexivity.
Claim. Let $J$ denote the J-cost function. Suppose $f : ℝ → ℝ$ satisfies $f(1) = 1$ and $J(f(x)) < J(x)$ for every $x > 0$ with $x ≠ 1$. Then $f(y) = y$ and $y > 0$ together imply $y = 1$.
background
The module formalizes the emergence of the recognition operator R̂ as the unique cost-minimizing update on the J-cost landscape, following the argument of pre-Big-Bang §6. J-cost is the Lyapunov function attached to the recognition composition law, with the midpoint map serving as the canonical example that decreases J-cost while fixing 1. The upstream lemma lt_irrefl records that no element satisfies n < n under the order relation induced from LogicNat.
proof idea
The proof is a direct term-mode contradiction. It assumes a positive fixed point y ≠ 1, feeds the assumption into the decrease hypothesis to produce Jcost y < Jcost y, and discharges the absurdity by rewriting the fixed-point equation and invoking lt_irrefl.
why it matters
The theorem supplies the lyapunov_unique clause inside the downstream certificate rHatEmergenceCert, which assembles the fixed-point and decrease properties of the midpoint map. It converts the SCAFFOLD annotation of pre-Big-Bang §6 into proved status, anchoring the claim that R̂ is the sole J-cost gradient flow with fixed point at 1. The result sits after J-uniqueness in the forcing chain and before the emergence of spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.