Independent-Set Threshold Games and Geodetic Removal on Odd Cycles

In the geodetic removal game, players select vertices until the convex hull of the unselected vertices, taken along shortest paths in the original graph, ceases to be the whole graph. We prove that the second player wins on every odd cycle of order at least five, resolving a conjecture of Benesh, Ernst, Meyer, Salmon and Sieben. The proof characterizes terminal selected sets as those containing a maximum independent set of an auxiliary cycle, then uses a dynamic pairing strategy. More generally, consider the impartial game in which vertices are selected until their union contains an independent set of a prescribed size r ≥ 2. On every path or cycle of order at least 2r, the second player can force termination on exactly move 2r − 2. We classify the remaining feasible path thresholds and prove the same exact-turn result for bipartite graphs with a given perfect matching. The strategies maintain paired selected vertices until a final move deliberately breaks the pairing. They admit constant-time responses after linear initialization. Version 2.1 clarifies the terminal-set characterization and improves the exposition; the mathematical results are unchanged. The Lean 4 companion covers the strategies, geodetic correspondence, boundary cases, bipartite extension and implementation bounds. It is available at GitHub release v1.0.1 and the MIT-licensed software archive. The formalization and manuscript have not undergone independent peer review.