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

24 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2023, Problem 5

Let n be an integer greater than 2. We will be arranging the numbers 1, 2, ... n² into an n × n grid. Such an arrangement is called row-valid if the numbers in each row can be permuted to make an arithmetic progression. Similarly, such an arrangement is called column-valid if the numbers in each column can be permuted to make an arithmetic progression.

Determine the values of n for which it possible to transform any row-valid arrangement into a column-valid arrangement by permuting the numbers in each row.

Imports (5)

Imported by 1 file

Compfiles.lean

def Usa2023P5.PermutedArithSeq line 36 source
standard axioms: propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Function.Embedding, Fin, HPow.hPow
Proof uses: Exists, And, Function.Bijective, Eq, HAdd.hAdd, Fin.mk, HMul.hMul
19 instances, coercions and auxiliary constants left out.
def Usa2023P5.row_valid line 40 source
standard axioms: propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Fin, HPow.hPow, Function.Injective2
Proof uses: Usa2023P5.PermutedArithSeq, Function.Embedding.mk
13 instances, coercions and auxiliary constants left out.
def Usa2023P5.col_valid line 43 source
standard axioms: propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Fin, HPow.hPow, Function.Injective2
Proof uses: Usa2023P5.PermutedArithSeq, Function.Embedding.mk
13 instances, coercions and auxiliary constants left out.
theorem Usa2023P5.injective_of_permuted_rows line 46 source
standard axioms: propext what this means
Statement uses: Function.Injective2, Function.Injective
Proof uses: Eq, And, Eq.mpr, id, congrArg, Eq.mp, of_eq_true, Eq.trans, True, congr, eq_self, and_self
1 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
determine Usa2023P5.solution_set line 55 source
standard axioms: propext what this means
Statement uses: Set, Nat
Proof uses: Set.ofPred, Nat.Prime
def Usa2023P5.trygub The Anton Trygub counterexample construction for composite n with prime divisor q, at the level of natural number values line 63 source
Source documentation
The Anton Trygub counterexample construction for composite n with prime divisor q, at the level of natural number values. Row 0 is 0, …, n-1; rows 1 ≤ r ≤ q are arithmetic progressions with difference q filling n, …, n*q+n-1; the remaining rows contain the leftover numbers in reading order.

no axioms what this means
Statement uses: Nat
Proof uses: ite, Eq, OfNat.ofNat, LE.le, HAdd.hAdd, HSub.hSub, HMul.hMul
10 instances, coercions and auxiliary constants left out.
```
def trygub (n q r c : ℕ) : ℕ :=
…
```
lemma Usa2023P5.trygub_row_zero line 66 source
no axioms what this means
Statement uses: Nat, Eq, Usa2023P5.trygub, OfNat.ofNat
Proof uses: rfl
2 instances, coercions and auxiliary constants left out.
lemma Usa2023P5.trygub_lt line 68 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, LE.le, OfNat.ofNat, HAdd.hAdd, Usa2023P5.trygub, HPow.hPow
Proof uses: id, dite, ite, Eq, HSub.hSub, HMul.hMul, Eq.mpr, congrFun', congrArg, ite_eq_left, Trans.trans, pow_two, Nat.le_mul_of_pos_left, Not, ite_eq_right, Nat.succ, Eq.symm, Nat.mul_succ, Eq.refl, Nat.mul_le_mul_left and 8 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
lemma Usa2023P5.trygub_eq_zero line 96 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Usa2023P5.trygub, And
Proof uses: id, dite, ite, HAdd.hAdd, HSub.hSub, HMul.hMul, Eq.mpr, implies_congr, congrFun', congrArg, ite_eq_left, Eq.refl, And.intro, Not, ite_eq_right
14 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Usa2023P5.trygub_mid_bounds Rows 1 ≤ r ≤ q contain values in [n, n*q+n) line 105 source
Source documentation
Rows 1 ≤ r ≤ q contain values in [n, n*q+n).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, OfNat.ofNat, LE.le, LT.lt, And, Usa2023P5.trygub, HAdd.hAdd, HMul.hMul
Proof uses: id, Eq.mpr, ite, Eq, HSub.hSub, congrArg, ite_eq_right, ite_eq_left, Trans.trans, Nat.succ, Eq.symm, Nat.mul_succ, Eq.refl, Nat.mul_le_mul_left, Nat.mul_comm
21 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma trygub_mid_bounds {n q r c : ℕ} (h0 : r ≠ 0) (hle : r ≤ q) (hc : c < n) :
    n ≤ trygub n q r c ∧ trygub n q r c < n * q + n := by
