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

27 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2026, Problem 2

Annie is playing a game where she starts with a row of positive integers, written on a blackboard, each of which is a power of 2. On each turn, she can erase two adjacent numbers and replace them with a power of 2 that is greater than either of the erased numbers. This shortens the row of numbers, and she continues to take turns until only one number remains. Annie wins the game if the final remaining number is less than 4 times the sum of the original numbers. Is it always possible for Annie to win, regardless of the starting row of numbers?

Imports (5)

Imported by 1 file

Compfiles.lean

def Usa2026P2.IsPow2 A positive integer which is a power of two (in particular 1 = 2 ^ 0 counts) line 34 source
Source documentation
A positive integer which is a power of two (in particular 1 = 2 ^ 0 counts).

standard axioms: propext what this means
Statement uses: Nat
Proof uses: Exists, Eq, HPow.hPow, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
```
def IsPow2 (x : ℕ) : Prop := ∃ k, x = 2 ^ k
```
inductive Usa2026P2.Move One legal turn of the game: the two adjacent entries x and y are erased and replaced by a power of two z which is strictly larger than both of them line 38 source
Source documentation
One legal turn of the game: the two adjacent entries x and y are erased and replaced by a power of two z which is strictly larger than both of them.

standard axioms: propext what this means
Statement uses: List, Nat
```
inductive Move : List ℕ → List ℕ → Prop
  | mk (l r : List ℕ) (x y z : ℕ) (hz : IsPow2 z) (hx : x < z) (hy : y < z) :
      Move (l ++ x :: y :: r) (l ++ z :: r)

snip begin

/-!
### Proof sketch

(following Evan Chen's USAMO 2026 solution notes,
<https://web.evanchen.cc/exams/USAMO-2026-notes.pdf>)
```
Mentions: Usa2026P2.IsPow2, solution
def Usa2026P2.innerSum For l = [b₁, ..., bₘ], innerSum l is `4 * b₁ + 4 * b₂ + line 70 source
Source documentation
For l = [b₁, ..., bₘ], innerSum l is 4 * b₁ + 4 * b₂ + ... + 4 * b_{m-1} + 2 * bₘ (and 0 for the empty list): the "tail" of S after the first entry.

no axioms what this means
Statement uses: List, Nat
2 instances, coercions and auxiliary constants left out.
```
def innerSum : List ℕ → ℕ
  | [] => 0
  | [x] => 2 * x
  | x :: y :: rest => 4 * x + innerSum (y :: rest)

/-- The target bound for a row `a = [a₁, ..., aₙ]`: `a₁` if `n = 1`, and
`2 * a₁ + 4 * a₂ + ... + 4 * a_{n-1} + 2 * aₙ` if `n ≥ 2` (and `0` if `n = 0`). -/
```
def Usa2026P2.S The target bound for a row a = [a₁, ..., aₙ]: a₁ if n = 1, and `2 * a₁ + 4 * a₂ + line 77 source
Source documentation
The target bound for a row a = [a₁, ..., aₙ]: a₁ if n = 1, and 2 * a₁ + 4 * a₂ + ... + 4 * a_{n-1} + 2 * aₙ if n ≥ 2 (and 0 if n = 0).

