consistent_minimum_cost
plain-language theorem explainer
Consistent configurations achieve non-negative cost with equality to zero precisely when the ratio equals one. Researchers deriving logic from cost minimization cite this as the base stability result. The proof is a direct term application of the defect non-negativity and zero-characterization lemmas to the configuration ratio.
Claim. Let $c$ be a consistent configuration with positive ratio $r$. Then the cost of $c$ satisfies $cost(c) ≥ 0$, and $cost(c) = 0$ if and only if $r = 1$.
background
In the LogicFromCost module a ConsistentConfig is a structure carrying a proposition P, a positive real ratio r, and the proof that r > 0. The cost of such a configuration is the defect function applied to r, where defect(x) = (x + x^{-1})/2 - 1. This module shows logical consistency emerges as the structure of cost-minimizing states: consistent propositions can reach zero defect while contradictions cannot. Upstream results supply the needed facts: defect_nonneg states that defect(x) ≥ 0 whenever x > 0, and defect_zero_iff_one states that defect(x) = 0 if and only if x = 1 for x > 0.
proof idea
The proof is a term-mode wrapper. Constructor splits the conjunction into the inequality and the equivalence. The first conjunct is discharged by exact defect_nonneg applied to the ratio_pos field. The second conjunct is discharged by exact defect_zero_iff_one applied to the same field.
why it matters
This is Theorem 5 of the module, the base case for the claim that logic is the structure of cost minimization. It feeds the module's main argument that stable configurations are exactly the logically consistent ones and that contradictions carry positive cost. In the Recognition Science chain it supplies the concrete link between J-cost minima and the emergence of consistency without imposing classical logic from outside the cost landscape.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.