…
```
Mentions: Usa2023P5.trygub
lemma Usa2023P5.trygub_top_bound Rows r > q contain values in [n*q+n, n^2) line 116 source
Source documentation
Rows r > q contain values in [n*q+n, n^2).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Not, LE.le, HAdd.hAdd, HMul.hMul, Usa2023P5.trygub
Proof uses: id, Eq.mpr, ite, Eq, OfNat.ofNat, HSub.hSub, congrArg, ite_eq_right
17 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma trygub_top_bound (n q : ℕ) {r : ℕ} (c : ℕ) (hle : ¬ r ≤ q) :
    n * q + n ≤ trygub n q r c := by
…
```
Mentions: Usa2023P5.trygub
lemma Usa2023P5.trygub_last_ge line 122 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HAdd.hAdd, HSub.hSub, HPow.hPow, Usa2023P5.trygub
Proof uses: id, dite, ite, Eq, HMul.hMul, Eq.mpr, congrArg, ite_eq_left, Not, ite_eq_right, Eq.symm, Nat.add_mul, Nat.sub_add_cancel, Eq.refl, add_mul, Nat.mul_comm, pow_two, Eq.mp
33 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma Usa2023P5.trygub_inj line 136 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HAdd.hAdd, LT.lt, Eq, Usa2023P5.trygub, And
Proof uses: dite, And.intro, rfl, Eq.mp, congrArg, Usa2023P5.trygub_row_zero, Eq.symm, Not, And.left, HMul.hMul, Usa2023P5.trygub_mid_bounds, Usa2023P5.trygub_top_bound, HSub.hSub, ite, ite_eq_left, ite_eq_right, HMod.hMod, Eq.mpr, id, Nat.add_mul_mod_self_left and 9 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 94 steps
Open to load the checked before-and-after goal states.
lemma Usa2023P5.trygub_eq_add_one line 205 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, Eq, Usa2023P5.trygub, HAdd.hAdd
Proof uses: dite, Eq.mp, ite, HSub.hSub, HMul.hMul, congrFun', congrArg, ite_eq_left, Not, Nat.add_zero, Nat.mul_zero, Eq.symm, ite_eq_right, Nat.le_mul_of_pos_right, Nat.mul_le_mul_left
22 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Usa2023P5.trygub_eq_two_mul_add_one line 219 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Dvd.dvd, LT.lt, Eq, Usa2023P5.trygub, HAdd.hAdd, HMul.hMul
Proof uses: dite, Eq.mp, ite, HSub.hSub, congrFun', congrArg, ite_eq_left, Not, ite_eq_right, HMod.hMod, Eq.mpr, id, Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt, Nat.add_comm, Eq.trans, Eq.symm, Nat.mul_le_mul_left
28 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
lemma Usa2023P5.trygub_mid line 238 source
no axioms what this means
Statement uses: Nat, Ne, OfNat.ofNat, LE.le, Eq, Usa2023P5.trygub, HAdd.hAdd, HSub.hSub, HMul.hMul
Proof uses: id, Eq.mpr, ite, congrArg, ite_eq_right, ite_eq_left, Eq.refl
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2023P5.trygub_top line 243 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Not, LE.le, Eq, Usa2023P5.trygub, HAdd.hAdd, HMul.hMul, HSub.hSub, OfNat.ofNat
Proof uses: id, Eq.mpr, ite, congrArg, ite_eq_right, Eq.refl
19 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2023P5.div_lt_of_mem The quotient of an element of Fin (n^2) by n is again in Fin n line 249 source
Source documentation
The quotient of an element of Fin (n^2) by n is again in Fin n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HPow.hPow, OfNat.ofNat, LT.lt, HDiv.hDiv
Proof uses: Nat.div_lt_of_lt_mul, Eq.mpr, HMul.hMul, id, Eq, congrArg, Eq.symm, pow_two, Fin.isLt
21 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma div_lt_of_mem {n : ℕ} (v : Fin (n ^ 2)) : v.val / n < n :=
…
```
lemma Usa2023P5.ap_k_pos The common difference of a permuted arithmetic progression of length at least 2 of elements of Fin (n^2) is positive line 254 source
Source documentation
The common difference of a permuted arithmetic progression of length at least 2 of elements of Fin (n^2) is positive.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, Fin, HPow.hPow, Function.Injective, Eq, HAdd.hAdd, Fin.mk, HMul.hMul
Proof uses: Decidable.byContradiction, Not, False, Fin.ext, Eq.mpr, id, congrArg, Nat.mul_zero, Nat.add_zero, Eq.refl, Eq.symm
29 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma ap_k_pos {n : ℕ} (hn : 0 < n) (h2 : 2 ≤ n) {f : Fin n → Fin (n ^ 2)} (hf : f.Injective)
    {p : Fin n → Fin n} (hp : p.Injective) {k : ℕ}
    (hk : ∀ m : Fin n, (f (p m)).val = (f (p ⟨0, hn⟩)).val + m.val * k) : 1 ≤ k := by
…
```
Mentions: f
lemma Usa2023P5.ap_res_inj For prime n, an arithmetic progression of length n whose common difference is not divisible by n hits every residue class mod n at most once line 269 source
Source documentation
For prime n, an arithmetic progression of length n whose common difference is not divisible by n hits every residue class mod n at most once.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, Not, Dvd.dvd, Fin, Eq, HMod.hMod, HAdd.hAdd, HMul.hMul
Proof uses: Fact, Fact.mk, ZMod, Eq.mpr, id, congrArg, propext, ZMod.natCast_eq_natCast_iff', Ne, OfNat.ofNat, Eq.mp, ZMod.natCast_eq_zero_iff, add_left_cancel, congr, Eq.trans, Nat.cast_add, Nat.cast_mul, mul_right_cancel₀, Eq.symm, Nat.mod_eq_of_lt and 4 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma ap_res_inj {n : ℕ} (hp : n.Prime) {k : ℕ} (hk : ¬ n ∣ k) (b : ℕ) {m₁ m₂ : Fin n}
    (h : (b + m₁.val * k) % n = (b + m₂.val * k) % n) : m₁ = m₂ := by
