Self-Contained Lean 4 Challenges for Geometers & Topologists

Want to contribute to PlasmaLean without learning plasma physics jargon or cloning a giant physics solver? Each of the 6 micro-bounties below is a self-contained, 35-line Lean 4 stub file using only standard Mathlib imports. Replacing sorry with a proof in any of these files directly unlocks a formal theorem in the PlasmaLean stellarator verification pipeline.