cost_pos_of_inconsistent
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.
claimLet $κ$ 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 in Recognition Science
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.
scope and limits
- Does not compute explicit numerical cost values for any concrete configuration.
- Does not apply when the configuration is consistent.
- Does not extend additivity beyond the independent-join case already axiomatized.
- Does not depend on the concrete Config structures from Gravity.ILG or Modal.Possibility beyond the abstract ConfigSpace interface.
Lean usage
have hpos : 0 < κ.C Γ := cost_pos_of_inconsistent κ Γ hformal statement (Lean)
185theorem cost_pos_of_inconsistent (κ : CostFunction Config) (Γ : Config)
186 (h : ¬IsConsistent Γ) : 0 < κ.C Γ :=
proof body
Term-mode proof.
187 (cost_pos_iff_inconsistent κ Γ).mpr h
188
189/-- Inconsistent configurations have nonzero cost. -/