Foundation Alpha Coordinate Fixation Alpha Pin Under High Calibration

Pinning the cost function

The cost function J(x) = (1/2)(x + 1/x) - 1 measures the price of a recognition event, a discrete record of a comparison, when the compared quantities sit at ratio x. A central theorem in Recognition Science proves this is the only function satisfying five plain conditions. But before that theorem can apply, one must choose among a family of candidate functions that all satisfy the earlier, weaker conditions. The family is F_α(x) = (1/α²)(cosh(α ln x) - 1), with α ≥ 1. Each member has the same second derivative at the neutral point x = 1, so that standard calibration cannot tell them apart.

The declaration alpha_pin_under_high_calibration closes this gap. It proves that if a fourth-derivative calibration holds, namely G⁗(0) = 1 in log coordinates, then α² = 1. Combined with the convention α ≥ 1, this forces α = 1. The theorem then concludes that the cost function is exactly J. In plain terms, the higher the order of the calibration condition, the fewer functions survive; the fourth derivative is the first one that separates the family, and it selects the single reciprocal form.

This is a theorem in the framework's machine-checked library of formal theorems, meaning the reasoning is verified step by step. The proof is short: the fourth derivative of F_α at zero is α², so setting it to 1 gives α = 1, and then the cost reduces to J. The result is one of three candidate routes to fixing α; the other two, a generator calibration and an action-functional minimisation, remain open targets. This route was chosen because it fits the existing calibration framework with the smallest change.

The consequence is that the α-coordinate freedom is closed. Within the bilinear branch, J is now the unique calibrated cost. This does not by itself prove the full five-condition theorem, nor does it assign a value to the fine-structure constant. It is a precise, narrow result: one calibration condition, one family, one pinned value.

/-- **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 α-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 α-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

/-- The `α = 1` bilinear cost is exactly `Jcost`. -/
theorem alpha_pinned_to_one_implies_J (x : ℝ) (hx : 0 < x) :
    CostAlpha 1 x = Jcost x :=
  cost_alpha_one_eq_jcost x hx

What this page does not claim

This does not prove the full five-condition uniqueness theorem for J. This does not assign a value to the fine-structure constant. This does not establish that the fourth-derivative calibration is the only possible one.

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: