pith. sign in
theorem

alpha_pin_under_high_calibration

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

plain-language theorem explainer

The α-pin theorem establishes that fourth-derivative calibration at zero of the bilinear cost family forces the parameter α to equal 1 when α ≥ 1. Branch-selection work in Recognition Science cites this result to isolate the canonical J-cost from the one-parameter family. The proof first invokes the equivalence that high calibration holds precisely when α² = 1, then applies linear arithmetic under the positivity assumption to conclude α = 1.

Claim. Let $G_α(t) = α^{-2} (cosh(α t) - 1)$. If $α ≥ 1$ and the fourth derivative of $G_α$ at $t=0$ equals 1, then $α = 1$.

background

The Alpha-Coordinate Fixation module isolates the canonical cost by higher-derivative calibration of the bilinear family. CostAlphaLog(α, t) is defined as α^{-2}(cosh(α t) - 1), the α-parameterized cost expressed in logarithmic coordinates. IsHighCalibratedLog(G) is the predicate that the fourth derivative of G at zero equals 1. The module works inside the setting where the branch-selection theorem has already reduced calibrated costs to this one-parameter family with the rigidity convention α ≥ 1. The key upstream equivalence states that IsHighCalibratedLog(CostAlphaLog α) holds if and only if α² = 1.

proof idea

The tactic proof first obtains α ≠ 0 by linear arithmetic. It then applies the equivalence costAlphaLog_high_calibrated_iff to convert the calibration hypothesis into the equation α² = 1. The final step invokes nlinarith on the conjunction of α ≥ 1 and α² = 1 to conclude α = 1.

why it matters

This result supplies the α-pin step inside the certification structure alphaCoordinateFixationCert and is invoked directly by the uniqueness theorem J_uniquely_calibrated_via_higher_derivative to obtain CostAlpha α x = Jcost x. It realises Option 2 of the three candidate fixations listed in the branch-selection paper, using fourth-derivative calibration to force α = 1 and thereby recover the J-cost that appears at T5 of the forcing chain. The other two fixation routes remain open.

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

papers checked against this theorem (showing 30 of 517)

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.