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

11 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2012, Problem 4

Find all functions $f : \mathbb{N} \to \mathbb{N}$ such that $f(n!) = f(n)!$ for all positive integers $n$ and such that $m - n$ divides $f(m) - f(n)$ for all distinct positive integers $m, n$.

Imports (6)

Imported by 1 file

Compfiles.lean

def Usa2012P4.IsSolution The conditions of the problem on a function f : ℕ → ℕ line 37 source
Source documentation
The conditions of the problem on a function f : ℕ → ℕ. Since the problem is about functions on the positive integers, we require positivity of f on positive inputs explicitly; the value f 0 is irrelevant.

no axioms what this means
Statement uses: Nat
Proof uses: And, LT.lt, OfNat.ofNat, Eq, Nat.factorial, Ne, Dvd.dvd, Int, HSub.hSub
7 instances, coercions and auxiliary constants left out.
```
def IsSolution (f : ℕ → ℕ) : Prop :=
…
```
Mentions: f
lemma Usa2012P4.eq_one_or_two_of_factorial_eq_self If a positive integer equals its own factorial, then it is 1 or 2 line 47 source
Source documentation
If a positive integer equals its own factorial, then it is 1 or 2.

standard axioms: propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Nat.factorial, Or
Proof uses: Nat.succ, Exists, Nat.exists_eq_succ_of_ne_zero, Iff.mp, Ne, Nat.pos_iff_ne_zero, id, HMul.hMul, HAdd.hAdd, Eq.mpr, congrArg, Eq.mp, Nat.factorial_succ, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm and 29 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma eq_one_or_two_of_factorial_eq_self {x : ℕ} (hx : 0 < x) (h : x ! = x) :
    x = 1 ∨ x = 2 := by
