Specular Reflection in Spectral Fokker-Planck: A Penalty Method with Proven Convergence

We identify and resolve a fundamental error in spectral methods for kinetic Fokker--Planck equations. The standard cosine (Neumann) basis enforces \(\partial p/\partial x = 0\) at spatial boundaries, which is the correct reflecting boundary condition for overdamped (position-only) dynamics. For kinetic systems with velocity (\(\partial_t p + v\partial_x p + F\partial_v p = D\partial^2_v p\)), the physical reflecting condition is specular reflection: \(p(x_b, -v) = p(x_b, v)\). We prove (with counterexample) that Neumann does NOT imply specular reflection --- the two conditions are mathematically distinct. We propose a penalty method: add \(-\lambda P\) to the generator, where \(P\) projects onto the odd-in-velocity component at the boundary. The key observation is that the cosine basis satisfies \(\varphi_b(-v) = (-1)^b \varphi_b(v)\), so \(P\) simply penalizes odd-indexed velocity modes at boundary x-points. We prove: (1) the penalized generator is dissipative (all eigenvalues \(\leq 0\)), (2) the convergence rate is \(O(\rho^{-N} + 1/\lambda)\) with optimal \(\lambda = \rho^N\), (3) the kinetic spectral gap is bounded below by the overdamped gap divided by \((1 + v_{\max}^2/D)\). All results are formally verified in Lean 4 (12/12 levels graduated, 0 sorry), establishing the first machine-checked spectral method for kinetic boundary conditions. The method is demonstrated on the phase-space three-body problem, reducing the boundary error from 41\% (Neumann) to 4.7\% (penalty) at 950\(\times\) speedup over Monte Carlo.