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

87 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2013, Problem 3

Let n be a positive integer. There are n(n+1)/2 tokens, each with a black side and a white side, arranged into an equilateral triangle, with the biggest row containing n tokens. Initially, each token has the white side up. An operation is to choose a line parallel to the sides of the triangle, and flip all the tokens on that line. A configuration is called admissible if it can be obtained from the initial configuration by performing a finite number of operations. For each admissible configuration C, let f(C) denote the smallest number of operations required to obtain C from the initial configuration. Find the maximum value of f(C), where C varies over all admissible configurations.

Imports (7)

Imported by 1 file

Compfiles.lean

def Usa2013P3.Token The tokens are indexed by pairs (a, b) of natural numbers with a + b < n line 43 source
Source documentation
The tokens are indexed by pairs (a, b) of natural numbers with a + b < n. One should think of barycentric coordinates (a, b, c) with a + b + c = n - 1, so that c = n - 1 - a - b is determined.

no axioms what this means
Statement uses: Nat
Proof uses: Subtype, Prod, LT.lt, HAdd.hAdd, Prod.fst, Prod.snd
3 instances, coercions and auxiliary constants left out.
```
def Token (n : ℕ) := { p : ℕ × ℕ // p.1 + p.2 < n }
```
lemma Usa2013P3.lt_left line 45 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HAdd.hAdd
7 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.lt_right line 46 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HAdd.hAdd
7 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.lt_third line 47 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HAdd.hAdd, HSub.hSub, OfNat.ofNat
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
structure Usa2013P3.Moves A choice of lines to flip: for each of the three directions and each i < n, whether the i-th line in that direction is flipped line 54 source
Source documentation
A choice of lines to flip: for each of the three directions and each i < n, whether the i-th line in that direction is flipped. The three lines through the token (a, b, c) are the a-th, b-th and c-th lines of the three directions respectively.

no axioms what this means
Statement uses: Nat
```
structure Moves (n : ℕ) where
…
```
def Usa2013P3.applyMoves Documented declaration: applyMoves line 62 source
Source documentation
The configuration reached from the initial (all-white) configuration by performing the moves v: token (a, b) ends up black iff an odd number of the three lines through it were flipped.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2013P3.Moves, Usa2013P3.Token, Bool
Proof uses: Bool.xor, Usa2013P3.Moves.x, Fin.mk, Prod.fst, Prod, LT.lt, HAdd.hAdd, Prod.snd, Usa2013P3.Moves.y, Usa2013P3.Moves.z, HSub.hSub, OfNat.ofNat
10 instances, coercions and auxiliary constants left out.
```
def applyMoves {n : ℕ} (v : Moves n) (t : Token n) : Bool :=
…
```
Mentions: Usa2013P3.Moves, Usa2013P3.Token
def Usa2013P3.Admissible A configuration is admissible if it can be obtained from the initial configuration by a finite number of operations line 70 source
Source documentation
A configuration is admissible if it can be obtained from the initial configuration by a finite number of operations. Since the operations commute and are involutions, every sequence of operations is described by a Moves.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2013P3.Token, Bool
Proof uses: Exists, Usa2013P3.Moves, Eq, Usa2013P3.applyMoves
```
def Admissible {n : ℕ} (C : Token n → Bool) : Prop := ∃ v : Moves n, applyMoves v = C
```
Mentions: Usa2013P3.Token, Usa2013P3.Moves, Usa2013P3.applyMoves
def Usa2013P3.weight The number of operations in a Moves: the total number of flipped lines line 73 source
Source documentation
The number of operations in a Moves: the total number of flipped lines.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2013P3.Moves
Proof uses: HAdd.hAdd, Finset.card, Fin, Finset.filter, Eq, Bool, Usa2013P3.Moves.x, Bool.true, Finset.univ, Usa2013P3.Moves.y, Usa2013P3.Moves.z
4 instances, coercions and auxiliary constants left out.
```
def weight {n : ℕ} (v : Moves n) : ℕ :=
…
```
Mentions: Usa2013P3.Moves
def Usa2013P3.f f C is the smallest number of operations required to obtain C line 79 source
Source documentation
f C is the smallest number of operations required to obtain C.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2013P3.Token, Bool
Proof uses: InfSet.sInf, Set.ofPred, Exists, Usa2013P3.Moves, And, Eq, Usa2013P3.applyMoves, Usa2013P3.weight
1 instances, coercions and auxiliary constants left out.
```
noncomputable def f {n : ℕ} (C : Token n → Bool) : ℕ :=
…
```
Mentions: Usa2013P3.Token
determine Usa2013P3.answer line 82 source
no axioms what this means
Statement uses: Nat
Proof uses: HAdd.hAdd, HMul.hMul, OfNat.ofNat, HDiv.hDiv, HMod.hMod
9 instances, coercions and auxiliary constants left out.
def Usa2013P3.Moves.vxor Pointwise xor of two Moves line 87 source
Source documentation
Pointwise xor of two Moves.

no axioms what this means
Statement uses: Nat, Usa2013P3.Moves
Proof uses: Usa2013P3.Moves.mk, Fin, Bool.xor, Usa2013P3.Moves.x, Usa2013P3.Moves.y, Usa2013P3.Moves.z
```
def Moves.vxor {n : ℕ} (v w : Moves n) : Moves n :=
…
```
Mentions: Usa2013P3.Moves
def Usa2013P3.e The "even-length line" indicator: the i-th line of any direction contains n - i tokens, which is even iff i ≡ n (mod 2) line 92 source
Source documentation
The "even-length line" indicator: the i-th line of any direction contains n - i tokens, which is even iff i ≡ n (mod 2).

no axioms what this means
Statement uses: Nat, Fin, Bool
Proof uses: Decidable.decide, Eq, HMod.hMod, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
```
def e (n : ℕ) : Fin n → Bool := fun i => decide (i.val % 2 = n % 2)
```
def Usa2013P3.sp The element of the move-span indexed by three bits line 97 source
Source documentation
The element of the move-span indexed by three bits. With g₁ = (1,1,0), g₂ = (0,1,1) and θ = (e,e,e), this is ε₁ • g₁ ^^ ε₂ • g₂ ^^ ε₃ • θ.

