Jcost_continuous_pos
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, ∞).
claimThe 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 in Recognition Science
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.
scope and limits
- Does not establish continuity at zero or on non-positive reals.
- Does not derive differentiability or higher regularity.
- Does not replace convexity or calibration in uniqueness arguments.
- Does not address discrete or multidimensional extensions.
formal statement (Lean)
130lemma Jcost_continuous_pos : ContinuousOn Jcost (Ioi 0) := by
proof body
Tactic-mode proof.
131 classical
132 have h1 : ContinuousOn (fun x : ℝ => x) (Ioi 0) := continuousOn_id
133 have h2 : ContinuousOn (fun x : ℝ => x⁻¹) (Ioi 0) := by
134 refine ContinuousOn.inv₀ (f:=fun x : ℝ => x) (s:=Ioi 0) h1 ?hneq
135 intro x hx; exact ne_of_gt hx
136 have h3 : ContinuousOn (fun x : ℝ => x + x⁻¹) (Ioi 0) := h1.add h2
137 have h4 : ContinuousOn (fun x : ℝ => (1 / 2 : ℝ) * (x + x⁻¹)) (Ioi 0) :=
138 (continuousOn_const).mul h3
139 have h5 : ContinuousOn (fun x : ℝ => (1 / 2 : ℝ) * (x + x⁻¹) - 1) (Ioi 0) :=
140 h4.sub continuousOn_const
141 simpa [Jcost, one_div, div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc, sub_eq_add_neg]
142 using h5
143
144/-- `Jcost` satisfies reciprocal symmetry in the theorem-surface format. -/