cost_pos_iff_inconsistent
plain-language theorem explainer
Cost is positive precisely when a configuration is inconsistent. Recognition theorists cite the equivalence to separate zero-cost consistent states from positive-cost inconsistent ones under the recognition-work axioms. The proof is a direct biconditional split that invokes the dichotomy axiom in each direction together with non-negativity of C.
Claim. Let $κ$ be a cost function on a configuration space. For any configuration $Γ$, $0 < κ.C(Γ) ↔ ¬IsConsistent(Γ)$.
background
The module formalises the recognition-work constraint theorem from the T-1 → T0 bridge paper. A CostFunction on ConfigSpace consists of a map C : Config → ℝ together with three axioms: nonnegativity (0 ≤ C Γ for all Γ), the dichotomy (C Γ = 0 ↔ IsConsistent Γ), and independent additivity (C(join Γ₁ Γ₂) = C Γ₁ + C Γ₂ whenever Γ₁ and Γ₂ are independent). The local setting therefore treats cost as the quantitative measure of recognition work required to resolve inconsistency.
proof idea
The term proof applies constructor to split the biconditional. Forward direction: assume 0 < κ.C Γ, suppose IsConsistent Γ for contradiction, then dichotomy gives κ.C Γ = 0 and linarith yields the desired falsehood. Reverse direction: assume ¬IsConsistent Γ, then dichotomy implies κ.C Γ ≠ 0; nonnegativity plus lt_of_le_of_ne produces the strict inequality.
why it matters
The equivalence supplies the positive-cost direction needed by cost_pos_of_inconsistent and by the master certificate recognition_work_constraint_cert. It therefore closes the recognition-work constraint step in the foundation module, directly supporting the dichotomy axiom that characterises the T0 base of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.