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

47 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2010, Problem 6

There are 68 ordered pairs (not necessarily distinct) of nonzero integers on a blackboard. It's known that for no integer k does both (k, k) and (−k, −k) appear. A student erases some of the 136 integers such that no two erased integers have sum zero, and scores one point for each ordered pair with at least one erased integer. What is the maximum possible score the student can guarantee?

Imports (15)

Imported by 1 file

Compfiles.lean

def Usa2010P6.ValidErase A choice of integers to erase is valid if no two erased integers sum to zero line 48 source
Source documentation
A choice of integers to erase is valid if no two erased integers sum to zero. (If a value x is erased at some position, erasing every occurrence of x is never worse, so the optimal strategies correspond exactly to sets of values T with x ∈ T → -x ∉ T.)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Int
Proof uses: Membership.mem, Not, Neg.neg
3 instances, coercions and auxiliary constants left out.
```
def ValidErase (T : Finset ℤ) : Prop := ∀ x ∈ T, -x ∉ T
```
def Usa2010P6.score The score obtained by erasing the set T from the board L: one point for each ordered pair with at least one erased entry line 52 source
Source documentation
The score obtained by erasing the set T from the board L: one point for each ordered pair with at least one erased entry.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Int, Finset, Nat
Proof uses: List.length, List.filter, Decidable.decide, Or, Membership.mem, Prod.fst, Prod.snd
5 instances, coercions and auxiliary constants left out.
```
def score (L : List (ℤ × ℤ)) (T : Finset ℤ) : ℕ :=
…
```
structure Usa2010P6.ValidBoard A valid board: 68 ordered pairs of nonzero integers such that for no k do both (k, k) and (-k, -k) appear line 57 source
Source documentation
A valid board: 68 ordered pairs of nonzero integers such that for no k do both (k, k) and (-k, -k) appear.

no axioms what this means
Statement uses: List, Prod, Int
```
structure ValidBoard (L : List (ℤ × ℤ)) : Prop where
…
```
determine Usa2010P6.N The maximum score the student can guarantee line 63 source
Source documentation
The maximum score the student can guarantee.

