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

12 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1980, Problem 2

Find the maximum possible number of three term arithmetic progressions in a monotone sequence of n distinct reals.

Imports (6)

Imported by 1 file

Compfiles.lean

def Usa1980P2.apPairs For a sequence a : ℕ → ℝ and an index j, the finset of pairs (i, k) with i < j < k < n such that a i, a j, a k forms a three-term arithmetic progression line 47 source
Source documentation
For a sequence a : ℕ → ℝ and an index j, the finset of pairs (i, k) with i < j < k < n such that a i, a j, a k forms a three-term arithmetic progression. Every three-term arithmetic progression with indices below n corresponds to exactly one such pair, with j its middle index.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Finset, Prod
Proof uses: Finset.filter, Eq, HAdd.hAdd, Prod.fst, Prod.snd, HMul.hMul, OfNat.ofNat, SProd.sprod, Finset.range, Finset.Ioo
11 instances, coercions and auxiliary constants left out.
```
noncomputable def apPairs (n : ℕ) (a : ℕ → ℝ) (j : ℕ) : Finset (ℕ × ℕ) :=
…
```
def Usa1980P2.apCount The number of three-term arithmetic progressions among the first n terms of a, counted by their middle index line 52 source
Source documentation
The number of three-term arithmetic progressions among the first n terms of a, counted by their middle index.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: Finset.sum, Finset.range, Finset.card, Prod, Usa1980P2.apPairs
1 instances, coercions and auxiliary constants left out.
```
noncomputable def apCount (n : ℕ) (a : ℕ → ℝ) : ℕ :=
…
```
theorem Usa1980P2.mem_apPairs line 55 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Prod, Iff, Membership.mem, Finset, Usa1980P2.apPairs, And, LT.lt, Prod.fst, Prod.snd, Eq, HAdd.hAdd, HMul.hMul, OfNat.ofNat
Proof uses: Eq.mpr, id, congrFun', congrArg, Eq.trans, Finset.filter, SProd.sprod, Finset.range, Finset.Ioo, congr, Iff.intro, And.intro
35 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Usa1980P2.card_apPairs_le Documented declaration: card_apPairs_le line 63 source
Source documentation
A three-term progression is determined by its middle term together with any one of its other two terms, so the number of progressions with middle index j is at most min j (n - 1 - j).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, StrictMonoOn, Set.Iio, LE.le, Finset.card, Prod, Usa1980P2.apPairs, Min.min, HSub.hSub, OfNat.ofNat
Proof uses: le_min, Finset.range, Finset.card_le_card_of_injOn, Prod.fst, Membership.mem, Set, Finset, Iff.mpr, LT.lt, Finset.mem_range, And.left, And, Prod.snd, Eq, HAdd.hAdd, HMul.hMul, Eq.mp, congrArg, propext, Usa1980P2.mem_apPairs and 69 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
```
theorem card_apPairs_le (n : ℕ) (a : ℕ → ℝ) (ha : StrictMonoOn a (Set.Iio n)) (j : ℕ) :
    (apPairs n a j).card ≤ min j (n - 1 - j) := by
…
```
Mentions: Usa1980P2.apPairs
theorem Usa1980P2.sum_min_step The per-index bounds telescope in steps of two: ∑ j < n + 2, min j (n + 1 - j) = ∑ j < n, min j (n - 1 - j) + n line 98 source
Source documentation
The per-index bounds telescope in steps of two: ∑ j < n + 2, min j (n + 1 - j) = ∑ j < n, min j (n - 1 - j) + n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.sum, Finset.range, HAdd.hAdd, OfNat.ofNat, Min.min, HSub.hSub
Proof uses: Eq.mpr, id, congrArg, Finset.sum_range_succ', Finset.sum_range_succ, congrFun', Eq.trans, congr, Nat.sub_self, Nat.min_zero, add_zero, Nat.zero_min, Membership.mem, Finset, Eq.mp, LT.lt, propext, Finset.mem_range, min_add_add_right, Eq.refl and 11 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
theorem sum_min_step (n : ℕ) :
    (∑ j ∈ range (n + 2), min j (n + 1 - j)) = (∑ j ∈ range n, min j (n - 1 - j)) + n := by
