pith. machine review for the scientific record. sign in
structure definition def or abbrev

CostFunction

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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. -/

used by (16)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (23)

Lean names referenced from this declaration's body.