additive_emp_left
plain-language theorem explainer
The theorem states that for any cost function κ the cost of joining the empty configuration on the left to Γ equals the cost of Γ. Researchers formalizing the recognition-work bridge would cite this as the left-unit case of independent additivity. The proof is a one-line rewrite using the emp_join identity.
Claim. Let κ be a cost function on a configuration space satisfying the dichotomy and independent-additivity axioms. For any configuration Γ, κ.C(join(∅, Γ)) = κ.C(Γ).
background
A CostFunction κ on Config consists of a map C : Config → ℝ together with proofs that C is nonnegative, that C(Γ) = 0 if and only if Γ is consistent (dichotomy), and that C(join(Γ₁, Γ₂)) = C(Γ₁) + C(Γ₂) whenever Γ₁ and Γ₂ are independent (independent additivity). The module CostFromDistinction formalizes the T-1 → T0 bridge by imposing this quantitative structure on recognition work. The two Config structures imported from Gravity.ILG and Modal.Possibility supply concrete realizations of the join and independence operations used in the statement.
proof idea
The proof is a one-line wrapper that applies the emp_join lemma to rewrite the left-hand side directly into the right-hand side.
why it matters
This supplies the left-unit property required by the independent-additivity axiom inside the recognition-work constraint theorem. It closes the degenerate case of the empty configuration so that cost decomposes cleanly over independent inconsistent components. The module's main result, recognition_work_constraint_theorem, depends on such unit properties to conclude that cost is uniquely determined by its values on indecomposable inconsistent generators.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.