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

27 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2017, Problem 5

Determine the set of positive real numbers c such that there exists a labeling of the lattice points in ℤ² with positive integers for which:

only finitely many distinct labels occur, and
for each label i, the distance between any two points labeled i is at least cⁱ.

Imports (2)

Imported by 1 file

Compfiles.lean

determine Usa2017P5.solution_set line 30 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Real
Proof uses: Set.Ioo, OfNat.ofNat, Real.sqrt
6 instances, coercions and auxiliary constants left out.
def Usa2017P5.dist line 32 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Int, Real
Proof uses: Usa2017P5.dist.match_1, Real.sqrt, HAdd.hAdd, HPow.hPow, Nat, HSub.hSub, OfNat.ofNat
11 instances, coercions and auxiliary constants left out.
def Usa2017P5.labelling line 40 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: Subtype, Prod, Int, Nat, And, Set.Finite, Set.range, LT.lt, OfNat.ofNat, Ne, Eq, LE.le, HPow.hPow, Usa2017P5.dist
7 instances, coercions and auxiliary constants left out.
instance Usa2017P5.(instance at line 46) line 46 source
instance Usa2017P5.(instance at line 51) line 51 source
instance Usa2017P5.(instance at line 53) line 53 source
abbrev Usa2017P5.transpose line 55 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Int, Real, Usa2017P5.labelling
Proof uses: HAdd.hAdd, Subtype.mk, Nat, And, Set.Finite, Set.range, LT.lt, OfNat.ofNat, Ne, Eq, LE.le, HPow.hPow, Usa2017P5.dist, Function.comp
13 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
abbrev Usa2017P5.flip line 67 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Usa2017P5.labelling
Proof uses: Prod, Int, Prod.mk, HSub.hSub, HPow.hPow, OfNat.ofNat, Prod.fst, Prod.snd, Subtype.mk, And, Set.Finite, Set.range, LT.lt, Ne, Eq, LE.le, Usa2017P5.dist, Function.comp
14 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P5.dist_lt line 80 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Int, Nat, LE.le, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Subtype, Membership.mem, Finset, Finset.Icc, Neg.neg, HPow.hPow, Or, LT.lt, abs, Prod.fst, Prod.snd, Real, Usa2017P5.dist and 2 more
Proof uses: Eq.mpr, HSub.hSub, id, Eq, congrArg, Usa2017P5.dist.eq_1, Trans.trans, rfl, of_eq_true, Eq.trans, True, congr, congrFun', Int.cast_abs, sq_abs, eq_self, propext, Real.sqrt_lt_sqrt_iff_of_pos, Subtype.mk, add_lt_add_iff_of_le_of_le and 25 more
177 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P5.dist_lt' line 99 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Int, Nat, Eq, HMul.hMul, OfNat.ofNat, HAdd.hAdd, Subtype, Membership.mem, Finset, Finset.Icc, Neg.neg, HPow.hPow, LT.lt, Real, Usa2017P5.dist, Prod.mk, Prod.fst, Prod.snd, Real.sqrt
Proof uses: Eq.mpr, HSub.hSub, id, congrArg, Usa2017P5.dist.eq_1, Trans.trans, LE.le, abs, rfl, of_eq_true, Eq.trans, True, congr, congrFun', Int.cast_abs, sq_abs, eq_self, propext, Real.sqrt_le_sqrt_iff, Subtype.mk and 76 more
173 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P5.dist_ne line 113 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Int, Ne, LE.le, Real, OfNat.ofNat, Usa2017P5.dist
Proof uses: Prod.mk, Eq.mpr, Real.sqrt, HAdd.hAdd, HPow.hPow, Nat, HSub.hSub, id, Eq, congrArg, Usa2017P5.dist.eq_1, Iff.mpr, Real.one_le_sqrt, Eq.trans, congrFun', Eq.symm, Nat.cast_one, congr, Int.cast_one, dite and 84 more
120 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P5.dist_scale line 127 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Eq, Real, Usa2017P5.dist, Prod.mk, HMul.hMul, OfNat.ofNat, Nat
Proof uses: id, Eq.mpr, Real.sqrt, HAdd.hAdd, HPow.hPow, HSub.hSub, congr, congrArg, Eq.trans, congrFun', mul_pow, Int.cast_mul, Int.cast_add, Int.cast_pow, Int.cast_sub, Int.cast_ofNat, Real.sqrt_mul, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl and 67 more
114 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P5.exclusion line 135 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Int, Nat, Ne, Eq, LE.le, Real, HPow.hPow, Real.sqrt, OfNat.ofNat, Usa2017P5.dist, Subtype, Membership.mem, Finset, Finset.Icc, Neg.neg, LT.lt, HAdd.hAdd, Prod.mk, Prod.fst and 2 more
Proof uses: Mathlib.Tactic.Contrapose.contrapose₃, Eq.mpr, Not, Exists, And, id, implies_congr, Eq.refl, Eq.trans, Mathlib.Tactic.Push.not_forall_eq, congrArg, funext, Exists.intro, And.intro, Mathlib.Tactic.Contrapose.contrapose₄, eq_of_heq, HEq, HEq.refl, Eq.symm, And.left and 3 more
71 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P5.square_squeeze' line 149 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2017P5.labelling, Real.sqrt, OfNat.ofNat, Real, Exists, Prod, Subtype, Membership.mem, Finset, Finset.range, HPow.hPow, LT.lt, HMul.hMul, Int, Usa2017P5.instCoeOutProdSubtypeNatMemFinsetRangeHPowOfNatInt.match_1, Prod.mk
Proof uses: Nat.recAux, Exists.intro, Subtype.mk, of_eq_true, Eq.trans, Eq, True, Singleton.singleton, congrFun', congrArg, pow_zero, eq_self, Eq.mpr, And, Set.Finite, Set.range, Not, LE.le, Usa2017P5.dist, id and 143 more
274 instances, coercions and auxiliary constants left out.

