`Compfiles/Usa2026P6.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 2026, Problem 6

Let a and b be positive integers such that φ(ab + 1) divides a² + b² + 1. Prove that a and b are Fibonacci numbers.

Imports (9)

Imported by 1 file

Compfiles.lean

def Usa2026P6.FibPair The classification of solutions of a^2 + b^2 + 1 = 3 * a * b: either a = b = 1, or {a, b} = {F_{2k-1}, F_{2k+1}} for some k ≥ 1 line 51 source
Source documentation
The classification of solutions of a^2 + b^2 + 1 = 3 * a * b: either a = b = 1, or {a, b} = {F_{2k-1}, F_{2k+1}} for some k ≥ 1.

no axioms what this means
Statement uses: Nat
Proof uses: Or, And, Eq, OfNat.ofNat, Exists, LE.le, Nat.fib, HSub.hSub, HMul.hMul, HAdd.hAdd
8 instances, coercions and auxiliary constants left out.
```
def FibPair (a b : ℕ) : Prop :=
…
```
lemma Usa2026P6.quotient_eq_three_aux Vieta jumping step: if a * b ∣ a^2 + b^2 + 1 with 0 < a ≤ b, then the quotient equals 3 line 59 source
Source documentation
Vieta jumping step: if a * b ∣ a^2 + b^2 + 1 with 0 < a ≤ b, then the quotient equals 3. Strong induction on the sum (the induction hypothesis is passed explicitly).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Eq, HAdd.hAdd, OfNat.ofNat, Dvd.dvd, HMul.hMul, HPow.hPow, HDiv.hDiv, LE.le
Proof uses: Eq.mpr, id, congrArg, Nat.mul_div_right, mul_pos, Eq.refl, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, Neg.neg, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr and 94 more
132 instances, coercions and auxiliary constants left out.

Tactic trace: 65 steps
Open to load the checked before-and-after goal states.
```
lemma quotient_eq_three_aux {s : ℕ}
    (IH : ∀ t : ℕ, t < s → ∀ a b : ℕ, a + b = t → 0 < a → 0 < b →
      a * b ∣ a ^ 2 + b ^ 2 + 1 → (a ^ 2 + b ^ 2 + 1) / (a * b) = 3)
    {a b : ℕ} (ha : 0 < a) (hb : 0 < b) (hsum : a + b = s) (hle : a ≤ b)
    (hdvd : a * b ∣ a ^ 2 + b ^ 2 + 1) : (a ^ 2 + b ^ 2 + 1) / (a * b) = 3 := by
…
```
lemma Usa2026P6.quotient_eq_three If a * b ∣ a^2 + b^2 + 1 for positive naturals a, b, then the quotient is 3 line 128 source
Source documentation
If a * b ∣ a^2 + b^2 + 1 for positive naturals a, b, then the quotient is 3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Dvd.dvd, HMul.hMul, HAdd.hAdd, HPow.hPow, Eq, HDiv.hDiv
Proof uses: Nat.strong_induction_on, LE.le, Or, le_or_gt, Usa2026P6.quotient_eq_three_aux, Eq.mpr, id, congrArg, mul_comm, add_comm, le_of_lt, Eq.mp, rfl
42 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma quotient_eq_three {a b : ℕ} (ha : 0 < a) (hb : 0 < b)
    (hdvd : a * b ∣ a ^ 2 + b ^ 2 + 1) : (a ^ 2 + b ^ 2 + 1) / (a * b) = 3 := by
…
```
lemma Usa2026P6.fib_add_four The Fibonacci recurrence over four steps: F_{n+4} + F_n = 3 * F_{n+2} line 146 source
Source documentation
The Fibonacci recurrence over four steps: F_{n+4} + F_n = 3 * F_{n+2}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HAdd.hAdd, Nat.fib, OfNat.ofNat, HMul.hMul
Proof uses: Nat.fib_add_two
9 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma fib_add_four (n : ℕ) : Nat.fib (n + 4) + Nat.fib n = 3 * Nat.fib (n + 2) := by
…
```
lemma Usa2026P6.fib_pair_aux Vieta jumping for the equation a^2 + b^2 + 1 = 3 * a * b with 0 < a ≤ b: the pair is a FibPair line 154 source
Source documentation
Vieta jumping for the equation a^2 + b^2 + 1 = 3 * a * b with 0 < a ≤ b: the pair is a FibPair.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Eq, HAdd.hAdd, OfNat.ofNat, HPow.hPow, HMul.hMul, Usa2026P6.FibPair, LE.le
Proof uses: Or, eq_or_lt_of_le, Or.inl, And, Exists, Nat.fib, HSub.hSub, Eq.mpr, id, congrArg, Eq.symm, mul_assoc, pow_two, Eq.refl, Iff.mp, mul_eq_one, Units, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Int and 102 more
143 instances, coercions and auxiliary constants left out.

Tactic trace: 94 steps
Open to load the checked before-and-after goal states.
```
lemma fib_pair_aux {s : ℕ}
    (IH : ∀ t : ℕ, t < s → ∀ a b : ℕ, a + b = t → 0 < a → 0 < b →
      a ^ 2 + b ^ 2 + 1 = 3 * a * b → FibPair a b)
    {a b : ℕ} (ha : 0 < a) (hb : 0 < b) (hsum : a + b = s) (hle : a ≤ b)
    (h : a ^ 2 + b ^ 2 + 1 = 3 * a * b) : FibPair a b := by
