add_event_balanced_list

formal source

 279
 280/-- **THEOREM (Balance Preservation)**: Adding an event and its reciprocal to a balanced
 281    list preserves the balance property. -/
 282theorem add_event_balanced_list (l : List RecognitionEvent) (h : balanced_list l) (e : RecognitionEvent) :
 283    balanced_list (e :: reciprocal e :: l) := by
 284  intro x
 285  unfold balanced_list at h
 286  -- The new list is e :: reciprocal e :: l
 287  -- count x in this list = (if x = e then 1 else 0) + (if x = reciprocal e then 1 else 0) + count x l
 288  simp only [List.count_cons]
 289  -- Using h: count x l = count (reciprocal x) l
 290  rw [h x]
 291  -- Now need: (e == x) + (reciprocal e == x) = (e == reciprocal x) + (reciprocal e == reciprocal x)
 292  -- where == is decidable equality (beq)
 293  -- This follows from the symmetry: x ↔ reciprocal x swaps e and reciprocal e
 294  -- Specifically: (e == x) = (reciprocal e == reciprocal x) and (reciprocal e == x) = (e == reciprocal x)
 295  -- Using: x = e ↔ reciprocal x = reciprocal e, and x = reciprocal e ↔ reciprocal x = e
 296  have key1 : (e == x) = (reciprocal e == reciprocal x) := by
 297    -- e == x ↔ e = x (since DecidableEq RecognitionEvent)
 298    -- e = x ↔ reciprocal e = reciprocal x (by reciprocal_inj symmetry)
 299    cases h1 : e == x
 300    · -- e ≠ x
 301      have hne : e ≠ x := by simpa using h1
 302      have hne' : reciprocal e ≠ reciprocal x := fun h => hne ((reciprocal_inj e x).mp h)
 303      simp [hne', beq_eq_false_iff_ne]
 304    · -- e = x
 305      have heq : e = x := by simpa using h1
 306      have heq' : reciprocal e = reciprocal x := by rw [heq]
 307      simp [heq']
 308  have key2 : (reciprocal e == x) = (e == reciprocal x) := by
 309    cases h2 : reciprocal e == x
 310    · -- reciprocal e ≠ x
 311      have hne : reciprocal e ≠ x := by simpa using h2
 312      have hne' : e ≠ reciprocal x := fun h => hne (by rw [← reciprocal_reciprocal x, h, reciprocal_reciprocal])