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

13 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1985, Problem 2

Find all real roots of the quartic x⁴ - (2N + 1)x² - x + N² + N - 1 = 0 correct to 4 decimal places, where N = 10¹⁰.

Imports (6)

Imported by 1 file

Compfiles.lean

lemma Usa1985P2.quartic_eq The quartic of the problem rewrites as (x² - N - 1/2)² - x - 5/4; this is the key observation of the solution (see https://prase.cz/kalva/usa/usoln/usol852.html) line 34 source
Source documentation
The quartic of the problem rewrites as (x² - N - 1/2)² - x - 5/4; this is the key observation of the solution (see https://prase.cz/kalva/usa/usoln/usol852.html).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, HSub.hSub, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul, HDiv.hDiv
Proof uses: Mathlib.Tactic.Ring.of_eq, Int.rawCast, inferInstance, Ring, Int.negOfNat, Nat.rawCast, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Ring.Common.pow_add, Mathlib.Tactic.Ring.Common.single_pow and 71 more
85 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma quartic_eq (N x : ℝ) :
    x ^ 4 - (2 * N + 1) * x ^ 2 - x + N ^ 2 + N - 1 =
      (x ^ 2 - N - 1 / 2) ^ 2 - x - 5 / 4 := by
…
```
def Usa1985P2.f The function whose zeros are the real roots of the quartic line 40 source
Source documentation
The function whose zeros are the real roots of the quartic.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: HSub.hSub, HPow.hPow, Nat, OfNat.ofNat, HDiv.hDiv
17 instances, coercions and auxiliary constants left out.
```
noncomputable def f (N : ℝ) (x : ℝ) : ℝ := (x ^ 2 - N - 1 / 2) ^ 2 - x - 5 / 4
```
lemma Usa1985P2.f_def line 42 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, Usa1985P2.f, HSub.hSub, HPow.hPow, Nat, OfNat.ofNat, HDiv.hDiv
Proof uses: rfl
16 instances, coercions and auxiliary constants left out.
lemma Usa1985P2.f_continuous line 44 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Continuous, Usa1985P2.f
Proof uses: id, Eq.mpr, HSub.hSub, HPow.hPow, Nat, OfNat.ofNat, HDiv.hDiv, Inv.inv, Eq, congrArg, funext, congrFun', one_div, Continuous.add_const, Continuous.fun_add, Neg.neg, Continuous.fun_pow, continuous_id', ContinuousNeg.continuous_neg
39 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa1985P2.exists_root_of_sign_change A sign change of f N on an interval locates a root in its interior line 49 source
Source documentation
A sign change of f N on an interval locates a root in its interior.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, LT.lt, HMul.hMul, Usa1985P2.f, OfNat.ofNat, Exists, And, Membership.mem, Set, Set.Ioo, Eq
Proof uses: ContinuousOn, Set.Icc, Continuous.continuousOn, Usa1985P2.f_continuous, Or, Iff.mp, mul_neg_iff, HAdd.hAdd, Set.image, intermediate_value_Ioo', And.intro, Exists.intro, intermediate_value_Ioo
67 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma exists_root_of_sign_change {N : ℝ} {a b : ℝ} (hab : a ≤ b)
    (h : f N a * f N b < 0) : ∃ x ∈ Set.Ioo a b, f N x = 0 := by
…
```
Mentions: h, Usa1985P2.f
lemma Usa1985P2.f_pos_of_nonpos Documented declaration: f_pos_of_nonpos line 63 source
Source documentation
The quartic has no nonpositive real roots when N = 10^10: for x ≤ -5/4 the right side x + 5/4 of (x² - N - 1/2)² = x + 5/4 is too small, and for -5/4 < x ≤ 0 the left side is huge while the right side stays below 5/4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, HPow.hPow, Nat, OfNat.ofNat, LE.le, LT.lt, Usa1985P2.f
Proof uses: Eq.mpr, HSub.hSub, HDiv.hDiv, id, congrArg, Usa1985P2.f_def, Neg.neg, Or, le_or_gt, lt_or_eq_of_le, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HMul.hMul, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr and 138 more
137 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
```
lemma f_pos_of_nonpos {N : ℝ} (hN : N = 10 ^ 10) {x : ℝ} (hx : x ≤ 0) :
    0 < f N x := by
…
```
Mentions: Usa1985P2.f
lemma Usa1985P2.f_lt_f_of_lt f N is strictly antitone on {x ≥ 0 | x² ≤ N + 1/2} line 85 source
Source documentation
f N is strictly antitone on {x ≥ 0 | x² ≤ N + 1/2}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, OfNat.ofNat, LT.lt, HPow.hPow, Nat, HAdd.hAdd, HDiv.hDiv, Usa1985P2.f
Proof uses: HSub.hSub, Iff.mpr, sub_pos, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, 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.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo and 111 more
133 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma f_lt_f_of_lt {N : ℝ} {x y : ℝ} (hx : 0 ≤ x) (hxy : x < y)
    (hy : y ^ 2 ≤ N + 1 / 2) : f N y < f N x := by
…
```
Mentions: Usa1985P2.f
lemma Usa1985P2.eq_of_region1 Hence there is at most one root in {x ≥ 0 | x² ≤ N + 1/2} line 98 source
Source documentation
Hence there is at most one root in {x ≥ 0 | x² ≤ N + 1/2}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, OfNat.ofNat, HPow.hPow, Nat, HAdd.hAdd, HDiv.hDiv, Eq, Usa1985P2.f
Proof uses: LT.lt, Or, lt_trichotomy, absurd, Usa1985P2.f_lt_f_of_lt, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr and 35 more
82 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma eq_of_region1 {N : ℝ} {x y : ℝ}
    (hx0 : 0 ≤ x) (hx2 : x ^ 2 ≤ N + 1 / 2) (hfx : f N x = 0)
    (hy0 : 0 ≤ y) (hy2 : y ^ 2 ≤ N + 1 / 2) (hfy : f N y = 0) : x = y := by
…
```
Mentions: Usa1985P2.f
lemma Usa1985P2.region2_key Two roots x < y lying in {x² ≥ C} would force (y + x) * ((y² - C) + (x² - C)) = 1 line 108 source
Source documentation
Two roots x < y lying in {x² ≥ C} would force (y + x) * ((y² - C) + (x² - C)) = 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, Eq, HPow.hPow, Nat, HSub.hSub, OfNat.ofNat, HAdd.hAdd, HDiv.hDiv, HMul.hMul
Proof uses: Iff.mpr, sub_pos, Trans.trans, rfl, Eq.mpr, id, congrArg, mul_assoc, Eq.refl, sq_sub_sq, sub_sub_sub_cancel_right, mul_comm, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, NNRat.rawCast and 55 more
125 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma region2_key {x y : ℝ} (hxy : x < y) (C : ℝ)
    (e1 : (x ^ 2 - C) ^ 2 = x + 5 / 4) (e2 : (y ^ 2 - C) ^ 2 = y + 5 / 4) :
    (y + x) * ((y ^ 2 - C) + (x ^ 2 - C)) = 1 := by
…
```
lemma Usa1985P2.region2_aux But for N = 10^10 two roots in {x² ≥ N + 1/2} are impossible: the left side of the identity above exceeds 2 * 10^5 * 316 line 121 source
Source documentation
But for N = 10^10 two roots in {x² ≥ N + 1/2} are impossible: the left side of the identity above exceeds 2 * 10^5 * 316.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, HPow.hPow, Nat, OfNat.ofNat, LE.le, HAdd.hAdd, HDiv.hDiv, Usa1985P2.f, LT.lt, False
Proof uses: HSub.hSub, Mathlib.Tactic.Ring.of_eq, Rat.rawCast, Int.negOfNat, HMul.hMul, Nat.rawCast, Mathlib.Tactic.Ring.Common.sub_congr, NNRat.rawCast, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Ring.Common.pow_add, Mathlib.Tactic.Ring.Common.single_pow and 133 more
125 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
```
lemma region2_aux {N : ℝ} (hN : N = 10 ^ 10) {x y : ℝ}
    (hx0 : 0 ≤ x) (hx2 : N + 1 / 2 ≤ x ^ 2) (hfx : f N x = 0)
    (hxy : x < y) (hy2 : N + 1 / 2 ≤ y ^ 2) (hfy : f N y = 0) : False := by
…
```
Mentions: Usa1985P2.f
lemma Usa1985P2.eq_of_region2 At most one root in {x ≥ 0 | x² ≥ N + 1/2} line 159 source
Source documentation
At most one root in {x ≥ 0 | x² ≥ N + 1/2}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, HPow.hPow, Nat, OfNat.ofNat, LE.le, HAdd.hAdd, HDiv.hDiv, Usa1985P2.f
Proof uses: LT.lt, Or, lt_trichotomy, False.elim, Usa1985P2.region2_aux
43 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma eq_of_region2 {N : ℝ} (hN : N = 10 ^ 10) {x y : ℝ}
    (hx0 : 0 ≤ x) (hx2 : N + 1 / 2 ≤ x ^ 2) (hfx : f N x = 0)
    (hy0 : 0 ≤ y) (hy2 : N + 1 / 2 ≤ y ^ 2) (hfy : f N y = 0) : x = y := by
…
```
Mentions: Usa1985P2.f
determine Usa1985P2.answer The two real roots, correct to 4 decimal places line 170 source
Source documentation
The two real roots, correct to 4 decimal places.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Real
Proof uses: Prod.mk, OfScientific.ofScientific, Bool.true
2 instances, coercions and auxiliary constants left out.
```
determine answer : ℝ × ℝ := (99999.9984, 100000.0016)
```
problem Usa1985P2.usa1985_p2 line 172 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, HPow.hPow, Nat, OfNat.ofNat, Exists, And, LT.lt, Iff, HSub.hSub, HAdd.hAdd, HMul.hMul, Or, abs, Prod.fst, Usa1985P2.answer, OfScientific.ofScientific, Bool.true, Prod.snd
Proof uses: Usa1985P2.f, Eq.mpr, HDiv.hDiv, id, congrArg, Usa1985P2.f_def, Mathlib.Meta.NormNum.isNNRat_lt_true, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Meta.NormNum.IsRat.to_isNNRat, Mathlib.Meta.NormNum.isRat_sub, Int.ofNat, Eq.refl, Mathlib.Meta.NormNum.IsNNRat.to_isRat, Mathlib.Meta.NormNum.isRat_pow, Int.negOfNat, Mathlib.Meta.NormNum.isNNRat_pow, Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true, Mathlib.Meta.NormNum.isNNRat_nnratCast and 142 more
159 instances, coercions and auxiliary constants left out.

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