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

30 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2006, Problem 5

A mathematical frog jumps along the number line. The frog starts at 1, and jumps according to the following rule: if the frog is at integer n, then it can jump either to n + 1 or to n + 2 ^ (mₙ + 1), where 2 ^ mₙ is the largest power of 2 that is a factor of n. Show that if k ≥ 2 is a positive integer and i is a nonnegative integer, then the minimum number of jumps needed to reach 2 ^ i * k is greater than the minimum number of jumps needed to reach 2 ^ i.

Imports (14)

Imported by 1 file

Compfiles.lean

def Usa2006P5.nu The exponent of the largest power of 2 dividing the integer x (the 2-adic valuation of x) line 44 source
Source documentation
The exponent of the largest power of 2 dividing the integer x (the 2-adic valuation of x).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Nat
Proof uses: Finsupp, Nat.factorization, Int.natAbs, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
```
noncomputable def nu (x : ℤ) : ℕ := x.natAbs.factorization 2
```
def Usa2006P5.ValidPath Documented declaration: ValidPath line 49 source
Source documentation
ValidPath x ss holds when the list ss of jump lengths can legally be performed by the frog starting at position x: each jump has length 1 or length 2 ^ (ν₂ n + 1), where n is the position the frog jumps from.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, List, Nat
2 instances, coercions and auxiliary constants left out.
```
def ValidPath : ℤ → List ℕ → Prop
  | _, [] => True
  | x, s :: ss => (s = 1 ∨ s = 2 ^ (nu x + 1)) ∧ ValidPath (x + (s : ℤ)) ss

/-- The frog can reach position `m` in exactly `j` jumps starting from `1`. -/
```
Mentions: Usa2006P5.nu
def Usa2006P5.Reachable The frog can reach position m in exactly j jumps starting from 1 line 54 source
Source documentation
The frog can reach position m in exactly j jumps starting from 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Nat
Proof uses: Exists, List, And, Usa2006P5.ValidPath, OfNat.ofNat, Eq, HAdd.hAdd, List.sum, List.length
8 instances, coercions and auxiliary constants left out.
```
def Reachable (m : ℤ) (j : ℕ) : Prop :=
…
```
def Usa2006P5.minJumps The minimum number of jumps the frog needs to reach position m line 58 source
Source documentation
The minimum number of jumps the frog needs to reach position m.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Nat
Proof uses: InfSet.sInf, Set.ofPred, Usa2006P5.Reachable
1 instances, coercions and auxiliary constants left out.
```
noncomputable def minJumps (m : ℤ) : ℕ := sInf { j | Reachable m j }
…
```
Mentions: Usa2006P5.Reachable
def Usa2006P5.BigBound BigBound m c x ss holds when every jump of ss (performed starting from position x) that ends at a position greater than c has length at most 2 ^ m line 65 source
Source documentation
BigBound m c x ss holds when every jump of ss (performed starting from position x) that ends at a position greater than c has length at most 2 ^ m.

standard axioms: propext what this means
Statement uses: Nat, Int, List
2 instances, coercions and auxiliary constants left out.
```
def BigBound (m : ℕ) (c : ℤ) : ℤ → List ℕ → Prop
  | _, [] => True
  | x, s :: ss => (c < x + (s : ℤ) → s ≤ 2 ^ m) ∧ BigBound m c (x + (s : ℤ)) ss

/-- `filt e c y ss` processes the list of jumps `ss` starting at position `y`,
deleting every jump whose length is divisible by `2 ^ (e + 1)` and which lands
at a position greater than `c`.  This is the deletion operation of the
official solution: deleting such jumps keeps the path valid. -/
```
Mentions: Usa2006P5.filt, solution
def Usa2006P5.filt Documented declaration: filt line 73 source
Source documentation
filt e c y ss processes the list of jumps ss starting at position y, deleting every jump whose length is divisible by 2 ^ (e + 1) and which lands at a position greater than c. This is the deletion operation of the official solution: deleting such jumps keeps the path valid.

