pith. sign in
def

alphaCoordinateFixationCert

definition
show as:
module
IndisputableMonolith.Foundation.AlphaCoordinateFixation
domain
Foundation
line
218 · github
papers citing
3 papers (below)

plain-language theorem explainer

The definition alphaCoordinateFixationCert assembles four supporting lemmas into the AlphaCoordinateFixationCert structure, thereby certifying that fourth-derivative calibration at zero pins alpha to 1 within the bilinear cost family and isolates the J-cost. Researchers tracing branch selection in Recognition Science would cite it when closing the higher-derivative route to alpha fixation. The construction is a direct structure instantiation that wires each field to its corresponding theorem.

Claim. The Alpha-Coordinate Fixation Certificate states that the fourth derivative of $G_α(t) = α^{-2}(cosh(α t)-1)$ at $t=0$ equals $α^2$, that the cost is high-calibrated if and only if $α^2=1$, that high calibration together with $α≥1$ forces $α=1$, and that the resulting cost on positive reals coincides with the J-cost.

background

Within the bilinear branch produced by BranchSelection the cost takes the one-parameter form $G_α(t) = α^{-2}(cosh(α t)-1)$ for $α≥1$. The second derivative at zero is identically 1 for every α, but the fourth derivative at zero equals α²; this supplies the invariant that distinguishes members of the family. The module implements Option 2 of the three candidate α-fixation routes listed in §5 of the companion paper RS_Branch_Selection.tex, extending the existing IsCalibrated framework with the smallest additional surface.

proof idea

The definition is a one-line structure constructor that directly populates the four fields of AlphaCoordinateFixationCert by reference to the upstream theorems costAlphaLog_fourth_deriv_at_zero, costAlphaLog_high_calibrated_iff, alpha_pin_under_high_calibration, and J_uniquely_calibrated_via_higher_derivative.

why it matters

This certificate supplies the concrete object that closes the higher-derivative calibration path, feeding immediately into the inhabitedness result alphaCoordinateFixationCert_inhabited. It realises the J-uniqueness step of the forcing chain by forcing α=1 under the rigidity convention and thereby recovering the canonical reciprocal cost. The choice of this route over the two remaining open options (generator calibration and action minimisation) is justified by its direct compatibility with the derivative-based calibration already present in the IsCalibrated infrastructure.

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

papers checked against this theorem (showing 3 of 3)