no axioms what this means
Statement uses: List, Nat
Proof uses: Usa2026P2.innerSum.match_1, Unit, OfNat.ofNat, HAdd.hAdd, HMul.hMul, Usa2026P2.innerSum, List.cons
5 instances, coercions and auxiliary constants left out.
```
def S : List ℕ → ℕ
  | [] => 0
  | [x] => x
  | x :: y :: rest => 2 * x + innerSum (y :: rest)
```
Mentions: Usa2026P2.innerSum
theorem Usa2026P2.innerSum_nil line 82 source
no axioms what this means
Statement uses: Eq, Nat, Usa2026P2.innerSum, List.nil, OfNat.ofNat
Proof uses: rfl
1 instances, coercions and auxiliary constants left out.
theorem Usa2026P2.innerSum_singleton line 83 source
no axioms what this means
Statement uses: Nat, Eq, Usa2026P2.innerSum, List.cons, List.nil, HMul.hMul, OfNat.ofNat
Proof uses: rfl
3 instances, coercions and auxiliary constants left out.
theorem Usa2026P2.innerSum_cons_cons line 84 source
no axioms what this means
Statement uses: Nat, List, Eq, Usa2026P2.innerSum, List.cons, HAdd.hAdd, HMul.hMul, OfNat.ofNat
Proof uses: rfl
5 instances, coercions and auxiliary constants left out.
theorem Usa2026P2.S_nil line 87 source
no axioms what this means
Statement uses: Eq, Nat, Usa2026P2.S, List.nil, OfNat.ofNat
Proof uses: rfl
1 instances, coercions and auxiliary constants left out.
theorem Usa2026P2.S_singleton line 88 source
no axioms what this means
Statement uses: Nat, Eq, Usa2026P2.S, List.cons, List.nil
Proof uses: rfl
theorem Usa2026P2.S_cons_cons line 89 source
no axioms what this means
Statement uses: Nat, List, Eq, Usa2026P2.S, List.cons, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Usa2026P2.innerSum
Proof uses: rfl
5 instances, coercions and auxiliary constants left out.
theorem Usa2026P2.innerSum_le_four_mul_sum line 92 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, LE.le, Usa2026P2.innerSum, HMul.hMul, OfNat.ofNat, List.sum
16 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem Usa2026P2.S_lt_four_mul_sum The bound S a is always less than four times the sum of the row line 101 source
Source documentation
The bound S a is always less than four times the sum of the row.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, Ne, List.nil, Membership.mem, LT.lt, OfNat.ofNat, Usa2026P2.S, HMul.hMul, List.sum
Proof uses: False.elim, rfl, List.cons, List.mem_singleton_self, Eq.mpr, id, Eq, congrArg, List.sum_singleton, HAdd.hAdd, List.mem_cons_self, LE.le, Usa2026P2.innerSum, Usa2026P2.innerSum_le_four_mul_sum
23 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem S_lt_four_mul_sum : ∀ (a : List ℕ), a ≠ [] → (∀ x ∈ a, 0 < x) → S a < 4 * a.sum
  | [], h, _ => (h rfl).elim
  | [x], _, h => by
      have hx : 0 < x := h x (List.mem_singleton_self x)
…
```
Mentions: Usa2026P2.S, h
theorem Usa2026P2.two_mul_last_le_innerSum The last entry of a nonempty row, doubled, is at most innerSum of the row line 114 source
Source documentation
The last entry of a nonempty row, doubled, is at most innerSum of the row.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, LE.le, HMul.hMul, OfNat.ofNat, Usa2026P2.innerSum, HAppend.hAppend, List.cons, List.nil
14 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem two_mul_last_le_innerSum : ∀ (q : List ℕ) (y : ℕ), 2 * y ≤ innerSum (q ++ [y])
  | [], y => le_refl _
  | [x], y => by
      simp only [List.singleton_append, innerSum_cons_cons, innerSum_singleton]
      lia
  | x :: z :: q', y => by
      have ih := two_mul_last_le_innerSum (z :: q') y
…
```
Mentions: Usa2026P2.innerSum, Usa2026P2.innerSum_cons_cons, Usa2026P2.innerSum_singleton
theorem Usa2026P2.two_mul_getLast_le_S The last entry of a row with at least two entries, doubled, is at most S of the row line 127 source
Source documentation
The last entry of a row with at least two entries, doubled, is at most S of the row.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, LE.le, OfNat.ofNat, List.length, Ne, List.nil, HMul.hMul, List.getLast, Usa2026P2.S
Proof uses: Exists, Eq, List.cons, List.exists_cons_of_ne_nil, False, False.elim, Eq.mp, Eq.trans, congrArg, zero_add, Eq.symm, Eq.mpr, HAdd.hAdd, Usa2026P2.innerSum, id, Usa2026P2.S_cons_cons, List.cons_ne_nil, rfl, HAppend.hAppend, List.dropLast and 2 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
theorem two_mul_getLast_le_S (a : List ℕ) (ha : 2 ≤ a.length) (h : a ≠ []) :
    2 * a.getLast h ≤ S a := by
