IsCalibrated
plain-language theorem explainer
The calibration condition normalizes the curvature of a cost functional at the identity by requiring the second derivative of its log-reparametrized form at zero to equal one. Researchers proving T5 uniqueness of the cost algebra in Recognition Science cite this definition to fix the scale of solutions to the functional equation. It is introduced directly as the equality of that second derivative to unity, which is equivalent to the stated limit form.
Claim. A function $F:ℝ→ℝ$ is calibrated when the second derivative at zero of $G(t):=F(e^t)$ equals one, i.e., $G''(0)=1$.
background
This module supplies lemmas for the T5 cost uniqueness proof. The reparametrization $G(t)=F(exp t)$ converts the multiplicative Recognition Composition Law into an additive equation in log coordinates. Upstream, the Calibration axiom states that the second derivative at the origin in log coordinates equals 1; this normalizes the curvature of the cost functional at unity and ensures a unique solution rather than a family. The shifted form $H=G+1$ then satisfies the d'Alembert equation under the composition law.
proof idea
The declaration is a direct definition that records the calibration condition as the second derivative of the reparametrized function equaling one at the origin. No lemmas or tactics are applied; it simply packages the normalization hypothesis for downstream uniqueness arguments.
why it matters
This definition supplies the calibration hypothesis required by the parent theorems cost_algebra_unique and cost_algebra_unique_aczel, which establish that any cost satisfying the axioms plus this condition must equal the J function (T5 in the forcing chain). It implements the normalization step that anchors the scale so the self-similar fixed point and eight-tick octave follow uniquely. The result touches the open question of minimal regularity assumptions needed to invoke Aczél's theorem without extra hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
One golden-ratio curve organizes four periodic-table trends at once
"The model's input cost function J is the unique solution on R_>0 of the functional equation J(xy) + J(x/y) = 2 J(x) J(y) + 2 J(x) + 2 J(y), under the regularity conditions of continuity, normalization J(1)=0, stationarity J'(1)=0, and positive curvature J''(1)>0 ... The unique solution is J(x) = ½(x + x⁻¹) − 1 = cosh(ln x) − 1."