standard axioms: propext what this means
Statement uses: Nat, Int, List
2 instances, coercions and auxiliary constants left out.
```
def filt (e : ℕ) (c : ℤ) : ℤ → List ℕ → List ℕ
  | _, [] => []
  | y, s :: ss =>
    if (2 : ℤ) ^ (e + 1) ∣ (s : ℤ) ∧ c < y + (s : ℤ) then filt e c y ss
    else s :: filt e c (y + (s : ℤ)) ss
```
lemma Usa2006P5.natAbs_two_pow line 79 source
standard axioms: propext what this means
Statement uses: Nat, Eq, Int.natAbs, HPow.hPow, Int, OfNat.ofNat
Proof uses: Eq.mpr, id, congrArg, Int.natAbs_pow, of_eq_true, Eq.trans, True, congrFun', Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_natAbs_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, eq_self, eq_true, True.intro
21 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2006P5.two_pow_nu_dvd line 83 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Dvd.dvd, HPow.hPow, Nat, OfNat.ofNat, Usa2006P5.nu
Proof uses: Eq.mpr, Int.natAbs, id, Eq, congrArg, Eq.symm, propext, Int.natAbs_dvd_natAbs, Usa2006P5.natAbs_two_pow, Nat.ordProj_dvd
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2006P5.not_two_pow_succ_nu_dvd line 87 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Ne, OfNat.ofNat, Not, Dvd.dvd, HPow.hPow, Nat, HAdd.hAdd, Usa2006P5.nu
Proof uses: Eq.mpr, Int.natAbs, id, Eq, congrArg, Eq.symm, propext, Int.natAbs_dvd_natAbs, Usa2006P5.natAbs_two_pow, Nat.pow_succ_factorization_not_dvd, Iff.mpr, Int.natAbs_ne_zero, Nat.prime_two
20 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2006P5.nu_eq_of The 2-adic valuation is characterized by divisibility line 92 source
Source documentation
The 2-adic valuation is characterized by divisibility.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Nat, Ne, OfNat.ofNat, Dvd.dvd, HPow.hPow, Not, HAdd.hAdd, Eq, Usa2006P5.nu
Proof uses: LT.lt, Or, lt_trichotomy, False.elim, dvd_trans, pow_dvd_pow, Usa2006P5.two_pow_nu_dvd, Eq.symm, Usa2006P5.not_two_pow_succ_nu_dvd
26 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma nu_eq_of {x : ℤ} {a : ℕ} (hx : x ≠ 0) (h1 : (2 : ℤ) ^ a ∣ x)
    (h2 : ¬ (2 : ℤ) ^ (a + 1) ∣ x) : nu x = a := by
…
```
Mentions: Usa2006P5.nu
lemma Usa2006P5.nu_congr Shifting by a multiple of 2 ^ e does not change the 2-adic valuation, as long as the valuation is smaller than e line 104 source
Source documentation
Shifting by a multiple of 2 ^ e does not change the 2-adic valuation, as long as the valuation is smaller than e.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Nat, Ne, OfNat.ofNat, Dvd.dvd, HPow.hPow, HSub.hSub, LT.lt, Usa2006P5.nu, Eq
Proof uses: Usa2006P5.nu_eq_of, dvd_trans, pow_dvd_pow, Usa2006P5.two_pow_nu_dvd, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, HMul.hMul, Nat.rawCast, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.sub_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat and 26 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma nu_congr {y y' : ℤ} {e : ℕ} (hy : y ≠ 0) (hy' : y' ≠ 0)
    (hd : (2 : ℤ) ^ e ∣ y - y') (hlt : nu y < e) : nu y' = nu y := by
…
```
Mentions: Usa2006P5.nu
lemma Usa2006P5.validPath_cons line 121 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Nat, List, Iff, Usa2006P5.ValidPath, List.cons, And, Or, Eq, OfNat.ofNat, HPow.hPow, HAdd.hAdd, Usa2006P5.nu
Proof uses: Iff.rfl
10 instances, coercions and auxiliary constants left out.
lemma Usa2006P5.ValidPath.append line 125 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, List, Nat, Iff, Usa2006P5.ValidPath, HAppend.hAppend, And, HAdd.hAdd, List.sum
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, True, congrArg, congrFun', OfNat.ofNat, CharP.cast_eq_zero, add_zero, true_and, iff_self, Eq.mpr, List.cons, id, Eq, List.cons_append, Or, HPow.hPow, Usa2006P5.nu and 19 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Usa2006P5.ValidPath.pow_two Every jump of a valid path is a power of two line 142 source
Source documentation
Every jump of a valid path is a power of two.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, List, Nat, Usa2006P5.ValidPath, Membership.mem, Exists, Eq, HPow.hPow, OfNat.ofNat
Proof uses: List.rec, List.nil, False.elim, Eq.mp, False, List.cons, Or, HAdd.hAdd, Usa2006P5.nu, And, Iff.mp, Usa2006P5.validPath_cons, List.mem_cons, Exists.intro, rfl, Eq.symm
21 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma ValidPath.pow_two {x : ℤ} {ss : List ℕ} (h : ValidPath x ss) :
    ∀ s ∈ ss, ∃ t, s = 2 ^ t := by