Tactic trace: 194 steps
Open to load the checked before-and-after goal states.
def Usa2017P5.label line 294 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Int
2 instances, coercions and auxiliary constants left out.
lemma Usa2017P5.label_max line 301 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Int, LE.le, Usa2017P5.label, HAdd.hAdd, HMul.hMul, OfNat.ofNat
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrArg, congrFun', MulZeroClass.mul_zero, zero_add, Eq.mpr, ite, Odd, Prod.fst, Prod.snd, And, Prod.mk, HDiv.hDiv, id, Eq, Nat.succ, Usa2017P5.label.eq_2
28 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P5.label_finite line 308 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Set.Finite, Set.range, Prod, Int, Usa2017P5.label
Proof uses: Eq.mpr, BddAbove, id, Eq, Exists, Membership.mem, Set, LE.le, congrArg, funext, forall_congr, implies_congr, Eq.refl, Exists.intro, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Usa2017P5.label_max
19 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P5.label_pos line 314 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Int, LT.lt, OfNat.ofNat, Usa2017P5.label
Proof uses: Nat.recAux, of_eq_true, Eq.trans, Eq, True, eq_self, Eq.mpr, HAdd.hAdd, ite, Odd, Prod.fst, Prod.snd, And, Prod.mk, HDiv.hDiv, id, congrArg, Nat.succ, Usa2017P5.label.eq_2
34 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P5.label_cases line 320 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Int, Or, Eq, Usa2017P5.label, HAdd.hAdd, OfNat.ofNat, Prod.mk, HDiv.hDiv, Prod.fst, Prod.snd
Proof uses: dite, Odd, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', ite_eq_left_of_eq_true, ite, And, eq_true, eq_self, False, false_or, true_or, Not, ite_eq_right_of_eq_false, eq_false, or_true
25 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P5.label_one_iff line 326 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Int, Iff, Eq, Usa2017P5.label, HAdd.hAdd, OfNat.ofNat, Odd, Prod.fst, Prod.snd
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P5.label_two_iff line 329 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Int, Iff, Eq, Usa2017P5.label, HAdd.hAdd, OfNat.ofNat, And, Odd, Prod.fst, Prod.snd
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P5.label_more_iff line 332 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Int, Iff, Eq, Usa2017P5.label, HAdd.hAdd, OfNat.ofNat, Prod.mk, HDiv.hDiv, Prod.fst, Prod.snd, And, Even
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P5.label_max_exists_eq line 335 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Int, Eq, Usa2017P5.label, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Exists, Prod.mk, HPow.hPow
Proof uses: Nat.recAux, Exists.intro, Prod.fst, Prod.snd, of_eq_true, Eq.trans, True, congrArg, congr, pow_zero, mul_one, Prod.mk.eta, eq_self, HDiv.hDiv
34 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P5.label_congr line 342 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Int, Eq, Usa2017P5.label, HAdd.hAdd, OfNat.ofNat, Or, And, Odd, Prod.fst, Prod.snd, Even
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2017P5.label_dist For the normal case, following the bound of √2 ^ i < dist p₁ p₂ line 349 source
Source comment
For the normal case, following the bound of √2 ^ i < dist p₁ p₂

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Int, Ne, Nat, Eq, Usa2017P5.label, HAdd.hAdd, HMul.hMul, OfNat.ofNat, LE.le, Real, HPow.hPow, Real.sqrt, Usa2017P5.dist
Proof uses: Nat.recAux, And, Odd, Prod.fst, Prod.snd, Or, Even, Usa2017P5.label_congr, Eq.mpr, id, congrArg, Iff.mpr, Usa2017P5.label_one_iff, pow_one, HSub.hSub, Prod.mk, Usa2017P5.dist.eq_1, propext, Real.sqrt_le_iff, And.intro and 119 more
193 instances, coercions and auxiliary constants left out.

