`heavy-ball-lean` is a Lean 4 / Mathlib library formalising a certified convergence argument for the heavy ball method, also known as Polyak momentum. The library works over a real inner product space, packages smoothness and strong-convexity assumptions, defines the classical constant parameters, records a momentum update and Lyapunov energy, and proves geometric decay of the certified energy and function-value gap. The method is a Lyapunov-energy proof of linear convergence for a certified heavy-ball orbit. The development is machine-checked in Lean 4 with zero `sorry`, zero `admit`, and standard Lean/Mathlib axioms only.