cost_ne_zero_of_inconsistent
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.
claimLet $κ$ 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 in Recognition Science
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.
scope and limits
- Does not assign explicit numerical values to cost beyond nonnegativity.
- Does not apply to configurations that fail independent additivity.
- Does not address dependent or overlapping configurations.
- Does not derive the value of cost on consistent configurations beyond zero.
formal statement (Lean)
190theorem cost_ne_zero_of_inconsistent (κ : CostFunction Config) (Γ : Config)
191 (h : ¬IsConsistent Γ) : κ.C Γ ≠ 0 := by
proof body
Term-mode proof.
192 have := cost_pos_of_inconsistent κ Γ h
193 linarith
194
195/-! ### Three-way and finite-pairwise-independent additivity -/
196
197/-- Cost is additive over three pairwise-independent configurations.
198This is the building block for finite induction. The pairwise
199hypotheses `_h₁₂`, `_h₁₃` are stated for readability but only the
200joint independence `h₁_join` and the pair-independence `h₂₃` are used
201in the proof, since the pairwise structure is encoded in the join. -/