IsCalibratedLimit
IsCalibratedLimit encodes the limit-form calibration condition for a cost function F. It requires that the second-order curvature of the shifted log-reparametrization H F equals 1 at the origin. Researchers on the T5 J-uniqueness proof cite it when linking normalized costs to their calibrated limits. The declaration is a direct one-line abbreviation of HasLogCurvature applied to H F.
claimA cost function $F$ satisfies the calibrated limit condition when the limit as $t$ approaches 0 of $2(H_F(t)-1)/t^2$ equals 1, where $H_F(t)=F(e^t)+1$.
background
The module supplies lemmas for the T5 cost uniqueness proof. It introduces the log-coordinate reparametrization $G_F(t)=F(e^t)$ and the shifted version $H_F(t)=G_F(t)+1$. HasLogCurvature $H$ $κ$ asserts that the limit as $t$ approaches 0 of $2(H(t)-1)/t^2$ equals $κ$ (from the sibling definition at line 156). Upstream, the algebra module defines the shifted cost $H(x)=J(x)+1=½(x+x^{-1})$, under which the Recognition Composition Law becomes the d'Alembert equation $H(xy)+H(x/y)=2H(x)H(y)$.
proof idea
The declaration is a one-line definition that sets IsCalibratedLimit F to HasLogCurvature (H F) 1.
why it matters in Recognition Science
This definition is invoked by the equivalence lemmas isCalibratedLimit_of_isCalibrated and isCalibrated_of_isCalibratedLimit. It fills a step in the T5 J-uniqueness proof by expressing the infinitesimal calibration condition that matches the second derivative of the cosh-type solution at zero. In the framework it anchors the forcing chain from T5 through T8 by ensuring the cost function has the curvature required for the phi-ladder mass formula.
scope and limits
- Does not assert that any particular F satisfies the limit condition.
- Does not derive the curvature value from normalization or differentiability hypotheses.
- Does not address behavior at finite t or global solutions of the functional equation.
formal statement (Lean)
606def IsCalibratedLimit (F : ℝ → ℝ) : Prop :=
proof body
Definition body.
607 HasLogCurvature (H F) 1
608