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

7 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1991, Problem 3

Define the function $f$ on the natural numbers by $f(1) = 2$, $f(n) = 2^{f(n-1)}$. Show that $f(n)$ has the same residue mod $m$ for all sufficiently large $n$.

Imports (5)

Imported by 1 file

Compfiles.lean

def Usa1991P3.f The tower-of-exponents function of the problem, with the index shifted by one: f 0 = 2 and f (n + 1) = 2 ^ f n, so that the problem's f n is our f (n - 1) line 32 source

Source documentation

The tower-of-exponents function of the problem, with the index shifted by one: f 0 = 2 and f (n + 1) = 2 ^ f n, so that the problem's f n is our f (n - 1).

standard axioms: propext what this means

Statement uses: Nat

2 instances, coercions and auxiliary constants left out.

def f : ℕ → ℕ
  | 0 => 2
  | n + 1 => 2 ^ f n

snip begin

/- The trick of the problem is to use strong induction on the modulus `m`
(not on `n`). The case `m = 1` is trivial. If `m` is even, write `m = 2 ^ a * b`
with `b` odd: by the induction hypothesis `f n` is eventually constant mod `b`,
while `f n` is eventually `0` mod `2 ^ a`, so the Chinese remainder theorem gives
that `f n` is eventually constant mod `m`. If `m` is odd, then `2 ^ φ m ≡ 1 [MOD m]`
by Euler's theorem and `φ m < m`, so by the induction hypothesis `f n` is eventually

lemma Usa1991P3.f_succ line 46 source
standard axioms: propext what this means
Statement uses: Nat, Eq, Usa1991P3.f, HAdd.hAdd, OfNat.ofNat, HPow.hPow
Proof uses: rfl
10 instances, coercions and auxiliary constants left out.
lemma Usa1991P3.le_f The tower grows at least linearly line 49 source
Source documentation
The tower grows at least linearly.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HAdd.hAdd, OfNat.ofNat, Usa1991P3.f
Proof uses: Nat.recAux, Nat.le.refl, HPow.hPow, Nat.pow_le_pow_right, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, LT.lt, Nat.lt_two_pow_self, Trans.trans, Eq, rfl
25 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma le_f (n : ℕ) : n + 2 ≤ f n := by
…
```
Mentions: Usa1991P3.f
lemma Usa1991P3.f_monotone line 62 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monotone, Nat, Usa1991P3.f
Proof uses: monotone_nat_of_le_succ, LT.lt, HPow.hPow, OfNat.ofNat, Nat.lt_two_pow_self, Trans.trans, LE.le, Eq, HAdd.hAdd, LT.lt.le, rfl
12 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa1991P3.two_pow_dvd_f Eventually f n is divisible by any prescribed power of two line 70 source
Source documentation
Eventually f n is divisible by any prescribed power of two.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Dvd.dvd, HPow.hPow, Usa1991P3.f
Proof uses: Eq, HAdd.hAdd, Exists, Exists.intro, HSub.hSub, Usa1991P3.le_f, Nat.pow_dvd_pow, Eq.symm
22 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma two_pow_dvd_f (a n : ℕ) (ha : 1 ≤ a) (hn : a ≤ n) : 2 ^ a ∣ f n := by
…
```
Mentions: Usa1991P3.f
lemma Usa1991P3.eventually_constant_mod Main step: strong induction on the modulus line 76 source
Source documentation
Main step: strong induction on the modulus.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Exists, Nat.ModEq, Usa1991P3.f
Proof uses: Nat.strong_induction_on, LT.lt, Eq, Or, eq_or_lt_of_le, Exists.intro, of_eq_true, HMod.hMod, Eq.trans, True, congr, congrArg, Nat.mod_one, eq_self, dite, Even, And, Odd, HMul.hMul, HPow.hPow and 119 more
131 instances, coercions and auxiliary constants left out.

Tactic trace: 59 steps
Open to load the checked before-and-after goal states.
```
lemma eventually_constant_mod (m : ℕ) (hm : 1 ≤ m) :
    ∃ N : ℕ, ∀ n : ℕ, N ≤ n → f n ≡ f N [MOD m] := by
…
```
Mentions: Usa1991P3.f
problem Usa1991P3.usa1991_p3 line 134 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Exists, Nat.ModEq, Usa1991P3.f
Proof uses: Usa1991P3.eventually_constant_mod
4 instances, coercions and auxiliary constants left out.