…
```
Mentions: h, Usa2006P5.ValidPath
lemma Usa2006P5.ValidPath.one_le_of_mem line 155 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, List, Nat, Usa2006P5.ValidPath, Membership.mem, LE.le, OfNat.ofNat
Proof uses: Eq, HPow.hPow, Exists, Usa2006P5.ValidPath.pow_two, Nat.one_le_two_pow, Eq.symm
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2006P5.bigBound_cons line 160 source
standard axioms: propext what this means
Statement uses: Nat, Int, List, Iff, Usa2006P5.BigBound, List.cons, And, LT.lt, HAdd.hAdd, LE.le, HPow.hPow, OfNat.ofNat
Proof uses: Iff.rfl
11 instances, coercions and auxiliary constants left out.
lemma Usa2006P5.bigBound_of_forall line 164 source
standard axioms: propext what this means
Statement uses: Nat, Int, List, Membership.mem, LE.le, HPow.hPow, OfNat.ofNat, Usa2006P5.BigBound
Proof uses: List.rec, List.nil, True.intro, List.cons, Eq.mpr, And, LT.lt, HAdd.hAdd, id, Eq, congrArg, propext, Usa2006P5.bigBound_cons, And.intro, List.mem_cons_self, List.mem_cons_of_mem
19 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2006P5.eq_two_pow_of Documented declaration: eq_two_pow_of line 175 source
Source documentation
A jump that is deleted by filt (divisible by 2 ^ (e + 1) and landing beyond c) must have length exactly 2 ^ (e + 1), because all jumps landing beyond c have length at most 2 ^ (e + 1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, LE.le, OfNat.ofNat, Dvd.dvd, HPow.hPow, HAdd.hAdd, LT.lt, Eq
Proof uses: lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, HSub.hSub, 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.neg_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.neg_add, Mathlib.Meta.NormNum.IsInt.to_raw_eq and 35 more
88 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma eq_two_pow_of {e : ℕ} {c y y' : ℤ} {s : ℕ}
    (hs1 : 1 ≤ s) (hdvd : (2 : ℤ) ^ (e + 1) ∣ (s : ℤ)) (hc : c < y' + (s : ℤ))
    (hyy' : y' ≤ y) (hbb1 : c < y + (s : ℤ) → s ≤ 2 ^ (e + 1)) :
    s = 2 ^ (e + 1) := by
…
```
lemma Usa2006P5.filt_cons_delete line 187 source
standard axioms: propext what this means
Statement uses: Nat, Int, List, Dvd.dvd, HPow.hPow, OfNat.ofNat, HAdd.hAdd, LT.lt, Eq, Usa2006P5.filt, List.cons
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, ite_eq_left_of_eq_true, And, congr, eq_true, and_self, eq_self
29 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2006P5.filt_cons_keep line 192 source
standard axioms: propext what this means
Statement uses: Nat, Int, List, Not, And, Dvd.dvd, HPow.hPow, OfNat.ofNat, HAdd.hAdd, LT.lt, Eq, Usa2006P5.filt, List.cons
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, ite_eq_right_of_eq_false, eq_false, eq_self
29 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2006P5.filt_valid The key validity lemma: after deleting jumps divisible by 2 ^ (e + 1) that land beyond c, the remaining path is still valid line 202 source
Source documentation
The key validity lemma: after deleting jumps divisible by 2 ^ (e + 1) that land beyond c, the remaining path is still valid. The hypothesis hor says that either no jump has been deleted so far (so the two positions coincide), or the current filtered position is within 2 ^ (e + 1) beyond which no deletion can have occurred yet.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, List, Usa2006P5.ValidPath, LE.le, OfNat.ofNat, Dvd.dvd, HPow.hPow, HAdd.hAdd, HSub.hSub, Or, Eq, LT.lt, Usa2006P5.BigBound, Usa2006P5.filt
Proof uses: List.rec, List.nil, True.intro, List.cons, Usa2006P5.nu, And, Iff.mp, Usa2006P5.validPath_cons, Usa2006P5.bigBound_cons, Eq.mpr, id, congrArg, Nat.one_le_two_pow, Nat.cast_nonneg, dite, Usa2006P5.filt_cons_delete, And.left, And.right, Usa2006P5.eq_two_pow_of, le_of_not_gt and 90 more
113 instances, coercions and auxiliary constants left out.

