Plectis Atlas
Search

↑ and ↓ move, Enter opens, Esc closes.

Lean statement

Row–column overlap on occupied boards

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.

Theorems selected for verification: OAI.RowColumn.occupied_overlap_endpoint OAI.RowColumn.occupied_overlap

Lean statement file: OccupiedOverlap.leanShow on the mapOpenAI’s Lean catalogue does not list this as a main result; the release’s Lean notes for family 238 link it.

Problems reported

  • Problem reported Listed as broken in the same way, without further detail in the post. Alex Meiburg, Several of the comparator challenges in the OpenAI release are broken and hackable, 2026-10-08 Source
  • Proof verification reported unsuccessful With the definition holes pinned, Comparator stops on a mismatch between challenge and solution at the endpoint definition; the author suspects a dependent-type technicality with a trivial fix. Jack McCarthy, Re-running Comparator with the definition holes pinned, 2026-10-09 Source
  • Correction Removing the five definition holes broke the check on an auxiliary-lemma mismatch; a small fix to the solution makes it pass with no holes (Lean kernel only, no sandbox). Jack McCarthy, OpenAI math: Comparator fixes (mirror of openai/math at fd4aeeb), 2026-10-09 Source

The Lean statement

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

abbrev OccupiedOverlapEndpoint : Prop :=  ∃ C : ℝ, 0 < C ∧ ∀ (m n : ℕ) (Ω : Finset (Board m n))    (a : YoungDiagram) (e : Ω ≃ Cell a) (h : ℕ),    1 ≤ h → h ≤ m * n → InHook a h →    ∀ (r c u v : ℕ)      (ρ : Representation ℂ (rowGroup Ω) (EuclideanSpace ℂ (Fin r)))      (τ : Representation ℂ (columnGroup Ω) (EuclideanSpace ℂ (Fin c))),      Representation.IsIrreducible ρ → Representation.IsIrreducible τ →      IsUnitary ρ → IsUnitary τ →    ∀ (I : Fin u → EuclideanSpace ℂ (Fin r) →ₗᵢ[ℂ] hilbertSpace a)      (J : Fin v → EuclideanSpace ℂ (Fin c) →ₗᵢ[ℂ] hilbertSpace a),      CompleteCopies (V := EuclideanSpace ℂ (Fin r)) (W := hilbertSpace a) ρ ((relabelledUnitary a e).comp (rowGroup Ω).subtype) I →      CompleteCopies (V := EuclideanSpace ℂ (Fin c)) (W := hilbertSpace a) τ ((relabelledUnitary a e).comp (columnGroup Ω).subtype) J →      allCopyOverlap (V := EuclideanSpace ℂ (Fin r)) (W := EuclideanSpace ℂ (Fin c))        (X := hilbertSpace a) I J ≤        Real.exp (C * (((m + n + 1 : ℕ) : ℝ) * (h : ℝ)^2 *          Real.log ((m * n : ℕ) + 2) + (m * n - Ω.card : ℕ))) *          min 1 ((r : ℝ) * c / Module.finrank ℂ (space a))theorem RowColumn.occupied_overlap_endpoint : RowColumn.OccupiedOverlapEndpoint := by  sorrytheorem RowColumn.occupied_overlap : RowColumn.OccupiedOverlapEndpoint := 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.CubeShuffle.Specht.Cell line 9

    abbrev Cell (μ : YoungDiagram) := {x : ℕ × ℕ // x ∈ μ.cells}
  • definition OAI.CubeShuffle.Specht.row line 10

    def row {μ : YoungDiagram} (x : Cell μ) : ℕ := x.1.1
  • definition OAI.CubeShuffle.Specht.col line 11

    def col {μ : YoungDiagram} (x : Cell μ) : ℕ := x.1.2
  • definition OAI.CubeShuffle.Specht.rowIndex line 15

    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.CubeShuffle.Specht.Tabloid line 18

    abbrev Tabloid (μ : YoungDiagram) :=  {f : Cell μ → Fin (μ.colLen 0) // ∃ p : Equiv.Perm (Cell μ), f = rowIndex ∘ p}
  • definition OAI.CubeShuffle.Specht.baseTabloid line 23

    noncomputable def baseTabloid (μ : YoungDiagram) : Tabloid μ := ⟨rowIndex, 1, rfl⟩
  • definition OAI.CubeShuffle.Specht.tabloidAct line 25

    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.CubeShuffle.Specht.tabloidRep line 57

    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.CubeShuffle.Specht.delta line 72

    noncomputable def delta {μ : YoungDiagram} (f : Tabloid μ) : Tabloid μ → ℂ :=  fun g => if g=f then 1 else 0
  • definition OAI.CubeShuffle.Specht.colGroup line 75

    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.CubeShuffle.Specht.permSign line 81

    noncomputable def permSign {α : Type*} [Fintype α] [DecidableEq α] (p : Equiv.Perm α) : ℂ :=  ((Equiv.Perm.sign p : ℤ) : ℂ)
  • definition OAI.CubeShuffle.Specht.alternator line 86

    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.CubeShuffle.Specht.polytabloid line 93

    noncomputable def polytabloid (μ : YoungDiagram) : Tabloid μ → ℂ :=  alternator (colGroup μ) (tabloidRep μ) (delta (baseTabloid μ))
  • definition OAI.CubeShuffle.Specht.space line 96

    noncomputable def space (μ : YoungDiagram) : Submodule ℂ (Tabloid μ → ℂ) :=  Submodule.span ℂ (Set.range (fun p : Equiv.Perm (Cell μ) => tabloidRep μ p (polytabloid μ)))
  • definition OAI.CubeShuffle.Specht.subrepresentation line 114

    noncomputable def subrepresentation (μ : YoungDiagram) : Subrepresentation (tabloidRep μ) :=  ⟨space μ, fun p v hv => action_mem_space μ p v hv⟩
  • definition OAI.CubeShuffle.Specht.representation line 117

    noncomputable def representation (μ : YoungDiagram) :    Representation ℂ (Equiv.Perm (Cell μ)) (space μ) :=  (subrepresentation μ).toRepresentation
  • abbreviation OAI.CubeShuffle.PermutationHilbert.H line 130

    abbrev H (X : Type*) [Fintype X] := EuclideanSpace ℂ X
  • definition OAI.CubeShuffle.Specht.hilbertEquiv line 138

    noncomputable def hilbertEquiv (μ : YoungDiagram) :    (Tabloid μ → ℂ) ≃ₗ[ℂ] PermutationHilbert.H (Tabloid μ) :=  (WithLp.linearEquiv 2 ℂ (Tabloid μ → ℂ)).symm
  • definition OAI.CubeShuffle.Specht.hilbertSpace line 142

    noncomputable def hilbertSpace (μ : YoungDiagram) :    Submodule ℂ (PermutationHilbert.H (Tabloid μ)) := (space μ).map (hilbertEquiv μ).toLinearMap
  • definition OAI.CubeShuffle.Specht.spaceHilbertEquiv line 145

    noncomputable def spaceHilbertEquiv (μ : YoungDiagram) : space μ ≃ₗ[ℂ] hilbertSpace μ :=  (hilbertEquiv μ).submoduleMap (space μ)
  • definition OAI.CubeShuffle.Specht.unitaryRepresentation line 148

    noncomputable def unitaryRepresentation (μ : YoungDiagram) :    Representation ℂ (Equiv.Perm (Cell μ)) (hilbertSpace μ) :=  ((spaceHilbertEquiv μ).conjAlgEquiv ℂ).toMonoidHom.comp (representation μ)
  • definition OAI.CubeShuffle.Specht.relabelledUnitary line 154

    noncomputable def relabelledUnitary (μ : YoungDiagram) (e : α ≃ Cell μ) :    Representation ℂ (Equiv.Perm α) (hilbertSpace μ) :=  (unitaryRepresentation μ).comp e.permCongrHom.toMonoidHom
  • definition OAI.CubeShuffle.UnitaryFinite.IsUnitary line 169

    def IsUnitary (ρ : Representation ℂ G V) : Prop :=  ∀ g v w, inner ℂ (ρ g v) (ρ g w) = inner ℂ v w
  • definition OAI.RowColumn.lineGroup line 182

    def lineGroup {α β : Type*} (f : α → β) : Subgroup (Equiv.Perm α) where  carrier := {g | ∀ x, f (g x) = f x}  one_mem' := by intro x; rfl  mul_mem' := by    intro a b ha hb x    exact (ha (b x)).trans (hb x)  inv_mem' := by    intro a ha x    simpa using (ha (a⁻¹ x)).symm

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

Definitions taken from OpenAI’s library 5

Comparator compares only the name and type of each definition listed here. When a theorem is configured, its proof uses the definition in OpenAI’s solution library. Read that definition as well as the one in this file when comparing the statement with the paper.

  • Comparator checks the name and type of IsUnitary; its definition is in OpenAI’s library, in the modules that OAI.RepresentationTheory.RowColumn.Occupied imports.
  • Comparator checks the name and type of hilbertSpace; its definition is in OpenAI’s library, in the modules that OAI.RepresentationTheory.RowColumn.Occupied imports.
  • Comparator checks the name and type of unitaryRepresentation; its definition is in OpenAI’s library, in the modules that OAI.RepresentationTheory.RowColumn.Occupied imports.
  • Comparator checks the name and type of relabelledUnitary; its definition is in OpenAI’s library, in the modules that OAI.RepresentationTheory.RowColumn.Occupied imports.
  • Comparator checks the name and type of OccupiedOverlapEndpoint; its definition is in OpenAI’s library, in the modules that OAI.RepresentationTheory.RowColumn.Occupied imports.

Paper theorem cited in the Lean source

A source comment for OAI.RowColumn.occupied_overlap_endpoint names this theorem’s label in the paper’s TeX source. Read the source comment from line 200

/-- `thm:occupied` (weighted.tex:76–84), including the empty occupied subset,
arbitrary deletion layout and every orthogonal multiplicity copy. The absolute
constant is 128; dimensions, unnormalized trace and operator norm are literal. -/

Theorem 5.1 of Row–column symmetry and contraction of coordinate sweeps

Theorem (Overlap on an arbitrary occupied board)

Take a grid with m rows and n columns, mn=N, and consider any subset of s=N-t cells, with the group G_s on those cells. Let a\vdash s lie in the h,h-hook, 1\le h\le N. Decompose V_a under the within-row permutation subgroup of G_s, and also (separately) the within-column subgroup. For types \sigma,\theta of these two groups, let I_{\sigma,u}: V_\sigma\to V_a, I_{\theta,v}: V_\theta\to V_a be isometric embeddings giving orthogonal copies and spanning the respective isotypic spaces. Then

\sum_{u,v}\|I_{\sigma,u}^* I_{\theta,v}\|_\infty^2 \ \le\ \exp\{C[(m+n+1)h^2\log(N+2)+t]\}\ \min\left\{1,\frac{D_\sigma D_\theta}{D_a}\right\}.

Here \sigma and \theta can each consist of a tuple of partitions, and the infinity norm is the operator norm. For s=0 the empty representation has dimension one.

Section 5, Signed representations on occupied cells Read it in the paper TeX source, line 96
Show the TeX
Take a grid with \(m\) rows and \(n\) columns, \(mn=N\), and consider any subset of \(s=N-t\) cells, with the group \(G_s\) on those cells. Let \(a\vdash s\) lie in the \(h,h\)-hook, \(1\le h\le N\). Decompose \(V_a\) under the within-row permutation subgroup of \(G_s\), and also (separately) the within-column subgroup. For types \(\sigma,\theta\) of these two groups, let \(I_{\sigma,u}: V_\sigma\to V_a\), \(I_{\theta,v}: V_\theta\to V_a\) be isometric embeddings giving orthogonal copies and spanning the respective isotypic spaces. Then
\begin{equation}
 \sum_{u,v}\|I_{\sigma,u}^* I_{\theta,v}\|_\infty^2
 \ \le\
 \exp\{C[(m+n+1)h^2\log(N+2)+t]\}\ \min\left\{1,\frac{D_\sigma D_\theta}{D_a}\right\}.       
\end{equation}
Here \(\sigma\) and \(\theta\) can each consist of a tuple of partitions, and the infinity norm is the operator norm. For \(s=0\) the empty representation has dimension one.

Other possible paper matches, closest wording first

  • Proposition 10.2 of Row–column symmetry and contraction of coordinate sweeps. Words of the Lean statement, its names split into words, that also appear in the theorem: carrier, overlap, dimensional, cells, hook, products and nine more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: selecting.
  • Proposition 5.3 of Signed tensor densities and diagram budgets for the Thorp shuffle. Words of the Lean statement, its names split into words, that also appear in the theorem: board, copy, occupied, overlap, multiplicity, cells and ten more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: contain, supported and bound.
  • Corollary 9.4 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: action, acting, apply, orthogonal, multiplicity, subgroups and ten more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: supported and estimate.
  • Corollary 5.2 of Signed tensor densities and diagram budgets for the Thorp shuffle. Words of the Lean statement, its names split into words, that also appear in the theorem: board, occupied, cells, isotypic, min, diagrams and six more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: missing, conclusion, dimension and full.
  • 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: actions, acting, function, space, norm, tuples and five more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: bound.
  • Theorem 9.1 of From partial permutation information to Fourier bounds. Words of the Lean statement, its names split into words, that also appear in the theorem: equivariant, form, space, operator, choose, multiplicity and six more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: conclusion and full.

Reported Comparator runs

three independent groups report that Comparator accepted runs for this Lean statement file: Carlos Toledo’s cert-machine; MathVet; Neal McBurnett’s openai-math-lean-tooling. 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

MathVet

How they ran it, in their words

An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge. Its protocol describes a planned error-rate study; this import does not establish that the study has been completed.

  • Accepted Their term: “comparator-sandboxed-pass”.

    Re-run through Comparator in a sandboxed virtual machine: accepted.

    Reported 8 October 2026, at the release version shown here. Original verification report

Neal McBurnett’s openai-math-lean-tooling

How they ran it, in their words

Each challenge’s solution is built and checked by Comparator at the pinned release, on Lean leanprover/lean4:v4.34.1, recording the verdict, the check time and the peak memory; the run was still in progress at this snapshot (192 accepted, 224 pending).

  • Accepted Their term: “accepted”.

    Re-run through Comparator with Lean’s kernel: accepted (the check took 744 s; peak memory 6.6 GiB).

    Reported 11 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.

Definitions compared by name and type only (5): IsUnitary, hilbertSpace, unitaryRepresentation, relabelledUnitary, OccupiedOverlapEndpoint. Their bodies come from OpenAI’s solution library.

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 supporting row–column estimate bounds the total squared overlap over all multiplicity copies on an occupied board, with explicit dependence on the row and column representation dimensions, the global dimension, the number of missing cells, and the number of rows or columns containing the global Young diagram. The paper's full physical-mixing conclusion is outside these selected representation estimates.”

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

Supporting material

The complete Lean statement file

266 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: 126 to its own declarations, 170 to Mathlib’s documentation. 21 declared names also link to the same declaration in OpenAI’s library. 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 CubeShuffle.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]@[simp] lemma tabloidAct_inv {μ : YoungDiagram} (p : Equiv.Perm (Cell μ)) :    tabloidAct p⁻¹ = (tabloidAct p)⁻¹ := by  ext f x  simp [tabloidAct,Equiv.Perm.inv_def]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]    rfl@[simp] lemma tabloidRep_apply {μ : YoungDiagram} (p : Equiv.Perm (Cell μ))    (v : Tabloid μ → ℂ) (f : Tabloid μ) : tabloidRep μ p v f = v (tabloidAct p⁻¹ f) := 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 : ℤ) : ℂ)section Alternatorvariable {α 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 α) • ρ cend Alternatornoncomputable 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 CubeShuffle.Spechtnamespace CubeShuffle.PermutationHilbertopen scoped BigOperators ComplexConjugate Classicalopen Complexvariable {X : Type*} [Fintype X]abbrev H (X : Type*) [Fintype X] := EuclideanSpace ℂ Xend CubeShuffle.PermutationHilbertnamespace CubeShuffle.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 μ).toLinearMapnoncomputable 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 CubeShuffle.Spechtnamespace CubeShuffle.UnitaryFiniteopen scoped BigOperators ComplexConjugate Classicalvariable {G : Type*} [Group G] [Fintype G]variable {V W : Type*} [NormedAddCommGroup V] [InnerProductSpace ℂ V]  [FiniteDimensional ℂ V] [NormedAddCommGroup W] [InnerProductSpace ℂ W]  [FiniteDimensional ℂ W]def IsUnitary (ρ : Representation ℂ G V) : Prop :=  ∀ g v w, inner ℂ (ρ g v) (ρ g w) = inner ℂ v wend CubeShuffle.UnitaryFinitenoncomputable sectionopen scoped BigOperators Classicalnamespace RowColumnopen CubeShuffle CubeShuffle.Specht CubeShuffle.UnitaryFinite/-- Permutations preserving each fibre of a given line map. -/def lineGroup {α β : Type*} (f : α → β) : Subgroup (Equiv.Perm α) where  carrier := {g | ∀ x, f (g x) = f x}  one_mem' := by intro x; rfl  mul_mem' := by    intro a b ha hb x    exact (ha (b x)).trans (hb x)  inv_mem' := by    intro a ha x    simpa using (ha (a⁻¹ x)).symmabbrev Board (m n : ℕ) := Fin m × Fin nabbrev rowGroup {m n : ℕ} (Ω : Finset (Board m n)) :=  lineGroup (fun x : Ω => x.1.1)abbrev columnGroup {m n : ℕ} (Ω : Finset (Board m n)) :=  lineGroup (fun x : Ω => x.1.2)/-- Zero-based form of the manuscript's (h,h)-hook. -/def InHook (a : YoungDiagram) (h : ℕ) : Prop :=  ∀ c ∈ a.cells, c.1 < h ∨ c.2 < hsection Copiesvariable {G V W : Type*} [Group G]  [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V]  [NormedAddCommGroup W] [InnerProductSpace ℂ W] [FiniteDimensional ℂ W]/-- An actual equivariant inclusion, not an unspecified overlap matrix. -/def Intertwines (ρ : Representation ℂ G V) (τ : Representation ℂ G W)    (I : V →ₗ[ℂ] W) : Prop :=  ∀ g v, I (ρ g v) = τ g (I v)/-- All orthogonal multiplicity copies of one irreducible type. The completenesscondition quantifies over genuine intertwiners, i.e. it is exactly the isotypicspace condition. -/def CompleteCopies (ρ : Representation ℂ G V) (τ : Representation ℂ G W)    {u : ℕ} (I : Fin u → V →ₗᵢ[ℂ] W) : Prop :=  (∀ i, Intertwines ρ τ (I i).toLinearMap) ∧  (∀ i j, i ≠ j → ∀ v w, inner ℂ (I i v) (I j w) = 0) ∧  ∀ J : V →ₗ[ℂ] W, Intertwines ρ τ J →    LinearMap.range J ≤ ⨆ i, LinearMap.range (I i).toLinearMapend Copies/-- The all-copy operator-overlap sum, with each squared operator norm. -/def allCopyOverlap {V W X : Type*}    [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V]    [NormedAddCommGroup W] [InnerProductSpace ℂ W] [FiniteDimensional ℂ W]    [NormedAddCommGroup X] [InnerProductSpace ℂ X] [FiniteDimensional ℂ X]    {u v : ℕ} (I : Fin u → V →ₗᵢ[ℂ] X) (J : Fin v → W →ₗᵢ[ℂ] X) : ℝ :=  ∑ i, ∑ j, ‖((I i).toContinuousLinearMap.adjoint).comp    (J j).toContinuousLinearMap‖ ^ 2/-- Exact occupied-board main. Carriers are in orthonormal coordinates; arbitraryunitary irreducibles of the two actual line groups are quantified over (equivalently,the tuples of line partitions in the manuscript). Labelling `e` chooses the actionof the Specht module on the occupied cells and forces |a| = |Ω|. -/abbrev OccupiedOverlapEndpoint : Prop :=  ∃ C : ℝ, 0 < C ∧ ∀ (m n : ℕ) (Ω : Finset (Board m n))    (a : YoungDiagram) (e : Ω ≃ Cell a) (h : ℕ),    1 ≤ h → h ≤ m * n → InHook a h →    ∀ (r c u v : ℕ)      (ρ : Representation ℂ (rowGroup Ω) (EuclideanSpace ℂ (Fin r)))      (τ : Representation ℂ (columnGroup Ω) (EuclideanSpace ℂ (Fin c))),      Representation.IsIrreducible ρ → Representation.IsIrreducible τ →      IsUnitary ρ → IsUnitary τ →    ∀ (I : Fin u → EuclideanSpace ℂ (Fin r) →ₗᵢ[ℂ] hilbertSpace a)      (J : Fin v → EuclideanSpace ℂ (Fin c) →ₗᵢ[ℂ] hilbertSpace a),      CompleteCopies (V := EuclideanSpace ℂ (Fin r)) (W := hilbertSpace a) ρ ((relabelledUnitary a e).comp (rowGroup Ω).subtype) I →      CompleteCopies (V := EuclideanSpace ℂ (Fin c)) (W := hilbertSpace a) τ ((relabelledUnitary a e).comp (columnGroup Ω).subtype) J →      allCopyOverlap (V := EuclideanSpace ℂ (Fin r)) (W := EuclideanSpace ℂ (Fin c))        (X := hilbertSpace a) I J ≤        Real.exp (C * (((m + n + 1 : ℕ) : ℝ) * (h : ℝ)^2 *          Real.log ((m * n : ℕ) + 2) + (m * n - Ω.card : ℕ))) *          min 1 ((r : ℝ) * c / Module.finrank ℂ (space a))end RowColumnendtheorem RowColumn.occupied_overlap_endpoint : RowColumn.OccupiedOverlapEndpoint := by  sorrytheorem RowColumn.occupied_overlap : RowColumn.OccupiedOverlapEndpoint := 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
OpenAI’s Lean catalogue
OpenAI’s Lean catalogue does not list this as a main result; the release’s Lean notes for family 238 link it.
Solution module
OAI.RepresentationTheory.RowColumn.Occupied
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
33 local vocabulary declarations
Lines of Lean, without comments or blank lines
160
Second proof-verification program (nanoda)
Off in OpenAI's configuration.

