Foundation Alpha Coordinate Fixation Cost Alpha Log High Calibrated Iff

The higher-derivative calibration

The declaration costAlphaLog_high_calibrated_iff establishes a precise equivalence about a family of cost functions used in the framework's branch selection. In plain terms, it says: for a function in the bilinear family, the condition that its fourth derivative at zero equals one holds exactly when the parameter α satisfies α² = 1. This is a theorem in the machine-checked library of formal theorems, meaning it is a proved statement, not a conjecture.

To see why this matters, start with the family itself. The framework models a cost function in log coordinates as cost, a measure of how much a recognition event deviates from a baseline. The family is written as G_α(t) = (1/α²)(cosh(αt) − 1), with α ≥ 1. The second derivative at zero, G''(0), equals 1 for every α, so it cannot distinguish one member of the family from another. The fourth derivative at zero, however, equals α², so it does distinguish them. The theorem costAlphaLog_high_calibrated_iff formalizes exactly this: the higher-derivative calibration condition G^(4)(0) = 1 is equivalent to α² = 1.

Combined with the convention α ≥ 1, this forces α = 1, and the cost function becomes J(x) = (1/2)(x + 1/x) − 1, the canonical reciprocal cost. The framework's library proves this pinning in a chain: the fourth-derivative calibration pins α, and then the α = 1 cost is exactly J. This closes the α-coordinate freedom within the bilinear branch, leaving J as the unique calibrated cost under this route.

What the declaration does not claim is equally important. It does not claim that this higher-derivative calibration is the only way to fix α; the framework lists two other candidate fixations, generator calibration and action-functional minimisation, which remain open targets. It also does not claim that the fourth-derivative condition is physically motivated beyond being a mathematical calibration choice. The theorem is conditional: it holds within the bilinear family and under the convention α ≥ 1, not for all possible cost functions.

/-- The α-cost is high-calibrated iff `α² = 1`. -/
theorem costAlphaLog_high_calibrated_iff (α : ℝ) (hα : α ≠ 0) :
    IsHighCalibratedLog (CostAlphaLog α) ↔ α ^ 2 = 1 := by
  unfold IsHighCalibratedLog
  rw [costAlphaLog_fourth_deriv_at_zero α hα]

/-- **The fourth derivative of `CostAlphaLog α` at zero is `α²`.**

This is the calibration invariant that distinguishes different `α` values
within the bilinear family: the second derivative `G_α''(0) = 1` is
constant, but the fourth derivative `G_α^(4)(0) = α²` separates them. -/
theorem costAlphaLog_fourth_deriv_at_zero (α : ℝ) (hα : α ≠ 0) :
    deriv (deriv (deriv (deriv (CostAlphaLog α)))) 0 = α ^ 2 := by
  have := (hasDerivAt_costAlphaLog_fourth α hα 0).deriv
  rw [this]
  simp [mul_zero, cosh_zero]

/-- **The α-pin theorem.** Within the bilinear `α`-family with the
rigidity-paper convention `α ≥ 1`, higher-derivative calibration forces
`α = 1`. -/
theorem alpha_pin_under_high_calibration
    (α : ℝ) (h_pos : 1 ≤ α)
    (h_calib : IsHighCalibratedLog (CostAlphaLog α)) :
    α = 1 := by
  have hα_ne : α ≠ 0 := by linarith
  have hα_sq : α ^ 2 = 1 :=
    (costAlphaLog_high_calibrated_iff α hα_ne).mp h_calib
  -- α ≥ 1 and α² = 1 forces α = 1.
  nlinarith

What this page does not claim

The higher-derivative calibration is the only way to fix α. The fourth-derivative condition is physically motivated. The theorem applies outside the bilinear family or without the α ≥ 1 convention.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/AlphaCoordinateFixation.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: