`Compfiles/Usa2016P1.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 2016, Problem 1

Let X₁, X₂, …, X₁₀₀ be a sequence of mutually distinct nonempty subsets of a set S. Any two sets Xᵢ and Xᵢ₊₁ are disjoint and their union is not the whole set S, that is, Xᵢ ∩ Xᵢ₊₁ = ∅ and Xᵢ ∪ Xᵢ₊₁ ≠ S, for all i ∈ {1, …, 99}. Find the smallest possible number of elements in S.

Imports (5)

Imported by 1 file

Compfiles.lean

def Usa2016P1.HasChain Documented declaration: HasChain line 35 source
Source documentation
HasChain n means that an n-element set (which we may take to be Fin n) admits a sequence of 100 mutually distinct nonempty subsets in which any two consecutive sets are disjoint and do not cover the whole set.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Exists, Fin, OfNat.ofNat, Finset, And, Finset.Nonempty, Eq, Disjoint, Fin.castSucc, Fin.succ, Ne, Union.union, Finset.univ
6 instances, coercions and auxiliary constants left out.
```
def HasChain (n : ℕ) : Prop :=
…
```
def Usa2016P1.witness An explicit chain of 100 subsets of an 8-element set line 49 source
Source documentation
An explicit chain of 100 subsets of an 8-element set. (Obtained from the inductive construction of the official solution: start from the chain 34, 1, 23, 4, 12, 3, 14, 2, 13 on a 4-element set and repeatedly duplicate the chain, glue the two copies together with the empty set in between, and insert a new element into alternating positions.)

standard axioms: Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Finset
Proof uses: Matrix.vecCons, Insert.insert, Singleton.singleton, Matrix.vecEmpty
7 instances, coercions and auxiliary constants left out.
```
def witness : Fin 100 → Finset (Fin 8) := ![
…
```
lemma Usa2016P1.hasChain_eight The explicit witness verifies that HasChain 8 holds line 152 source
Source documentation
The explicit witness verifies that HasChain 8 holds.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2016P1.HasChain, OfNat.ofNat, Nat
Proof uses: Exists.intro, Fin, Finset, And, Finset.Nonempty, Eq, Disjoint, Fin.castSucc, Fin.succ, Ne, Union.union, Finset.univ, Usa2016P1.witness, And.intro
10 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma hasChain_eight : HasChain 8 :=
…
```
Mentions: Usa2016P1.HasChain
lemma Usa2016P1.not_hasChain_of_le_six Any chain on an n-element set uses at most 2 ^ n - 1 nonempty subsets, so n ≤ 6 is impossible since 2 ^ 6 - 1 < 100 line 157 source
Source documentation
Any chain on an n-element set uses at most 2 ^ n - 1 nonempty subsets, so n ≤ 6 is impossible since 2 ^ 6 - 1 < 100.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Not, Usa2016P1.HasChain
Proof uses: Fin, Finset, And, Finset.Nonempty, Eq, Disjoint, Fin.castSucc, Fin.succ, Ne, Union.union, Finset.univ, False, Finset.image, Finset.erase, EmptyCollection.emptyCollection, Membership.mem, Exists, Eq.mp, congrArg, propext and 24 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma not_hasChain_of_le_six {n : ℕ} (hn : n ≤ 6) : ¬ HasChain n := by
…
```
Mentions: Usa2016P1.HasChain
lemma Usa2016P1.not_hasChain_seven The main combinatorial estimate: no chain exists on a 7-element set line 178 source
Source documentation
The main combinatorial estimate: no chain exists on a 7-element set. Sets of size at least 4 must be preceded by sets of size at most 2, and there are only 28 nonempty subsets of size at most 2 and 35 subsets of size 3, so a chain on 7 elements has length at most 28 + 35 + (28 + 1) = 92 < 100.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Not, Usa2016P1.HasChain, OfNat.ofNat, Nat
Proof uses: Fin, Finset, And, Finset.Nonempty, Eq, Disjoint, Fin.castSucc, Fin.succ, Ne, Union.union, Finset.univ, False, LE.le, HAdd.hAdd, Finset.card, LT.lt, Iff.mpr, Finset.ssubset_univ_iff, Finset.card_lt_card, Eq.mpr and 63 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 100 steps
Open to load the checked before-and-after goal states.
```
lemma not_hasChain_seven : ¬ HasChain 7 := by
…
```
Mentions: Usa2016P1.HasChain
determine Usa2016P1.solution_value line 289 source
no axioms what this means
Statement uses: Nat
Proof uses: OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
problem Usa2016P1.usa2016_p1 line 291 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsLeast, Nat, Set.ofPred, Usa2016P1.HasChain, Usa2016P1.solution_value
Proof uses: Eq, OfNat.ofNat, rfl, And.intro, Membership.mem, Set, lowerBounds, Usa2016P1.hasChain_eight, Eq.mpr, LE.le, id, congrArg, propext, mem_lowerBounds, Decidable.byContradiction, Not, LT.lt, Or, False, lt_or_ge and 4 more
16 instances, coercions and auxiliary constants left out.

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