…
```
Mentions: Usa2026P6.FibPair, h
lemma Usa2026P6.fib_pair The solutions of a^2 + b^2 + 1 = 3 * a * b in positive integers are exactly the pairs {F_{2k-1}, F_{2k+1}} (and (1, 1)) line 239 source
Source documentation
The solutions of a^2 + b^2 + 1 = 3 * a * b in positive integers are exactly the pairs {F_{2k-1}, F_{2k+1}} (and (1, 1)).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, HAdd.hAdd, HPow.hPow, HMul.hMul, Usa2026P6.FibPair
Proof uses: Nat.strong_induction_on, LE.le, Or, le_or_gt, Usa2026P6.fib_pair_aux, Eq.mpr, id, congrArg, add_comm, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_add and 19 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma fib_pair {a b : ℕ} (ha : 0 < a) (hb : 0 < b)
    (h : a ^ 2 + b ^ 2 + 1 = 3 * a * b) : FibPair a b := by
…
```
Mentions: h, Usa2026P6.FibPair
lemma Usa2026P6.fibPair_fib Every entry of a FibPair is a Fibonacci number line 263 source
Source documentation
Every entry of a FibPair is a Fibonacci number.

no axioms what this means
Statement uses: Nat, Usa2026P6.FibPair, And, Exists, Eq, Nat.fib
Proof uses: OfNat.ofNat, LE.le, Or, HSub.hSub, HMul.hMul, HAdd.hAdd, And.intro, Exists.intro, Eq.symm, Nat.fib_one
12 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma fibPair_fib {a b : ℕ} (h : FibPair a b) :
    (∃ m, a = Nat.fib m) ∧ (∃ n, b = Nat.fib n) := by
…
```
Mentions: h, Usa2026P6.FibPair
lemma Usa2026P6.sq_mod_two Parity helper: a square has the same parity as its root line 272 source
Source documentation
Parity helper: a square has the same parity as its root.

standard axioms: propext what this means
Statement uses: Nat, Eq, HMod.hMod, HPow.hPow, OfNat.ofNat
Proof uses: Eq.mpr, HMul.hMul, id, congrArg, pow_two, Nat.mul_mod, LT.lt, Nat.mod_lt, two_pos, dite, LE.le, Eq.refl, Eq.symm, le_antisymm, Nat.ge_of_not_lt, Mathlib.Tactic.IntervalCases.of_lt_right, Nat.rawCast, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_ofNat, Not and 1 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma sq_mod_two (x : ℕ) : x ^ 2 % 2 = x % 2 := by
…
```
lemma Usa2026P6.sq_mod_four_of_odd Odd squares are 1 mod 4 line 278 source
Source documentation
Odd squares are 1 mod 4.

standard axioms: propext what this means
Statement uses: Nat, Eq, HMod.hMod, OfNat.ofNat, HPow.hPow
Proof uses: Eq.mpr, id, congrArg, Nat.mod_mod_of_dvd, of_decide_eq_true, Dvd.dvd, Bool, Decidable.decide, Bool.true, Eq.refl, LT.lt, Nat.mod_lt, HMul.hMul, pow_two, Nat.mul_mod, dite, LE.le, Eq.symm, le_antisymm, Nat.ge_of_not_lt and 12 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma sq_mod_four_of_odd {x : ℕ} (hx : x % 2 = 1) : x ^ 2 % 4 = 1 := by
…
```
lemma Usa2026P6.sq_mod_four_of_even Even squares are 0 mod 4 line 291 source
Source documentation
Even squares are 0 mod 4.

standard axioms: propext what this means
Statement uses: Nat, Eq, HMod.hMod, OfNat.ofNat, HPow.hPow
Proof uses: Eq.mpr, id, congrArg, Nat.mod_mod_of_dvd, of_decide_eq_true, Dvd.dvd, Bool, Decidable.decide, Bool.true, Eq.refl, LT.lt, Nat.mod_lt, HMul.hMul, pow_two, Nat.mul_mod, dite, LE.le, False.elim, Eq.mp, False and 12 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma sq_mod_four_of_even {x : ℕ} (hx : x % 2 = 0) : x ^ 2 % 4 = 0 := by
…
```
problem Usa2026P6.usa2026_p6 line 305 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Dvd.dvd, Nat.totient, HAdd.hAdd, HMul.hMul, HPow.hPow, And, Exists, Eq, Nat.fib
Proof uses: dite, And.intro, Exists.intro, Eq.symm, Nat.fib_one, Not, LE.le, Decidable.byContradiction, Nat.mul_le_mul, le_antisymm, Nat.le_of_lt_succ, Eq.mp, congrFun', congrArg, mul_one, Nat.eq_one_of_mul_eq_one_right, Nat.eq_one_of_mul_eq_one_left, rfl, Even.two_dvd, Nat.totient_even and 209 more
190 instances, coercions and auxiliary constants left out.

Tactic trace: 374 steps (first 200 of 374)
Open to load the checked before-and-after goal states.