`Compfiles/Usa2021P2.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 3305 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

55 declarations, 0 contain sorry, 0 declared as axioms

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.

Imports (4)

Imported by 1 file

Compfiles.lean

structure Usa2021P2.Park Documented declaration: Park line 53 source
Source documentation
A park: the combinatorial data of the Planar National Park, namely a finite simple graph (the junctions and trails) that is 3-regular (each junction is the endpoint of exactly three trails), together with a rotation system rot giving the cyclic order of the three trails at each junction (as provided by a planar layout; rot v sends each neighbour of v to the next one clockwise).
Turning "left" at a junction v, having arrived from u, means leaving towards rot v u; turning "right" means leaving towards rot v (rot v u).

standard axioms: Classical.choice, Quot.sound, propext what this means
```
structure Park where
…
```
instance Usa2021P2.Park.(instance at line 70) line 70 source
instance Usa2021P2.Park.(instance at line 71) line 71 source
instance Usa2021P2.Park.(instance at line 72) line 72 source
def Usa2021P2.Park.turn Leaving junction v (having arrived from u) by the trail on the left (p = true) or on the right (p = false) line 78 source
Source documentation
Leaving junction v (having arrived from u) by the trail on the left (p = true) or on the right (p = false).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Usa2021P2.Park.V, Bool
Proof uses: cond, Usa2021P2.Park.rot
```
def turn (v u : P.V) (p : Bool) : P.V :=
…
```
lemma Usa2021P2.Park.turn_adj line 81 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Usa2021P2.Park.V, SimpleGraph.Adj, Usa2021P2.Park.G, Bool, Usa2021P2.Park.turn
Proof uses: Eq, Bool.false, Usa2021P2.Park.rot_adj, Usa2021P2.Park.rot, Eq.symm, Bool.true, Eq.refl
2 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2021P2.Park.rot_inv_ne line 87 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Usa2021P2.Park.V, SimpleGraph.Adj, Usa2021P2.Park.G, Ne, Usa2021P2.Park.rot
Proof uses: Eq, Usa2021P2.Park.rot_inv, Usa2021P2.Park.rot_ne, Eq.mp, congrArg

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2021P2.Park.turn_ne The visitor never leaves a junction by the trail she arrived on line 94 source
Source documentation
The visitor never leaves a junction by the trail she arrived on.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Usa2021P2.Park.V, SimpleGraph.Adj, Usa2021P2.Park.G, Bool, Ne, Usa2021P2.Park.turn
Proof uses: Eq, Bool.false, Usa2021P2.Park.rot_inv_ne, Eq.symm, Bool.true, Usa2021P2.Park.rot_ne, Eq.refl
2 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma turn_ne {u v : P.V} (h : P.G.Adj v u) (p : Bool) : P.turn v u p ≠ u := by
…
```
Mentions: h
lemma Usa2021P2.Park.turn_inv_turn Turning one way and then, from the same junction, the other way undoes the turn: rot and rot ∘ rot are inverse 3-cycles on the neighbours line 101 source
Source documentation
Turning one way and then, from the same junction, the other way undoes the turn: rot and rot ∘ rot are inverse 3-cycles on the neighbours.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Usa2021P2.Park.V, SimpleGraph.Adj, Usa2021P2.Park.G, Bool, Eq, Usa2021P2.Park.turn, Bool.not
Proof uses: Bool.false, Usa2021P2.Park.rot_inv, Eq.symm, Bool.true, Eq.refl
2 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma turn_inv_turn {u v : P.V} (h : P.G.Adj v u) (p : Bool) :
    P.turn v (P.turn v u p) (!p) = u := by
