IsHighCalibratedLog
The high-calibration predicate asserts that a log-reparametrized cost function G has fourth derivative exactly one at zero. Researchers formalizing branch selection in Recognition Science cite it to isolate the canonical J-cost by forcing α=1 inside the bilinear family. The definition is a direct extraction of the fourth-order Taylor coefficient from the cosh form.
claimA function $G : ℝ → ℝ$ is high-calibrated when its fourth derivative at the origin satisfies $G^{(4)}(0) = 1$.
background
The Alpha-Coordinate Fixation module works inside the bilinear branch $F_α(x) = α^{-2}(cosh(α ln x) - 1)$ for α ≥ 1 produced by BranchSelection. The log reparametrization $G(t) = F(e^t)$ gives the explicit family $G_α(t) = α^{-2}(cosh(α t) - 1)$. Direct differentiation shows the fourth derivative at zero equals α², so the predicate selects the case α² = 1. This extends the α-invariant unit-curvature condition G''(0) = 1 already present in Cost.costAlphaLog_unit_curvature.
proof idea
One-line definition that directly encodes the fourth-derivative condition at zero on the supplied function G.
why it matters in Recognition Science
The predicate supplies the calibration hypothesis for alpha_pin_under_high_calibration and J_uniquely_calibrated_via_higher_derivative. It implements Option 2 of the three α-fixation routes listed in §5 of RS_Branch_Selection.tex. In the Recognition Science framework it completes the higher-derivative path to T5 J-uniqueness, isolating the reciprocal cost J on positive reals while the generator-calibration and action-minimization routes remain open.
scope and limits
- Does not assume any functional form for G beyond the fourth-derivative value at zero.
- Does not impose positivity, monotonicity or other regularity conditions on G.
- Does not address generator calibration or action-functional minimization routes to α-fixation.
- Applies only inside the bilinear family produced by BranchSelection.
formal statement (Lean)
151def IsHighCalibratedLog (G : ℝ → ℝ) : Prop :=
proof body
Definition body.
152 deriv (deriv (deriv (deriv G))) 0 = 1
153
154/-- The α-cost is high-calibrated iff `α² = 1`. -/