Compfiles/Usa1999P3.lean

GitHub source file

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

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 1999, Problem 3

Let p > 2 be a prime and let a, b, c, d be integers not divisible by p, such that

{ra/p} + {rb/p} + {rc/p} + {rd/p} = 2

for any integer r not divisible by p. (Here, {t} = t − ⌊t⌋ is the fractional part.) Prove that at least two of the numbers a + b, a + c, a + d, b + c, b + d, c + d are divisible by p.

Imports (4)
Imported by 1 file
  1. def Usa1999P3.rt The primitive p-th root of unity used throughout the proof line 60 source

    Source documentation

    The primitive p-th root of unity used throughout the proof.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Complex

    Proof uses: Complex.exp, HDiv.hDiv, HMul.hMul, OfNat.ofNat, Real.pi, Complex.I

    10 instances, coercions and auxiliary constants left out.

    def rt (p : ℕ) : ℂ := Complex.exp (2 * Real.pi * Complex.I / p)
  2. def Usa1999P3.chi The additive character ZMod p → ℂ given by j ↦ ζ ^ j.val line 63 source

    Source documentation

    The additive character ZMod p → ℂ given by j ↦ ζ ^ j.val.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, ZMod, Complex

    Proof uses: HPow.hPow, Usa1999P3.rt, ZMod.val

    5 instances, coercions and auxiliary constants left out.

    def chi (p : ℕ) (j : ZMod p) : ℂ := rt p ^ j.val

    Mentions: Usa1999P3.rt

  3. def Usa1999P3.Sw The weighted character sum ∑ k, k.val * χ (j * k) line 66 source

    Source documentation

    The weighted character sum ∑ k, k.val * χ (j * k).

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, NeZero, ZMod, Complex

    Proof uses: Finset.sum, Finset.univ, HMul.hMul, ZMod.val, Usa1999P3.chi

    15 instances, coercions and auxiliary constants left out.

    def Sw (p : ℕ) [NeZero p] (j : ZMod p) : ℂ := ∑ k : ZMod p, (k.val : ℂ) * chi p (j * k)

    Mentions: Usa1999P3.chi

  4. lemma Usa1999P3.isPrimitiveRoot_rt line 68 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Nat.Prime, IsPrimitiveRoot, Complex, Usa1999P3.rt

    Proof uses: id, Complex.isPrimitiveRoot_exp, LT.lt.ne', OfNat.ofNat, Nat.Prime.pos

    6 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

  5. lemma Usa1999P3.chi_zero line 72 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Eq, Complex, Usa1999P3.chi, OfNat.ofNat, ZMod

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HPow.hPow, Usa1999P3.rt, ZMod.val, ZMod.val_zero, pow_zero, eq_self

    25 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  6. lemma Usa1999P3.chi_add line 75 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Nat.Prime, ZMod, Eq, Complex, Usa1999P3.chi, HAdd.hAdd, HMul.hMul

    Proof uses: NeZero, NeZero.mk, LT.lt.ne', OfNat.ofNat, Nat.Prime.pos, HPow.hPow, Usa1999P3.rt, IsPrimitiveRoot.pow_eq_one, Usa1999P3.isPrimitiveRoot_rt, LT.lt, ZMod.val, ZMod.val_lt, id, Eq.mpr, HMod.hMod, congrArg, ZMod.val_add, LE.le, Or, lt_or_ge and 11 more

    51 instances, coercions and auxiliary constants left out.

    Tactic trace: 23 steps

    Open to load the checked before-and-after goal states.

  7. lemma Usa1999P3.chi_eq_one_iff line 97 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Nat.Prime, ZMod, Iff, Eq, Complex, Usa1999P3.chi, OfNat.ofNat

    Proof uses: NeZero, NeZero.mk, LT.lt.ne', Nat.Prime.pos, IsPrimitiveRoot, Usa1999P3.rt, Usa1999P3.isPrimitiveRoot_rt, Iff.intro, Dvd.dvd, ZMod.val, Iff.mp, HPow.hPow, IsPrimitiveRoot.pow_eq_one_iff_dvd, Nat.eq_zero_of_dvd_of_lt, ZMod.val_lt, ZMod.val_eq_zero, Usa1999P3.chi_zero, Eq.symm

    30 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

    Open to load the checked before-and-after goal states.

  8. lemma Usa1999P3.sum_zmod_val Sums over ZMod p of a function of the residue can be written as sums over Finset.range p line 110 source

    Source documentation

    Sums over ZMod p of a function of the residue can be written as sums over Finset.range p.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, NeZero, Complex, Eq, Finset.sum, ZMod, Finset.univ, ZMod.val, Finset.range

    Proof uses: Finset.sum_bij, Membership.mem, Finset, Iff.mpr, LT.lt, Finset.mem_range, ZMod.val_lt, ZMod.natCast_zmod_val, Eq.mpr, id, congrArg, Eq.symm, Eq.refl, Iff.mp, Exists.intro, Exists, Finset.mem_univ, ZMod.val_natCast_of_lt

    17 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

    Open to load the checked before-and-after goal states.

    lemma sum_zmod_val {p : ℕ} [NeZero p] (f : ℕ → ℂ) :
    ∑ j : ZMod p, f (j.val) = ∑ i ∈ Finset.range p, f i := by
