Lean statement

Nine routing-density and representation estimates

Lean is a language for mathematical statements and proofs that a computer can verify. This page shows one statement file from OpenAI’s release, possible paper matches and independent reports. The code-like names below identify the definitions or theorems selected by the proof-verification settings.

Theorem selected for verification: OAI.ThorpNine.main

Lean statement file: ThorpRouting.leanShow on the mapFamily 238. OpenAI lists this as a main result in its Lean catalogue.

See the candidate theorem Who ran the proof-verification program Report a comparison with the paper (GitHub issue)

The Lean statement

The lines of the Lean statement that state the theorem, then the definitions in the file that it uses.

theorem ThorpNine.main :    ThorpNine.Adaptive.Thorp.AdaptiveBounds.MainStatement ∧    ThorpNine.Casimir.Thorp.CasimirBounds.MainStatement ∧    ThorpNine.Dense.Thorp.DenseTruncation.MainStatement ∧    ThorpNine.Contact.Thorp.SparseContact.MainStatement ∧    ThorpNine.Harmonic.Thorp.HarmonicBounds.MainStatement ∧    ThorpNine.Smoothing.Thorp.StrongSmoothing.MainStatement ∧    ThorpNine.Tail.Thorp.StrongTail.MainStatement ∧    ThorpNine.HighTail.Thorp.HighHeight.MainStatement ∧    ThorpNine.SparseSaving.Thorp.SparseRegime.MainStatement := by  sorry

A Lean statement states the theorem and leaves its proof as sorry on purpose. OpenAI’s proof is in a separate solution module, and a program called Comparator checks that proof against this statement.

Definitions needed to read it

Local definitions the statement names, followed through the definitions they name in turn. The match is by name in the source text, so a name reached only through notation can be missed; the full file is below.

abbreviation OAI.ThorpNine.Adaptive.Thorp.Card line 11
```
abbrev Card (d : ℕ) := Fin d → Bool
```

definition OAI.ThorpNine.Adaptive.Thorp.switchFun line 13

def switchFun {d : ℕ} (ξ : Card d → Bool) (x : Card (d + 1)) : Card (d + 1) :=  Fin.cons (Bool.xor (x 0) (ξ (Fin.tail x))) (Fin.tail x)

definition OAI.ThorpNine.Adaptive.Thorp.pairSwitch line 25

def pairSwitch {d : ℕ} (ξ : Card d → Bool) : Equiv.Perm (Card (d + 1)) :=  { toFun := switchFun ξ    invFun := switchFun ξ    left_inv := switchFun_involutive ξ    right_inv := switchFun_involutive ξ }

definition OAI.ThorpNine.Adaptive.Thorp.Butterfly line 31

def Butterfly : ℕ → Type  | 0 => Unit  | d + 1 => (Card d → Bool) × (Bool → Butterfly d)

definition OAI.ThorpNine.Adaptive.Thorp.childLift line 35

def childLift {d : ℕ} (p : Bool → Equiv.Perm (Card d)) : Equiv.Perm (Card (d + 1)) where  toFun x := Fin.cons (x 0) (p (x 0) (Fin.tail x))  invFun x := Fin.cons (x 0) ((p (x 0)).symm (Fin.tail x))  left_inv x := by simp only [Fin.cons_zero, Fin.tail_cons, Equiv.symm_apply_apply, Fin.cons_self_tail]  right_inv x := by simp only [Fin.cons_zero, Fin.tail_cons, Equiv.apply_symm_apply, Fin.cons_self_tail]

definition OAI.ThorpNine.Adaptive.Thorp.butterflyPerm line 41

def butterflyPerm : (d : ℕ) → Butterfly d → Equiv.Perm (Card d)  | 0, _ => 1  | d + 1, b => pairSwitch b.1 * childLift (fun ε => butterflyPerm d (b.2 ε))

definition OAI.ThorpNine.Adaptive.Thorp.SwitchIndex line 45

def SwitchIndex : ℕ → Type  | 0 => Empty  | d + 1 => Sum (Card d) (Bool × SwitchIndex d)

definition OAI.ThorpNine.Adaptive.Thorp.decodeButterfly line 59

def decodeButterfly : (d : ℕ) → (SwitchIndex d → Bool) → Butterfly d  | 0, _ => ()  | d + 1, ω => (fun y => ω (Sum.inl y), fun ε =>      decodeButterfly d (fun i => ω (Sum.inr (ε,i))))

abbreviation OAI.ThorpNine.Adaptive.Thorp.Specht.Cell line 69

