`Compfiles/Usa1972P4.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 1972, Problem 4

Let k be the real cube root of 2. Find integers A, B, C, a, b, c such that

|(Ax² + Bx + C)/(ax² + bx + c) − k| < |x − k|

for all non-negative rational numbers x.

Imports (10)

Imported by 1 file

Compfiles.lean

abbrev Usa1972P4.IsSolution Documented declaration: IsSolution line 40 source
Source documentation
The property that the integers A, B, C, a, b, c solve the problem for the real cube root k of 2: the rational function (Ax² + Bx + C)/(ax² + bx + c) approximates k strictly better than x does, for every non-negative rational number x.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Real
Proof uses: Rat, LE.le, OfNat.ofNat, LT.lt, abs, HSub.hSub, HDiv.hDiv, HAdd.hAdd, HMul.hMul, HPow.hPow, Nat
23 instances, coercions and auxiliary constants left out.
```
abbrev IsSolution (A B C a b c : ℤ) (k : ℝ) : Prop :=
…
```
lemma Usa1972P4.rat_cube_ne_two There is no rational number whose cube equals 2 line 62 source
Source documentation
There is no rational number whose cube equals 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Rat, Ne, HPow.hPow, Nat, OfNat.ofNat
Proof uses: Eq, Rat.den, cast, Not, Eq.symm, Eq.trans, congrArg, Nat.cast_zero, Rat.den_nz, Int, Rat.num, HMul.hMul, congr, Nat.cast_mul, Nat.cast_pow, Int.cast_mul, Int.cast_ofNat, Int.cast_pow, congrFun', Int.cast_natCast and 111 more
146 instances, coercions and auxiliary constants left out.

Tactic trace: 47 steps
Open to load the checked before-and-after goal states.
```
lemma rat_cube_ne_two (q : ℚ) : q ^ 3 ≠ 2 := by
…
```
lemma Usa1972P4.ratCast_ne_of_cube_eq_two A rational number is never equal to the real cube root of 2 line 105 source
Source documentation
A rational number is never equal to the real cube root of 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, HPow.hPow, Nat, OfNat.ofNat, Rat, Ne
Proof uses: False, Eq.mpr, id, congrFun', congrArg, Rat.cast_pow, Usa1972P4.rat_cube_ne_two, cast, Eq.trans, Eq.symm, Rat.cast_ofNat
42 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma ratCast_ne_of_cube_eq_two {k : ℝ} (hk : k ^ 3 = 2) (q : ℚ) : (q : ℝ) ≠ k := by
…
```
lemma Usa1972P4.cube_eq_two_factor The key factorization, using k³ = 2: (2x² + 2x + 2) − (x² + 2x + 2)k = (x − k)((2 − k)x + 2 − k²) line 114 source
Source documentation
The key factorization, using k³ = 2: (2x² + 2x + 2) − (x² + 2x + 2)k = (x − k)((2 − k)x + 2 − k²).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, HPow.hPow, Nat, OfNat.ofNat, HSub.hSub, HAdd.hAdd, HMul.hMul
Proof uses: Mathlib.Tactic.LinearCombination.eq_of_eq, Eq.symm, Mathlib.Tactic.LinearCombination.eq_rearrange, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.sub_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl and 42 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma cube_eq_two_factor {k x : ℝ} (hk : k ^ 3 = 2) :
    2 * x ^ 2 + 2 * x + 2 - (x ^ 2 + 2 * x + 2) * k =
      (x - k) * ((2 - k) * x + 2 - k ^ 2) := by
…
```
lemma Usa1972P4.one_lt_of_cube_eq_two line 119 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, HPow.hPow, Nat, OfNat.ofNat, LT.lt
Proof uses: Odd, Exists.intro, HAdd.hAdd, HMul.hMul, rfl, Eq.mpr, id, congrArg, Eq.symm, propext, Odd.pow_lt_pow, one_pow, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.false
65 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa1972P4.lt_two_of_cube_eq_two line 124 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, HPow.hPow, Nat, OfNat.ofNat, LT.lt
Proof uses: Odd, Exists.intro, HAdd.hAdd, HMul.hMul, rfl, Eq.mpr, id, congrArg, Eq.symm, propext, Odd.pow_lt_pow, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.bit1, Bool, Bool.false
60 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa1972P4.sq_lt_two_of_cube_eq_two line 129 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, HPow.hPow, Nat, OfNat.ofNat, LT.lt
Proof uses: Usa1972P4.one_lt_of_cube_eq_two, LT.lt.trans, zero_lt_one, HMul.hMul, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, Nat.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, Mathlib.Tactic.Ring.Common.mul_pow_mul and 25 more
73 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Usa1972P4.main_inequality With (A, B, C, a, b, c) = (2, 2, 2, 1, 2, 2), the required inequality holds for every non-negative rational number x line 141 source
Source documentation
With (A, B, C, a, b, c) = (2, 2, 2, 1, 2, 2), the required inequality holds for every non-negative rational number x.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, HPow.hPow, Nat, OfNat.ofNat, Rat, LE.le, LT.lt, abs, HSub.hSub, HDiv.hDiv, HAdd.hAdd, HMul.hMul
Proof uses: LT.lt.trans, zero_lt_one, Usa1972P4.one_lt_of_cube_eq_two, Usa1972P4.lt_two_of_cube_eq_two, Usa1972P4.sq_lt_two_of_cube_eq_two, cast, Eq.trans, congrFun', congrArg, Eq.symm, Nat.cast_zero, sq_nonneg, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance and 85 more
150 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
lemma main_inequality {k : ℝ} (hk : k ^ 3 = 2) (x : ℚ) (hx : 0 ≤ x) :
    |(2 * (x : ℝ) ^ 2 + 2 * (x : ℝ) + 2) / ((x : ℝ) ^ 2 + 2 * (x : ℝ) + 2) - k| <
      |(x : ℝ) - k| := by
…
```
determine Usa1972P4.solution line 174 source
no axioms what this means
Statement uses: Prod, Int
Proof uses: Prod.mk, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
problem Usa1972P4.usa1972_p4 line 176 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, HPow.hPow, Nat, OfNat.ofNat, Usa1972P4.usa1972_p4.match_1, Prod, Int, Usa1972P4.solution, Usa1972P4.IsSolution
Proof uses: Rat, LE.le, Eq.mpr, LT.lt, abs, HSub.hSub, HDiv.hDiv, HAdd.hAdd, HMul.hMul, id, congrFun', congrArg, congr, Int.cast_ofNat, Eq.trans, Int.cast_one, one_mul, Usa1972P4.main_inequality
46 instances, coercions and auxiliary constants left out.

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