CalibrationCert
plain-language theorem explainer
Packages the A4 calibration axiom: the log-cost Jlog has unit curvature at the identity, i.e. its second derivative at 0 equals 1. Anyone citing the uniqueness of J under A1–A4 (forcing chain T5) uses this certificate. Verification is discharged by three calculus lemmas on hyperbolic derivatives of Jlog.
Claim. A calibration certificate is a unit record whose verification predicate asserts three facts about the log-cost $J_{\log}(t)=\cosh t-1$: $\partial_t J_{\log}=\sinh$, $\partial_t^2 J_{\log}=\cosh$, and $\partial_t^2 J_{\log}(0)=1$ (unit curvature at the identity).
background
In Recognition Science the cost on ratios is fixed by four axioms A1–A4. A1–A3 (reciprocal symmetry, zero at identity, strict convexity) leave a free positive scale factor. A4, unit curvature of the log-pullback at zero, kills that freedom and forces $J(x)=(x+x^{-1})/2-1=\cosh(\log x)-1$, the unique solution in the T5 step of the forcing chain.
The log-cost is $J_{\log}(t):=J(e^t)$. By definition (or the closed form) $J_{\log}(t)=\cosh t-1$. Standard hyperbolic calculus then gives first derivative $\sinh$ and second derivative $\cosh$, so evaluating at $t=0$ yields curvature 1.
This module sits in the verification layer: it packages that calculus fact as a certificate object rather than leaving it as a bare lemma, so downstream measurement and SI-reporting code can depend on a single named witness.
proof idea
The structure itself is empty (a unit certificate). The content is the simp predicate verified, a conjunction of three propositions, and the theorem that every certificate satisfies it.
verified_any is a three-goal refine: the first conjunct is exactly the upstream lemma that $\partial_t J_{\log}=\sinh$; the second is the lemma that $\partial_t^2 J_{\log}=\cosh$; the third is the calibration theorem that the second derivative at zero equals 1 (proved upstream by rewriting with the second-derivative lemma and cosh_zero). No new analysis is done here; it is a packaging wrapper.
why it matters
This is the formal A4 witness that completes T5 J-uniqueness: without unit curvature any positive multiple $\alpha J$ would satisfy A1–A3, and the overall scale of the Recognition cost would be free. With A4 the scale is fixed, which pins RS-native constants downstream (including the curvature normalization that feeds mass-ladder and coupling extractions).
Parent consumers live in the single-anchor measurement stack: the SI calibration record, the derived external calibration, exact reporting of $c$ in m/s, and one-act reporting of $\hbar$ in J·s all take a CalibrationCert (or the parallel measurement certificate that reuses the name). The module doc states the role cleanly: calibration fixes the overall scale so the unique solution is exactly $J$, not $\alpha J$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.