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

9 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1990, Problem 1

A license plate has six digits from 0 to 9 and may have leading zeros. If two plates must always differ in at least two places, what is the largest number of plates that is possible?

Imports (5)

Imported by 1 file

Compfiles.lean

abbrev Usa1990P1.Plate A license plate: six digits, each from 0 to 9 (leading zeros allowed) line 32 source
Source documentation
A license plate: six digits, each from 0 to 9 (leading zeros allowed). We model digits as elements of ZMod 10 so that digit sums modulo ten are available for the checksum argument.

no axioms what this means
Proof uses: Fin, OfNat.ofNat, Nat, ZMod
1 instances, coercions and auxiliary constants left out.
```
abbrev Plate := Fin 6 → ZMod 10
```
def Usa1990P1.IsValid A collection of plates is valid if any two distinct plates in it differ in at least two places line 36 source
Source documentation
A collection of plates is valid if any two distinct plates in it differ in at least two places.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Usa1990P1.Plate
Proof uses: Membership.mem, Ne, LE.le, Nat, OfNat.ofNat, hammingDist, Fin, ZMod
6 instances, coercions and auxiliary constants left out.
```
def IsValid (S : Finset Plate) : Prop :=
…
```
Mentions: S, Usa1990P1.Plate
def Usa1990P1.extend The checksum construction: given five digits f : Fin 5 → ZMod 10, build a six-digit plate whose last digit makes the total digit sum congruent to zero modulo ten line 44 source
Source documentation
The checksum construction: given five digits f : Fin 5 → ZMod 10, build a six-digit plate whose last digit makes the total digit sum congruent to zero modulo ten.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, ZMod, Usa1990P1.Plate
Proof uses: HAdd.hAdd, Fin.lastCases, Neg.neg, Finset.sum, Finset.univ
16 instances, coercions and auxiliary constants left out.
```
def extend (f : Fin 5 → ZMod 10) : Plate :=
…
```
Mentions: f, Usa1990P1.Plate
theorem Usa1990P1.sum_extend The digit sum of a plate built by extend is zero modulo ten line 48 source
Source documentation
The digit sum of a plate built by extend is zero modulo ten.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, ZMod, Eq, Finset.sum, Finset.univ, Usa1990P1.extend
Proof uses: Eq.mpr, HAdd.hAdd, Fin.castSucc, Fin.last, id, congrArg, Fin.sum_univ_castSucc, Fin.lastCases, Neg.neg, Fin.lastCases_last, congrFun', Finset.sum_congr, Eq.refl, Finset, Membership.mem, Fin.lastCases_castSucc, add_neg_cancel
35 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem sum_extend (f : Fin 5 → ZMod 10) : ∑ j, extend f j = 0 := by
…
```
Mentions: f, Usa1990P1.extend
theorem Usa1990P1.extend_injective The first five digits determine a plate built by extend line 56 source
Source documentation
The first five digits determine a plate built by extend.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Function.Injective, Fin, OfNat.ofNat, Nat, ZMod, Usa1990P1.Plate, Usa1990P1.extend
Proof uses: Eq, funext, Fin.castSucc, congrFun, Eq.mp, congr, congrArg, Fin.lastCases_castSucc, HAdd.hAdd, Neg.neg, Finset.sum, Finset.univ
16 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem extend_injective : Function.Injective extend := by
…
```
Mentions: Usa1990P1.extend
theorem Usa1990P1.hammingDist_ge_two_of_sum_eq Two plates with the same digit sum modulo ten cannot differ in exactly one place; hence distinct plates of equal sum differ in at least two places line 65 source
Source documentation
Two plates with the same digit sum modulo ten cannot differ in exactly one place; hence distinct plates of equal sum differ in at least two places.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, ZMod, OfNat.ofNat, Eq, Finset.sum, Finset.univ, Ne, LE.le, hammingDist
Proof uses: Finset.card, Finset.filter, Finset, Singleton.singleton, Exists, False, Iff.mp, Finset.card_eq_one, Membership.mem, Eq.rec, Finset.mem_singleton_self, Eq.symm, And.right, And, Finset.mem_filter, HSub.hSub, Eq.mpr, id, congrArg, Finset.sum_sub_distrib and 14 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
theorem hammingDist_ge_two_of_sum_eq {n : ℕ} {p q : Fin n → ZMod 10}
    (hsum : ∑ i, p i = ∑ i, q i) (hne : p ≠ q) :
    2 ≤ hammingDist p q := by
…
```
theorem Usa1990P1.card_le_of_valid Upper bound: a valid collection of plates has at most 10 ^ 5 members line 99 source
Source documentation
Upper bound: a valid collection of plates has at most 10 ^ 5 members. Indeed, two plates agreeing on the first five digits differ in at most one place, so the "first five digits" map is injective on any valid collection, whose codomain has size 10 ^ 5.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Usa1990P1.Plate, Usa1990P1.IsValid, LE.le, Nat, Finset.card, HPow.hPow, OfNat.ofNat
Proof uses: Set.InjOn, Fin, ZMod, Fin.castSucc, Membership.mem, Set, Eq, Decidable.byContradiction, Not, hammingDist, Iff.mp, Finset.mem_coe, Finset.filter, Ne, Finset.univ, Singleton.singleton, HAdd.hAdd, Fin.last, Iff.mpr, Finset.mem_singleton and 22 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
theorem card_le_of_valid {S : Finset Plate} (hS : IsValid S) :
    S.card ≤ 10 ^ 5 := by
…
```
Mentions: S, Usa1990P1.Plate, Usa1990P1.IsValid
determine Usa1990P1.answer line 123 source
standard axioms: propext what this means
Statement uses: Nat
Proof uses: HPow.hPow, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
problem Usa1990P1.usa1990_p1 line 125 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsGreatest, Nat, Set.ofPred, Exists, Finset, Usa1990P1.Plate, And, Eq, Finset.card, Usa1990P1.IsValid, Usa1990P1.answer
Proof uses: And.intro, Membership.mem, Set, upperBounds, Exists.intro, Finset.image, Fin, OfNat.ofNat, ZMod, Usa1990P1.extend, Finset.univ, id, Eq.mpr, HPow.hPow, congrArg, Finset.card_image_of_injOn, Function.Injective.injOn, Usa1990P1.extend_injective, Fintype.card, Finset.card_univ and 18 more
28 instances, coercions and auxiliary constants left out.

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