with

formal source

 347
 348/--
 349**Master certificate**: bundles the recognition-work constraint
 350theorem with its immediate consequences.
 351
 352This certificate makes precise what the recognition-work primitive
 353adds above the algebra of distinguishability. It is non-vacuous: the
 354calibration component picks out a specific inconsistent
 355configuration with a specific positive cost, and the additivity
 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