FiniteDescriptionRegularity
FiniteDescriptionRegularity packages three independent properties for a function J from reals to reals: continuity on the positive reals, strict convexity on the positive reals, and a second-derivative calibration condition after logarithmic substitution. Ledger reconstruction proofs in the closed observable framework cite it to keep the finite-description obligations separately verifiable rather than bundled. The declaration is a structure definition equipped with direct field-extraction conversions to the legacy RegularityCert record.
claimLet $J : (0,∞) → ℝ$. The predicate holds when $J$ is continuous on $(0,∞)$, strictly convex on $(0,∞)$, and satisfies $d²/dt² [J(e^t)]|_{t=0} = 1$.
background
The ClosedObservableFramework module splits the regularity seam into three auditable structures to support ledger reconstruction. ContinuityFromFiniteDescription requires J continuous on the open interval (0, ∞). StrictConvexityFromClosure requires J strictly convex on (0, ∞). CalibrationFromUnitChoice requires the second derivative of J ∘ exp at zero to equal 1. These replace the single RegularityCert bundle while preserving compatibility via conversion maps. The module setting is Gap 1 of the axiom-closure plan, absorbing R1, R2, R5, R6 as definitions and leaving the regularity axiom as the finite-description content of C3.
proof idea
The declaration is a structure definition that directly assembles the three component structures. The accompanying toRegularityCert and toFiniteDescriptionRegularity definitions are one-line wrappers that extract and repackage the continuous, strict_convex, and calibration fields.
why it matters in Recognition Science
It is invoked by the ledger_reconstruction definition, which states that a closed observable framework canonically carries a zero-parameter comparison ledger with R1–R6 absorbed and the remaining seam tracked as these explicit obligations. The split supports the Regularity Axiom in Phase 6 of the axiom-closure plan, encoding the finite-description content of C3. It keeps continuity, convexity, and calibration independently auditable for downstream users.
scope and limits
- Does not prove existence of any J satisfying the three properties.
- Does not derive the explicit form of J from the Recognition functional equation.
- Does not extend the conditions beyond the positive reals.
- Does not incorporate conservation or ratio-interface axioms.
formal statement (Lean)
86structure FiniteDescriptionRegularity (J : ℝ → ℝ) : Prop where
87 continuity : ContinuityFromFiniteDescription J
88 convexity : StrictConvexityFromClosure J
89 calibration : CalibrationFromUnitChoice J
90
91/-- Fold the split finite-description obligations back into the legacy bundle. -/
92def FiniteDescriptionRegularity.toRegularityCert {J : ℝ → ℝ}
93 (h : FiniteDescriptionRegularity J) : RegularityCert J where
94 continuous := h.continuity.continuous
proof body
Definition body.
95 strict_convex := h.convexity.strict_convex
96 calibration := h.calibration.calibration
97
98/-- Unfold the legacy regularity bundle into the split obligations. -/
99def RegularityCert.toFiniteDescriptionRegularity {J : ℝ → ℝ}
100 (h : RegularityCert J) : FiniteDescriptionRegularity J where
101 continuity := ⟨h.continuous⟩
102 convexity := ⟨h.strict_convex⟩
103 calibration := ⟨h.calibration⟩
104
105/-- **R6 as theorem**: Compositional closure follows from continuity.
106If J is continuous on R_{>0}, then J(xy) + J(x/y) is finite. -/