abbrev Cell (μ : YoungDiagram) := {x : ℕ × ℕ // x ∈ μ.cells}

definition OAI.ThorpNine.Adaptive.Thorp.Specht.row line 71

def row {μ : YoungDiagram} (x : Cell μ) : ℕ := x.1.1

definition OAI.ThorpNine.Adaptive.Thorp.Specht.col line 73

def col {μ : YoungDiagram} (x : Cell μ) : ℕ := x.1.2

definition OAI.ThorpNine.Adaptive.Thorp.Specht.rowIndex line 78

noncomputable def rowIndex {μ : YoungDiagram} (x : Cell μ) : Fin (μ.colLen 0) :=  ⟨row x, (row_lt_colLen x).trans_le (μ.colLen_anti 0 (col x) (Nat.zero_le _))⟩

abbreviation OAI.ThorpNine.Adaptive.Thorp.Specht.Tabloid line 81

abbrev Tabloid (μ : YoungDiagram) :=  {f : Cell μ → Fin (μ.colLen 0) // ∃ p : Equiv.Perm (Cell μ), f = rowIndex ∘ p}

definition OAI.ThorpNine.Adaptive.Thorp.Specht.baseTabloid line 86

noncomputable def baseTabloid (μ : YoungDiagram) : Tabloid μ := ⟨rowIndex, 1, rfl⟩

definition OAI.ThorpNine.Adaptive.Thorp.Specht.tabloidAct line 88

noncomputable def tabloidAct {μ : YoungDiagram} (p : Equiv.Perm (Cell μ)) :    Equiv.Perm (Tabloid μ) where

Show the remaining 12 lines

  toFun f := ⟨fun x => f.1 (p⁻¹ x), by    obtain ⟨q,hq⟩ := f.2    refine ⟨q*p⁻¹, ?_⟩    funext x    simp only [hq,Function.comp_apply,Equiv.Perm.mul_apply]⟩  invFun f := ⟨fun x => f.1 (p x), by    obtain ⟨q,hq⟩ := f.2    refine ⟨q*p, ?_⟩    funext x    simp only [hq,Function.comp_apply,Equiv.Perm.mul_apply]⟩  left_inv f := by apply Subtype.ext; funext x; simp  right_inv f := by apply Subtype.ext; funext x; simp

definition OAI.ThorpNine.Adaptive.Thorp.Specht.tabloidRep line 115

noncomputable def tabloidRep (μ : YoungDiagram) :    Representation ℂ (Equiv.Perm (Cell μ)) (Tabloid μ → ℂ) where

Show the remaining 9 lines

  toFun p :=    { toFun := fun v f => v (tabloidAct p⁻¹ f)      map_add' := by intros; rfl      map_smul' := by intros; rfl }  map_one' := by ext v f; simp  map_mul' p q := by    ext v f    simp only [mul_inv_rev,tabloidAct_mul,Equiv.Perm.mul_apply]    rfl

definition OAI.ThorpNine.Adaptive.Thorp.Specht.delta line 127

noncomputable def delta {μ : YoungDiagram} (f : Tabloid μ) : Tabloid μ → ℂ :=  fun g => if g=f then 1 else 0

definition OAI.ThorpNine.Adaptive.Thorp.Specht.colGroup line 130

noncomputable def colGroup (μ : YoungDiagram) : Subgroup (Equiv.Perm (Cell μ)) where  carrier := {p | ∀ x, col (p x) = col x}  one_mem' := by intro x; rfl  mul_mem' := by intro p q hp hq x; exact (hp (q x)).trans (hq x)  inv_mem' := by intro p hp x; simpa using (hp (p⁻¹ x)).symm

definition OAI.ThorpNine.Adaptive.Thorp.Specht.permSign line 136

noncomputable def permSign {α : Type*} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) : ℂ :=  ((Equiv.Perm.sign p : ℤ) : ℂ)

definition OAI.ThorpNine.Adaptive.Thorp.Specht.alternator line 143

noncomputable def alternator (C : Subgroup (Equiv.Perm α))    (ρ : Representation ℂ (Equiv.Perm α) V) : Module.End ℂ V := by  classical  exact ∑ c : C, permSign (c : Equiv.Perm α) • ρ c

definition OAI.ThorpNine.Adaptive.Thorp.Specht.polytabloid line 150

noncomputable def polytabloid (μ : YoungDiagram) : Tabloid μ → ℂ :=  alternator (colGroup μ) (tabloidRep μ) (delta (baseTabloid μ))

definition OAI.ThorpNine.Adaptive.Thorp.Specht.space line 153

noncomputable def space (μ : YoungDiagram) : Submodule ℂ (Tabloid μ → ℂ) :=  Submodule.span ℂ (Set.range (fun p : Equiv.Perm (Cell μ) => tabloidRep μ p (polytabloid μ)))

definition OAI.ThorpNine.Adaptive.Thorp.Specht.subrepresentation line 171

noncomputable def subrepresentation (μ : YoungDiagram) : Subrepresentation (tabloidRep μ) :=  ⟨space μ, fun p v hv => action_mem_space μ p v hv⟩

definition OAI.ThorpNine.Adaptive.Thorp.Specht.representation line 174

noncomputable def representation (μ : YoungDiagram) :    Representation ℂ (Equiv.Perm (Cell μ)) (space μ) :=  (subrepresentation μ).toRepresentation

18 more definitions are reached the same way; the full file lists them.

Possible paper match, with no recorded review

Atlas selected this possible match by comparing words in the Lean statement with every statement in the family. No review of whether the statements mean the same thing is recorded.

Words of the Lean statement, its names split into words, that also appear in the theorem: high, heights, tail, cycle, switch, delta, log, bound and one more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: conditional.

Statements in Routing densities and representation contraction for Thorp sweeps come first because the release’s name for this Lean statement shares words with that paper’s title.

Proposition 5.1 of Routing densities and representation contraction for Thorp sweeps

Proposition (High-height cycle tail)

There are absolute b,\delta>0 and an integer J_0\ge1 such that, uniformly in the tracked input injection of size r and for every integer J\ge J_0,

\begin{aligned}\log_2\E 2^{b\sum_{j\ge J}C_j}&\le O(r2^{-bJ}),\\ \log_2\E 2^{b\sum_jC_j}&\le O(r(r/n)^\delta).\end{aligned}

The first bound also holds with expectation conditional on all input-side switches and all output switches of heights at most s, for every integer 0\le s\le d with 2s<J, uniformly in the fixed switch values and with the same absolute implied constant.

Section 5, Certificate tails and numerical dense bounds Read it in the paper TeX source, line 5

Show the TeX

There are absolute $b,\delta>0$ and an integer $J_0\ge1$ such that, uniformly in the tracked input injection of size $r$ and for every integer $J\ge J_0$,
\begin{align}
 \log_2\E 2^{b\sum_{j\ge J}C_j}&\le O(r2^{-bJ}),\\
 \log_2\E 2^{b\sum_jC_j}&\le O(r(r/n)^\delta).
\end{align}
The first bound also holds with expectation conditional on all input-side
switches and all output switches of heights at most $s$, for every integer
$0\le s\le d$ with $2s<J$, uniformly in the fixed switch values and with
the same absolute implied constant.

Other possible paper matches, closest wording first

Proposition 7.1 of Routing densities and representation contraction for Thorp sweeps. Words of the Lean statement, its names split into words, that also appear in the theorem: contact, k/2, reversed, sparse, operator and zero. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: coordinate and estimate.
Theorem 8.1 of Routing densities and representation contraction for Thorp sweeps. Words of the Lean statement, its names split into words, that also appear in the theorem: casimir, cycle, permutation, law, sweeps, bound and one more. Found in the paper’s title, which its main theorem states: representation and thorp. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: density.
Proposition 8.3 of Compatibility entropy and the spectrum of a Thorp sweep. Words of the Lean statement, its names split into words, that also appear in the theorem: harmonic, actions, acting, k/2, function, space and six more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: coordinate.
Proposition 5.2 of Routing densities and representation contraction for Thorp sweeps. Words of the Lean statement, its names split into words, that also appear in the theorem: dense, truncation, exp and integer. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: exceeds and density.
Corollary 7.3 of Routing densities and representation contraction for Thorp sweeps. Words of the Lean statement, its names split into words, that also appear in the theorem: k/4, saving, 3/4, sparse and log.
Proposition 6.3 of Routing densities and representation contraction for Thorp sweeps. Words of the Lean statement, its names split into words, that also appear in the theorem: strong, tail, one and bound. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: coordinate and density.

How Atlas selects possible matches: it compares words in the Lean statement with every statement in the family. It also splits Lean names into words. The release’s label and note receive less weight; a main theorem wins a close match. If the Lean wording yields no clear match, Atlas uses the catalogue description. This selects passages to compare; it does not establish that they mean the same thing.

Reported Comparator runs

One independent group reports that Comparator accepted a run for this Lean statement file: Carlos Toledo’s cert-machine. Each group reports its own Comparator run for this statement file. Atlas has not repeated the runs.

For a configured theorem, Comparator tests whether OpenAI’s proof proves the exact Lean statement. Some files instead configure definitions for comparison by name and type. Acceptance does not establish that the statement means the same thing as the paper’s theorem.

Carlos Toledo’s cert-machine

How they ran it, in their words

Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule; every family’s challenge statements read against OpenAI’s headline, clause by clause. Decider: Comparator (leanprover/comparator d03acab1 = tag v4.34.0, built with the release’s toolchain v4.34.1), lean4export 076e8e57, landrun 811cfff5, nanoda_lib 3a240721 — on GitHub’s Linux runners (.github/workflows/openai-math-kernel.yml), one j…

Accepted Their term: “CERTIFIED”.
Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.
Reported 10 October 2026, at the release version shown here. Original verification report

What an accepted Comparator run would establish

If Comparator is run under this configuration and accepts, the solution proves the configured theorem using only the allowed axioms, and the Lean kernel accepts every step.

This configuration lists no definition holes, so every definition the statement uses is compared as it is written in this file.

Allowed axioms: propext, Quot.sound, Classical.choice

Acceptance leaves open whether the Lean statement means the same thing as the paper’s theorem, whether the paper’s other claims are correct, and whether the result is new. Those questions require comparing the definitions and statements, reviewing the paper’s arguments, and reading the earlier literature.

Do family 238’s Lean statements express the advertised result?

These assessments compare all the family’s Lean statements with the whole result OpenAI describes in its catalogue. They do not assess this statement alone. Each group uses its own published rules.

MathVet and cert-machine agree on how much of the advertised result the Lean statements express.

MathVet
Finds the whole advertised result stated or implied Their term: “full”.
The challenge statements imply the headline claim after unpacking definitions or one routine step. Their record
Their note: ThorpResults.remaining_main (ThorpRemaining) is a conjunction whose last conjunct OptimalOrderMain := IsTheta atTop (mixingTime d) (log (2^d)) states exactly the Θ(log N) mixing for N = 2^d cards, with mixingTime d := sInf {t | distance d t ≤ 1/4}, distance d t := tv (law d t) (uniform d) the total-variation distance of the full permutation law (and InformationMain records that lawFrom from any starting deck has the same distance, plus distance d (2048 d) → 0); the 12 other challenge files are supporting Fourier/representation estimates (regular_trace_smoothing, binary_sweep_contraction_and_mixing, robust_permanent, ...). All of them state estimates for the same hand-built Thorp shuffle.
Definitions the group asks readers to compare with the paper: Custom Thorp shuffle and 'mixing time': step (d+1) c := (pairSwitch d c on the head bit, then rotate the coordinate order) on State d := Equiv.Perm (Fin d → Bool) with Coins (d+1) = (Fin d → Bool) → Bool iid fair coins, fairMass, tv, mixingTime d := sInf {t | distance d t ≤ 1/4}; this is the standard pair-swap-and-interleave Thorp shuffle and TV-from-uniform with ε = 1/4, but it is a hand-written model and the Θ-statement hides explicit constants (1600d, 2048d, ...). OccupiedOverlap shows an axiom_files hit (HookModel.lean) that is a doc-comment false positive.
Carlos Toledo’s cert-machine
Finds the whole advertised result stated or implied Their term: “MATCHES”.
The challenge statements state the headline as OpenAI wrote it. Their record

Read the complete assessments on the family page.

OpenAI’s own note on what this Lean statement covers

“The conditional high-height estimate requires a sufficiently large cutoff height $J$ that exceeds twice the number $s$ of coordinates in the fixed low block, so $J>2s$. These are the earlier nine statements associated with the paper; its changed later statements and six other result blocks are outside this scope.”
Quoted from OpenAI’s Lean note for this family

An AI agent drafted an interpretation of that note, classifying this statement as “unclear”. No human review of the draft is recorded.

Supporting material

The complete Lean statement file

2,579 lines, copied from release version fd4aeeb. A name defined in this file links to its line; pointing at the name shows its definition.

Declared in this fileOpenAI’s library at fd4aeebOther linked names open the current documentation for Mathlib, Lean’s mathematical library.

Links in the file: 1,261 to its own declarations, 1,611 to Mathlib’s documentation. 167 declared names also link to the same declaration in OpenAI’s library. 36 identifiers stay plain because they resolve to no single declaration: variables Lean binds automatically, notation, or names the scan of the pinned sources did not find. OpenAI uses Mathlib version d13f23b. The linked documentation describes the current version, so names that have since changed may be missing there.

import Mathlibnamespace OAInamespace ThorpNine.Adaptivenamespace Thorpopen scoped BigOperatorsopen Filterabbrev Card (d : ℕ) := Fin d → Booldef switchFun {d : ℕ} (ξ : Card d → Bool) (x : Card (d + 1)) : Card (d + 1) :=  Fin.cons (Bool.xor (x 0) (ξ (Fin.tail x))) (Fin.tail x)theorem switchFun_involutive {d : ℕ} (ξ : Card d → Bool) :    Function.Involutive (switchFun ξ) := by  intro x  funext i  refine Fin.cases ?_ (fun j => ?_) i  · simp only [switchFun, Fin.cons_zero, Fin.tail_cons]    cases x 0 <;> cases ξ (Fin.tail x) <;> rfl  · simp [switchFun, Fin.tail]def pairSwitch {d : ℕ} (ξ : Card d → Bool) : Equiv.Perm (Card (d + 1)) :=  { toFun := switchFun ξ    invFun := switchFun ξ    left_inv := switchFun_involutive ξ    right_inv := switchFun_involutive ξ }def Butterfly : ℕ → Type  | 0 => Unit  | d + 1 => (Card d → Bool) × (Bool → Butterfly d)def childLift {d : ℕ} (p : Bool → Equiv.Perm (Card d)) : Equiv.Perm (Card (d + 1)) where  toFun x := Fin.cons (x 0) (p (x 0) (Fin.tail x))  invFun x := Fin.cons (x 0) ((p (x 0)).symm (Fin.tail x))  left_inv x := by simp only [Fin.cons_zero, Fin.tail_cons, Equiv.symm_apply_apply, Fin.cons_self_tail]  right_inv x := by simp only [Fin.cons_zero, Fin.tail_cons, Equiv.apply_symm_apply, Fin.cons_self_tail]def butterflyPerm : (d : ℕ) → Butterfly d → Equiv.Perm (Card d)  | 0, _ => 1  | d + 1, b => pairSwitch b.1 * childLift (fun ε => butterflyPerm d (b.2 ε))def SwitchIndex : ℕ → Type  | 0 => Empty  | d + 1 => Sum (Card d) (Bool × SwitchIndex d)instance (d : ℕ) : Fintype (SwitchIndex d) := by  induction d with  | zero => exact inferInstanceAs (Fintype Empty)  | succ d ih => exact inferInstanceAs (Fintype (Sum (Card d) (Bool × SwitchIndex d)))instance (d : ℕ) : DecidableEq (SwitchIndex d) := by  induction d with  | zero => exact inferInstanceAs (DecidableEq Empty)  | succ d ih => exact inferInstanceAs (DecidableEq (Sum (Card d) (Bool × SwitchIndex d)))def decodeButterfly : (d : ℕ) → (SwitchIndex d → Bool) → Butterfly d  | 0, _ => ()  | d + 1, ω => (fun y => ω (Sum.inl y), fun ε =>      decodeButterfly d (fun i => ω (Sum.inr (ε,i))))end Thorpnamespace Thorp.Spechtopen scoped BigOperators Classicalabbrev Cell (μ : YoungDiagram) := {x : ℕ × ℕ // x ∈ μ.cells}def row {μ : YoungDiagram} (x : Cell μ) : ℕ := x.1.1def col {μ : YoungDiagram} (x : Cell μ) : ℕ := x.1.2lemma row_lt_colLen {μ : YoungDiagram} (x : Cell μ) : row x < μ.colLen (col x) :=  YoungDiagram.mem_iff_lt_colLen.mp x.2noncomputable def rowIndex {μ : YoungDiagram} (x : Cell μ) : Fin (μ.colLen 0) :=  ⟨row x, (row_lt_colLen x).trans_le (μ.colLen_anti 0 (col x) (Nat.zero_le _))⟩abbrev Tabloid (μ : YoungDiagram) :=  {f : Cell μ → Fin (μ.colLen 0) // ∃ p : Equiv.Perm (Cell μ), f = rowIndex ∘ p}noncomputable instance (μ : YoungDiagram) : Fintype (Tabloid μ) := Fintype.ofFinite _noncomputable def baseTabloid (μ : YoungDiagram) : Tabloid μ := ⟨rowIndex, 1, rfl⟩noncomputable def tabloidAct {μ : YoungDiagram} (p : Equiv.Perm (Cell μ)) :    Equiv.Perm (Tabloid μ) where  toFun f := ⟨fun x => f.1 (p⁻¹ x), by    obtain ⟨q,hq⟩ := f.2    refine ⟨q*p⁻¹, ?_⟩    funext x    simp only [hq,Function.comp_apply,Equiv.Perm.mul_apply]⟩  invFun f := ⟨fun x => f.1 (p x), by    obtain ⟨q,hq⟩ := f.2    refine ⟨q*p, ?_⟩    funext x    simp only [hq,Function.comp_apply,Equiv.Perm.mul_apply]⟩  left_inv f := by apply Subtype.ext; funext x; simp  right_inv f := by apply Subtype.ext; funext x; simp@[simp] lemma tabloidAct_apply {μ : YoungDiagram} (p : Equiv.Perm (Cell μ))    (f : Tabloid μ) (x : Cell μ) : (tabloidAct p f).1 x = f.1 (p⁻¹ x) := rfl@[simp] lemma tabloidAct_one (μ : YoungDiagram) : tabloidAct (1 : Equiv.Perm (Cell μ)) = 1 := by  ext f x  rfl@[simp] lemma tabloidAct_mul {μ : YoungDiagram} (p q : Equiv.Perm (Cell μ)) :    tabloidAct (p*q) = tabloidAct p * tabloidAct q := by  ext f x  simp only [tabloidAct_apply, mul_inv_rev,Equiv.Perm.mul_apply]noncomputable def tabloidRep (μ : YoungDiagram) :    Representation ℂ (Equiv.Perm (Cell μ)) (Tabloid μ → ℂ) where  toFun p :=    { toFun := fun v f => v (tabloidAct p⁻¹ f)      map_add' := by intros; rfl      map_smul' := by intros; rfl }  map_one' := by ext v f; simp  map_mul' p q := by    ext v f    simp only [mul_inv_rev,tabloidAct_mul,Equiv.Perm.mul_apply]    rflnoncomputable def delta {μ : YoungDiagram} (f : Tabloid μ) : Tabloid μ → ℂ :=  fun g => if g=f then 1 else 0noncomputable def colGroup (μ : YoungDiagram) : Subgroup (Equiv.Perm (Cell μ)) where  carrier := {p | ∀ x, col (p x) = col x}  one_mem' := by intro x; rfl  mul_mem' := by intro p q hp hq x; exact (hp (q x)).trans (hq x)  inv_mem' := by intro p hp x; simpa using (hp (p⁻¹ x)).symmnoncomputable def permSign {α : Type*} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) : ℂ :=  ((Equiv.Perm.sign p : ℤ) : ℂ)sectionvariable {α V : Type*} [Fintype α] [DecidableEq α] [AddCommGroup V] [Module ℂ V]noncomputable def alternator (C : Subgroup (Equiv.Perm α))    (ρ : Representation ℂ (Equiv.Perm α) V) : Module.End ℂ V := by  classical  exact ∑ c : C, permSign (c : Equiv.Perm α) • ρ cendnoncomputable def polytabloid (μ : YoungDiagram) : Tabloid μ → ℂ :=  alternator (colGroup μ) (tabloidRep μ) (delta (baseTabloid μ))noncomputable def space (μ : YoungDiagram) : Submodule ℂ (Tabloid μ → ℂ) :=  Submodule.span ℂ (Set.range (fun p : Equiv.Perm (Cell μ) => tabloidRep μ p (polytabloid μ)))lemma orbit_mem_space (μ : YoungDiagram) (p : Equiv.Perm (Cell μ)) :    tabloidRep μ p (polytabloid μ) ∈ space μ := Submodule.subset_span ⟨p,rfl⟩lemma action_mem_space (μ : YoungDiagram) (p : Equiv.Perm (Cell μ))    (v : Tabloid μ → ℂ) (hv : v ∈ space μ) : tabloidRep μ p v ∈ space μ := by  induction hv using Submodule.span_induction with  | mem v hv =>    obtain ⟨q,rfl⟩ := hv    change ((tabloidRep μ p)*(tabloidRep μ q)) (polytabloid μ) ∈ space μ    rw [←map_mul]    exact orbit_mem_space μ (p*q)  | zero => simp  | add v w hv hw ihv ihw => simpa using (space μ).add_mem ihv ihw  | smul a v hv ih => simpa using (space μ).smul_mem a ihnoncomputable def subrepresentation (μ : YoungDiagram) : Subrepresentation (tabloidRep μ) :=  ⟨space μ, fun p v hv => action_mem_space μ p v hv⟩noncomputable def representation (μ : YoungDiagram) :    Representation ℂ (Equiv.Perm (Cell μ)) (space μ) :=  (subrepresentation μ).toRepresentationend Thorp.Spechtnamespace Thorp.PermutationHilbertopen scoped BigOperators ComplexConjugate Classicalopen Complexvariable {X : Type*} [Fintype X]abbrev H (X : Type*) [Fintype X] := EuclideanSpace ℂ Xend Thorp.PermutationHilbertnamespace Thorp.Spechtopen scoped BigOperators Classicalnoncomputable def hilbertEquiv (μ : YoungDiagram) :    (Tabloid μ → ℂ) ≃ₗ[ℂ] PermutationHilbert.H (Tabloid μ) :=  (WithLp.linearEquiv 2 ℂ (Tabloid μ → ℂ)).symmnoncomputable def hilbertSpace (μ : YoungDiagram) :    Submodule ℂ (PermutationHilbert.H (Tabloid μ)) := (space μ).map (hilbertEquiv μ).toLinearMapend Thorp.Spechtnamespace Thorp.UnitaryFinitesectionopen scoped BigOperators ComplexConjugate Classicalvariable {G : Type*} [Group G] [Fintype G]variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V]noncomputable def continuousRepresentation (ρ : Representation ℂ G V) : G →* (V →L[ℂ] V) where  toFun g := (ρ g).toContinuousLinearMap  map_one' := by ext v; simp  map_mul' g h := by ext v; simpendopen scoped BigOperators Classicalvariable {G : Type*} [Group G] [Fintype G]variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V]variable {Ω Ξ : Type*} [Fintype Ω] [Fintype Ξ]noncomputable def sampleOperator (ρ : Representation ℂ G V) (P : Ω → G) : V →L[ℂ] V :=  (Fintype.card Ω:ℂ)⁻¹ • ∑ ω,continuousRepresentation ρ (P ω)end Thorp.UnitaryFinitenamespace Thorp.Spechtopen scoped BigOperators Classicalnoncomputable def spaceHilbertEquiv (μ : YoungDiagram) : space μ ≃ₗ[ℂ] hilbertSpace μ :=  (hilbertEquiv μ).submoduleMap (space μ)noncomputable def unitaryRepresentation (μ : YoungDiagram) :    Representation ℂ (Equiv.Perm (Cell μ)) (hilbertSpace μ) :=  ((spaceHilbertEquiv μ).conjAlgEquiv ℂ).toMonoidHom.comp (representation μ)variable {α ι : Type*} [Fintype α] [Fintype ι]noncomputable def relabelledUnitary (μ : YoungDiagram) (e : α ≃ Cell μ) :    Representation ℂ (Equiv.Perm α) (hilbertSpace μ) :=  (unitaryRepresentation μ).comp e.permCongrHom.toMonoidHomend Thorp.Spechtnamespace Thorp.SparseContactopen scoped BigOperatorsnoncomputable def sweepOperator (d : ℕ) (μ : YoungDiagram)    (e : Card d ≃ Specht.Cell μ) (reverse : Bool) :    Specht.hilbertSpace μ →L[ℂ] Specht.hilbertSpace μ :=  UnitaryFinite.sampleOperator (V := Specht.hilbertSpace μ) (Specht.relabelledUnitary μ e)    (fun ω : SwitchIndex d → Bool => if reverse then      (butterflyPerm d (decodeButterfly d ω))⁻¹ else butterflyPerm d (decodeButterfly d ω))end Thorp.SparseContactnamespace Thorp.Casimiropen scoped BigOperators Classicalopen Filternoncomputable def levelScale (n k : ℕ) : ℝ :=  (k:ℝ) * (1 + Real.log ((n:ℝ)/(k:ℝ)))end Thorp.Casimirnamespace Thorp.AdaptiveBoundsopen scoped BigOperators Classicalopen Casimirnoncomputable def positiveSquare {V : Type*} [NormedAddCommGroup V]    [InnerProductSpace ℂ V] [FiniteDimensional ℂ V] (T : V →L[ℂ] V) : V →L[ℂ] V :=  T * T.adjointnoncomputable def F (d : ℕ) (μ : YoungDiagram) (e : Card d ≃ Specht.Cell μ)    (rev : Bool) : Specht.hilbertSpace μ →L[ℂ] Specht.hilbertSpace μ :=  positiveSquare (V := Specht.hilbertSpace μ) (SparseContact.sweepOperator d μ e rev)noncomputable def fourthTrace (d : ℕ) (μ : YoungDiagram)    (e : Card d ≃ Specht.Cell μ) (rev : Bool) : ℝ :=  (LinearMap.trace ℂ (Specht.hilbertSpace μ) ((F d μ e rev)^4).toLinearMap).redef MainStatement : Prop :=  ∃ c c' C c₀ : ℝ, 0<c ∧ 0<c' ∧ 0<C ∧ 0<c₀ ∧    ∀ (d : ℕ) (μ : YoungDiagram) (e : Card d ≃ Specht.Cell μ) (rev : Bool),      let h := levelScale (2^d) (μ.card-μ.rowLen 0)      let D : ℝ := Module.finrank ℂ (Specht.space μ)      ‖F d μ e rev‖ ≤ Real.exp (-c*h) ∧      fourthTrace d μ e rev ≤ Real.exp (-c'*Real.log D+C*h) ∧      ‖SparseContact.sweepOperator d μ e rev‖ ≤ Real.exp (-c₀*(Real.log D+h))end Thorp.AdaptiveBoundsend ThorpNine.Adaptiverun_cmd do  Lean.modifyEnv fun env => Lean.Meta.auxLemmasExt.setState env {}  let matcherCache := Lean.mkIdent    (Lean.mkPrivateNameCore `Lean.Meta.Match.Match `Lean.Meta.Match.matcherExt)  Lean.Elab.Command.elabCommand (← `(command|    run_cmd Lean.modifyEnv fun env => Lean.EnvExtension.setState $matcherCache env {}))namespace ThorpNine.Casimirnamespace Thorpopen scoped BigOperatorsopen Filterabbrev Card (d : ℕ) := Fin d → Booldef Coins : ℕ → Type  | 0 => Unit  | d + 1 => Card d → Boolinstance (d : ℕ) : Fintype (Coins d) := by  cases d <;> dsimp [Coins] <;> infer_instancedef switchFun {d : ℕ} (ξ : Card d → Bool) (x : Card (d + 1)) : Card (d + 1) :=  Fin.cons (Bool.xor (x 0) (ξ (Fin.tail x))) (Fin.tail x)theorem switchFun_involutive {d : ℕ} (ξ : Card d → Bool) :    Function.Involutive (switchFun ξ) := by  intro x  funext i  refine Fin.cases ?_ (fun j => ?_) i  · simp only [switchFun, Fin.cons_zero, Fin.tail_cons]    cases x 0 <;> cases ξ (Fin.tail x) <;> rfl  · simp [switchFun, Fin.tail]def pairSwitch {d : ℕ} (ξ : Card d → Bool) : Equiv.Perm (Card (d + 1)) :=  { toFun := switchFun ξ    invFun := switchFun ξ    left_inv := switchFun_involutive ξ    right_inv := switchFun_involutive ξ }def rotate (d : ℕ) : Equiv.Perm (Card d) where  toFun x i := x (finRotate d i)  invFun x i := x ((finRotate d).symm i)  left_inv x := by funext i; simp only [Equiv.apply_symm_apply]  right_inv x := by funext i; simp only [Equiv.symm_apply_apply]def step : (d : ℕ) → Coins d → Equiv.Perm (Card d)  | 0, _ => 1  | d + 1, ξ => rotate (d + 1) * pairSwitch ξdef run (d : ℕ) : (t : ℕ) → (Fin t → Coins d) → Equiv.Perm (Card d)  | 0, _ => 1  | t + 1, ω => step d (ω (Fin.last t)) * run d t (fun i => ω i.castSucc)noncomputable def law (d t : ℕ) (g : Equiv.Perm (Card d)) : ℝ :=  (Fintype.card {ω : Fin t → Coins d // run d t ω = g} : ℝ) /    (Fintype.card (Fin t → Coins d) : ℝ)def Butterfly : ℕ → Type  | 0 => Unit  | d + 1 => (Card d → Bool) × (Bool → Butterfly d)def childLift {d : ℕ} (p : Bool → Equiv.Perm (Card d)) : Equiv.Perm (Card (d + 1)) where  toFun x := Fin.cons (x 0) (p (x 0) (Fin.tail x))  invFun x := Fin.cons (x 0) ((p (x 0)).symm (Fin.tail x))  left_inv x := by simp only [Fin.cons_zero, Fin.tail_cons, Equiv.symm_apply_apply, Fin.cons_self_tail]  right_inv x := by simp only [Fin.cons_zero, Fin.tail_cons, Equiv.apply_symm_apply, Fin.cons_self_tail]def butterflyPerm : (d : ℕ) → Butterfly d → Equiv.Perm (Card d)  | 0, _ => 1  | d + 1, b => pairSwitch b.1 * childLift (fun ε => butterflyPerm d (b.2 ε))noncomputable def finiteMean {Ω : Type*} [Fintype Ω] (f : Ω → ℝ) : ℝ :=  (∑ ω, f ω) / Fintype.card Ωdef SwitchIndex : ℕ → Type  | 0 => Empty  | d + 1 => Sum (Card d) (Bool × SwitchIndex d)instance (d : ℕ) : Fintype (SwitchIndex d) := by  induction d with  | zero => exact inferInstanceAs (Fintype Empty)  | succ d ih => exact inferInstanceAs (Fintype (Sum (Card d) (Bool × SwitchIndex d)))instance (d : ℕ) : DecidableEq (SwitchIndex d) := by  induction d with  | zero => exact inferInstanceAs (DecidableEq Empty)  | succ d ih => exact inferInstanceAs (DecidableEq (Sum (Card d) (Bool × SwitchIndex d)))def decodeButterfly : (d : ℕ) → (SwitchIndex d → Bool) → Butterfly d  | 0, _ => ()  | d + 1, ω => (fun y => ω (Sum.inl y), fun ε =>      decodeButterfly d (fun i => ω (Sum.inr (ε,i))))end Thorpnamespace Thorp.PairRoutingopen scoped BigOperatorsopen Filtervariable {ι α : Type*} [Fintype ι] [Fintype α] [DecidableEq α]noncomputable def tupleProbability {Ω β : Type*} [Fintype Ω] [DecidableEq β]    (P : Ω → Equiv.Perm β) (x y : ι → β) : ℝ := by  classical  exact finiteMean (fun ω => if ∀ i, P ω (x i) = y i then 1 else 0)end Thorp.PairRoutingnamespace Thorpopen scoped BigOperatorsopen Filterabbrev BenesCoins (d : ℕ) := (SwitchIndex d → Bool) × (SwitchIndex d → Bool)def palindromePerm (d : ℕ) (ω : BenesCoins d) : Equiv.Perm (Card d) :=  butterflyPerm d (decodeButterfly d ω.1) * (butterflyPerm d (decodeButterfly d ω.2)).symmnoncomputable def palindromeRowMoment (d : ℕ) {ι : Type*} [Fintype ι]    (e : ι ↪ Card d) (a : ℝ) : ℝ :=  finiteMean (fun f : ι ↪ Card d =>    ((Fintype.card (ι ↪ Card d):ℝ)*PairRouting.tupleProbability (palindromePerm d) e f)^(1+a))end Thorpnamespace Thorp.Spechtopen scoped BigOperators Classicalabbrev Cell (μ : YoungDiagram) := {x : ℕ × ℕ // x ∈ μ.cells}def row {μ : YoungDiagram} (x : Cell μ) : ℕ := x.1.1def col {μ : YoungDiagram} (x : Cell μ) : ℕ := x.1.2lemma row_lt_colLen {μ : YoungDiagram} (x : Cell μ) : row x < μ.colLen (col x) :=  YoungDiagram.mem_iff_lt_colLen.mp x.2noncomputable def rowIndex {μ : YoungDiagram} (x : Cell μ) : Fin (μ.colLen 0) :=  ⟨row x, (row_lt_colLen x).trans_le (μ.colLen_anti 0 (col x) (Nat.zero_le _))⟩abbrev Tabloid (μ : YoungDiagram) :=  {f : Cell μ → Fin (μ.colLen 0) // ∃ p : Equiv.Perm (Cell μ), f = rowIndex ∘ p}noncomputable instance (μ : YoungDiagram) : Fintype (Tabloid μ) := Fintype.ofFinite _noncomputable def baseTabloid (μ : YoungDiagram) : Tabloid μ := ⟨rowIndex, 1, rfl⟩noncomputable def tabloidAct {μ : YoungDiagram} (p : Equiv.Perm (Cell μ)) :    Equiv.Perm (Tabloid μ) where  toFun f := ⟨fun x => f.1 (p⁻¹ x), by    obtain ⟨q,hq⟩ := f.2    refine ⟨q*p⁻¹, ?_⟩    funext x    simp only [hq,Function.comp_apply,Equiv.Perm.mul_apply]⟩  invFun f := ⟨fun x => f.1 (p x), by    obtain ⟨q,hq⟩ := f.2    refine ⟨q*p, ?_⟩    funext x    simp only [hq,Function.comp_apply,Equiv.Perm.mul_apply]⟩  left_inv f := by apply Subtype.ext; funext x; simp  right_inv f := by apply Subtype.ext; funext x; simp@[simp] lemma tabloidAct_apply {μ : YoungDiagram} (p : Equiv.Perm (Cell μ))    (f : Tabloid μ) (x : Cell μ) : (tabloidAct p f).1 x = f.1 (p⁻¹ x) := rfl@[simp] lemma tabloidAct_one (μ : YoungDiagram) : tabloidAct (1 : Equiv.Perm (Cell μ)) = 1 := by  ext f x  rfl@[simp] lemma tabloidAct_mul {μ : YoungDiagram} (p q : Equiv.Perm (Cell μ)) :    tabloidAct (p*q) = tabloidAct p * tabloidAct q := by  ext f x  simp only [tabloidAct_apply, mul_inv_rev,Equiv.Perm.mul_apply]noncomputable def tabloidRep (μ : YoungDiagram) :    Representation ℂ (Equiv.Perm (Cell μ)) (Tabloid μ → ℂ) where  toFun p :=    { toFun := fun v f => v (tabloidAct p⁻¹ f)      map_add' := by intros; rfl      map_smul' := by intros; rfl }  map_one' := by ext v f; simp  map_mul' p q := by    ext v f    simp only [mul_inv_rev,tabloidAct_mul,Equiv.Perm.mul_apply]    rflnoncomputable def delta {μ : YoungDiagram} (f : Tabloid μ) : Tabloid μ → ℂ :=  fun g => if g=f then 1 else 0noncomputable def colGroup (μ : YoungDiagram) : Subgroup (Equiv.Perm (Cell μ)) where  carrier := {p | ∀ x, col (p x) = col x}  one_mem' := by intro x; rfl  mul_mem' := by intro p q hp hq x; exact (hp (q x)).trans (hq x)  inv_mem' := by intro p hp x; simpa using (hp (p⁻¹ x)).symmnoncomputable def permSign {α : Type*} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) : ℂ :=  ((Equiv.Perm.sign p : ℤ) : ℂ)sectionvariable {α V : Type*} [Fintype α] [DecidableEq α] [AddCommGroup V] [Module ℂ V]noncomputable def alternator (C : Subgroup (Equiv.Perm α))    (ρ : Representation ℂ (Equiv.Perm α) V) : Module.End ℂ V := by  classical  exact ∑ c : C, permSign (c : Equiv.Perm α) • ρ cendnoncomputable def polytabloid (μ : YoungDiagram) : Tabloid μ → ℂ :=  alternator (colGroup μ) (tabloidRep μ) (delta (baseTabloid μ))noncomputable def space (μ : YoungDiagram) : Submodule ℂ (Tabloid μ → ℂ) :=  Submodule.span ℂ (Set.range (fun p : Equiv.Perm (Cell μ) => tabloidRep μ p (polytabloid μ)))lemma orbit_mem_space (μ : YoungDiagram) (p : Equiv.Perm (Cell μ)) :    tabloidRep μ p (polytabloid μ) ∈ space μ := Submodule.subset_span ⟨p,rfl⟩lemma action_mem_space (μ : YoungDiagram) (p : Equiv.Perm (Cell μ))    (v : Tabloid μ → ℂ) (hv : v ∈ space μ) : tabloidRep μ p v ∈ space μ := by  induction hv using Submodule.span_induction with  | mem v hv =>    obtain ⟨q,rfl⟩ := hv    change ((tabloidRep μ p)*(tabloidRep μ q)) (polytabloid μ) ∈ space μ    rw [←map_mul]    exact orbit_mem_space μ (p*q)  | zero => simp  | add v w hv hw ihv ihw => simpa using (space μ).add_mem ihv ihw  | smul a v hv ih => simpa using (space μ).smul_mem a ihnoncomputable def subrepresentation (μ : YoungDiagram) : Subrepresentation (tabloidRep μ) :=  ⟨space μ, fun p v hv => action_mem_space μ p v hv⟩noncomputable def representation (μ : YoungDiagram) :    Representation ℂ (Equiv.Perm (Cell μ)) (space μ) :=  (subrepresentation μ).toRepresentationend Thorp.Spechtnamespace Thorp.PermutationHilbertopen scoped BigOperators ComplexConjugate Classicalopen Complexvariable {X : Type*} [Fintype X]abbrev H (X : Type*) [Fintype X] := EuclideanSpace ℂ Xend Thorp.PermutationHilbertnamespace Thorp.Spechtopen scoped BigOperators Classicalnoncomputable def hilbertEquiv (μ : YoungDiagram) :    (Tabloid μ → ℂ) ≃ₗ[ℂ] PermutationHilbert.H (Tabloid μ) :=  (WithLp.linearEquiv 2 ℂ (Tabloid μ → ℂ)).symmnoncomputable def hilbertSpace (μ : YoungDiagram) :    Submodule ℂ (PermutationHilbert.H (Tabloid μ)) := (space μ).map (hilbertEquiv μ).toLinearMapend Thorp.Spechtnamespace Thorp.UnitaryFinitesectionopen scoped BigOperators ComplexConjugate Classicalvariable {G : Type*} [Group G] [Fintype G]variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V]noncomputable def continuousRepresentation (ρ : Representation ℂ G V) : G →* (V →L[ℂ] V) where  toFun g := (ρ g).toContinuousLinearMap  map_one' := by ext v; simp  map_mul' g h := by ext v; simpendopen scoped BigOperators Classicalvariable {G : Type*} [Group G] [Fintype G]variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V]variable {Ω Ξ : Type*} [Fintype Ω] [Fintype Ξ]noncomputable def sampleOperator (ρ : Representation ℂ G V) (P : Ω → G) : V →L[ℂ] V :=  (Fintype.card Ω:ℂ)⁻¹ • ∑ ω,continuousRepresentation ρ (P ω)end Thorp.UnitaryFinitenamespace Thorp.Spechtopen scoped BigOperators Classicalnoncomputable def spaceHilbertEquiv (μ : YoungDiagram) : space μ ≃ₗ[ℂ] hilbertSpace μ :=  (hilbertEquiv μ).submoduleMap (space μ)noncomputable def unitaryRepresentation (μ : YoungDiagram) :    Representation ℂ (Equiv.Perm (Cell μ)) (hilbertSpace μ) :=  ((spaceHilbertEquiv μ).conjAlgEquiv ℂ).toMonoidHom.comp (representation μ)variable {α ι : Type*} [Fintype α] [Fintype ι]noncomputable def relabelledUnitary (μ : YoungDiagram) (e : α ≃ Cell μ) :    Representation ℂ (Equiv.Perm α) (hilbertSpace μ) :=  (unitaryRepresentation μ).comp e.permCongrHom.toMonoidHomend Thorp.Spechtnamespace Thorp.CasimirBoundsopen scoped BigOperators Classicalopen Filternoncomputable def levelScale (n k : ℕ) : ℝ :=  (k:ℝ) * (1 + Real.log ((n:ℝ)/(k:ℝ)))noncomputable def K (d : ℕ) (μ : YoungDiagram) (e : Card d ≃ Specht.Cell μ) :    Specht.hilbertSpace μ →L[ℂ] Specht.hilbertSpace μ :=  UnitaryFinite.sampleOperator (V := Specht.hilbertSpace μ)    (Specht.relabelledUnitary μ e) (palindromePerm d)noncomputable def traceMoment (d : ℕ) (μ : YoungDiagram)    (e : Card d ≃ Specht.Cell μ) (r : ℕ) : ℝ :=  (LinearMap.trace ℂ (Specht.hilbertSpace μ) ((K d μ e)^r).toLinearMap).renoncomputable def fromDistance (d t : ℕ) (σ : Equiv.Perm (Card d)) : ℝ :=  (1/2:ℝ) * ∑ g : Equiv.Perm (Card d),    |law d t (g*σ⁻¹) - 1/(Nat.factorial (2^d):ℝ)|def MainStatement : Prop :=  ∃ a C : ℝ, 0 < a ∧ 0 < C ∧    (∀ d k : ℕ, 1 ≤ k → k ≤ 2^d → ∀ x : Fin k ↪ Card d,      (palindromeRowMoment d x (1/64))^(64/65:ℝ) ≤        Real.exp (C*levelScale (2^d) k)) ∧    (∀ (d : ℕ) (μ : YoungDiagram) (e : Card d ≃ Specht.Cell μ),      0 < μ.card-μ.rowLen 0 →        ‖K d μ e‖ ≤ Real.exp (-a*levelScale (2^d) (μ.card-μ.rowLen 0)) ∧        (Module.finrank ℂ (Specht.space μ):ℝ) * traceMoment d μ e 65 ≤          Real.exp (C*levelScale (2^d) (μ.card-μ.rowLen 0))) ∧    (∃ l : ℕ, 0 < l ∧ ∀ starts : (d : ℕ) → Equiv.Perm (Card d),      Tendsto (fun d => fromDistance d (l*d) (starts d)) atTop (nhds 0))end Thorp.CasimirBoundsend ThorpNine.Casimirrun_cmd do  Lean.modifyEnv fun env => Lean.Meta.auxLemmasExt.setState env {}  let matcherCache := Lean.mkIdent    (Lean.mkPrivateNameCore `Lean.Meta.Match.Match `Lean.Meta.Match.matcherExt)  Lean.Elab.Command.elabCommand (← `(command|    run_cmd Lean.modifyEnv fun env => Lean.EnvExtension.setState $matcherCache env {}))namespace ThorpNine.Densenamespace Thorpopen scoped BigOperatorsopen Filterabbrev Card (d : ℕ) := Fin d → Booldef switchFun {d : ℕ} (ξ : Card d → Bool) (x : Card (d + 1)) : Card (d + 1) :=  Fin.cons (Bool.xor (x 0) (ξ (Fin.tail x))) (Fin.tail x)theorem switchFun_involutive {d : ℕ} (ξ : Card d → Bool) :    Function.Involutive (switchFun ξ) := by  intro x  funext i  refine Fin.cases ?_ (fun j => ?_) i  · simp only [switchFun, Fin.cons_zero, Fin.tail_cons]    cases x 0 <;> cases ξ (Fin.tail x) <;> rfl  · simp [switchFun, Fin.tail]def pairSwitch {d : ℕ} (ξ : Card d → Bool) : Equiv.Perm (Card (d + 1)) :=  { toFun := switchFun ξ    invFun := switchFun ξ    left_inv := switchFun_involutive ξ    right_inv := switchFun_involutive ξ }def Butterfly : ℕ → Type  | 0 => Unit  | d + 1 => (Card d → Bool) × (Bool → Butterfly d)def childLift {d : ℕ} (p : Bool → Equiv.Perm (Card d)) : Equiv.Perm (Card (d + 1)) where  toFun x := Fin.cons (x 0) (p (x 0) (Fin.tail x))  invFun x := Fin.cons (x 0) ((p (x 0)).symm (Fin.tail x))  left_inv x := by simp only [Fin.cons_zero, Fin.tail_cons, Equiv.symm_apply_apply, Fin.cons_self_tail]  right_inv x := by simp only [Fin.cons_zero, Fin.tail_cons, Equiv.apply_symm_apply, Fin.cons_self_tail]def butterflyPerm : (d : ℕ) → Butterfly d → Equiv.Perm (Card d)  | 0, _ => 1  | d + 1, b => pairSwitch b.1 * childLift (fun ε => butterflyPerm d (b.2 ε))noncomputable def finiteMean {Ω : Type*} [Fintype Ω] (f : Ω → ℝ) : ℝ :=  (∑ ω, f ω) / Fintype.card Ωdef SwitchIndex : ℕ → Type  | 0 => Empty  | d + 1 => Sum (Card d) (Bool × SwitchIndex d)instance (d : ℕ) : Fintype (SwitchIndex d) := by  induction d with  | zero => exact inferInstanceAs (Fintype Empty)  | succ d ih => exact inferInstanceAs (Fintype (Sum (Card d) (Bool × SwitchIndex d)))instance (d : ℕ) : DecidableEq (SwitchIndex d) := by  induction d with  | zero => exact inferInstanceAs (DecidableEq Empty)  | succ d ih => exact inferInstanceAs (DecidableEq (Sum (Card d) (Bool × SwitchIndex d)))def decodeButterfly : (d : ℕ) → (SwitchIndex d → Bool) → Butterfly d  | 0, _ => ()  | d + 1, ω => (fun y => ω (Sum.inl y), fun ε =>      decodeButterfly d (fun i => ω (Sum.inr (ε,i))))variable {α : Type*} [Fintype α] [DecidableEq α]noncomputable def orbitSet (p : Equiv.Perm α) (x : α) : Finset α :=  Finset.univ.filter (p.SameCycle x)end Thorpnamespace Thorp.RoutingNetworkopen scoped BigOperatorsopen Filtervariable {α ι : Type*} [Fintype α] [DecidableEq α] [Fintype ι] [DecidableEq ι]variable {A : ℕ}abbrev SelectedCycle (p : Equiv.Perm (α)) (S : Finset (α)) :=  {C : Finset (α) // (∃ x, C = orbitSet p x) ∧ C ⊆ S}noncomputable instance (p : Equiv.Perm (α)) (S : Finset (α)) :    Fintype (SelectedCycle p S) := Fintype.ofFinite _end Thorp.RoutingNetworknamespace Thorpopen scoped BigOperatorsopen Filtersectionvariable {β : Type*} [Fintype β] [DecidableEq β]def pairLayer (ξ : β → Bool) : Equiv.Perm (Bool × β) where  toFun x := (Bool.xor x.1 (ξ x.2),x.2)  invFun x := (Bool.xor x.1 (ξ x.2),x.2)  left_inv x := by    rcases x with ⟨b,x⟩    change (Bool.xor (Bool.xor b (ξ x)) (ξ x),x) = (b,x)    cases b <;> cases ξ x <;> rfl  right_inv x := by    rcases x with ⟨b,x⟩    change (Bool.xor (Bool.xor b (ξ x)) (ξ x),x) = (b,x)    cases b <;> cases ξ x <;> rflenddef coinStepEquiv (d : ℕ) : (SwitchIndex (d+1) → Bool) ≃    ((SwitchIndex d → Bool) × (SwitchIndex d → Bool)) × (Card d → Bool) where  toFun ω := ((fun i => ω (Sum.inr (false,i)),fun i => ω (Sum.inr (true,i))),    fun x => ω (Sum.inl x))  invFun ω := Sum.elim ω.2 (fun bi => if bi.1 then ω.1.2 bi.2 else ω.1.1 bi.2)  left_inv ω := by    funext i    cases i with    | inl x => rfl    | inr bi => cases bi with | mk b i => cases b <;> rfl  right_inv ω := by    rcases ω with ⟨⟨ω₀,ω₁⟩,ξ⟩    rfldef headTailEquiv (d : ℕ) : Card (d+1) ≃ Bool × Card d :=  (Fin.consEquiv (fun _ : Fin (d+1) => Bool)).symmend Thorpnamespace Thorp.CycleColoringopen scoped BigOperatorsopen Filtervariable {α : Type*} [Fintype α] [DecidableEq α]def alternatingPerm (p : Equiv.Perm α) : Equiv.Perm (Bool × α) where  toFun x := if x.1 then (false,p x.2) else (true,x.2)  invFun x := if x.1 then (false,x.2) else (true,p.symm x.2)  left_inv x := by rcases x with ⟨b,x⟩; cases b <;> simp  right_inv x := by rcases x with ⟨b,x⟩; cases b <;> simpend Thorp.CycleColoringnamespace Thorp.PairRoutingopen scoped BigOperatorsopen Filtervariable {ι α : Type*} [Fintype ι] [Fintype α] [DecidableEq α]def required (x : ι → Bool × α) (c : ι → Bool) (i : ι) : Bool := Bool.xor (x i).1 (c i)def Compatible (x : ι → Bool × α) (c : ι → Bool) : Prop :=  ∀ i j, (x i).2 = (x j).2 → required x c i = required x c jdef colors (x : ι → Bool × α) (ξ : α → Bool) (i : ι) : Bool :=  Bool.xor (x i).1 (ξ (x i).2)omit [Fintype ι] [Fintype α] [DecidableEq α] inlemma required_colors (x : ι → Bool × α) (ξ : α → Bool) (i : ι) :    required x (colors x ξ) i = ξ (x i).2 := by  simp only [required,colors]  cases (x i).1 <;> cases ξ (x i).2 <;> rflomit [Fintype ι] [Fintype α] [DecidableEq α] inlemma colors_compatible (x : ι → Bool × α) (ξ : α → Bool) : Compatible x (colors x ξ) := by  intro i j he  simp only [required_colors,he]omit [Fintype ι] [Fintype α] [DecidableEq α] inlemma Compatible.tail_injective {x : ι ↪ Bool × α} {c : ι → Bool} (hc : Compatible x c) (b : Bool) :    Function.Injective (fun i : {i : ι // c i = b} => (x i.val).2) := by  intro i j he  apply Subtype.ext  apply x.injective  apply Prod.ext  · have hh := hc i j he    simp only [required,i.property,j.property] at hh    cases h₀ : (x i.val).1 <;> cases h₁ : (x j.val).1 <;> cases b <;> simp_all  · exact hedef childEmbedding (x : ι ↪ Bool × α) (c : ι → Bool) (hc : Compatible x c) (b : Bool) :    {i : ι // c i = b} ↪ α := ⟨fun i => (x i.val).2,hc.tail_injective b⟩noncomputable def labelSet (e : ι ↪ Bool × α) : Finset (Bool × α) := Finset.univ.image edef alternatingProjection (p : Bool → Equiv.Perm α) : Equiv.Perm α := (p false).symm * p truenoncomputable def alternatingCycles (e : ι ↪ Bool × α) (p : Bool → Equiv.Perm α) : ℕ :=  Fintype.card (RoutingNetwork.SelectedCycle    (CycleColoring.alternatingPerm (alternatingProjection p)) (labelSet e))def switchedEmbedding (e : ι ↪ Bool × α) (ξ : α → Bool) : ι ↪ Bool × α :=  e.trans (pairLayer ξ).toEmbeddingend Thorp.PairRoutingnamespace Thorpopen scoped BigOperatorsopen Filterabbrev BenesCoins (d : ℕ) := (SwitchIndex d → Bool) × (SwitchIndex d → Bool)def palindromePerm (d : ℕ) (ω : BenesCoins d) : Equiv.Perm (Card d) :=  butterflyPerm d (decodeButterfly d ω.1) * (butterflyPerm d (decodeButterfly d ω.2)).symmdef sandwichShuffle {A B C D E F : Type*} :    ((A × B) × C) × ((D × E) × F) ≃ ((A × D) × (B × E)) × (F × C) where  toFun x := (((x.1.1.1,x.2.1.1),(x.1.1.2,x.2.1.2)),(x.2.2,x.1.2))  invFun x := (((x.1.1.1,x.1.2.1),x.2.2),((x.1.1.2,x.1.2.2),x.2.1))  left_inv _ := rfl  right_inv _ := rfldef benesStepEquiv (d : ℕ) : BenesCoins (d+1) ≃    (BenesCoins d × BenesCoins d) × ((Card d → Bool) × (Card d → Bool)) :=  (Equiv.prodCongr (coinStepEquiv d) (coinStepEquiv d)).trans sandwichShufflenoncomputable def palindromeCost : (d : ℕ) → {ι : Type*} → [Fintype ι] →    (ι ↪ Card d) → BenesCoins d → ℕ  | 0, _, _, _, _ => 0  | d+1, _, _, e, ω =>      let σ := benesStepEquiv d ω      let x := e.trans (headTailEquiv d).toEmbedding      let c := PairRouting.colors x σ.2.1      let hc := PairRouting.colors_compatible x σ.2.1      PairRouting.alternatingCycles (PairRouting.switchedEmbedding x σ.2.1)          (fun b => palindromePerm d (if b then σ.1.2 else σ.1.1)) +        palindromeCost d (PairRouting.childEmbedding x c hc false) σ.1.1 +        palindromeCost d (PairRouting.childEmbedding x c hc true) σ.1.2end Thorpnamespace Thorp.DenseTruncationopen scoped BigOperatorsdef AdmissibleCycleLaw (j : ℕ) (p : ℕ → ℝ) : Prop :=  (∀ l, 0 ≤ p l) ∧ HasSum p 1 ∧    ∀ l, p l ≤ ((l + 1 : ℕ) : ℝ) / (2 : ℝ) ^ (j - 1)noncomputable def h (j : ℕ) : ℝ :=  sSup {z : ℝ | ∃ p : ℕ → ℝ, AdmissibleCycleLaw j p ∧    z = ∑' l : ℕ, p l / ((l + 1 : ℕ) : ℝ)}def AdmissibleAllocation (ρ : ℝ) (x : ℕ → ℝ) : Prop :=  (∀ j, 0 ≤ x j ∧ x j ≤ 1) ∧    (∑' j : ℕ, x j / (2 : ℝ) ^ (j + 1)) ≤ ρnoncomputable def H (ρ : ℝ) : ℝ :=  sSup {z : ℝ | ∃ x : ℕ → ℝ, AdmissibleAllocation ρ x ∧    z = (1 / 2 : ℝ) * ∑' j : ℕ, h (j + 1) * x j}noncomputable def entropyCorrection (ρ : ℝ) : ℝ :=  (-ρ - (1 - ρ) * Real.log (1 - ρ)) / (ρ * Real.log 2)noncomputable def densityExponent (d r : ℕ) (x : Fin r ↪ Card d)    (ω : BenesCoins d) : ℝ :=  palindromeCost d x ω +    Real.log (((2 ^ d).descFactorial r : ℝ) / ((2 : ℝ) ^ d) ^ r) / Real.log 2def MainStatement : Prop :=  ∀ ρ : ℝ, 0 < ρ → ∀ ε : ℝ, 0 < ε →    ∃ c : ℝ, 0 < c ∧ ∀ d r : ℕ, 1 ≤ d → 1 ≤ r →      (r : ℝ) / (2 : ℝ) ^ d = ρ → ∀ x : Fin r ↪ Card d,      finiteMean (fun ω : BenesCoins d =>        if (r : ℝ) * (H ρ + entropyCorrection ρ + ε) < densityExponent d r x ω        then (1 : ℝ) else 0) ≤ Real.exp (-c * r)end Thorp.DenseTruncationend ThorpNine.Denserun_cmd do  Lean.modifyEnv fun env => Lean.Meta.auxLemmasExt.setState env {}  let matcherCache := Lean.mkIdent    (Lean.mkPrivateNameCore `Lean.Meta.Match.Match `Lean.Meta.Match.matcherExt)  Lean.Elab.Command.elabCommand (← `(command|    run_cmd Lean.modifyEnv fun env => Lean.EnvExtension.setState $matcherCache env {}))namespace ThorpNine.Contactnamespace Thorpopen scoped BigOperatorsopen Filterabbrev Card (d : ℕ) := Fin d → Booldef switchFun {d : ℕ} (ξ : Card d → Bool) (x : Card (d + 1)) : Card (d + 1) :=  Fin.cons (Bool.xor (x 0) (ξ (Fin.tail x))) (Fin.tail x)theorem switchFun_involutive {d : ℕ} (ξ : Card d → Bool) :    Function.Involutive (switchFun ξ) := by  intro x  funext i  refine Fin.cases ?_ (fun j => ?_) i  · simp only [switchFun, Fin.cons_zero, Fin.tail_cons]    cases x 0 <;> cases ξ (Fin.tail x) <;> rfl  · simp [switchFun, Fin.tail]def pairSwitch {d : ℕ} (ξ : Card d → Bool) : Equiv.Perm (Card (d + 1)) :=  { toFun := switchFun ξ    invFun := switchFun ξ    left_inv := switchFun_involutive ξ    right_inv := switchFun_involutive ξ }def Butterfly : ℕ → Type  | 0 => Unit  | d + 1 => (Card d → Bool) × (Bool → Butterfly d)def childLift {d : ℕ} (p : Bool → Equiv.Perm (Card d)) : Equiv.Perm (Card (d + 1)) where  toFun x := Fin.cons (x 0) (p (x 0) (Fin.tail x))  invFun x := Fin.cons (x 0) ((p (x 0)).symm (Fin.tail x))  left_inv x := by simp only [Fin.cons_zero, Fin.tail_cons, Equiv.symm_apply_apply, Fin.cons_self_tail]  right_inv x := by simp only [Fin.cons_zero, Fin.tail_cons, Equiv.apply_symm_apply, Fin.cons_self_tail]def butterflyPerm : (d : ℕ) → Butterfly d → Equiv.Perm (Card d)  | 0, _ => 1  | d + 1, b => pairSwitch b.1 * childLift (fun ε => butterflyPerm d (b.2 ε))def SwitchIndex : ℕ → Type  | 0 => Empty  | d + 1 => Sum (Card d) (Bool × SwitchIndex d)instance (d : ℕ) : Fintype (SwitchIndex d) := by  induction d with  | zero => exact inferInstanceAs (Fintype Empty)  | succ d ih => exact inferInstanceAs (Fintype (Sum (Card d) (Bool × SwitchIndex d)))instance (d : ℕ) : DecidableEq (SwitchIndex d) := by  induction d with  | zero => exact inferInstanceAs (DecidableEq Empty)  | succ d ih => exact inferInstanceAs (DecidableEq (Sum (Card d) (Bool × SwitchIndex d)))def decodeButterfly : (d : ℕ) → (SwitchIndex d → Bool) → Butterfly d  | 0, _ => ()  | d + 1, ω => (fun y => ω (Sum.inl y), fun ε =>      decodeButterfly d (fun i => ω (Sum.inr (ε,i))))end Thorpnamespace Thorp.Spechtopen scoped BigOperators Classicalabbrev Cell (μ : YoungDiagram) := {x : ℕ × ℕ // x ∈ μ.cells}def row {μ : YoungDiagram} (x : Cell μ) : ℕ := x.1.1def col {μ : YoungDiagram} (x : Cell μ) : ℕ := x.1.2lemma row_lt_colLen {μ : YoungDiagram} (x : Cell μ) : row x < μ.colLen (col x) :=  YoungDiagram.mem_iff_lt_colLen.mp x.2noncomputable def rowIndex {μ : YoungDiagram} (x : Cell μ) : Fin (μ.colLen 0) :=  ⟨row x, (row_lt_colLen x).trans_le (μ.colLen_anti 0 (col x) (Nat.zero_le _))⟩abbrev Tabloid (μ : YoungDiagram) :=  {f : Cell μ → Fin (μ.colLen 0) // ∃ p : Equiv.Perm (Cell μ), f = rowIndex ∘ p}noncomputable instance (μ : YoungDiagram) : Fintype (Tabloid μ) := Fintype.ofFinite _noncomputable def baseTabloid (μ : YoungDiagram) : Tabloid μ := ⟨rowIndex, 1, rfl⟩noncomputable def tabloidAct {μ : YoungDiagram} (p : Equiv.Perm (Cell μ)) :    Equiv.Perm (Tabloid μ) where  toFun f := ⟨fun x => f.1 (p⁻¹ x), by    obtain ⟨q,hq⟩ := f.2    refine ⟨q*p⁻¹, ?_⟩    funext x    simp only [hq,Function.comp_apply,Equiv.Perm.mul_apply]⟩  invFun f := ⟨fun x => f.1 (p x), by    obtain ⟨q,hq⟩ := f.2    refine ⟨q*p, ?_⟩    funext x    simp only [hq,Function.comp_apply,Equiv.Perm.mul_apply]⟩  left_inv f := by apply Subtype.ext; funext x; simp  right_inv f := by apply Subtype.ext; funext x; simp@[simp] lemma tabloidAct_apply {μ : YoungDiagram} (p : Equiv.Perm (Cell μ))    (f : Tabloid μ) (x : Cell μ) : (tabloidAct p f).1 x = f.1 (p⁻¹ x) := rfl@[simp] lemma tabloidAct_one (μ : YoungDiagram) : tabloidAct (1 : Equiv.Perm (Cell μ)) = 1 := by  ext f x  rfl@[simp] lemma tabloidAct_mul {μ : YoungDiagram} (p q : Equiv.Perm (Cell μ)) :    tabloidAct (p*q) = tabloidAct p * tabloidAct q := by  ext f x  simp only [tabloidAct_apply, mul_inv_rev,Equiv.Perm.mul_apply]noncomputable def tabloidRep (μ : YoungDiagram) :    Representation ℂ (Equiv.Perm (Cell μ)) (Tabloid μ → ℂ) where  toFun p :=    { toFun := fun v f => v (tabloidAct p⁻¹ f)      map_add' := by intros; rfl      map_smul' := by intros; rfl }  map_one' := by ext v f; simp  map_mul' p q := by    ext v f    simp only [mul_inv_rev,tabloidAct_mul,Equiv.Perm.mul_apply]    rflnoncomputable def delta {μ : YoungDiagram} (f : Tabloid μ) : Tabloid μ → ℂ :=  fun g => if g=f then 1 else 0noncomputable def colGroup (μ : YoungDiagram) : Subgroup (Equiv.Perm (Cell μ)) where  carrier := {p | ∀ x, col (p x) = col x}  one_mem' := by intro x; rfl  mul_mem' := by intro p q hp hq x; exact (hp (q x)).trans (hq x)  inv_mem' := by intro p hp x; simpa using (hp (p⁻¹ x)).symmnoncomputable def permSign {α : Type*} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) : ℂ :=  ((Equiv.Perm.sign p : ℤ) : ℂ)sectionvariable {α V : Type*} [Fintype α] [DecidableEq α] [AddCommGroup V] [Module ℂ V]noncomputable def alternator (C : Subgroup (Equiv.Perm α))    (ρ : Representation ℂ (Equiv.Perm α) V) : Module.End ℂ V := by  classical  exact ∑ c : C, permSign (c : Equiv.Perm α) • ρ cendnoncomputable def polytabloid (μ : YoungDiagram) : Tabloid μ → ℂ :=  alternator (colGroup μ) (tabloidRep μ) (delta (baseTabloid μ))noncomputable def space (μ : YoungDiagram) : Submodule ℂ (Tabloid μ → ℂ) :=  Submodule.span ℂ (Set.range (fun p : Equiv.Perm (Cell μ) => tabloidRep μ p (polytabloid μ)))lemma orbit_mem_space (μ : YoungDiagram) (p : Equiv.Perm (Cell μ)) :    tabloidRep μ p (polytabloid μ) ∈ space μ := Submodule.subset_span ⟨p,rfl⟩lemma action_mem_space (μ : YoungDiagram) (p : Equiv.Perm (Cell μ))    (v : Tabloid μ → ℂ) (hv : v ∈ space μ) : tabloidRep μ p v ∈ space μ := by  induction hv using Submodule.span_induction with  | mem v hv =>    obtain ⟨q,rfl⟩ := hv    change ((tabloidRep μ p)*(tabloidRep μ q)) (polytabloid μ) ∈ space μ    rw [←map_mul]    exact orbit_mem_space μ (p*q)  | zero => simp  | add v w hv hw ihv ihw => simpa using (space μ).add_mem ihv ihw  | smul a v hv ih => simpa using (space μ).smul_mem a ihnoncomputable def subrepresentation (μ : YoungDiagram) : Subrepresentation (tabloidRep μ) :=  ⟨space μ, fun p v hv => action_mem_space μ p v hv⟩noncomputable def representation (μ : YoungDiagram) :    Representation ℂ (Equiv.Perm (Cell μ)) (space μ) :=  (subrepresentation μ).toRepresentationend Thorp.Spechtnamespace Thorp.PermutationHilbertopen scoped BigOperators ComplexConjugate Classicalopen Complexvariable {X : Type*} [Fintype X]abbrev H (X : Type*) [Fintype X] := EuclideanSpace ℂ Xend Thorp.PermutationHilbertnamespace Thorp.Spechtopen scoped BigOperators Classicalnoncomputable def hilbertEquiv (μ : YoungDiagram) :    (Tabloid μ → ℂ) ≃ₗ[ℂ] PermutationHilbert.H (Tabloid μ) :=  (WithLp.linearEquiv 2 ℂ (Tabloid μ → ℂ)).symmnoncomputable def hilbertSpace (μ : YoungDiagram) :    Submodule ℂ (PermutationHilbert.H (Tabloid μ)) := (space μ).map (hilbertEquiv μ).toLinearMapend Thorp.Spechtnamespace Thorp.UnitaryFinitesectionopen scoped BigOperators ComplexConjugate Classicalvariable {G : Type*} [Group G] [Fintype G]variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V]noncomputable def continuousRepresentation (ρ : Representation ℂ G V) : G →* (V →L[ℂ] V) where  toFun g := (ρ g).toContinuousLinearMap  map_one' := by ext v; simp  map_mul' g h := by ext v; simpendopen scoped BigOperators Classicalvariable {G : Type*} [Group G] [Fintype G]variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V]variable {Ω Ξ : Type*} [Fintype Ω] [Fintype Ξ]noncomputable def sampleOperator (ρ : Representation ℂ G V) (P : Ω → G) : V →L[ℂ] V :=  (Fintype.card Ω:ℂ)⁻¹ • ∑ ω,continuousRepresentation ρ (P ω)end Thorp.UnitaryFinitenamespace Thorp.Spechtopen scoped BigOperators Classicalnoncomputable def spaceHilbertEquiv (μ : YoungDiagram) : space μ ≃ₗ[ℂ] hilbertSpace μ :=  (hilbertEquiv μ).submoduleMap (space μ)noncomputable def unitaryRepresentation (μ : YoungDiagram) :    Representation ℂ (Equiv.Perm (Cell μ)) (hilbertSpace μ) :=  ((spaceHilbertEquiv μ).conjAlgEquiv ℂ).toMonoidHom.comp (representation μ)variable {α ι : Type*} [Fintype α] [Fintype ι]noncomputable def relabelledUnitary (μ : YoungDiagram) (e : α ≃ Cell μ) :    Representation ℂ (Equiv.Perm α) (hilbertSpace μ) :=  (unitaryRepresentation μ).comp e.permCongrHom.toMonoidHomend Thorp.Spechtnamespace Thorp.SparseContactopen scoped BigOperatorsnoncomputable def sweepOperator (d : ℕ) (μ : YoungDiagram)    (e : Card d ≃ Specht.Cell μ) (reverse : Bool) :    Specht.hilbertSpace μ →L[ℂ] Specht.hilbertSpace μ :=  UnitaryFinite.sampleOperator (V := Specht.hilbertSpace μ) (Specht.relabelledUnitary μ e)    (fun ω : SwitchIndex d → Bool => if reverse then      (butterflyPerm d (decodeButterfly d ω))⁻¹ else butterflyPerm d (decodeButterfly d ω))def MainStatement : Prop :=  ∃ Cstar C : ℝ, 0 < Cstar ∧ 0 < C ∧    ∀ (d : ℕ), 1 ≤ d → ∀ (μ : YoungDiagram) (e : Card d ≃ Specht.Cell μ),      let k := μ.card - μ.rowLen 0      1 ≤ k → k < 2^d → ∀ reverse : Bool,        ‖sweepOperator d μ e reverse‖^2 ≤          min 1 ((Cstar * d * k / (2:ℝ)^d) ^ ((k:ℝ)/2)) ∧        (k = 1 → sweepOperator d μ e reverse = 0) ∧        ‖sweepOperator d μ e reverse‖^2 ≤          C^k * (1+(d:ℝ))^(C*k) * ((k:ℝ)/(2:ℝ)^d)^((k:ℝ)/2)end Thorp.SparseContactend ThorpNine.Contactrun_cmd do  Lean.modifyEnv fun env => Lean.Meta.auxLemmasExt.setState env {}  let matcherCache := Lean.mkIdent    (Lean.mkPrivateNameCore `Lean.Meta.Match.Match `Lean.Meta.Match.matcherExt)  Lean.Elab.Command.elabCommand (← `(command|    run_cmd Lean.modifyEnv fun env => Lean.EnvExtension.setState $matcherCache env {}))namespace ThorpNine.Harmonicnamespace Thorpopen scoped BigOperatorsopen Filterabbrev Card (d : ℕ) := Fin d → Booldef switchFun {d : ℕ} (ξ : Card d → Bool) (x : Card (d + 1)) : Card (d + 1) :=  Fin.cons (Bool.xor (x 0) (ξ (Fin.tail x))) (Fin.tail x)theorem switchFun_involutive {d : ℕ} (ξ : Card d → Bool) :    Function.Involutive (switchFun ξ) := by  intro x  funext i  refine Fin.cases ?_ (fun j => ?_) i  · simp only [switchFun, Fin.cons_zero, Fin.tail_cons]    cases x 0 <;> cases ξ (Fin.tail x) <;> rfl  · simp [switchFun, Fin.tail]def pairSwitch {d : ℕ} (ξ : Card d → Bool) : Equiv.Perm (Card (d + 1)) :=  { toFun := switchFun ξ    invFun := switchFun ξ    left_inv := switchFun_involutive ξ    right_inv := switchFun_involutive ξ }def Butterfly : ℕ → Type  | 0 => Unit  | d + 1 => (Card d → Bool) × (Bool → Butterfly d)def childLift {d : ℕ} (p : Bool → Equiv.Perm (Card d)) : Equiv.Perm (Card (d + 1)) where  toFun x := Fin.cons (x 0) (p (x 0) (Fin.tail x))  invFun x := Fin.cons (x 0) ((p (x 0)).symm (Fin.tail x))  left_inv x := by simp only [Fin.cons_zero, Fin.tail_cons, Equiv.symm_apply_apply, Fin.cons_self_tail]  right_inv x := by simp only [Fin.cons_zero, Fin.tail_cons, Equiv.apply_symm_apply, Fin.cons_self_tail]def butterflyPerm : (d : ℕ) → Butterfly d → Equiv.Perm (Card d)  | 0, _ => 1  | d + 1, b => pairSwitch b.1 * childLift (fun ε => butterflyPerm d (b.2 ε))noncomputable def finiteMean {Ω : Type*} [Fintype Ω] (f : Ω → ℝ) : ℝ :=  (∑ ω, f ω) / Fintype.card Ωdef SwitchIndex : ℕ → Type  | 0 => Empty  | d + 1 => Sum (Card d) (Bool × SwitchIndex d)instance (d : ℕ) : Fintype (SwitchIndex d) := by  induction d with  | zero => exact inferInstanceAs (Fintype Empty)  | succ d ih => exact inferInstanceAs (Fintype (Sum (Card d) (Bool × SwitchIndex d)))instance (d : ℕ) : DecidableEq (SwitchIndex d) := by  induction d with  | zero => exact inferInstanceAs (DecidableEq Empty)  | succ d ih => exact inferInstanceAs (DecidableEq (Sum (Card d) (Bool × SwitchIndex d)))def decodeButterfly : (d : ℕ) → (SwitchIndex d → Bool) → Butterfly d  | 0, _ => ()  | d + 1, ω => (fun y => ω (Sum.inl y), fun ε =>      decodeButterfly d (fun i => ω (Sum.inr (ε,i))))end Thorpnamespace Thorp.PairRoutingopen scoped BigOperatorsopen Filtervariable {ι α : Type*} [Fintype ι] [Fintype α] [DecidableEq α]noncomputable def tupleProbability {Ω β : Type*} [Fintype Ω] [DecidableEq β]    (P : Ω → Equiv.Perm β) (x y : ι → β) : ℝ := by  classical  exact finiteMean (fun ω => if ∀ i, P ω (x i) = y i then 1 else 0)end Thorp.PairRoutingnamespace Thorpopen scoped BigOperatorsopen Filterabbrev BenesCoins (d : ℕ) := (SwitchIndex d → Bool) × (SwitchIndex d → Bool)def palindromePerm (d : ℕ) (ω : BenesCoins d) : Equiv.Perm (Card d) :=  butterflyPerm d (decodeButterfly d ω.1) * (butterflyPerm d (decodeButterfly d ω.2)).symmend Thorpnamespace Thorp.Spechtopen scoped BigOperators Classicalabbrev Cell (μ : YoungDiagram) := {x : ℕ × ℕ // x ∈ μ.cells}def row {μ : YoungDiagram} (x : Cell μ) : ℕ := x.1.1def col {μ : YoungDiagram} (x : Cell μ) : ℕ := x.1.2lemma row_lt_colLen {μ : YoungDiagram} (x : Cell μ) : row x < μ.colLen (col x) :=  YoungDiagram.mem_iff_lt_colLen.mp x.2noncomputable def rowIndex {μ : YoungDiagram} (x : Cell μ) : Fin (μ.colLen 0) :=  ⟨row x, (row_lt_colLen x).trans_le (μ.colLen_anti 0 (col x) (Nat.zero_le _))⟩abbrev Tabloid (μ : YoungDiagram) :=  {f : Cell μ → Fin (μ.colLen 0) // ∃ p : Equiv.Perm (Cell μ), f = rowIndex ∘ p}noncomputable instance (μ : YoungDiagram) : Fintype (Tabloid μ) := Fintype.ofFinite _noncomputable def baseTabloid (μ : YoungDiagram) : Tabloid μ := ⟨rowIndex, 1, rfl⟩noncomputable def tabloidAct {μ : YoungDiagram} (p : Equiv.Perm (Cell μ)) :    Equiv.Perm (Tabloid μ) where  toFun f := ⟨fun x => f.1 (p⁻¹ x), by    obtain ⟨q,hq⟩ := f.2    refine ⟨q*p⁻¹, ?_⟩    funext x    simp only [hq,Function.comp_apply,Equiv.Perm.mul_apply]⟩  invFun f := ⟨fun x => f.1 (p x), by    obtain ⟨q,hq⟩ := f.2    refine ⟨q*p, ?_⟩    funext x    simp only [hq,Function.comp_apply,Equiv.Perm.mul_apply]⟩  left_inv f := by apply Subtype.ext; funext x; simp  right_inv f := by apply Subtype.ext; funext x; simp@[simp] lemma tabloidAct_apply {μ : YoungDiagram} (p : Equiv.Perm (Cell μ))    (f : Tabloid μ) (x : Cell μ) : (tabloidAct p f).1 x = f.1 (p⁻¹ x) := rfl@[simp] lemma tabloidAct_one (μ : YoungDiagram) : tabloidAct (1 : Equiv.Perm (Cell μ)) = 1 := by  ext f x  rfl@[simp] lemma tabloidAct_mul {μ : YoungDiagram} (p q : Equiv.Perm (Cell μ)) :    tabloidAct (p*q) = tabloidAct p * tabloidAct q := by  ext f x  simp only [tabloidAct_apply, mul_inv_rev,Equiv.Perm.mul_apply]noncomputable def tabloidRep (μ : YoungDiagram) :    Representation ℂ (Equiv.Perm (Cell μ)) (Tabloid μ → ℂ) where  toFun p :=    { toFun := fun v f => v (tabloidAct p⁻¹ f)      map_add' := by intros; rfl      map_smul' := by intros; rfl }  map_one' := by ext v f; simp  map_mul' p q := by    ext v f    simp only [mul_inv_rev,tabloidAct_mul,Equiv.Perm.mul_apply]    rflnoncomputable def delta {μ : YoungDiagram} (f : Tabloid μ) : Tabloid μ → ℂ :=  fun g => if g=f then 1 else 0noncomputable def colGroup (μ : YoungDiagram) : Subgroup (Equiv.Perm (Cell μ)) where  carrier := {p | ∀ x, col (p x) = col x}  one_mem' := by intro x; rfl  mul_mem' := by intro p q hp hq x; exact (hp (q x)).trans (hq x)  inv_mem' := by intro p hp x; simpa using (hp (p⁻¹ x)).symmnoncomputable def permSign {α : Type*} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) : ℂ :=  ((Equiv.Perm.sign p : ℤ) : ℂ)sectionvariable {α V : Type*} [Fintype α] [DecidableEq α] [AddCommGroup V] [Module ℂ V]noncomputable def alternator (C : Subgroup (Equiv.Perm α))    (ρ : Representation ℂ (Equiv.Perm α) V) : Module.End ℂ V := by  classical  exact ∑ c : C, permSign (c : Equiv.Perm α) • ρ cendnoncomputable def polytabloid (μ : YoungDiagram) : Tabloid μ → ℂ :=  alternator (colGroup μ) (tabloidRep μ) (delta (baseTabloid μ))noncomputable def space (μ : YoungDiagram) : Submodule ℂ (Tabloid μ → ℂ) :=  Submodule.span ℂ (Set.range (fun p : Equiv.Perm (Cell μ) => tabloidRep μ p (polytabloid μ)))lemma orbit_mem_space (μ : YoungDiagram) (p : Equiv.Perm (Cell μ)) :    tabloidRep μ p (polytabloid μ) ∈ space μ := Submodule.subset_span ⟨p,rfl⟩lemma action_mem_space (μ : YoungDiagram) (p : Equiv.Perm (Cell μ))    (v : Tabloid μ → ℂ) (hv : v ∈ space μ) : tabloidRep μ p v ∈ space μ := by  induction hv using Submodule.span_induction with  | mem v hv =>    obtain ⟨q,rfl⟩ := hv    change ((tabloidRep μ p)*(tabloidRep μ q)) (polytabloid μ) ∈ space μ    rw [←map_mul]    exact orbit_mem_space μ (p*q)  | zero => simp  | add v w hv hw ihv ihw => simpa using (space μ).add_mem ihv ihw  | smul a v hv ih => simpa using (space μ).smul_mem a ihnoncomputable def subrepresentation (μ : YoungDiagram) : Subrepresentation (tabloidRep μ) :=  ⟨space μ, fun p v hv => action_mem_space μ p v hv⟩noncomputable def representation (μ : YoungDiagram) :    Representation ℂ (Equiv.Perm (Cell μ)) (space μ) :=  (subrepresentation μ).toRepresentationend Thorp.Spechtnamespace Thorp.PermutationHilbertopen scoped BigOperators ComplexConjugate Classicalopen Complexvariable {X : Type*} [Fintype X]abbrev H (X : Type*) [Fintype X] := EuclideanSpace ℂ Xend Thorp.PermutationHilbertnamespace Thorp.Spechtopen scoped BigOperators Classicalnoncomputable def hilbertEquiv (μ : YoungDiagram) :    (Tabloid μ → ℂ) ≃ₗ[ℂ] PermutationHilbert.H (Tabloid μ) :=  (WithLp.linearEquiv 2 ℂ (Tabloid μ → ℂ)).symmnoncomputable def hilbertSpace (μ : YoungDiagram) :    Submodule ℂ (PermutationHilbert.H (Tabloid μ)) := (space μ).map (hilbertEquiv μ).toLinearMapend Thorp.Spechtnamespace Thorp.UnitaryFinitesectionopen scoped BigOperators ComplexConjugate Classicalvariable {G : Type*} [Group G] [Fintype G]variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V]noncomputable def continuousRepresentation (ρ : Representation ℂ G V) : G →* (V →L[ℂ] V) where  toFun g := (ρ g).toContinuousLinearMap  map_one' := by ext v; simp  map_mul' g h := by ext v; simpendopen scoped BigOperators Classicalvariable {G : Type*} [Group G] [Fintype G]variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V]variable {Ω Ξ : Type*} [Fintype Ω] [Fintype Ξ]noncomputable def sampleOperator (ρ : Representation ℂ G V) (P : Ω → G) : V →L[ℂ] V :=  (Fintype.card Ω:ℂ)⁻¹ • ∑ ω,continuousRepresentation ρ (P ω)end Thorp.UnitaryFinitenamespace Thorp.Spechtopen scoped BigOperators Classicalnoncomputable def spaceHilbertEquiv (μ : YoungDiagram) : space μ ≃ₗ[ℂ] hilbertSpace μ :=  (hilbertEquiv μ).submoduleMap (space μ)noncomputable def unitaryRepresentation (μ : YoungDiagram) :    Representation ℂ (Equiv.Perm (Cell μ)) (hilbertSpace μ) :=  ((spaceHilbertEquiv μ).conjAlgEquiv ℂ).toMonoidHom.comp (representation μ)variable {α ι : Type*} [Fintype α] [Fintype ι]noncomputable def relabelledUnitary (μ : YoungDiagram) (e : α ≃ Cell μ) :    Representation ℂ (Equiv.Perm α) (hilbertSpace μ) :=  (unitaryRepresentation μ).comp e.permCongrHom.toMonoidHomend Thorp.Spechtnamespace Thorp.SparseContactopen scoped BigOperatorsnoncomputable def sweepOperator (d : ℕ) (μ : YoungDiagram)    (e : Card d ≃ Specht.Cell μ) (reverse : Bool) :    Specht.hilbertSpace μ →L[ℂ] Specht.hilbertSpace μ :=  UnitaryFinite.sampleOperator (V := Specht.hilbertSpace μ) (Specht.relabelledUnitary μ e)    (fun ω : SwitchIndex d → Bool => if reverse then      (butterflyPerm d (decodeButterfly d ω))⁻¹ else butterflyPerm d (decodeButterfly d ω))end Thorp.SparseContactnamespace Thorp.StrongSmoothingdef coordinateRelabel (d : ℕ) (order : Equiv.Perm (Fin d)) : Equiv.Perm (Card d) where  toFun x := fun i => x (order.symm i)  invFun x := fun i => x (order i)  left_inv x := by funext i; simp  right_inv x := by funext i; simpdef sweep (d : ℕ) (order : Equiv.Perm (Fin d)) (ω : SwitchIndex d → Bool) :    Equiv.Perm (Card d) :=  coordinateRelabel d order * butterflyPerm d (decodeButterfly d ω) *    (coordinateRelabel d order)⁻¹abbrev Tuples (d l : ℕ) := Fin l ↪ Card dnoncomputable def sweepKernel (d l : ℕ) (order : Equiv.Perm (Fin d)) :    Matrix (Tuples d l) (Tuples d l) ℝ :=  fun x y => PairRouting.tupleProbability (sweep d order) x ynoncomputable def reflectedKernel (d l : ℕ) (order : Equiv.Perm (Fin d)) (orientation : Bool) :    Matrix (Tuples d l) (Tuples d l) ℝ :=  let A := sweepKernel d l order  if orientation then A * A.transpose else A.transpose * Aend Thorp.StrongSmoothingnamespace Thorp.StrongTailopen scoped BigOperators Classicalopen Spechtdef tailDiagram (μ : YoungDiagram) : YoungDiagram :=  YoungDiagram.ofRowLens μ.rowLens.tail μ.rowLens_sorted.pairwise.tail.sortedGEend Thorp.StrongTailnamespace Thorp.Casimiropen scoped BigOperators Classicalopen Filternoncomputable def levelScale (n k : ℕ) : ℝ :=  (k:ℝ) * (1 + Real.log ((n:ℝ)/(k:ℝ)))noncomputable def K (d : ℕ) (μ : YoungDiagram) (e : Card d ≃ Specht.Cell μ) :    Specht.hilbertSpace μ →L[ℂ] Specht.hilbertSpace μ :=  UnitaryFinite.sampleOperator (V := Specht.hilbertSpace μ)    (Specht.relabelledUnitary μ e) (palindromePerm d)end Thorp.Casimirnamespace Thorp.HarmonicBoundsopen scoped BigOperators Classicalopen _root_.OAI.ThorpNine.Harmonic.Thorp.Casimir StrongSmoothingabbrev tail (μ : YoungDiagram) := StrongTail.tailDiagram μnoncomputable def W (d : ℕ) (μ : YoungDiagram) (e : Card d ≃ Specht.Cell μ) : ℝ := ‖K d μ e‖noncomputable def tupleTrace (d k : ℕ) (order : Equiv.Perm (Fin d)) (rev : Bool) (p : ℕ) : ℝ :=  Matrix.trace ((reflectedKernel d k order rev)^p)def MainStatement : Prop :=  ∃ c C ζ δ cTail c₁ c₂ : ℝ, ∃ p₀ : ℕ,    0<c ∧ 0<C ∧ 0<ζ ∧ 0<δ ∧ δ<1 ∧ 0<cTail ∧ 0<c₁ ∧ 0<c₂ ∧ 0<p₀ ∧    (∀ (d : ℕ) (μ : YoungDiagram) (e : Card d ≃ Specht.Cell μ),      0<μ.card-μ.rowLen 0 →      let L := levelScale (2^d) (μ.card-μ.rowLen 0)      let f : ℝ := Module.finrank ℂ (Specht.space (tail μ))      let D : ℝ := Module.finrank ℂ (Specht.space μ)      W d μ e ≤ Real.exp (-c*L) ∧      W d μ e ≤ Real.exp (C*L)*f^(-ζ) ∧      (∀ rev : Bool, ‖SparseContact.sweepOperator d μ e rev‖ ≤        Real.exp (-cTail*(L+Real.log f))) ∧      W d μ e ≤ Real.exp (-c₁*L)*D^(-c₂)) ∧    (∀ d k : ℕ, 1≤k → k≤2^d → ∀ (order : Equiv.Perm (Fin d)) (rev : Bool),      (∀ x : Tuples d k,        finiteMean (fun y => ((Fintype.card (Tuples d k):ℝ)*          reflectedKernel d k order rev x y)^(1+δ)) ≤        Real.exp (C*levelScale (2^d) k)) ∧      tupleTrace d k order rev p₀ ≤ Real.exp (C*levelScale (2^d) k))end Thorp.HarmonicBoundsend ThorpNine.Harmonicrun_cmd do  Lean.modifyEnv fun env => Lean.Meta.auxLemmasExt.setState env {}  let matcherCache := Lean.mkIdent    (Lean.mkPrivateNameCore `Lean.Meta.Match.Match `Lean.Meta.Match.matcherExt)  Lean.Elab.Command.elabCommand (← `(command|    run_cmd Lean.modifyEnv fun env => Lean.EnvExtension.setState $matcherCache env {}))namespace ThorpNine.Smoothingnamespace Thorpopen scoped BigOperatorsopen Filterabbrev Card (d : ℕ) := Fin d → Booldef switchFun {d : ℕ} (ξ : Card d → Bool) (x : Card (d + 1)) : Card (d + 1) :=  Fin.cons (Bool.xor (x 0) (ξ (Fin.tail x))) (Fin.tail x)theorem switchFun_involutive {d : ℕ} (ξ : Card d → Bool) :    Function.Involutive (switchFun ξ) := by  intro x  funext i  refine Fin.cases ?_ (fun j => ?_) i  · simp only [switchFun, Fin.cons_zero, Fin.tail_cons]    cases x 0 <;> cases ξ (Fin.tail x) <;> rfl  · simp [switchFun, Fin.tail]def pairSwitch {d : ℕ} (ξ : Card d → Bool) : Equiv.Perm (Card (d + 1)) :=  { toFun := switchFun ξ    invFun := switchFun ξ    left_inv := switchFun_involutive ξ    right_inv := switchFun_involutive ξ }def Butterfly : ℕ → Type  | 0 => Unit  | d + 1 => (Card d → Bool) × (Bool → Butterfly d)def childLift {d : ℕ} (p : Bool → Equiv.Perm (Card d)) : Equiv.Perm (Card (d + 1)) where  toFun x := Fin.cons (x 0) (p (x 0) (Fin.tail x))  invFun x := Fin.cons (x 0) ((p (x 0)).symm (Fin.tail x))  left_inv x := by simp only [Fin.cons_zero, Fin.tail_cons, Equiv.symm_apply_apply, Fin.cons_self_tail]  right_inv x := by simp only [Fin.cons_zero, Fin.tail_cons, Equiv.apply_symm_apply, Fin.cons_self_tail]def butterflyPerm : (d : ℕ) → Butterfly d → Equiv.Perm (Card d)  | 0, _ => 1  | d + 1, b => pairSwitch b.1 * childLift (fun ε => butterflyPerm d (b.2 ε))noncomputable def finiteMean {Ω : Type*} [Fintype Ω] (f : Ω → ℝ) : ℝ :=  (∑ ω, f ω) / Fintype.card Ωdef SwitchIndex : ℕ → Type  | 0 => Empty  | d + 1 => Sum (Card d) (Bool × SwitchIndex d)instance (d : ℕ) : Fintype (SwitchIndex d) := by  induction d with  | zero => exact inferInstanceAs (Fintype Empty)  | succ d ih => exact inferInstanceAs (Fintype (Sum (Card d) (Bool × SwitchIndex d)))instance (d : ℕ) : DecidableEq (SwitchIndex d) := by  induction d with  | zero => exact inferInstanceAs (DecidableEq Empty)  | succ d ih => exact inferInstanceAs (DecidableEq (Sum (Card d) (Bool × SwitchIndex d)))def decodeButterfly : (d : ℕ) → (SwitchIndex d → Bool) → Butterfly d  | 0, _ => ()  | d + 1, ω => (fun y => ω (Sum.inl y), fun ε =>      decodeButterfly d (fun i => ω (Sum.inr (ε,i))))end Thorpnamespace Thorp.PairRoutingopen scoped BigOperatorsopen Filtervariable {ι α : Type*} [Fintype ι] [Fintype α] [DecidableEq α]noncomputable def tupleProbability {Ω β : Type*} [Fintype Ω] [DecidableEq β]    (P : Ω → Equiv.Perm β) (x y : ι → β) : ℝ := by  classical  exact finiteMean (fun ω => if ∀ i, P ω (x i) = y i then 1 else 0)end Thorp.PairRoutingnamespace Thorp.StrongSmoothingdef coordinateRelabel (d : ℕ) (order : Equiv.Perm (Fin d)) : Equiv.Perm (Card d) where  toFun x := fun i => x (order.symm i)  invFun x := fun i => x (order i)  left_inv x := by funext i; simp  right_inv x := by funext i; simpdef sweep (d : ℕ) (order : Equiv.Perm (Fin d)) (ω : SwitchIndex d → Bool) :    Equiv.Perm (Card d) :=  coordinateRelabel d order * butterflyPerm d (decodeButterfly d ω) *    (coordinateRelabel d order)⁻¹abbrev Tuples (d l : ℕ) := Fin l ↪ Card dnoncomputable def sweepKernel (d l : ℕ) (order : Equiv.Perm (Fin d)) :    Matrix (Tuples d l) (Tuples d l) ℝ :=  fun x y => PairRouting.tupleProbability (sweep d order) x ynoncomputable def reflectedKernel (d l : ℕ) (order : Equiv.Perm (Fin d)) (orientation : Bool) :    Matrix (Tuples d l) (Tuples d l) ℝ :=  let A := sweepKernel d l order  if orientation then A * A.transpose else A.transpose * Anoncomputable def regularAbsoluteEvenTrace (d : ℕ) (order : Equiv.Perm (Fin d)) (u : ℕ) : ℝ :=  Matrix.trace ((reflectedKernel d (2^d) order false)^u)def MainStatement : Prop :=  ∃ u : ℕ, 1 ≤ u ∧ ∃ C : ℝ,    (∀ d l : ℕ, l ≤ 2^d → ∀ order : Equiv.Perm (Fin d), ∀ orientation : Bool,      ∀ x y : Tuples d l,        ((reflectedKernel d l order orientation)^u) x y ≤          Real.exp (C*l)/((2^d).descFactorial l:ℝ)) ∧    (∀ d : ℕ, ∀ order : Equiv.Perm (Fin d),      regularAbsoluteEvenTrace d order u ≤ Real.exp (C*(2:ℝ)^d))end Thorp.StrongSmoothingend ThorpNine.Smoothingrun_cmd do  Lean.modifyEnv fun env => Lean.Meta.auxLemmasExt.setState env {}  let matcherCache := Lean.mkIdent    (Lean.mkPrivateNameCore `Lean.Meta.Match.Match `Lean.Meta.Match.matcherExt)  Lean.Elab.Command.elabCommand (← `(command|    run_cmd Lean.modifyEnv fun env => Lean.EnvExtension.setState $matcherCache env {}))namespace ThorpNine.Tailnamespace Thorpopen scoped BigOperatorsopen Filterabbrev Card (d : ℕ) := Fin d → Booldef switchFun {d : ℕ} (ξ : Card d → Bool) (x : Card (d + 1)) : Card (d + 1) :=  Fin.cons (Bool.xor (x 0) (ξ (Fin.tail x))) (Fin.tail x)theorem switchFun_involutive {d : ℕ} (ξ : Card d → Bool) :    Function.Involutive (switchFun ξ) := by  intro x  funext i  refine Fin.cases ?_ (fun j => ?_) i  · simp only [switchFun, Fin.cons_zero, Fin.tail_cons]    cases x 0 <;> cases ξ (Fin.tail x) <;> rfl  · simp [switchFun, Fin.tail]def pairSwitch {d : ℕ} (ξ : Card d → Bool) : Equiv.Perm (Card (d + 1)) :=  { toFun := switchFun ξ    invFun := switchFun ξ    left_inv := switchFun_involutive ξ    right_inv := switchFun_involutive ξ }def Butterfly : ℕ → Type  | 0 => Unit  | d + 1 => (Card d → Bool) × (Bool → Butterfly d)def childLift {d : ℕ} (p : Bool → Equiv.Perm (Card d)) : Equiv.Perm (Card (d + 1)) where  toFun x := Fin.cons (x 0) (p (x 0) (Fin.tail x))  invFun x := Fin.cons (x 0) ((p (x 0)).symm (Fin.tail x))  left_inv x := by simp only [Fin.cons_zero, Fin.tail_cons, Equiv.symm_apply_apply, Fin.cons_self_tail]  right_inv x := by simp only [Fin.cons_zero, Fin.tail_cons, Equiv.apply_symm_apply, Fin.cons_self_tail]def butterflyPerm : (d : ℕ) → Butterfly d → Equiv.Perm (Card d)  | 0, _ => 1  | d + 1, b => pairSwitch b.1 * childLift (fun ε => butterflyPerm d (b.2 ε))noncomputable def finiteMean {Ω : Type*} [Fintype Ω] (f : Ω → ℝ) : ℝ :=  (∑ ω, f ω) / Fintype.card Ωdef SwitchIndex : ℕ → Type  | 0 => Empty  | d + 1 => Sum (Card d) (Bool × SwitchIndex d)instance (d : ℕ) : Fintype (SwitchIndex d) := by  induction d with  | zero => exact inferInstanceAs (Fintype Empty)  | succ d ih => exact inferInstanceAs (Fintype (Sum (Card d) (Bool × SwitchIndex d)))instance (d : ℕ) : DecidableEq (SwitchIndex d) := by  induction d with  | zero => exact inferInstanceAs (DecidableEq Empty)  | succ d ih => exact inferInstanceAs (DecidableEq (Sum (Card d) (Bool × SwitchIndex d)))def decodeButterfly : (d : ℕ) → (SwitchIndex d → Bool) → Butterfly d  | 0, _ => ()  | d + 1, ω => (fun y => ω (Sum.inl y), fun ε =>      decodeButterfly d (fun i => ω (Sum.inr (ε,i))))end Thorpnamespace Thorp.PairRoutingopen scoped BigOperatorsopen Filtervariable {ι α : Type*} [Fintype ι] [Fintype α] [DecidableEq α]noncomputable def tupleProbability {Ω β : Type*} [Fintype Ω] [DecidableEq β]    (P : Ω → Equiv.Perm β) (x y : ι → β) : ℝ := by  classical  exact finiteMean (fun ω => if ∀ i, P ω (x i) = y i then 1 else 0)end Thorp.PairRoutingnamespace Thorp.Spechtopen scoped BigOperators Classicalabbrev Cell (μ : YoungDiagram) := {x : ℕ × ℕ // x ∈ μ.cells}def row {μ : YoungDiagram} (x : Cell μ) : ℕ := x.1.1def col {μ : YoungDiagram} (x : Cell μ) : ℕ := x.1.2lemma row_lt_colLen {μ : YoungDiagram} (x : Cell μ) : row x < μ.colLen (col x) :=  YoungDiagram.mem_iff_lt_colLen.mp x.2noncomputable def rowIndex {μ : YoungDiagram} (x : Cell μ) : Fin (μ.colLen 0) :=  ⟨row x, (row_lt_colLen x).trans_le (μ.colLen_anti 0 (col x) (Nat.zero_le _))⟩abbrev Tabloid (μ : YoungDiagram) :=  {f : Cell μ → Fin (μ.colLen 0) // ∃ p : Equiv.Perm (Cell μ), f = rowIndex ∘ p}noncomputable instance (μ : YoungDiagram) : Fintype (Tabloid μ) := Fintype.ofFinite _noncomputable def baseTabloid (μ : YoungDiagram) : Tabloid μ := ⟨rowIndex, 1, rfl⟩noncomputable def tabloidAct {μ : YoungDiagram} (p : Equiv.Perm (Cell μ)) :    Equiv.Perm (Tabloid μ) where  toFun f := ⟨fun x => f.1 (p⁻¹ x), by    obtain ⟨q,hq⟩ := f.2    refine ⟨q*p⁻¹, ?_⟩    funext x    simp only [hq,Function.comp_apply,Equiv.Perm.mul_apply]⟩  invFun f := ⟨fun x => f.1 (p x), by    obtain ⟨q,hq⟩ := f.2    refine ⟨q*p, ?_⟩    funext x    simp only [hq,Function.comp_apply,Equiv.Perm.mul_apply]⟩  left_inv f := by apply Subtype.ext; funext x; simp  right_inv f := by apply Subtype.ext; funext x; simp@[simp] lemma tabloidAct_apply {μ : YoungDiagram} (p : Equiv.Perm (Cell μ))    (f : Tabloid μ) (x : Cell μ) : (tabloidAct p f).1 x = f.1 (p⁻¹ x) := rfl@[simp] lemma tabloidAct_one (μ : YoungDiagram) : tabloidAct (1 : Equiv.Perm (Cell μ)) = 1 := by  ext f x  rfl@[simp] lemma tabloidAct_mul {μ : YoungDiagram} (p q : Equiv.Perm (Cell μ)) :    tabloidAct (p*q) = tabloidAct p * tabloidAct q := by  ext f x  simp only [tabloidAct_apply, mul_inv_rev,Equiv.Perm.mul_apply]noncomputable def tabloidRep (μ : YoungDiagram) :    Representation ℂ (Equiv.Perm (Cell μ)) (Tabloid μ → ℂ) where  toFun p :=    { toFun := fun v f => v (tabloidAct p⁻¹ f)      map_add' := by intros; rfl      map_smul' := by intros; rfl }  map_one' := by ext v f; simp  map_mul' p q := by    ext v f    simp only [mul_inv_rev,tabloidAct_mul,Equiv.Perm.mul_apply]    rflnoncomputable def delta {μ : YoungDiagram} (f : Tabloid μ) : Tabloid μ → ℂ :=  fun g => if g=f then 1 else 0noncomputable def colGroup (μ : YoungDiagram) : Subgroup (Equiv.Perm (Cell μ)) where  carrier := {p | ∀ x, col (p x) = col x}  one_mem' := by intro x; rfl  mul_mem' := by intro p q hp hq x; exact (hp (q x)).trans (hq x)  inv_mem' := by intro p hp x; simpa using (hp (p⁻¹ x)).symmnoncomputable def permSign {α : Type*} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) : ℂ :=  ((Equiv.Perm.sign p : ℤ) : ℂ)sectionvariable {α V : Type*} [Fintype α] [DecidableEq α] [AddCommGroup V] [Module ℂ V]noncomputable def alternator (C : Subgroup (Equiv.Perm α))    (ρ : Representation ℂ (Equiv.Perm α) V) : Module.End ℂ V := by  classical  exact ∑ c : C, permSign (c : Equiv.Perm α) • ρ cendnoncomputable def polytabloid (μ : YoungDiagram) : Tabloid μ → ℂ :=  alternator (colGroup μ) (tabloidRep μ) (delta (baseTabloid μ))noncomputable def space (μ : YoungDiagram) : Submodule ℂ (Tabloid μ → ℂ) :=  Submodule.span ℂ (Set.range (fun p : Equiv.Perm (Cell μ) => tabloidRep μ p (polytabloid μ)))lemma orbit_mem_space (μ : YoungDiagram) (p : Equiv.Perm (Cell μ)) :    tabloidRep μ p (polytabloid μ) ∈ space μ := Submodule.subset_span ⟨p,rfl⟩lemma action_mem_space (μ : YoungDiagram) (p : Equiv.Perm (Cell μ))    (v : Tabloid μ → ℂ) (hv : v ∈ space μ) : tabloidRep μ p v ∈ space μ := by  induction hv using Submodule.span_induction with  | mem v hv =>    obtain ⟨q,rfl⟩ := hv    change ((tabloidRep μ p)*(tabloidRep μ q)) (polytabloid μ) ∈ space μ    rw [←map_mul]    exact orbit_mem_space μ (p*q)  | zero => simp  | add v w hv hw ihv ihw => simpa using (space μ).add_mem ihv ihw  | smul a v hv ih => simpa using (space μ).smul_mem a ihnoncomputable def subrepresentation (μ : YoungDiagram) : Subrepresentation (tabloidRep μ) :=  ⟨space μ, fun p v hv => action_mem_space μ p v hv⟩noncomputable def representation (μ : YoungDiagram) :    Representation ℂ (Equiv.Perm (Cell μ)) (space μ) :=  (subrepresentation μ).toRepresentationend Thorp.Spechtnamespace Thorp.PermutationHilbertopen scoped BigOperators ComplexConjugate Classicalopen Complexvariable {X : Type*} [Fintype X]abbrev H (X : Type*) [Fintype X] := EuclideanSpace ℂ Xend Thorp.PermutationHilbertnamespace Thorp.Spechtopen scoped BigOperators Classicalnoncomputable def hilbertEquiv (μ : YoungDiagram) :    (Tabloid μ → ℂ) ≃ₗ[ℂ] PermutationHilbert.H (Tabloid μ) :=  (WithLp.linearEquiv 2 ℂ (Tabloid μ → ℂ)).symmnoncomputable def hilbertSpace (μ : YoungDiagram) :    Submodule ℂ (PermutationHilbert.H (Tabloid μ)) := (space μ).map (hilbertEquiv μ).toLinearMapend Thorp.Spechtnamespace Thorp.UnitaryFinitesectionopen scoped BigOperators ComplexConjugate Classicalvariable {G : Type*} [Group G] [Fintype G]variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V]noncomputable def continuousRepresentation (ρ : Representation ℂ G V) : G →* (V →L[ℂ] V) where  toFun g := (ρ g).toContinuousLinearMap  map_one' := by ext v; simp  map_mul' g h := by ext v; simpendopen scoped BigOperators Classicalvariable {G : Type*} [Group G] [Fintype G]variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V]variable {Ω Ξ : Type*} [Fintype Ω] [Fintype Ξ]noncomputable def sampleOperator (ρ : Representation ℂ G V) (P : Ω → G) : V →L[ℂ] V :=  (Fintype.card Ω:ℂ)⁻¹ • ∑ ω,continuousRepresentation ρ (P ω)end Thorp.UnitaryFinitenamespace Thorp.Spechtopen scoped BigOperators Classicalnoncomputable def spaceHilbertEquiv (μ : YoungDiagram) : space μ ≃ₗ[ℂ] hilbertSpace μ :=  (hilbertEquiv μ).submoduleMap (space μ)noncomputable def unitaryRepresentation (μ : YoungDiagram) :    Representation ℂ (Equiv.Perm (Cell μ)) (hilbertSpace μ) :=  ((spaceHilbertEquiv μ).conjAlgEquiv ℂ).toMonoidHom.comp (representation μ)variable {α ι : Type*} [Fintype α] [Fintype ι]noncomputable def relabelledUnitary (μ : YoungDiagram) (e : α ≃ Cell μ) :    Representation ℂ (Equiv.Perm α) (hilbertSpace μ) :=  (unitaryRepresentation μ).comp e.permCongrHom.toMonoidHomend Thorp.Spechtnamespace Thorp.SparseContactopen scoped BigOperatorsnoncomputable def sweepOperator (d : ℕ) (μ : YoungDiagram)    (e : Card d ≃ Specht.Cell μ) (reverse : Bool) :    Specht.hilbertSpace μ →L[ℂ] Specht.hilbertSpace μ :=  UnitaryFinite.sampleOperator (V := Specht.hilbertSpace μ) (Specht.relabelledUnitary μ e)    (fun ω : SwitchIndex d → Bool => if reverse then      (butterflyPerm d (decodeButterfly d ω))⁻¹ else butterflyPerm d (decodeButterfly d ω))end Thorp.SparseContactnamespace Thorp.StrongSmoothingdef coordinateRelabel (d : ℕ) (order : Equiv.Perm (Fin d)) : Equiv.Perm (Card d) where  toFun x := fun i => x (order.symm i)  invFun x := fun i => x (order i)  left_inv x := by funext i; simp  right_inv x := by funext i; simpdef sweep (d : ℕ) (order : Equiv.Perm (Fin d)) (ω : SwitchIndex d → Bool) :    Equiv.Perm (Card d) :=  coordinateRelabel d order * butterflyPerm d (decodeButterfly d ω) *    (coordinateRelabel d order)⁻¹abbrev Tuples (d l : ℕ) := Fin l ↪ Card dnoncomputable def sweepKernel (d l : ℕ) (order : Equiv.Perm (Fin d)) :    Matrix (Tuples d l) (Tuples d l) ℝ :=  fun x y => PairRouting.tupleProbability (sweep d order) x ynoncomputable def reflectedKernel (d l : ℕ) (order : Equiv.Perm (Fin d)) (orientation : Bool) :    Matrix (Tuples d l) (Tuples d l) ℝ :=  let A := sweepKernel d l order  if orientation then A * A.transpose else A.transpose * Aend Thorp.StrongSmoothingnamespace Thorp.StrongTailopen scoped BigOperators Classicalopen Spechtdef tailDiagram (μ : YoungDiagram) : YoungDiagram :=  YoungDiagram.ofRowLens μ.rowLens.tail μ.rowLens_sorted.pairwise.tail.sortedGEend Thorp.StrongTailnamespace Thorp.StrongTailopen scoped BigOperators Classicalopen StrongSmoothingdef DensityAt (p C : ℝ) : Prop :=  ∀ (d l : ℕ), l ≤ 2^d → ∀ (order : Equiv.Perm (Fin d)) (rev : Bool)    (x : StrongSmoothing.Tuples d l),    let H := StrongSmoothing.reflectedKernel d l order rev    (Thorp.finiteMean (fun y => ((Fintype.card (StrongSmoothing.Tuples d l):ℝ)*H x y)^p)      ≤ Real.exp (C*l)) ∧    (Thorp.finiteMean (fun y => ((Fintype.card (StrongSmoothing.Tuples d l):ℝ)*H y x)^p)      ≤ Real.exp (C*l)) ∧    (((2:ℝ)^d)^l)⁻¹ * (∑ y, ((((2:ℝ)^d)^l)*H x y)^p) ≤ Real.exp (C*l) ∧    (((2:ℝ)^d)^l)⁻¹ * (∑ y, ((((2:ℝ)^d)^l)*H y x)^p) ≤ Real.exp (C*l)end Thorp.StrongTailnamespace Thorp.StrongTailopen scoped BigOperators Classicalopen Specht UnitaryFinitedef MainStatement : Prop :=  ∃ p Cdensity C : ℝ, 1 < p ∧ p ≤ 2 ∧ DensityAt p Cdensity ∧    ∀ (d : ℕ) (μ : YoungDiagram) (e : Card d ≃ Specht.Cell μ) (rev : Bool),      ‖SparseContact.sweepOperator d μ e rev‖^2 ≤       Real.exp (C*(μ.card-μ.rowLen 0 : ℕ)) *       (Module.finrank ℂ (Specht.space (tailDiagram μ)):ℝ)^(-((p-1)/p))end Thorp.StrongTailend ThorpNine.Tailrun_cmd do  Lean.modifyEnv fun env => Lean.Meta.auxLemmasExt.setState env {}  let matcherCache := Lean.mkIdent    (Lean.mkPrivateNameCore `Lean.Meta.Match.Match `Lean.Meta.Match.matcherExt)  Lean.Elab.Command.elabCommand (← `(command|    run_cmd Lean.modifyEnv fun env => Lean.EnvExtension.setState $matcherCache env {}))namespace ThorpNine.HighTailnamespace Thorpopen scoped BigOperatorsopen Filterabbrev Card (d : ℕ) := Fin d → Booldef switchFun {d : ℕ} (ξ : Card d → Bool) (x : Card (d + 1)) : Card (d + 1) :=  Fin.cons (Bool.xor (x 0) (ξ (Fin.tail x))) (Fin.tail x)theorem switchFun_involutive {d : ℕ} (ξ : Card d → Bool) :    Function.Involutive (switchFun ξ) := by  intro x  funext i  refine Fin.cases ?_ (fun j => ?_) i  · simp only [switchFun, Fin.cons_zero, Fin.tail_cons]    cases x 0 <;> cases ξ (Fin.tail x) <;> rfl  · simp [switchFun, Fin.tail]def pairSwitch {d : ℕ} (ξ : Card d → Bool) : Equiv.Perm (Card (d + 1)) :=  { toFun := switchFun ξ    invFun := switchFun ξ    left_inv := switchFun_involutive ξ    right_inv := switchFun_involutive ξ }def Butterfly : ℕ → Type  | 0 => Unit  | d + 1 => (Card d → Bool) × (Bool → Butterfly d)def childLift {d : ℕ} (p : Bool → Equiv.Perm (Card d)) : Equiv.Perm (Card (d + 1)) where  toFun x := Fin.cons (x 0) (p (x 0) (Fin.tail x))  invFun x := Fin.cons (x 0) ((p (x 0)).symm (Fin.tail x))  left_inv x := by simp only [Fin.cons_zero, Fin.tail_cons, Equiv.symm_apply_apply, Fin.cons_self_tail]  right_inv x := by simp only [Fin.cons_zero, Fin.tail_cons, Equiv.apply_symm_apply, Fin.cons_self_tail]def butterflyPerm : (d : ℕ) → Butterfly d → Equiv.Perm (Card d)  | 0, _ => 1  | d + 1, b => pairSwitch b.1 * childLift (fun ε => butterflyPerm d (b.2 ε))noncomputable def finiteMean {Ω : Type*} [Fintype Ω] (f : Ω → ℝ) : ℝ :=  (∑ ω, f ω) / Fintype.card Ωdef SwitchIndex : ℕ → Type  | 0 => Empty  | d + 1 => Sum (Card d) (Bool × SwitchIndex d)instance (d : ℕ) : Fintype (SwitchIndex d) := by  induction d with  | zero => exact inferInstanceAs (Fintype Empty)  | succ d ih => exact inferInstanceAs (Fintype (Sum (Card d) (Bool × SwitchIndex d)))instance (d : ℕ) : DecidableEq (SwitchIndex d) := by  induction d with  | zero => exact inferInstanceAs (DecidableEq Empty)  | succ d ih => exact inferInstanceAs (DecidableEq (Sum (Card d) (Bool × SwitchIndex d)))def decodeButterfly : (d : ℕ) → (SwitchIndex d → Bool) → Butterfly d  | 0, _ => ()  | d + 1, ω => (fun y => ω (Sum.inl y), fun ε =>      decodeButterfly d (fun i => ω (Sum.inr (ε,i))))variable {α : Type*} [Fintype α] [DecidableEq α]noncomputable def orbitSet (p : Equiv.Perm α) (x : α) : Finset α :=  Finset.univ.filter (p.SameCycle x)end Thorpnamespace Thorp.RoutingNetworkopen scoped BigOperatorsopen Filtervariable {α ι : Type*} [Fintype α] [DecidableEq α] [Fintype ι] [DecidableEq ι]variable {A : ℕ}abbrev SelectedCycle (p : Equiv.Perm (α)) (S : Finset (α)) :=  {C : Finset (α) // (∃ x, C = orbitSet p x) ∧ C ⊆ S}noncomputable instance (p : Equiv.Perm (α)) (S : Finset (α)) :    Fintype (SelectedCycle p S) := Fintype.ofFinite _end Thorp.RoutingNetworknamespace Thorpopen scoped BigOperatorsopen Filterdef cardSplit : (r s : ℕ) → Card (s+r) ≃ Card r × Card s  | 0, s =>    { toFun := fun x => ((fun i => Fin.elim0 i), x)      invFun := fun x => x.2      left_inv := fun _ => rfl      right_inv := fun x => by        apply Prod.ext        · exact Subsingleton.elim _ _        · rfl }  | r+1, s =>    { toFun := fun x => (Fin.cons (x 0) ((cardSplit r s (Fin.tail x)).1),        (cardSplit r s (Fin.tail x)).2)      invFun := fun x => Fin.cons (x.1 0) ((cardSplit r s).symm (Fin.tail x.1,x.2))      left_inv := by        intro x        simp only [Fin.cons_zero, Fin.tail_cons, Prod.mk.eta, Equiv.symm_apply_apply, Fin.cons_self_tail]      right_inv := by        intro x        simp only [Fin.cons_zero, Fin.tail_cons, Equiv.apply_symm_apply, Fin.cons_self_tail] }def assembleBits : (r s : ℕ) → (Card r × SwitchIndex s → Bool) →    (Card s × SwitchIndex r → Bool) → SwitchIndex (s+r) → Bool  | 0, _, lo, _, i => lo ((fun j => Fin.elim0 j), i)  | r+1, s, _, hi, Sum.inl y => hi ((cardSplit r s y).2,Sum.inl (cardSplit r s y).1)  | r+1, s, lo, hi, Sum.inr (b,i) => assembleBits r s      (fun j => lo (Fin.cons b j.1,j.2)) (fun j => hi (j.1,Sum.inr (b,j.2))) isectionvariable {β : Type*} [Fintype β] [DecidableEq β]def pairLayer (ξ : β → Bool) : Equiv.Perm (Bool × β) where  toFun x := (Bool.xor x.1 (ξ x.2),x.2)  invFun x := (Bool.xor x.1 (ξ x.2),x.2)  left_inv x := by    rcases x with ⟨b,x⟩    change (Bool.xor (Bool.xor b (ξ x)) (ξ x),x) = (b,x)    cases b <;> cases ξ x <;> rfl  right_inv x := by    rcases x with ⟨b,x⟩    change (Bool.xor (Bool.xor b (ξ x)) (ξ x),x) = (b,x)    cases b <;> cases ξ x <;> rflenddef coinStepEquiv (d : ℕ) : (SwitchIndex (d+1) → Bool) ≃    ((SwitchIndex d → Bool) × (SwitchIndex d → Bool)) × (Card d → Bool) where  toFun ω := ((fun i => ω (Sum.inr (false,i)),fun i => ω (Sum.inr (true,i))),    fun x => ω (Sum.inl x))  invFun ω := Sum.elim ω.2 (fun bi => if bi.1 then ω.1.2 bi.2 else ω.1.1 bi.2)  left_inv ω := by    funext i    cases i with    | inl x => rfl    | inr bi => cases bi with | mk b i => cases b <;> rfl  right_inv ω := by    rcases ω with ⟨⟨ω₀,ω₁⟩,ξ⟩    rfldef headTailEquiv (d : ℕ) : Card (d+1) ≃ Bool × Card d :=  (Fin.consEquiv (fun _ : Fin (d+1) => Bool)).symmend Thorpnamespace Thorp.CycleColoringopen scoped BigOperatorsopen Filtervariable {α : Type*} [Fintype α] [DecidableEq α]def alternatingPerm (p : Equiv.Perm α) : Equiv.Perm (Bool × α) where  toFun x := if x.1 then (false,p x.2) else (true,x.2)  invFun x := if x.1 then (false,x.2) else (true,p.symm x.2)  left_inv x := by rcases x with ⟨b,x⟩; cases b <;> simp  right_inv x := by rcases x with ⟨b,x⟩; cases b <;> simpend Thorp.CycleColoringnamespace Thorp.PairRoutingopen scoped BigOperatorsopen Filtervariable {ι α : Type*} [Fintype ι] [Fintype α] [DecidableEq α]def required (x : ι → Bool × α) (c : ι → Bool) (i : ι) : Bool := Bool.xor (x i).1 (c i)def Compatible (x : ι → Bool × α) (c : ι → Bool) : Prop :=  ∀ i j, (x i).2 = (x j).2 → required x c i = required x c jdef colors (x : ι → Bool × α) (ξ : α → Bool) (i : ι) : Bool :=  Bool.xor (x i).1 (ξ (x i).2)omit [Fintype ι] [Fintype α] [DecidableEq α] inlemma required_colors (x : ι → Bool × α) (ξ : α → Bool) (i : ι) :    required x (colors x ξ) i = ξ (x i).2 := by  simp only [required,colors]  cases (x i).1 <;> cases ξ (x i).2 <;> rflomit [Fintype ι] [Fintype α] [DecidableEq α] inlemma colors_compatible (x : ι → Bool × α) (ξ : α → Bool) : Compatible x (colors x ξ) := by  intro i j he  simp only [required_colors,he]omit [Fintype ι] [Fintype α] [DecidableEq α] inlemma Compatible.tail_injective {x : ι ↪ Bool × α} {c : ι → Bool} (hc : Compatible x c) (b : Bool) :    Function.Injective (fun i : {i : ι // c i = b} => (x i.val).2) := by  intro i j he  apply Subtype.ext  apply x.injective  apply Prod.ext  · have hh := hc i j he    simp only [required,i.property,j.property] at hh    cases h₀ : (x i.val).1 <;> cases h₁ : (x j.val).1 <;> cases b <;> simp_all  · exact hedef childEmbedding (x : ι ↪ Bool × α) (c : ι → Bool) (hc : Compatible x c) (b : Bool) :    {i : ι // c i = b} ↪ α := ⟨fun i => (x i.val).2,hc.tail_injective b⟩noncomputable def labelSet (e : ι ↪ Bool × α) : Finset (Bool × α) := Finset.univ.image edef alternatingProjection (p : Bool → Equiv.Perm α) : Equiv.Perm α := (p false).symm * p truenoncomputable def alternatingCycles (e : ι ↪ Bool × α) (p : Bool → Equiv.Perm α) : ℕ :=  Fintype.card (RoutingNetwork.SelectedCycle    (CycleColoring.alternatingPerm (alternatingProjection p)) (labelSet e))def switchedEmbedding (e : ι ↪ Bool × α) (ξ : α → Bool) : ι ↪ Bool × α :=  e.trans (pairLayer ξ).toEmbeddingend Thorp.PairRoutingnamespace Thorpsectionopen scoped BigOperatorsopen Filterabbrev BenesCoins (d : ℕ) := (SwitchIndex d → Bool) × (SwitchIndex d → Bool)def palindromePerm (d : ℕ) (ω : BenesCoins d) : Equiv.Perm (Card d) :=  butterflyPerm d (decodeButterfly d ω.1) * (butterflyPerm d (decodeButterfly d ω.2)).symmdef sandwichShuffle {A B C D E F : Type*} :    ((A × B) × C) × ((D × E) × F) ≃ ((A × D) × (B × E)) × (F × C) where  toFun x := (((x.1.1.1,x.2.1.1),(x.1.1.2,x.2.1.2)),(x.2.2,x.1.2))  invFun x := (((x.1.1.1,x.1.2.1),x.2.2),((x.1.1.2,x.1.2.2),x.2.1))  left_inv _ := rfl  right_inv _ := rfldef benesStepEquiv (d : ℕ) : BenesCoins (d+1) ≃    (BenesCoins d × BenesCoins d) × ((Card d → Bool) × (Card d → Bool)) :=  (Equiv.prodCongr (coinStepEquiv d) (coinStepEquiv d)).trans sandwichShufflenoncomputable def palindromeCost : (d : ℕ) → {ι : Type*} → [Fintype ι] →    (ι ↪ Card d) → BenesCoins d → ℕ  | 0, _, _, _, _ => 0  | d+1, _, _, e, ω =>      let σ := benesStepEquiv d ω      let x := e.trans (headTailEquiv d).toEmbedding      let c := PairRouting.colors x σ.2.1      let hc := PairRouting.colors_compatible x σ.2.1      PairRouting.alternatingCycles (PairRouting.switchedEmbedding x σ.2.1)          (fun b => palindromePerm d (if b then σ.1.2 else σ.1.1)) +        palindromeCost d (PairRouting.childEmbedding x c hc false) σ.1.1 +        palindromeCost d (PairRouting.childEmbedding x c hc true) σ.1.2endnoncomputable def palindromeLowCost (H : ℕ) : (d : ℕ) → {ι : Type*} → [Fintype ι] →    (ι ↪ Card d) → BenesCoins d → ℕ  | 0, _, _, _, _ => 0  | d+1, _, _, e, ω =>      let σ := benesStepEquiv d ω      let x := e.trans (headTailEquiv d).toEmbedding      let c := PairRouting.colors x σ.2.1      let hc := PairRouting.colors_compatible x σ.2.1      (if d+1 ≤ H then PairRouting.alternatingCycles (PairRouting.switchedEmbedding x σ.2.1)          (fun b => palindromePerm d (if b then σ.1.2 else σ.1.1)) else 0) +        palindromeLowCost H d (PairRouting.childEmbedding x c hc false) σ.1.1 +        palindromeLowCost H d (PairRouting.childEmbedding x c hc true) σ.1.2end Thorpnamespace Thorp.HighHeightopen scoped BigOperators Classicalnoncomputable def highCost (J d : ℕ) {ι : Type*} [Fintype ι]    (x : ι ↪ Card d) (ω : BenesCoins d) : ℕ :=  palindromeCost d x ω-palindromeLowCost (J-1) d x ωdef MainStatement : Prop :=  ∃ b δ C : ℝ, 0<b ∧ 0<δ ∧ 0<C ∧ ∃ J₀ : ℕ, 1≤J₀ ∧    (∀ d k : ℕ, ∀ x : Fin k ↪ Card d, ∀ J : ℕ, J₀≤J →      Real.log (finiteMean (fun ω : BenesCoins d => ((2:ℝ)^b)^(highCost J d x ω)))/Real.log 2 ≤        C*k*(2:ℝ)^(-b*J)) ∧    (∀ d k : ℕ, ∀ x : Fin k ↪ Card d,      Real.log (finiteMean (fun ω : BenesCoins d => ((2:ℝ)^b)^(palindromeCost d x ω)))/Real.log 2 ≤        C*k*((k:ℝ)/(2:ℝ)^d)^δ) ∧    (∀ r s k : ℕ, ∀ x : Fin k ↪ Card (s+r), ∀ J : ℕ, J₀≤J → 2*s<J →      ∀ (X : SwitchIndex (s+r) → Bool) (lo : Card r × SwitchIndex s → Bool),      Real.log (finiteMean (fun hi : Card s × SwitchIndex r → Bool =>        ((2:ℝ)^b)^(highCost J (s+r) x (assembleBits r s lo hi,X))))/Real.log 2 ≤          C*k*(2:ℝ)^(-b*J))end Thorp.HighHeightend ThorpNine.HighTailrun_cmd do  Lean.modifyEnv fun env => Lean.Meta.auxLemmasExt.setState env {}  let matcherCache := Lean.mkIdent    (Lean.mkPrivateNameCore `Lean.Meta.Match.Match `Lean.Meta.Match.matcherExt)  Lean.Elab.Command.elabCommand (← `(command|    run_cmd Lean.modifyEnv fun env => Lean.EnvExtension.setState $matcherCache env {}))namespace ThorpNine.SparseSavingnamespace Thorpopen scoped BigOperatorsopen Filterabbrev Card (d : ℕ) := Fin d → Booldef switchFun {d : ℕ} (ξ : Card d → Bool) (x : Card (d + 1)) : Card (d + 1) :=  Fin.cons (Bool.xor (x 0) (ξ (Fin.tail x))) (Fin.tail x)theorem switchFun_involutive {d : ℕ} (ξ : Card d → Bool) :    Function.Involutive (switchFun ξ) := by  intro x  funext i  refine Fin.cases ?_ (fun j => ?_) i  · simp only [switchFun, Fin.cons_zero, Fin.tail_cons]    cases x 0 <;> cases ξ (Fin.tail x) <;> rfl  · simp [switchFun, Fin.tail]def pairSwitch {d : ℕ} (ξ : Card d → Bool) : Equiv.Perm (Card (d + 1)) :=  { toFun := switchFun ξ    invFun := switchFun ξ    left_inv := switchFun_involutive ξ    right_inv := switchFun_involutive ξ }def Butterfly : ℕ → Type  | 0 => Unit  | d + 1 => (Card d → Bool) × (Bool → Butterfly d)def childLift {d : ℕ} (p : Bool → Equiv.Perm (Card d)) : Equiv.Perm (Card (d + 1)) where  toFun x := Fin.cons (x 0) (p (x 0) (Fin.tail x))  invFun x := Fin.cons (x 0) ((p (x 0)).symm (Fin.tail x))  left_inv x := by simp only [Fin.cons_zero, Fin.tail_cons, Equiv.symm_apply_apply, Fin.cons_self_tail]  right_inv x := by simp only [Fin.cons_zero, Fin.tail_cons, Equiv.apply_symm_apply, Fin.cons_self_tail]def butterflyPerm : (d : ℕ) → Butterfly d → Equiv.Perm (Card d)  | 0, _ => 1  | d + 1, b => pairSwitch b.1 * childLift (fun ε => butterflyPerm d (b.2 ε))def SwitchIndex : ℕ → Type  | 0 => Empty  | d + 1 => Sum (Card d) (Bool × SwitchIndex d)instance (d : ℕ) : Fintype (SwitchIndex d) := by  induction d with  | zero => exact inferInstanceAs (Fintype Empty)  | succ d ih => exact inferInstanceAs (Fintype (Sum (Card d) (Bool × SwitchIndex d)))instance (d : ℕ) : DecidableEq (SwitchIndex d) := by  induction d with  | zero => exact inferInstanceAs (DecidableEq Empty)  | succ d ih => exact inferInstanceAs (DecidableEq (Sum (Card d) (Bool × SwitchIndex d)))def decodeButterfly : (d : ℕ) → (SwitchIndex d → Bool) → Butterfly d  | 0, _ => ()  | d + 1, ω => (fun y => ω (Sum.inl y), fun ε =>      decodeButterfly d (fun i => ω (Sum.inr (ε,i))))end Thorpnamespace Thorp.Spechtopen scoped BigOperators Classicalabbrev Cell (μ : YoungDiagram) := {x : ℕ × ℕ // x ∈ μ.cells}def row {μ : YoungDiagram} (x : Cell μ) : ℕ := x.1.1def col {μ : YoungDiagram} (x : Cell μ) : ℕ := x.1.2lemma row_lt_colLen {μ : YoungDiagram} (x : Cell μ) : row x < μ.colLen (col x) :=  YoungDiagram.mem_iff_lt_colLen.mp x.2noncomputable def rowIndex {μ : YoungDiagram} (x : Cell μ) : Fin (μ.colLen 0) :=  ⟨row x, (row_lt_colLen x).trans_le (μ.colLen_anti 0 (col x) (Nat.zero_le _))⟩abbrev Tabloid (μ : YoungDiagram) :=  {f : Cell μ → Fin (μ.colLen 0) // ∃ p : Equiv.Perm (Cell μ), f = rowIndex ∘ p}noncomputable instance (μ : YoungDiagram) : Fintype (Tabloid μ) := Fintype.ofFinite _noncomputable def baseTabloid (μ : YoungDiagram) : Tabloid μ := ⟨rowIndex, 1, rfl⟩noncomputable def tabloidAct {μ : YoungDiagram} (p : Equiv.Perm (Cell μ)) :    Equiv.Perm (Tabloid μ) where  toFun f := ⟨fun x => f.1 (p⁻¹ x), by    obtain ⟨q,hq⟩ := f.2    refine ⟨q*p⁻¹, ?_⟩    funext x    simp only [hq,Function.comp_apply,Equiv.Perm.mul_apply]⟩  invFun f := ⟨fun x => f.1 (p x), by    obtain ⟨q,hq⟩ := f.2    refine ⟨q*p, ?_⟩    funext x    simp only [hq,Function.comp_apply,Equiv.Perm.mul_apply]⟩  left_inv f := by apply Subtype.ext; funext x; simp  right_inv f := by apply Subtype.ext; funext x; simp@[simp] lemma tabloidAct_apply {μ : YoungDiagram} (p : Equiv.Perm (Cell μ))    (f : Tabloid μ) (x : Cell μ) : (tabloidAct p f).1 x = f.1 (p⁻¹ x) := rfl@[simp] lemma tabloidAct_one (μ : YoungDiagram) : tabloidAct (1 : Equiv.Perm (Cell μ)) = 1 := by  ext f x  rfl@[simp] lemma tabloidAct_mul {μ : YoungDiagram} (p q : Equiv.Perm (Cell μ)) :    tabloidAct (p*q) = tabloidAct p * tabloidAct q := by  ext f x  simp only [tabloidAct_apply, mul_inv_rev,Equiv.Perm.mul_apply]noncomputable def tabloidRep (μ : YoungDiagram) :    Representation ℂ (Equiv.Perm (Cell μ)) (Tabloid μ → ℂ) where  toFun p :=    { toFun := fun v f => v (tabloidAct p⁻¹ f)      map_add' := by intros; rfl      map_smul' := by intros; rfl }  map_one' := by ext v f; simp  map_mul' p q := by    ext v f    simp only [mul_inv_rev,tabloidAct_mul,Equiv.Perm.mul_apply]    rflnoncomputable def delta {μ : YoungDiagram} (f : Tabloid μ) : Tabloid μ → ℂ :=  fun g => if g=f then 1 else 0noncomputable def colGroup (μ : YoungDiagram) : Subgroup (Equiv.Perm (Cell μ)) where  carrier := {p | ∀ x, col (p x) = col x}  one_mem' := by intro x; rfl  mul_mem' := by intro p q hp hq x; exact (hp (q x)).trans (hq x)  inv_mem' := by intro p hp x; simpa using (hp (p⁻¹ x)).symmnoncomputable def permSign {α : Type*} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) : ℂ :=  ((Equiv.Perm.sign p : ℤ) : ℂ)sectionvariable {α V : Type*} [Fintype α] [DecidableEq α] [AddCommGroup V] [Module ℂ V]noncomputable def alternator (C : Subgroup (Equiv.Perm α))    (ρ : Representation ℂ (Equiv.Perm α) V) : Module.End ℂ V := by  classical  exact ∑ c : C, permSign (c : Equiv.Perm α) • ρ cendnoncomputable def polytabloid (μ : YoungDiagram) : Tabloid μ → ℂ :=  alternator (colGroup μ) (tabloidRep μ) (delta (baseTabloid μ))noncomputable def space (μ : YoungDiagram) : Submodule ℂ (Tabloid μ → ℂ) :=  Submodule.span ℂ (Set.range (fun p : Equiv.Perm (Cell μ) => tabloidRep μ p (polytabloid μ)))lemma orbit_mem_space (μ : YoungDiagram) (p : Equiv.Perm (Cell μ)) :    tabloidRep μ p (polytabloid μ) ∈ space μ := Submodule.subset_span ⟨p,rfl⟩lemma action_mem_space (μ : YoungDiagram) (p : Equiv.Perm (Cell μ))    (v : Tabloid μ → ℂ) (hv : v ∈ space μ) : tabloidRep μ p v ∈ space μ := by  induction hv using Submodule.span_induction with  | mem v hv =>    obtain ⟨q,rfl⟩ := hv    change ((tabloidRep μ p)*(tabloidRep μ q)) (polytabloid μ) ∈ space μ    rw [←map_mul]    exact orbit_mem_space μ (p*q)  | zero => simp  | add v w hv hw ihv ihw => simpa using (space μ).add_mem ihv ihw  | smul a v hv ih => simpa using (space μ).smul_mem a ihnoncomputable def subrepresentation (μ : YoungDiagram) : Subrepresentation (tabloidRep μ) :=  ⟨space μ, fun p v hv => action_mem_space μ p v hv⟩noncomputable def representation (μ : YoungDiagram) :    Representation ℂ (Equiv.Perm (Cell μ)) (space μ) :=  (subrepresentation μ).toRepresentationend Thorp.Spechtnamespace Thorp.PermutationHilbertopen scoped BigOperators ComplexConjugate Classicalopen Complexvariable {X : Type*} [Fintype X]abbrev H (X : Type*) [Fintype X] := EuclideanSpace ℂ Xend Thorp.PermutationHilbertnamespace Thorp.Spechtopen scoped BigOperators Classicalnoncomputable def hilbertEquiv (μ : YoungDiagram) :    (Tabloid μ → ℂ) ≃ₗ[ℂ] PermutationHilbert.H (Tabloid μ) :=  (WithLp.linearEquiv 2 ℂ (Tabloid μ → ℂ)).symmnoncomputable def hilbertSpace (μ : YoungDiagram) :    Submodule ℂ (PermutationHilbert.H (Tabloid μ)) := (space μ).map (hilbertEquiv μ).toLinearMapend Thorp.Spechtnamespace Thorp.UnitaryFinitesectionopen scoped BigOperators ComplexConjugate Classicalvariable {G : Type*} [Group G] [Fintype G]variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V]noncomputable def continuousRepresentation (ρ : Representation ℂ G V) : G →* (V →L[ℂ] V) where  toFun g := (ρ g).toContinuousLinearMap  map_one' := by ext v; simp  map_mul' g h := by ext v; simpendopen scoped BigOperators Classicalvariable {G : Type*} [Group G] [Fintype G]variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V]variable {Ω Ξ : Type*} [Fintype Ω] [Fintype Ξ]noncomputable def sampleOperator (ρ : Representation ℂ G V) (P : Ω → G) : V →L[ℂ] V :=  (Fintype.card Ω:ℂ)⁻¹ • ∑ ω,continuousRepresentation ρ (P ω)end Thorp.UnitaryFinitenamespace Thorp.Spechtopen scoped BigOperators Classicalnoncomputable def spaceHilbertEquiv (μ : YoungDiagram) : space μ ≃ₗ[ℂ] hilbertSpace μ :=  (hilbertEquiv μ).submoduleMap (space μ)noncomputable def unitaryRepresentation (μ : YoungDiagram) :    Representation ℂ (Equiv.Perm (Cell μ)) (hilbertSpace μ) :=  ((spaceHilbertEquiv μ).conjAlgEquiv ℂ).toMonoidHom.comp (representation μ)variable {α ι : Type*} [Fintype α] [Fintype ι]noncomputable def relabelledUnitary (μ : YoungDiagram) (e : α ≃ Cell μ) :    Representation ℂ (Equiv.Perm α) (hilbertSpace μ) :=  (unitaryRepresentation μ).comp e.permCongrHom.toMonoidHomend Thorp.Spechtnamespace Thorp.SparseContactopen scoped BigOperatorsnoncomputable def sweepOperator (d : ℕ) (μ : YoungDiagram)    (e : Card d ≃ Specht.Cell μ) (reverse : Bool) :    Specht.hilbertSpace μ →L[ℂ] Specht.hilbertSpace μ :=  UnitaryFinite.sampleOperator (V := Specht.hilbertSpace μ) (Specht.relabelledUnitary μ e)    (fun ω : SwitchIndex d → Bool => if reverse then      (butterflyPerm d (decodeButterfly d ω))⁻¹ else butterflyPerm d (decodeButterfly d ω))end Thorp.SparseContactnamespace Thorp.SparseRegimedef MainStatement : Prop :=  ∃ (C : ℝ) (d₀ : ℕ), 0 < C ∧ 0 < d₀ ∧    ∀ (d : ℕ) (μ : YoungDiagram) (e : Thorp.Card d ≃ Thorp.Specht.Cell μ),      let k := μ.card - μ.rowLen 0      1 ≤ k → k < 2^d → (d:ℝ)^((3:ℝ)/4) ≤ Real.log ((2:ℝ)^d/k) →      ∀ rev : Bool,        ‖Thorp.SparseContact.sweepOperator d μ e rev‖^2 ≤          Real.exp (C*k)*((k:ℝ)/(2:ℝ)^d)^((k:ℝ)/4) ∧        (d₀ ≤ d → ‖Thorp.SparseContact.sweepOperator d μ e rev‖^2 ≤          ((k:ℝ)/(2:ℝ)^d)^((k:ℝ)/4))end Thorp.SparseRegimeend ThorpNine.SparseSavingtheorem ThorpNine.main :    ThorpNine.Adaptive.Thorp.AdaptiveBounds.MainStatement ∧    ThorpNine.Casimir.Thorp.CasimirBounds.MainStatement ∧    ThorpNine.Dense.Thorp.DenseTruncation.MainStatement ∧    ThorpNine.Contact.Thorp.SparseContact.MainStatement ∧    ThorpNine.Harmonic.Thorp.HarmonicBounds.MainStatement ∧    ThorpNine.Smoothing.Thorp.StrongSmoothing.MainStatement ∧    ThorpNine.Tail.Thorp.StrongTail.MainStatement ∧    ThorpNine.HighTail.Thorp.HighHeight.MainStatement ∧    ThorpNine.SparseSaving.Thorp.SparseRegime.MainStatement := by  sorryend OAI

Every extracted statement of the accompanying papers

The statements the atlas extracted automatically from each accompanying paper’s TeX source, with links to the full sources.

Optimal-order mixing of the Thorp shuffle

Theorem (Optimal-order mixing)

As d\to\infty,

\|q_d^{*(1600d)}-U_n\|_{\mathrm{TV}}\longrightarrow0.

For every integer t\ge0,

\|q_d^{*t}-U_n\|_{\mathrm{TV}} \ge 1-\frac{2^{tn/2}}{n!}.

Consequently the mixing time at distance 1/4 satisfies

t_{\mathrm{mix}}(d)\ge \left\lceil\frac2n\log_2\frac{3n!}{4}\right\rceil =2d-O(1), \qquad t_{\mathrm{mix}}(d)=\Theta(d).

Section 1, Introduction Read it in the paper TeX source, line 53

Show the TeX

As $d\to\infty$,
\[
 \|q_d^{*(1600d)}-U_n\|_{\mathrm{TV}}\longrightarrow0.
\]
For every integer $t\ge0$,
\[
 \|q_d^{*t}-U_n\|_{\mathrm{TV}}
 \ge 1-\frac{2^{tn/2}}{n!}.
\]
Consequently the mixing time at distance $1/4$ satisfies
\[
 t_{\mathrm{mix}}(d)\ge
 \left\lceil\frac2n\log_2\frac{3n!}{4}\right\rceil
 =2d-O(1),
 \qquad t_{\mathrm{mix}}(d)=\Theta(d).
\]

From partial permutation information to Fourier bounds

Theorem (Complementary cosets control Fourier matrices)

Partition X into b nonempty sets M_1,\ldots,M_b. Put H_i=H_{M_i}. Suppose f is a nonnegative measure on G of mass at most one and, for every g\in G and i,

f(gH_i)\le \frac{B}{[G:H_i]}.

For every u>0 and every irreducible \rho of degree D,

\|\widehat f(\rho)\|_{\HS}^2 \le bBC_uD^{-1+(u+2)/b}.

There is also an independent orbit-span proof of the bound

\|\widehat f(\rho)\|_{\op}^2 \le bBC_uD^{-1+(u+2)/b}.

No restriction is imposed on block sizes or on the multiplicities in \rho|_{H_1\times\cdots\times H_b}.

Section 1, What partial observations can determine Read it in the paper TeX source, line 18

Show the TeX

Partition $X$ into $b$ nonempty sets $M_1,\ldots,M_b$. Put $H_i=H_{M_i}$. Suppose $f$ is a nonnegative measure on $G$ of mass at most one and, for every $g\in G$ and $i$,
\begin{equation}
 f(gH_i)\le \frac{B}{[G:H_i]}.
\end{equation}
For every $u>0$ and every irreducible $\rho$ of degree $D$,
\begin{equation}
 \|\widehat f(\rho)\|_{\HS}^2
 \le bBC_uD^{-1+(u+2)/b}.
\end{equation}
There is also an independent orbit-span proof of the bound
\begin{equation}
 \|\widehat f(\rho)\|_{\op}^2
 \le bBC_uD^{-1+(u+2)/b}.
\end{equation}
No restriction is imposed on block sizes or on the multiplicities in $\rho|_{H_1\times\cdots\times H_b}$.

Conditional permutations in a revealed switching environment

Theorem (Conditional permutation and full-deck mixing)

Let n=2^d, and start the shuffle from any deterministic deck. After J(s_0+1) sweeps, where s_0=400 and J=40000, the conditional free-slot law defined above satisfies

\sup_{\text{initial layouts}}\E_{\mathcal E} \|\nu_{\mathcal E}-U_{n/2}\|_{\TV}\longrightarrow0 \qquad(d\longrightarrow\infty).

Consequently the full-deck law approaches uniform, uniformly in the starting deck, after 16\,040\,400d physical shuffles. For every integer t\ge0, after t physical shuffles the full-deck distance from uniform is at least 1-2^{tn/2}/n!. Thus the full-deck mixing time is of order d.

Section 1, Introduction Read it in the paper TeX source, line 11

Show the TeX

Let $n=2^d$, and start the shuffle from any deterministic deck.
After $J(s_0+1)$ sweeps, where $s_0=400$ and $J=40000$, the conditional free-slot law defined above satisfies
\[
 \sup_{\text{initial layouts}}\E_{\mathcal E}
       \|\nu_{\mathcal E}-U_{n/2}\|_{\TV}\longrightarrow0
       \qquad(d\longrightarrow\infty).
\]
Consequently the full-deck law approaches uniform, uniformly in the starting deck, after $16\,040\,400d$ physical shuffles. For every integer $t\ge0$, after $t$ physical shuffles the full-deck distance from uniform is at least
$1-2^{tn/2}/n!$. Thus the full-deck mixing time is of order $d$.

Routing densities and representation contraction for Thorp sweeps

Theorem (Routing density and representation contraction)

There are absolute constants \eta,c,C>0 such that, with a=1/1000,

\log\E_{y\sim u_{N,k}}R_x(y)^{1+a} \le Ck(k/N)^\eta \qquad(1\le k\le N),

uniformly over every starting injection x. For every sufficiently large dyadic N and every nontrivial irreducible representation,

T_N(\lambda)=0\quad\hbox{or}\quad \|T_N(\lambda)\|_{\op}\le D_\lambda^{-c}.

Consequently an absolute number of forward sweeps has worst-start total-variation distance from uniform tending to zero as d\to\infty.

Section 1, Introduction Read it in the paper TeX source, line 30

Show the TeX

There are absolute constants $\eta,c,C>0$ such that, with $a=1/1000$,
\[
 \log\E_{y\sim u_{N,k}}R_x(y)^{1+a}
 \le Ck(k/N)^\eta
 \qquad(1\le k\le N),
\]
uniformly over every starting injection $x$. For every sufficiently
large dyadic $N$ and every nontrivial irreducible representation,
\[
 T_N(\lambda)=0\quad\hbox{or}\quad
 \|T_N(\lambda)\|_{\op}\le D_\lambda^{-c}.
\]
Consequently an absolute number of forward sweeps has worst-start
total-variation distance from uniform tending to zero as $d\to\infty$.

Row–column symmetry and contraction of coordinate sweeps

Theorem (Weighted sweep moments)

There are positive weights W_\lambda, an absolute finite p_*, and real exponents 2\le p_d\le p_* such that, for every d\ge1 and every \lambda\vdash2^d,

D_\lambda^{3/4}\le W_\lambda\le D_\lambda, \qquad W_\lambda\|K_d(\lambda)\|_{p_d}^{p_d}\le1.

Consequently \|K_d(\lambda)\|_{\rm op}\le D_\lambda^{-3/(4p_*)}.

Section 1, Introduction Read it in the paper TeX source, line 60

Show the TeX

There are positive weights $W_\lambda$, an absolute finite $p_*$, and real
exponents $2\le p_d\le p_*$ such that, for every $d\ge1$ and every
$\lambda\vdash2^d$,
\begin{equation}
 D_\lambda^{3/4}\le W_\lambda\le D_\lambda,
 \qquad W_\lambda\|K_d(\lambda)\|_{p_d}^{p_d}\le1.
\end{equation}
Consequently $\|K_d(\lambda)\|_{\rm op}\le D_\lambda^{-3/(4p_*)}$.

Corollary (Optimal order of mixing)

There is an absolute constant C such that, for every d\ge1,

\left\lceil\frac2N\log_2\frac{3N!}{4}\right\rceil \le t_{\rm mix}(d)\le Cd, \qquad N=2^d.

In particular t_{\rm mix}(d)=\Theta(d), and its lower bound is 2d-O(1).

Section 1, Introduction Read it in the paper TeX source, line 93

Show the TeX

There is an absolute constant $C$ such that, for every $d\ge1$,
\[
 \left\lceil\frac2N\log_2\frac{3N!}{4}\right\rceil
 \le t_{\rm mix}(d)\le Cd,
 \qquad N=2^d.
\]
In particular $t_{\rm mix}(d)=\Theta(d)$, and its lower bound is
$2d-O(1)$.

Random-subspace tests and trace smoothing for coordinate sweeps

Theorem (Regular-trace smoothing)

There is an absolute P\ge2 such that for every dyadic n\ge2,

\operatorname{Tr}_{\rm reg}|Q_n|^P\le1+n^{-10}.

If v is an integer with 2v\ge P, then v independent sweeps have total-variation distance at most \frac12n^{-5} from uniform, from every deterministic initial deck. Here \|\mu-\nu\|_{\rm TV}=\tfrac12\sum_g|\mu(g)-\nu(g)|.

Section 1, Introduction Read it in the paper TeX source, line 24

Show the TeX

There is an absolute $P\ge2$ such that for every dyadic $n\ge2$,
\begin{equation}
 \operatorname{Tr}_{\rm reg}|Q_n|^P\le1+n^{-10}.
\end{equation}
If $v$ is an integer with $2v\ge P$, then $v$ independent sweeps have total-variation distance at most $\frac12n^{-5}$ from uniform, from every deterministic initial deck. Here $\|\mu-\nu\|_{\rm TV}=\tfrac12\sum_g|\mu(g)-\nu(g)|$.

Compatibility entropy and the spectrum of a Thorp sweep

Theorem (Weighted compatibility)

There are absolute constants L,C_0>0 such that the following holds. Put m=\sqrt n, assume m/2\le A,D\le2m, and take m sufficiently large that \theta=1-L/\log m>0. For all nonnegative functions w_i:S_D\to[0,\infty) and v_k:S_A\to[0,\infty),

\frac{n!}{|R||C|}\, \mathbb E_U\!\left[\mathbf1_{\mathcal I} \prod_{i=1}^A w_i(r_i)\prod_{k=1}^D v_k(c_k)\right] \le e^{C_0n^{.54}} \prod_{i=1}^A(\mathbb E w_i^{1/\theta})^\theta \prod_{k=1}^D(\mathbb E v_k^{1/\theta})^\theta .

The expectations on the right are uniform on the indicated symmetric groups, and logarithms are natural.

Section 1, Introduction Read it in the paper TeX source, line 24

Show the TeX

There are absolute constants $L,C_0>0$ such that the following holds. Put $m=\sqrt n$, assume $m/2\le A,D\le2m$, and take $m$ sufficiently large that $\theta=1-L/\log m>0$. For all nonnegative functions $w_i:S_D\to[0,\infty)$ and $v_k:S_A\to[0,\infty)$,
\begin{equation}
 \frac{n!}{|R||C|}\,
 \mathbb E_U\!\left[\mathbf1_{\mathcal I}
       \prod_{i=1}^A w_i(r_i)\prod_{k=1}^D v_k(c_k)\right]
 \le e^{C_0n^{.54}}
       \prod_{i=1}^A(\mathbb E w_i^{1/\theta})^\theta
       \prod_{k=1}^D(\mathbb E v_k^{1/\theta})^\theta .
\end{equation}
The expectations on the right are uniform on the indicated symmetric groups, and logarithms are natural.

Theorem (A bounded regular moment)

There is an absolute finite p_*>0 such that, for every dyadic n,

Z_n(p_*)\le1+\frac1{16}.

For every integer M\ge p_*, M independent forward sweeps have worst-start total-variation distance at most 1/8 from uniform.

Section 1, Introduction Read it in the paper TeX source, line 45

Show the TeX

There is an absolute finite $p_*>0$ such that, for every dyadic $n$,
\begin{equation}
 Z_n(p_*)\le1+\frac1{16}.
\end{equation}
For every integer $M\ge p_*$, $M$ independent forward sweeps have worst-start total-variation distance at most $1/8$ from uniform.

Corollary (Singular ranks and full-deck mixing)

For every nontrivial \lambda\vdash n and 1\le r\le D_\lambda,

s_r(T_{n,\lambda})\le(16D_\lambda r)^{-1/(2p_*)}.

If s_j(T_n) denotes the full regular singular list, including all multiplicities and zeros, then

s_j(T_n)\le j^{-1/(2p_*)}\qquad(1\le j\le n!).

The constant singular value is the first value. The physical Thorp chain has worst-start 1/4 mixing time \Theta(d); more precisely its lower bound is 2d-O(1). For every fixed integer M>p_*, the worst-start total-variation distance after Md physical shuffles tends to zero as d\to\infty.

Section 1, Introduction Read it in the paper TeX source, line 53

Show the TeX

For every nontrivial $\lambda\vdash n$ and $1\le r\le D_\lambda$,
\[
 s_r(T_{n,\lambda})\le(16D_\lambda r)^{-1/(2p_*)}.
\]
If $s_j(T_n)$ denotes the full regular singular list, including all multiplicities and zeros, then
\[
 s_j(T_n)\le j^{-1/(2p_*)}\qquad(1\le j\le n!).
\]
The constant singular value is the first value. The physical Thorp chain has worst-start $1/4$ mixing time $\Theta(d)$; more precisely its lower bound is $2d-O(1)$. For every fixed integer $M>p_*$, the worst-start total-variation distance after $Md$ physical shuffles tends to zero as $d\to\infty$.

Signed tensor densities and diagram budgets for the Thorp shuffle

Theorem (A moment bound for every signed occurrence)

For each sufficiently small fixed \bar\eta>0, choose a sufficiently small \bar\kappa>0 with \bar\kappa<\bar\eta/256. There is an integer r\ge1, depending only on these fixed constants, such that for every d\ge1, every \lambda\vdash n=2^d, and every occurrence (ten:spin:eq:1),

\log\!\left(D_\lambda\operatorname{Tr}_{V_\lambda}(B_n^*B_n)^r\right) \le\eta_d F(\alpha,\beta)+g_n(l),

where

\eta_d=\bar\eta\left(1-\frac1{2\sqrt d}\right),\qquad \kappa_d=\bar\kappa\left(1-\frac1{2\sqrt d}\right),\qquad g_n(l)=\max\{0,\kappa_d l\log n-l\log(n/l)\}.

Set g_n(0)=0 and interpret the logarithm of a zero trace as -\infty.

Section 1, Introduction Read it in the paper TeX source, line 48

Show the TeX

For each sufficiently small fixed $\bar\eta>0$, choose a sufficiently
small $\bar\kappa>0$ with $\bar\kappa<\bar\eta/256$. There is an
integer $r\ge1$, depending only on these fixed constants, such that for
every $d\ge1$, every $\lambda\vdash n=2^d$, and every
occurrence~\eqref{ten:spin:eq:1},
\begin{equation}
 \log\!\left(D_\lambda\operatorname{Tr}_{V_\lambda}(B_n^*B_n)^r\right)
 \le\eta_d F(\alpha,\beta)+g_n(l),
\end{equation}
where
\[
 \eta_d=\bar\eta\left(1-\frac1{2\sqrt d}\right),\qquad
 \kappa_d=\bar\kappa\left(1-\frac1{2\sqrt d}\right),\qquad
 g_n(l)=\max\{0,\kappa_d l\log n-l\log(n/l)\}.
\]
Set $g_n(0)=0$ and interpret the logarithm of a zero trace as $-\infty$.

Corollary (Fixed-sweep convergence of the full deck)

There is an absolute positive integer L such that

\mathbb E_{U_{S_n}}|f_{d,L}-1|^2\longrightarrow0 \qquad(d\longrightarrow\infty).

The convergence is uniform over starting orders. Moreover t_{\mathrm{mix}}(d)=\Theta(d).

Section 1, Introduction Read it in the paper TeX source, line 82

Show the TeX

There is an absolute positive integer $L$ such that
\[
 \mathbb E_{U_{S_n}}|f_{d,L}-1|^2\longrightarrow0
 \qquad(d\longrightarrow\infty).
\]
The convergence is uniform over starting orders. Moreover
$t_{\mathrm{mix}}(d)=\Theta(d)$.

Conditional coordinate sweeps and analytic transfer

Theorem (Binary sweep contraction)

There are absolute constants g>0 and d_0 such that, for d\ge d_0 and every \lambda\vdash 2^d,

\|K_\lambda\|_{\op}\le D_\lambda^{-g}.

The sign representation is annihilated. There is an absolute positive integer w such that the law after w independent sweeps converges to uniform in total variation as d\to\infty, uniformly over deterministic initial decks.

Section 1, Introduction Read it in the paper TeX source, line 54

Show the TeX

There are absolute constants \(g>0\) and \(d_0\) such that, for \(d\ge d_0\)
and every \(\lambda\vdash 2^d\),
\[
 \|K_\lambda\|_{\op}\le D_\lambda^{-g}.
\]
The sign representation is annihilated. There is an absolute positive integer \(w\)
such that the law after \(w\) independent sweeps converges to uniform in
total variation as \(d\to\infty\), uniformly over deterministic initial
decks.

Proposition (Support obstruction)

For every integer t\ge0,

\|q_d^{*t}-U_N\|_{\TV}\ge1-\frac{2^{tN/2}}{N!}.

Consequently,

t_{\rm mix}(d)\ge \left\lceil\frac2N\log_2\!\left(\frac{3N!}{4}\right)\right\rceil =2d-O(1).

Section 1, Introduction Read it in the paper TeX source, line 68

Show the TeX

For every integer \(t\ge0\),
\[
 \|q_d^{*t}-U_N\|_{\TV}\ge1-\frac{2^{tN/2}}{N!}.
\]
Consequently,
\[
 t_{\rm mix}(d)\ge
 \left\lceil\frac2N\log_2\!\left(\frac{3N!}{4}\right)\right\rceil
 =2d-O(1).
\]

A strict four-row permanent inequality and permutation moments

Theorem (A robust four-row inequality)

There are absolute constants p_0\in(4/3,2) and \varepsilon>0 with the following property. Let \nu be a probability measure on S_4 such that

\|\nu-u\|_{\TV}<\varepsilon, \qquad \nu\{\pi:\pi(i)=j\}=\frac14\quad(1\le i,j\le4).

Then every four nonnegative functions on \{1,2,3,4\} satisfy

\E_\nu\prod_{i=1}^4f_i(\pi(i))\le\prod_{i=1}^4\|f_i\|_{p_0}.

Section 1, Introduction Read it in the paper TeX source, line 14

Show the TeX

There are absolute constants $p_0\in(4/3,2)$ and $\varepsilon>0$ with the following property. Let $\nu$ be a probability measure on $S_4$ such that
\[
 \|\nu-u\|_{\TV}<\varepsilon,
 \qquad
 \nu\{\pi:\pi(i)=j\}=\frac14\quad(1\le i,j\le4).
\]
Then every four nonnegative functions on $\{1,2,3,4\}$ satisfy
\begin{equation}
 \E_\nu\prod_{i=1}^4f_i(\pi(i))\le\prod_{i=1}^4\|f_i\|_{p_0}.
\end{equation}

Theorem (A fixed moment with a degree saving)

There exist an even integer r\ge2 and \eta>0, independent of N, such that for every dyadic N and every \lambda\vdash N,

D_\lambda\Tr B_N(\lambda)^r\le D_\lambda^{1-\eta}.

Consequently there is an absolute integer q for which the total-variation distance of q independent forward sweeps from uniform tends to zero as N\to\infty, uniformly over the starting deck.

Section 1, Introduction Read it in the paper TeX source, line 46

Show the TeX

There exist an even integer $r\ge2$ and $\eta>0$, independent of $N$, such that for every dyadic $N$ and every $\lambda\vdash N$,
\begin{equation}
 D_\lambda\Tr B_N(\lambda)^r\le D_\lambda^{1-\eta}.
\end{equation}
Consequently there is an absolute integer $q$ for which the total-variation distance of $q$ independent forward sweeps from uniform tends to zero as $N\to\infty$, uniformly over the starting deck.

Configuration and file facts

File: lean/ComparatorChallenges/ThorpRouting.lean
OpenAI’s Lean catalogue: OpenAI lists this as a main result in its Lean catalogue.
Solution module: OAI/Probability/ThorpRouting/Main.lean
Allowed axioms: propext, Quot.sound, Classical.choiceThe axioms this configuration allows a proof to use. A replay shows which of them a proof uses.
Imports: Mathlib
Imports from outside Mathlib: None
Local vocabulary: 357 local vocabulary declarations
Lines of Lean, without comments or blank lines: 1,565
Second proof-verification program (nanoda): Off in OpenAI's configuration.

A shareable summary of this page: the proposed paper match, what the Lean statement expresses, and which reviews are recorded.

Plectis Atlas