cost_pos_of_inconsistent
plain-language theorem explainer
Inconsistent configurations incur strictly positive cost under any cost function satisfying the dichotomy and independent-additivity axioms. Researchers formalizing the recognition-work constraint would cite this when establishing that inconsistency forces nonzero recognition cost. The proof is a one-line wrapper applying the right-to-left direction of the related iff statement.
Claim. Let $κ$ be a cost function on a configuration space satisfying dichotomy and independent additivity. For any configuration $Γ$, if $Γ$ is inconsistent then $0 < κ.C(Γ)$.
background
The module formalizes the recognition-work constraint from the T-1 to T0 bridge paper. A CostFunction $κ$ on ConfigSpace satisfies two axioms: (D) dichotomy, $κ.C(Γ) = 0$ if and only if $Γ$ is consistent, and (A) independent additivity, $κ.C(join Γ₁ Γ₂) = κ.C(Γ₁) + κ.C(Γ₂)$ whenever Γ₁ and Γ₂ are independent. The upstream theorem cost_pos_iff_inconsistent states that $0 < κ.C(Γ) ↔ ¬IsConsistent Γ, proved by applying the dichotomy axiom in both directions and using linarith on the resulting equality to zero.
proof idea
The proof is a one-line wrapper that applies the right-to-left direction of cost_pos_iff_inconsistent to the hypothesis that Γ is inconsistent.
why it matters
This result feeds the downstream theorems additive_strict_of_both_inconsistent and cost_ne_zero_of_inconsistent, which derive strict inequality and nonzero cost for joins of inconsistent configurations. It fills the positivity direction inside the recognition_work_constraint_theorem of the module, reinforcing the T-1 to T0 bridge where recognition work enforces positive cost on inconsistent states. No open scaffolding remains here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.