Statement comparison

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

Plectis Atlas

Row–column overlap on occupied boards

Family 238: Optimal logarithmic mixing of the Thorp shuffle

Cited in the Lean source

Theorem (Overlap on an arbitrary occupied board)

Take a grid with m rows and n columns, mn=N, and consider any subset of s=N-t cells, with the group G_s on those cells. Let a\vdash s lie in the h,h-hook, 1\le h\le N. Decompose V_a under the within-row permutation subgroup of G_s, and also (separately) the within-column subgroup. For types \sigma,\theta of these two groups, let I_{\sigma,u}: V_\sigma\to V_a, I_{\theta,v}: V_\theta\to V_a be isometric embeddings giving orthogonal copies and spanning the respective isotypic spaces. Then

\sum_{u,v}\|I_{\sigma,u}^* I_{\theta,v}\|_\infty^2 \ \le\ \exp\{C[(m+n+1)h^2\log(N+2)+t]\}\ \min\left\{1,\frac{D_\sigma D_\theta}{D_a}\right\}.

Here \sigma and \theta can each consist of a tuple of partitions, and the infinity norm is the operator norm. For s=0 the empty representation has dimension one.

Row–column symmetry and contraction of coordinate sweeps

TeX label thm:occupied, build/sections/weighted.tex, line 96

