Jcost_regularity_cert
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove the uniqueness theorem T5 itself.
- Does not address behavior of Jcost at zero or for negative arguments.
- Does not derive the composition law or normalization axioms from more primitive assumptions.
- Applies exclusively to the specific Jcost function rather than arbitrary cost functionals.
formal statement (Lean)
203noncomputable def Jcost_regularity_cert :
204 IndisputableMonolith.Foundation.ClosedFramework.RegularityCert Cost.Jcost where
205 continuous := Jcost_continuous_pos
proof body
Definition body.
206 strict_convex := Cost.Jcost_strictConvexOn_pos
207 calibration := CPM.LawOfExistence.RS.Jcost_log_second_deriv_normalized
208
209end CostUniqueness
210end IndisputableMonolith