IsStable

formal source

  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
 101  /-- The proposition P -/
 102  P : Prop
 103  /-- Ratio for P -/
 104  ratio_P : ℝ
 105  /-- Ratio for ¬P (should be complementary) -/
 106  ratio_notP : ℝ
 107  /-- Both ratios positive -/
 108  ratio_P_pos : ratio_P > 0
 109  ratio_notP_pos : ratio_notP > 0
 110  /-- Complementarity: the product is 1 -/
 111  complementary : ratio_P * ratio_notP = 1
 112