`ConsistentConfig`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.LogicFromCost
domain: Foundation
line: 182 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.LogicFromCost on GitHub at line 182.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 179
 180/-- A consistent configuration: P without ¬P asserted.
 181    This can achieve zero cost. -/
 182structure ConsistentConfig where
 183  /-- The proposition P -/
 184  P : Prop
 185  /-- The ratio for P -/
 186  ratio : ℝ
 187  /-- Ratio is positive -/
 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.

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.