CalibrationFromUnitChoice
plain-language theorem explainer
CalibrationFromUnitChoice isolates the second-derivative normalization on the J-cost after logarithmic substitution. Ledger reconstruction arguments in the ClosedObservableFramework cite it when decomposing the regularity axiom into separately auditable continuity, convexity, and calibration pieces. The structure is a direct field extraction with no further proof content.
Claim. Let $J : (0,∞) → ℝ$. The calibration condition holds when the second derivative of the map $t ↦ J(e^t)$ equals 1 at $t=0$.
background
The ClosedObservableFramework module treats the J-cost as the central observable derived from phi-forcing. It absorbs several ratio and conservation axioms as structure fields, leaving only the Regularity Axiom to encode the finite-description content of C3. The legacy RegularityCert bundles three obligations: continuity on the positive reals, strict convexity, and the calibration condition now split out here.
proof idea
One-line structure definition that extracts the calibration field previously contained inside RegularityCert. No tactics or lemmas are applied; the declaration simply names the second-derivative equality as a Prop field.
why it matters
The declaration supplies the calibration component of FiniteDescriptionRegularity, which folds the split obligations back into the legacy bundle for downstream users. It completes the explicit split of the regularity seam required by the axiom-closure plan in Gap 1. The condition directly implements the unit-normalization step that follows J-uniqueness in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.