Braid Realization at Zero Angular Momentum for the Planar N-Body Problem

We prove that for the planar Newtonian \(N\)-body problem with arbitrary positive masses and zero angular momentum (\(J = 0\)), every reduced free homotopy class of periodic orbits with all pairwise winding numbers nonzero is realized by a collision-free periodic orbit. The case \(N = 3\) is proved by Levi-Civita regularization and a topological action premium: the winding number constraint forces the action minimizer to avoid each binary collision, at an exact energy cost of factor 2 (the "topological premium"). The extension to \(N \geq 4\) combines two independent collision avoidance mechanisms — winding number obstruction for binary collisions and Marchal's averaging lemma for triple and higher collisions — yielding collision-free minimizers by a two-layer argument. For the spatial (\(\mathbb{R}^3\)) problem, the question is vacuously resolved: the ordered configuration space is simply connected (the binary collision set has codimension 3), so there is only the trivial homotopy class.

All logical compositions are formalized in a kernel-verified proof system (Lean 4) with 49 declarations, 39 kernel-verified, and zero sorry. The external mathematical facts (regularization theorems, Marchal's lemma) are declared honestly as cited references, not as kernel-verified proofs.

Keywords: \(N\)-body problem, braid realization, zero angular momentum, collision avoidance, winding numbers, Marchal averaging, Levi-Civita regularization, Lean 4 formalization