…
```
Mentions: h
lemma Usa2012P4.lt_of_dvd_factorial_sub If d ≥ 2 divides `(t ! line 62 source
Source documentation
If d ≥ 2 divides (t ! : ℤ) - c but does not divide c, then t < d, because d ∣ t ! as soon as t ≥ d.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Dvd.dvd, HSub.hSub, Nat.factorial, LE.le, OfNat.ofNat, Not, LT.lt
Proof uses: Decidable.byContradiction, Iff.mp, not_lt, Iff.mpr, Int.natCast_dvd_natCast, Nat.dvd_factorial, dvd_sub, Eq, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, Mathlib.Tactic.Ring.Common.sub_congr, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.Common.atom_pf and 25 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma lt_of_dvd_factorial_sub {d t : ℕ} {c : ℤ} (h : (d : ℤ) ∣ (t ! : ℤ) - c)
    (hd : 2 ≤ d) (hdc : ¬(d : ℤ) ∣ c) : t < d := by
…
```
Mentions: h
def Usa2012P4.iterFac Iterated factorials starting at 3: iterFac 0 = 3 and iterFac (r + 1) = (iterFac r)! line 76 source
Source documentation
Iterated factorials starting at 3: iterFac 0 = 3 and iterFac (r + 1) = (iterFac r)!. These are used to produce arbitrarily large fixed points of f (Shankar Padmanabhan's argument).

no axioms what this means
Statement uses: Nat
2 instances, coercions and auxiliary constants left out.
```
def iterFac : ℕ → ℕ
  | 0 => 3
  | r + 1 => (iterFac r)!
```
lemma Usa2012P4.iterFac_ge line 80 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, HAdd.hAdd, OfNat.ofNat, Usa2012P4.iterFac
Proof uses: Nat.recAux, le_refl, LT.lt, Nat.factorial, Nat.lt_factorial_self, le_trans, id
12 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Usa2012P4.f_iterFac Every iterated factorial of 3 is a fixed point of f, once f 3 = 3 line 89 source
Source documentation
Every iterated factorial of 3 is a fixed point of f, once f 3 = 3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Nat.factorial, Usa2012P4.iterFac
Proof uses: Nat.recAux, LE.le, HAdd.hAdd, Usa2012P4.iterFac_ge, id, Eq.mpr, congrArg, Eq.refl
8 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma f_iterFac {f : ℕ → ℕ} (hfact : ∀ n, 0 < n → f (n !) = (f n)!) (hf3 : f 3 = 3)
    (r : ℕ) : f (iterFac r) = iterFac r := by
…
```
Mentions: f, Usa2012P4.iterFac
lemma Usa2012P4.eq_one_const_of_f_two_eq_one Case f 2 = 1: then f is identically 1 on positive integers line 99 source
Source documentation
Case f 2 = 1: then f is identically 1 on positive integers.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Nat.factorial, Ne, Dvd.dvd, Int, HSub.hSub
Proof uses: LE.le, Nat.factorial_le, rfl, Nat.factorial_pos, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Iff.mpr, Int.natCast_dvd_natCast, Nat.dvd_factorial, of_decide_eq_true, id, Decidable.decide, Bool.true, dvd_trans, dvd_sub, Eq.mp, congrArg and 21 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 47 steps
Open to load the checked before-and-after goal states.
```
lemma eq_one_const_of_f_two_eq_one {f : ℕ → ℕ} (hpos : ∀ n, 0 < n → 0 < f n)
    (hfact : ∀ n, 0 < n → f (n !) = (f n)!)
    (hdiv : ∀ (m n : ℕ), 0 < m → 0 < n → m ≠ n → (m : ℤ) - n ∣ (f m : ℤ) - f n)
    (hf2 : f 2 = 1) (n : ℕ) (hn : 0 < n) : f n = 1 := by
…
```
Mentions: f
lemma Usa2012P4.eq_two_const_of_f_one_two_eq_two Case f 1 = f 2 = 2: then f is identically 2 on positive integers line 133 source
Source documentation
Case f 1 = f 2 = 2: then f is identically 2 on positive integers.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Nat.factorial, Ne, Dvd.dvd, Int, HSub.hSub
Proof uses: Nat.zero_lt_succ, Eq.mp, congrArg, rfl, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Usa2012P4.lt_of_dvd_factorial_sub, Mathlib.Meta.NormNum.isNat_le_true, Bool.true, of_decide_eq_true, Not, id, Decidable.decide, dite, LE.le, absurd, Eq.symm and 19 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 64 steps
Open to load the checked before-and-after goal states.
```
lemma eq_two_const_of_f_one_two_eq_two {f : ℕ → ℕ} (hpos : ∀ n, 0 < n → 0 < f n)
    (hfact : ∀ n, 0 < n → f (n !) = (f n)!)
    (hdiv : ∀ (m n : ℕ), 0 < m → 0 < n → m ≠ n → (m : ℤ) - n ∣ (f m : ℤ) - f n)
    (hf1 : f 1 = 2) (hf2 : f 2 = 2) (n : ℕ) (hn : 0 < n) : f n = 2 := by
…
```
Mentions: f
lemma Usa2012P4.eq_id_of_f_one_eq_one Case f 1 = 1 and f 2 = 2: then f is the identity on positive integers line 176 source
Source documentation
Case f 1 = 1 and f 2 = 2: then f is the identity on positive integers.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Nat.factorial, Ne, Dvd.dvd, Int, HSub.hSub
Proof uses: Nat.zero_lt_succ, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Usa2012P4.lt_of_dvd_factorial_sub, Eq.mp, congrArg, Mathlib.Meta.NormNum.isNat_le_true, Bool.true, of_decide_eq_true, Not, id, Decidable.decide, Mathlib.Meta.NormNum.isNat_lt_true, dite, LE.le, absurd, Eq.symm and 63 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 48 steps
Open to load the checked before-and-after goal states.
```
lemma eq_id_of_f_one_eq_one {f : ℕ → ℕ} (hpos : ∀ n, 0 < n → 0 < f n)
    (hfact : ∀ n, 0 < n → f (n !) = (f n)!)
    (hdiv : ∀ (m n : ℕ), 0 < m → 0 < n → m ≠ n → (m : ℤ) - n ∣ (f m : ℤ) - f n)
    (hf1 : f 1 = 1) (hf2 : f 2 = 2) (n : ℕ) (hn : 0 < n) : f n = n := by
…
```
Mentions: f
determine Usa2012P4.solution_set The answer: the constant functions 1 and 2, and the identity (on positive integers) line 221 source
Source documentation
The answer: the constant functions 1 and 2, and the identity (on positive integers).

no axioms what this means
Statement uses: Set, Nat
Proof uses: Set.ofPred, Or, LT.lt, OfNat.ofNat, Eq
2 instances, coercions and auxiliary constants left out.
```
determine solution_set : Set (ℕ → ℕ) :=
…
```
problem Usa2012P4.usa2012_p4 line 224 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Iff, Membership.mem, Set, Usa2012P4.solution_set, Usa2012P4.IsSolution
Proof uses: Iff.intro, LT.lt, OfNat.ofNat, Eq, Or, And.intro, And, Nat.factorial, Ne, Dvd.dvd, Int, HSub.hSub, Eq.mpr, id, congrArg, zero_lt_one, Nat.factorial_pos, Nat.factorial_one, Eq.refl, sub_self and 16 more
42 instances, coercions and auxiliary constants left out.

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