no axioms what this means
Statement uses: Nat
Proof uses: OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
```
determine N : ℕ := 43
…
```
def Usa2010P6.qProb The probability weight: rational 309/500 approximating (√5-1)/2, satisfying q² + q ≤ 1 and 68 * q > 42 line 69 source
Source documentation
The probability weight: rational 309/500 approximating (√5-1)/2, satisfying q² + q ≤ 1 and 68 * q > 42.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Rat
Proof uses: HDiv.hDiv, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
```
def qProb : ℚ := 309 / 500
```
def Usa2010P6.w weight of a strategy t (the set of vertices where we pick the "a" side) line 72 source
Source documentation
weight of a strategy t (the set of vertices where we pick the "a" side)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Rat, Finset, Fin
Proof uses: HMul.hMul, HPow.hPow, Finset.card, HSub.hSub, OfNat.ofNat
8 instances, coercions and auxiliary constants left out.
```
noncomputable def w (n : ℕ) (q : ℚ) (t : Finset (Fin n)) : ℚ :=
…
```
lemma Usa2010P6.cond_weight Conditional marginal: total weight of strategies containing all of S₀ and disjoint from S₁, when S₀ ∩ S₁ = ∅ line 77 source
Source documentation
Conditional marginal: total weight of strategies containing all of S₀ and disjoint from S₁, when S₀ ∩ S₁ = ∅.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Rat, Finset, Fin, Disjoint, Eq, Finset.sum, Finset.univ, ite, And, LE.le, Usa2010P6.w, OfNat.ofNat, HMul.hMul, HPow.hPow, Finset.card, HSub.hSub
Proof uses: Membership.mem, Finset.prod, HAdd.hAdd, Finset.powerset, SDiff.sdiff, Finset.prod_add, id, dite, Not, Iff.mp, Finset.disjoint_left, of_eq_true, Eq.trans, True, congr, congrArg, ite_eq_right_of_eq_false, eq_false, ite_eq_left_of_eq_true, eq_true and 48 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 67 steps
Open to load the checked before-and-after goal states.
```
lemma cond_weight (n : ℕ) (q : ℚ) (S₀ S₁ : Finset (Fin n)) (hd : Disjoint S₀ S₁) :
    ∑ t : Finset (Fin n), (if S₀ ⊆ t ∧ Disjoint t S₁ then w n q t else 0)
      = q ^ S₀.card * (1 - q) ^ S₁.card := by
…
```
Mentions: Usa2010P6.w
lemma Usa2010P6.total_weight total weight = 1 line 141 source
Source documentation
total weight = 1

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Rat, Eq, Finset.sum, Finset, Fin, Finset.univ, Usa2010P6.w, OfNat.ofNat
Proof uses: ite, And, LE.le, EmptyCollection.emptyCollection, Disjoint, HMul.hMul, HPow.hPow, Finset.card, HSub.hSub, Usa2010P6.cond_weight, of_eq_true, Eq.trans, Bot.bot, True, eq_self, Eq.mp, congr, congrArg, Finset.sum_congr, Eq.refl and 5 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma total_weight (n : ℕ) (q : ℚ) : ∑ t : Finset (Fin n), w n q t = 1 := by
…
```
Mentions: Usa2010P6.w
lemma Usa2010P6.w_pos line 145 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Rat, LT.lt, OfNat.ofNat, Finset, Fin, Usa2010P6.w
Proof uses: mul_pos, HPow.hPow, Finset.card, HSub.hSub, pow_pos, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, HMul.hMul, Nat.rawCast, Mathlib.Tactic.Ring.Common.sub_congr and 33 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def Usa2010P6.V The set of absolute values appearing on the board line 153 source
Source documentation
The set of absolute values appearing on the board.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Int, Finset, Nat
Proof uses: List.toFinset, List.flatMap, List.cons, Int.natAbs, Prod.fst, Prod.snd, List.nil
1 instances, coercions and auxiliary constants left out.
```
def V (L : List (ℤ × ℤ)) : Finset ℕ :=
…
```
lemma Usa2010P6.natAbs_mem_V line 156 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Int, Membership.mem, And, Nat, Finset, Usa2010P6.V, Int.natAbs, Prod.fst, Prod.snd
Proof uses: And.intro, Iff.mpr, List.toFinset, List.flatMap, List.cons, List.nil, List.mem_toFinset, Exists, List.mem_flatMap, Exists.intro, of_eq_true, Eq.trans, Or, Eq, True, congr, congrArg, eq_self, False, or_false and 2 more
9 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa2010P6.V_ne_zero line 163 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Int, Usa2010P6.ValidBoard, Nat, Membership.mem, Finset, Usa2010P6.V, Ne, OfNat.ofNat
Proof uses: And, List.cons, Int.natAbs, Prod.fst, Prod.snd, List.nil, Exists, Eq.mp, List.flatMap, congrArg, propext, List.mem_flatMap, List.toFinset, List.mem_toFinset, Usa2010P6.V.eq_1, Usa2010P6.ValidBoard.nonzero, Eq, Or, Eq.trans, False and 7 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
def Usa2010P6.nV number of distinct absolute values line 174 source
Source documentation
number of distinct absolute values

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Int, Nat
Proof uses: Finset.card, Usa2010P6.V
```
noncomputable def nV (L : List (ℤ × ℤ)) : ℕ := (V L).card
```
Mentions: Usa2010P6.V
def Usa2010P6.kE enumeration of the absolute values line 177 source
Source documentation
enumeration of the absolute values

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Int, Fin, Usa2010P6.nV, Nat
Proof uses: Membership.mem, Finset, Usa2010P6.V, OrderIso, Finset.card, Subtype, Finset.orderIsoOfFin
15 instances, coercions and auxiliary constants left out.
```
noncomputable def kE (L : List (ℤ × ℤ)) : Fin (nV L) → ℕ :=
…
```
Mentions: Usa2010P6.nV
lemma Usa2010P6.kE_inj line 180 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Int, Function.Injective, Fin, Usa2010P6.nV, Nat, Usa2010P6.kE
Proof uses: Eq, OrderIso.injective, Finset.card, Usa2010P6.V, Subtype, Membership.mem, Finset, Finset.orderIsoOfFin, rfl, Subtype.ext, OrderIso
13 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2010P6.kE_ne_zero line 185 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Int, Usa2010P6.ValidBoard, Fin, Usa2010P6.nV, Ne, Nat, Usa2010P6.kE, OfNat.ofNat
Proof uses: Membership.mem, Finset, Usa2010P6.V, OrderIso, Finset.card, Subtype, Finset.orderIsoOfFin, rfl, Subtype.property, Usa2010P6.V_ne_zero
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2010P6.kE_cov line 189 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Int, Nat, Membership.mem, Finset, Usa2010P6.V, Exists, Fin, Usa2010P6.nV, Eq, Usa2010P6.kE
Proof uses: Exists.intro, OrderIso, Subtype, Finset.card, OrderIso.symm, Finset.orderIsoOfFin, rfl, Subtype.mk, of_eq_true, Eq.trans, True, congrFun', congrArg, OrderIso.apply_symm_apply, eq_self
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Usa2010P6.aE the "a" side representative: if the negative loop (-k,-k) appears, we take -k as the representative (making all loops "positive"); otherwise k line 195 source
Source documentation
the "a" side representative: if the negative loop (-k,-k) appears, we take -k as the representative (making all loops "positive"); otherwise k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Int, Fin, Usa2010P6.nV
Proof uses: ite, Membership.mem, Prod.mk, Neg.neg, Usa2010P6.kE
9 instances, coercions and auxiliary constants left out.
```
noncomputable def aE (L : List (ℤ × ℤ)) : Fin (nV L) → ℤ :=
…
```
Mentions: Usa2010P6.nV
lemma Usa2010P6.aE_natAbs line 198 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Int, Fin, Usa2010P6.nV, Eq, Nat, Int.natAbs, Usa2010P6.aE, Usa2010P6.kE
Proof uses: dite, Membership.mem, Prod.mk, Neg.neg, of_eq_true, Eq.trans, True, congrFun', congrArg, ite_eq_left_of_eq_true, eq_true, Int.natAbs_neg, eq_self, Not, ite_eq_right_of_eq_false, eq_false
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2010P6.aE_ne_zero line 202 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Int, Usa2010P6.ValidBoard, Fin, Usa2010P6.nV, Ne, Usa2010P6.aE, OfNat.ofNat
Proof uses: Eq, Nat, Int.natAbs, Usa2010P6.kE, Usa2010P6.aE_natAbs, Usa2010P6.kE_ne_zero, Eq.symm, Eq.mp, congrArg, Int.natAbs_zero
3 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2010P6.loop_excl line 209 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Int, Usa2010P6.ValidBoard, Fin, Usa2010P6.nV, Not, Membership.mem, Prod.mk, Neg.neg, Usa2010P6.aE
Proof uses: dite, Usa2010P6.kE, Eq, of_eq_true, Eq.trans, True, congrFun', congrArg, ite_eq_left_of_eq_true, eq_true, eq_self, Eq.mpr, id, Usa2010P6.ValidBoard.no_both_loops, ite_eq_right_of_eq_false, eq_false
13 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
def Usa2010P6.Tof the erased set for strategy t line 220 source
Source documentation
the erased set for strategy t

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Int, Finset, Fin, Usa2010P6.nV
Proof uses: Union.union, Finset.biUnion, Singleton.singleton, Usa2010P6.aE, SDiff.sdiff, Finset.univ, Neg.neg
7 instances, coercions and auxiliary constants left out.
```
noncomputable def Tof (L : List (ℤ × ℤ)) (t : Finset (Fin (nV L))) : Finset ℤ :=
…
```
Mentions: Usa2010P6.nV
lemma Usa2010P6.mem_Tof line 223 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Int, Finset, Fin, Usa2010P6.nV, Iff, Membership.mem, Usa2010P6.Tof, Or, Exists, And, Eq, Usa2010P6.aE, SDiff.sdiff, Finset.univ, Neg.neg
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Union.union, Finset.biUnion, Singleton.singleton, congr, funext, iff_self
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2010P6.validErase_Tof line 227 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Int, Usa2010P6.ValidBoard, Finset, Fin, Usa2010P6.nV, Usa2010P6.ValidErase, Usa2010P6.Tof
Proof uses: Membership.mem, Neg.neg, Or, Eq, Usa2010P6.aE, Nat, Int.natAbs, Usa2010P6.kE, Eq.mpr, id, congrArg, of_eq_true, Eq.trans, True, congrFun', Usa2010P6.aE_natAbs, eq_self, Int.natAbs_neg, Eq.symm, Usa2010P6.kE_inj and 84 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
lemma Usa2010P6.list_filter_length line 263 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Bool, Eq, Nat, List.length, List.filter, List.sum, List.map, ite, Bool.true, OfNat.ofNat
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, True, congrArg, List.map_nil, eq_self, dite, List.cons, Eq.mpr, id, List.filter_cons_of_pos, List.map_cons, HAdd.hAdd, List.sum_cons, List.length_cons, congrFun', ite_eq_left_of_eq_true, Not and 7 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Usa2010P6.sum_finset_list_map line 275 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, List, Rat, Eq, Finset.sum, List.sum, List.map
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, OfNat.ofNat, True, congr, congrArg, funext, List.map_nil, Finset.sum_const_zero, eq_self, Eq.mpr, List.cons, HAdd.hAdd, id, List.map_cons, Finset.sum_add_distrib, Eq.refl
17 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2010P6.score_cast line 285 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Int, Finset, Eq, Rat, Usa2010P6.score, List.sum, List.map, ite, Or, Membership.mem, Prod.fst, Prod.snd, OfNat.ofNat
Proof uses: Nat, Bool, Decidable.decide, Bool.true, List.rec, of_eq_true, List.nil, Eq.trans, True, congr, congrArg, congrFun', funext, ite_congr, Bool.or, Bool.decide_or, Bool.or_eq_true, decide_eq_true_eq, Eq.refl, Not and 26 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Usa2010P6.expected_score line 299 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Int, Eq, Rat, Finset.sum, Finset, Fin, Usa2010P6.nV, Finset.univ, HMul.hMul, Usa2010P6.w, Usa2010P6.qProb, Usa2010P6.score, Usa2010P6.Tof, List.sum, List.map, ite, Or, Membership.mem and 3 more
Proof uses: Trans.trans, Finset.sum_congr, rfl, Eq.mpr, id, congrArg, Usa2010P6.score_cast, Eq.refl, Eq.symm, List.sum_map_mul_left, Usa2010P6.sum_finset_list_map, Add, Zero, Eq.rec, List.map_congr_left, mul_boole
46 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa2010P6.W_ge line 323 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Int, Usa2010P6.ValidBoard, Membership.mem, LE.le, Rat, Usa2010P6.qProb, Finset.sum, Finset, Fin, Usa2010P6.nV, Finset.univ, ite, Or, Usa2010P6.Tof, Prod.fst, Prod.snd, Usa2010P6.w, OfNat.ofNat
Proof uses: And, Ne, Usa2010P6.ValidBoard.nonzero, Nat, Usa2010P6.V, Int.natAbs, Usa2010P6.natAbs_mem_V, Eq, Usa2010P6.kE, Exists, Usa2010P6.kE_cov, Usa2010P6.aE, Neg.neg, Eq.mpr, id, congrArg, Usa2010P6.aE_natAbs, Eq.symm, Iff.mp, Int.natAbs_eq_natAbs_iff and 155 more
165 instances, coercions and auxiliary constants left out.

Tactic trace: 183 steps
Open to load the checked before-and-after goal states.
lemma Usa2010P6.lower_bound line 521 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Prod, Int, Usa2010P6.ValidBoard, Exists, Finset, And, Usa2010P6.ValidErase, LE.le, Nat, OfNat.ofNat, Usa2010P6.score
Proof uses: Rat, List.sum, List.map, Usa2010P6.qProb, Finset.sum, Fin, Usa2010P6.nV, Finset.univ, ite, Or, Membership.mem, Usa2010P6.Tof, Prod.fst, Prod.snd, Usa2010P6.w, List.sum_le_sum, Usa2010P6.W_ge, Eq, HMul.hMul, Eq.mpr and 98 more
127 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
def Usa2010P6.L0 The extremal board: five loops (i,i) for each i ∈ {1,…,8} and one negative edge (-i,-j) for each 1 ≤ j < i ≤ 8 (a K₈ on the negative side) line 549 source
Source documentation
The extremal board: five loops (i,i) for each i ∈ {1,…,8} and one negative edge (-i,-j) for each 1 ≤ j < i ≤ 8 (a K₈ on the negative side).

no axioms what this means
Statement uses: List, Prod, Int
Proof uses: HAppend.hAppend, List.flatMap, List.replicate, OfNat.ofNat, Nat, Prod.mk, HAdd.hAdd, Bind.bind, List.range, Pure.pure, List.map, Neg.neg
13 instances, coercions and auxiliary constants left out.
```
def L0 : List (ℤ × ℤ) :=
…
```
def Usa2010P6.upperLoopList The loop part of L0: five loops (i,i) for each i ∈ {1,…,8} line 554 source
Source documentation
The loop part of L0: five loops (i,i) for each i ∈ {1,…,8}.

no axioms what this means
Statement uses: List, Prod, Int
Proof uses: List.flatMap, Nat, List.replicate, OfNat.ofNat, Prod.mk, HAdd.hAdd, List.range
6 instances, coercions and auxiliary constants left out.
```
def upperLoopList : List (ℤ × ℤ) :=
…
```
def Usa2010P6.upperNegList The negative part of L0: one edge (-i,-j) for each 1 ≤ j < i ≤ 8 line 558 source
Source documentation
The negative part of L0: one edge (-i,-j) for each 1 ≤ j < i ≤ 8.

no axioms what this means
Statement uses: List, Prod, Int
Proof uses: List.flatMap, Nat, List.map, Prod.mk, Neg.neg, HAdd.hAdd, OfNat.ofNat, List.range
7 instances, coercions and auxiliary constants left out.
```
def upperNegList : List (ℤ × ℤ) :=
…
```
lemma Usa2010P6.upperLoopList_def line 562 source
no axioms what this means
Statement uses: Eq, List, Prod, Int, Usa2010P6.upperLoopList, List.flatMap, Nat, List.replicate, OfNat.ofNat, Prod.mk, HAdd.hAdd, List.range
Proof uses: rfl
6 instances, coercions and auxiliary constants left out.
lemma Usa2010P6.upperNegList_def line 567 source
no axioms what this means
Statement uses: Eq, List, Prod, Int, Usa2010P6.upperNegList, List.flatMap, Nat, List.map, Prod.mk, Neg.neg, HAdd.hAdd, OfNat.ofNat, List.range
Proof uses: rfl
7 instances, coercions and auxiliary constants left out.
lemma Usa2010P6.upper_L0_eq line 572 source
no axioms what this means
Statement uses: Eq, List, Prod, Int, Usa2010P6.L0, HAppend.hAppend, Usa2010P6.upperLoopList, Usa2010P6.upperNegList
Proof uses: rfl
2 instances, coercions and auxiliary constants left out.
lemma Usa2010P6.upper_sum_map_range Bridge between List.sum over List.range and Finset.sum over Finset.range line 575 source
Source documentation
Bridge between List.sum over List.range and Finset.sum over Finset.range.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, List.sum, List.map, List.range, Finset.sum, Finset.range
Proof uses: Nat.recAux, of_eq_true, OfNat.ofNat, Eq.trans, True, congrFun', congrArg, List, List.nil, List.map_nil, eq_self, HAdd.hAdd, congr, List.cons, HAppend.hAppend, List.range_succ, List.map_append, List.map_cons, List.sum_append, add_zero and 1 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma upper_sum_map_range (g : ℕ → ℕ) (n : ℕ) :
    ((List.range n).map g).sum = ∑ i ∈ Finset.range n, g i := by
…
```
lemma Usa2010P6.upper_filter_length_eq_card For a list without duplicates, the length of a filtered list equals the cardinality of the corresponding filtered finset line 584 source
Source documentation
For a list without duplicates, the length of a filtered list equals the cardinality of the corresponding filtered finset.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, List.Nodup, Bool, Eq, List.length, List.filter, Finset.card, Finset.filter, Bool.true, List.toFinset
Proof uses: Eq.mpr, id, congrArg, Finset, Eq.symm, List.toFinset_filter, List.toFinset_card_of_nodup, List.Nodup.filter, Eq.refl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma upper_filter_length_eq_card (l : List ℕ) (hl : l.Nodup) (p : ℕ → Bool) :
    (l.filter p).length = (l.toFinset.filter (fun a => p a = true)).card := by
