`CostFunction`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.CostFromDistinction
domain: Foundation
line: 147 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.CostFromDistinction on GitHub at line 147.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 144in the abstract setting we cannot derive it from (D) and (A) alone
 145without restricting to specific concrete configuration spaces.
 146-/
 147structure CostFunction (Config : Type u) [ConfigSpace Config] where
 148  /-- The cost function itself, taking values in the non-negative reals. -/
 149  C : Config → ℝ
 150  /-- Cost is non-negative. -/
 151  nonneg : ∀ Γ, 0 ≤ C Γ
 152  /-- (D) Dichotomy: zero cost characterises consistency. -/
 153  dichotomy : ∀ Γ, C Γ = 0 ↔ IsConsistent Γ
 154  /-- (A) Independent additivity: the recognition-work constraint. -/
 155  additivity : ∀ Γ₁ Γ₂, Independent Γ₁ Γ₂ → C (join Γ₁ Γ₂) = C Γ₁ + C Γ₂
 156
 157namespace CostFunction
 158
 159variable {Config : Type u} [ConfigSpace Config]
 160
 161/-! ### Immediate consequences of the axioms -/
 162
 163/-- The empty configuration has zero cost. -/
 164theorem emp_cost_zero (κ : CostFunction Config) :
 165    κ.C emp = 0 :=
 166  (κ.dichotomy emp).mpr emp_consistent
 167
 168/-- Cost is positive if and only if the configuration is inconsistent. -/
 169theorem cost_pos_iff_inconsistent (κ : CostFunction Config) (Γ : Config) :
 170    0 < κ.C Γ ↔ ¬IsConsistent Γ := by
 171  constructor
 172  · intro h hc
 173    have h0 : κ.C Γ = 0 := (κ.dichotomy Γ).mpr hc
 174    linarith
 175  · intro hi
 176    have hne : κ.C Γ ≠ 0 := fun heq => hi ((κ.dichotomy Γ).mp heq)
 177    exact lt_of_le_of_ne (κ.nonneg Γ) (Ne.symm hne)

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.