Tactic trace: 83 steps
Open to load the checked before-and-after goal states.
```
lemma filt_valid {e : ℕ} {c y y' : ℤ} {ss : List ℕ}
    (hv : ValidPath y ss) (hy : 1 ≤ y) (hy' : 1 ≤ y') (hyy' : y' ≤ y)
    (hdvd : (2 : ℤ) ^ (e + 1) ∣ y - y')
    (hor : y = y' ∨ c < y' + 2 ^ (e + 1))
    (hbb : BigBound (e + 1) c y ss) :
    ValidPath y' (filt e c y' ss) := by
…
```
Mentions: Usa2006P5.ValidPath, Usa2006P5.BigBound, Usa2006P5.filt
lemma Usa2006P5.filt_count Counting lemma: the total length deleted by filt is a multiple of 2 ^ (e + 1), and the number of deleted jumps equals that multiple line 264 source
Source documentation
Counting lemma: the total length deleted by filt is a multiple of 2 ^ (e + 1), and the number of deleted jumps equals that multiple.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, List, Membership.mem, Exists, Eq, HPow.hPow, OfNat.ofNat, LE.le, Usa2006P5.BigBound, HAdd.hAdd, And, HSub.hSub, List.sum, Usa2006P5.filt, HMul.hMul, List.length
Proof uses: List.rec, List.nil, Exists.intro, of_eq_true, Eq.trans, True, congr, congrArg, CharP.cast_eq_zero, sub_self, congrFun', MulZeroClass.zero_mul, eq_self, add_zero, and_self, List.cons, LT.lt, Iff.mp, Usa2006P5.bigBound_cons, List.mem_cons_self and 91 more
117 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
```
lemma filt_count {e : ℕ} {c y y' : ℤ} {ss : List ℕ}
    (hp2 : ∀ s ∈ ss, ∃ t, s = 2 ^ t) (hyy' : y' ≤ y) (hbb : BigBound (e + 1) c y ss) :
    ∃ r : ℕ, ((ss.sum : ℤ) - ((filt e c y' ss).sum : ℤ)) = (r : ℤ) * 2 ^ (e + 1) ∧
      ss.length = (filt e c y' ss).length + r := by
…
```
Mentions: Usa2006P5.BigBound, Usa2006P5.filt
lemma Usa2006P5.filt_lower Documented declaration: filt_lower line 298 source
Source documentation
Lower bound lemma: if filt deletes at least one jump, then the last deleted jump starts at a position p' whose 2-adic valuation is exactly e, which lands beyond c, and which is at most the final endpoint.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, List, Usa2006P5.ValidPath, LE.le, OfNat.ofNat, Dvd.dvd, HPow.hPow, HAdd.hAdd, HSub.hSub, Usa2006P5.BigBound, LT.lt, List.length, Usa2006P5.filt, Exists, And, Eq, Usa2006P5.nu, List.sum
Proof uses: List.rec, List.nil, False.elim, Eq.mp, False, List.cons, Or, Iff.mp, Usa2006P5.validPath_cons, Usa2006P5.bigBound_cons, Eq.mpr, id, congrArg, Nat.one_le_two_pow, dite, Usa2006P5.filt_cons_delete, And.left, And.right, Usa2006P5.eq_two_pow_of, le_of_not_gt and 77 more
124 instances, coercions and auxiliary constants left out.

