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

23 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1999, Problem 1

Some checkers placed on an n × n checkerboard satisfy the following conditions: a. every square that does not contain a checker shares a side with one that does; b. given any pair of squares that contain checkers, there is a sequence of squares containing checkers, starting and ending with the given squares, such that every two consecutive squares of the sequence share a side.

Prove that at least (n²-2)/3 checkers have been placed on the board.

Imports (12)

Imported by 1 file

Compfiles.lean

def Usa1999P1.checkerboard line 41 source
no axioms what this means
Statement uses: Nat
Proof uses: Prod, Fin
def Usa1999P1.adjacent line 43 source
no axioms what this means
Statement uses: Nat, Usa1999P1.checkerboard
Proof uses: Usa1999P1.adjacent.match_1, Fin, Or, And, Eq, HAdd.hAdd, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
instance Usa1999P1.checkerboardFintype line 52 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fintype, Usa1999P1.checkerboard
Proof uses: Fintype.mk
2 instances, coercions and auxiliary constants left out.
instance Usa1999P1.checkerboardDecidableEq line 55 source
no axioms what this means
Statement uses: Nat, DecidableEq, Usa1999P1.checkerboard
1 instances, coercions and auxiliary constants left out.
instance Usa1999P1.pathGraphDecidableRel line 58 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, DecidableRel, Fin, SimpleGraph.Adj, SimpleGraph.pathGraph
Proof uses: Eq.mpr, Decidable, Or, Eq, HAdd.hAdd, OfNat.ofNat, inferInstance
7 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
instance Usa1999P1.adjacentDecidableRel line 63 source
no axioms what this means
Statement uses: Nat, DecidableRel, Usa1999P1.checkerboard, Usa1999P1.adjacent
Proof uses: Fin, Decidable, Prod.mk, id, inferInstance, Usa1999P1.adjacent.match_1, Or, And, Eq, HAdd.hAdd, OfNat.ofNat
8 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def Usa1999P1.gridGraph Use the full grid graph and the subgraph induced by the checkers line 71 source
Source comment
Use the full grid graph and the subgraph induced by the checkers.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, SimpleGraph, Usa1999P1.checkerboard
Proof uses: SimpleGraph.boxProd, Fin, SimpleGraph.pathGraph
```
def gridGraph (n : ℕ) : SimpleGraph (checkerboard n) :=
…
```
Mentions: Usa1999P1.checkerboard
lemma Usa1999P1.gridGraph_adj line 74 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa1999P1.checkerboard, Iff, SimpleGraph.Adj, Usa1999P1.gridGraph, Usa1999P1.adjacent
Proof uses: Fin, Prod.mk, Eq.mpr, Or, And, Eq, HAdd.hAdd, OfNat.ofNat, id, congrFun', congrArg, Eq.trans, Prod, SimpleGraph.boxProd, SimpleGraph.pathGraph, Prod.fst, Prod.snd, congr, Iff.intro, Iff.mpr and 8 more
11 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
instance Usa1999P1.gridGraphDecidableRel line 82 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, DecidableRel, Usa1999P1.checkerboard, SimpleGraph.Adj, Usa1999P1.gridGraph
Proof uses: decidable_of_iff, Usa1999P1.adjacent
2 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
instance Usa1999P1.gridGraphNeighborSetFintype line 86 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa1999P1.checkerboard, Fintype, SimpleGraph.neighborSet, Usa1999P1.gridGraph
Proof uses: Fin, id, Prod.mk, SimpleGraph.pathGraph, Membership.mem, Set, Prod.fst, Prod.snd
9 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def Usa1999P1.checkerGraph line 93 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa1999P1.checkerboard, SimpleGraph, Subtype, Membership.mem
Proof uses: SimpleGraph.induce, Usa1999P1.gridGraph
4 instances, coercions and auxiliary constants left out.
instance Usa1999P1.checkerGraphDecidableRel line 96 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa1999P1.checkerboard, DecidableRel, Subtype, Membership.mem, SimpleGraph.Adj, Usa1999P1.checkerGraph
Proof uses: id, inferInstance, SimpleGraph.induce, Usa1999P1.gridGraph, Set, Function.Embedding, Function.Embedding.subtype
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa1999P1.pathGraph_degree_le_two A path vertex has at most one neighbor on each side line 102 source
Source comment
A path vertex has at most one neighbor on each side.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, LE.le, SimpleGraph.degree, SimpleGraph.pathGraph, Membership.mem, Set, SimpleGraph.neighborSet, OfNat.ofNat
Proof uses: Bool, Decidable.decide, Eq, HAdd.hAdd, Eq.mpr, Fintype.card, id, congrArg, Eq.symm, SimpleGraph.card_neighborSet_eq_degree, LE.le.trans_eq, Fintype.card_le_of_injective, Subtype.ext, Fin.ext, Or, Iff.mp, SimpleGraph.Adj, SimpleGraph.pathGraph_adj, Subtype.property, dite and 20 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma pathGraph_degree_le_two {n : ℕ} (x : Fin n) :
    (SimpleGraph.pathGraph n).degree x ≤ 2 := by