…
```
lemma Usa2010P6.upper_mem_loopList Elements of the loop part of L0 are diagonal pairs (i+1, i+1) with i < 8 line 589 source
Source documentation
Elements of the loop part of L0 are diagonal pairs (i+1, i+1) with i < 8.

standard axioms: Quot.sound, propext what this means
Statement uses: Prod, Int, Membership.mem, List, Usa2010P6.upperLoopList, Exists, Nat, And, LT.lt, OfNat.ofNat, Eq, Prod.mk, HAdd.hAdd
Proof uses: Ne, Eq.mp, Eq.trans, List.flatMap, List.replicate, List.range, congrArg, funext, congr, Exists.intro, And.intro
21 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma upper_mem_loopList {p : ℤ × ℤ} (h : p ∈ upperLoopList) :
    ∃ i : ℕ, i < 8 ∧ p = ((i : ℤ) + 1, (i : ℤ) + 1) := by
…
```
Mentions: h, Usa2010P6.upperLoopList
lemma Usa2010P6.upper_not_mem_negList_diag No diagonal pair (k,k) occurs in the negative part of L0: its entries (-(i+1), -(j+1)) always have j < i, hence distinct components line 597 source
Source documentation
No diagonal pair (k,k) occurs in the negative part of L0: its entries (-(i+1), -(j+1)) always have j < i, hence distinct components.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Not, Membership.mem, Prod, List, Usa2010P6.upperNegList, Prod.mk
Proof uses: Nat, And, LT.lt, OfNat.ofNat, Exists, Eq, Neg.neg, HAdd.hAdd, False, Eq.mp, Eq.trans, List.flatMap, List.map, List.range, congrArg, funext, congr, congrFun', Prod.mk.injEq
17 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma upper_not_mem_negList_diag (k : ℤ) : (k, k) ∉ upperNegList := by
…
```
Mentions: Usa2010P6.upperNegList
lemma Usa2010P6.upper_card_choose_le Documented declaration: upper_card_choose_le line 608 source
Source documentation
The combinatorial heart of the upper bound: for any A : Finset ℕ, a choose 2 ≤ ∑ i ∈ A, #(A ∩ range i), proved by enumerating A in increasing order via Finset.orderEmbOfFin.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, LE.le, HDiv.hDiv, HMul.hMul, Finset.card, HSub.hSub, OfNat.ofNat, Finset.sum, Inter.inter, Finset.range
Proof uses: Eq, Fin, Finset.univ, OrderEmbedding, Finset.orderEmbOfFin, rfl, Finset.image, Finset.sum_image, Set.InjOn.mono, Set.univ, Set.subset_univ, Function.Injective.injOn, RelEmbedding, RelEmbedding.injective, Eq.mp, congrArg, Finset.image_orderEmbOfFin_univ, Function.Injective, Fin.mk, LT.lt.trans and 28 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma upper_card_choose_le (A : Finset ℕ) :
    A.card * (A.card - 1) / 2 ≤ ∑ i ∈ A, (A ∩ Finset.range i).card := by
…
```
lemma Usa2010P6.validBoard_L0 line 648 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2010P6.ValidBoard, Usa2010P6.L0
Proof uses: Usa2010P6.ValidBoard.mk, of_decide_eq_true, Eq, Nat, List.length, Prod, Int, OfNat.ofNat, id, Bool, Decidable.decide, Bool.true, Eq.refl, Membership.mem, List, And, Ne, Prod.fst, Prod.snd, Prod.mk and 18 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma Usa2010P6.upper_loopScore The loop part contributes exactly 5 * a, where a counts the indices i ∈ {1,…,8} with i ∈ T line 668 source
Source documentation
The loop part contributes exactly 5 * a, where a counts the indices i ∈ {1,…,8} with i ∈ T.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Int, Eq, Nat, List.length, Prod, List.filter, Decidable.decide, Or, Membership.mem, Prod.fst, Prod.snd, Usa2010P6.upperLoopList, HMul.hMul, OfNat.ofNat, Finset.card, Finset.filter, HAdd.hAdd, Finset.range
Proof uses: Finset.sum, ite, Eq.mpr, id, congrArg, Eq.symm, Finset.sum_filter, HSMul.hSMul, Finset.sum_const, nsmul_eq_mul, of_eq_true, Eq.trans, True, Nat.mul_comm, eq_self, List.flatMap, List.replicate, Prod.mk, List.range, List and 29 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma upper_loopScore (T : Finset ℤ) :
    (upperLoopList.filter (fun p => decide (p.1 ∈ T ∨ p.2 ∈ T))).length
      = 5 * ((Finset.range 8).filter (fun (i : ℕ) => (i : ℤ) + 1 ∈ T)).card := by