…
```
Mentions: h, Usa2026P2.S
theorem Usa2026P2.innerSum_cons Expanding innerSum at the head of a nonempty tail: the head entry is counted with coefficient 4 in innerSum but with coefficient 2 in S line 143 source
Source documentation
Expanding innerSum at the head of a nonempty tail: the head entry is counted with coefficient 4 in innerSum but with coefficient 2 in S.

standard axioms: propext what this means
Statement uses: Nat, List, Ne, List.nil, Eq, Usa2026P2.innerSum, List.cons, HAdd.hAdd, Usa2026P2.S, HMul.hMul, OfNat.ofNat
Proof uses: Exists, List.exists_cons_of_ne_nil, id, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, 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.mpr, congrArg, Eq.symm, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_add, Mathlib.Tactic.Ring.Common.mul_pf_right, Mathlib.Meta.NormNum.IsNat.to_raw_eq and 10 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem innerSum_cons (y : ℕ) (m : List ℕ) (hm : m ≠ []) :
    innerSum (y :: m) = S (y :: m) + 2 * y := by
…
```
Mentions: Usa2026P2.innerSum, Usa2026P2.S
theorem Usa2026P2.S_cons_cons_append Expanding S at the two leftmost entries of a row line 150 source
Source documentation
Expanding S at the two leftmost entries of a row.

standard axioms: propext what this means
Statement uses: Nat, List, Ne, HAppend.hAppend, List.nil, Eq, Usa2026P2.S, List.cons, HAdd.hAdd, HMul.hMul, OfNat.ofNat
Proof uses: Eq.mpr, id, congrArg, rfl, Usa2026P2.innerSum, Usa2026P2.S_cons_cons, Usa2026P2.innerSum_cons, Eq.refl
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem S_cons_cons_append (p₁ p₂ : ℕ) (p'' l : List ℕ) (h : p'' ++ l ≠ []) :
    S ((p₁ :: p₂ :: p'') ++ l) = 2 * p₁ + (S ((p₂ :: p'') ++ l) + 2 * p₂) := by
…
```
Mentions: h, Usa2026P2.S
theorem Usa2026P2.S_append Documented declaration: S_append line 158 source
Source documentation
The overlap identity: if a row is decomposed as p ++ x :: q with both p and q nonempty (so x is a middle entry, counted with coefficient 4), then its S-value is the sum of the S-values of the overlapping parts p ++ [x] and x :: q.

standard axioms: propext what this means
Statement uses: List, Nat, Ne, List.nil, Eq, Usa2026P2.S, HAppend.hAppend, List.cons, HAdd.hAdd
10 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
theorem S_append : ∀ (p q : List ℕ) (x : ℕ), p ≠ [] → q ≠ [] →
    S (p ++ x :: q) = S (p ++ [x]) + S (x :: q)
  | [], _, _, h, _ => (h rfl).elim
  | [p₁], q, x, _, hq => by
      obtain ⟨q₁, q', rfl⟩ := List.exists_cons_of_ne_nil hq
…
```
Mentions: Usa2026P2.S, h
theorem Usa2026P2.exists_split The key combinatorial step: any row with at least two entries can be cut into a nonempty prefix and a nonempty suffix whose S-values are both at most S a / 2 line 174 source
Source documentation
The key combinatorial step: any row with at least two entries can be cut into a nonempty prefix and a nonempty suffix whose S-values are both at most S a / 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, LE.le, OfNat.ofNat, List.length, Exists, And, LT.lt, HMul.hMul, Usa2026P2.S, List.take, List.drop
Proof uses: Ne, List.nil, Eq, False, False.elim, Eq.mp, Eq.trans, Eq.symm, List.cons, List.exists_cons_of_ne_nil, congrArg, zero_add, rfl, Eq.mpr, id, Usa2026P2.S_singleton, HAdd.hAdd, Usa2026P2.innerSum, Usa2026P2.S_cons_cons, Nat.le_add_right and 27 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 41 steps
Open to load the checked before-and-after goal states.
```
theorem exists_split (a : List ℕ) (ha : 2 ≤ a.length) :
    ∃ k, 1 ≤ k ∧ k < a.length ∧ 2 * S (a.take k) ≤ S a ∧ 2 * S (a.drop k) ≤ S a := by
…
```
Mentions: Usa2026P2.S
inductive Usa2026P2.Reduces Reduces a m means that the row a can be reduced to the single number m by a sequence of legal moves line 226 source
Source documentation
Reduces a m means that the row a can be reduced to the single number m by a sequence of legal moves. A derivation is a full binary tree whose leaves are the entries of a and whose internal nodes are powers of two larger than their children; conversely any play of the game produces such a tree (the last move combines the reductions of two complementary blocks), so Reduces a m holds exactly when Annie can achieve the final number m.

