IsHighCalibratedLog
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Finite R-transform approximates standard version within O(1/N)
"H_µ(z) = ∫ log(z − t) dµ(t); H*_µ(s) := inf_{x>0}{sx − H_µ(x)}; (H*)'(H'(x)) = x."