…
```
lemma Usa2010P6.upper_negUnscored The number of unscored negative edges is at least a choose 2: for each i ∈ A, all edges (-(i+1), -(j+1)) with j ∈ A, j < i are unscored line 686 source
Source documentation
The number of unscored negative edges is at least a choose 2: for each i ∈ A, all edges (-(i+1), -(j+1)) with j ∈ A, j < i are unscored.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Int, Usa2010P6.ValidErase, LE.le, Nat, HDiv.hDiv, HMul.hMul, Finset.card, Finset.filter, Membership.mem, HAdd.hAdd, OfNat.ofNat, Finset.range, HSub.hSub, List.length, Prod, List.filter, Decidable.decide, And, Not and 3 more
Proof uses: Eq.mpr, id, Eq, congrArg, rfl, Finset.filter_subset, le_trans, Finset.sum, Inter.inter, Usa2010P6.upper_card_choose_le, ite, Eq.symm, Finset.sum_filter, AddCommMonoid, Eq.rec, Eq.refl, Finset.filter_mem_eq_of_subset, List.flatMap, List.map, Prod.mk and 40 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 41 steps
Open to load the checked before-and-after goal states.
```
lemma upper_negUnscored (T : Finset ℤ) (hT : ValidErase T) :
    ((Finset.range 8).filter (fun (i : ℕ) => (i : ℤ) + 1 ∈ T)).card
        * (((Finset.range 8).filter (fun (i : ℕ) => (i : ℤ) + 1 ∈ T)).card - 1) / 2
      ≤ (upperNegList.filter (fun p => decide (p.1 ∉ T ∧ p.2 ∉ T))).length := by