standard axioms: propext what this means
Statement uses: List, Nat
```
inductive Reduces : List ℕ → ℕ → Prop
  | base (x : ℕ) : Reduces [x] x
  | append (u v : List ℕ) (x y z : ℕ) (hu : Reduces u x) (hv : Reduces v y)
      (hz : IsPow2 z) (hx : x < z) (hy : y < z) : Reduces (u ++ v) z

/-- A number reachable from a row of powers of two is again a power of two. -/
```
Mentions: base, Usa2026P2.IsPow2
theorem Usa2026P2.reduces_isPow2 A number reachable from a row of powers of two is again a power of two line 232 source
Source documentation
A number reachable from a row of powers of two is again a power of two.

standard axioms: propext what this means
Statement uses: List, Nat, Usa2026P2.Reduces, Membership.mem, Usa2026P2.IsPow2
Proof uses: Usa2026P2.Reduces.rec, List.cons, List.nil, List.mem_singleton_self, LT.lt, HAppend.hAppend
5 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem reduces_isPow2 {l : List ℕ} {m : ℕ} (h : Reduces l m)
    (hp : ∀ x ∈ l, IsPow2 x) : IsPow2 m := by
…
```
Mentions: h, Usa2026P2.Reduces, Usa2026P2.IsPow2
theorem Usa2026P2.exists_reduces_le The main induction: every nonempty row of powers of two can be reduced to a single number which is at most S of the row line 240 source
Source documentation
The main induction: every nonempty row of powers of two can be reduced to a single number which is at most S of the row.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List, Eq, List.length, Ne, List.nil, Membership.mem, Usa2026P2.IsPow2, Exists, And, Usa2026P2.Reduces, LE.le, Usa2026P2.S
Proof uses: Nat.strong_induction_on, LT.lt, False.elim, rfl, List.cons, Exists.intro, And.intro, Usa2026P2.Reduces.base, le_of_eq, Eq.symm, Usa2026P2.S_singleton, OfNat.ofNat, of_eq_true, HAdd.hAdd, Eq.trans, True, Function.swap, HMul.hMul, List.take, List.drop and 60 more
97 instances, coercions and auxiliary constants left out.

Tactic trace: 68 steps
Open to load the checked before-and-after goal states.
```
theorem exists_reduces_le :
    ∀ n : ℕ, ∀ a : List ℕ, a.length = n → a ≠ [] → (∀ x ∈ a, IsPow2 x) →
      ∃ m, Reduces a m ∧ m ≤ S a := by
…
```
Mentions: Usa2026P2.IsPow2, Usa2026P2.Reduces, Usa2026P2.S
theorem Usa2026P2.Move.append_right Moves can also be performed with an additional row appended on the right line 293 source
Source documentation
Moves can also be performed with an additional row appended on the right.

standard axioms: propext what this means
Statement uses: List, Nat, Usa2026P2.Move, HAppend.hAppend
Proof uses: Eq, HEq, Usa2026P2.IsPow2, LT.lt, List.cons, Usa2026P2.Move.mk, Eq.mpr, id, congrArg, of_eq_true, Eq.trans, True, congrFun', List.append_assoc, eq_self, Eq.symm, Eq.refl, HEq.refl
7 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem Move.append_right {a b : List ℕ} (h : Move a b) (r : List ℕ) :
    Move (a ++ r) (b ++ r) := by
…
```
Mentions: h, Usa2026P2.Move
theorem Usa2026P2.Move.append_left Moves can also be performed with an additional row appended on the left line 301 source
Source documentation
Moves can also be performed with an additional row appended on the left.

