`Compfiles/Usa2014P6.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 2014, Problem 6

Prove that there is a constant c > 0 with the following property: If a, b, n are positive integers such that gcd(a + i, b + j) > 1 for all i, j ∈ {0, 1, ..., n}, then min{a, b} > (cn)ⁿ.

Imports (13)

Imported by 1 file

Compfiles.lean

lemma Usa2014P6.sum_range_one_div_le_aux Dyadic bound for harmonic sums: the sum of 1/(k+1) for k < 2^m - 1 is at most m line 42 source
Source documentation
Dyadic bound for harmonic sums: the sum of 1/(k+1) for k < 2^m - 1 is at most m.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Rat, Finset.sum, Finset.range, HSub.hSub, HPow.hPow, OfNat.ofNat, HDiv.hDiv, HAdd.hAdd
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, EmptyCollection.emptyCollection, Finset, Inv.inv, congrFun', pow_zero, tsub_self, funext, one_div, CharP.cast_eq_zero, Eq, HMul.hMul, pow_succ, Nat.one_le_pow, Mathlib.Meta.NormNum.isNat_lt_true and 89 more
147 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
```
lemma sum_range_one_div_le_aux (m : ℕ) :
    ∑ k ∈ Finset.range (2 ^ m - 1), (1 : ℚ) / (k + 1) ≤ m := by
…
```
lemma Usa2014P6.sum_Icc_one_div_le_clog The harmonic sum ∑ k ∈ Icc 1 M, 1/k is at most Nat.clog 2 (M + 1) line 76 source
Source documentation
The harmonic sum ∑ k ∈ Icc 1 M, 1/k is at most Nat.clog 2 (M + 1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Rat, Finset.sum, Finset.Icc, OfNat.ofNat, HDiv.hDiv, Nat.clog, HAdd.hAdd
Proof uses: HPow.hPow, Nat.le_pow_clog, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, HSub.hSub, Eq, Finset, Finset.Ico, Eq.symm, Finset.Ico_add_one_right_eq_Icc, Finset.range, Eq.mpr, id, congrArg, Finset.sum_Ico_eq_sum_range, Nat.add_sub_cancel_right, Nat.cast_add and 17 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma sum_Icc_one_div_le_clog (M : ℕ) :
    ∑ k ∈ Finset.Icc 1 M, (1 : ℚ) / k ≤ Nat.clog 2 (M + 1) := by
…
```
lemma Usa2014P6.primesum_inv_sq_le The sum of 1/p^2 over the primes p ≤ M is bounded away from 1/2 (with room to spare for lower order terms) line 100 source
Source documentation
The sum of 1/p^2 over the primes p ≤ M is bounded away from 1/2 (with room to spare for lower order terms).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Rat, Finset.sum, Finset.filter, Nat.Prime, Finset.range, HAdd.hAdd, HDiv.hDiv, HPow.hPow
Proof uses: Eq, LT.lt, Finset, Not, Finset.filter_congr, Membership.mem, Nat.not_lt, Eq.mpr, id, congrArg, Eq.symm, Finset.sum_filter_add_sum_filter_not, HSub.hSub, Finset.sum_le_sum_of_subset_of_nonneg, And, Eq.trans, congrFun', And.intro, And.right, Eq.mp and 185 more
174 instances, coercions and auxiliary constants left out.

Tactic trace: 80 steps
Open to load the checked before-and-after goal states.
```
lemma primesum_inv_sq_le (M : ℕ) (hM : 50 ≤ M) :
    ∑ p ∈ (Finset.range (M + 1)).filter Nat.Prime, (1 : ℚ) / p ^ 2 ≤ 47 / 100 := by
…
```
lemma Usa2014P6.card_filter_dvd_le The number of i < N with p ∣ a + i is at most N / p + 1, as a rational inequality line 179 source
Source documentation
The number of i < N with p ∣ a + i is at most N / p + 1, as a rational inequality.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, Rat, Finset.card, Finset.filter, Dvd.dvd, HAdd.hAdd, Finset.range, HDiv.hDiv
Proof uses: Eq, Finset.Ioc, HSub.hSub, Finset.card_bij, Membership.mem, Finset, Eq.mpr, And, id, Eq.trans, congrFun', congrArg, And.intro, Eq.mp, propext, Finset.mem_range, Finset.mem_filter, And.right, Nat.add_left_cancel, Exists.intro and 101 more
147 instances, coercions and auxiliary constants left out.