…
```
lemma Usa1999P1.gridGraph_degree_le_four A square has at most four side-neighbors line 121 source
Source comment
A square has at most four side-neighbors.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa1999P1.checkerboard, LE.le, SimpleGraph.degree, Usa1999P1.gridGraph, OfNat.ofNat
Proof uses: Prod, Fin, SimpleGraph.boxProd, SimpleGraph.pathGraph, Membership.mem, Set, SimpleGraph.neighborSet, Prod.fst, Prod.snd, Eq.mpr, HAdd.hAdd, id, Eq, congrArg, SimpleGraph.degree_boxProd, Nat.add_le_add, Usa1999P1.pathGraph_degree_le_two
13 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma gridGraph_degree_le_four {n : ℕ} (x : checkerboard n) :
    (gridGraph n).degree x ≤ 4 := by
…
```
Mentions: Usa1999P1.checkerboard, Usa1999P1.gridGraph
lemma Usa1999P1.checkerGraph_preconnected The path hypothesis makes the checker graph preconnected line 131 source
Source comment
The path hypothesis makes the checker graph preconnected.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa1999P1.checkerboard, Membership.mem, Exists, List, And, List.IsChain, Usa1999P1.adjacent, Eq, Option, List.head?, Option.some, List.getLast?, SimpleGraph.Preconnected, Subtype, Usa1999P1.checkerGraph
Proof uses: SimpleGraph.Reachable, Subtype.property, Ne, List.nil, False, False.elim, Eq.mp, eq_false', Option.none, noConfusion_of_Nat, Option.ctorIdx, Eq.symm, List.pmap, Subtype.mk, Eq.mpr, Not, id, congrArg, SimpleGraph.Adj, List.isChain_pmap_of_isChain and 28 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma checkerGraph_preconnected {n : ℕ} {c : Finset (checkerboard n)}
    (hb : ∀ x ∈ c, ∀ y ∈ c,
      ∃ p : List (checkerboard n),
        (∀ z, z ∈ p → z ∈ c) ∧
        List.IsChain adjacent p ∧
        List.head? p = x ∧
        List.getLast? p = y) :
    (checkerGraph c).Preconnected := by
…
```
Mentions: Usa1999P1.checkerboard, Usa1999P1.adjacent, Usa1999P1.checkerGraph
lemma Usa1999P1.preconnected_twice_card_le_sum_degrees_add_two A preconnected finite graph has internal degree sum at least twice its vertex count minus two line 156 source
Source comment
A preconnected finite graph has internal degree sum at least twice its vertex count minus two.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Preconnected, LE.le, Nat, HMul.hMul, OfNat.ofNat, Fintype.card, HAdd.hAdd, Finset.sum, Finset.univ, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet
Proof uses: IsEmpty, Nonempty, Or, Eq, isEmpty_or_nonempty, Or.inl, of_eq_true, Eq.trans, True, congr, congrArg, Fintype.card_eq_zero, MulZeroClass.mul_zero, congrFun', EmptyCollection.emptyCollection, Finset, Finset.sum_congr, Finset.univ_eq_empty, SimpleGraph.IsIsolated.degree_eq_zero, SimpleGraph.IsIsolated and 82 more
104 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma preconnected_twice_card_le_sum_degrees_add_two
    {V : Type*} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj]
    (hG : G.Preconnected) :
    2 * Fintype.card V ≤ (∑ v, G.degree v) + 2 := by
…
```
def Usa1999P1.emptySquares line 169 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa1999P1.checkerboard
Proof uses: SDiff.sdiff, Finset.univ
3 instances, coercions and auxiliary constants left out.
def Usa1999P1.boundaryNeighbors line 173 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa1999P1.checkerboard, Subtype, Membership.mem
Proof uses: SDiff.sdiff, SimpleGraph.neighborFinset, Usa1999P1.gridGraph
8 instances, coercions and auxiliary constants left out.
lemma Usa1999P1.checkerGraph_degree_eq_inter Count checker-neighbors inside the full grid neighborhood line 178 source
Source comment
Count checker-neighbors inside the full grid neighborhood.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa1999P1.checkerboard, Subtype, Membership.mem, Eq, SimpleGraph.degree, Usa1999P1.checkerGraph, Set, SimpleGraph.neighborSet, Finset.card, Inter.inter, SimpleGraph.neighborFinset, Usa1999P1.gridGraph
Proof uses: Function.Embedding, Function.Embedding.mk, Subtype.val_injective, Finset.map, Finset.ext, Eq.mpr, Iff, Exists, SimpleGraph.Adj, Subtype.mk, Iff.mpr, Iff.of_eq, Eq.refl, And, id, congr, congrArg, Eq.trans, funext, congrFun' and 9 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma checkerGraph_degree_eq_inter {n : ℕ} (c : Finset (checkerboard n)) (x : c) :
    (checkerGraph c).degree x =
      ((gridGraph n).neighborFinset x.1 ∩ c).card := by
