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

25 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1995, Problem 1

Let p be an odd prime. The sequence (aₙ) n ≥ 0 is defined as follows: a₀ = 0, a₁ = 1, ..., a_{p-2} = p - 2, and for all n ≥ p - 1, aₙ is the least integer greater than a_{n-1} such that a₀, a₁, ..., aₙ does not contain an arithmetic progression of length p.

Prove that, for all n, aₙ is the number obtained by writing n in base p - 1 and reading the result in base p.

Imports (4)

Imported by 1 file

Compfiles.lean

def Usa1995P1.HasAp Documented declaration: HasAp line 38 source
Source documentation
HasAp a p n m means that the first n + 1 terms a 0, a 1, …, a (n-1), m (where the candidate m is the n-th term) contain an arithmetic progression of length p: there are strictly increasing indices v 0 < v 1 < … < v (p-1), all at most n, whose values form an arithmetic progression. The last conjunct splits the value condition according to whether the index is the final position n (where the candidate m sits) or not.

standard axioms: propext what this means
Statement uses: Nat
Proof uses: Exists, Fin, And, StrictMono, LE.le, LT.lt, Eq, HAdd.hAdd, HMul.hMul
10 instances, coercions and auxiliary constants left out.
```
def HasAp (a : ℕ → ℕ) (p n m : ℕ) : Prop :=
…
```
def Usa1995P1.DigitFree A natural number is (p)-digit-free if no digit of its base-p expansion equals p - 1 line 47 source
Source documentation
A natural number is (p)-digit-free if no digit of its base-p expansion equals p - 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Membership.mem, List, Nat.digits, Ne, HSub.hSub, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
```
def DigitFree (p m : ℕ) : Prop := ∀ d ∈ Nat.digits p m, d ≠ p - 1
```
def Usa1995P1.bSeq bSeq p n is the number obtained by writing n in base p - 1 and reading the result in base p line 51 source
Source documentation
bSeq p n is the number obtained by writing n in base p - 1 and reading the result in base p.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Nat.ofDigits, Nat.digits, HSub.hSub, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
```
def bSeq (p n : ℕ) : ℕ := Nat.ofDigits p (Nat.digits (p - 1) n)
```
def Usa1995P1.phi phi p m reads the base-p digits of m in base p - 1 line 55 source
Source documentation
phi p m reads the base-p digits of m in base p - 1. On digit-free numbers it is the inverse of bSeq p.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Nat.ofDigits, HSub.hSub, OfNat.ofNat, Nat.digits
4 instances, coercions and auxiliary constants left out.
```
def phi (p m : ℕ) : ℕ := Nat.ofDigits (p - 1) (Nat.digits p m)
```
lemma Usa1995P1.phi_def line 57 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa1995P1.phi, Nat.ofDigits, HSub.hSub, OfNat.ofNat, Nat.digits
Proof uses: rfl
4 instances, coercions and auxiliary constants left out.
lemma Usa1995P1.bSeq_def line 59 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa1995P1.bSeq, Nat.ofDigits, Nat.digits, HSub.hSub, OfNat.ofNat
Proof uses: rfl
4 instances, coercions and auxiliary constants left out.
lemma Usa1995P1.ofDigits_cons_nat line 61 source
standard axioms: propext what this means
Statement uses: Nat, List, Eq, Nat.ofDigits, List.cons, HAdd.hAdd, HMul.hMul
Proof uses: of_eq_true, eq_self
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa1995P1.ofDigits_eq_zero_iff line 65 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Ne, OfNat.ofNat, List, Iff, Eq, Nat.ofDigits, Membership.mem
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, True, congr, congrArg, eq_self, forall_congr, False, implies_congr, Eq.refl, implies_true, iff_self, Eq.mpr, List.cons, HAdd.hAdd, HMul.hMul, id, Usa1995P1.ofDigits_cons_nat and 7 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Usa1995P1.phi_pos line 79 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, Usa1995P1.phi
Proof uses: Eq.mpr, Ne, id, Eq, congrArg, propext, Nat.pos_iff_ne_zero, Eq.mp, Membership.mem, List, Nat.digits, Iff.mp, Nat.ofDigits, HSub.hSub, Usa1995P1.ofDigits_eq_zero_iff, Iff.mpr, Nat.ofDigits_digits
12 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Usa1995P1.digits_ofDigits_ne If every entry of l is < b and different from c, then every base-b digit of Nat.ofDigits b l is different from c line 91 source
Source documentation
If every entry of l is < b and different from c, then every base-b digit of Nat.ofDigits b l is different from c.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, List, Membership.mem, Ne, Nat.digits, Nat.ofDigits
Proof uses: List.rec, List.nil, absurd, Eq.mp, congrArg, Nat.digits_zero, Nat.ofDigits_nil, of_eq_true, Not, Eq.trans, False, True, not_false_eq_true, List.cons, Eq, GT.gt, Or, Nat.eq_zero_or_pos, List.mem_cons_self, HMod.hMod and 16 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
lemma digits_ofDigits_ne {b c : ℕ} (hb : 1 < b) :
    ∀ {l : List ℕ}, (∀ d ∈ l, d < b) → (∀ d ∈ l, d ≠ c) →
      ∀ d ∈ Nat.digits b (Nat.ofDigits b l), d ≠ c := by
