RSPossible

formal source

  55def RSNecessary (x : ℝ) : Prop := 0 < x ∧ defect x = 0
  56
  57/-- **RSPossible**: x is possible iff it has positive ratio (finite J-cost). -/
  58def RSPossible (x : ℝ) : Prop := 0 < x
  59
  60/-- **RSActual**: x is actual iff it is RSNecessary (i.e., x = 1). -/
  61def RSActual (x : ℝ) : Prop := RSNecessary x
  62
  63/-- **RSImpossible**: x is impossible iff x ≤ 0 (violates ledger positivity). -/
  64def RSImpossible (x : ℝ) : Prop := x ≤ 0
  65
  66/-! ## I. Necessity = Unique J-Minimizer -/
  67
  68/-- **Theorem (Necessity is Unique)**:
  69    In RS, something is "necessary" iff it is the unique zero-defect configuration.
  70    Only x = 1 is necessary — there is exactly ONE necessary thing. -/
  71theorem necessity_is_unique_minimizer :
  72    -- Exactly one thing is necessary
  73    ∃! x : ℝ, RSNecessary x := by
  74  use 1
  75  constructor
  76  · exact ⟨by norm_num, defect_at_one⟩
  77  · intro y ⟨hy_pos, hy_zero⟩
  78    exact (defect_zero_iff_one hy_pos).mp hy_zero
  79
  80/-- **Theorem**: The necessary thing is x = 1 (the existent). -/
  81theorem necessary_is_one (x : ℝ) : RSNecessary x ↔ x = 1 := by
  82  constructor
  83  · intro ⟨hpos, hzero⟩; exact (defect_zero_iff_one hpos).mp hzero
  84  · intro h; rw [h]; exact ⟨by norm_num, defect_at_one⟩
  85
  86/-! ## II. Possibility = Positive Ratio -/
  87
  88/-- **Theorem (Possibility is Positive Ratio)**: