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

RecognitionWorkConstraintCert

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)

 359structure RecognitionWorkConstraintCert
 360    (Config : Type u) [ConfigSpace Config] where
 361  /-- A cost function on the configuration space. -/
 362  κ : CostFunction Config
 363  /-- Empty cost is zero (immediate from dichotomy + emp_consistent). -/
 364  emp_zero : κ.C emp = 0
 365  /-- Cost-positivity characterises inconsistency. -/
 366  pos_iff_inconsistent : ∀ Γ, 0 < κ.C Γ ↔ ¬IsConsistent Γ
 367  /-- Cost is additive over independent joins. -/
 368  additive_indep : ∀ Γ₁ Γ₂, Independent Γ₁ Γ₂ →
 369    κ.C (join Γ₁ Γ₂) = κ.C Γ₁ + κ.C Γ₂
 370  /-- Cost is uniquely determined on independent decompositions by
 371      its values on the components. -/
 372  uniqueness :
 373    ∀ (κ₂ : CostFunction Config) (S : Set Config),
 374      (∀ Γ ∈ S, κ.C Γ = κ₂.C Γ) →
 375      ∀ Γ₁ Γ₂, Γ₁ ∈ S → Γ₂ ∈ S → Independent Γ₁ Γ₂ →
 376        κ.C (join Γ₁ Γ₂) = κ₂.C (join Γ₁ Γ₂)
 377
 378/-- Construct the master constraint certificate from any cost function
 379satisfying the dichotomy and independent-additivity axioms. -/

used by (2)

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

depends on (21)

Lean names referenced from this declaration's body.