Tactic trace: 68 steps
Open to load the checked before-and-after goal states.
```
lemma filt_lower {e : ℕ} {c y y' : ℤ} {ss : List ℕ}
    (hv : ValidPath y ss) (hy : 1 ≤ y) (hy' : 1 ≤ y') (hyy' : y' ≤ y)
    (hdvd : (2 : ℤ) ^ (e + 1) ∣ y - y') (hbb : BigBound (e + 1) c y ss)
    (hlen : (filt e c y' ss).length < ss.length) :
    ∃ p' : ℤ, 1 ≤ p' ∧ nu p' = e ∧ c < p' + 2 ^ (e + 1) ∧
      p' ≤ y' + ((filt e c y' ss).sum : ℤ) := by
…
```
Mentions: Usa2006P5.ValidPath, Usa2006P5.BigBound, Usa2006P5.filt, Usa2006P5.nu
lemma Usa2006P5.filt_bigbound Transfer lemma: after filt has removed the jumps of length 2 ^ (e + 1), every remaining jump landing beyond c has length at most 2 ^ e line 356 source
Source documentation
Transfer lemma: after filt has removed the jumps of length 2 ^ (e + 1), every remaining jump landing beyond c has length at most 2 ^ e.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, List, Membership.mem, Exists, Eq, HPow.hPow, OfNat.ofNat, LE.le, Usa2006P5.BigBound, HAdd.hAdd, Usa2006P5.filt
Proof uses: List.rec, List.nil, True.intro, List.cons, LT.lt, And, Iff.mp, Usa2006P5.bigBound_cons, dite, Dvd.dvd, Eq.mpr, id, congrArg, Usa2006P5.filt_cons_delete, And.left, And.right, List.mem_cons_of_mem, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp and 58 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
lemma filt_bigbound {e : ℕ} {c y y' : ℤ} {ss : List ℕ}
    (hp2 : ∀ s ∈ ss, ∃ t, s = 2 ^ t) (hyy' : y' ≤ y) (hbb : BigBound (e + 1) c y ss) :
    BigBound e c y' (filt e c y' ss) := by
