Jcost_continuous_pos
plain-language theorem explainer
The lemma shows that the J-cost function remains continuous on the positive reals. Researchers proving uniqueness of cost functionals under the Recognition Composition Law cite it to secure the regularity hypothesis. The proof constructs this continuity explicitly by composing the identity, reciprocal, addition, constant scaling, and subtraction on the open interval (0, ∞).
Claim. The map $J : (0, ∞) → ℝ$ defined by $J(x) = (x + x^{-1})/2 - 1$ is continuous on $(0, ∞)$.
background
The CostUniqueness module consolidates results toward the main T5 uniqueness theorem: any cost functional satisfying symmetry, unit normalization, strict convexity, and calibration equals Jcost on positive reals. Jcost is the explicit functional $J(x) = (x + x^{-1})/2 - 1$ that obeys the Recognition Composition Law. Upstream results include the reciprocal automorphism and the arithmetic operations that define the algebraic structure of J.
proof idea
The tactic proof obtains continuity of the identity on (0, ∞), extends it to the reciprocal via ContinuousOn.inv₀, adds the maps, scales the sum by the constant 1/2, subtracts the constant 1, and applies simpa to match the definition of Jcost.
why it matters
This lemma supplies the continuity component of the RegularityCert for Jcost, which is required by the unconditional uniqueness theorem unique_cost_on_pos_from_rcl. It completes the regularity part of T5 J-uniqueness in the forcing chain, allowing the framework to identify J as the unique cost satisfying the RCL and calibration conditions on positive reals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.