Compfiles/Usa2025P1.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

3 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2025, Problem 1

Fix positive integers k and d. Prove that for all sufficiently large odd positive integers n, the digits of the base-2n representation of n ^ k are all greater than d.

Imports (3)
Imported by 1 file
  1. lemma Usa2025P1.residue_mod For odd n and 1 ≤ ℓ ≤ k, the residue of n ^ k modulo (2 * n) ^ ℓ has the form c * n ^ ℓ for an odd c (so in particular 1 ≤ c) line 33 source

    Source documentation

    For odd n and 1 ≤ ℓ ≤ k, the residue of n ^ k modulo (2 * n) ^ ℓ has the form c * n ^ ℓ for an odd c (so in particular 1 ≤ c). In other words, the ℓ rightmost base-(2 * n) digits of n ^ k are the base-(2 * n) digits of c * n ^ ℓ.

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

    Statement uses: Nat, Odd, LE.le, OfNat.ofNat, Exists, And, Eq, HMod.hMod, HPow.hPow, HMul.hMul

    Proof uses: LT.lt, Odd.pos, HSub.hSub, Eq.mpr, id, congrArg, propext, Nat.odd_iff, Nat.mod_mod_of_dvd, dvd_pow_self, Iff.mp, Odd.pow, Exists.intro, And.intro, Dvd.dvd, mul_pow, mul_dvd_mul_right, Nat.dvd_sub_mod, Nat.sub_mul, HAdd.hAdd and 15 more

    45 instances, coercions and auxiliary constants left out.

    Tactic trace: 24 steps

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

    lemma residue_mod {n k ℓ : ℕ} (hodd : Odd n) (hℓ1 : 1 ≤ ℓ) (hℓk : ℓ ≤ k) :
    ∃ c : ℕ, Odd c ∧ 1 ≤ c ∧ n ^ k % (2 * n) ^ ℓ = c * n ^ ℓ := by
…
  2. lemma Usa2025P1.digit_of_mod The i-th base-b digit of m (counting from the right, starting at 0) equals E / b ^ i, where E = m % b ^ (i + 1) is the residue of m modulo the next power of b line 65 source

    Source documentation

    The i-th base-b digit of m (counting from the right, starting at 0) equals E / b ^ i, where E = m % b ^ (i + 1) is the residue of m modulo the next power of b.

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, HMod.hMod, HPow.hPow, HAdd.hAdd, HDiv.hDiv

    Proof uses: Eq.mpr, id, congrArg, Eq.symm, Nat.mod_lt, Nat.pow_pos, HMul.hMul, pow_succ, Eq.mp, Nat.div_add_mod, rfl, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf, Eq.refl, Mathlib.Tactic.Ring.Common.pow_add, Mathlib.Tactic.Ring.Common.single_pow and 21 more

    39 instances, coercions and auxiliary constants left out.

    Tactic trace: 19 steps

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

    lemma digit_of_mod {m b E i : ℕ} (hb : 1 < b) (hm : m % b ^ (i + 1) = E) :
    m / b ^ i % b = E / b ^ i := by
…
  3. problem Usa2025P1.usa2025_p1 line 88 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Exists, LE.le, Odd, Membership.mem, List, Nat.digits, HMul.hMul, HPow.hPow

    Proof uses: Exists.intro, HAdd.hAdd, HSub.hSub, Odd.pos, List.length, Eq, GetElem.getElem, Iff.mp, List.mem_iff_getElem, Eq.mpr, id, congrArg, propext, Nat.digits_length_le_iff, Nat.pow_lt_pow_left, HMod.hMod, HDiv.hDiv, List.getD, Nat.getD_digits, Eq.trans and 48 more

    66 instances, coercions and auxiliary constants left out.

    Tactic trace: 44 steps

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