pith. sign in
theorem

costAlphaLog_fourth_deriv_at_zero

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

plain-language theorem explainer

The fourth derivative at zero of the alpha-parameterized cost in logarithmic coordinates equals alpha squared for nonzero alpha. Workers on branch selection in Recognition Science cite this identity when applying higher-order calibration to isolate the canonical reciprocal cost J. The argument is a direct term application of the fourth-derivative existence result at the evaluation point, followed by algebraic simplification.

Claim. Let $G_α(t) := (1/α²)(cosh(α t) - 1)$ for $α ∈ ℝ ∖ {0}$. Then the fourth derivative of $G_α$ at $t=0$ satisfies $G_α^{(4)}(0) = α²$.

background

In the Alpha Coordinate Fixation module, higher-derivative calibration is developed as one route to select the parameter α in the bilinear family of costs. The relevant function is the log-reparametrized cost G_α(t) defined by (1/α²)(cosh(α t) - 1). Its Taylor expansion at the origin begins with the constant term zero, linear term zero, quadratic term t²/2 (hence unit second derivative), cubic term zero, and quartic term (α² t⁴)/24.

proof idea

The proof applies the upstream lemma establishing the general fourth-derivative formula at the point t=0 to obtain the expression α² cosh(α · 0). It then rewrites the derivative value and simplifies the hyperbolic cosine at zero together with the zero-multiplication rule.

why it matters

The result is invoked directly by the high-calibration equivalence theorem, which states that the α-cost is high-calibrated precisely when α² equals one. This equivalence is packaged into the alphaCoordinateFixationCert definition that collects the fixation certificates. It realizes the higher-derivative calibration option from section 5 of the branch-selection paper and thereby contributes to forcing the coordinate α to one, which recovers the J-cost via the uniqueness result.

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

papers checked against this theorem (showing 30 of 115)

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.