…
```
theorem Usa1980P2.sum_min_closed Closed form of the total bound: ∑ j < n, min j (n - 1 - j) = (n - 1)² / 4 line 111 source
Source documentation
Closed form of the total bound: ∑ j < n, min j (n - 1 - j) = (n - 1)² / 4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.sum, Finset.range, Min.min, HSub.hSub, OfNat.ofNat, HDiv.hDiv, HPow.hPow
Proof uses: And, HAdd.hAdd, Nat.recAux, And.intro, of_eq_true, Eq.trans, True, congr, congrArg, EmptyCollection.emptyCollection, Finset, funext, congrFun', zero_tsub, inf_of_le_right, LE.le, Finset.sum_const_zero, zero_pow, Not, False and 57 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
theorem sum_min_closed (n : ℕ) : (∑ j ∈ range n, min j (n - 1 - j)) = (n - 1)^2 / 4 := by
…
```
theorem Usa1980P2.strictMonoOn_cast The sequence a i = i is strictly increasing on Set.Iio n line 129 source
Source documentation
The sequence a i = i is strictly increasing on Set.Iio n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, StrictMonoOn, Real, Set.Iio
Proof uses: StrictMono.strictMonoOn, strictMono_nat_of_lt_succ, cast, LT.lt, HAdd.hAdd, OfNat.ofNat, Eq.symm, Nat.lt_succ_self
29 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem strictMonoOn_cast (n : ℕ) : StrictMonoOn (fun i : ℕ => (i : ℝ)) (Set.Iio n) :=
…
```
theorem Usa1980P2.card_apPairs_cast Documented declaration: card_apPairs_cast line 135 source
Source documentation
Equality holds in card_apPairs_le for the sequence a i = i: the pairs (j - 1 - d, j + 1 + d) for d < min j (n - 1 - j) are distinct elements of apPairs n (fun i => (i : ℝ)) j.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Prod, Usa1980P2.apPairs, Real, Min.min, HSub.hSub, OfNat.ofNat
Proof uses: le_antisymm, Usa1980P2.card_apPairs_le, Usa1980P2.strictMonoOn_cast, LE.le, Finset.range, Finset.card_le_card_of_injOn, Prod.mk, HAdd.hAdd, Membership.mem, Set, Finset, Eq.mpr, id, congrArg, propext, Finset.mem_coe, And, LT.lt, Prod.fst, Prod.snd and 13 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
theorem card_apPairs_cast (n : ℕ) (j : ℕ) :
    (apPairs n (fun i => (i : ℝ)) j).card = min j (n - 1 - j) := by
…
```
Mentions: Usa1980P2.apPairs
theorem Usa1980P2.apCount_cast The bound is achieved by the sequence a i = i line 159 source
Source documentation
The bound is achieved by the sequence a i = i.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa1980P2.apCount, Real, HDiv.hDiv, HPow.hPow, HSub.hSub, OfNat.ofNat
Proof uses: id, Eq.mpr, Finset.sum, Finset.range, Finset.card, Prod, Usa1980P2.apPairs, Min.min, congrArg, Eq.symm, Usa1980P2.sum_min_closed, Finset.sum_congr, rfl, Finset, Membership.mem, Usa1980P2.card_apPairs_cast
26 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem apCount_cast (n : ℕ) : apCount n (fun i : ℕ => (i : ℝ)) = (n - 1)^2 / 4 := by
…
```
Mentions: Usa1980P2.apCount
theorem Usa1980P2.apCount_le The bound holds for every strictly increasing sequence line 165 source
Source documentation
The bound holds for every strictly increasing sequence.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, StrictMonoOn, Set.Iio, LE.le, Usa1980P2.apCount, HDiv.hDiv, HPow.hPow, HSub.hSub, OfNat.ofNat
Proof uses: id, Eq.mpr, Finset.sum, Finset.range, Finset.card, Prod, Usa1980P2.apPairs, Min.min, Eq, congrArg, Eq.symm, Usa1980P2.sum_min_closed, Finset.sum_le_sum, Membership.mem, Finset, Usa1980P2.card_apPairs_le
30 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem apCount_le (n : ℕ) (a : ℕ → ℝ) (ha : StrictMonoOn a (Set.Iio n)) :
    apCount n a ≤ (n - 1)^2 / 4 := by
…
```
Mentions: Usa1980P2.apCount
determine Usa1980P2.answer line 173 source
standard axioms: propext what this means
Statement uses: Nat
Proof uses: HDiv.hDiv, HPow.hPow, HSub.hSub, OfNat.ofNat
9 instances, coercions and auxiliary constants left out.
problem Usa1980P2.usa1980_p2 line 175 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, IsGreatest, Set.ofPred, Exists, Real, And, StrictMonoOn, Set.Iio, Eq, Usa1980P2.apCount, Usa1980P2.answer
Proof uses: And.intro, Membership.mem, Set, upperBounds, Exists.intro, Usa1980P2.strictMonoOn_cast, Eq.symm, HDiv.hDiv, HPow.hPow, HSub.hSub, OfNat.ofNat, Usa1980P2.apCount_cast, LE.le, Usa1980P2.apCount_le
21 instances, coercions and auxiliary constants left out.

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