Two-fold Langford sequences exist exactly when 3l >= 2d - 1: a Lean 4 proof, with the m-fold counting bound attained for every m