…
```
Mentions: Usa2010P6.ValidErase
lemma Usa2010P6.upper_arith Case check: for a ≤ 8, 5a + 28 - a(a-1)/2 ≤ 43 line 733 source
Source documentation
Case check: for a ≤ 8, 5a + 28 - a(a-1)/2 ≤ 43.

standard axioms: propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HAdd.hAdd, HMul.hMul, HSub.hSub, HDiv.hDiv
Proof uses: dite, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.symm, le_antisymm, Nat.rawCast, Mathlib.Tactic.IntervalCases.of_le_right, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_ofNat, Not, Nat.ge_of_not_lt, Nat.zero_le
24 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma upper_arith (a : ℕ) (ha : a ≤ 8) : 5 * a + (28 - a * (a - 1) / 2) ≤ 43 := by
…
```
lemma Usa2010P6.upper_score line 736 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Int, Usa2010P6.ValidErase, LE.le, Nat, Usa2010P6.score, Usa2010P6.L0, OfNat.ofNat
Proof uses: Eq, List.length, Prod, Usa2010P6.upperNegList, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, List.filter, Or, Membership.mem, Prod.fst, Prod.snd, Usa2010P6.upperLoopList, HMul.hMul, Finset.card, Finset.filter, HAdd.hAdd and 30 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
problem Usa2010P6.usa2010_p6 line 766 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsGreatest, Nat, Set.ofPred, List, Prod, Int, Usa2010P6.ValidBoard, Exists, Finset, And, Usa2010P6.ValidErase, LE.le, Usa2010P6.score, Usa2010P6.N
Proof uses: And.intro, Membership.mem, Set, upperBounds, Usa2010P6.lower_bound, Usa2010P6.L0, Usa2010P6.validBoard_L0, le_trans, Usa2010P6.upper_score
6 instances, coercions and auxiliary constants left out.

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