consistent_zero_cost_possible
plain-language theorem explainer
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.
Claim. There 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.