RSExists

formal source

  34noncomputable section
  35
  36/-- Recognition existence: `x` exists iff J(x) = 0. -/
  37def RSExists (x : ℝ) : Prop := Jcost x = 0
  38
  39/-- RSExists iff x = 1 (the unique J-cost minimiser). -/
  40theorem rsExists_iff_one {x : ℝ} (hx : 0 < x) :
  41    RSExists x ↔ x = 1 := by
  42  unfold RSExists
  43  constructor
  44  · intro h
  45    by_contra hne
  46    exact absurd h (ne_of_gt (Jcost_pos_of_ne_one x hx hne))
  47  · rintro rfl
  48    exact Jcost_unit0
  49
  50/-- Non-existence costs more than zero. -/
  51theorem non_existence_has_positive_cost {x : ℝ} (hx : 0 < x) (hne : x ≠ 1) :
  52    0 < Jcost x :=
  53  Jcost_pos_of_ne_one x hx hne
  54
  55/-- The unique "nothing" reference: cost is unbounded on (0,∞). -/
  56theorem divergence_at_zero_direction :
  57    ¬ ∃ (C : ℝ), ∀ (ε : ℝ), 0 < ε → Jcost ε ≤ C := by
  58  intro ⟨C, hC⟩
  59  -- Pick ε = 1/(2*(|C|+2)); then J(ε) > |C|+1 > C
  60  -- Actual proof: pick ε = 1/4, then J(1/4) = (1/4-1)²/(2·1/4) = (9/16)/(1/2) = 9/8
  61  -- That only bounds J away from C when C < 9/8.
  62  -- For large C, pick ε = 1/(C+2):
  63  -- J(1/(C+2)) = (1/(C+2)-1)²/(2/(C+2)) = (C+1)²/(C+2)²·(C+2)/2 = (C+1)²/(2(C+2))
  64  -- For C ≥ 0: (C+1)²/(2(C+2)) > C ↔ (C+1)² > 2C(C+2) = 2C²+4C ↔ C²+2C+1 > 2C²+4C ↔ 0 > C²+2C-1
  65  -- This fails for C ≥ 1. Need a better choice. Use ε = 1/(2C+4):
  66  -- J(1/(2C+4)) = (1/(2C+4)-1)²/(2/(2C+4)) = ((2C+3)/(2C+4))²·(2C+4)/2 = (2C+3)²/(2(2C+4))
  67  -- Compare with C: (2C+3)²/(2(2C+4)) > C ↔ (2C+3)² > 2C(2C+4) = 4C²+8C