consistent_zero_cost_possible
Consistent configurations reach zero cost at ratio 1. Researchers deriving logic from cost minimization cite this to separate stable propositions from contradictions. The proof is a direct term construction that supplies a ConsistentConfig with ratio 1 and applies the defect_at_one lemma.
claimThere exists a consistent configuration $c$ such that the defect of its ratio is zero: $c = (P, r)$ with $r > 0$ and defect$(r) = 0$.
background
The LogicFromCost module shows that logical consistency emerges as the structure of cost-minimizing configurations. A ConsistentConfig is a structure holding a proposition P together with a positive real ratio; its cost is defined as defect of that ratio. The upstream defect_at_one theorem states that defect 1 = 0, which is the minimum value of the defect function derived from the J-cost.
proof idea
The proof is a term-mode construction. It builds the tuple ⟨True, 1, norm_num⟩ to witness a ConsistentConfig and then unfolds consistent_cost to reduce directly to defect_at_one.
why it matters in Recognition Science
This supplies the existence half of logic_from_cost and logic_from_cost_summary, which together establish that consistency achieves zero cost while contradictions cannot. It supports the Recognition Science claim that logic is the structure of J-cost minima, specifically the fixed point at ratio 1.
scope and limits
- Does not assert that every consistent configuration has zero cost.
- Does not prove the impossibility of contradictory configurations.
- Does not derive the full logic_from_cost theorem.
Lean usage
have h : ∃ c : ConsistentConfig, consistent_cost c = 0 := consistent_zero_cost_possibleformal statement (Lean)
197theorem consistent_zero_cost_possible :
198 ∃ c : ConsistentConfig, consistent_cost c = 0 := by
proof body
Term-mode proof.
199 use ⟨True, 1, by norm_num⟩
200 unfold consistent_cost
201 exact defect_at_one
202
203/-- **THEOREM 5**: The minimum cost for consistency is 0, achieved at ratio = 1. -/