Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

OAI.ThorpNine.main

Open

by wurtle · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

The theorem states, as an admitted result, that nine separate formal statements about Thorp-shuffle routing hold simultaneously. Throughout, Card d is the set of d-bit strings (the 2^d cards), the sweep operator of a Young diagram mu (with the d bits relabelled to its cells by a bijection e) is the average over all butterfly switch settings of the Specht-module action of the butterfly permutation (or of its inverse, if the reverse flag is set), k = |mu| minus the first row length measures how far mu is from a single row, and the level scale of n and k is k(1+log(n/k)). (1) Adaptive: for some positive constants c, c', C, c0, for every d, mu, e and reverse flag, with h the level scale of 2^d and k, and D the dimension of the Specht module, the norm of the positive square F = S S* of the sweep operator S is at most exp(-c h), the trace of F^4 is at most exp(-c' log D + C h), and the norm of S is at most exp(-c0 (log D + h)). (2) Casimir: for some positive a and C, the palindrome row moment of order 1/64, raised to 64/65, is at most exp(C times level scale) for every injective k-tuple of cards; for every mu with k>0, the operator norm of the palindrome-shuffle operator K is at most exp(-a times level scale) and dim(Specht module) times the real trace of K^65 is at most exp(C times level scale); and for some positive integer l, from any starting permutations the total variation distance of the law of ld shuffle steps from uniform on all permutations of 2^d cards tends to 0 as d tends to infinity. (3) Dense truncation: for every density rho>0 and epsilon>0 there is c>0 such that, for r = rho 2^d, every injective r-tuple x, the proportion of palindrome-Benes coin outcomes whose density exponent exceeds r(H(rho)+entropy correction(rho)+epsilon) is at most exp(-c r), where H is a supremum over admissible cycle-length laws and allocations defined in the source. (4) Sparse contact: there are positive constants such that, for d at least 1 and 1 <= k < 2^d, the squared sweep-operator norm is at most min(1,(C d k/2^d)^(k/2)), the operator is zero when k=1, and the squared norm is also at most C^k (1+d)^(Ck) (k/2^d)^(k/2). (5) Harmonic: there exist positive constants (with 0<delta<1) and a positive integer p0 such that, for k>0, the norm W of K is at most exp(-c L), at most exp(CL) f^(-zeta) with f the dimension of the Specht module of the tail diagram (mu with its first row removed), and at most exp(-c1 L) D^(-c2); the sweep operator norm is at most exp(-cTail(L+log f)); and for each tuple length k with 1<=k<=2^d, the reflected tuple kernel has (1+delta)-moment bounded by exp(C times level scale) and its p0-th power trace bounded by exp(C times level scale). (6) Smoothing: there is an integer u>=1 and constant C such that the u-th power of every reflected sweep kernel on injective l-tuples has entries at most exp(Cl) divided by the falling factorial of 2^d, and the trace of the u-th power of the full-length kernel is at most exp(C 2^d). (7) Tail: for some p in (1,2] satisfying a density condition (L^p moment bounds of normalized kernel rows and columns by exp(C l)) and some C, the squared sweep-operator norm is at most exp(C k) times the dimension of the tail diagram's Specht module raised to -(p-1)/p. (8) High tail: for positive b, delta, C and some J0, the exponential moment 2^(b*cost) of the palindrome cost above height J-1 has base-2 logarithm at most C k 2^(-bJ) for J>=J0, the full palindrome cost has such moment at most C k (k/2^d)^delta, and a conditional version holds for the split coordinates when 2s<J. (9) Sparse saving: for some C and d0>0, whenever k<2^d and d^(3/4) <= log(2^d/k), the squared sweep norm is at most exp(Ck)(k/2^d)^(k/4), and for d>=d0 at most (k/2^d)^(k/4).

Preamble
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/ThorpRouting.lean; bytes 97159..97737
-- Kind: theorem; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.

import Mathlib
import Definitions.Def_ThorpRouting

namespace OAI

Formal statement
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

end OAI
Source
https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/ThorpRouting.lean
Human review
  • Endorsed by Community (Bot) · Oct 7, 2026

    Confirmed by the moderator at approval.

  • Endorsed by marwahaha · Oct 7, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me