FiniteDescriptionRegularity
plain-language theorem explainer
FiniteDescriptionRegularity packages three separate regularity conditions on a real function J into one auditable record for use in closed observable frameworks. Ledger reconstruction proofs cite it to keep continuity on the positives, strict convexity on the positives, and the logarithmic second-derivative calibration as independently checkable obligations rather than a single legacy bundle. The declaration is a plain structure definition together with two one-line conversion maps to and from the older RegularityCert.
Claim. Let $J : (0,∞) → ℝ$. The map $J$ satisfies finite-description regularity when it is continuous on $(0,∞)$, strictly convex on $(0,∞)$, and obeys the calibration identity $(d²/dt²) J(e^t) |_{t=0} = 1$.
background
The ClosedObservableFramework module splits the regularity seam so that continuity, convexity and calibration become separately auditable. ContinuityFromFiniteDescription requires ContinuousOn J (Set.Ioi 0). StrictConvexityFromClosure requires StrictConvexOn ℝ (Set.Ioi 0) J. CalibrationFromUnitChoice requires that the second derivative of the composition of J with the exponential equals 1 at the origin. The legacy RegularityCert simply bundles the same three fields for backward compatibility. This split sits inside the ledger-reconstruction setting where R1, R2, R5 and R6 have already been absorbed as definitions and only the finite-description content of the regularity axiom remains.
proof idea
The declaration is a structure that directly assembles the three sub-structures ContinuityFromFiniteDescription, StrictConvexityFromClosure and CalibrationFromUnitChoice. The two conversion functions are one-line wrappers: toRegularityCert extracts the three fields into the legacy bundle, while toFiniteDescriptionRegularity wraps each field of the legacy bundle back into the corresponding sub-structure.
why it matters
FiniteDescriptionRegularity supplies the explicit regularity hypothesis required by the Ledger Reconstruction Theorem. It realises the Regularity Axiom of Phase 6 in the axiom-closure plan, encoding the finite-description content of C3 while keeping the three obligations independently verifiable. The structure feeds directly into ledger_reconstruction and preserves compatibility with the older RegularityCert for users who still expect a single record.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.