then

formal source

 291A **calibration** of a cost function on a configuration space is a
 292choice of distinguished inconsistent configuration `α` and a positive
 293value `δ` such that `κ.C α = δ`. The recognition-work constraint
 294theorem then says that any other cost function `κ'` agreeing with
 295`κ` on `α` and on the chosen indecomposable inconsistent
 296configurations agrees with `κ` everywhere expressible as
 297independent joins of those generators.
 298-/
 299structure Calibration (κ : CostFunction Config) where
 300  /-- A distinguished inconsistent configuration. -/
 301  α : Config
 302  /-- The chosen positive cost value. -/
 303  δ : ℝ
 304  /-- The chosen value is positive. -/
 305  δ_pos : 0 < δ
 306  /-- The configuration is inconsistent. -/
 307  α_inconsistent : ¬IsConsistent α
 308  /-- The cost function takes the chosen value at the chosen
 309      configuration. -/
 310  agrees : κ.C α = δ
 311
 312namespace Calibration
 313
 314variable {κ : CostFunction Config}
 315
 316/-- A calibrated cost function is positive on the calibration witness. -/
 317theorem calibration_pos (cal : Calibration κ) : 0 < κ.C cal.α := by
 318  rw [cal.agrees]
 319  exact cal.δ_pos
 320
 321/-- Two cost functions agreeing on a calibration's witness agree on
 322all independent extensions of that witness with consistent
 323configurations (which contribute zero by the dichotomy). -/
 324theorem extension_to_consistent