Prescribed digit sums in residue classes and a conjecture of Murthy (OEIS A077754)

We prove an equidistribution theorem for numbers with all-nonzero decimal digits and prescribed digit sum and residue class. As a corollary, we resolve Murthy's conjecture (OEIS A077754, 2002): an integer n admits a multiple with at least two nonzero digits and digit sum n iff n is not in {1, 2, 5, 11} ∪ 10ℕ. The corollary is fully machine-verified in Lean 4 with mathlib (theorem A077754, zero sorry). The deposit includes the paper (paper.pdf), the complete Lean formalization (A077754.lean, CornerTable.lean), an independent Python verifier (~90 lines, stdlib) re-deriving all finite certificates, and the pinned build files (lakefile.toml, lake-manifest.json, lean-toolchain) for long-term reproducibility.