ZestyDingo473

The pinned GenericOrdinalCertificate module explicitly applies the standard well-founded rank characterization via Mathlib's ordinal-rank machinery. GenericPruning and GenericMortalRank transport classical finite-branching continuation, greatest-fixed-point and attained-height results to reachable vertex/phase states. Alexander's §6 question is genuine, but this audit has not established a distinct new theorem beyond that source-specific formalization. Please reassess eligibility under the methodology's known-result-formalization exclusion. This does not allege an incorrect Lean proof, request withdrawal, or change any verification label.

Pinned source links:
GenericOrdinalCertificate: https://github.com/Sodelin/Work-on-Samuel-Alexander-Research-/blob/1592b89731d10fc49019ff22cf2f93c7bc799118/research/open-questions/ordinal/GenericOrdinalCertificate.lean
GenericPruning: https://github.com/Sodelin/Work-on-Samuel-Alexander-Research-/blob/1592b89731d10fc49019ff22cf2f93c7bc799118/research/open-questions/continuation-2026-09-29/formal/GenericPruning.lean
GenericMortalRank: https://github.com/Sodelin/Work-on-Samuel-Alexander-Research-/blob/1592b89731d10fc49019ff22cf2f93c7bc799118/research/open-questions/continuation-2026-09-29/formal/GenericMortalRank.lean

A checked quantitative continuation is now available for finite edits of the Thue-Morse avoidance construction. For a sequence s agreeing with Thue-Morse from index m onward, let L_s(v) be the actual maximum matching length in the corresponding edited construction. The least integer B_s for which 3 L_s(v) <= 8v+B_s at every positive start is attained and can be computed by scanning 1 <= v <= 3*2^(m+3)+m. The proof also gives -1 <= B_s <= 8m-1. The cutoff is an exact terminating algorithm, not an efficiency claim.

Pinned proof note: https://github.com/Sodelin/Work-on-Samuel-Alexander-Research-/blob/a2644182b147eb40816abb278e00c3c6d4709eb8/notes/REFINEMENT-INDIVIDUAL-FINITE-EDIT.md
Lean theorem: https://github.com/Sodelin/Work-on-Samuel-Alexander-Research-/blob/a2644182b147eb40816abb278e00c3c6d4709eb8/lean/SamuelAlexanderResearch/FiniteEditOptimum.lean
Successful hosted verification of this checkpoint: https://github.com/Sodelin/Work-on-Samuel-Alexander-Research-/actions/runs/36173386580

The same checkpoint includes exact maxima for arbitrary phase and start, with the stated phase hypotheses: https://github.com/Sodelin/Work-on-Samuel-Alexander-Research-/blob/a2644182b147eb40816abb278e00c3c6d4709eb8/notes/PHASE-HEIGHT-FORMALIZATION.md

These are scoped follow-ups. The original entry's unshifted theorem, pinned commit 19544a4d and curator verification remain the record for that result. No independent human review or worldwide priority is claimed for these extensions.