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

35 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2008, Problem 3

Let n be a positive integer. Denote by Sₙ the set of points (x, y) with integer coordinates such that

|x| + |y + 1/2| < n.

A path is a sequence of distinct points (x₁, y₁), (x₂, y₂), ..., (x_ℓ, y_ℓ) in Sₙ such that, for i = 2, ..., ℓ, the distance between (xᵢ, yᵢ) and (xᵢ₋₁, yᵢ₋₁) is 1. Prove that the points in Sₙ cannot be partitioned into fewer than n paths.

Imports (16)

Imported by 1 file

Compfiles.lean

def Usa2008P3.rowK The half-width of the row of S n at height y: the row consists of the points (x, y) with |x| ≤ rowK n y line 48 source
Source documentation
The half-width of the row of S n at height y: the row consists of the points (x, y) with |x| ≤ rowK n y.

no axioms what this means
Statement uses: Nat, Int
Proof uses: ite, LE.le, OfNat.ofNat, HSub.hSub, HAdd.hAdd
9 instances, coercions and auxiliary constants left out.
```
def rowK (n : ℕ) (y : ℤ) : ℤ := if 0 ≤ y then (n : ℤ) - 1 - y else (n : ℤ) + y
```
def Usa2008P3.S The set Sₙ of the problem, namely the integer points (x, y) with |x| + |y + 1/2| < n line 53 source
Source documentation
The set Sₙ of the problem, namely the integer points (x, y) with |x| + |y + 1/2| < n. Multiplying by two, this is 2|x| + |2y + 1| < 2n, and we build the set row by row.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Prod, Int
Proof uses: Finset.biUnion, Finset.Icc, Neg.neg, HSub.hSub, OfNat.ofNat, SProd.sprod, Usa2008P3.rowK, Singleton.singleton
12 instances, coercions and auxiliary constants left out.
```
noncomputable def S (n : ℕ) : Finset (ℤ × ℤ) :=
…
```
def Usa2008P3.Adj Two lattice points are adjacent when their (Manhattan) distance is 1 line 58 source
Source documentation
Two lattice points are adjacent when their (Manhattan) distance is 1.

standard axioms: propext what this means
Statement uses: Prod, Int
Proof uses: Eq, HAdd.hAdd, abs, HSub.hSub, Prod.fst, Prod.snd, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
```
def Adj (p q : ℤ × ℤ) : Prop := |p.1 - q.1| + |p.2 - q.2| = 1
…
```
def Usa2008P3.f The auxiliary potential: blue points are those with f p ≡ 2n - 1 (mod 4) line 86 source
Source documentation
The auxiliary potential: blue points are those with f p ≡ 2n - 1 (mod 4).

standard axioms: propext what this means
Statement uses: Prod, Int
Proof uses: HAdd.hAdd, HMul.hMul, OfNat.ofNat, Prod.fst, abs, Prod.snd
7 instances, coercions and auxiliary constants left out.
```
def f (p : ℤ × ℤ) : ℤ := 2 * p.1 + |2 * p.2 + 1|
```
def Usa2008P3.blue The blue predicate line 89 source
Source documentation
The blue predicate.

standard axioms: propext what this means
Statement uses: Nat, Prod, Int
Proof uses: Int.ModEq, OfNat.ofNat, Usa2008P3.f, HSub.hSub, HMul.hMul
7 instances, coercions and auxiliary constants left out.
```
def blue (n : ℕ) (p : ℤ × ℤ) : Prop := f p ≡ 2 * (n : ℤ) - 1 [ZMOD 4]
```
Mentions: Usa2008P3.f
instance Usa2008P3.(instance at line 91) line 91 source
def Usa2008P3.chi The colour of a point as ±1 (+1 for blue, -1 for red) line 95 source
Source documentation
The colour of a point as ±1 (+1 for blue, -1 for red).

standard axioms: propext what this means
Statement uses: Nat, Prod, Int
Proof uses: ite, Usa2008P3.blue, OfNat.ofNat, Neg.neg
3 instances, coercions and auxiliary constants left out.
```
def chi (n : ℕ) (p : ℤ × ℤ) : ℤ := if blue n p then 1 else -1
```
Mentions: Usa2008P3.blue
def Usa2008P3.sig The sum of colours along a list of points line 98 source
Source documentation
The sum of colours along a list of points.

