Papers With

← All papers
First page of A Winner Classification for Rooted Partizan Edge Geography on Heterogeneous Bouquets of Cycles

A Winner Classification for Rooted Partizan Edge Geography on Heterogeneous Bouquets of Cycles

Adam Tilèpe

math.CO Oct 26, 2026 · v1
formalization combinatorics mathlib
Read PDF arXiv abstract Code
TL;DR
The winner classification for rooted partizan edge geography on bouquets of cycles is fully formalized and machine-checked in Lean 4 with Mathlib, using an accompanying source file.
Abstract
We consider an undirected edge-traversal game on a finite bouquet of simple cycles. Each of two players controls a token, both tokens begin at the common root, and the players alternate traversing edges that have not been used by either token. A player with no legal move loses. We prove that the first player wins precisely when the number of cycles of odd edge-length is odd, without assuming equal cycle lengths. The proof uses a simultaneous induction on root and defense configurations, with an exact analysis of the forced race between two opened cycles. We also explain how the classification corresponds to a completed Lean 4 formalization of the underlying game on finite edge sets.
Problem

In rooted partizan edge geography on a finite bouquet of simple cycles, two players each move their own token from a common root along edges not yet used by either token, and a player with no legal move loses. The question is which player wins, with no assumption that the cycle lengths are equal.

Approach

The proof uses simultaneous strong induction on root positions and defense positions. It includes an exact four-case analysis of the forced race between two opened cycles, and the defense coordinates are measured from the consumed entrance. The Lean 4 development defines the game on an actual undirected simple graph, built from State, Legal, advance and the inductive predicate edgeGameForceWin. It then proves the classification through a canonical corridor-and-petal model and reduces the real double-root game to that model.

Results

The first player wins exactly when the number of odd-length cycles is odd. Explicit formulas for defense positions are also given. The Lean source, pinned to a fixed toolchain and Mathlib revision, gives a mechanically checked proof of the main classification.