IsCalibrated
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not prove existence of the second derivative.
- Does not enforce the composition law or reciprocal symmetry.
- Does not determine the explicit form of the cost function.
- Does not address global behavior or higher derivatives.
formal statement (Lean)
601def IsCalibrated (F : ℝ → ℝ) : Prop :=
proof body
Definition body.
602 deriv (deriv (G F)) 0 = 1
603
604/-- **Calibration (limit form)**:
605lim_{t→0} 2·F(e^t)/t² = 1, expressed on H = G + 1. -/
used by (12)
-
cost_algebra_unique -
cost_algebra_unique_aczel -
PrimitiveCostHypotheses -
washburn_uniqueness_of_contDiff -
isCalibratedLimit_of_isCalibrated -
isCalibrated_of_isCalibratedLimit -
washburn_uniqueness -
washburn_uniqueness_aczel -
washburn_uniqueness_aczel -
Jcost_is_calibrated -
unique_cost_on_pos_from_rcl -
J_is_unique_cost_under_logic