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-/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.