no axioms what this means
Statement uses: Nat, Prod, Bool, Usa2013P3.Moves
Proof uses: Usa2013P3.Moves.mk, Fin, Bool.xor, Prod.fst, Bool.and, Prod.snd, Usa2013P3.e
```
def sp (n : ℕ) (ε : Bool × Bool × Bool) : Moves n :=
…
```
Mentions: Usa2013P3.Moves
lemma Usa2013P3.xor_eq_false_iff line 102 source
standard axioms: propext what this means
Statement uses: Bool, Iff, Eq, Bool.xor, Bool.false
Proof uses: of_eq_true, Eq.trans, True, congr, congrArg, congrFun', bne_self_eq_false, eq_self, iff_self, Eq.symm, Bool.true, False, bne, Bool.not, Bool.bne_true, Bool.not_false, Bool.true_eq_false, Bool.false_eq_true, Eq.refl, Bool.bne_false
5 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.applyMoves_vxor line 105 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2013P3.Moves, Usa2013P3.Token, Eq, Bool, Usa2013P3.applyMoves, Usa2013P3.Moves.vxor, Bool.xor
Proof uses: Prod, LT.lt, HAdd.hAdd, Prod.fst, Prod.snd, Subtype.mk, Prod.mk, id, of_decide_eq_true, Decidable.decide, Bool.true, Eq.refl, Usa2013P3.Moves.x, Fin.mk, Usa2013P3.Moves.y, Usa2013P3.Moves.z, HSub.hSub, OfNat.ofNat
13 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.theta_aux The key property of θ = (e,e,e): every token lies on an even number of even-length lines line 119 source
Source documentation
The key property of θ = (e,e,e): every token lies on an even number of even-length lines. Indeed, with c = n - 1 - a - b we have a + b + c = n - 1, so among a % 2, b % 2, c % 2 the number of values equal to n % 2 is even.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HAdd.hAdd, Eq, Bool, Bool.xor, Decidable.decide, HMod.hMod, OfNat.ofNat, HSub.hSub, Bool.false
Proof uses: dite, LE.le, False.elim, False, Eq.mp, eq_false, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_natMod, Mathlib.Meta.NormNum.isNat_add, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Eq.symm, le_antisymm, Nat.ge_of_not_lt, Mathlib.Tactic.IntervalCases.of_lt_right, Nat.rawCast, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Not, of_decide_eq_true, id and 2 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma theta_aux (n a b : ℕ) (h : a + b < n) :
    (decide (a % 2 = n % 2) ^^ decide (b % 2 = n % 2) ^^
      decide ((n - 1 - a - b) % 2 = n % 2)) = false := by
…
```
Mentions: h
lemma Usa2013P3.applyMoves_sp Every element of the span acts trivially on configurations line 135 source
Source documentation
Every element of the span acts trivially on configurations.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prod, Bool, Usa2013P3.Token, Eq, Usa2013P3.applyMoves, Usa2013P3.sp, Bool.false
Proof uses: Prod.mk, LT.lt, HAdd.hAdd, Prod.fst, Prod.snd, Subtype.mk, Bool.xor, Decidable.decide, HMod.hMod, OfNat.ofNat, HSub.hSub, Usa2013P3.theta_aux, id, Bool.and, of_eq_true, Eq.trans, True, congrFun', congrArg, congr and 17 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma applyMoves_sp {n : ℕ} (ε : Bool × Bool × Bool) (t : Token n) :
    applyMoves (sp n ε) t = false := by
…
```
Mentions: Usa2013P3.Token, Usa2013P3.applyMoves, Usa2013P3.sp
lemma Usa2013P3.sp_vxor The span elements are closed under xor, componentwise on the bits line 149 source
Source documentation
The span elements are closed under xor, componentwise on the bits.

