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

10 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2012, Problem 1

Find all integers n ≥ 3 such that among any n positive real numbers a₁, a₂, ..., aₙ with

max(a₁, a₂, ..., aₙ) ≤ n · min(a₁, a₂, ..., aₙ),

there exist three that are the side lengths of an acute triangle.

Imports (7)

Imported by 1 file

Compfiles.lean

def Usa2012P1.IsAcuteTriple Documented declaration: IsAcuteTriple line 37 source
Source documentation
Three real numbers are the side lengths of an acute triangle iff the strict triangle inequalities hold and the sum of the squares of any two of them is strictly greater than the square of the third one.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: And, GT.gt, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat
8 instances, coercions and auxiliary constants left out.
```
def IsAcuteTriple (x y z : ℝ) : Prop :=
…
```
def Usa2012P1.IsGood Documented declaration: IsGood line 45 source
Source documentation
The property of n that the problem asks to characterize: among any n positive real numbers whose maximum is at most n times their minimum (here expressed as a i ≤ n * a j for all indices i j), some three are the side lengths of an acute triangle.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Fin, Real, LT.lt, OfNat.ofNat, LE.le, HMul.hMul, Exists, And, Ne, Usa2012P1.IsAcuteTriple
8 instances, coercions and auxiliary constants left out.
```
def IsGood (n : ℕ) : Prop :=
…
```
determine Usa2012P1.solution_set line 51 source
no axioms what this means
Statement uses: Set, Nat
Proof uses: Set.ofPred, LE.le, OfNat.ofNat
2 instances, coercions and auxiliary constants left out.
lemma Usa2012P1.sq_add_sq_le_of_not_isAcuteTriple For a sorted triple x ≤ y ≤ z of positive reals, failing to be the side lengths of an acute triangle implies z ^ 2 ≥ x ^ 2 + y ^ 2 line 57 source
Source documentation
For a sorted triple x ≤ y ≤ z of positive reals, failing to be the side lengths of an acute triangle implies z ^ 2 ≥ x ^ 2 + y ^ 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, LE.le, Not, Usa2012P1.IsAcuteTriple, HAdd.hAdd, HPow.hPow, Nat
Proof uses: Decidable.byContradiction, LE.le.trans, And.intro, GT.gt, And, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, HMul.hMul, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.pow_congr and 75 more
94 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma sq_add_sq_le_of_not_isAcuteTriple {x y z : ℝ}
    (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) (hxy : x ≤ y) (hyz : y ≤ z)
    (h : ¬ IsAcuteTriple x y z) : x ^ 2 + y ^ 2 ≤ z ^ 2 := by
…
```
Mentions: h, Usa2012P1.IsAcuteTriple
lemma Usa2012P1.sq_lt_fib The Fibonacci numbers outgrow the squares from index 13 on line 76 source
Source documentation
The Fibonacci numbers outgrow the squares from index 13 on.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, HPow.hPow, Nat.fib
Proof uses: And, HAdd.hAdd, Nat.le_induction, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, And.intro, And.right, HMul.hMul, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, Neg.neg, HSub.hSub, congrArg and 82 more
87 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma sq_lt_fib {m : ℕ} (hm : 13 ≤ m) : m ^ 2 < Nat.fib m := by
…
```
lemma Usa2012P1.fib_mul_sq_le Documented declaration: fib_mul_sq_le line 90 source
Source documentation
If a monotone tuple of positive reals contains no three terms that are the side lengths of an acute triangle, then its squares grow at least as fast as the Fibonacci numbers: b i ^ 2 ≥ F_{i+1} * b 0 ^ 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Real, LT.lt, OfNat.ofNat, Monotone, LE.le, HAdd.hAdd, HPow.hPow, HMul.hMul, Nat.fib, Fin.mk
Proof uses: Nat.twoStepInduction, Eq.mpr, id, Eq, congrFun', congrArg, Eq.trans, zero_add, Nat.cast_one, one_mul, le_refl, Nat.fib_two, pow_le_pow_left₀, le_of_lt, Nat.fib_add_two, add_mul, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub and 56 more
108 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
lemma fib_mul_sq_le {n : ℕ} {b : Fin n → ℝ} (hn : 0 < n)
    (hb_pos : ∀ i, 0 < b i) (hb_mono : Monotone b)
    (hsq : ∀ i j k : Fin n, i < j → j < k → b i ^ 2 + b j ^ 2 ≤ b k ^ 2) :
    ∀ i : ℕ, ∀ h : i < n, (Nat.fib (i + 1) : ℝ) * b ⟨0, hn⟩ ^ 2 ≤ b ⟨i, h⟩ ^ 2 := by
…
```
Mentions: h
lemma Usa2012P1.isGood_of_thirteen_le Every n ≥ 13 has the required property line 120 source
Source documentation
Every n ≥ 13 has the required property.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Usa2012P1.IsGood
Proof uses: Fin, Real, LT.lt, HMul.hMul, Classical.byContradiction, Exists, And, Ne, Usa2012P1.IsAcuteTriple, Not, Equiv.Perm, Tuple.sort, Function.comp, Monotone, Tuple.monotone_sort, Function.Injective, Equiv.injective, HAdd.hAdd, HPow.hPow, Usa2012P1.sq_add_sq_le_of_not_isAcuteTriple and 89 more
96 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
lemma isGood_of_thirteen_le {n : ℕ} (hn : 13 ≤ n) : IsGood n := by
…
```
Mentions: Usa2012P1.IsGood
def Usa2012P1.counterexSeq The counterexample for n ≤ 12: the numbers √F₁, √F₂, ... where F is the Fibonacci sequence line 159 source
Source documentation
The counterexample for n ≤ 12: the numbers √F₁, √F₂, ... where F is the Fibonacci sequence.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Real
Proof uses: Real.sqrt, Nat.fib, HAdd.hAdd, OfNat.ofNat
6 instances, coercions and auxiliary constants left out.
```
noncomputable def counterexSeq (n : ℕ) : Fin n → ℝ := fun i ↦ √(Nat.fib (i.val + 1) : ℝ)
```
lemma Usa2012P1.not_isGood_of_le_twelve No n with 3 ≤ n ≤ 12 has the required property line 162 source
Source documentation
No n with 3 ≤ n ≤ 12 has the required property.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Not, Usa2012P1.IsGood
Proof uses: Nat.fib, HPow.hPow, dite, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.symm, le_antisymm, Nat.rawCast, Mathlib.Tactic.IntervalCases.of_le_right, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_ofNat, Nat.ge_of_not_lt, Mathlib.Tactic.IntervalCases.of_le_left, LT.lt, Real and 99 more
110 instances, coercions and auxiliary constants left out.

Tactic trace: 97 steps
Open to load the checked before-and-after goal states.
```
lemma not_isGood_of_le_twelve {n : ℕ} (h3 : 3 ≤ n) (h12 : n ≤ 12) : ¬ IsGood n := by
…
```
Mentions: Usa2012P1.IsGood
problem Usa2012P1.usa2012_p1 line 244 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Iff, And, LE.le, OfNat.ofNat, Usa2012P1.IsGood, Membership.mem, Set, Usa2012P1.solution_set
Proof uses: Iff.intro, Decidable.byContradiction, Not, Usa2012P1.not_isGood_of_le_twelve, And.intro, Usa2012P1.isGood_of_thirteen_le
11 instances, coercions and auxiliary constants left out.

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