emp_cost_zero
plain-language theorem explainer
The empty configuration has zero cost under any cost function obeying the dichotomy and independent-additivity axioms. Workers on the recognition-work constraint would cite this as the zero base case for all cost calculations in the T-1 to T0 bridge. The proof is a direct term application of the right-to-left direction of the dichotomy axiom to the consistency of the empty configuration.
Claim. Let $κ$ be a cost function on a configuration space. Then the cost of the empty configuration is zero: $κ(∅) = 0$.
background
This theorem belongs to the CostFromDistinction module, which formalizes the recognition-work constraint from RS_Cost_From_Distinction.tex. The module defines ConfigSpace as a typeclass supplying consistency, join, and independence. A CostFunction is a map C to non-negative reals obeying two axioms: dichotomy (C(Γ) = 0 iff Γ is consistent) and independent additivity (C(join Γ₁ Γ₂) = C(Γ₁) + C(Γ₂) when Γ₁ and Γ₂ share no predicates). The empty configuration emp is the join unit and is consistent by the ConfigSpace axioms. The CostFunction structure encodes these axioms directly, with its dichotomy field supplying the equivalence used here.
proof idea
The proof is a one-line term-mode wrapper. It applies the right-to-left implication of the dichotomy field of κ at the empty configuration, using the fact that emp is consistent.
why it matters
This supplies the emp_zero field inside recognition_work_constraint_cert, which packages the full constraint certificate from any valid cost function. It anchors the quantitative structure of the recognition-work bridge: costs start at zero on the empty case and accumulate only over inconsistent independent components. The result closes the gap identified in the module documentation, where the recognition-work narrative would otherwise reduce to a naming convention without the independent-additivity axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.