…
```
lemma Usa1995P1.digits_getD The k-th digit of m in base b (with 0 padding) line 121 source
Source documentation
The k-th digit of m in base b (with 0 padding).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, List.getD, Nat.digits, HMod.hMod, HDiv.hDiv, HPow.hPow
Proof uses: Nat.recAux, GT.gt, Or, Nat.eq_zero_or_pos, of_eq_true, Eq.trans, True, congr, congrArg, Option.getD, GetElem?.getElem?, List, List.length, List.nil, Option.none, congrFun', Nat.digits_zero, List.getD_eq_getElem?_getD, Option, getElem?_neg and 19 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma digits_getD {b : ℕ} (hb : 1 < b) (m k : ℕ) :
    (Nat.digits b m).getD k 0 = m / b ^ k % b := by
…
```
lemma Usa1995P1.mem_digits_of_getD_ne_zero line 134 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, List.getD, Nat.digits, OfNat.ofNat, Ne, Membership.mem, List
Proof uses: LT.lt, List.length, Decidable.byContradiction, Not, LE.le, Nat.le_of_not_lt, Eq.symm, Eq.mp, congrArg, List.getD_eq_default, Eq.mpr, GetElem.getElem, id, List.getD_eq_getElem, List.getElem_mem
8 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Usa1995P1.digit_add_mul_eq Adding a multiple of d = e * p^(k+1) + c * p^k only affects the k-th base-p digit through c (no carries into that digit from below) line 147 source
Source documentation
Adding a multiple of d = e * p^(k+1) + c * p^k only affects the k-th base-p digit through c (no carries into that digit from below).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, HAdd.hAdd, HMul.hMul, HPow.hPow, HMod.hMod, HDiv.hDiv
Proof uses: pow_pos, pow_succ', rfl, Eq.mpr, id, congrArg, Eq.rec, Nat.mod_lt, Eq.symm, Nat.div_add_mod, Eq.mp, pow_succ, Nat.div_div_eq_div_mul, mul_comm, Eq.refl, 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 and 30 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
```
lemma digit_add_mul_eq {p : ℕ} (hp : 1 < p) {x d k c e : ℕ} (i : ℕ)
    (hd : d = e * p ^ (k + 1) + c * p ^ k) :
    (x + i * d) / p ^ k % p = (x / p ^ k % p + i * c) % p := by
…
```
lemma Usa1995P1.ofDigits_map_add_mul line 185 source
standard axioms: propext what this means
Statement uses: Nat, List, Eq, Nat.ofDigits, List.map, HAdd.hAdd, HMul.hMul
Proof uses: List.rec, of_eq_true, List.nil, Eq.trans, OfNat.ofNat, True, congr, congrArg, List.map_nil, MulZeroClass.mul_zero, add_zero, eq_self, Eq.mpr, List.cons, id, List.map_cons, Usa1995P1.ofDigits_cons_nat, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast and 19 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa1995P1.phi_strictMono_on_digitFree The key monotonicity fact: phi is strictly increasing on digit-free numbers line 198 source
Source documentation
The key monotonicity fact: phi is strictly increasing on digit-free numbers. Proved by strong induction on the smaller number, comparing the least significant base-p digits.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Usa1995P1.DigitFree, LT.lt, Usa1995P1.phi
Proof uses: Nat.strong_induction_on, Eq, GT.gt, Or, Nat.eq_zero_or_pos, of_eq_true, Eq.trans, True, congrFun', congrArg, List, Nat.digits, List.nil, Nat.ofDigits, HSub.hSub, Nat.digits_zero, eq_self, Eq.mpr, id, Usa1995P1.phi_pos and 28 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 49 steps
Open to load the checked before-and-after goal states.
```
lemma phi_strictMono_on_digitFree {p : ℕ} (hp : 2 ≤ p) (x : ℕ) :
    ∀ y, DigitFree p x → DigitFree p y → x < y → phi p x < phi p y := by
…
```
Mentions: Usa1995P1.DigitFree, Usa1995P1.phi
lemma Usa1995P1.digits_bSeq The base-p digits of bSeq p n are exactly the base-(p-1) digits of n line 242 source
Source documentation
The base-p digits of bSeq p n are exactly the base-(p-1) digits of n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, List, Nat.digits, Usa1995P1.bSeq, HSub.hSub
Proof uses: Eq.mpr, Nat.ofDigits, id, congrArg, Usa1995P1.bSeq_def, Nat.digits_ofDigits, Membership.mem, LT.lt.trans, Nat.digits_lt_base, Ne, List.nil, Or, List.getLast, eq_or_ne, False.elim, Eq.mp, Nat.digits_zero, rfl, Eq.symm, Nat.getLast_digit_ne_zero
16 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma digits_bSeq {p : ℕ} (hp : 3 ≤ p) (n : ℕ) :
    Nat.digits p (bSeq p n) = Nat.digits (p - 1) n := by
