pith. machine review for the scientific record. sign in
theorem

alpha_pin_under_high_calibration

proved
show as:
view math explainer →
module
IndisputableMonolith.Foundation.AlphaCoordinateFixation
domain
Foundation
line
165 · github
papers citing
170 papers (below)

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.AlphaCoordinateFixation on GitHub at line 165.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 162/-- **The α-pin theorem.** Within the bilinear `α`-family with the
 163rigidity-paper convention `α ≥ 1`, higher-derivative calibration forces
 164`α = 1`. -/
 165theorem alpha_pin_under_high_calibration
 166    (α : ℝ) (h_pos : 1 ≤ α)
 167    (h_calib : IsHighCalibratedLog (CostAlphaLog α)) :
 168    α = 1 := by
 169  have hα_ne : α ≠ 0 := by linarith
 170  have hα_sq : α ^ 2 = 1 :=
 171    (costAlphaLog_high_calibrated_iff α hα_ne).mp h_calib
 172  -- α ≥ 1 and α² = 1 forces α = 1.
 173  nlinarith
 174
 175/-! ## J is the unique high-calibrated bilinear cost -/
 176
 177/-- The `α = 1` bilinear cost is exactly `Jcost`. -/
 178theorem alpha_pinned_to_one_implies_J (x : ℝ) (hx : 0 < x) :
 179    CostAlpha 1 x = Jcost x :=
 180  cost_alpha_one_eq_jcost x hx
 181
 182/-- **The full uniqueness theorem.** Within the bilinear `α`-family,
 183under the convention `α ≥ 1`, higher-derivative calibration forces
 184`α = 1`, and the cost on positive reals is exactly `Jcost`. -/
 185theorem J_uniquely_calibrated_via_higher_derivative
 186    (α : ℝ) (h_pos : 1 ≤ α)
 187    (h_calib : IsHighCalibratedLog (CostAlphaLog α)) :
 188    ∀ x : ℝ, 0 < x → CostAlpha α x = Jcost x := by
 189  intro x hx
 190  have hα_eq : α = 1 := alpha_pin_under_high_calibration α h_pos h_calib
 191  rw [hα_eq]
 192  exact cost_alpha_one_eq_jcost x hx
 193
 194/-! ## Headline Certificate -/
 195