Exact spectrum of maximal decimal digit-sum multipliers below 12 for OEIS A277223, with two explicit infinite families at k = 7 and k = 11, fully formalized in Lean 4 and kernel-verified by a CI gate (lake build + leanchecker). Proofs developed with GLM 5.3 (Z.ai); all claims machine-checked.
-
Updated
Aug 29, 2026 - Lean