Machine-checked Lean 4 proof of the general Courtade–Kumar inequality released