Reproducibility package: The exact value of N(k,4) for binary words, a computer-assisted proof for combinatorics on words formalized in lean 4

This is a complete reproducibility package for the theorem N(k,4) = 4k for every integer k >= 11. A word is a k-power if it is the concatenation of k identical blocks, and a 4-antipower if it is the concatenation of four pairwise distinct blocks of equal length. N(k,4) denotes the least length N such that every binary word of length N contains a k-power or a 4-antipower as a factor. The theorem resolves a conjecture of Jeffrey Shallit, recorded as Conjecture 6.1 in Samin Riasat's 2019 MMath thesis and as Remark 3 of Fleischer, Riasat and Shallit (Information Processing Letters 164 (2020), 106021). Both previously known bounds are due to others and are recalled rather than claimed here: the lower bound N(k,4) >= 4k is the case r = 4 of Fleischer, Riasat and Shallit's N(k,r) >= (2r-4)k, and the linear upper bound N(k,4) <= 72k+96 is the case r = 4 of Theorem 1.3(1)(a) of Riasat's thesis. The exact values are likewise largely known: Appendix A of that thesis tabulates N(k,4) for every k <= 30. The contribution here is the classification of the extremal words of length 4k-1 for k >= 11, the matching upper bound N(k,4) <= 4k that follows from it, the exact values at k = 31 and k = 32, and the formalization. The proof proceeds by classification: for k >= 11 the only binary words of length 4k-1 avoiding both structures are x_k = (01)^(k-1) 000 (10)^(k-1) and its complement. The classification is proved by induction on k, with an exhaustive base for 11 <= k <= 42. The package contains the full mathematical write-up; three code-independent verifiers for the finite base, namely two independently written C++ prefix-enumeration programs implementing the same search strategy and a structurally independent whole-word SAT encoding; programs and captured outputs for the exact values 2 <= k <= 32; a script verifying the period-3 certificate table; an audit of the uniform lemmas; SHA-256 checksums for every file; the complete Lean 4 formalization with a captured build and axiom-audit transcript; the manuscript in source and PDF form; and run_all_checks.sh, a single command that runs every check the archive can perform on its own and reports PASS/FAIL. The Lean development contains no 'sorry'. The deductive content of the proof, including the soundness of the search checker, is verified by the Lean kernel; the 32 base-case evaluations are admitted through native_decide and two finite period-3 decisions through bv_decide, both of which are trusted rather than kernel-reduced. The captured #print axioms output is included. This proof does not provide a computation-free derivation, since its base range is established computationally in the mathematical argument as well; whether some future argument settles those cases without computation is open.