consistent_minimum_cost
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive classical logic itself from cost minimization.
- Does not apply to configurations that assert both P and ¬P.
- Does not give an explicit closed-form expression for consistent_cost beyond its identification with defect.
- Does not address systems containing multiple interacting propositions.
formal statement (Lean)
204theorem consistent_minimum_cost (c : ConsistentConfig) :
205 consistent_cost c ≥ 0 ∧ (consistent_cost c = 0 ↔ c.ratio = 1) := by
proof body
Term-mode proof.
206 constructor
207 · exact defect_nonneg c.ratio_pos
208 · exact defect_zero_iff_one c.ratio_pos
209
210/-! ## Logic Emerges from Cost -/
211
212/-- **THE MAIN THEOREM**: Logic is the structure of cost minimization.
213
214 1. Contradictions cannot have zero cost (they're unstable)
215 2. Consistent propositions can have zero cost (they can stabilize)
216 3. Therefore: the stable configurations are the logically consistent ones
217 4. Therefore: logic = the structure of what can exist = what minimizes cost
218
219 This proves: logical consistency is not imposed from outside.
220 It emerges from the cost landscape. Logic is cheap. -/