…
```
Mentions: Usa2006P5.BigBound, Usa2006P5.filt
lemma Usa2006P5.base_prefix Base case of the main induction: if every jump landing beyond 2 ^ i has length 1, then some prefix of the path ends exactly at 2 ^ i line 385 source
Source documentation
Base case of the main induction: if every jump landing beyond 2 ^ i has length 1, then some prefix of the path ends exactly at 2 ^ i.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Nat, List, LE.le, OfNat.ofNat, HPow.hPow, Usa2006P5.ValidPath, Usa2006P5.BigBound, HAdd.hAdd, List.sum, Exists, And, List.IsPrefix, Eq
Proof uses: List.rec, List.nil, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, HMul.hMul, Nat.rawCast, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.cast_pos and 79 more
109 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
```
lemma base_prefix {x : ℤ} {i : ℕ} {ss : List ℕ} (hx1 : 1 ≤ x) (hx2 : x ≤ (2 : ℤ) ^ i)
    (hv : ValidPath x ss) (hbb : BigBound 0 ((2 : ℤ) ^ i) x ss)
    (hge : (2 : ℤ) ^ i ≤ x + (ss.sum : ℤ)) :
    ∃ ss' : List ℕ, ss' <+: ss ∧ x + (ss'.sum : ℤ) = (2 : ℤ) ^ i := by
…
```
Mentions: Usa2006P5.ValidPath, Usa2006P5.BigBound
lemma Usa2006P5.key_lemma The main induction line 425 source
Source documentation
The main induction. From a valid path whose endpoint is at least 2 ^ i and divisible by 2 ^ min i e, where every jump landing beyond 2 ^ i has length at most 2 ^ e, we can extract a valid path to 2 ^ i of at most the same length, and strictly shorter if the original endpoint exceeds 2 ^ i.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List, Usa2006P5.ValidPath, OfNat.ofNat, Int, Usa2006P5.BigBound, HPow.hPow, Dvd.dvd, Min.min, HAdd.hAdd, List.sum, LE.le, Exists, And, Eq, List.length, LT.lt
Proof uses: Nat.recAux, List.IsPrefix, Usa2006P5.base_prefix, le_rfl, pow_pos, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, Nat.rawCast and 122 more
191 instances, coercions and auxiliary constants left out.

Tactic trace: 149 steps
Open to load the checked before-and-after goal states.
```
lemma key_lemma (i : ℕ) (e : ℕ) (ss : List ℕ)
    (hv : ValidPath 1 ss) (hbb : BigBound e ((2 : ℤ) ^ i) 1 ss)
    (hdiv : (2 : ℤ) ^ min i e ∣ (1 : ℤ) + (ss.sum : ℤ))
    (hge : (2 : ℤ) ^ i ≤ (1 : ℤ) + (ss.sum : ℤ)) :
    ∃ ss' : List ℕ, ValidPath 1 ss' ∧ (1 : ℤ) + (ss'.sum : ℤ) = (2 : ℤ) ^ i ∧
      ss'.length ≤ ss.length ∧ ((2 : ℤ) ^ i < (1 : ℤ) + (ss.sum : ℤ) → ss'.length < ss.length) := by
…
```
Mentions: Usa2006P5.ValidPath, Usa2006P5.BigBound
lemma Usa2006P5.validPath_replicate_one line 559 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Nat, Usa2006P5.ValidPath, List.replicate, OfNat.ofNat
Proof uses: Nat.recAux, True.intro, Eq.mpr, HAdd.hAdd, List.cons, id, Eq, congrArg, List, List.replicate_succ, And, Or, HPow.hPow, Usa2006P5.nu, propext, Usa2006P5.validPath_cons, And.intro, Or.inl, rfl
12 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2006P5.reachable_all_ones Every position m ≥ 1 is reachable, by jumping +1 every time line 567 source
Source documentation
Every position m ≥ 1 is reachable, by jumping +1 every time.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, LE.le, OfNat.ofNat, Usa2006P5.Reachable, Int.toNat, HSub.hSub
Proof uses: Exists.intro, List, Nat, And, Usa2006P5.ValidPath, Eq, HAdd.hAdd, List.sum, List.length, List.replicate, And.intro, Usa2006P5.validPath_replicate_one, Eq.mpr, HSMul.hSMul, id, congrArg, List.sum_replicate, HMul.hMul, smul_eq_mul, mul_one and 48 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma reachable_all_ones {m : ℤ} (hm : 1 ≤ m) : Reachable m (m - 1).toNat := by
…
```
Mentions: Usa2006P5.Reachable
lemma Usa2006P5.minJumps_mem line 574 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, LE.le, OfNat.ofNat, Membership.mem, Nat, Set, Set.ofPred, Usa2006P5.Reachable, Usa2006P5.minJumps
Proof uses: Nat.sInf_mem, Exists.intro, Int.toNat, HSub.hSub, Usa2006P5.reachable_all_ones
8 instances, coercions and auxiliary constants left out.
problem Usa2006P5.usa2006_p5 line 579 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, GT.gt, Usa2006P5.minJumps, HMul.hMul, Int, HPow.hPow
Proof uses: cast, Eq.symm, LT.lt, pow_pos, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast and 89 more
144 instances, coercions and auxiliary constants left out.

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