…
```
Mentions: h
lemma Usa2021P2.Park.turn_inj line 105 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Usa2021P2.Park.V, SimpleGraph.Adj, Usa2021P2.Park.G, Bool, Eq, Usa2021P2.Park.turn
Proof uses: Bool.not, congrArg, Eq.mp, Usa2021P2.Park.turn_inv_turn

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2021P2.Park.turn_not_two_cycle A turn and its mirror image cannot both be turns in the same direction: the 3-cycle turn v · p has no 2-cycle line 113 source
Source documentation
A turn and its mirror image cannot both be turns in the same direction: the 3-cycle turn v · p has no 2-cycle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Usa2021P2.Park.V, SimpleGraph.Adj, Usa2021P2.Park.G, Bool, Eq, Usa2021P2.Park.turn, False
Proof uses: Bool.false, Usa2021P2.Park.rot, Eq.mpr, id, congrArg, Eq.refl, Usa2021P2.Park.rot_inv, Usa2021P2.Park.rot_ne, Eq.mp, Eq.symm, Bool.true, Usa2021P2.Park.rot_inv_ne
2 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma turn_not_two_cycle {a c v : P.V} (ha : P.G.Adj v a) (p : Bool)
    (hac : P.turn v a p = c) (hca : P.turn v c p = a) : False := by
…
```
def Usa2021P2.Park.Valid The states of the visitor that occur in a walk: the junction she came from and the junction she has just entered are joined by a trail line 136 source
Source documentation
The states of the visitor that occur in a walk: the junction she came from and the junction she has just entered are joined by a trail. The last component is the direction of her next turn (true = left).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool
Proof uses: SimpleGraph.Adj, Usa2021P2.Park.G, Prod.fst, Prod.snd
```
def Valid (σ : P.V × P.V × Bool) : Prop := P.G.Adj σ.2.1 σ.1
```
instance Usa2021P2.Park.(instance at line 138) line 138 source
def Usa2021P2.Park.step One step of the walk: turn at the current junction and traverse the chosen trail; the next turn has the opposite direction line 143 source
Source documentation
One step of the walk: turn at the current junction and traverse the chosen trail; the next turn has the opposite direction.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool
Proof uses: Prod.mk, Prod.fst, Prod.snd, Usa2021P2.Park.turn, Bool.not
```
def step (σ : P.V × P.V × Bool) : P.V × P.V × Bool :=
…
```
def Usa2021P2.Park.stepInv The inverse step: the process is deterministic in both directions line 147 source
Source documentation
The inverse step: the process is deterministic in both directions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool
Proof uses: Prod.mk, Usa2021P2.Park.turn, Prod.fst, Prod.snd, Bool.not
```
def stepInv (σ : P.V × P.V × Bool) : P.V × P.V × Bool :=
…
```
lemma Usa2021P2.Park.valid_step line 150 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool, Usa2021P2.Park.Valid, Usa2021P2.Park.step
Proof uses: SimpleGraph.Adj.symm, Usa2021P2.Park.G, Prod.fst, Prod.snd, Usa2021P2.Park.turn, Usa2021P2.Park.turn_adj
lemma Usa2021P2.Park.valid_stepInv line 153 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool, Usa2021P2.Park.Valid, Usa2021P2.Park.stepInv
Proof uses: Usa2021P2.Park.turn_adj, Prod.fst, Prod.snd, SimpleGraph.Adj.symm, Usa2021P2.Park.G
lemma Usa2021P2.Park.stepInv_step line 156 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool, Usa2021P2.Park.Valid, Eq, Usa2021P2.Park.stepInv, Usa2021P2.Park.step
Proof uses: Prod.mk, Prod.ext, Usa2021P2.Park.turn_inv_turn, Prod.fst, Prod.snd, rfl, Bool.not_not
1 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2021P2.Park.step_stepInv line 161 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool, Usa2021P2.Park.Valid, Eq, Usa2021P2.Park.step, Usa2021P2.Park.stepInv
Proof uses: Prod.mk, Prod.ext, rfl, Prod.fst, Prod.snd, Usa2021P2.Park.turn_inv_turn, SimpleGraph.Adj.symm, Usa2021P2.Park.G, Bool.not_not
1 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2021P2.Park.step_injective line 166 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool, Usa2021P2.Park.Valid, Eq, Usa2021P2.Park.step
Proof uses: Eq.mpr, Usa2021P2.Park.stepInv, id, congrArg, Eq.symm, Usa2021P2.Park.stepInv_step, Eq.refl

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2021P2.Park.valid_walk line 170 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool, Usa2021P2.Park.Valid, Nat, Nat.iterate, Usa2021P2.Park.step
Proof uses: Nat.recAux, Eq.mpr, HAdd.hAdd, OfNat.ofNat, id, Eq, congrArg, Nat.succ, Function.iterate_succ_apply', Usa2021P2.Park.valid_step
3 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2021P2.Park.parity_walk The direction of the turns alternates between left and right line 177 source
Source documentation
The direction of the turns alternates between left and right.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool, Nat, Eq, Prod.snd, Nat.iterate, Usa2021P2.Park.step, ite, Even, Bool.not
Proof uses: Nat.recAux, of_eq_true, OfNat.ofNat, Eq.trans, True, congrArg, ite_eq_left_of_eq_true, eq_self, Eq.mpr, HAdd.hAdd, id, Nat.succ, Function.iterate_succ_apply', dite, ite_eq_left, ite_eq_right, Not, False, eq_true, not_true_eq_false and 4 more
10 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma parity_walk (σ₀ : P.V × P.V × Bool) (k : ℕ) :
    (P.step^[k] σ₀).2.2 = if Even k then σ₀.2.2 else !σ₀.2.2 := by
