module
public import Mathlib.Tactic
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Combinatorics.SimpleGraph.Basic
public section
/-!
# USA Mathematical Olympiad 2021, Problem 2
The Planar National Park is a subset of the Euclidean plane consisting of several
trails which meet at junctions. Every trail has its two endpoints at two different
junctions, whereas each junction is the endpoint of exactly three trails. Trails
only intersect at junctions (in particular, trails only meet at endpoints).
Finally, no trails begin and end at the same two junctions.
A visitor walks through the park as follows: she begins at a junction and starts
walking along a trail. At the end of that first trail, she enters a junction and
turns left. On the next junction she turns right, and so on, alternating left and
right turns at each junction. She does this until she gets back to the junction
where she started. What is the largest possible number of times she could have
entered any junction during her walk, over all possible layouts of the park?
# Formalization notes
A park is axiomatized below as a finite simple 3-regular graph equipped with a
rotation system (`Park`). The example park `Park.wangPark` is the example of
Danielle Wang from the official solution.
-/
namespace Usa2021P2
/-- The set of all possible numbers of times the visitor could have entered a
junction during her walk, over all parks and all choices of starting junction
and first trail. -/
def numberOfEntries : Set ℕ :=
{ n | ∃ (P : Park) (σ₀ : P.V × P.V × Bool) (h₀ : P.Valid σ₀) (v : P.V),
P.entries σ₀ h₀ v = n }
/- determine -/ abbrev solution : ℕ := sorry
theorem usa2021_p2 : IsGreatest numberOfEntries solution := sorry
end Usa2021P2
This problem has a complete formalized solution.