…
```
Mentions: h
def Usa2023P5.trygubArr The Trygub arrangement, packaged as a grid of elements of Fin (n^2) line 290 source
Source documentation
The Trygub arrangement, packaged as a grid of elements of Fin (n^2).

standard axioms: propext what this means
Statement uses: Nat, Fin, LT.lt, Usa2023P5.trygub, HPow.hPow, OfNat.ofNat
Proof uses: Fin.mk
14 instances, coercions and auxiliary constants left out.
```
def trygubArr (n q : ℕ) (hbound : ∀ r c : Fin n, trygub n q r.val c.val < n ^ 2) :
    Fin n → Fin n → Fin (n ^ 2) :=
…
```
Mentions: Usa2023P5.trygub
lemma Usa2023P5.trygubArr_injective2 line 294 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, HAdd.hAdd, Fin, LT.lt, Usa2023P5.trygub, HPow.hPow, Function.Injective2, Usa2023P5.trygubArr
Proof uses: Eq, congrArg, And, Usa2023P5.trygub_inj, Fin.isLt, And.intro, Fin.ext
21 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2023P5.trygubArr_row_valid line 302 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, Fin, Usa2023P5.trygub, HPow.hPow, Function.Injective2, Usa2023P5.trygubArr, Usa2023P5.row_valid
Proof uses: dite, Usa2023P5.PermutedArithSeq, Function.Embedding.mk, Eq, Exists.intro, And, Function.Bijective, Exists, Function.Embedding, HAdd.hAdd, Fin.mk, HMul.hMul, id, And.intro, Function.bijective_id, Eq.mpr, congrArg, Usa2023P5.trygub_row_zero, Not, HSub.hSub and 3 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
problem Usa2023P5.usa2023_p5 line 328 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Iff, Membership.mem, Set, Usa2023P5.solution_set, Fin, HPow.hPow, Function.Injective2, Usa2023P5.row_valid, Nat.zero_lt_of_lt, Exists, Function.Injective, Usa2023P5.col_valid, Usa2023P5.injective_of_permuted_rows
Proof uses: Iff.intro, Nat.Prime, LE.le, And, Function.Bijective, Eq, HAdd.hAdd, Fin.mk, HMul.hMul, Function.Embedding, Function.Embedding.mk, Usa2023P5.PermutedArithSeq, Exists.intro, And.intro, Dvd.dvd, HMod.hMod, And.right, Function.Surjective, And.left, Eq.mpr and 96 more
101 instances, coercions and auxiliary constants left out.

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