StrictConvexityFromClosure
plain-language theorem explainer
The structure packages the requirement that a cost function is strictly convex on the positive reals. Researchers reconstructing ledgers from finite descriptions cite this when splitting regularity obligations into independent parts. It is a direct definition that records the strict convexity predicate without additional proof steps.
Claim. A cost functional $J : ℝ → ℝ$ satisfies the strict-convexity-from-closure condition when $J$ is strictly convex on the open interval $(0, ∞)$.
background
The Closed Observable Framework absorbs positive-valued observables, ratio interfaces, and conservation laws as structure fields in phases 1, 2, and 6 of the axiom-closure plan. This leaves the Regularity Axiom as the sole remaining substantive condition, which encodes the finite-description content of C3.
proof idea
This is a structure definition consisting of a single field that directly invokes the strict convexity predicate on the positive reals. No lemmas or tactics are applied beyond the definition itself.
why it matters
This declaration splits the regularity seam for use in the FiniteDescriptionRegularity structure, which folds continuity, convexity, and calibration back into the legacy bundle. It fills the convexity component of the Regularity Axiom in the Closed Observable Framework. Within the Recognition Science framework, it supports J-uniqueness by ensuring the cost functional has the curvature needed for self-similar fixed points and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.