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

7 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1976, Problem 1

The squares of a 4 x 7 chess board are colored red or blue. Show that however the coloring is done, we can find a rectangle with four distinct corner squares all the same color. Find a counter-example to show that this is not true for a 4 x 6 board.

Imports (4)

Imported by 1 file

Compfiles.lean

def Usa1976P1.HasMonoRectangle Documented declaration: HasMonoRectangle line 32 source
Source documentation
A coloring (true = red, false = blue) of an m × n board has a monochromatic rectangle if there are two distinct rows and two distinct columns whose four intersection squares all have the same color.

no axioms what this means
Statement uses: Nat, Fin, Bool
Proof uses: Exists, And, Ne, Eq
```
def HasMonoRectangle {m n : ℕ} (c : Fin m → Fin n → Bool) : Prop :=
…
```
determine Usa1976P1.counterexample A 4 x 6 coloring with no monochromatic rectangle line 48 source
Source documentation
A 4 x 6 coloring with no monochromatic rectangle. Written row by row, with true = red:
```
R B R B R B
R B B R B R
B R R B B R
B R B R R B
```
Every column has two red and two blue squares, and no two columns have their red squares in the same two rows or their blue squares in the same two rows, so there can be no monochromatic rectangle.
standard axioms: propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Bool
Proof uses: Matrix.vecCons, Bool.true, Bool.false, Matrix.vecEmpty
2 instances, coercions and auxiliary constants left out.
```
determine counterexample : Fin 4 → Fin 6 → Bool :=
…
```
def Usa1976P1.monoTriples The monochromatic pairs of rows in column j, tagged with their color: (r1, r2, b) means r1 < r2 and both squares (r1, j) and (r2, j) have color b line 59 source
Source documentation
The monochromatic pairs of rows in column j, tagged with their color: (r1, r2, b) means r1 < r2 and both squares (r1, j) and (r2, j) have color b.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Bool, Finset, Prod
Proof uses: Finset.filter, And, LT.lt, Prod.fst, Prod.snd, Eq, Finset.univ
9 instances, coercions and auxiliary constants left out.
```
def monoTriples (c : Fin 4 → Fin 7 → Bool) (j : Fin 7) :
    Finset (Fin 4 × Fin 4 × Bool) :=
…
```
lemma Usa1976P1.two_le_card_monoTriples Documented declaration: two_le_card_monoTriples line 67 source
Source documentation
In any column of 4 squares colored with 2 colors, if k squares are red then 4 - k are blue, so the number of monochromatic pairs of squares is k.choose 2 + (4 - k).choose 2 ≥ 1 + 1 = 2. There are only 16 possible columns, so we check them all.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Bool, LE.le, Finset.card, Prod, Usa1976P1.monoTriples
Proof uses: Finset.filter, And, LT.lt, Prod.fst, Prod.snd, Eq, Finset.univ, of_decide_eq_true, id, Decidable.decide, Bool.true, Eq.refl
15 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma two_le_card_monoTriples (c : Fin 4 → Fin 7 → Bool) (j : Fin 7) :
    2 ≤ (monoTriples c j).card := by
…
```
Mentions: Usa1976P1.monoTriples
lemma Usa1976P1.card_colored_rowPairs There are 6 pairs of distinct rows and 2 colors, hence 12 colored pairs of rows line 77 source
Source documentation
There are 6 pairs of distinct rows and 2 colors, hence 12 colored pairs of rows.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finset.card, Prod, Fin, OfNat.ofNat, Bool, Finset.filter, LT.lt, Prod.fst, Prod.snd, Finset.univ
Proof uses: of_decide_eq_true, id, Decidable.decide, Bool.true, Eq.refl
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma card_colored_rowPairs :
    (Finset.univ.filter fun t : Fin 4 × Fin 4 × Bool ↦ t.1 < t.2.1).card = 12 := by
…
```
problem Usa1976P1.usa1976_p1_first line 83 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Bool, Usa1976P1.HasMonoRectangle
Proof uses: id, Decidable.byContradiction, Exists, And, Ne, Eq, Not, Set.PairwiseDisjoint, Finset, Prod, Finset.univ, Usa1976P1.monoTriples, Membership.mem, Set, Eq.mpr, Function.onFun, Disjoint, Prod.mk, Exists.intro, And.intro and 29 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
problem Usa1976P1.usa1976_p1_second line 118 source
standard axioms: Quot.sound, propext what this means
Statement uses: Not, Usa1976P1.HasMonoRectangle, OfNat.ofNat, Nat, Usa1976P1.counterexample
Proof uses: id, of_decide_eq_true, Exists, Fin, Bool, And, Ne, Eq, Decidable.decide, Bool.true, Eq.refl
8 instances, coercions and auxiliary constants left out.

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