calibration_unit_is_a_gauge
plain-language theorem explainer
The δ-forced continuum cost form is a one-parameter family F_c(t)=cosh(c t)-1; its only invariant is the log-curvature c² at the unit, the family is faithful for c>0, and curvature 1 selects exactly c=1 (i.e. J). Anyone citing the PRC calibration or the shrunk δ-certificate uses this as Item 2. The proof is a three-way packaging of the curvature identity, injectivity, and the curvature-one characterization.
Claim. For every real $c$, the second derivative at $0$ of $t \mapsto \cosh(c t)-1$ equals $c^2$. Distinct positive parameters give distinct cost functions: if $c,d>0$ and $\cosh(c\cdot)-1=\cosh(d\cdot)-1$ as functions, then $c=d$. For $c>0$, that second derivative equals $1$ if and only if $c=1$ (the member that is $J$ in log coordinates).
background
In the Primitive Recognition Calculus, the discrete δ-carrier forces a continuum cost of the shape $\cosh(c t)-1$ on the log-coordinate $t$, but does not fix the positive scale $c$. That residual freedom is a gauge: the continuum second-derivative (log-curvature) at the unit is invisible to the discrete carrier.
The unique T5 cost is $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$. In log coordinates the $c=1$ member is exactly $J$. Upstream, logCurvature computes the second derivative at $0$ as $c^2$; clog_inj shows distinct positive $c$ give distinct functions ("The cost family is faithful"); curvature_one_iff_J shows normalized curvature $1$ picks out $c=1$.
Local setting is the PRC calibration target: isolate what the δ program does and does not fix before feeding the RS forcing chain.
proof idea
Term-mode triple of already-proved facts. First conjunct is logCurvature verbatim: differentiate $t\mapsto\cosh(c t)-1$ twice and evaluate at $0$ to get $c^2$. Second conjunct applies clog_inj: equal cost functions share the same curvature invariant, so $c^2=d^2$ with $c,d>0$ forces $c=d$. Third conjunct is curvature_one_iff_J: rewrite the second derivative via logCurvature, then $c^2=1$ and $c>0$ give $c=1$. No extra algebra in this wrapper.
why it matters
This is Item 2 of the δ-program headlines: the forced cost form leaves a faithful one-parameter gauge whose only invariant is log-curvature $c^2$, and curvature $1$ selects $J$. Downstream it is wired into prc_shrunk_certificate as the field cost_form_free_unit, part of the claim "Seven proved headlines, no axioms, no sorry."
Framework link: T5 J-uniqueness identifies $J(x)=\cosh(\log x)-1$; the present result says the continuum family still has a free positive unit until one normalizes curvature to $1$. That normalization is a gauge choice, not a δ-forcing. It clarifies the boundary between what the discrete carrier determines and what must be fixed by continuum calibration before the RS chain (RCL, φ, eight-tick, $D=3$) runs on a fully pinned cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.