RegularityCert
plain-language theorem explainer
RegularityCert packages three conditions on a function J from the reals to the reals: continuity on the positive reals, strict convexity on the positive reals, and the normalization that the second derivative of J composed with the exponential equals one at the origin. Cost-uniqueness arguments in the framework cite the bundle to confirm that Jcost meets the regularity needed before invoking the T5 uniqueness theorem. The declaration is a plain structure definition that records the three field obligations for legacy compatibility with split-reg
Claim. A function $J : (0,∞) → ℝ$ satisfies the regularity certificate when it is continuous on $(0,∞)$, strictly convex on $(0,∞)$, and obeys $(d²/dt²)J(e^t)|_{t=0} = 1$.
background
The ClosedObservableFramework module collects positive-valued observables, ratio interfaces, and conservation as structure fields while absorbing R1, R2, R5, R6 as definitions; the remaining Regularity Axiom encodes the finite-description content of C3. RegularityCert is the legacy single-record form of that axiom. Upstream, FiniteDescriptionRegularity splits the same seam into three independently auditable structures (continuity from finite description, strict convexity from closure, and calibration from unit choice), while ArithmeticOf.extracted supplies the Peano surface and initial data extracted from any LogicRealization.
proof idea
The declaration is a structure definition whose three fields directly record the continuity, strict-convexity, and calibration obligations; it functions as a one-line wrapper that folds the split FiniteDescriptionRegularity obligations back into the legacy bundle for downstream users.
why it matters
RegularityCert is referenced by Jcost_regularity_cert and unique_cost_on_pos in CostUniqueness, where the former constructs the instance for Jcost and the latter applies it to conclude that any admissible cost equals Jcost on the positives. It occupies the legacy slot for the Regularity Axiom in the Closed Observable Framework, which encodes the finite-description content of C3 in the axiom-closure plan and thereby supports the T5 J-uniqueness step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.