Independent-Set Threshold Games and Geodetic Removal on Odd Cycles

This paper gives complete mathematical proofs for independent-set threshold games on paths, cycles and matched bipartite graphs, and resolves the odd-cycle geodetic removal conjecture of Benesh, Ernst, Meyer, Salmon and Sieben. Version 2.0 adds the public whole-paper Kernel-Only Lean 4 companion. The companion is available in GitHub release v1.0.1 at https://github.com/crabsatellite/odd-cycle-geodetic-removal/releases/tag/v1.0.1 and in the stable software archive at https://doi.org/10.5281/zenodo.22747324. Its signed verification receipt binds 26 paper-facing endpoints and reports only propext, Classical.choice and Quot.sound. The formalization and manuscript have not undergone independent peer review.