Tactic trace: 73 steps
Open to load the checked before-and-after goal states.
```
lemma card_filter_dvd_le (a N p : ℕ) (ha : 0 < a) (hp : 0 < p) :
    (((range N).filter (fun i => p ∣ a + i)).card : ℚ) ≤ (N : ℚ) / p + 1 := by
…
```
lemma Usa2014P6.two_hundred_mul_succ_le_pow Auxiliary exponential bound used in the estimate 100 * clog 2 (n^2) ≤ n line 248 source
Source documentation
Auxiliary exponential bound used in the estimate 100 * clog 2 (n^2) ≤ n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HMul.hMul, HAdd.hAdd, HPow.hPow
Proof uses: Nat.le_induction, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_mul, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.isNat_add, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.trans, Eq, Nat.pow, Mathlib.Meta.NormNum.IsNatPowT.bit1, Bool, Bool.true, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf and 33 more
84 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma two_hundred_mul_succ_le_pow (k : ℕ) (hk : 15 ≤ k) : 200 * (k + 1) ≤ 2 ^ k := by
…
```
lemma Usa2014P6.hundred_clog_le For n ≥ 2^15 and M + 1 ≤ n^2 we have 100 * Nat.clog 2 (M + 1) ≤ n line 257 source
Source documentation
For n ≥ 2^15 and M + 1 ≤ n^2 we have 100 * Nat.clog 2 (M + 1) ≤ n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HPow.hPow, OfNat.ofNat, HAdd.hAdd, HMul.hMul, Nat.clog
Proof uses: LT.lt, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Nat.log, Nat.le_log_of_pow_le, Nat.lt_pow_succ_log_self, Nat.clog_mono_right, pow_le_pow_left₀, Nat.zero_le, le_of_lt, Eq, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl and 25 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma hundred_clog_le (n M : ℕ) (hn : 2 ^ 15 ≤ n) (hM : M + 1 ≤ n ^ 2) :
    100 * Nat.clog 2 (M + 1) ≤ n := by
…
```
lemma Usa2014P6.pow_gt_final The final numerical inequality: for n ≥ 2^15, (n^2/1000)^((n+3)/2) > (n/65536)^n + n line 278 source
Source documentation
The final numerical inequality: for n ≥ 2^15, (n^2/1000)^((n+3)/2) > (n/65536)^n + n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HPow.hPow, OfNat.ofNat, LT.lt, Real, HAdd.hAdd, HMul.hMul, HDiv.hDiv
Proof uses: cast, Eq.symm, Eq.trans, congrFun', congrArg, pow_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast and 151 more
188 instances, coercions and auxiliary constants left out.

Tactic trace: 161 steps
Open to load the checked before-and-after goal states.
```
lemma pow_gt_final (n : ℕ) (hn : 2 ^ 15 ≤ n) :
    (1 / 65536 * (n : ℝ)) ^ n + n < ((n : ℝ) ^ 2 / 1000) ^ ((n + 3) / 2) := by
…
```
lemma Usa2014P6.row_bound Documented declaration: row_bound line 421 source
Source documentation
The heart of the proof: for n ≥ 2^15, some a + i (and symmetrically some b + j) is divisible by more than (n+1)/2 distinct primes exceeding n^2/1000, which forces a to be huge.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, HPow.hPow, Membership.mem, Finset, Finset.range, HAdd.hAdd, Nat.gcd, Real, HDiv.hDiv
Proof uses: Eq, rfl, le_trans, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.trans, Nat.pow, Mathlib.Meta.NormNum.IsNatPowT.bit1, Bool, Bool.true, Eq.mpr, id, congrArg, HMul.hMul, propext, Nat.le_div_iff_mul_le, Mathlib.Meta.NormNum.isNat_lt_true and 280 more
294 instances, coercions and auxiliary constants left out.

Tactic trace: 316 steps (first 200 of 316)
Open to load the checked before-and-after goal states.
```
lemma row_bound (a b n : ℕ) (ha : 0 < a) (hb : 0 < b) (hn : 2 ^ 15 ≤ n)
    (h : ∀ i ∈ range (n + 1), ∀ j ∈ range (n + 1), 1 < Nat.gcd (a + i) (b + j)) :
    ((n : ℝ) ^ 2 / 1000) ^ ((n + 3) / 2) ≤ (a : ℝ) + n := by
…
```
Mentions: h
problem Usa2014P6.usa2014_p6 line 722 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, Real, And, LT.lt, OfNat.ofNat, Nat, Membership.mem, Finset, Finset.range, HAdd.hAdd, Nat.gcd, HPow.hPow, HMul.hMul, Min.min
Proof uses: Exists.intro, HDiv.hDiv, And.intro, Mathlib.Meta.NormNum.isNNRat_lt_true, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, Inv.inv, Eq.refl, Nat.cast_one, Mathlib.Meta.NormNum.isNNRat_inv_pos, Mathlib.Meta.NormNum.instAtLeastTwo, Nat.mul, Bool, Bool.true, LE.le, Or, lt_or_ge and 121 more
146 instances, coercions and auxiliary constants left out.

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