standard axioms: propext what this means
Statement uses: List, Nat, Usa2026P2.Move, HAppend.hAppend
Proof uses: Eq, HEq, Usa2026P2.IsPow2, LT.lt, List.cons, Usa2026P2.Move.mk, Eq.mpr, id, congrArg, of_eq_true, Eq.trans, True, List.append_assoc, eq_self, Eq.symm, Eq.refl, HEq.refl
7 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem Move.append_left (l : List ℕ) {a b : List ℕ} (h : Move a b) :
    Move (l ++ a) (l ++ b) := by
…
```
Mentions: h, Usa2026P2.Move
theorem Usa2026P2.reflTransGen_map Pushing a chain of moves through a context map line 309 source
Source documentation
Pushing a chain of moves through a context map.

standard axioms: propext what this means
Statement uses: List, Nat, Usa2026P2.Move, Relation.ReflTransGen
Proof uses: Relation.ReflTransGen.rec, Relation.ReflTransGen.refl, Relation.ReflTransGen.trans, Relation.ReflTransGen.single

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem reflTransGen_map (f : List ℕ → List ℕ)
    (hf : ∀ {s t : List ℕ}, Move s t → Move (f s) (f t)) {a b : List ℕ}
    (h : Relation.ReflTransGen Move a b) : Relation.ReflTransGen Move (f a) (f b) := by
…
```
Mentions: f, Usa2026P2.Move, h
theorem Usa2026P2.reduces_moves A Reduces derivation yields an actual sequence of legal moves: reduce the left block, then the right block, then combine the two remaining adjacent numbers line 318 source
Source documentation
A Reduces derivation yields an actual sequence of legal moves: reduce the left block, then the right block, then combine the two remaining adjacent numbers.

standard axioms: propext what this means
Statement uses: List, Nat, Usa2026P2.Reduces, Relation.ReflTransGen, Usa2026P2.Move, List.cons, List.nil
Proof uses: Usa2026P2.Reduces.rec, Relation.ReflTransGen.refl, Usa2026P2.IsPow2, LT.lt, HAppend.hAppend, Usa2026P2.reflTransGen_map, Usa2026P2.Move.append_right, Usa2026P2.Move.append_left, Relation.ReflTransGen.single, Usa2026P2.Move.mk, Relation.ReflTransGen.trans
3 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem reduces_moves {a : List ℕ} {m : ℕ} (h : Reduces a m) :
    Relation.ReflTransGen Move a [m] := by
…
```
Mentions: h, Usa2026P2.Reduces, Usa2026P2.Move
theorem Usa2026P2.IsPow2.pos Powers of two are positive line 332 source
Source documentation
Powers of two are positive.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2026P2.IsPow2, LT.lt, OfNat.ofNat
Proof uses: Eq, HPow.hPow, pow_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Nat.ble, Eq.symm
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem IsPow2.pos {x : ℕ} (h : IsPow2 x) : 0 < x := by
…
```
Mentions: h, Usa2026P2.IsPow2
problem Usa2026P2.usa2026_p2 The answer is yes: from any starting row of powers of two, Annie can always reach a single number which is less than four times the sum of the starting row line 340 source
Source documentation
The answer is yes: from any starting row of powers of two, Annie can always reach a single number which is less than four times the sum of the starting row.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, Ne, List.nil, Membership.mem, Usa2026P2.IsPow2, Exists, And, Relation.ReflTransGen, Usa2026P2.Move, List.cons, LT.lt, HMul.hMul, OfNat.ofNat, List.sum
Proof uses: Usa2026P2.Reduces, LE.le, Usa2026P2.S, Usa2026P2.exists_reduces_le, List.length, rfl, Usa2026P2.IsPow2.pos, Exists.intro, And.intro, Usa2026P2.reduces_moves, lt_of_le_of_lt, Usa2026P2.S_lt_four_mul_sum
20 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
problem usa2026_p2 (a : List ℕ) (ha : a ≠ []) (hp : ∀ x ∈ a, IsPow2 x) :
    ∃ m, Relation.ReflTransGen Move a [m] ∧ m < 4 * a.sum := by
…
```
Mentions: Usa2026P2.IsPow2, Usa2026P2.Move