Jcost_regularity_cert
plain-language theorem explainer
Jcost meets the three regularity conditions of the ClosedObservableFramework: continuity on (0,∞), strict convexity on (0,∞), and unit calibration of its second log-derivative at zero. Researchers proving the T5 uniqueness theorem for cost functionals would cite this certificate to discharge the regularity obligations. The definition is a direct record construction that assembles three separate lemmas, one for each field.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$. Then $J$ is continuous on $(0,∞)$, strictly convex on $(0,∞)$, and satisfies $d^2/dt^2 [J(e^t)]_{t=0} = 1$.
background
The CostUniqueness module consolidates results toward the main T5 uniqueness theorem: any cost functional satisfying symmetry, unit normalization, strict convexity, and calibration must coincide with Jcost on positive reals. Jcost is the explicit function $J(x) = (x + x^{-1})/2 - 1$ that satisfies the Recognition Composition Law with the required normalization. The RegularityCert structure from ClosedObservableFramework is a record bundling exactly three obligations: continuity on the positive reals, strict convexity on the positive reals, and the calibration condition that the second derivative of the composition with the exponential equals 1 at the origin.
proof idea
The definition constructs the RegularityCert record by direct field assignment. It sets the continuous field to the lemma Jcost_continuous_pos, the strict_convex field to the theorem Jcost_strictConvexOn_pos, and the calibration field to the lemma Jcost_log_second_deriv_normalized from LawOfExistence. No additional tactics are required beyond the record syntax.
why it matters
This certificate supplies the regularity assumptions required by the T5 uniqueness theorem in the same module, which asserts that Jcost is the only cost functional meeting those conditions. It completes the regularity seam in the T5 chain of Recognition Science, where T5 establishes J-uniqueness as the self-similar fixed point. The definition touches no open scaffolding questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.