 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/--
 390**Recognition-Work Constraint Theorem (formal headline).**
 391
 392There exists a master certificate of the recognition-work constraint
 393on any configuration space and any cost function satisfying the two
 394bridge axioms. The certificate makes the constraint explicit:
 395
 3961. The empty configuration has zero cost.
 3972. Cost is positive iff inconsistent.
 3983. Cost is additive over independent joins.
 3994. Two cost functions agreeing on a generating set agree on all
 400   independent decompositions.
 401
 402This formalises the substantive constraint that the recognition-work
 403primitive places on the cost function. Without independent
 404additivity (axiom A), the dichotomy alone (axiom D) is just a binary
 405stipulation. With both axioms, the cost function is constrained to
 406factor through the independent-decomposition structure of the
 407configuration space.
 408-/
 409theorem recognition_work_constraint_theorem
 410    (κ : CostFunction Config) :

papers checked against this theorem

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