PropConfig

formal source

  67    - ratio = 1: perfectly balanced (true and stable)
  68    - ratio → 0: completely absent (false)
  69    - ratio → ∞: unbounded assertion (unstable) -/
  70structure PropConfig where
  71  /-- The proposition -/
  72  prop : Prop
  73  /-- The configuration ratio (how "present" the proposition is) -/
  74  ratio : ℝ
  75  /-- The ratio is positive -/
  76  ratio_pos : ratio > 0
  77
  78/-- The cost of a propositional configuration. -/
  79noncomputable def prop_cost (c : PropConfig) : ℝ := defect c.ratio
  80
  81/-- A configuration is stable if its cost is zero. -/
  82def IsStable (c : PropConfig) : Prop := prop_cost c = 0
  83
  84/-- A configuration is unstable if its cost is positive. -/
  85def IsUnstable (c : PropConfig) : Prop := prop_cost c > 0
  86
  87/-! ## Contradiction Has Infinite Cost -/
  88
  89/-- A contradiction configuration: both P and ¬P are asserted.
  90
  91    In RS terms, this would require:
  92    - A config for P with ratio r
  93    - A config for ¬P with ratio 1/r (complementary)
  94    - Both to be stable (cost = 0)
  95
  96    But if P is stable at ratio 1, then ¬P would need ratio 1 too.
  97    And if both are "true", we have P ∧ ¬P = False.
  98
  99    The key insight: complementary ratios can't both be 1. -/
 100structure ContradictionConfig where