standard axioms: propext what this means
Statement uses: Nat, List, Prod, Int
Proof uses: List.sum, List.map, Usa2008P3.chi
4 instances, coercions and auxiliary constants left out.
```
def sig (n : ℕ) (P : List (ℤ × ℤ)) : ℤ := (P.map (chi n)).sum
```
Mentions: P, Usa2008P3.chi
def Usa2008P3.b0 The number of blue points on the axis y = 0 in a list line 101 source
Source documentation
The number of blue points on the axis y = 0 in a list.

standard axioms: propext what this means
Statement uses: Nat, List, Prod, Int
Proof uses: List.length, List.filter, Decidable.decide, And, Usa2008P3.blue, Eq, Prod.snd, OfNat.ofNat
6 instances, coercions and auxiliary constants left out.
```
def b0 (n : ℕ) (P : List (ℤ × ℤ)) : ℤ :=
…
```
Mentions: P
def Usa2008P3.GH The "good head" condition on a list: either the head is red, or it lies in B₀ (blue, y = 0) and the second point (if any) is red line 107 source
Source documentation
The "good head" condition on a list: either the head is red, or it lies in B₀ (blue, y = 0) and the second point (if any) is red. For such lists the colour sum is at most the number of B₀-points.

standard axioms: propext what this means
Statement uses: Nat, List, Prod, Int
Proof uses: Usa2008P3.GH.match_1, Unit, True, Or, Not, Usa2008P3.blue, Eq, Prod.snd, OfNat.ofNat, And
1 instances, coercions and auxiliary constants left out.
```
def GH (n : ℕ) : List (ℤ × ℤ) → Prop
  | [] => True
  | [p] => ¬ blue n p ∨ p.2 = 0
  | p :: q :: _ => ¬ blue n p ∨ (p.2 = 0 ∧ ¬ blue n q)
```
Mentions: Usa2008P3.blue
lemma Usa2008P3.chi_of_blue line 112 source
standard axioms: propext what this means
Statement uses: Nat, Prod, Int, Usa2008P3.blue, Eq, Usa2008P3.chi, OfNat.ofNat
Proof uses: ite_eq_left, Neg.neg
4 instances, coercions and auxiliary constants left out.
lemma Usa2008P3.chi_of_not_blue line 114 source
standard axioms: propext what this means
Statement uses: Nat, Prod, Int, Not, Usa2008P3.blue, Eq, Usa2008P3.chi, Neg.neg, OfNat.ofNat
Proof uses: ite_eq_right
5 instances, coercions and auxiliary constants left out.
lemma Usa2008P3.sig_cons line 116 source
standard axioms: propext what this means
Statement uses: Nat, Prod, Int, List, Eq, Usa2008P3.sig, List.cons, HAdd.hAdd, Usa2008P3.chi
Proof uses: rfl
2 instances, coercions and auxiliary constants left out.
lemma Usa2008P3.sig_nil line 119 source
standard axioms: propext what this means
Statement uses: Nat, Eq, Int, Usa2008P3.sig, List.nil, Prod, OfNat.ofNat
Proof uses: rfl
1 instances, coercions and auxiliary constants left out.
lemma Usa2008P3.b0_cons line 121 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Prod, Int, List, Eq, Usa2008P3.b0, List.cons, HAdd.hAdd, ite, And, Usa2008P3.blue, Prod.snd, OfNat.ofNat
Proof uses: id, dite, List.length, List.filter, Decidable.decide, Eq.mpr, congrArg, ite_eq_left, List.filter_cons_of_pos, of_eq_true, Bool, Bool.true, Eq.trans, True, congrFun', Decidable.decide.congr_simp, congr, eq_true, eq_self, and_self and 32 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Usa2008P3.b0_nil line 131 source
standard axioms: propext what this means
Statement uses: Nat, Eq, Int, Usa2008P3.b0, List.nil, Prod, OfNat.ofNat
Proof uses: rfl
1 instances, coercions and auxiliary constants left out.
lemma Usa2008P3.rowK_of_nonneg line 133 source
no axioms what this means
Statement uses: Nat, Int, LE.le, OfNat.ofNat, Eq, Usa2008P3.rowK, HSub.hSub
Proof uses: Eq.mpr, ite, HAdd.hAdd, id, congrArg, rfl, ite_eq_left, Eq.refl
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2008P3.rowK_of_neg line 136 source
no axioms what this means
Statement uses: Nat, Int, Not, LE.le, OfNat.ofNat, Eq, Usa2008P3.rowK, HAdd.hAdd
Proof uses: Eq.mpr, ite, HSub.hSub, id, congrArg, rfl, ite_eq_right, Eq.refl
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2008P3.mem_S line 141 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Int, Iff, Membership.mem, Finset, Usa2008P3.S, LT.lt, HAdd.hAdd, HMul.hMul, OfNat.ofNat, abs, Prod.fst, Prod.snd
Proof uses: id, Eq.mpr, Finset.biUnion, Finset.Icc, Neg.neg, HSub.hSub, SProd.sprod, Usa2008P3.rowK, Singleton.singleton, Exists, And, Eq, congrArg, propext, Finset.mem_biUnion, Iff.intro, LE.le, Eq.mp, Finset.mem_singleton, Finset.mem_Icc and 14 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 44 steps
Open to load the checked before-and-after goal states.
lemma Usa2008P3.rowK_nonneg line 178 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Membership.mem, Finset, Finset.Icc, Neg.neg, HSub.hSub, OfNat.ofNat, LE.le, Usa2008P3.rowK
Proof uses: id, dite, ite, HAdd.hAdd, Eq.mpr, Eq, congrArg, ite_eq_left, Eq.mp, And, propext, Finset.mem_Icc, Not, ite_eq_right
28 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2008P3.adj_cases Adjacent points differ by a unit step in exactly one coordinate line 185 source
Source documentation
Adjacent points differ by a unit step in exactly one coordinate.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Int, Usa2008P3.Adj, Or, And, Eq, Prod.fst, Prod.snd, HAdd.hAdd, OfNat.ofNat, HSub.hSub
Proof uses: abs, LE.le, Neg.neg, LT.lt, abs_cases
34 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma adj_cases {p q : ℤ × ℤ} (h : Adj p q) :
    (p.1 = q.1 ∧ (p.2 = q.2 + 1 ∨ p.2 = q.2 - 1)) ∨
      (p.2 = q.2 ∧ (p.1 = q.1 + 1 ∨ p.1 = q.1 - 1)) := by
