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

32 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2006, Problem 3

For integral m, let p(m) be the greatest prime divisor of m. By convention, we set p(±1) = 1 and p(0) = ∞. Find all polynomials f with integer coefficients such that the sequence

{p(f(n²)) − 2n}, n = 0, 1, 2, ...

is bounded above. (In particular, this requires f(n²) ≠ 0 for n ≥ 0.)

Imports (8)

Imported by 1 file

Compfiles.lean

def Usa2006P3.gpd The greatest prime divisor of an integer m, with the convention gpd (±1) = 1 line 43 source
Source documentation
The greatest prime divisor of an integer m, with the convention gpd (±1) = 1. (The value at 0 is irrelevant for the problem, which requires f(n²) ≠ 0 anyway.)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Nat
Proof uses: WithBot.unbotD, OfNat.ofNat, Finset.max, Nat.primeFactors, Int.natAbs
2 instances, coercions and auxiliary constants left out.
```
noncomputable def gpd (m : ℤ) : ℕ := (m.natAbs.primeFactors.max).unbotD 1
```
def Usa2006P3.BddCond The condition that the sequence p(f(n²)) − 2n is bounded above (and defined for every n) line 47 source
Source documentation
The condition that the sequence p(f(n²)) − 2n is bounded above (and defined for every n).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Int
Proof uses: Exists, Nat, And, Ne, Polynomial.eval, HPow.hPow, OfNat.ofNat, LE.le, HSub.hSub, Usa2006P3.gpd, HMul.hMul
15 instances, coercions and auxiliary constants left out.
```
def BddCond (f : ℤ[X]) : Prop :=
…
```
Mentions: f
def Usa2006P3.Classification The classification: f is a nonzero constant times a (possibly empty) product of factors 4X − a² with a an odd integer line 53 source
Source documentation
The classification: f is a nonzero constant times a (possibly empty) product of factors 4X − a² with a an odd integer.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Int
Proof uses: Exists, List, And, Ne, OfNat.ofNat, Membership.mem, Odd, Eq, HMul.hMul, RingHom, Polynomial.C, List.prod, List.map, HSub.hSub, Polynomial.X, HPow.hPow, Nat
19 instances, coercions and auxiliary constants left out.
```
def Classification (f : ℤ[X]) : Prop :=
…
```
Mentions: f
def Usa2006P3.Pbound An auxiliary formulation of boundedness: every prime divisor of f(n²) is at most 2n + B line 59 source
Source documentation
An auxiliary formulation of boundedness: every prime divisor of f(n²) is at most 2n + B.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Int, Nat
Proof uses: And, Ne, Polynomial.eval, HPow.hPow, OfNat.ofNat, Nat.Prime, Dvd.dvd, LE.le, HAdd.hAdd, HMul.hMul
16 instances, coercions and auxiliary constants left out.
```
def Pbound (f : ℤ[X]) (B : ℕ) : Prop :=
…
```
Mentions: f
lemma Usa2006P3.gpd_eq_max' line 63 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Finset.Nonempty, Nat, Nat.primeFactors, Int.natAbs, Eq, Usa2006P3.gpd, Finset.max'
Proof uses: Eq.mpr, WithBot.unbotD, OfNat.ofNat, Finset.max, id, congrArg, Usa2006P3.gpd.eq_1, WithBot, Eq.symm, Finset.coe_max', WithBot.unbotD_coe, Eq.refl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2006P3.gpd_eq_one_of_not_nonempty line 67 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Not, Finset.Nonempty, Nat, Nat.primeFactors, Int.natAbs, Eq, Usa2006P3.gpd, OfNat.ofNat
Proof uses: Eq.mpr, WithBot.unbotD, Finset.max, id, congrArg, Usa2006P3.gpd.eq_1, EmptyCollection.emptyCollection, Finset, Eq.mp, propext, Finset.not_nonempty_iff_eq_empty, Bot.bot, WithBot, Finset.max_empty, WithBot.unbotD_bot, Eq.refl
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2006P3.bddCond_iff The two formulations of the boundedness condition agree line 73 source
Source documentation
The two formulations of the boundedness condition agree.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Int, Iff, Usa2006P3.BddCond, Exists, Nat, Usa2006P3.Pbound
Proof uses: Iff.intro, And, Ne, Polynomial.eval, HPow.hPow, OfNat.ofNat, LE.le, HSub.hSub, Usa2006P3.gpd, HMul.hMul, Exists.intro, Int.toNat, And.intro, Nat.Prime, Dvd.dvd, HAdd.hAdd, And.left, Membership.mem, Finset, Nat.primeFactors and 101 more
102 instances, coercions and auxiliary constants left out.