Tactic trace: 68 steps
Open to load the checked before-and-after goal states.
```
lemma label_dist {p₁ p₂ : ℤ × ℤ} (h_ne : p₁ ≠ p₂) {limit : ℕ}
  (hp : label limit p₁ = label limit p₂)
  (hv : label limit p₁ ≠ 2 * limit + 1) : √2 ^ (label limit p₁) ≤ dist p₁ p₂ := by
…
```
Mentions: Usa2017P5.label, Usa2017P5.dist
lemma Usa2017P5.label_dist_max For the last case, where all of the rest of the unfilled squares are marked with the same label line 409 source
Source comment
For the last case, where all of the rest of the unfilled squares are marked with the same label

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Int, Ne, Nat, Eq, Usa2017P5.label, HAdd.hAdd, HMul.hMul, OfNat.ofNat, LE.le, Real, HPow.hPow, Real.sqrt, Usa2017P5.dist
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrFun', congrArg, MulZeroClass.mul_zero, pow_zero, eq_true, Usa2017P5.dist_ne, Exists, Prod.mk, Usa2017P5.label_max_exists_eq, Eq.mpr, id, congr, pow_succ, Usa2017P5.dist_scale, Nat.mul_add_one, pow_add and 23 more
85 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
lemma label_dist_max {p₁ p₂ : ℤ × ℤ} (h : p₁ ≠ p₂) {limit : ℕ}
  (hp₁ : label limit p₁ = 2 * limit + 1) (hp₂ : label limit p₂ = 2 * limit + 1)
  : √2 ^ (2 * limit) ≤ dist p₁ p₂ := by
…
```
Mentions: h, Usa2017P5.label, Usa2017P5.dist
problem Usa2017P5.usa2017_p5 line 431 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Iff, Membership.mem, Set, Usa2017P5.solution_set, And, LT.lt, OfNat.ofNat, Exists, Prod, Int, Nat, Set.Finite, Set.range, Ne, Eq, LE.le, HPow.hPow, Usa2017P5.dist
Proof uses: Eq.mpr, Set.Ioo, Real.sqrt, id, congrArg, Usa2017P5.solution_set.eq_1, propext, Set.mem_Ioo, and_congr_right_iff, Iff.intro, HDiv.hDiv, Real.log, HMul.hMul, HSub.hSub, exists_nat_gt, HAdd.hAdd, Real.pow_lt_iff_lt_log, of_eq_true, Eq.trans, True and 113 more
198 instances, coercions and auxiliary constants left out.

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