…
```
Mentions: Usa1999P1.checkerboard, Usa1999P1.checkerGraph, Usa1999P1.gridGraph
lemma Usa1999P1.gridGraph_degree_eq_checkerGraph_degree_add_boundary Split each checker degree into internal and boundary neighbors line 192 source
Source comment
Split each checker degree into internal and boundary neighbors.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa1999P1.checkerboard, Subtype, Membership.mem, Eq, SimpleGraph.degree, Usa1999P1.gridGraph, HAdd.hAdd, Usa1999P1.checkerGraph, Set, SimpleGraph.neighborSet, Finset.card, Usa1999P1.boundaryNeighbors
Proof uses: Eq.mpr, SimpleGraph.neighborFinset, id, congrArg, Eq.symm, SimpleGraph.card_neighborFinset_eq_degree, Inter.inter, Usa1999P1.checkerGraph_degree_eq_inter, SDiff.sdiff, Usa1999P1.boundaryNeighbors.eq_1, Finset.card_inter_add_card_sdiff
25 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma gridGraph_degree_eq_checkerGraph_degree_add_boundary {n : ℕ}
    (c : Finset (checkerboard n)) (x : c) :
    (gridGraph n).degree x.1 = (checkerGraph c).degree x +
      (boundaryNeighbors c x).card := by
…
```
Mentions: Usa1999P1.checkerboard, Usa1999P1.gridGraph, Usa1999P1.checkerGraph, Usa1999P1.boundaryNeighbors
lemma Usa1999P1.emptySquares_card_le_boundary_sum Every empty square is covered by a boundary-neighbor set of some checker line 201 source
Source comment
Every empty square is covered by a boundary-neighbor set of some checker.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa1999P1.checkerboard, Or, Membership.mem, Exists, And, Usa1999P1.adjacent, LE.le, Finset.card, Usa1999P1.emptySquares, Finset.sum, Subtype, Finset.univ, Usa1999P1.boundaryNeighbors
Proof uses: Finset.biUnion, Not, Eq.mp, Eq.trans, SDiff.sdiff, True, congrFun', congrArg, true_and, False.elim, Iff.mpr, Finset.mem_biUnion, Exists.intro, Subtype.mk, And.intro, Finset.mem_univ, Eq.mpr, SimpleGraph.neighborFinset, Usa1999P1.gridGraph, id and 11 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma emptySquares_card_le_boundary_sum {n : ℕ} (c : Finset (checkerboard n))
    (ha : ∀ x : checkerboard n, x ∈ c ∨ (∃ y ∈ c, adjacent x y)) :
    (emptySquares c).card ≤ ∑ x : c, (boundaryNeighbors c x).card := by
…
```
Mentions: Usa1999P1.checkerboard, Usa1999P1.adjacent, Usa1999P1.emptySquares, Usa1999P1.boundaryNeighbors
lemma Usa1999P1.emptySquares_card_add_checker_card Empty squares and checker squares partition the board line 221 source
Source comment
Empty squares and checker squares partition the board.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa1999P1.checkerboard, Eq, HAdd.hAdd, Finset.card, Usa1999P1.emptySquares, HPow.hPow, OfNat.ofNat
Proof uses: Eq.mpr, SDiff.sdiff, Finset.univ, id, congrArg, Usa1999P1.emptySquares.eq_1, Finset.card_sdiff_add_card_eq_card, of_eq_true, LE.le, Fintype.card, Finset.card_univ, Prod, Fin, HMul.hMul, Fintype.card_prod, Fintype.card_fin, pow_two, Eq.refl
28 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma emptySquares_card_add_checker_card {n : ℕ} (c : Finset (checkerboard n)) :
    (emptySquares c).card + c.card = n^2 := by
…
```
Mentions: Usa1999P1.checkerboard, Usa1999P1.emptySquares
problem Usa1999P1.usa1999_p1 line 232 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Usa1999P1.checkerboard, Or, Membership.mem, Exists, And, Usa1999P1.adjacent, List, List.IsChain, Eq, Option, List.head?, Option.some, List.getLast?, LE.le, HPow.hPow, OfNat.ofNat, HAdd.hAdd, HMul.hMul and 1 more
Proof uses: Usa1999P1.emptySquares, Finset.sum, Subtype, Finset.univ, Usa1999P1.boundaryNeighbors, id, Usa1999P1.emptySquares_card_le_boundary_sum, Usa1999P1.emptySquares_card_add_checker_card, SimpleGraph.degree, Usa1999P1.gridGraph, Trans.trans, Finset.sum_le_sum, Usa1999P1.gridGraph_degree_le_four, of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.attach, HSMul.hSMul and 90 more
111 instances, coercions and auxiliary constants left out.

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