The Lean statement says

abbrev OccupiedOverlapEndpoint : Prop :=  ∃ C : ℝ, 0 < C ∧ ∀ (m n : ℕ) (Ω : Finset (Board m n))    (a : YoungDiagram) (e : Ω ≃ Cell a) (h : ℕ),    1 ≤ h → h ≤ m * n → InHook a h →    ∀ (r c u v : ℕ)      (ρ : Representation ℂ (rowGroup Ω) (EuclideanSpace ℂ (Fin r)))      (τ : Representation ℂ (columnGroup Ω) (EuclideanSpace ℂ (Fin c))),      Representation.IsIrreducible ρ → Representation.IsIrreducible τ →      IsUnitary ρ → IsUnitary τ →    ∀ (I : Fin u → EuclideanSpace ℂ (Fin r) →ₗᵢ[ℂ] hilbertSpace a)      (J : Fin v → EuclideanSpace ℂ (Fin c) →ₗᵢ[ℂ] hilbertSpace a),      CompleteCopies (V := EuclideanSpace ℂ (Fin r)) (W := hilbertSpace a) ρ ((relabelledUnitary a e).comp (rowGroup Ω).subtype) I →      CompleteCopies (V := EuclideanSpace ℂ (Fin c)) (W := hilbertSpace a) τ ((relabelledUnitary a e).comp (columnGroup Ω).subtype) J →      allCopyOverlap (V := EuclideanSpace ℂ (Fin r)) (W := EuclideanSpace ℂ (Fin c))        (X := hilbertSpace a) I J ≤        Real.exp (C * (((m + n + 1 : ℕ) : ℝ) * (h : ℝ)^2 *          Real.log ((m * n : ℕ) + 2) + (m * n - Ω.card : ℕ))) *          min 1 ((r : ℝ) * c / Module.finrank ℂ (space a))

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.

Comparator checks only the name and type of 5 definitions, among them IsUnitary; their bodies come from the solution.

The Lean source cites this theorem by its label. Atlas records no review of whether the two statements mean the same thing.three independent groups report that Comparator accepted runs for this file at the release version shown here.Statement review: none recorded

33 local vocabulary declarationsAllowed axioms: propext, Quot.sound, Classical.choiceopenai/math at fd4aeebwcook04.github.io/plectis-atlas/statements/OccupiedOverlap.html

Recorded comparisons with the paper

Atlas records no contributed comparison of this statement with the paper.

Contributed Comparator run reports

Atlas records no contributed report of running Comparator for this statement file.

Questions to resolve when comparing this statement with the paper

  • 5 definition holes: Comparator compares these by name and type only, so a reader checks what each solution body means.

Compare this statement with the paperShare a Comparator run reportSuggest a change