Tactic trace: 51 steps
Open to load the checked before-and-after goal states.
```
lemma bddCond_iff (f : ℤ[X]) : BddCond f ↔ ∃ B, Pbound f B := by
…
```
Mentions: f, Usa2006P3.BddCond, Usa2006P3.Pbound
lemma Usa2006P3.natAbs_list_prod line 121 source
standard axioms: Classical.choice, propext what this means
Statement uses: List, Int, Eq, Nat, Int.natAbs, List.prod, List.map
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, OfNat.ofNat, True, congr, congrArg, Int.natAbs_of_isUnit, IsUnit, List.map_nil, eq_self, List.cons, HMul.hMul, Int.natAbs_mul, List.map_cons
22 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2006P3.prime_dvd_list_prod line 127 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, List, Dvd.dvd, List.prod, Exists, And, Membership.mem
Proof uses: List.rec, List.nil, absurd, Eq, OfNat.ofNat, Iff.mp, Nat.dvd_one, Nat.Prime.ne_one, List.cons, Or, HMul.hMul, Nat.Prime.dvd_mul, Eq.mp, congrArg, List.prod_cons, Exists.intro, And.intro, List.mem_cons_self, List.exists_mem_cons_of_exists
11 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Usa2006P3.eval_factor line 139 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Eq, Polynomial.eval, HSub.hSub, Polynomial, HMul.hMul, RingHom, Polynomial.C, OfNat.ofNat, Polynomial.X, HPow.hPow, Nat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, congr, eq_intCast, Int.cast_ofNat, Int.cast_pow, Polynomial.eval_sub, Polynomial.eval_mul, Polynomial.eval_ofNat, Polynomial.eval_X, Polynomial.eval_pow, Polynomial.eval_intCast, eq_self
63 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2006P3.eval_prod_factors line 143 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Int, Eq, Polynomial.eval, List.prod, Polynomial, List.map, HSub.hSub, HMul.hMul, RingHom, Polynomial.C, OfNat.ofNat, Polynomial.X, HPow.hPow, Nat
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, True, congr, congrArg, congrFun', funext, eq_intCast, Int.cast_ofNat, Int.cast_pow, List.map_nil, Polynomial.eval_one, eq_self, Eq.mpr, List.cons, id, List.map_cons, List.prod_cons and 3 more
67 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2006P3.factor_eq line 152 source
standard axioms: Quot.sound, propext what this means
Statement uses: Int, Eq, HSub.hSub, HMul.hMul, OfNat.ofNat, HPow.hPow, Nat, HAdd.hAdd
Proof uses: Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm, Mathlib.Tactic.Ring.Common.pow_add, Mathlib.Tactic.Ring.Common.single_pow and 35 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2006P3.odd_ne_even line 154 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Odd, Even, False
Proof uses: Eq, HAdd.hAdd, HMul.hMul, OfNat.ofNat
19 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2006P3.odd_sq_sub_four_mul_ne_zero line 159 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Odd, Ne, HSub.hSub, HMul.hMul, OfNat.ofNat, HPow.hPow, Nat
Proof uses: Eq, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, Nat.rawCast, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 66 more
84 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Usa2006P3.pbound_of_classification The easy direction: every polynomial of the classified form satisfies the boundedness condition line 170 source
Source documentation
The easy direction: every polynomial of the classified form satisfies the boundedness condition.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Int, Usa2006P3.Classification, Exists, Nat, Usa2006P3.Pbound
Proof uses: List, And, Ne, OfNat.ofNat, Membership.mem, Odd, Eq, HMul.hMul, RingHom, Polynomial.C, List.prod, List.map, HSub.hSub, Polynomial.X, HPow.hPow, Exists.intro, HAdd.hAdd, Int.natAbs, Finset.sum, List.toFinset and 98 more
112 instances, coercions and auxiliary constants left out.

Tactic trace: 59 steps
Open to load the checked before-and-after goal states.
```
lemma pbound_of_classification (f : ℤ[X]) (h : Classification f) :
    ∃ B, Pbound f B := by
…
```
Mentions: f, h, Usa2006P3.Classification, Usa2006P3.Pbound
lemma Usa2006P3.schur Schur's theorem: a nonconstant polynomial with integer coefficients takes some value divisible by a prime outside any given finite set of primes line 226 source
Source documentation
Schur's theorem: a nonconstant polynomial with integer coefficients takes some value divisible by a prime outside any given finite set of primes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Int, Ne, Nat, Polynomial.natDegree, OfNat.ofNat, Finset, Membership.mem, Nat.Prime, Exists, And, Not, Dvd.dvd, Polynomial.eval
Proof uses: dite, Eq, Finsupp, Polynomial.coeff, Eq.mpr, id, congrArg, Polynomial.coeff_zero_eq_eval_zero, HMul.hMul, Polynomial.X, Iff.mpr, Polynomial.X_dvd_iff, LE.le, HAdd.hAdd, Finset.sup, Nat.exists_infinite_primes, Exists.intro, And.intro, Finset.le_sup, of_eq_true and 139 more
167 instances, coercions and auxiliary constants left out.