…

    Mentions: f

  9. lemma Usa1999P3.sum_chi_self line 125 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, NeZero, Nat.Prime, LT.lt, OfNat.ofNat, Eq, Complex, Finset.sum, ZMod, Finset.univ, Usa1999P3.chi

    Proof uses: IsPrimitiveRoot, Usa1999P3.rt, Usa1999P3.isPrimitiveRoot_rt, id, Eq.mpr, HPow.hPow, ZMod.val, Finset.range, congrArg, Usa1999P3.sum_zmod_val, IsPrimitiveRoot.geom_sum_eq_zero

    28 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

    Open to load the checked before-and-after goal states.

  10. lemma Usa1999P3.sum_chi line 132 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, NeZero, Nat.Prime, LT.lt, OfNat.ofNat, ZMod, Eq, Complex, Finset.sum, Finset.univ, Usa1999P3.chi, HMul.hMul, ite

    Proof uses: Fact, Fact.mk, dite, Eq.mpr, id, congrArg, ite_eq_left, rfl, Finset.sum_congr, Finset, Membership.mem, MulZeroClass.zero_mul, Usa1999P3.chi_zero, HSMul.hSMul, Finset.card, Finset.sum_const, Fintype.card, Finset.card_univ, ZMod.card, nsmul_eq_mul and 10 more

    69 instances, coercions and auxiliary constants left out.

    Tactic trace: 21 steps

    Open to load the checked before-and-after goal states.

  11. lemma Usa1999P3.Sw_mul_sub_one The key identity (χ j - 1) * Sw j = p for nonzero j, obtained by reindexing the sum defining Sw along k ↦ k + 1 line 156 source

    Source documentation

    The key identity (χ j - 1) * Sw j = p for nonzero j, obtained by reindexing the sum defining Sw along k ↦ k + 1.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, NeZero, Nat.Prime, LT.lt, OfNat.ofNat, ZMod, Ne, Eq, Complex, HMul.hMul, HSub.hSub, Usa1999P3.chi, Usa1999P3.Sw

    Proof uses: Finset.sum, Finset.univ, ZMod.val, id, Eq.mpr, congrArg, Finset.mul_sum, HAdd.hAdd, Finset.sum_congr, rfl, Finset, Membership.mem, Trans.trans, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, Eq.symm, Eq.refl and 87 more

    111 instances, coercions and auxiliary constants left out.

    Tactic trace: 80 steps

    Open to load the checked before-and-after goal states.

    lemma Sw_mul_sub_one {p : ℕ} [NeZero p] (hp : p.Prime) (hp2 : 2 < p) {j : ZMod p} (hj : j ≠ 0) :
    (chi p j - 1) * Sw p j = (p : ℂ) := by
…

    Mentions: Usa1999P3.chi, Usa1999P3.Sw

  12. lemma Usa1999P3.alg_symm The symmetric-polynomial identity obtained by clearing denominators in ∑ 1 / (xᵢ - 1) = -2 line 243 source

    Source documentation

    The symmetric-polynomial identity obtained by clearing denominators in ∑ 1 / (xᵢ - 1) = -2.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Complex, Ne, OfNat.ofNat, Eq, HAdd.hAdd, HDiv.hDiv, HSub.hSub, Neg.neg, Nat, HMul.hMul

    Proof uses: Iff.mpr, sub_ne_zero, Mathlib.Tactic.LinearCombination.eq_of_eq, inferInstance, CommGroupWithZero, Eq.symm, Eq.mp, Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq, Mathlib.Tactic.FieldSimp.NF.eval, Mathlib.Tactic.FieldSimp.NF.cons, Prod.mk, Int, List.nil, Prod, Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul, rfl, Eq.trans, Mathlib.Tactic.FieldSimp.subst_add, congr_arg₂, Mathlib.Tactic.FieldSimp.NF.div_eq_eval and 76 more

    101 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

    Open to load the checked before-and-after goal states.

    lemma alg_symm {x₁ x₂ x₃ x₄ : ℂ} (h₁ : x₁ ≠ 1) (h₂ : x₂ ≠ 1) (h₃ : x₃ ≠ 1) (h₄ : x₄ ≠ 1)
    (h : 1 / (x₁ - 1) + 1 / (x₂ - 1) + 1 / (x₃ - 1) + 1 / (x₄ - 1) = -2) :
    2 + (x₁ * x₂ * x₃ + x₁ * x₂ * x₄ + x₁ * x₃ * x₄ + x₂ * x₃ * x₄)
      = x₁ + x₂ + x₃ + x₄ + 2 * (x₁ * x₂ * x₃ * x₄) := by
…

    Mentions: h

  13. problem Usa1999P3.usa1999_p3 line 258 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Nat.Prime, LT.lt, OfNat.ofNat, Int, Not, Dvd.dvd, Eq, Real, HAdd.hAdd, Int.fract, HDiv.hDiv, HMul.hMul, Or, And

    Proof uses: NeZero, NeZero.mk, LT.lt.ne', Nat.Prime.pos, Fact, Fact.mk, ZMod, rfl, Ne, Iff.mpr, Iff.not, ZMod.intCast_zmod_eq_zero_iff_dvd, ZMod.val, Eq.mpr, id, congrArg, Int.cast_natCast, ZMod.natCast_zmod_val, Eq.symm, propext and 159 more

    228 instances, coercions and auxiliary constants left out.

    Tactic trace: 389 steps (first 200 of 389)

    Open to load the checked before-and-after goal states.