RecognitionWorkConstraintCert

formal source

 356component constrains the cost on all independent extensions of that
 357configuration.
 358-/
 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. -/
 380def recognition_work_constraint_cert
 381    (κ : CostFunction Config) :
 382    RecognitionWorkConstraintCert Config where
 383  κ := κ
 384  emp_zero := emp_cost_zero κ
 385  pos_iff_inconsistent := cost_pos_iff_inconsistent κ
 386  additive_indep := κ.additivity
 387  uniqueness := uniqueness_on_indep_decomposition κ
 388
 389/--