Tactic trace: 140 steps
Open to load the checked before-and-after goal states.
```
lemma schur (h : ℤ[X]) (hd : h.natDegree ≠ 0) (s : Finset ℕ) (hs : ∀ q ∈ s, q.Prime) :
    ∃ q : ℕ, q.Prime ∧ q ∉ s ∧ ∃ m : ℕ, (q : ℤ) ∣ h.eval (m : ℤ) := by
…
```
Mentions: h
def Usa2006P3.Fs The integer-valued function Fs f t = 4^d · f(t²/4), where d = f.natDegree; the powers of 4 clear the denominators line 371 source
Source documentation
The integer-valued function Fs f t = 4^d · f(t²/4), where d = f.natDegree; the powers of 4 clear the denominators.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Int
Proof uses: Finset.sum, Nat, Finset.range, HAdd.hAdd, Polynomial.natDegree, OfNat.ofNat, HMul.hMul, HPow.hPow, HSub.hSub, Finsupp, Polynomial.coeff
20 instances, coercions and auxiliary constants left out.
```
def Fs (f : ℤ[X]) (t : ℤ) : ℤ :=
…
```
Mentions: f
lemma Usa2006P3.Fs_two_mul line 374 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Int, Eq, Usa2006P3.Fs, HMul.hMul, OfNat.ofNat, HPow.hPow, Nat, Polynomial.natDegree, Polynomial.eval
Proof uses: Eq.mpr, Finset.sum, Finset.range, HAdd.hAdd, HSub.hSub, Finsupp, Polynomial.coeff, id, congrArg, Usa2006P3.Fs.eq_1, Polynomial.eval_eq_sum_range, Finset.mul_sum, Finset.sum_congr, rfl, Finset, Membership.mem, LE.le, Nat.le_of_lt_succ, Eq.mp, LT.lt and 44 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Usa2006P3.Fs_neg line 391 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Int, Eq, Usa2006P3.Fs, Neg.neg
Proof uses: id, Finset.sum_congr, Nat, Finset.range, HAdd.hAdd, Polynomial.natDegree, OfNat.ofNat, HMul.hMul, HPow.hPow, HSub.hSub, Finsupp, Polynomial.coeff, rfl, Finset, Membership.mem, Eq.mpr, congrArg, Even.neg_pow, Exists.intro, two_mul and 1 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2006P3.intModEq_sum line 397 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, Finset, Int, Membership.mem, Int.ModEq, Finset.sum
Proof uses: Finset.induction, EmptyCollection.emptyCollection, Int.ModEq.refl, Not, Insert.insert, Eq.mpr, HAdd.hAdd, id, Eq, congrArg, Finset.sum_insert, Int.ModEq.add, Finset.mem_insert_self, Finset.mem_insert_of_mem
13 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2006P3.Fs_modEq line 407 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Int, Int.ModEq, Usa2006P3.Fs
Proof uses: Usa2006P3.intModEq_sum, Nat, Finset.range, HAdd.hAdd, Polynomial.natDegree, OfNat.ofNat, HMul.hMul, HPow.hPow, HSub.hSub, Finsupp, Polynomial.coeff, Membership.mem, Finset, Int.ModEq.mul, Int.ModEq.refl, Int.ModEq.pow
22 instances, coercions and auxiliary constants left out.
lemma Usa2006P3.Fs_cast line 411 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Int, Eq, Rat, HMul.hMul, HPow.hPow, Nat, OfNat.ofNat, Polynomial.natDegree, Polynomial.eval, HDiv.hDiv, Polynomial.map, Int.castRingHom, Usa2006P3.Fs
Proof uses: Eq.mpr, Finset.sum, Finset.range, Nat.succ, Finsupp, Polynomial.coeff, id, congrArg, Polynomial.eval_eq_sum_range', lt_of_le_of_lt, Polynomial.natDegree_map_le, Nat.lt_succ_self, Finset.mul_sum, HAdd.hAdd, HSub.hSub, Usa2006P3.Fs.eq_1, Int.cast_sum, Finset.sum_congr, rfl, Finset and 93 more
128 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma Usa2006P3.eval_modEq line 432 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Int, Int.ModEq, Polynomial.eval
Proof uses: Polynomial.induction_on, Eq.mpr, RingHom, Polynomial.C, id, Eq, congr, congrArg, Polynomial.eval_C, Int.ModEq.refl, HAdd.hAdd, Polynomial.eval_add, Int.ModEq.add, Nat, HMul.hMul, HPow.hPow, Polynomial.X, OfNat.ofNat, Eq.trans, Polynomial.eval_mul and 6 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Usa2006P3.exists_root_of_pbound If f is nonconstant and satisfies the prime bound, then f has a root of the form (2k+1)²/4 over ℚ line 447 source
Source documentation
If f is nonconstant and satisfies the prime bound, then f has a root of the form (2k+1)²/4 over ℚ. This is the heart of the proof: a large prime q dividing f(n²) forces q = 2n + 2k + 1 with k ≤ B, and then q divides Fs f (2k+1); since there are infinitely many such primes but only finitely many possible k, some Fs f (2k+1) vanishes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Int, Ne, Nat, Polynomial.natDegree, OfNat.ofNat, Usa2006P3.Pbound, Exists, Eq, Rat, Polynomial.eval, HDiv.hDiv, HPow.hPow, HAdd.hAdd, HMul.hMul, Polynomial.map, Int.castRingHom
Proof uses: Classical.byContradiction, Not, Usa2006P3.Fs, Usa2006P3.Fs_cast, Or, False, Eq.mp, congrArg, propext, mul_eq_zero, Int.cast_zero, absurd, pow_ne_zero, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Int.cast_natCast, Finset.prod and 132 more
195 instances, coercions and auxiliary constants left out.

