pith. sign in
theorem

costAlphaLog_high_calibrated_iff

proved
show as:
module
IndisputableMonolith.Foundation.AlphaCoordinateFixation
domain
Foundation
line
155 · github
papers citing
223 papers (below)

plain-language theorem explainer

The theorem equates high-calibration of the α-cost (fourth derivative of G at zero equals one) with the algebraic condition α² = 1. Branch-selection work in Recognition Science cites it to isolate the canonical J-cost inside the bilinear family. The proof is a one-line wrapper that unfolds the calibration predicate and substitutes the fourth-derivative evaluation lemma.

Claim. Let $G_α(t) = α^{-2}(cosh(α t) - 1)$. Then $G_α^{(4)}(0) = 1$ if and only if $α^2 = 1$, for $α ≠ 0$.

background

The module AlphaCoordinateFixation formalizes Option 2 of the three candidate α-fixations listed in the companion branch-selection paper. It works inside the one-parameter family obtained from the bilinear branch theorem: $G_α(t) = α^{-2}(cosh(α t) - 1)$ for α ≥ 1. The second derivative at zero is identically 1 for every α, so unit-curvature calibration does not distinguish members of the family. Higher-derivative calibration is defined by the predicate IsHighCalibratedLog G, which requires the fourth derivative of G at zero to equal 1.

proof idea

The proof is a one-line wrapper. It unfolds the definition of IsHighCalibratedLog and rewrites the fourth-derivative evaluation supplied by the upstream lemma costAlphaLog_fourth_deriv_at_zero, which states that the fourth derivative of CostAlphaLog α at zero equals α².

why it matters

This result supplies the algebraic half of the α-pin theorem (alpha_pin_under_high_calibration) and is recorded inside the certificate alphaCoordinateFixationCert. It closes the higher-derivative route to J-uniqueness inside the Recognition framework, complementing T5 (J-uniqueness) and the eight-tick octave structure. The other two fixation routes (generator calibration and action minimization) remain open.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.

papers checked against this theorem (showing 30 of 223)

The full set is indexed internally; the public theorem page shows a capped sample so high-use declarations do not become many-thousand-row pages.