…
```
lemma Usa2021P2.Park.stepInv_iterate line 189 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool, Usa2021P2.Park.Valid, Nat, LE.le, Eq, Nat.iterate, Usa2021P2.Park.stepInv, Usa2021P2.Park.step, HSub.hSub
Proof uses: Nat.recAux, OfNat.ofNat, Eq.refl, HAdd.hAdd, Eq.mpr, id, Eq.rec, Eq.trans, congrArg, Nat.succ, Function.iterate_succ_apply', Usa2021P2.Park.stepInv_step, Usa2021P2.Park.valid_walk, Function.iterate_succ_apply
12 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Usa2021P2.Park.eq_of_walk_eq If two iterates of the walk agree, the orbit has closed up with period j - i line 206 source
Source documentation
If two iterates of the walk agree, the orbit has closed up with period j - i.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool, Usa2021P2.Park.Valid, Nat, LE.le, Eq, Nat.iterate, Usa2021P2.Park.step, HSub.hSub
Proof uses: Usa2021P2.Park.stepInv, Usa2021P2.Park.stepInv_iterate, le_rfl, Eq.mp, OfNat.ofNat, congrArg, Nat.sub_self
8 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma eq_of_walk_eq {σ₀ : P.V × P.V × Bool} (h₀ : P.Valid σ₀) {i j : ℕ} (hij : i ≤ j)
    (h : P.step^[i] σ₀ = P.step^[j] σ₀) : P.step^[j - i] σ₀ = σ₀ := by
…
```
Mentions: h
lemma Usa2021P2.Park.exists_period The walk is periodic: some positive iterate returns to the initial state line 216 source
Source documentation
The walk is periodic: some positive iterate returns to the initial state.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool, Usa2021P2.Park.Valid, Exists, Nat, And, GT.gt, OfNat.ofNat, Eq, Nat.iterate, Usa2021P2.Park.step
Proof uses: Membership.mem, Finset, Finset.range, HAdd.hAdd, Fintype.card, Subtype, Ne, Subtype.mk, Usa2021P2.Park.valid_walk, Finset.exists_ne_map_eq_of_card_lt_of_maps_to, Finset.univ, Eq.mpr, LT.lt, Finset.card, id, congrArg, Finset.card_range, Set, Finset.mem_univ, LE.le and 7 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma exists_period {σ₀ : P.V × P.V × Bool} (h₀ : P.Valid σ₀) :
    ∃ T > 0, P.step^[T] σ₀ = σ₀ := by
