cost_ne_zero_of_inconsistent
plain-language theorem explainer
Inconsistent configurations have nonzero cost under any cost function obeying the recognition-work axioms. Researchers formalizing the T-1 to T0 bridge in Recognition Science cite this to confirm that cost vanishes exactly on consistent configurations. The proof is a one-line wrapper that invokes the positive-cost lemma for inconsistent inputs and finishes with linear arithmetic.
Claim. Let $κ$ be a cost function on a configuration space. If configuration $Γ$ is inconsistent, then $κ.C(Γ) ≠ 0$.
background
The module CostFromDistinction formalizes the recognition-work constraint theorem that bridges T-1 to T0. A CostFunction consists of a map $C$ from configurations to nonnegative reals together with the dichotomy axiom (cost zero if and only if the configuration is consistent) and the independent-additivity axiom (cost of a join equals the sum of costs when the joined configurations share no predicates). The upstream lemma cost_pos_of_inconsistent already shows that inconsistent configurations carry strictly positive cost; the present result converts that strict inequality into a nonzero statement.
proof idea
The proof is a one-line wrapper. It applies the lemma cost_pos_of_inconsistent to obtain the strict inequality $0 < κ.C Γ$ and then invokes linarith to reach the desired nonzero conclusion.
why it matters
This theorem completes the dichotomy half of the recognition-work constraint inside the CostFromDistinction module. It guarantees that cost is nonzero precisely when a configuration is inconsistent, which is required for the uniqueness-on-indep-decomposition result and for the overall recognition-work constraint theorem stated in the module documentation. The result sits directly on the T-1 to T0 bridge and supplies the quantitative distinction that turns the satisfiability dichotomy into a genuine cost function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.