Tactic trace: 115 steps
Open to load the checked before-and-after goal states.
```
lemma exists_root_of_pbound (f : ℤ[X]) (hd : f.natDegree ≠ 0) (B : ℕ) (hB : Pbound f B) :
    ∃ k : ℕ, (f.map (Int.castRingHom ℚ)).eval (((2 * k + 1 : ℕ) : ℚ) ^ 2 / 4) = 0 := by
…
```
Mentions: f, Usa2006P3.Pbound
lemma Usa2006P3.coeff_factor_one line 558 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Eq, Finsupp, Nat, Polynomial.coeff, HSub.hSub, Polynomial, HMul.hMul, RingHom, Polynomial.C, OfNat.ofNat, Polynomial.X, HPow.hPow
Proof uses: Eq.mpr, id, congrArg, Polynomial.coeff_sub, Polynomial.coeff_C_mul, Polynomial.coeff_X_one, HAdd.hAdd, Polynomial.coeff_C_succ, mul_one, sub_zero, Eq.refl
64 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2006P3.coeff_factor_zero line 561 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Eq, Finsupp, Nat, Polynomial.coeff, HSub.hSub, Polynomial, HMul.hMul, RingHom, Polynomial.C, OfNat.ofNat, Polynomial.X, HPow.hPow, Neg.neg
Proof uses: Eq.mpr, id, congrArg, Polynomial.coeff_sub, Polynomial.coeff_C_mul, Polynomial.coeff_X_zero, Polynomial.coeff_C_zero, MulZeroClass.mul_zero, zero_sub, Eq.refl
55 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2006P3.isPrimitive_factor 4X − a² with a odd is a primitive polynomial over ℤ line 565 source
Source documentation
4X − a² with a odd is a primitive polynomial over ℤ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Odd, Polynomial.IsPrimitive, HSub.hSub, Polynomial, HMul.hMul, RingHom, Polynomial.C, OfNat.ofNat, Polynomial.X, HPow.hPow, Nat
Proof uses: Eq.mpr, Dvd.dvd, IsUnit, id, Eq, congrArg, propext, Polynomial.isPrimitive_iff_isUnit_of_C_dvd, Finsupp, Polynomial.coeff, Eq.mp, Polynomial.C_dvd_iff_dvd_coeff, Usa2006P3.coeff_factor_one, Neg.neg, Usa2006P3.coeff_factor_zero, Int.natAbs, Iff.mpr, Int.natAbs_dvd_natAbs, of_decide_eq_true, Bool and 17 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma isPrimitive_factor {a : ℤ} (ha : Odd a) : (C 4 * X - C (a ^ 2)).IsPrimitive := by
…
```
lemma Usa2006P3.factor_dvd_of_root If f has the root (2k+1)²/4 over ℚ, then 4X − (2k+1)² divides f over ℤ (Gauss's lemma) line 590 source
Source documentation
If f has the root (2k+1)²/4 over ℚ, then 4X − (2k+1)² divides f over ℤ (Gauss's lemma).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Int, Nat, Eq, Rat, Polynomial.eval, HDiv.hDiv, HPow.hPow, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Polynomial.map, Int.castRingHom, Dvd.dvd, HSub.hSub, RingHom, Polynomial.C, Polynomial.X
Proof uses: Eq.mpr, id, congrArg, rfl, Odd, Exists.intro, congrFun', Eq.trans, Nat.cast_add, congr, Nat.cast_mul, Nat.cast_one, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, 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.Tactic.Ring.Common.atom_pf and 78 more
165 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
```
lemma factor_dvd_of_root (f : ℤ[X]) {k : ℕ}
    (hroot : (f.map (Int.castRingHom ℚ)).eval (((2 * k + 1 : ℕ) : ℚ) ^ 2 / 4) = 0) :
    (C 4 * X - C (((2 * k + 1 : ℕ) : ℤ) ^ 2)) ∣ f := by
