calibration_gap_closed_by_normalized_interface
plain-language theorem explainer
The calibration gap is fully classified: discrete recognition laws leave a one-real torsor of cost units, while the normalized one-act continuum interface is necessary and sufficient to force the unit to 1. Anyone citing cost-unit uniqueness or closure of Axiom 3 (Calibration) would use this. The proof is a four-conjunct term packaging forcing, necessity/sufficiency, existence, and clog-injectivity.
Claim. The following hold simultaneously: (i) every normalized one-act interface (a positive cost unit whose primitive one-act chart has unit log-curvature) has unit equal to $1$; (ii) for every $c>0$, one has $c=1$ if and only if the one-act curvature of $c$ equals $1$; (iii) there exists a normalized one-act interface with unit $1$; (iv) if $c,d>0$ and $t\mapsto\cosh(ct)-1$ equals $t\mapsto\cosh(dt)-1$ as functions, then $c=d$.
background
In the Primitive Recognition Calculus, discrete orbit laws do not pin the cost unit: they leave a faithful one-real torsor (the sibling fact discrete_does_not_force_unit). Closing that gap needs a minimal continuum-side datum, not a full field completion.
A normalized one-act interface is exactly that datum: a positive real unit together with the assertion that the primitive one-act chart has unit log-curvature (oneActCurvature unit = 1). One-act curvature is the continuum avatar of Axiom 3 (Calibration) from CostAxioms: if $G(t)=F(e^t)$, then $G''(0)=1$, which normalizes curvature of the cost at unity and selects a unique solution rather than a family.
Upstream, unit_forced_by_one_act and calibration_datum_necessary_and_sufficient already show that for positive $c$, the curvature condition is necessary and sufficient for $c=1$. The canonical interface is the member with unit $1$ itself. The fourth clause is clog-injectivity for the family $t\mapsto\cosh(ct)-1$, tying the scale to the unique J-cost shape $\cosh(\log x)-1$.
proof idea
Term-mode four-way conjunction, no tactics.
- Universal forcing: apply
normalized_interface_forces_J, which reduces any interface's curvature_unit viaunit_forced_by_one_acttoI.unit = 1. - Necessity and sufficiency: for each positive $c$, invoke
calibration_datum_necessary_and_sufficient(the symmetric form of the same one-act forcing). - Existence: pair
canonicalInterface(unit $:= 1$, curvature discharged byoneActCurvature_eqandnorm_num) withrfl. - Scale uniqueness: apply
Calibration.clog_injto the equality of the two cosh-minus-one charts.
The whole theorem is therefore a packaging certificate, not a new computation.
why it matters
This is the calibration closure theorem for the Delta-real layer: it states that the cost-unit issue is not discrete-forced and is closed exactly by the minimal second-order recognition interface. That matches the CostAxioms Calibration class (second log-derivative at the origin equals 1) and feeds the unique J-cost of the forcing chain (T5: $J(x)=\cosh(\log x)-1$).
Downstream it is consumed by strongClosureCertificate in DeltaNativeStrongClosure, the concrete certificate assembling the closed Delta-native theorem surface (real forgetful display, generable carrier, certified analytic protocols). Without this four-part package, the strong-closure bundle would still carry an open calibration torsor.
In framework terms it finishes the local half of Axiom 3 inside PRC: one continuum curvature datum, no more and no less, before native strong closure and later constants (phi-ladder, alpha band) are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.