gistfile1.txt

/-! ### Move runs -/

/-- `k` left moves: `(a, b) ⇝ (2^k a, b + k)`. -/
theorem reach_M1s (k a b : Nat) : Reaches (a, b) (2^k * a, b + k) := by
  induction k with
  | zero => simpa using Reaches.refl (a, b)
  | succ k ih =>
    refine ih.tail (Step.left' ?_ rfl)
    calc 2^(k+1) * a = 2^k * 2 * a := by rw [Nat.pow_succ]
      _ = 2 * (2^k * a) := by rw [Nat.mul_comm (2^k) 2, Nat.mul_assoc]

/-- `k` right moves: `(a, b) ⇝ (a + k, 2^k b)`. -/
theorem reach_M2s (k a b : Nat) : Reaches (a, b) (a + k, 2^k * b) := by
  induction k with
  | zero => simpa using Reaches.refl (a, b)
  | succ k ih =>
    refine ih.tail (Step.right' rfl ?_)
    calc 2^(k+1) * b = 2^k * 2 * b := by rw [Nat.pow_succ]
      _ = 2 * (2^k * b) := by rw [Nat.mul_comm (2^k) 2, Nat.mul_assoc]

/-! ### Good lines

`GoodP t`: every point of the line `b = 2a + t` terminates.
`GoodN u`: every point of the line `b = 2a - u` (i.e. `2a = b + u`) terminates.
Together: every slope-2 line, of any integer offset. -/

def GoodP (t : Nat) : Prop := ∀ a, Terminates (a, 2*a + t)

def GoodN (u : Nat) : Prop := ∀ a b, 2*a = b + u → Terminates (a, b)

/-- Seed: offset 1 (family F₁). -/
theorem goodP_one : GoodP 1 := fun a => fin_p1 a

/-- Seed: offset 2 (family F₂). -/
theorem goodP_two : GoodP 2 := fun a => fin_p2 a

/-- Seed: offset −1 (family F₋₁). -/
theorem goodN_one : GoodN 1 := by
  intro a b hab
  match a, hab with
  | a'+1, hab =>
    have e : b = 2*a' + 1 := by omega
    rw [e]; exact fin_m1 a'

/-- HALF: `M2^j` then `M1^j` carries the offset-`2j` line to the offset-`j` line:
`(a, 2a+2j) ⇝ (a+j, 2^{j+1}(a+j)) ⇝ (2^j(a+j), 2^{j+1}(a+j)+j)`. -/
theorem half (j : Nat) (h : GoodP j) : GoodP (2*j) := by
  intro a
  have e : 2*a + 2*j = 2*(a + j) := by omega
  rw [e]
  have r1 : Reaches (a, 2*(a+j)) (a + j, 2^j * (2*(a+j))) := reach_M2s j a _
  have r2 : Reaches (a + j, 2^j * (2*(a+j))) (2^j * (a+j), 2^j * (2*(a+j)) + j) :=
    reach_M1s j _ _
  have happ : Terminates (2^j * (a+j), 2*(2^j*(a+j)) + j) := h _
  have e2 : 2^j * (2*(a+j)) = 2*(2^j*(a+j)) := Nat.mul_left_comm _ _ _
  rw [e2] at r1 r2
  exact Terminates.of_reaches (r1.trans r2) happ

/-- REFL⁺: two left moves send the offset-`t` line into the *mirrored*
offset-`-(2t+4)` line: `(a, 2a+t) ⇝ (4a, 2a+t+2)` and `2(2a+t+2) = 4a + (2t+4)`. -/
theorem reflP (t : Nat) (h : GoodN (2*t + 4)) : GoodP t := by
  intro a
  have s1 : Step (a, 2*a + t) (2*a, 2*a + t + 1) := Step.left' rfl rfl
  have s2 : Step (2*a, 2*a + t + 1) (4*a, 2*a + t + 2) :=
    Step.left' (by omega) rfl
  have hterm : Terminates (2*a + t + 2, 4*a) := h _ _ (by omega)
  exact Terminates.of_reaches ((Reaches.single s1).trans (Reaches.single s2)) hterm.swap

/-- REFL⁻: two left moves send the mirrored offset-`-u` line into the
offset-`2u-4` line (stated with `2u = v + 4` to stay in ℕ). -/
theorem reflN (u v : Nat) (hv : 2*u = v + 4) (h : GoodP v) : GoodN u := by
  intro a b hab
  have s1 : Step (a, b) (2*a, b + 1) := Step.left' rfl rfl
  have s2 : Step (2*a, b + 1) (4*a, b + 2) := Step.left' (by omega) rfl
  have hterm : Terminates (b + 2, 4*a) := by
    have hp := h (b + 2)
    have e : 2*(b+2) + v = 4*a := by omega
    rwa [e] at hp
  exact Terminates.of_reaches ((Reaches.single s1).trans (Reaches.single s2)) hterm.swap

/-- Offset 4 is good (halving from seed 2). -/
theorem goodP_four : GoodP 4 := by
  have h := half 2 goodP_two
  simpa using h

/-- Offset 0 is good: `0 ⟸ᴿ −4 ⟸ᴿ 4 ⟸ᴴ 2`. -/
theorem goodP_zero : GoodP 0 := by
  have gn4 : GoodN 4 := reflN 4 4 (by omega) goodP_four
  have h := reflP 0 (by simpa using gn4)
  exact h

/-- Every nonnegative slope-2 offset is good.  Strong induction on the offset:
even offsets halve (HALF); an odd offset `t` follows the chain
`(t+1)/2 →ᴴ t+1 →ᴴ 2t+2 →ᴴ 4t+4 →ᴿ⁻ −(2t+4) →ᴿ⁺ t`. -/
theorem goodP_all : ∀ t, GoodP t := by
  have H : ∀ n t, t ≤ n → GoodP t := by
    intro n
    induction n with
    | zero =>
      intro t ht
      have e : t = 0 := by omega
      rw [e]; exact goodP_zero
    | succ n ihn =>
      intro t ht
      match t with
      | 0 => exact goodP_zero
      | 1 => exact goodP_one
      | 2 => exact goodP_two
      | (t+3) =>
        cases Nat.mod_two_eq_zero_or_one (t+3) with
        | inl heven =>
          -- t+3 = 2j with j < t+3
          have hj : t + 3 = 2 * ((t+3)/2) := by omega
          have g := half ((t+3)/2) (ihn ((t+3)/2) (by omega))
          rwa [← hj] at g
        | inr hodd =>
          -- t+3 odd, so t+4 = 2w
          have hw : t + 4 = 2 * ((t+4)/2) := by omega
          have g1 : GoodP ((t+4)/2) := ihn ((t+4)/2) (by omega)
          have g2 : GoodP (t+4) := by
            have := half ((t+4)/2) g1; rwa [← hw] at this
          have g3 : GoodP (2*(t+4)) := half (t+4) g2
          have g4 : GoodP (2*(2*(t+4))) := half (2*(t+4)) g3
          have gn : GoodN (2*(t+3) + 4) :=
            reflN (2*(t+3) + 4) (2*(2*(t+4))) (by omega) g4
          exact reflP (t+3) gn
  exact fun t => H t t (Nat.le_refl t)

/-- Every negative slope-2 offset is good. -/
theorem goodN_all : ∀ u, GoodN u
  | 0 => fun a b hab => by
      have e : b = 2*a + 0 := by omega
      rw [e]; exact goodP_all 0 a
  | 1 => goodN_one
  | (u+2) => reflN (u+2) (2*u) (by omega) (goodP_all (2*u))

/-! ### Main theorem -/

/-- **The process can always be steered to termination**: from every starting
pair `(a, b)` there is a sequence of moves reaching the diagonal. -/
theorem terminates_all (a b : Nat) : Terminates (a, b) := by
  by_cases h : 2*a ≤ b
  · have g := goodP_all (b - 2*a) a
    have e : 2*a + (b - 2*a) = b := by omega
    rwa [e] at g
  · exact goodN_all (2*a - b) a b (by omega)


/-- A move choice that avoids landing on the diagonal (possible from any
off-diagonal state). -/
def avoid (s : Nat × Nat) : Nat × Nat :=
  if 2*s.1 = s.2 + 1 then (s.1 + 1, 2*s.2) else (2*s.1, s.2 + 1)

theorem avoid_step (s : Nat × Nat) : Step s (avoid s) := by
  obtain ⟨a, b⟩ := s
  unfold avoid
  by_cases h : 2*a = b + 1
  · simp only [if_pos h]
    exact Step.right a b
  · simp only [if_neg h]
    exact Step.left a b

theorem avoid_ne {s : Nat × Nat} (h : s.1 ≠ s.2) :
    (avoid s).1 ≠ (avoid s).2 := by
  obtain ⟨a, b⟩ := s
  have h' : a ≠ b := h
  simp only [avoid]
  by_cases h1 : 2*a = b + 1
  · rw [if_pos h1]
    -- (a+1, 2b) on the diagonal would need a+1 = 2b with 2a = b+1 ⇒ a = b = 1,
    -- contradicting a ≠ b.
    show a + 1 ≠ 2*b
    omega
  · rw [if_neg h1]
    show 2*a ≠ b + 1
    exact h1

/-- The infinite avoiding orbit. -/
def orbit (s : Nat × Nat) : Nat → Nat × Nat
  | 0 => s
  | n+1 => avoid (orbit s n)

/-- Under adversarial choices, no off-diagonal start is forced to terminate:
there is an infinite play never touching the diagonal. -/
theorem escape_forever {a b : Nat} (h : a ≠ b) :
    ∃ f : Nat → Nat × Nat, f 0 = (a, b) ∧
      (∀ n, Step (f n) (f (n+1))) ∧ (∀ n, (f n).1 ≠ (f n).2) := by
  refine ⟨orbit (a, b), rfl, fun n => avoid_step _, ?_⟩
  intro n
  induction n with
  | zero => exact h
  | succ n ih => exact avoid_ne ih