…
```
Mentions: f
lemma Usa2006P3.pbound_of_mul_factor The cofactor of a 4X − a² factor still satisfies the prime bound line 621 source
Source documentation
The cofactor of a 4X − a² factor still satisfies the prime bound.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Int, Nat, Eq, HMul.hMul, HSub.hSub, RingHom, Polynomial.C, OfNat.ofNat, Polynomial.X, HPow.hPow, Usa2006P3.Pbound
Proof uses: Ne, Polynomial.eval, And.left, Nat.Prime, Dvd.dvd, LE.le, HAdd.hAdd, And.intro, right_ne_zero_of_mul, Eq.mp, congrArg, Polynomial.eval_mul, And.right, Eq.mpr, id, dvd_trans, dvd_mul_left
46 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma pbound_of_mul_factor {f f₁ : ℤ[X]} {a : ℤ} (B : ℕ)
    (hf : f = (C 4 * X - C (a ^ 2)) * f₁) (hB : Pbound f B) : Pbound f₁ B := by
…
```
Mentions: f, Usa2006P3.Pbound
lemma Usa2006P3.classification_of_pbound Documented declaration: classification_of_pbound line 633 source
Source documentation
The classification theorem, proved by strong induction on the degree: a nonconstant f satisfying the bound has a root (2k+1)²/4, hence a factor 4X − (2k+1)², and the cofactor has smaller degree.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Polynomial, Int, Eq, Polynomial.natDegree, Exists, Usa2006P3.Pbound, Usa2006P3.Classification
Proof uses: Nat.strong_induction_on, LT.lt, dite, OfNat.ofNat, RingHom, Polynomial.C, Finsupp, Polynomial.coeff, Polynomial.eq_C_of_natDegree_eq_zero, Eq.trans, Ne, Polynomial.eval, HPow.hPow, And.left, Nat.Prime, Dvd.dvd, LE.le, HAdd.hAdd, HMul.hMul, id and 105 more
115 instances, coercions and auxiliary constants left out.

Tactic trace: 66 steps
Open to load the checked before-and-after goal states.
```
lemma classification_of_pbound : ∀ d : ℕ, ∀ f : ℤ[X], f.natDegree = d →
    (∃ B, Pbound f B) → Classification f := by
…
```
Mentions: f, Usa2006P3.Pbound, Usa2006P3.Classification
lemma Usa2006P3.classification_iff_pbound The full classification, in the prime-bound formulation line 685 source
Source documentation
The full classification, in the prime-bound formulation.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Int, Iff, Exists, Nat, Usa2006P3.Pbound, Usa2006P3.Classification
Proof uses: Iff.intro, Usa2006P3.classification_of_pbound, Polynomial.natDegree, rfl, Usa2006P3.pbound_of_classification
2 instances, coercions and auxiliary constants left out.
```
lemma classification_iff_pbound (f : ℤ[X]) :
    (∃ B, Pbound f B) ↔ Classification f :=
…
```
Mentions: f, Usa2006P3.Pbound, Usa2006P3.Classification
problem Usa2006P3.usa2006_p3 line 691 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Polynomial, Int, Iff, Usa2006P3.BddCond, Usa2006P3.Classification
Proof uses: Eq.mpr, Exists, Nat, Usa2006P3.Pbound, id, Eq, congrArg, propext, Usa2006P3.bddCond_iff, Usa2006P3.classification_iff_pbound
2 instances, coercions and auxiliary constants left out.

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