standard axioms: Quot.sound what this means
Statement uses: Nat, Prod, Bool, Eq, Usa2013P3.Moves, Usa2013P3.Moves.vxor, Usa2013P3.sp, Prod.mk, Bool.xor, Prod.fst, Prod.snd
Proof uses: Usa2013P3.Moves.ext, funext, Fin, Usa2013P3.Moves.x, id, Bool.and, of_decide_eq_true, Decidable.decide, Bool.true, Eq.refl, Usa2013P3.e, Usa2013P3.Moves.y, Usa2013P3.Moves.z
3 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma sp_vxor {n : ℕ} (ε ε' : Bool × Bool × Bool) :
    Moves.vxor (sp n ε) (sp n ε') =
      sp n (ε.1 ^^ ε'.1, ε.2.1 ^^ ε'.2.1, ε.2.2 ^^ ε'.2.2) := by
…
```
Mentions: Usa2013P3.Moves.vxor, Usa2013P3.sp
def Usa2013P3.zeroMove The zero move line 176 source
Source documentation
The zero move.

no axioms what this means
Statement uses: Nat, Usa2013P3.Moves
Proof uses: Usa2013P3.Moves.mk, Fin, Bool.false
```
def zeroMove (n : ℕ) : Moves n := ⟨fun _ => false, fun _ => false, fun _ => false⟩
```
Mentions: Usa2013P3.Moves
lemma Usa2013P3.vxor_self line 178 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Usa2013P3.Moves, Eq, Usa2013P3.Moves.vxor, Usa2013P3.zeroMove
Proof uses: Usa2013P3.Moves.ext, funext, Fin, Bool, Usa2013P3.Moves.x, of_eq_true, Bool.false, Eq.trans, True, congrFun', congrArg, Usa2013P3.Moves.mk, congr, Bool.xor, Usa2013P3.Moves.y, Usa2013P3.Moves.z, bne, bne_self_eq_false, eq_self
3 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.vxor_zero line 181 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Usa2013P3.Moves, Eq, Usa2013P3.Moves.vxor, Usa2013P3.zeroMove
Proof uses: Usa2013P3.Moves.ext, funext, Fin, Bool, Usa2013P3.Moves.x, of_eq_true, Eq.trans, True, congrFun', congrArg, Usa2013P3.Moves.mk, Usa2013P3.Moves.y, Usa2013P3.Moves.z, congr, Bool.xor, bne, Bool.false, Bool.bne_false, eq_self
2 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.vxor_comm line 184 source
standard axioms: Quot.sound what this means
Statement uses: Nat, Usa2013P3.Moves, Eq, Usa2013P3.Moves.vxor
Proof uses: Usa2013P3.Moves.ext, funext, Fin, Bool, Usa2013P3.Moves.x, id, Bool.xor_comm, Usa2013P3.Moves.y, Usa2013P3.Moves.z

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.vxor_assoc line 190 source
standard axioms: Quot.sound what this means
Statement uses: Nat, Usa2013P3.Moves, Eq, Usa2013P3.Moves.vxor
Proof uses: Usa2013P3.Moves.ext, funext, Fin, Bool, Usa2013P3.Moves.x, id, Bool.xor_assoc, Usa2013P3.Moves.y, Usa2013P3.Moves.z

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.vxor_eq_zero line 197 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Usa2013P3.Moves, Eq, Usa2013P3.Moves.vxor, Usa2013P3.zeroMove
Proof uses: Usa2013P3.Moves.ext, funext, Fin, Bool, Usa2013P3.Moves.x, Bool.xor, Bool.false, congrFun, congrArg, Iff.mp, Usa2013P3.xor_eq_false_iff, Usa2013P3.Moves.y, Usa2013P3.Moves.z

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.Count.period_shift line 214 source
lemma Usa2013P3.Count.card_filter_range_four_mul line 221 source
lemma Usa2013P3.Count.card_filter_range_periodic Count of a periodic (period 4) predicate over Finset.range (4 * k + r) line 248 source
Source documentation
Count of a periodic (period 4) predicate over Finset.range (4 * k + r).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Bool, Eq, HAdd.hAdd, OfNat.ofNat, Finset.card, Finset.filter, Bool.true, Finset.range, HMul.hMul
Proof uses: Disjoint, Finset, Finset.map, addLeftEmbedding, Eq.mpr, Membership.mem, Not, id, congrArg, propext, Finset.disjoint_left, LT.lt, Iff.mp, Finset.mem_range, And.left, And, Finset.mem_filter, Function.Embedding, Exists, False and 20 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma card_filter_range_periodic (q : ℕ → Bool) (hq : ∀ i, q (i + 4) = q i) (k r : ℕ) :
    ((Finset.range (4 * k + r)).filter fun i => q i = true).card =
      k * ((Finset.range 4).filter fun i => q i = true).card +
        ((Finset.range r).filter fun i => q i = true).card := by
…
```
lemma Usa2013P3.Count.card_fin_filter Bridge: counting a ℕ-predicate on Fin n vs on Finset.range n line 272 source
Source documentation
Bridge: counting a ℕ-predicate on Fin n vs on Finset.range n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Bool, Eq, Finset.card, Fin, Finset.filter, Bool.true, Finset.univ, Finset.range
Proof uses: Eq.mpr, Finset.sum, ite, OfNat.ofNat, id, congrArg, Finset.card_filter, Fin.sum_univ_eq_sum_range
8 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma card_fin_filter (q : ℕ → Bool) (n : ℕ) :
    (Finset.univ.filter fun i : Fin n => q i.val = true).card =
      ((Finset.range n).filter fun i => q i = true).card := by
…
```
lemma Usa2013P3.Count.count_eval Combined: count of a 4-periodic predicate over Fin (4 * k + r) line 279 source
Source documentation
Combined: count of a 4-periodic predicate over Fin (4 * k + r).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Bool, Eq, HAdd.hAdd, OfNat.ofNat, HMul.hMul, Finset.card, Fin, Finset.filter, Bool.true, Finset.univ, Finset.range
Proof uses: Eq.mpr, id, congrArg, Usa2013P3.Count.card_fin_filter, Usa2013P3.Count.card_filter_range_periodic
16 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma count_eval (P : ℕ → Bool) (hP : ∀ i, P (i + 4) = P i) {n k r : ℕ} (hn : n = 4 * k + r) :
    (Finset.univ.filter fun i : Fin n => P i.val = true).card =
      k * ((Finset.range 4).filter fun i => P i = true).card +
        ((Finset.range r).filter fun i => P i = true).card := by
…
```
Mentions: P
lemma Usa2013P3.Count.card_range_modeq Number of i < n with i % 2 = n % 2 line 287 source
Source documentation
Number of i < n with i % 2 = n % 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Finset.filter, HMod.hMod, OfNat.ofNat, Finset.range, HDiv.hDiv
Proof uses: Nat.twoStepInduction, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, HAdd.hAdd, Not, Membership.mem, Finset, Finset.notMem_range_self, And.left, Iff.mp, And, Finset.mem_filter, Eq.mpr, congrArg, Nat.add_mod_right, Insert.insert and 10 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma card_range_modeq (n : ℕ) :
    ((Finset.range n).filter fun i => i % 2 = n % 2).card = n / 2 := by
…
```
def Usa2013P3.bv Documented declaration: bv line 304 source
Source documentation
The contribution of one direction to the weight of v ^^ sp ε: the number of flipped lines of that direction, as a function of the "full flip" bit δ and the "theta flip" bit τ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool
Proof uses: Finset.card, Finset.filter, Eq, Bool.xor, Bool.and, Usa2013P3.e, Bool.true, Finset.univ
2 instances, coercions and auxiliary constants left out.
```
def bv {n : ℕ} (α : Fin n → Bool) (δ τ : Bool) : ℕ :=
…
```
def Usa2013P3.pon Number of ones of α on odd-length lines line 308 source
Source documentation
Number of ones of α on odd-length lines.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool
Proof uses: Finset.card, Finset.filter, And, Eq, Bool.true, Usa2013P3.e, Bool.false, Finset.univ
3 instances, coercions and auxiliary constants left out.
```
def pon {n : ℕ} (α : Fin n → Bool) : ℕ :=
…
```
def Usa2013P3.qon Number of ones of α on even-length lines line 312 source
Source documentation
Number of ones of α on even-length lines.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool
Proof uses: Finset.card, Finset.filter, And, Eq, Bool.true, Usa2013P3.e, Finset.univ
3 instances, coercions and auxiliary constants left out.
```
def qon {n : ℕ} (α : Fin n → Bool) : ℕ :=
…
```
def Usa2013P3.Ocard Number of odd-length lines in one direction line 316 source
Source documentation
Number of odd-length lines in one direction.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finset.card, Fin, Finset.filter, Eq, Bool, Usa2013P3.e, Bool.false, Finset.univ
2 instances, coercions and auxiliary constants left out.
```
def Ocard (n : ℕ) : ℕ := (Finset.univ.filter fun i => e n i = false).card
```
Mentions: Usa2013P3.e
def Usa2013P3.Ecard Number of even-length lines in one direction line 319 source
Source documentation
Number of even-length lines in one direction.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finset.card, Fin, Finset.filter, Eq, Bool, Usa2013P3.e, Bool.true, Finset.univ
2 instances, coercions and auxiliary constants left out.
```
def Ecard (n : ℕ) : ℕ := (Finset.univ.filter fun i => e n i = true).card
```
Mentions: Usa2013P3.e
lemma Usa2013P3.Ecard_eq line 321 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Usa2013P3.Ecard, HDiv.hDiv, OfNat.ofNat
Proof uses: Finset.card, Fin, Finset.filter, Bool, Decidable.decide, HMod.hMod, Bool.true, Finset.univ, Finset.range, Usa2013P3.Count.card_fin_filter, Usa2013P3.e, congrArg, Finset, Finset.filter_congr, Membership.mem, of_eq_true, Iff, Eq.trans, True, congr and 7 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.OE_sum line 334 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HAdd.hAdd, Usa2013P3.Ocard, Usa2013P3.Ecard
Proof uses: Eq.mpr, Finset.card, Fin, Finset.filter, Bool, Usa2013P3.e, Bool.false, Finset.univ, id, congrArg, Usa2013P3.Ocard.eq_1, Bool.true, Usa2013P3.Ecard.eq_1, Not, Finset, Finset.filter_congr, Membership.mem, Iff, of_eq_true, Eq.trans and 16 more
11 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.pon_le line 341 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, LE.le, Usa2013P3.pon, Usa2013P3.Ocard
Proof uses: Finset.card_le_card, Finset.filter, And, Eq, Bool.true, Usa2013P3.e, Bool.false, Finset.univ, Membership.mem, Finset, Eq.mpr, id, And.intro, Finset.mem_univ, And.right, Eq.mp
7 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.qon_le line 347 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, LE.le, Usa2013P3.qon, Usa2013P3.Ecard
Proof uses: Finset.card_le_card, Finset.filter, And, Eq, Bool.true, Usa2013P3.e, Finset.univ, Membership.mem, Finset, Eq.mpr, id, And.intro, Finset.mem_univ, And.right, Eq.mp
7 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.card_e_true Counting ones of α ^^ c on the even-length lines line 354 source
Source documentation
Counting ones of α ^^ c on the even-length lines.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Finset.card, Finset.filter, Bool.xor, Bool.true, Usa2013P3.e, Finset.univ, cond, HSub.hSub, Usa2013P3.Ecard, Usa2013P3.qon
Proof uses: Bool.false, id, Eq.mpr, congrArg, Finset, Finset.filter_congr, Membership.mem, of_eq_true, Iff, Eq.trans, True, congrFun', Bool.bne_false, iff_self, And, Finset.filter_filter, and_comm, Eq.refl, Eq.symm, congr and 18 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
```
lemma card_e_true {n : ℕ} (α : Fin n → Bool) (c : Bool) :
    ((Finset.univ.filter fun i => e n i = true).filter fun i => (α i ^^ c) = true).card =
      cond c (Ecard n - qon α) (qon α) := by
…
```
Mentions: Usa2013P3.e, Usa2013P3.Ecard, Usa2013P3.qon
lemma Usa2013P3.card_e_false Counting ones of α ^^ c on the odd-length lines line 386 source
Source documentation
Counting ones of α ^^ c on the odd-length lines.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Finset.card, Finset.filter, Bool.xor, Bool.true, Usa2013P3.e, Bool.false, Finset.univ, cond, HSub.hSub, Usa2013P3.Ocard, Usa2013P3.pon
Proof uses: id, Eq.mpr, congrArg, Finset, Finset.filter_congr, Membership.mem, of_eq_true, Iff, Eq.trans, True, congrFun', Bool.bne_false, iff_self, And, Finset.filter_filter, and_comm, Eq.refl, Eq.symm, congr, bne and 17 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
```
lemma card_e_false {n : ℕ} (α : Fin n → Bool) (c : Bool) :
    ((Finset.univ.filter fun i => e n i = false).filter fun i => (α i ^^ c) = true).card =
      cond c (Ocard n - pon α) (pon α) := by
…
```
Mentions: Usa2013P3.e, Usa2013P3.Ocard, Usa2013P3.pon
lemma Usa2013P3.bv_eq Master formula for the block values line 418 source
Source documentation
Master formula for the block values.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Usa2013P3.bv, HAdd.hAdd, cond, Bool.xor, HSub.hSub, Usa2013P3.Ecard, Usa2013P3.qon, Usa2013P3.Ocard, Usa2013P3.pon
Proof uses: Finset, Finset.filter, Bool.and, Usa2013P3.e, Bool.true, Finset.univ, Union.union, And, Bool.false, Finset.ext, Eq.mpr, Iff, Membership.mem, Or, id, congr, congrArg, Eq.trans, True, congrFun' and 35 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
```
lemma bv_eq {n : ℕ} (α : Fin n → Bool) (δ τ : Bool) :
    bv α δ τ = cond (δ ^^ τ) (Ecard n - qon α) (qon α) +
      cond δ (Ocard n - pon α) (pon α) := by
…
```
Mentions: Usa2013P3.bv, Usa2013P3.Ecard, Usa2013P3.qon, Usa2013P3.Ocard, Usa2013P3.pon
lemma Usa2013P3.bv_ff The four block values line 462 source
Source documentation
The four block values.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Usa2013P3.bv, Bool.false, HAdd.hAdd, Usa2013P3.pon, Usa2013P3.qon
Proof uses: Eq.mpr, cond, Bool.xor, HSub.hSub, Usa2013P3.Ecard, Usa2013P3.Ocard, id, congrArg, Usa2013P3.bv_eq, congrFun', congr, Eq.trans, ite, Bool.true, bne_self_eq_false, Bool.cond_eq_ite, ite_eq_right_of_eq_false, Bool.false_eq_true
10 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma bv_ff {n : ℕ} (α : Fin n → Bool) : bv α false false = pon α + qon α := by
…
```
Mentions: Usa2013P3.bv, Usa2013P3.pon, Usa2013P3.qon
lemma Usa2013P3.bv_tf line 467 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Usa2013P3.bv, Bool.true, Bool.false, HAdd.hAdd, HSub.hSub, Usa2013P3.Ocard, Usa2013P3.pon, Usa2013P3.Ecard, Usa2013P3.qon
Proof uses: Eq.mpr, cond, Bool.xor, id, congrArg, Usa2013P3.bv_eq, congrFun', congr, Eq.trans, ite, Bool.bne_false, Bool.cond_eq_ite, ite_eq_left_of_eq_true, eq_self
10 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.bv_ft line 473 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Usa2013P3.bv, Bool.false, Bool.true, HAdd.hAdd, Usa2013P3.pon, HSub.hSub, Usa2013P3.Ecard, Usa2013P3.qon
Proof uses: Eq.mpr, cond, Bool.xor, Usa2013P3.Ocard, id, congrArg, Usa2013P3.bv_eq, congrFun', congr, Eq.trans, ite, bne, Bool.not, Bool.bne_true, Bool.not_false, Bool.cond_eq_ite, ite_eq_left_of_eq_true, eq_self, ite_eq_right_of_eq_false, Bool.false_eq_true
11 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.bv_tt line 479 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Usa2013P3.bv, Bool.true, HAdd.hAdd, HSub.hSub, Usa2013P3.Ocard, Usa2013P3.pon, Usa2013P3.qon
Proof uses: Eq.mpr, cond, Bool.xor, Usa2013P3.Ecard, id, congrArg, Usa2013P3.bv_eq, congrFun', congr, Eq.trans, ite, Bool.false, bne_self_eq_false, Bool.cond_eq_ite, ite_eq_right_of_eq_false, Bool.false_eq_true, ite_eq_left_of_eq_true, eq_self
12 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.pair_id Pair identity: the two values obtained by flipping a whole direction sum to n line 487 source
Source documentation
Pair identity: the two values obtained by flipping a whole direction sum to n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, HAdd.hAdd, Usa2013P3.bv, Bool.false, Bool.true
Proof uses: Eq.mpr, cond, Bool.xor, HSub.hSub, Usa2013P3.Ecard, Usa2013P3.qon, Usa2013P3.Ocard, Usa2013P3.pon, id, congrArg, Usa2013P3.bv_eq, LE.le, Usa2013P3.pon_le, Usa2013P3.qon_le, Usa2013P3.OE_sum, congrFun', congr, Eq.trans, ite, bne_self_eq_false and 12 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma pair_id {n : ℕ} (α : Fin n → Bool) (τ : Bool) :
    bv α false τ + bv α true τ = n := by
…
```
Mentions: Usa2013P3.bv
lemma Usa2013P3.weight_vxor_sp The weight of a coset element splits into the three block values line 495 source
Source documentation
The weight of a coset element splits into the three block values.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2013P3.Moves, Bool, Eq, Usa2013P3.weight, Usa2013P3.Moves.vxor, Usa2013P3.sp, Prod.mk, Prod, HAdd.hAdd, Usa2013P3.bv, Usa2013P3.Moves.x, Usa2013P3.Moves.y, Bool.xor, Usa2013P3.Moves.z
Proof uses: of_eq_true, Eq.trans, Finset.card, Fin, Finset.filter, Bool.and, Usa2013P3.e, Bool.true, Finset.univ, True, congr, congrArg, Finset, Finset.filter_congr, Membership.mem, Iff.of_eq, congrFun', Usa2013P3.Moves.mk, funext, Prod.fst and 3 more
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma weight_vxor_sp {n : ℕ} (v : Moves n) (ε1 ε2 ε3 : Bool) :
    weight (Moves.vxor v (sp n (ε1, ε2, ε3))) =
      bv v.x ε1 ε3 + bv v.y (ε1 ^^ ε2) ε3 + bv v.z ε2 ε3 := by
…
```
Mentions: Usa2013P3.Moves, Usa2013P3.weight, Usa2013P3.Moves.vxor, Usa2013P3.sp, Usa2013P3.bv
lemma Usa2013P3.sum_weights The weights of the eight coset elements sum to 12n line 501 source
Source documentation
The weights of the eight coset elements sum to 12n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2013P3.Moves, Eq, HAdd.hAdd, Usa2013P3.weight, Usa2013P3.Moves.vxor, Usa2013P3.sp, Prod.mk, Bool, Prod, Bool.false, Bool.true, HMul.hMul, OfNat.ofNat
Proof uses: Eq.mpr, Usa2013P3.bv, Usa2013P3.Moves.x, Usa2013P3.Moves.y, Bool.xor, Usa2013P3.Moves.z, id, congrFun', congrArg, congr, Usa2013P3.weight_vxor_sp, Usa2013P3.pair_id, Bool.xor_false, Eq.trans, Bool.not, Bool.xor_true, Bool.not_false, Bool.not_true
11 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma sum_weights {n : ℕ} (v : Moves n) :
    weight (Moves.vxor v (sp n (false, false, false))) +
    weight (Moves.vxor v (sp n (false, false, true))) +
    weight (Moves.vxor v (sp n (false, true, false))) +
    weight (Moves.vxor v (sp n (false, true, true))) +
    weight (Moves.vxor v (sp n (true, false, false))) +
    weight (Moves.vxor v (sp n (true, false, true))) +
    weight (Moves.vxor v (sp n (true, true, false))) +
    weight (Moves.vxor v (sp n (true, true, true))) = 12 * n := by
…
```
Mentions: Usa2013P3.Moves, Usa2013P3.weight, Usa2013P3.Moves.vxor, Usa2013P3.sp
lemma Usa2013P3.pair_weight line 519 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2013P3.Moves, Bool, Eq, HAdd.hAdd, Usa2013P3.weight, Usa2013P3.Moves.vxor, Usa2013P3.sp, Prod.mk, Prod, Bool.false, Bool.true, HMul.hMul, OfNat.ofNat, Usa2013P3.bv, Usa2013P3.Moves.x
Proof uses: Usa2013P3.Moves.y, Usa2013P3.pair_id, Usa2013P3.Moves.z, Eq.mpr, Bool.xor, id, congrArg, Usa2013P3.weight_vxor_sp, congrFun', congr, Bool.false_xor, Eq.symm, Bool.xor_false, Eq.trans, Bool.not, Bool.xor_true, Bool.not_true, Eq.refl
14 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.pair_weight_y Pairing to isolate the y-block line 532 source
Source documentation
Pairing to isolate the y-block.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2013P3.Moves, Bool, Eq, HAdd.hAdd, Usa2013P3.weight, Usa2013P3.Moves.vxor, Usa2013P3.sp, Prod.mk, Prod, Bool.false, Bool.true, Bool.not, HMul.hMul, OfNat.ofNat, Usa2013P3.bv, Usa2013P3.Moves.y
Proof uses: Usa2013P3.Moves.x, Usa2013P3.pair_id, Usa2013P3.Moves.z, Eq.mpr, Bool.xor, id, congrArg, Usa2013P3.weight_vxor_sp, congrFun', congr, bne_self_eq_false, Eq.trans, Bool.not_false, Eq.symm, bne, Bool.bne_true, Bool.not_true, Bool.bne_false, Eq.refl
17 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma pair_weight_y {n : ℕ} (v : Moves n) (ε2 τ : Bool) :
    weight (Moves.vxor v (sp n (false, ε2, τ))) +
      weight (Moves.vxor v (sp n (true, !ε2, τ))) = 2 * bv v.y ε2 τ + 2 * n := by
…
```
Mentions: Usa2013P3.Moves, Usa2013P3.weight, Usa2013P3.Moves.vxor, Usa2013P3.sp, Usa2013P3.bv
lemma Usa2013P3.pair_weight_z Pairing to isolate the z-block line 541 source
Source documentation
Pairing to isolate the z-block.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2013P3.Moves, Bool, Eq, HAdd.hAdd, Usa2013P3.weight, Usa2013P3.Moves.vxor, Usa2013P3.sp, Prod.mk, Prod, Bool.false, Bool.true, HMul.hMul, OfNat.ofNat, Usa2013P3.bv, Usa2013P3.Moves.z
Proof uses: Usa2013P3.Moves.x, Usa2013P3.pair_id, Usa2013P3.Moves.y, Eq.mpr, Bool.xor, id, congrArg, Usa2013P3.weight_vxor_sp, congrFun', congr, bne_self_eq_false, Bool.bne_false, Eq.symm, Eq.trans, bne, Bool.not, Bool.bne_true, Bool.not_false, Eq.refl
17 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma pair_weight_z {n : ℕ} (v : Moves n) (ε2 τ : Bool) :
    weight (Moves.vxor v (sp n (false, ε2, τ))) +
      weight (Moves.vxor v (sp n (true, ε2, τ))) = 2 * bv v.z ε2 τ + 2 * n := by
…
```
Mentions: Usa2013P3.Moves, Usa2013P3.weight, Usa2013P3.Moves.vxor, Usa2013P3.sp, Usa2013P3.bv
lemma Usa2013P3.graph_of Documented declaration: graph_of line 552 source
Source documentation
In the case n = 4k + 3, if all eight coset weights are at least 6k+4, then for each block the two values where the block contributes 2k+1 form the graph of δ ↦ τ ⊕ c for some bit c.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, Usa2013P3.Ocard, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Usa2013P3.Ecard, And, LE.le, Usa2013P3.bv, Exists, Iff, Bool.xor
Proof uses: Bool.false, Bool.true, Usa2013P3.qon, Eq.mpr, Usa2013P3.pon, id, congrArg, Usa2013P3.bv_ff, HSub.hSub, Usa2013P3.bv_tt, Usa2013P3.pon_le, Usa2013P3.bv_ft, Usa2013P3.qon_le, Usa2013P3.pair_id, dite, Exists.intro, of_eq_true, Eq.trans, True, congr and 19 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 45 steps
Open to load the checked before-and-after goal states.
```
lemma graph_of {n : ℕ} (α : Fin n → Bool) (k : ℕ)
    (hO : Ocard n = 2 * k + 2) (hE : Ecard n = 2 * k + 1)
    (hb : ∀ δ τ : Bool, 2 * k + 1 ≤ bv α δ τ ∧ bv α δ τ ≤ 2 * k + 2) :
    ∃ c : Bool, ∀ δ τ : Bool, (bv α δ τ = 2 * k + 1) ↔ ((δ ^^ τ) = c) := by
…
```
Mentions: Usa2013P3.Ocard, Usa2013P3.Ecard, Usa2013P3.bv
lemma Usa2013P3.upper_bound The upper bound: every coset contains an element of weight at most 6 * (n / 4) + n % 4 line 592 source
Source documentation
The upper bound: every coset contains an element of weight at most 6 * (n / 4) + n % 4. The proof averages the eight coset weights (their sum is always 12n), with a parity refinement when n % 4 ∈ {2, 3}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2013P3.Moves, Exists, Prod, Bool, LE.le, Usa2013P3.weight, Usa2013P3.Moves.vxor, Usa2013P3.sp, Usa2013P3.answer
Proof uses: Decidable.byContradiction, Not, Eq, HAdd.hAdd, Prod.mk, Bool.false, Bool.true, HMul.hMul, OfNat.ofNat, Usa2013P3.sum_weights, And, LT.lt, False, Exists.intro, HDiv.hDiv, HMod.hMod, And.intro, Eq.mp, Eq.trans, binderNameHint and 56 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 135 steps
Open to load the checked before-and-after goal states.
```
lemma upper_bound {n : ℕ} (v : Moves n) :
    ∃ ε : Bool × Bool × Bool, weight (Moves.vxor v (sp n ε)) ≤ answer n := by
…
```
Mentions: Usa2013P3.Moves, Usa2013P3.weight, Usa2013P3.Moves.vxor, Usa2013P3.sp, Usa2013P3.answer
lemma Usa2013P3.lt_n2 Proof-producing helpers for token indices (kept as term-mode applications so that indices are syntactically reproducible) line 696 source
Source documentation
Proof-producing helpers for token indices (kept as term-mode applications so that indices are syntactically reproducible).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, HSub.hSub
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma lt_n2 {n : ℕ} (hn : 2 ≤ n) : n - 2 < n := by lia
```
lemma Usa2013P3.lt_n1 line 697 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, HSub.hSub
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.lt_n1j line 698 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HSub.hSub, OfNat.ofNat
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.lt_n2m line 699 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HAdd.hAdd, OfNat.ofNat, HSub.hSub
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.tp_y line 700 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HAdd.hAdd, HSub.hSub, OfNat.ofNat
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.tp_z line 701 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HAdd.hAdd, HSub.hSub, OfNat.ofNat
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.tp_y1 line 702 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, HAdd.hAdd, HSub.hSub
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.tp_last line 703 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, HAdd.hAdd, HSub.hSub
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.convFin Converting between Fin n indices with equal values line 706 source
Source documentation
Converting between Fin n indices with equal values.

no axioms what this means
Statement uses: Nat, Fin, Bool, LT.lt, Eq, Fin.mk
Proof uses: Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma convFin {n : ℕ} (f : Fin n → Bool) (a b : ℕ) (ha : a < n) (hb : b < n)
    (hab : a = b) : f ⟨a, ha⟩ = f ⟨b, hb⟩ := by
…
```
Mentions: Usa2013P3.f
lemma Usa2013P3.kernel_of_reduction Documented declaration: kernel_of_reduction line 715 source
Source documentation
The main reduction: if v acts trivially on all tokens and S is a span element that agrees with v on the three "boundary" lines (the length-n y-line, the length-n z-line and the length-2 x-line), then v = S. This is the propagation step of the kernel classification.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, Usa2013P3.Moves, Eq, Usa2013P3.Token, Bool, Usa2013P3.applyMoves, Bool.false, Usa2013P3.Moves.y, Fin.mk, Usa2013P3.Moves.z, Usa2013P3.Moves.x, HSub.hSub, Usa2013P3.lt_n2
Proof uses: Usa2013P3.Moves.vxor, rfl, funext, Eq.mpr, Bool.xor, id, congrArg, Usa2013P3.applyMoves_vxor, of_eq_true, Eq.trans, True, congrFun', congr, congrFun, bne_self_eq_false, eq_self, HAdd.hAdd, Usa2013P3.lt_left, Usa2013P3.lt_right, Usa2013P3.lt_third and 29 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 106 steps
Open to load the checked before-and-after goal states.
```
lemma kernel_of_reduction {n : ℕ} (hn : 0 < n) (hn2 : 2 ≤ n) (v S : Moves n)
    (hv : applyMoves v = fun _ => false)
    (hS : applyMoves S = fun _ => false)
    (hy : S.y ⟨0, hn⟩ = v.y ⟨0, hn⟩)
    (hz : S.z ⟨0, hn⟩ = v.z ⟨0, hn⟩)
    (hx : S.x ⟨n - 2, lt_n2 hn2⟩ = v.x ⟨n - 2, lt_n2 hn2⟩) :
    v = S := by
…
```
Mentions: S, Usa2013P3.Moves, Usa2013P3.applyMoves, Usa2013P3.lt_n2
lemma Usa2013P3.kernel_eq_span The kernel classification: a move that flips every token an even number of times is one of the eight span elements line 827 source
Source documentation
The kernel classification: a move that flips every token an even number of times is one of the eight span elements.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Usa2013P3.Moves, Eq, Usa2013P3.Token, Bool, Usa2013P3.applyMoves, Bool.false, Exists, Prod, Usa2013P3.sp
Proof uses: LE.le, Or, Fin, Fin.mk, rfl, Bool.xor, Usa2013P3.Moves.x, Usa2013P3.Moves.y, Usa2013P3.Moves.z, HAdd.hAdd, congrFun, Subtype.mk, Prod.fst, Prod.snd, Prod.mk, funext, congrArg, Subsingleton.elim, Exists.intro, Usa2013P3.Moves.ext and 44 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 120 steps
Open to load the checked before-and-after goal states.
```
lemma kernel_eq_span {n : ℕ} (hn : 0 < n) {v : Moves n}
    (hv : applyMoves v = fun _ => false) : ∃ ε : Bool × Bool × Bool, v = sp n ε := by
…
```
Mentions: Usa2013P3.Moves, Usa2013P3.applyMoves, Usa2013P3.sp
def Usa2013P3.P12 The four line-flipping patterns used for the extremal configuration: flip the lines whose index is 1 or 2 modulo 4 line 908 source
Source documentation
The four line-flipping patterns used for the extremal configuration: flip the lines whose index is 1 or 2 modulo 4.

no axioms what this means
Statement uses: Nat, Bool
Proof uses: Decidable.decide, Or, Eq, HMod.hMod, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
```
def P12 : ℕ → Bool := fun i => decide (i % 4 = 1 ∨ i % 4 = 2)
```
def Usa2013P3.P03 Indices 0 or 3 modulo 4 line 910 source
Source documentation
Indices 0 or 3 modulo 4.

no axioms what this means
Statement uses: Nat, Bool
Proof uses: Decidable.decide, Or, Eq, HMod.hMod, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
```
def P03 : ℕ → Bool := fun i => decide (i % 4 = 0 ∨ i % 4 = 3)
```
def Usa2013P3.P23 Indices 2 or 3 modulo 4 line 912 source
Source documentation
Indices 2 or 3 modulo 4.

no axioms what this means
Statement uses: Nat, Bool
Proof uses: Decidable.decide, Or, Eq, HMod.hMod, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
```
def P23 : ℕ → Bool := fun i => decide (i % 4 = 2 ∨ i % 4 = 3)
```
def Usa2013P3.P01 Indices 0 or 1 modulo 4 line 914 source
Source documentation
Indices 0 or 1 modulo 4.

no axioms what this means
Statement uses: Nat, Bool
Proof uses: Decidable.decide, Or, Eq, HMod.hMod, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
```
def P01 : ℕ → Bool := fun i => decide (i % 4 = 0 ∨ i % 4 = 1)
```
lemma Usa2013P3.P12_per line 916 source
standard axioms: propext what this means
Statement uses: Nat, Eq, Bool, Usa2013P3.P12, HAdd.hAdd, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, Bool.or, Decidable.decide, HMod.hMod, True, congr, congrArg, Or, Decidable.decide.congr_simp, congrFun', Nat.add_mod_right, Bool.decide_or, eq_self
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.P03_per line 917 source
standard axioms: propext what this means
Statement uses: Nat, Eq, Bool, Usa2013P3.P03, HAdd.hAdd, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, Bool.or, Decidable.decide, HMod.hMod, True, congr, congrArg, Or, Decidable.decide.congr_simp, congrFun', Nat.add_mod_right, Bool.decide_or, eq_self
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.P23_per line 918 source
standard axioms: propext what this means
Statement uses: Nat, Eq, Bool, Usa2013P3.P23, HAdd.hAdd, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, Bool.or, Decidable.decide, HMod.hMod, True, congr, congrArg, Or, Decidable.decide.congr_simp, congrFun', Nat.add_mod_right, Bool.decide_or, eq_self
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.P01_per line 919 source
standard axioms: propext what this means
Statement uses: Nat, Eq, Bool, Usa2013P3.P01, HAdd.hAdd, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, Bool.or, Decidable.decide, HMod.hMod, True, congr, congrArg, Or, Decidable.decide.congr_simp, congrFun', Nat.add_mod_right, Bool.decide_or, eq_self
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Usa2013P3.v0of Moves built from three periodic patterns line 922 source
Source documentation
Moves built from three periodic patterns.

no axioms what this means
Statement uses: Nat, Bool, Usa2013P3.Moves
Proof uses: Usa2013P3.Moves.mk, Fin
1 instances, coercions and auxiliary constants left out.
```
def v0of (n : ℕ) (Px Py Pz : ℕ → Bool) : Moves n :=
…
```
Mentions: Usa2013P3.Moves
lemma Usa2013P3.card_range4 line 925 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, DecidablePred, Eq, Finset.card, Finset.filter, Finset.range, OfNat.ofNat, HAdd.hAdd, ite
Proof uses: Eq.mpr, Finset.sum, id, congrArg, Finset.card_filter, Finset.sum_range_succ, of_eq_true, Eq.trans, True, congrFun', EmptyCollection.emptyCollection, Finset, Finset.sum_boole, Finset.filter_empty, CharP.cast_eq_zero, zero_add, eq_self
27 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.card_range0 line 933 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, DecidablePred, Eq, Finset.card, Finset.filter, Finset.range, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finset, EmptyCollection.emptyCollection, Finset.filter_empty, eq_self
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.card_range1 line 936 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, DecidablePred, Eq, Finset.card, Finset.filter, Finset.range, OfNat.ofNat, ite
Proof uses: Eq.mpr, Finset.sum, id, congrArg, Finset.card_filter, HAdd.hAdd, Finset.sum_range_succ, of_eq_true, Eq.trans, True, congrFun', EmptyCollection.emptyCollection, Finset, Finset.sum_boole, Finset.filter_empty, CharP.cast_eq_zero, zero_add, eq_self
24 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.card_range2 line 942 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, DecidablePred, Eq, Finset.card, Finset.filter, Finset.range, OfNat.ofNat, HAdd.hAdd, ite
Proof uses: Eq.mpr, Finset.sum, id, congrArg, Finset.card_filter, Finset.sum_range_succ, of_eq_true, Eq.trans, True, congrFun', EmptyCollection.emptyCollection, Finset, Finset.sum_boole, Finset.filter_empty, CharP.cast_eq_zero, zero_add, eq_self
27 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.card_range3 line 948 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, DecidablePred, Eq, Finset.card, Finset.filter, Finset.range, OfNat.ofNat, HAdd.hAdd, ite
Proof uses: Eq.mpr, Finset.sum, id, congrArg, Finset.card_filter, Finset.sum_range_succ, of_eq_true, Eq.trans, True, congrFun', EmptyCollection.emptyCollection, Finset, Finset.sum_boole, Finset.filter_empty, CharP.cast_eq_zero, zero_add, eq_self
27 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa2013P3.pon_eval Evaluating pon of a pattern move line 956 source
Source documentation
Evaluating pon of a pattern move.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, HAdd.hAdd, OfNat.ofNat, HMul.hMul, HMod.hMod, Usa2013P3.pon, Finset.card, Finset.filter, Bool.and, Bool.not, Decidable.decide, Bool.true, Finset.range
Proof uses: Usa2013P3.e, Finset.univ, congrArg, Finset, And, Bool.false, Finset.filter_congr, Membership.mem, Iff, of_eq_true, Eq.trans, False, True, congr, Bool.false_eq_true, eq_self, and_true, congrFun', Bool.not_false, Bool.and_true and 20 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma pon_eval {n : ℕ} (F : Fin n → Bool) (P : ℕ → Bool) (hF : ∀ i, F i = P i.val)
    (hP : ∀ i, P (i + 4) = P i) {k r s : ℕ} (hk : n = 4 * k + r) (hn2 : n % 2 = s) :
    pon F = k * (((Finset.range 4).filter fun i => ((P i && !decide (i % 2 = s))) = true).card) +
      (((Finset.range r).filter fun i => ((P i && !decide (i % 2 = s))) = true).card) := by
…
```
Mentions: P, Usa2013P3.pon
lemma Usa2013P3.qon_eval Evaluating qon of a pattern move line 975 source
Source documentation
Evaluating qon of a pattern move.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Bool, Eq, HAdd.hAdd, OfNat.ofNat, HMul.hMul, HMod.hMod, Usa2013P3.qon, Finset.card, Finset.filter, Bool.and, Decidable.decide, Bool.true, Finset.range
Proof uses: Usa2013P3.e, Finset.univ, congrArg, Finset, And, Finset.filter_congr, Membership.mem, Iff.symm, Bool.and_eq_true_iff, Eq.mpr, id, Iff, of_eq_true, Eq.trans, True, congr, Bool.and_eq_true, decide_eq_true_eq, iff_self, Usa2013P3.Count.card_fin_filter and 9 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma qon_eval {n : ℕ} (F : Fin n → Bool) (P : ℕ → Bool) (hF : ∀ i, F i = P i.val)
    (hP : ∀ i, P (i + 4) = P i) {k r s : ℕ} (hk : n = 4 * k + r) (hn2 : n % 2 = s) :
    qon F = k * (((Finset.range 4).filter fun i => ((P i && decide (i % 2 = s))) = true).card) +
      (((Finset.range r).filter fun i => ((P i && decide (i % 2 = s))) = true).card) := by
…
```
Mentions: P, Usa2013P3.qon
lemma Usa2013P3.lower_bound The lower bound: an explicit move all of whose coset elements have weight at least 6 * (n / 4) + n % 4 line 993 source
Source documentation
The lower bound: an explicit move all of whose coset elements have weight at least 6 * (n / 4) + n % 4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Exists, Usa2013P3.Moves, Prod, Bool, LE.le, Usa2013P3.answer, Usa2013P3.weight, Usa2013P3.Moves.vxor, Usa2013P3.sp
Proof uses: And, Eq, HAdd.hAdd, HMul.hMul, OfNat.ofNat, LT.lt, Exists.intro, HDiv.hDiv, HMod.hMod, And.intro, dite, Usa2013P3.v0of, Usa2013P3.P01, id, Usa2013P3.Ecard, Usa2013P3.Ecard_eq, Usa2013P3.Ocard, Usa2013P3.OE_sum, Usa2013P3.pon, Usa2013P3.Moves.x and 81 more
97 instances, coercions and auxiliary constants left out.

Tactic trace: 140 steps
Open to load the checked before-and-after goal states.
```
lemma lower_bound {n : ℕ} :
    ∃ v : Moves n, ∀ ε : Bool × Bool × Bool, answer n ≤ weight (Moves.vxor v (sp n ε)) := by
…
```
Mentions: Usa2013P3.Moves, Usa2013P3.answer, Usa2013P3.weight, Usa2013P3.Moves.vxor, Usa2013P3.sp
lemma Usa2013P3.f_le f C is at most the weight of any move producing C line 1080 source
Source documentation
f C is at most the weight of any move producing C.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2013P3.Token, Bool, Usa2013P3.Moves, Eq, Usa2013P3.applyMoves, LE.le, Usa2013P3.f, Usa2013P3.weight
Proof uses: Nat.sInf_le, Set.ofPred, Exists, And, Exists.intro, And.intro, rfl
1 instances, coercions and auxiliary constants left out.
```
lemma f_le {n : ℕ} {C : Token n → Bool} {v : Moves n} (h : applyMoves v = C) :
    f C ≤ weight v :=
…
```
Mentions: Usa2013P3.Token, Usa2013P3.Moves, h, Usa2013P3.applyMoves, Usa2013P3.f, Usa2013P3.weight
lemma Usa2013P3.f_spec The minimum is attained: some move produces C with weight f C line 1085 source
Source documentation
The minimum is attained: some move produces C with weight f C.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2013P3.Token, Bool, Usa2013P3.Admissible, Exists, Usa2013P3.Moves, And, Eq, Usa2013P3.applyMoves, Usa2013P3.weight, Usa2013P3.f
Proof uses: Membership.mem, Set, Set.ofPred, InfSet.sInf, Nat.sInf_mem, Exists.intro, And.intro, rfl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma f_spec {n : ℕ} {C : Token n → Bool} (hC : Admissible C) :
    ∃ w : Moves n, applyMoves w = C ∧ weight w = f C := by
…
```
Mentions: Usa2013P3.Token, Usa2013P3.Admissible, Usa2013P3.Moves, Usa2013P3.applyMoves, Usa2013P3.weight, Usa2013P3.f
lemma Usa2013P3.f_le_answer The upper bound for f line 1095 source
Source documentation
The upper bound for f.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Usa2013P3.Token, Bool, Usa2013P3.Admissible, LE.le, Usa2013P3.f, Usa2013P3.answer
Proof uses: Usa2013P3.Moves, Eq, Usa2013P3.applyMoves, Prod, Usa2013P3.weight, Usa2013P3.Moves.vxor, Usa2013P3.sp, Exists, Usa2013P3.upper_bound, le_trans, Usa2013P3.f_le, Eq.mpr, id, congrArg, Eq.symm, funext, Bool.xor, Usa2013P3.applyMoves_vxor, Bool.false, Usa2013P3.applyMoves_sp and 6 more
4 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma f_le_answer {n : ℕ} (C : Token n → Bool) (hC : Admissible C) :
    f C ≤ answer n := by
…
```
Mentions: Usa2013P3.Token, Usa2013P3.Admissible, Usa2013P3.f, Usa2013P3.answer
lemma Usa2013P3.answer_le_f The lower bound for f: some admissible configuration needs at least answer n operations line 1107 source
Source documentation
The lower bound for f: some admissible configuration needs at least answer n operations.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Exists, Usa2013P3.Token, Bool, And, Usa2013P3.Admissible, LE.le, Usa2013P3.answer, Usa2013P3.f
Proof uses: Usa2013P3.Moves, Prod, Usa2013P3.weight, Usa2013P3.Moves.vxor, Usa2013P3.sp, Usa2013P3.lower_bound, Exists.intro, Usa2013P3.applyMoves, And.intro, Eq, rfl, Usa2013P3.kernel_eq_span, funext, Bool.false, Eq.mpr, Bool.xor, id, congrArg, Usa2013P3.applyMoves_vxor, of_eq_true and 13 more
11 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma answer_le_f {n : ℕ} (hn : 0 < n) :
    ∃ C : Token n → Bool, Admissible C ∧ answer n ≤ f C := by
…
```
Mentions: Usa2013P3.Token, Usa2013P3.Admissible, Usa2013P3.answer, Usa2013P3.f
problem Usa2013P3.usa2013_p3 line 1129 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, IsGreatest, Set.ofPred, Exists, Usa2013P3.Token, Bool, And, Usa2013P3.Admissible, Eq, Usa2013P3.f, Usa2013P3.answer
Proof uses: LE.le, Usa2013P3.answer_le_f, Usa2013P3.f_le_answer, le_antisymm, And.intro, Membership.mem, Set, upperBounds, Exists.intro
11 instances, coercions and auxiliary constants left out.

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