def
definition
consistent_cost
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.LogicFromCost on GitHub at line 191.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
188 ratio_pos : ratio > 0
189
190/-- The cost of a consistent configuration. -/
191noncomputable def consistent_cost (c : ConsistentConfig) : ℝ := defect c.ratio
192
193/-- **THEOREM 4**: Consistent configurations can have zero cost.
194
195 Unlike contradictions, a single proposition can stabilize at ratio = 1.
196 This is the minimum-cost state for a proposition. -/
197theorem consistent_zero_cost_possible :
198 ∃ c : ConsistentConfig, consistent_cost c = 0 := by
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. -/
204theorem consistent_minimum_cost (c : ConsistentConfig) :
205 consistent_cost c ≥ 0 ∧ (consistent_cost c = 0 ↔ c.ratio = 1) := by
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. -/
221theorem logic_from_cost :