…
```
Mentions: Usa1995P1.bSeq
lemma Usa1995P1.phi_bSeq line 254 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Usa1995P1.phi, Usa1995P1.bSeq
Proof uses: Eq.mpr, Nat.ofDigits, HSub.hSub, Nat.digits, id, congrArg, Usa1995P1.phi_def, List, Usa1995P1.digits_bSeq, Nat.ofDigits_digits, Eq.refl
7 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa1995P1.digitFree_bSeq line 257 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Usa1995P1.DigitFree, Usa1995P1.bSeq
Proof uses: Membership.mem, List, Nat.digits, LT.lt, HSub.hSub, Nat.digits_lt_base, Eq.mp, congrArg, Usa1995P1.digits_bSeq
10 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa1995P1.bSeq_phi line 263 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Usa1995P1.DigitFree, Eq, Usa1995P1.bSeq, Usa1995P1.phi
Proof uses: Eq.mpr, Nat.ofDigits, Nat.digits, HSub.hSub, id, congrArg, Usa1995P1.bSeq_def, Usa1995P1.phi_def, List, Nat.digits_ofDigits, Membership.mem, LT.lt, Nat.digits_lt_base, Ne, List.nil, Or, List.getLast, eq_or_ne, False.elim, Eq.mp and 6 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Usa1995P1.bSeq_strictMono line 277 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, StrictMono, Usa1995P1.bSeq
Proof uses: LT.lt, Or, Eq, lt_trichotomy, Usa1995P1.phi, congrArg, absurd, Eq.mp, Usa1995P1.phi_bSeq, ne_of_lt, Usa1995P1.phi_strictMono_on_digitFree, Usa1995P1.digitFree_bSeq
14 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Usa1995P1.bSeq_eq_self_of_lt line 289 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, HSub.hSub, Eq, Usa1995P1.bSeq
Proof uses: Eq.mpr, Nat.ofDigits, Nat.digits, id, congrArg, Usa1995P1.bSeq_def, GT.gt, Or, Nat.eq_zero_or_pos, List.nil, List, Nat.digits_zero, Nat.ofDigits_nil, Eq.refl, Eq.symm, List.cons, Nat.digits_of_lt, HAdd.hAdd, HMul.hMul, Nat.ofDigits_cons and 7 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Usa1995P1.exists_mem_digits_pred The non-existence part: among the values bSeq p i there is no arithmetic progression of length p line 301 source
Source documentation
The non-existence part: among the values bSeq p i there is no arithmetic progression of length p. If x, x + d, …, x + (p-1) d are all digit-free and d > 0, then looking at the least significant nonzero base-p digit of d, the k-th digits of the progression terms run through all residues mod p, so one of them equals p - 1: contradiction.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, LT.lt, OfNat.ofNat, Exists, And, Membership.mem, List, Nat.digits, HAdd.hAdd, HMul.hMul, HSub.hSub
Proof uses: Nat.Prime.one_lt, Fact, Fact.mk, NeZero, NeZero.mk, padicValNat, Eq, rfl, Dvd.dvd, HPow.hPow, pow_padicValNat_dvd, Not, pow_succ_padicValNat_not_dvd, False, Exists.intro, Eq.mpr, id, congrArg, pow_succ', Mathlib.Tactic.Ring.of_eq and 53 more
88 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
```
lemma exists_mem_digits_pred {p : ℕ} (hp : p.Prime) {x d : ℕ} (hd : 0 < d) :
    ∃ i < p, p - 1 ∈ Nat.digits p (x + i * d) := by
