`Compfiles/Usa2017P4.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

24 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2017, Problem 4

Let P₁, P₂, ..., P_{2n} be 2n distinct points on the unit circle x² + y² = 1, other than (1, 0). Each point is colored either red or blue, with exactly n red points and n blue points. Let R₁, R₂, ..., Rₙ be any ordering of the red points. Let B₁ be the nearest blue point to R₁ traveling counterclockwise around the circle starting from R₁. Then let B₂ be the nearest of the remaining blue points to R₂ traveling counterclockwise around the circle from R₂, and so on, until we have labeled all of the blue points B₁, ..., Bₙ. Show that the number of counterclockwise arcs of the form Rᵢ → Bᵢ that contain the point (1, 0) is independent of the way we chose the ordering R₁, ..., Rₙ of the red points.

Imports (3)

Imported by 1 file

Compfiles.lean

def Usa2017P4.shift Shift p forward (counterclockwise) by d positions, cyclically line 49 source
Source documentation
Shift p forward (counterclockwise) by d positions, cyclically.

no axioms what this means
Statement uses: Nat, Fin
Proof uses: Fin.mk, HMod.hMod, HAdd.hAdd
6 instances, coercions and auxiliary constants left out.
```
def shift (p : Fin m) (d : ℕ) : Fin m :=
…
```
def Usa2017P4.cdist The cyclic (counterclockwise) distance from a to b; it is 0 iff a = b line 53 source
Source documentation
The cyclic (counterclockwise) distance from a to b; it is 0 iff a = b.

no axioms what this means
Statement uses: Nat, Fin
Proof uses: HMod.hMod, HSub.hSub, HAdd.hAdd
7 instances, coercions and auxiliary constants left out.
```
def cdist (a b : Fin m) : ℕ := (b.val + m - a.val) % m
```
def Usa2017P4.wrap wrap r b is 1 when the counterclockwise arc from r to b passes through the cut point (1, 0), and 0 otherwise line 57 source
Source documentation
wrap r b is 1 when the counterclockwise arc from r to b passes through the cut point (1, 0), and 0 otherwise.

no axioms what this means
Statement uses: Nat, Fin
Proof uses: ite, LT.lt, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
```
def wrap (r b : Fin m) : ℕ := if b.val < r.val then 1 else 0
…
```
def Usa2017P4.avail The set of blue points that have not been used yet line 66 source
Source documentation
The set of blue points that have not been used yet.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Finset
Proof uses: Finset.filter, And, Eq, Bool.false, Not, Membership.mem, Finset.univ
8 instances, coercions and auxiliary constants left out.
```
def avail (used : Finset (Fin m)) : Finset (Fin m) :=
…
```
def Usa2017P4.nb The nearest available blue point to r, going counterclockwise from r (if one exists; otherwise, arbitrarily, r itself) line 71 source
Source documentation
The nearest available blue point to r, going counterclockwise from r (if one exists; otherwise, arbitrarily, r itself).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Finset
Proof uses: dite, Finset.Nonempty, Usa2017P4.avail, Classical.choose, And, Membership.mem, LE.le, Usa2017P4.cdist, Not
11 instances, coercions and auxiliary constants left out.
```
noncomputable def nb (used : Finset (Fin m)) (r : Fin m) : Fin m :=
…
```
def Usa2017P4.wraps The total number of arcs through (1, 0) produced when the red points listed in l are processed in order, starting from the set used of already-taken blue points line 79 source
Source documentation
The total number of arcs through (1, 0) produced when the red points listed in l are processed in order, starting from the set used of already-taken blue points.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, List, Finset
2 instances, coercions and auxiliary constants left out.
```
noncomputable def wraps : List (Fin m) → Finset (Fin m) → ℕ
  | [], _ => 0
  | (r :: rs), used => wrap r (nb c used r) + wraps rs (insert (nb c used r) used)

end Process

snip begin

section GeometryLemmas

