Pith. sign in
theorem

costAlphaLog_fourth_deriv_at_zero

proved
show as:

Why this theorem is linked from An integration-free approach for particle flow filtering unclear

Pith linked this Lean declaration because the review connected a specific passage in the paper to this theorem. The relation tag says how strong that connection is; it is not a generic placeholder.

D = R^{-1/2} H P H^T R^{-1/2} ... D = V Λ V^T ... Φ(λ,0) = I + E Ω(λ) F^T with ω_i(λ) = (1 + λ α_i)^{-1/2} - 1/α_i

Relation between the paper passage and the cited Recognition theorem.

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.