cost_zero_of_consistent
Consistent configurations incur zero cost under any cost function obeying the dichotomy and independent-additivity axioms. A physicist deriving recognition costs or a mathematician verifying the T-1 to T0 bridge would cite this to drop consistent states from cost calculations. The proof is a one-line application of the dichotomy axiom in the consistent-implies-zero direction.
claimLet $C$ be a cost function on a configuration space satisfying the dichotomy axiom. For any consistent configuration $Γ$, $C(Γ) = 0$.
background
CostFunction is the structure on a ConfigSpace that supplies a map $C$ from configurations to non-negative reals together with the two axioms of the recognition-work bridge: the dichotomy $C(Γ) = 0$ if and only if $Γ$ is consistent, and independent additivity $C(Γ_1 ∨ Γ_2) = C(Γ_1) + C(Γ_2)$ whenever $Γ_1$ and $Γ_2$ share no predicates. The module formalizes the substantive content of the T-1 → T0 bridge paper by showing that these two axioms alone force the cost framework; the module doc-comment notes that without independent additivity the recognition-work story would be merely a name for the dichotomy stipulation. The present theorem is the direct “consistent implies zero” half of the dichotomy property.
proof idea
The proof is the one-line term (κ.dichotomy Γ).mpr h, which applies the dichotomy field of the CostFunction structure in the reverse direction.
why it matters in Recognition Science
This result is invoked by the downstream theorem extension_to_consistent to conclude that cost functions agreeing on a calibration witness agree on all independent extensions by consistent configurations. It supplies the basic zero-cost property required by the recognition-work constraint theorem in the T-1 → T0 bridge, confirming that consistent configurations contribute no recognition work and thereby allowing the cost of any configuration to be reduced to the sum of costs of its inconsistent indecomposable components.
scope and limits
- Does not prove existence of cost functions satisfying the axioms.
- Does not compute explicit positive costs for inconsistent configurations.
- Does not depend on concrete models such as ILG or modal Config.
- Does not address infinite or non-independent joins.
formal statement (Lean)
180theorem cost_zero_of_consistent (κ : CostFunction Config) (Γ : Config)
181 (h : IsConsistent Γ) : κ.C Γ = 0 :=
proof body
Term-mode proof.
182 (κ.dichotomy Γ).mpr h
183
184/-- Inconsistent configurations have positive cost. -/