variable {m : ℕ}
```
Mentions: Usa2017P4.wrap, Usa2017P4.nb
lemma Usa2017P4.cdist_if line 91 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Eq, Usa2017P4.cdist, ite, LE.le, HSub.hSub, HAdd.hAdd
Proof uses: id, dite, HMod.hMod, Eq.mpr, congrArg, ite_eq_left, Nat.add_mod_right, Nat.mod_eq_of_lt, Eq.refl, Not, ite_eq_right
19 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P4.shift_cdist line 99 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Eq, Usa2017P4.shift, Usa2017P4.cdist
Proof uses: Fin.ext, id, LE.le, Or, HMod.hMod, HAdd.hAdd, HSub.hSub, le_total, Eq.mpr, congrArg, Nat.add_mod_right, Nat.mod_eq_of_lt, Fin.isLt, Eq.refl, LT.lt, eq_or_lt_of_le, OfNat.ofNat, Nat.mod_self, Nat.add_zero
21 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P4.cdist_left_inj line 116 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Eq, Usa2017P4.cdist
Proof uses: Eq.mpr, Usa2017P4.shift, id, congrArg, Eq.symm, Usa2017P4.shift_cdist, Eq.refl

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P4.cdist_pos line 119 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Ne, LT.lt, OfNat.ofNat, Usa2017P4.cdist
Proof uses: Eq.mpr, ite, LE.le, HSub.hSub, HAdd.hAdd, id, Eq, congrArg, Usa2017P4.cdist_if, Fin.ext, dite, ite_eq_left, Not, ite_eq_right
13 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P4.cdist_add_of_lt line 124 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, LT.lt, Usa2017P4.cdist, Eq, HAdd.hAdd
Proof uses: Eq.mpr, ite, LE.le, HSub.hSub, id, congr, congrArg, Usa2017P4.cdist_if, Fin.isLt, dite, congrFun', ite_eq_left, Eq.mp, Not, ite_eq_right
19 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P4.arc_rotate line 130 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Ne, LT.lt, Usa2017P4.cdist
Proof uses: Eq.mpr, ite, LE.le, HSub.hSub, HAdd.hAdd, id, Eq, congr, congrArg, Usa2017P4.cdist_if, Fin.isLt, Fin.ext, dite, congrFun', ite_eq_left, Not, Eq.mp, ite_eq_right
21 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P4.wrap_eq_of_mem_arc Key fact for the swapping argument: if p lies on the open counterclockwise arc from y to x, then wrap p y and wrap p x differ by an amount that does not depend on p line 140 source
Source documentation
Key fact for the swapping argument: if p lies on the open counterclockwise arc from y to x, then wrap p y and wrap p x differ by an amount that does not depend on p.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Ne, LT.lt, Usa2017P4.cdist, Eq, Usa2017P4.wrap, HAdd.hAdd, ite, OfNat.ofNat
Proof uses: Usa2017P4.cdist_pos, Ne.symm, Fin.isLt, rfl, Eq.mpr, id, congrArg, dite, congrFun', ite_eq_left, LE.le, Eq.mp, HSub.hSub, Usa2017P4.cdist_if, congr, Not, ite_eq_right, False, Eq.trans, eq_false' and 3 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma wrap_eq_of_mem_arc {y x p : Fin m} (hpy : p ≠ y) (h : cdist y p < cdist y x) :
    wrap p y = wrap p x + (if y.val < x.val then 1 else 0) := by
…
```
Mentions: h, Usa2017P4.cdist, Usa2017P4.wrap
lemma Usa2017P4.mem_avail line 156 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Finset, Iff, Membership.mem, Usa2017P4.avail, And, Eq, Bool.false, Not
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.filter, Finset.univ, true_and, iff_self
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P4.nb_eq_choose line 160 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Finset, Finset.Nonempty, Usa2017P4.avail, Eq, Usa2017P4.nb, Classical.choose, And, Membership.mem, LE.le, Usa2017P4.cdist, Finset.exists_min_image
Proof uses: dite_eq_left, Not
20 instances, coercions and auxiliary constants left out.
lemma Usa2017P4.nb_mem line 164 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Finset, Finset.Nonempty, Usa2017P4.avail, Membership.mem, Usa2017P4.nb
Proof uses: Eq.mpr, Classical.choose, And, LE.le, Usa2017P4.cdist, Finset.exists_min_image, id, Eq, congrArg, Usa2017P4.nb_eq_choose, And.left, Classical.choose_spec
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P4.nb_min line 169 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Finset, Finset.Nonempty, Usa2017P4.avail, Membership.mem, LE.le, Usa2017P4.cdist, Usa2017P4.nb
Proof uses: Eq.mpr, Classical.choose, And, Finset.exists_min_image, id, Eq, congrArg, Usa2017P4.nb_eq_choose, And.right, Classical.choose_spec
13 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P4.nb_eq_of Uniqueness of the nearest available blue point line 176 source
Source documentation
Uniqueness of the nearest available blue point.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Finset, Finset.Nonempty, Usa2017P4.avail, Membership.mem, LE.le, Usa2017P4.cdist, Eq, Usa2017P4.nb
Proof uses: Usa2017P4.cdist_left_inj, le_antisymm, Usa2017P4.nb_min, Usa2017P4.nb_mem
7 instances, coercions and auxiliary constants left out.
```
lemma nb_eq_of {used : Finset (Fin m)} {r b : Fin m} (h : (avail c used).Nonempty)
    (hb : b ∈ avail c used) (hmin : ∀ q ∈ avail c used, cdist r b ≤ cdist r q) :
    nb c used r = b :=
…
```
Mentions: h, Usa2017P4.avail, Usa2017P4.cdist, Usa2017P4.nb
lemma Usa2017P4.avail_insert line 181 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Finset, Eq, Usa2017P4.avail, Insert.insert, Finset.erase
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, And, Bool.false, Not, Ne, id, congr, congrArg, Eq.trans, Or, Iff.intro, 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 Usa2017P4.card_avail_insert line 187 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Finset, Membership.mem, Usa2017P4.avail, Eq, Finset.card, Insert.insert, HSub.hSub, OfNat.ofNat
Proof uses: Eq.mpr, Finset.erase, id, congrArg, Usa2017P4.avail_insert, Finset.card_erase_of_mem, Eq.refl
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P4.wraps_cons line 191 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, List, Finset, Eq, Usa2017P4.wraps, List.cons, HAdd.hAdd, Usa2017P4.wrap, Usa2017P4.nb, Insert.insert
Proof uses: rfl
4 instances, coercions and auxiliary constants left out.
lemma Usa2017P4.wraps_swap_pair The heart of the proof: processing two consecutive red points in either order produces the same number of arcs through (1, 0) and the same set of used blue points line 197 source
Source documentation
The heart of the proof: processing two consecutive red points in either order produces the same number of arcs through (1, 0) and the same set of used blue points.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Bool.true, Finset, LE.le, OfNat.ofNat, Finset.card, Usa2017P4.avail, And, HAdd.hAdd, Usa2017P4.wrap, Usa2017P4.nb, Insert.insert
Proof uses: Finset.Nonempty, Iff.mp, LT.lt, Finset.card_pos, Membership.mem, Usa2017P4.nb_mem, Eq.mpr, id, congrArg, Eq.symm, propext, HSub.hSub, Usa2017P4.card_avail_insert, Ne, Usa2017P4.cdist, lt_of_le_of_ne, Usa2017P4.nb_min, Usa2017P4.cdist_left_inj, dite, Finset.erase and 23 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 96 steps
Open to load the checked before-and-after goal states.
```
lemma wraps_swap_pair {r r' : Fin m} (hr : c r = true) (hr' : c r' = true)
    {used : Finset (Fin m)} (hcard : 2 ≤ (avail c used).card) :
    wrap r (nb c used r) + wrap r' (nb c (insert (nb c used r) used) r') =
      wrap r' (nb c used r') + wrap r (nb c (insert (nb c used r') used) r) ∧
    insert (nb c (insert (nb c used r) used) r') (insert (nb c used r) used) =
      insert (nb c (insert (nb c used r') used) r) (insert (nb c used r') used) := by
…
```
Mentions: Usa2017P4.avail, Usa2017P4.wrap, Usa2017P4.nb
lemma Usa2017P4.wraps_perm The wrap count is invariant under permuting the processing order of the red points (given that enough blue points remain available at every step) line 329 source
Source documentation
The wrap count is invariant under permuting the processing order of the red points (given that enough blue points remain available at every step).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, List, List.Perm, Membership.mem, Eq, Bool.true, Finset, LE.le, List.length, Finset.card, Usa2017P4.avail, Usa2017P4.wraps
Proof uses: List.Perm.rec, List.nil, Eq.refl, List.cons, LT.lt, OfNat.ofNat, HAdd.hAdd, rfl, Usa2017P4.nb, Usa2017P4.nb_mem, Iff.mp, Finset.Nonempty, Finset.card_pos, Eq.mpr, Usa2017P4.wrap, Insert.insert, id, congrArg, Usa2017P4.wraps_cons, HSub.hSub and 17 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
```
lemma wraps_perm {l₁ l₂ : List (Fin m)} (h : List.Perm l₁ l₂) :
    (∀ r ∈ l₁, c r = true) → ∀ used : Finset (Fin m),
      l₁.length ≤ (avail c used).card → wraps c l₁ used = wraps c l₂ used := by
…
```
Mentions: h, Usa2017P4.avail, Usa2017P4.wraps
problem Usa2017P4.usa2017_p4 USAMO 2017 Problem 4 line 370 source
Source documentation
USAMO 2017 Problem 4. With the notation introduced above (points recorded in counterclockwise order starting from (1, 0), true = red), the number of counterclockwise arcs Rᵢ → Bᵢ containing (1, 0) does not depend on the ordering R₁, ..., Rₙ of the red points.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Fin, HMul.hMul, Bool, Eq, Finset.card, Finset.filter, Bool.true, Finset.univ, List, List.Nodup, List.length, Membership.mem, Usa2017P4.wraps, EmptyCollection.emptyCollection, Finset
Proof uses: List.toFinset, Finset.eq_of_subset_of_card_le, Iff.mpr, And, Finset.mem_filter, And.intro, Finset.mem_univ, Eq.mp, congrArg, propext, List.mem_toFinset, Eq.mpr, LE.le, id, List.toFinset_card_of_nodup, le_refl, Iff, Eq.symm, Iff.rfl, List.Perm and 24 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
```
problem usa2017_p4 (n : ℕ) (_hn : 0 < n) (c : Fin (2 * n) → Bool)
    (hred : (Finset.univ.filter (fun i => c i = true)).card = n)
    (l₁ l₂ : List (Fin (2 * n)))
    (hnod₁ : l₁.Nodup) (hlen₁ : l₁.length = n) (hred₁ : ∀ r ∈ l₁, c r = true)
    (hnod₂ : l₂.Nodup) (hlen₂ : l₂.length = n) (hred₂ : ∀ r ∈ l₂, c r = true) :
    wraps c l₁ ∅ = wraps c l₂ ∅ := by
…
```
Mentions: Usa2017P4.wraps