additive_emp_left

formal source

 228
 229/-- Cost is additive over independent join with the empty configuration
 230(degenerate case of independent additivity). -/
 231theorem additive_emp_left (κ : CostFunction Config) (Γ : Config) :
 232    κ.C (join emp Γ) = κ.C Γ := by
 233  rw [emp_join]
 234
 235theorem additive_emp_right (κ : CostFunction Config) (Γ : Config) :
 236    κ.C (join Γ emp) = κ.C Γ := by
 237  rw [join_emp]
 238
 239/-! ### The Recognition-Work Constraint Theorem -/
 240
 241/--
 242**Recognition-Work Constraint Theorem (uniqueness on independent
 243decompositions).**
 244
 245If two cost functions `κ₁` and `κ₂` on the same configuration space
 246agree on a set `S` of configurations, and if a configuration `Γ`
 247decomposes as the join of two `S`-elements that are independent of
 248each other, then `κ₁` and `κ₂` agree at `Γ`.
 249
 250This is the substantive content of the recognition-work primitive:
 251once cost is constrained to be additive over independent joins, the
 252cost function is uniquely determined by its restriction to a
 253generating set of "indecomposable" configurations. Recognition work
 254is therefore not just a binary stipulation; it forces the cost
 255function to factor through the independent-decomposition structure of
 256the configuration space.
 257-/
 258theorem uniqueness_on_indep_decomposition
 259    (κ₁ κ₂ : CostFunction Config)
 260    (S : Set Config)
 261    (h_agree : ∀ Γ ∈ S, κ₁.C Γ = κ₂.C Γ) :