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

30 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1981, Problem 2

What is the largest number of towns that can meet the following criteria? Each pair is directly linked by just one of air, bus or train. At least one pair is linked by air, at least one pair by bus and at least one pair by train. No town has an air link, a bus link and a train link. No three towns, A, B, C are such that the links between AB, AC and BC are all air, all bus or all train.

Imports (2)

Imported by 1 file

Compfiles.lean

inductive Usa1981P2.Link The three possible link types between two towns line 30 source
Source documentation
The three possible link types between two towns.
```
inductive Link | air | bus | train
  deriving DecidableEq
```
instance Usa1981P2.(instance at line 33) line 33 source
abbrev Usa1981P2.colorsAt The set of link types that town v has to other towns line 38 source
Source documentation
The set of link types that town v has to other towns.
```
abbrev colorsAt {n : ℕ} (f : Fin n → Fin n → Link) (v : Fin n) : Finset Link :=
…
```
Mentions: f, Usa1981P2.Link
abbrev Usa1981P2.Valid Documented declaration: Valid line 44 source
Source documentation
A link assignment on n towns satisfying all the criteria of the problem: it is symmetric, all three link types are used, no town has all three link types, and no three towns are pairwise linked by the same type.
```
abbrev Valid {n : ℕ} (f : Fin n → Fin n → Link) : Prop :=
…
```
Mentions: f, Usa1981P2.Link
determine Usa1981P2.answer line 52 source

theorem Usa1981P2.three_le_card_colorsAt If a town u is linked to three other towns by three pairwise distinct link types, then u has at least three link types line 58 source

Source documentation

If a town u is linked to three other towns by three pairwise distinct link types, then u has at least three link types.

theorem three_le_card_colorsAt {n : ℕ} {f : Fin n → Fin n → Link} {u : Fin n}
    {p q r : Fin n} (hp : p ≠ u) (hq : q ≠ u) (hr : r ≠ u)
    {c₁ c₂ c₃ : Link} (h1 : f u p = c₁) (h2 : f u q = c₂) (h3 : f u r = c₃)
    (d12 : c₁ ≠ c₂) (d13 : c₁ ≠ c₃) (d23 : c₂ ≠ c₃) :
    3 ≤ (colorsAt f u).card := by
…

Mentions: f, Usa1981P2.Link, Usa1981P2.colorsAt

theorem Usa1981P2.fiber_card_le_two Key local fact: no town is linked to three other towns by the same link type line 79 source
Source documentation
Key local fact: no town is linked to three other towns by the same link type. (Among any three such towns, the links would have to avoid that type, and then either one of the three towns has all three link types, or the remaining links form a monochromatic triangle.)
```
theorem fiber_card_le_two {n : ℕ} {f : Fin n → Fin n → Link} (hf : Valid f)
    (v : Fin n) (c : Link) :
    (Finset.univ.filter fun w ↦ w ≠ v ∧ f v w = c).card ≤ 2 := by
…
```
Mentions: f, Usa1981P2.Link, Usa1981P2.Valid
theorem Usa1981P2.card_neighbors_le_four Every town is directly linked to at most four other towns: at most two link types, at most two links of each type line 116 source
Source documentation
Every town is directly linked to at most four other towns: at most two link types, at most two links of each type.
```
theorem card_neighbors_le_four {n : ℕ} {f : Fin n → Fin n → Link} (hf : Valid f)
    (v : Fin n) :
    (Finset.univ.filter (· ≠ v)).card ≤ 4 := by
…
```
Mentions: f, Usa1981P2.Link, Usa1981P2.Valid
theorem Usa1981P2.card_filter_ne line 137 source
def Usa1981P2.pair The ten unordered pairs of towns of Fin 5, in a fixed order line 143 source
Source documentation
The ten unordered pairs of towns of Fin 5, in a fixed order.
```
def pair : Fin 10 → Fin 5 × Fin 5 := fun k ↦
…
```
def Usa1981P2.edgeIdx The position of the unordered pair {i, j} in the list pair line 158 source
Source documentation
The position of the unordered pair {i, j} in the list pair.
```
def edgeIdx (i j : Fin 5) : Fin 10 :=
…
```
def Usa1981P2.mkColor A symmetric link assignment on five towns, reconstructed from its restriction to the ten unordered pairs line 174 source
Source documentation
A symmetric link assignment on five towns, reconstructed from its restriction to the ten unordered pairs.
```
def mkColor (u : Fin 10 → Link) : Fin 5 → Fin 5 → Link :=
…
```
Mentions: Usa1981P2.Link
theorem Usa1981P2.pair_edgeIdx line 177 source
theorem Usa1981P2.mkColor_eq line 181 source
theorem Usa1981P2.valid_mkColor Any valid assignment on five towns restricts to a valid assignment reconstructed from the ten unordered pairs line 192 source
Source documentation
Any valid assignment on five towns restricts to a valid assignment reconstructed from the ten unordered pairs.
```
theorem valid_mkColor {f : Fin 5 → Fin 5 → Link} (hf : Valid f) :
    Valid (mkColor fun k ↦ f (pair k).1 (pair k).2) := by
…
```
Mentions: f, Usa1981P2.Link, Usa1981P2.Valid, Usa1981P2.mkColor, Usa1981P2.pair
def Usa1981P2.seesAll3 Boolean check: does a town whose four links have these types see all three link types? line 223 source
Source documentation
Boolean check: does a town whose four links have these types see all three link types? (The || and && chains are explicitly right-nested so that simp normal forms match anonymous-constructor patterns.)
```
def seesAll3 (a b c d : Link) : Bool :=
…
```
Mentions: Usa1981P2.Link
def Usa1981P2.monoE Boolean check: is the triangle with these three link types monochromatic? line 230 source
Source documentation
Boolean check: is the triangle with these three link types monochromatic?
```
def monoE (x y z : Link) : Bool := x == y && x == z
```
Mentions: Usa1981P2.Link
def Usa1981P2.usesC Boolean check: is link type x used by the assignment u? line 233 source
Source documentation
Boolean check: is link type x used by the assignment u?
```
def usesC (u : Fin 10 → Link) (x : Link) : Bool :=
…
```
Mentions: Usa1981P2.Link
def Usa1981P2.validB A kernel-efficient Boolean version of Valid (mkColor u) line 243 source
Source documentation
A kernel-efficient Boolean version of Valid (mkColor u). The ten unordered pairs of Fin 5 are hard-coded by their positions in pair: the links at town 0 are u 0, u 1, u 2, u 3, at town 1 are u 0, u 4, u 5, u 6, at town 2 are u 1, u 4, u 7, u 8, at town 3 are u 2, u 5, u 7, u 9, and at town 4 are u 3, u 6, u 8, u 9; the ten triangles are listed similarly.
```
def validB (u : Fin 10 → Link) : Bool :=
…
```
Mentions: Usa1981P2.Link
def Usa1981P2.mkU Bundle ten link types into a function Fin 10 → Link line 253 source
Source documentation
Bundle ten link types into a function Fin 10 → Link.
```
def mkU (c₀ c₁ c₂ c₃ c₄ c₅ c₆ c₇ c₈ c₉ : Link) : Fin 10 → Link := fun k ↦
…
```
Mentions: Usa1981P2.Link
theorem Usa1981P2.edgeIdx_symm line 267 source
theorem Usa1981P2.mkColor_apply line 270 source
theorem Usa1981P2.mkColor_symm line 274 source