…
```
def Usa2021P2.Park.period The (minimal) period of the walk from σ₀ line 232 source
Source documentation
The (minimal) period of the walk from σ₀.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool, Usa2021P2.Park.Valid, Nat
Proof uses: Nat.find, And, GT.gt, OfNat.ofNat, Eq, Nat.iterate, Usa2021P2.Park.step, Usa2021P2.Park.exists_period
7 instances, coercions and auxiliary constants left out.
```
noncomputable def period {σ₀ : P.V × P.V × Bool} (h₀ : P.Valid σ₀) : ℕ :=
…
```
lemma Usa2021P2.Park.period_pos line 235 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool, Usa2021P2.Park.Valid, LT.lt, Nat, OfNat.ofNat, Usa2021P2.Park.period
Proof uses: And.left, GT.gt, Nat.find, And, Eq, Nat.iterate, Usa2021P2.Park.step, Usa2021P2.Park.exists_period, Nat.find_spec
9 instances, coercions and auxiliary constants left out.
lemma Usa2021P2.Park.period_eq line 238 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool, Usa2021P2.Park.Valid, Eq, Nat.iterate, Usa2021P2.Park.step, Usa2021P2.Park.period
Proof uses: And.right, GT.gt, Nat, Nat.find, And, OfNat.ofNat, Usa2021P2.Park.exists_period, Nat.find_spec
7 instances, coercions and auxiliary constants left out.
lemma Usa2021P2.Park.period_ne_of_lt line 242 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool, Usa2021P2.Park.Valid, Nat, LT.lt, OfNat.ofNat, Usa2021P2.Park.period, Ne, Nat.iterate, Usa2021P2.Park.step
Proof uses: Eq, LE.le, Nat.find_min', And, GT.gt, Usa2021P2.Park.exists_period, And.intro
11 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2021P2.Park.walk_inj_of_lt_period The iterates of the walk within one period are pairwise distinct line 249 source
Source documentation
The iterates of the walk within one period are pairwise distinct.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool, Usa2021P2.Park.Valid, Nat, LT.lt, Usa2021P2.Park.period, Eq, Nat.iterate, Usa2021P2.Park.step
Proof uses: LE.le, Or, le_total, eq_or_lt_of_le, Eq.refl, absurd, HSub.hSub, Usa2021P2.Park.eq_of_walk_eq, Usa2021P2.Park.period_ne_of_lt, Eq.symm
16 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma walk_inj_of_lt_period {σ₀ : P.V × P.V × Bool} (h₀ : P.Valid σ₀) {i j : ℕ}
    (hi : i < P.period h₀) (hj : j < P.period h₀)
    (h : P.step^[i] σ₀ = P.step^[j] σ₀) : i = j := by
…
```
Mentions: h
lemma Usa2021P2.Park.one_lt_period The period is at least two: one step never returns to the initial state line 261 source
Source documentation
The period is at least two: one step never returns to the initial state.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool, Usa2021P2.Park.Valid, LT.lt, Nat, OfNat.ofNat, Usa2021P2.Park.period
Proof uses: Usa2021P2.Park.period_pos, Decidable.byContradiction, Not, Eq, Eq.mp, LE.le, Nat.iterate, Usa2021P2.Park.step, Usa2021P2.Park.period_eq, False, Prod.mk, congrArg, Prod.fst, SimpleGraph.Adj.ne, Usa2021P2.Park.G, Prod.snd
12 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma one_lt_period {σ₀ : P.V × P.V × Bool} (h₀ : P.Valid σ₀) : 1 < P.period h₀ := by
…
```
lemma Usa2021P2.Park.return_at_period_sub_one The walk enters the starting junction again one step before the period line 273 source
Source documentation
The walk enters the starting junction again one step before the period.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool, Usa2021P2.Park.Valid, And, LT.lt, Nat, OfNat.ofNat, HSub.hSub, Usa2021P2.Park.period, Eq, Prod.fst, Prod.snd, Nat.iterate, Usa2021P2.Park.step
Proof uses: Usa2021P2.Park.one_lt_period, And.intro, Usa2021P2.Park.period_eq, Eq.mp, Nat.succ, congrArg, Function.iterate_succ_apply', HAdd.hAdd, Usa2021P2.Park.stepInv, Usa2021P2.Park.step_injective, Usa2021P2.Park.valid_walk, Usa2021P2.Park.valid_stepInv, Eq.trans, Eq.symm, Usa2021P2.Park.step_stepInv, Eq.mpr, id, Eq.refl
12 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma return_at_period_sub_one {σ₀ : P.V × P.V × Bool} (h₀ : P.Valid σ₀) :
    0 < P.period h₀ - 1 ∧ (P.step^[P.period h₀ - 1] σ₀).2.1 = σ₀.1 := by
…
```
lemma Usa2021P2.Park.exists_return The visitor always gets back to the junction where she started line 289 source
Source documentation
The visitor always gets back to the junction where she started.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool, Usa2021P2.Park.Valid, Exists, Nat, And, GT.gt, OfNat.ofNat, Eq, Prod.fst, Prod.snd, Nat.iterate, Usa2021P2.Park.step
Proof uses: Exists.intro, HSub.hSub, Usa2021P2.Park.period, And.intro, And.left, LT.lt, Usa2021P2.Park.return_at_period_sub_one, And.right
6 instances, coercions and auxiliary constants left out.
```
lemma exists_return {σ₀ : P.V × P.V × Bool} (h₀ : P.Valid σ₀) :
    ∃ k > 0, (P.step^[k] σ₀).2.1 = σ₀.1 :=
…
```
def Usa2021P2.Park.retTime The first time (> 0) at which the walk re-enters the starting junction line 294 source
Source documentation
The first time (> 0) at which the walk re-enters the starting junction.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool, Usa2021P2.Park.Valid, Nat
Proof uses: Nat.find, And, GT.gt, OfNat.ofNat, Eq, Prod.fst, Prod.snd, Nat.iterate, Usa2021P2.Park.step, Usa2021P2.Park.exists_return
5 instances, coercions and auxiliary constants left out.
```
noncomputable def retTime {σ₀ : P.V × P.V × Bool} (h₀ : P.Valid σ₀) : ℕ :=
…
```
lemma Usa2021P2.Park.retTime_pos line 297 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool, Usa2021P2.Park.Valid, LT.lt, Nat, OfNat.ofNat, Usa2021P2.Park.retTime
Proof uses: And.left, GT.gt, Nat.find, And, Eq, Prod.fst, Prod.snd, Nat.iterate, Usa2021P2.Park.step, Usa2021P2.Park.exists_return, Nat.find_spec
7 instances, coercions and auxiliary constants left out.
lemma Usa2021P2.Park.retTime_eq line 300 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool, Usa2021P2.Park.Valid, Eq, Prod.fst, Prod.snd, Nat.iterate, Usa2021P2.Park.step, Usa2021P2.Park.retTime
Proof uses: And.right, GT.gt, Nat, Nat.find, And, OfNat.ofNat, Usa2021P2.Park.exists_return, Nat.find_spec
5 instances, coercions and auxiliary constants left out.
lemma Usa2021P2.Park.retTime_min line 304 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool, Usa2021P2.Park.Valid, Nat, LT.lt, OfNat.ofNat, Usa2021P2.Park.retTime, Ne, Prod.fst, Prod.snd, Nat.iterate, Usa2021P2.Park.step
Proof uses: Eq, LE.le, Nat.find_min', And, GT.gt, Usa2021P2.Park.exists_return, And.intro
9 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2021P2.Park.retTime_le_period_sub_one line 310 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool, Usa2021P2.Park.Valid, LE.le, Nat, Usa2021P2.Park.retTime, HSub.hSub, Usa2021P2.Park.period, OfNat.ofNat
Proof uses: Nat.find_min', And, GT.gt, Eq, Prod.fst, Prod.snd, Nat.iterate, Usa2021P2.Park.step, Usa2021P2.Park.exists_return, Usa2021P2.Park.return_at_period_sub_one
11 instances, coercions and auxiliary constants left out.
def Usa2021P2.Park.entries Documented declaration: entries line 317 source
Source documentation
The number of times the visitor enters junction v during her walk, from the initial state σ₀ until she gets back to the starting junction (the final re-entry into the starting junction counts, the departure from it does not).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool, Usa2021P2.Park.Valid, Nat
Proof uses: HAdd.hAdd, Finset.card, Finset.filter, Eq, Prod.fst, Prod.snd, Nat.iterate, Usa2021P2.Park.step, Finset.range, Usa2021P2.Park.retTime, ite, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
```
noncomputable def entries (σ₀ : P.V × P.V × Bool) (h₀ : P.Valid σ₀) (v : P.V) : ℕ :=
…
```
theorem Usa2021P2.Park.no_mirror The key lemma: a trajectory never contains a turn and its mirror image, i.e. turns a → b → c and c → b → a through the same junction line 325 source
Source documentation
The key lemma: a trajectory never contains a turn and its mirror image, i.e. turns a → b → c and c → b → a through the same junction. Otherwise the turns adjacent to them at c would again be mirror images of each other, with a strictly smaller gap — an infinite descent.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool, Usa2021P2.Park.Valid, Nat, LE.le, OfNat.ofNat, Eq, Nat.iterate, Usa2021P2.Park.step, Prod.mk, HAdd.hAdd, Usa2021P2.Park.turn, False
Proof uses: Nat.strongRecOn, LT.lt, SimpleGraph.Adj, Usa2021P2.Park.G, Usa2021P2.Park.valid_walk, Eq.mp, congrArg, Eq.rec, Usa2021P2.Park.turn_adj, GE.ge, Or, Nat.lt_or_ge, Prod.fst, Nat.succ, Function.iterate_succ_apply', SimpleGraph.Adj.ne, Bool.not, dite, False.elim, Usa2021P2.Park.turn_not_two_cycle and 32 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 68 steps
Open to load the checked before-and-after goal states.
```
theorem no_mirror {σ₀ : P.V × P.V × Bool} (h₀ : P.Valid σ₀) :
    ∀ n : ℕ, ∀ (i : ℕ) (a b c : P.V) (p q : Bool),
      1 ≤ n → P.step^[i] σ₀ = (a, (b, p)) → P.step^[i + n] σ₀ = (c, (b, q)) →
      P.turn b a p = c → P.turn b c q = a → False := by
…
```
theorem Usa2021P2.Park.arrivals_le_three Documented declaration: arrivals_le_three line 390 source
Source documentation
In one period of the walk, any junction is entered at most three times: the (at most six) turns at v pair up into three mirror pairs, of which at most one turn each can occur by no_mirror.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool, Usa2021P2.Park.Valid, LE.le, Nat, Finset.card, Finset.filter, Eq, Prod.fst, Prod.snd, Nat.iterate, Usa2021P2.Park.step, Finset.range, Usa2021P2.Park.period, OfNat.ofNat
Proof uses: Finset, Eq.mpr, id, congrArg, rfl, Prod.mk, SProd.sprod, SimpleGraph.Adj, Usa2021P2.Park.G, Finset.univ, HMul.hMul, Finset.card_product, Usa2021P2.Park.decidableAdj, Usa2021P2.Park.fintypeV, Usa2021P2.Park.cubic, Fintype.card, Finset.card_univ, Fintype.card_bool, Eq.refl, Set.MapsTo and 54 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 119 steps
Open to load the checked before-and-after goal states.
```
theorem arrivals_le_three {σ₀ : P.V × P.V × Bool} (h₀ : P.Valid σ₀) (v : P.V) :
    ((Finset.range (P.period h₀)).filter
      fun k ↦ (P.step^[k] σ₀).2.1 = v).card ≤ 3 := by
…
```
theorem Usa2021P2.Park.entries_le_three The visitor enters any junction at most three times during her walk line 517 source
Source documentation
The visitor enters any junction at most three times during her walk.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool, Usa2021P2.Park.Valid, LE.le, Nat, Usa2021P2.Park.entries, OfNat.ofNat
Proof uses: id, dite, HAdd.hAdd, Finset.card, Finset.filter, Eq, Prod.fst, Prod.snd, Nat.iterate, Usa2021P2.Park.step, Finset.range, Usa2021P2.Park.retTime, ite, Eq.mpr, congrArg, ite_eq_left, Finset, EmptyCollection.emptyCollection, Not, Membership.mem and 31 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
theorem entries_le_three {σ₀ : P.V × P.V × Bool} (h₀ : P.Valid σ₀) (v : P.V) :
    P.entries σ₀ h₀ v ≤ 3 := by