…
```
Mentions: h, Usa2008P3.Adj
lemma Usa2008P3.f_diff Along an edge, f changes by ±2, except for the vertical pairs crossing the axis y = -1/2, where it does not change line 194 source
Source documentation
Along an edge, f changes by ±2, except for the vertical pairs crossing the axis y = -1/2, where it does not change.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Int, Usa2008P3.Adj, And, LE.le, abs, HSub.hSub, Usa2008P3.f, OfNat.ofNat, Eq, Prod.fst, Or, Prod.snd, Neg.neg
Proof uses: HAdd.hAdd, Usa2008P3.adj_cases, HMul.hMul, rfl, Eq.mpr, id, congrArg, HAdd, Eq.rec, Eq.refl, Lattice, AddGroup, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, Nat, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 37 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 79 steps
Open to load the checked before-and-after goal states.
```
lemma f_diff {p q : ℤ × ℤ} (h : Adj p q) :
    |f p - f q| ≤ 2 ∧
      (f p = f q → p.1 = q.1 ∧ ((p.2 = 0 ∧ q.2 = -1) ∨ (p.2 = -1 ∧ q.2 = 0))) := by
…
```
Mentions: h, Usa2008P3.Adj, Usa2008P3.f
lemma Usa2008P3.blue_adj Two adjacent blue points form a vertical pair crossing the axis line 264 source
Source documentation
Two adjacent blue points form a vertical pair crossing the axis.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Int, Usa2008P3.Adj, Usa2008P3.blue, And, Eq, Prod.fst, Or, Prod.snd, OfNat.ofNat, Neg.neg
Proof uses: Usa2008P3.f, LE.le, abs, HSub.hSub, And.left, Usa2008P3.f_diff, Int.ModEq, Int.ModEq.trans, HMul.hMul, Int.ModEq.symm, Eq.mp, congrArg, propext, abs_le, Dvd.dvd, Int.modEq_iff_dvd, And.right
30 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma blue_adj {n : ℕ} {p q : ℤ × ℤ} (hadj : Adj p q) (hp : blue n p) (hq : blue n q) :
    p.1 = q.1 ∧ ((p.2 = 0 ∧ q.2 = -1) ∨ (p.2 = -1 ∧ q.2 = 0)) := by
…
```
Mentions: Usa2008P3.Adj, Usa2008P3.blue
lemma Usa2008P3.Icc_neg_eq_map The symmetric integer interval [-K, K] as a map of range (2K+1) line 277 source
Source documentation
The symmetric integer interval [-K, K] as a map of range (2K+1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset, Int, Finset.Icc, Neg.neg, Finset.map, Function.Embedding.mk, HSub.hSub, Finset.range, HAdd.hAdd, HMul.hMul, OfNat.ofNat
Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, And, LE.le, Exists, LT.lt, id, congr, congrArg, Eq.trans, Function.Embedding, funext, congrFun', Iff.intro, Int.toNat, Int.toNat_of_nonneg, Exists.intro, And.intro
46 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma Icc_neg_eq_map (K : ℕ) :
    Finset.Icc (-(K : ℤ)) (K : ℤ) =
      (Finset.range (2 * K + 1)).map ⟨fun i : ℕ ↦ (i : ℤ) - (K : ℤ), by
        intro a b h
        dsimp only at h
        lia⟩ := by
…
```
Mentions: h
lemma Usa2008P3.sum_range_neg_one line 293 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, Finset.sum, Finset.range, HAdd.hAdd, HMul.hMul, OfNat.ofNat, HPow.hPow, Neg.neg
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrFun', congrArg, Singleton.singleton, Finset, MulZeroClass.mul_zero, zero_add, Finset.sum_singleton, pow_zero, eq_self, Eq.mpr, id, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos and 49 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa2008P3.row_sum The ±1 alternating sum over a symmetric interval equals 1 (each row of S n has one more blue point than red points) line 303 source
Source documentation
The ±1 alternating sum over a symmetric interval equals 1 (each row of S n has one more blue point than red points).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Even, HSub.hSub, Eq, Finset.sum, Finset.Icc, Neg.neg, ite, HAdd.hAdd, OfNat.ofNat
Proof uses: Iff, Eq.mpr, Dvd.dvd, id, congr, congrArg, Iff.intro, Eq.mp, Int.even_coe_nat, Finset.map, Function.Embedding.mk, Finset.range, HMul.hMul, Finset, Usa2008P3.Icc_neg_eq_map, Function.Embedding, Finset.sum_map, congrFun', Finset.sum_congr, Eq.refl and 9 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma row_sum (K : ℕ) (c : ℤ) (hc : Even (c - (K : ℤ))) :
    ∑ x ∈ Finset.Icc (-(K : ℤ)) (K : ℤ), (if Even (x + c) then (1 : ℤ) else -1) = 1 := by
…
```
lemma Usa2008P3.chi_eq The colour of (x, y) as an explicit parity test line 320 source
Source documentation
The colour of (x, y) as an explicit parity test.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Eq, Usa2008P3.chi, Prod.mk, ite, LE.le, OfNat.ofNat, Even, HSub.hSub, HAdd.hAdd, Neg.neg
Proof uses: dite, Eq.mpr, id, congrArg, ite_eq_left, Usa2008P3.f, HMul.hMul, abs, rfl, abs_of_nonneg, Eq.refl, Usa2008P3.blue, Usa2008P3.chi_of_blue, Int.ModEq, Dvd.dvd, propext, even_iff_two_dvd, Eq.mp, Int.modEq_iff_dvd, Not and 38 more
73 instances, coercions and auxiliary constants left out.

Tactic trace: 52 steps
Open to load the checked before-and-after goal states.
```
lemma chi_eq (n : ℕ) (x y : ℤ) :
    chi n (x, y) =
      if 0 ≤ y then (if Even (x + y + 1 - (n : ℤ)) then (1 : ℤ) else -1)
        else (if Even (x - y - (n : ℤ)) then (1 : ℤ) else -1) := by
…
```
Mentions: Usa2008P3.chi
lemma Usa2008P3.inner_sum The colour sum over the row at height y equals 1 line 370 source
Source documentation
The colour sum over the row at height y equals 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Membership.mem, Finset, Finset.Icc, Neg.neg, HSub.hSub, OfNat.ofNat, Eq, Finset.sum, Prod, SProd.sprod, Usa2008P3.rowK, Singleton.singleton, Usa2008P3.chi
Proof uses: Eq.mpr, Prod.mk, id, congrArg, Finset.sum_product, congrFun', Finset.sum_congr, Eq.refl, Finset.sum_singleton, LE.le, Usa2008P3.rowK_nonneg, Int.toNat, Int.toNat_of_nonneg, Eq.symm, dite, Even, HAdd.hAdd, Usa2008P3.rowK_of_nonneg, Exists.intro, Mathlib.Tactic.Ring.of_eq and 42 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
```
lemma inner_sum (n : ℕ) (y : ℤ) (hy : y ∈ Finset.Icc (-(n : ℤ)) ((n : ℤ) - 1)) :
    ∑ p ∈ (Finset.Icc (-(rowK n y)) (rowK n y)) ×ˢ {y}, chi n p = 1 := by
…
```
Mentions: Usa2008P3.rowK, Usa2008P3.chi
lemma Usa2008P3.sum_chi There are 2n more blue points than red points in S n line 402 source
Source documentation
There are 2n more blue points than red points in S n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, Finset.sum, Prod, Usa2008P3.S, Usa2008P3.chi, HMul.hMul, OfNat.ofNat
Proof uses: id, Eq.mpr, Finset.biUnion, Finset.Icc, Neg.neg, HSub.hSub, SProd.sprod, Finset, Usa2008P3.rowK, Singleton.singleton, congrArg, Finset.sum_biUnion, Membership.mem, Set, Ne, Function.onFun, Disjoint, Not, propext, Finset.disjoint_left and 62 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma sum_chi (n : ℕ) : ∑ p ∈ S n, chi n p = 2 * (n : ℤ) := by
…
```
Mentions: Usa2008P3.S, Usa2008P3.chi
lemma Usa2008P3.card_B0 Exactly n points of S n are blue and lie on the axis y = 0 line 420 source
Source documentation
Exactly n points of S n are blue and lie on the axis y = 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Prod, Int, Finset.filter, And, Usa2008P3.blue, Prod.snd, OfNat.ofNat, Usa2008P3.S
Proof uses: Usa2008P3.f, HAdd.hAdd, HMul.hMul, Prod.fst, abs, rfl, Eq.mpr, id, congrArg, of_eq_true, Eq.trans, True, congrFun', Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_abs_nonneg, Mathlib.Meta.NormNum.isNat_add, Eq.refl, Mathlib.Meta.NormNum.isNat_mul, Mathlib.Meta.NormNum.isNat_ofNat, eq_self and 73 more
102 instances, coercions and auxiliary constants left out.

Tactic trace: 61 steps
Open to load the checked before-and-after goal states.
```
lemma card_B0 (n : ℕ) :
    ((S n).filter (fun p ↦ blue n p ∧ p.2 = 0)).card = n := by
…
```
Mentions: Usa2008P3.S, Usa2008P3.blue
lemma Usa2008P3.path_bound Every path's colour sum exceeds its number of blue axial points by at most one; moreover, if the path has a "good head" (GH), the sum is at most the count itself line 479 source
Source documentation
Every path's colour sum exceeds its number of blue axial points by at most one; moreover, if the path has a "good head" (GH), the sum is at most the count itself. This packages the "cut at blue-blue pairs" argument: each unit of surplus is charged to a distinct blue point of the axis y = 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List, Prod, Int, List.IsChain, Usa2008P3.Adj, List.Nodup, And, LE.le, Usa2008P3.sig, HAdd.hAdd, Usa2008P3.b0, OfNat.ofNat, Usa2008P3.GH
Proof uses: List.rec, List.nil, And.intro, of_eq_true, Eq.trans, True, congrArg, zero_add, List.cons, Not, Membership.mem, Eq.mp, propext, List.nodup_cons, Eq, Exists, Or, List.isChain_cons_iff, dite, Usa2008P3.blue and 93 more
87 instances, coercions and auxiliary constants left out.

Tactic trace: 126 steps
Open to load the checked before-and-after goal states.
```
lemma path_bound {n : ℕ} (P : List (ℤ × ℤ)) (hchain : P.IsChain Adj) (hnodup : P.Nodup) :
    sig n P ≤ b0 n P + 1 ∧ (GH n P → sig n P ≤ b0 n P) := by
…
```
Mentions: P, Usa2008P3.Adj, Usa2008P3.sig, Usa2008P3.b0, Usa2008P3.GH
lemma Usa2008P3.sum_map_flatten line 580 source
standard axioms: propext what this means
Statement uses: List, Prod, Int, Eq, List.sum, List.map, List.flatten
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, OfNat.ofNat, True, congr, congrArg, List.map_nil, eq_self, List.cons, HAdd.hAdd, List.map_cons, HAppend.hAppend, List.map_append, List.sum_append
16 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2008P3.sum_b0_flatten line 588 source
standard axioms: propext what this means
Statement uses: List, Prod, Int, Bool, Eq, List.sum, List.map, List.length, List.filter, List.flatten
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, OfNat.ofNat, True, congr, congrArg, List.map_nil, CharP.cast_eq_zero, Nat, eq_self, Eq.mpr, List.cons, HAdd.hAdd, id, List.map_cons, HAppend.hAppend, List.filter_append, List.length_append and 12 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2008P3.map_sum_add_one line 599 source
standard axioms: propext what this means
Statement uses: List, Prod, Int, Eq, List.sum, List.map, HAdd.hAdd, OfNat.ofNat, List.length
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, True, congr, congrArg, List.map_nil, CharP.cast_eq_zero, Nat, add_zero, eq_self, Eq.mpr, List.cons, id, List.map_cons, congrFun', Nat.cast_add, Nat.cast_one, Mathlib.Tactic.Ring.of_eq and 14 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
problem Usa2008P3.usa2008_p3 USAMO 2008, Problem 3: any partition of Sₙ into paths uses at least n paths line 614 source
Source documentation
USAMO 2008, Problem 3: any partition of Sₙ into paths uses at least n paths. We model a partition as a list of lists of points: each list is a path (its points are distinct, lie in S n, and consecutive points are adjacent), the lists are pairwise disjoint, and together they cover S n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, List, Prod, Int, Membership.mem, Finset, Usa2008P3.S, List.Nodup, List.IsChain, Usa2008P3.Adj, List.Pairwise, List.Disjoint, Exists, And, LE.le, List.length
Proof uses: List.flatten, Iff.mpr, List.nodup_flatten, And.intro, Eq, List.toFinset, Finset.ext, Eq.mpr, Iff, id, congrFun', congrArg, Eq.trans, Iff.intro, List.sum, List.map, Usa2008P3.sig, HMul.hMul, Usa2008P3.chi, Usa2008P3.sum_map_flatten and 90 more
93 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
problem usa2008_p3 (n : ℕ) (_hn : 0 < n) (paths : List (List (ℤ × ℤ)))
    (hmem : ∀ P ∈ paths, ∀ p ∈ P, p ∈ S n)
    (hnodup : ∀ P ∈ paths, P.Nodup)
    (hchain : ∀ P ∈ paths, P.IsChain Adj)
    (hdisj : paths.Pairwise List.Disjoint)
    (hcover : ∀ p ∈ S n, ∃ P ∈ paths, p ∈ P) :
    n ≤ paths.length := by
…
```
Mentions: P, Usa2008P3.S, Usa2008P3.Adj