theorem Usa1981P2.card_le_two_iff A town has at most two link types unless it has all three of them line 281 source

Source documentation

A town has at most two link types unless it has all three of them.

theorem card_le_two_iff {n : ℕ} {f : Fin n → Fin n → Link} {v : Fin n} :
    (colorsAt f v).card ≤ 2 ↔
      ¬((∃ w, w ≠ v ∧ f v w = .air) ∧ (∃ w, w ≠ v ∧ f v w = .bus) ∧
        (∃ w, w ≠ v ∧ f v w = .train)) := by
…

Mentions: f, Usa1981P2.Link, Usa1981P2.colorsAt

theorem Usa1981P2.tri6 The six orderings of the monochromatic-triangle condition on three link types, derived from the canonical one line 322 source
Source documentation
The six orderings of the monochromatic-triangle condition on three link types, derived from the canonical one.
```
theorem tri6 {x y z : Link} (h : ¬(x = y ∧ x = z)) :
    ¬(x = y ∧ x = z) ∧ ¬(x = z ∧ x = y) ∧ ¬(y = x ∧ y = z) ∧
      ¬(y = z ∧ y = x) ∧ ¬(z = x ∧ z = y) ∧ ¬(z = y ∧ z = x) :=
…
```
Mentions: Usa1981P2.Link, h
theorem Usa1981P2.validB_iff The Boolean check validB decides validity of the reconstructed assignment line 333 source
Source documentation
The Boolean check validB decides validity of the reconstructed assignment.
```
theorem validB_iff (u : Fin 10 → Link) : validB u = true ↔ Valid (mkColor u) := by
…
```
Mentions: Usa1981P2.Link, Usa1981P2.validB, Usa1981P2.Valid, Usa1981P2.mkColor
theorem Usa1981P2.check5B The finite check over all 3^10 assignments, evaluated by kernel reduction line 548 source
Source documentation
The finite check over all 3^10 assignments, evaluated by kernel reduction. The enumeration is stated as ten nested quantifiers over Link — three choices each — so that the reduction stays shallow. The first four variables are case-split before the kernel reduction, so that the kernel only ever enumerates 3^6 = 729 assignments at a time; this keeps the peak elaboration memory low.
```
theorem check5B : ∀ c₀ c₁ c₂ c₃ c₄ c₅ c₆ c₇ c₈ c₉ : Link,
    validB (mkU c₀ c₁ c₂ c₃ c₄ c₅ c₆ c₇ c₈ c₉) = false := by
…
```
Mentions: Usa1981P2.Link, Usa1981P2.validB, Usa1981P2.mkU
theorem Usa1981P2.check5 A brute-force check: no link assignment on five towns satisfies all the criteria line 556 source
Source documentation
A brute-force check: no link assignment on five towns satisfies all the criteria. (The conditions only involve the ten unordered pairs, so there are only 3^10 symmetric assignments to check, see check5B.)
```
theorem check5 : ∀ u : Fin 10 → Link, ¬ Valid (mkColor u) := by
…
```
Mentions: Usa1981P2.Link, Usa1981P2.Valid, Usa1981P2.mkColor
theorem Usa1981P2.not_valid_five line 566 source
problem Usa1981P2.usa1981_p2 line 571 source