…
```
def Usa2021P2.Park.wangEdges Documented declaration: wangEdges line 546 source
Source documentation
The example of Danielle Wang from the official solution: a park with ten junctions A, B, ..., J (numbered 0 through 9) in which the visitor enters junction A = 0 three times. (This rotation system is planar — it has seven faces, so 10 - 15 + 7 = 2 — hence it really comes from a planar layout, though the formal statement does not require this.)

standard axioms: propext what this means
Statement uses: List, Prod, Fin, OfNat.ofNat, Nat
Proof uses: List.cons, Prod.mk, List.nil
4 instances, coercions and auxiliary constants left out.
```
def wangEdges : List (Fin 10 × Fin 10) :=
…
```
def Usa2021P2.Park.wangAdj line 550 source
standard axioms: propext what this means
Statement uses: Fin, OfNat.ofNat, Nat
Proof uses: Or, Membership.mem, Prod, List, Usa2021P2.Park.wangEdges, Prod.mk
3 instances, coercions and auxiliary constants left out.
instance Usa2021P2.Park.(instance at line 552) line 552 source
def Usa2021P2.Park.wangG line 555 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Fin, OfNat.ofNat, Nat
Proof uses: SimpleGraph.mk, Usa2021P2.Park.wangAdj
4 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
instance Usa2021P2.Park.(instance at line 562) line 562 source

def Usa2021P2.Park.wangRotN The cyclic order of the trails at each junction of wangPark line 566 source

Source documentation

The cyclic order of the trails at each junction of wangPark.

no axioms what this means

Statement uses: Nat

Proof uses: Usa2021P2.Park.wangRotN.match_1, Unit, OfNat.ofNat

1 instances, coercions and auxiliary constants left out.

def wangRotN : ℕ → ℕ → ℕ
  | 0, 1 => 2 | 0, 2 => 7 | 0, 7 => 1
  | 1, 0 => 9 | 1, 3 => 0 | 1, 9 => 3
  | 2, 0 => 3 | 2, 3 => 4 | 2, 4 => 0
  | 3, 1 => 6 | 3, 2 => 1 | 3, 6 => 2
  | 4, 2 => 5 | 4, 5 => 7 | 4, 7 => 2
  | 5, 4 => 6 | 5, 6 => 8 | 5, 8 => 4
  | 6, 3 => 9 | 6, 5 => 3 | 6, 9 => 5
  | 7, 0 => 4 | 7, 4 => 8 | 7, 8 => 0
  | 8, 5 => 9 | 8, 7 => 5 | 8, 9 => 7
  | 9, 1 => 8 | 9, 6 => 1 | 9, 8 => 6
  | _, _ => 0

def Usa2021P2.Park.wangRot line 579 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat
Proof uses: Fin.mk, HMod.hMod, Usa2021P2.Park.wangRotN
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Usa2021P2.Park.wangPark line 582 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park
Proof uses: Usa2021P2.Park.mk, Fin, OfNat.ofNat, Nat, inferInstance, Fintype, DecidableEq, Usa2021P2.Park.wangG, DecidableRel, SimpleGraph.Adj, Usa2021P2.Park.wangRot
8 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2021P2.Park.wang_valid line 594 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2021P2.Park.Valid, Usa2021P2.Park.wangPark, Prod.mk, Fin, OfNat.ofNat, Nat, Prod, Bool, Bool.true
Proof uses: id, of_decide_eq_true, Usa2021P2.Park.wangAdj, Eq, Decidable.decide, Eq.refl
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Usa2021P2.Park.wang_entries Documented declaration: wang_entries line 601 source
Source documentation
Starting from junction C = 2 along the trail to A = 0, the visitor's walk is C A H I F G D B A H E F G J B A C: she gets back to C after 16 trails, having entered junction A three times.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Usa2021P2.Park.entries, Usa2021P2.Park.wangPark, Prod.mk, Fin, OfNat.ofNat, Prod, Bool, Bool.true, Usa2021P2.Park.wang_valid
Proof uses: Usa2021P2.Park.retTime, Iff.mpr, Nat.find, And, GT.gt, Usa2021P2.Park.V, Prod.fst, Prod.snd, Nat.iterate, Usa2021P2.Park.step, Usa2021P2.Park.exists_return, LT.lt, Not, Nat.find_eq_iff, And.intro, of_decide_eq_true, id, Decidable.decide, Eq.refl, Eq.mpr and 9 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem wang_entries :
    wangPark.entries ((2, 0, true) : Fin 10 × Fin 10 × Bool) wang_valid (0 : Fin 10) = 3 := by
…
```
Mentions: Usa2021P2.Park.wang_valid
def Usa2021P2.numberOfEntries 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 line 615 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat
Proof uses: Set.ofPred, Exists, Usa2021P2.Park, Prod, Usa2021P2.Park.V, Bool, Usa2021P2.Park.Valid, Eq, Usa2021P2.Park.entries
```
def numberOfEntries : Set ℕ :=
…
```
determine Usa2021P2.solution line 619 source
no axioms what this means
Statement uses: Nat
Proof uses: OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
problem Usa2021P2.usa2021_p2 line 621 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsGreatest, Nat, Usa2021P2.numberOfEntries, Usa2021P2.solution
Proof uses: And.intro, Membership.mem, Set, upperBounds, Exists.intro, Usa2021P2.Park, Exists, Prod, Usa2021P2.Park.V, Bool, Usa2021P2.Park.Valid, Eq, Usa2021P2.Park.entries, Usa2021P2.Park.wangPark, Prod.mk, Fin, OfNat.ofNat, Bool.true, Usa2021P2.Park.wang_valid, Usa2021P2.Park.wang_entries and 2 more
8 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.