…
```
lemma Usa1995P1.not_hasAp If all candidate values are digit-free (here: values of bSeq p), there is no arithmetic progression of length p line 345 source
Source documentation
If all candidate values are digit-free (here: values of bSeq p), there is no arithmetic progression of length p.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, LE.le, OfNat.ofNat, Eq, ite, LT.lt, Usa1995P1.bSeq, Not, Usa1995P1.HasAp
Proof uses: Fin, And, StrictMono, Exists, HAdd.hAdd, HMul.hMul, False, dite, Eq.mpr, id, congrArg, ite_eq_left, And.left, ite_eq_right, And.right, Usa1995P1.DigitFree, Eq.symm, Usa1995P1.digitFree_bSeq, Ne, Fin.mk and 16 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
```
lemma not_hasAp {p : ℕ} (hp : p.Prime) (hp3 : 3 ≤ p) {a : ℕ → ℕ} {n m : ℕ}
    (h : ∀ i ≤ n, (if i < n then a i else m) = bSeq p i) : ¬ HasAp a p n m := by
…
```
Mentions: h, Usa1995P1.bSeq, Usa1995P1.HasAp
lemma Usa1995P1.hasAp_of_mem_digits_pred Documented declaration: hasAp_of_mem_digits_pred line 382 source
Source documentation
The construction part: if m < bSeq p n has a base-p digit equal to p - 1, then reducing every such digit of m by j (for j = p-1, …, 0) gives an arithmetic progression of length p whose first p - 1 terms are digit-free, hence equal to a at indices below n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, Eq, Usa1995P1.bSeq, Membership.mem, List, Nat.digits, HSub.hSub, Usa1995P1.HasAp
Proof uses: rfl, Nat.ofDigits, List.map, ite, HAdd.hAdd, HMul.hMul, funext, dite, of_eq_true, Eq.trans, True, congr, congrArg, ite_eq_left_of_eq_true, congrFun', eq_self, mul_one, zero_add, Not, ite_eq_right_of_eq_false and 43 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 139 steps
Open to load the checked before-and-after goal states.
```
lemma hasAp_of_mem_digits_pred {p : ℕ} (hp : 3 ≤ p) {a : ℕ → ℕ} {n m : ℕ}
    (IH : ∀ k < n, a k = bSeq p k) (hhi : m < bSeq p n)
    (hmem : p - 1 ∈ Nat.digits p m) : HasAp a p n m := by
…
```
Mentions: Usa1995P1.bSeq, Usa1995P1.HasAp
problem Usa1995P1.usa1995_p1 USA Mathematical Olympiad 1995, Problem 1 line 501 source
Source documentation
USA Mathematical Olympiad 1995, Problem 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, Odd, LT.lt, HSub.hSub, OfNat.ofNat, Eq, GE.ge, IsLeast, Set.ofPred, And, Not, Usa1995P1.HasAp, Nat.ofDigits, Nat.digits
Proof uses: LE.le, Nat.Prime.two_le, HAdd.hAdd, HMul.hMul, Usa1995P1.bSeq, Nat.strong_induction_on, Or, lt_or_ge, Eq.mpr, id, congrArg, Usa1995P1.bSeq_eq_self_of_lt, Eq.refl, And.intro, Usa1995P1.bSeq_strictMono, Usa1995P1.not_hasAp, dite, ite, ite_eq_left, ite_eq_right and 17 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 53 steps
Open to load the checked before-and-after goal states.
```
problem usa1995_p1 (p : ℕ) (hp : p.Prime) (ho : Odd p) (a : ℕ → ℕ)
    (ha₀ : ∀ n < p - 1, a n = n)
    (ha₁ : ∀ n ≥ p - 1, IsLeast {m | a (n - 1) < m ∧ ¬ HasAp a p n m} (a n)) :
    ∀ n, a n = Nat.ofDigits p (Nat.digits (p - 1) n) := by
…
```
Mentions: Usa1995P1.HasAp