Combinatorics

Improve the separation exponent between block sensitivity and sensitivity of total Boolean functions. This mission targets $\alpha\ge2.0391$; higher is better.

For every $\varepsilon>0$ and every integer $S\ge2$, the goal asks for a function $f$ with $s(f)\ge S$ and $bs(f)\ge s(f)^{2.0391-\varepsilon}$. The shared definition SensitivityCampaign.AchievesExponent expresses exactly this requirement.

Using a finite certificate. Choose a total Boolean function $f$, an input $x$, and integers $A,B>1$. Prove $s(f)\le A$, $B\le bs(f,x)$, and $A^{2.0391}\le B$, then apply SensitivityCampaign.finite_certificate. Here $bs(f,x)$ means block sensitivity at the chosen input. The shared theorem handles normalization and passage to arbitrarily large sensitivity. Its proof is a foundation milestone; a proof depending on an open milestone remains conditional until that milestone is proved.

Direct proofs of the asymptotic goal are equally welcome. Keep the shared definitions, replace the target value, and give your theorem a unique name. Use exact certified bounds; numerical estimates alone do not establish a record.

Background: the campaign proposal.

For every $\varepsilon>0$ and every integer $S\ge2$, there exists a total Boolean function $f$ with $s(f)\ge S$ and $bs(f)\ge s(f)^{2.0205-\varepsilon}$.

The construction refines the tournament recursion of OpenAI/math. It keeps all four sensitivity profiles, sharpens the target-row count to fifteen, and bounds the gate contribution by separating the cases with and without a sink.

At depth $d=17$, use tournament parameter $M=1475863$, label alphabet $r=88$, and $K=1439236$ disjoint OR copies. The proof obtains a finite seed and integers $A,B>1$ satisfying global sensitivity $s(f)\le A$, block sensitivity at zero $bs(f,0)\ge B$, and the exact integer comparison $A^{4041}<B^{2000}$. This implies $A^{2.0205}<B$; the shared finite-certificate theorem supplies arbitrarily large sensitivity and the campaign conclusion.

The shared campaign definitions are retained. The local proof was checked in Lean 4.33.1 with Mathlib 0df444a360eaa60ab8c11dca51a86af692955474. This draft targets a certified campaign improvement; no global optimality claim is made

Certify the separation exponent $\alpha\ge2.000252407$ using OpenAI's construction. Sensitivity $s(f)$ counts individual bit flips that change the output; block sensitivity $bs(f)$ counts disjoint sensitive blocks. Both are maximized over inputs. The notation $bs(f,x)$ fixes one input, and $0$ denotes the all-zero input.

The goal requires arbitrarily large sensitivity and $bs(f)\ge s(f)^{2.000252407-\varepsilon}$ for every $\varepsilon>0$. OpenAI's depth-nine seed, with $M=9^{10}$, supplies a slightly larger exponent; the displayed decimal must be certified exactly.

This mission is the campaign's foundation. Its central reusable milestone turns a finite certificate $s(f)\le A$, $bs(f,x)\ge B$, $A,B>1$, and $A^a\le B$ into the asymptotic claim at exponent $a\ge0$. Normalization and sensitivity growth are proof obligations. Later missions import this theorem and the shared definitions.

OpenAI's quantitative separation is already proved on Prove2Me. This mission certifies the numerical exponent and the reusable bridge; its goal remains Open until all required proofs are accepted.

Motivation

Random matrices arise when observations, signs, or model coefficients fluctuate. Their spectral norm measures the largest amplification they can cause to a vector. A bound on that norm can turn entrywise randomness into a statement about the behavior of an entire linear operator. Tropp's chapter develops a common framework for Gaussian and Rademacher sums of fixed matrices, then applies it to Wigner matrices, rectangular Gaussian matrices, random signs, Toeplitz matrices, and a rounding scheme for a quadratic optimization relaxation (Tropp, Chapter 4). The applications show what the general estimate says when the matrices have concrete structure.

The chapter's general matrix-series theorem, Theorem 4.1.1, is already an open statement in tc's Prove2Me Chapter 4 mission. This mission targets the squared-norm comparison in §4.1.2 and the worked consequences that are not part of that existing goal. They are useful benchmarks because their dimensions, coefficients, and variance statistics are explicit. The existing platform status is a formalization status: Tropp proves these mathematical bounds in the cited book; the Chapter 4 theorem and the results proposed here do not yet have machine-checked proofs.

Setting

Fix positive integers $d_1,d_2$ and a finite family of complex $d_1\times d_2$ matrices $B_k$. Let $\gamma_k$ be independent standard Gaussian real variables, each with mean zero and variance one. Their matrix Gaussian series is $Z=\sum_k\gamma_k B_k$. For a complex matrix $M$, write $M^*$ for its conjugate transpose and $\|M\|$ for its Euclidean operator norm. The matrix variance statistic is

$$v(Z)=\max\{\|\mathbb E(ZZ^*)\|,\ \|\mathbb E(Z^*Z)\|\}.$$

For this Gaussian series, the two expected products equal the corresponding sums of coefficient products, so $v(Z)$ can be computed from the fixed $B_k$. This is the same statistic and norm as Theorem 4.1.1, equations (4.1.2)–(4.1.4) (Tropp, p. 42). Expectations are entrywise Bochner integrals for matrix-valued functions and ordinary integrals for real quantities.

A Rademacher variable takes values $-1$ and $1$ with equal probability. Some companion examples replace the Gaussian coefficients by independent Rademacher variables. For a Hermitian square matrix $Y$, $\lambda_{\min}(Y)$ denotes its smallest real eigenvalue. In the signed-entry example, the relevant matrix statistic is the larger of the greatest squared row norm and the greatest squared column norm of a fixed matrix.

Formalization targets

Squared norm of a Gaussian series

The goal is the pair of inequalities in (4.1.7), together with explicit integrability of the random squared norm:

$$v(Z)\le\mathbb E\|Z\|^2\le2v(Z)\bigl(1+\log(d_1+d_2)\bigr).$$

The constants and the logarithm are exactly those printed on pp. 43–44. The left side identifies a necessary scale; the right side gives a dimension-dependent upper estimate. The two milestones are the Jensen lower-bound display and the tail-integration display in §4.1.2. The latter is stated for any measurable matrix with the chapter's tail bound and positive variance, because the displayed integration step itself uses only those properties. It retains the exact split-point expression and the factor $2$.

Worked series

Companion statements record the minimum-eigenvalue consequences (4.6.4)–(4.6.5), the Wigner estimate (4.2.3), the rectangular Gaussian estimate (4.2.6), the randomly signed-entry estimate (4.3.3), the Toeplitz estimate (4.4.3), and the MaxQP rounding scale in §4.5. Their deterministic variance identities are part of the statements, rather than assumptions. In particular the Wigner bound keeps $\log(2d)$ and the Toeplitz bound keeps the exact coefficient sum $dI_d$ (Tropp, pp. 46–52).

Significance

The squared-norm comparison says that $v(Z)$ is the correct baseline for the size of a Gaussian series in mean square, while allowing a logarithmic penalty for matrix dimension. It also shows why an expectation estimate and a tail estimate answer different questions: the chapter discusses examples where a tail bound can be loose even when the expected norm is controlled (Tropp, pp. 44–45). The example statements make the abstract variance statistic usable for standard matrix ensembles and for signed matrices with prescribed entries.

A machine-checked development would connect the existing spectral and probability definitions to explicit examples, finite-sum variance identities, and integrability of Gaussian matrix norms. Those components can be reused in later sampling and numerical linear algebra missions. The general Chapter 4 matrix-series theorem remains an open platform target; these application statements are not claimed to be already formalized or proved there.

Difficulty

The central obstacle is moving from a tail estimate for $\|Z\|$ to a finite, sharp expectation for $\|Z\|^2$. The tail estimate has a dimension factor, while the desired bound has its logarithm; an unspecialized bound at a single threshold does not provide the stated constant. At the modeling level, matrix variance uses expectations of matrix products, so it must coincide with the finite sums of coefficient squares for each example. A definition that silently returns zero for a nonintegrable Bochner integral would make the upper inequality misleading. The Gaussian law, measurability, and moment behavior therefore matter to the statement as well as to eventual proofs.

Formalization scope

Matrices use Matrix (Fin d₁) (Fin d₂) ℂ with $d_1,d_2\ge1$ and tc's spectralNorm and rectSecondMoment definitions. The probability space is arbitrary; coefficient functions are measurable and independent, and their pushforward laws are exactly standard Gaussian or Rademacher as the page requires. Families may be empty. Real random coefficients scale complex matrices. Integrability of $\|Z\|^2$ is a conclusion of the goal and tail-integration milestone, while the minimum-eigenvalue expectation companion likewise asserts integrability. The tail-integration milestone assumes $v(Z)>0$ because its displayed denominator divides by $v(Z)$; the Gaussian goal itself includes $v(Z)=0$.

The Wigner coefficients are indexed by pairs $i<j$; rectangular and signed-entry coefficients by row-column pairs; Toeplitz coefficients by diagonals $-(d-1),\ldots,d-1$. The Toeplitz index in Lean is shifted to Fin (2*d-1). Row and column maxima range over the nonempty finite row and column sets. The signed-entry theorem permits complex fixed entries and uses $|b_{ij}|^2$; the printed example starts with real entries. MaxQP uses the positive scale $\alpha=1/\sqrt{2\log(d_1+d_2)}$ and tc's positive-semidefinite order for the two relaxation constraints. None of the coefficient-square identities is supplied as a hypothesis; each is a conclusion to establish.

Context. The existing TroppMatrixConcentration.ch4_matrix_series formalizes Theorem 4.1.1 and is Open. Its Gaussian/Rademacher variance identity and norm/tail bounds provide the chapter context. The present goal specializes the same Gaussian model and asks for the separate second-moment result (4.1.7). Reusable contributions include finite-matrix identities, Gaussian moment integrability, and tail-integration lemmas. A valid proof must preserve the actual standard laws and independence, and cannot redefine $v(Z)$ as the expected squared norm.

Selected references

• Joel A. Tropp, An Introduction to Matrix Concentration Inequalities, Foundations and Trends in Machine Learning 8(1–2), 2015, arXiv:1501.01571v1, Chapter 4, pp. 42–52.

Motivation

An inequality involving only four rows can feed into a recursion for a much larger permutation shuffle. The source seeks an exponent strictly below two that survives a small perturbation of the uniform permutation law. The source is OpenAI's September 2026 manuscript.

Setting

A permanent expectation averages the product of four selected entries, one from each row and each column, over a probability law on the 24 permutations. Uniform marginals require every row to choose each column with probability $1/4$.

Formalization targets

$$\exists p_0\in(4/3,2),\ \varepsilon>0:\quad\sum_{\pi\in S_4}\nu(\pi)\prod_i f_i(\pi(i))\le\prod_i\left(\frac14\sum_j f_i(j)^{p_0}\right)^{1/p_0}.$$

The theorem is stated as admitted, not proved here. Sites are Fin 4, and a law is a real-valued mass function ν on the 24 permutations of the four sites. It states that there exist a real exponent p₀ with 4/3 < p₀ < 2 and a real ε > 0 such that the following holds for every law ν that is a probability law (all masses nonnegative and summing to 1), has total variation distance from the uniform law less than ε (total variation being half the sum over permutations π of |ν(π) − 1/24|), and has uniform marginals (for every pair of sites i and j, the total mass of permutations with π(i)=j equals 1/4). For every 4-by-4 array f of real numbers with all entries f(i,j) ≥ 0, the permanent expectation Σ_π ν(π) ∏_i f(i, π(i)) is at most the product over the four rows i of the normalized ℓ^{p₀} norm of row i, where the norm of a row g is ((Σ_j g(j)^{p₀})/4)^{1/p₀}, using the uniform counting normalization with division by 4.

The goal is OAI.FourRow.robust_permanent. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.

• remaining main.

Significance

The goal is uniform over all nonnegative arrays and all probability laws within the chosen total-variation neighborhood that have exactly uniform marginals. The shared Thorp bundle is included as a separate supporting target. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Near-uniformity alone does not enforce the marginal identities. The exponent improvement must hold even for highly uneven nonnegative row entries.

Formalization scope

The law has nonnegative real masses summing to one. Its distance from the uniform $1/24$ law is strictly less than the selected $\varepsilon$, and row norms use division by four. No explicit value for the existential exponent or radius is imposed.

The shared definitions are supplied by FourRowPermanent, ThorpRemaining. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, A strict four-row permanent inequality and permutation moments, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

Minimizing a submodular set function is one of the central tractable problems of combinatorial optimization. Minimum cuts in graphs and hypergraphs, matroid intersection and partition, the rank of a matroid union, and many problems in facility location, image segmentation and machine learning are special cases or subroutines of it. The question is algorithmic: given only a value oracle for $f$, find a set $U$ with $f(U) = \min_W f(W)$ using a number of operations bounded by a polynomial in $|V|$ alone, independent of the size of the values of $f$ (strongly polynomial).

Timeline.

• 1981. Grötschel, Lovász and Schrijver showed with the ellipsoid method that submodular functions can be minimized in strongly polynomial time (Combinatorica 1, 1981). The method is not combinatorial.
• 1985. Cunningham gave a combinatorial pseudo-polynomial algorithm for submodular function minimization (Combinatorica 5, 1985).
• 1999–2000. Two combinatorial strongly polynomial algorithms appeared independently: Iwata, Fleischer and Fujishige (J. ACM 48, 2001), and Schrijver, the paper of this mission (J. Combin. Theory Ser. B 80, 2000).

Schrijver's algorithm is the one usually taught. Its proof uses only the greedy vectors of $f$, a reachability digraph and a lexicographic potential.

Setting

Let $V = \{1,\dots,n\}$ and let $f$ be a real function on all subsets of $V$ that is submodular:

$$f(Y) + f(Z) \ge f(Y\cap Z) + f(Y\cup Z) \qquad (Y, Z \subseteq V),$$

normalized so that $f(\emptyset)=0$. For $x \in \mathbb R^V$ and $U \subseteq V$ write $x(U) = \sum_{v\in U} x(v)$. The base polytope is $B_f = \{x \in \mathbb R^V : x(U) \le f(U)\ \forall U,\ x(V) = f(V)\}$.

For a total order $\prec$ on $V$ let $v_\prec = \{u : u \prec v\}$. The greedy vector of $\prec$ is $h^\prec(v) = f(v_\prec\cup\{v\}) - f(v_\prec)$. A lower ideal of $\prec$ is a set closed under taking $\prec$-smaller elements. The interval $(s,t]_\prec$ is $\{v : s \prec v \preceq t\}$. For $s \prec u$, the order $\prec^{s,u}$ is obtained from $\prec$ by moving $u$ to the position just before $s$. The vector $\chi^u$ is the incidence vector of $u$.

The algorithm keeps a point $x = \lambda_1 h^{\prec_1} + \dots + \lambda_k h^{\prec_k}$ with $\lambda_i > 0$ and $\sum_i \lambda_i = 1$; initially $x = h^\prec$ for an arbitrary order. It forms the digraph $D = (V, A)$, where $A = \{(u,v) : u \prec_i v \text{ for some } i\}$, and the sets $P = \{x > 0\}$ and $N = \{x < 0\}$.

• Case 1: $D$ has no path from $P$ to $N$. The algorithm returns the set $U$ of vertices that can reach $N$.
• Case 2: there is such a path. Let $d(v)$ be the distance from $P$ to $v$ in $D$. The algorithm picks $t \in N$ maximizing $(d(t), t)$, then the largest $s$ with $(s,t)\in A$ and $d(s) = d(t)-1$, then an order $\prec_1$ maximizing $|(s,t]_{\prec_1}|$.
  • It finds $\delta \ge 0$ with $h^{\prec_1} + \delta(\chi^t - \chi^s)$ a convex combination of the $h^{\prec_1^{s,u}}$, $u \in (s,t]_{\prec_1}$.
  • It moves $x$ toward $y = x + \lambda_1\delta(\chi^t-\chi^s)$ as far as $x(t) \le 0$ allows.
  • It reduces the new convex decomposition to at most $|V|$ terms, dropping $\prec_1$ if $x'(t) < 0$.

Formalization targets

Goal: correctness, well-definedness and the iteration bound

For every submodular $f$ with $f(\emptyset)=0$:

$$\text{(i) in Case 1, } f(U) \le f(W)\ \forall W \subseteq V;\quad \text{(ii) every Case 2 state has a successor};\quad \text{(iii) every run has } m \le |V|^6 \text{ iterations}.$$

Part (iii) is the opening claim of §5 (p. 352), and part (i) is display (16) (p. 351). Part (ii) states that the description of §4 can always be carried out, and it keeps (iii) from holding vacuously.

Milestones

In order: the diminishing-returns inequality (9); $h^\prec(U) = f(U)$ on lower ideals and $h^\prec \in B_f$ (§2); the comparison (8) of $h^{\prec^{s,u}}$ with $h^\prec$; the subroutine (12); the Case 1 certificate (16); existence of a Case 2 iteration (§4, p. 352); the location (22) of new arcs; monotonicity (20) of distances; and the lexicographic decrease (21) of $(d(t), t, s, \alpha, \beta)$ while $d$ stays fixed.

Significance

The result. The theorem gives a submodular minimizer after a number of iterations bounded by a polynomial in $|V|$. Each iteration makes polynomially many oracle calls and arithmetic operations, so the algorithm is strongly polynomial. The same exchange-and-potential scheme underlies later improvements (Fleischer–Iwata's push-relabel variant, Iwata–Orlin, Orlin's $O(n^5)$ bound). Section 6 of the paper, the companion mission, transfers the result to submodular functions on ring families.

Formalizing it. The result is proved and has been in textbooks for twenty years. It has no machine-checked proof that we know of, in Lean or elsewhere, and Mathlib has no submodular minimization. A complete development yields a verified correctness and termination proof for a nontrivial combinatorial algorithm on the base polytope. It also yields reusable facts about greedy vectors and lower ideals, and a worked example of a lexicographic-potential termination argument.

Difficulty

Correctness (16) is short once $h^\prec(U) = f(U)$ on lower ideals is available. The difficulty is termination. A single iteration can increase $x$ at $t$ and decrease it at $s$, and it adds new orders and so new arcs. Neither $|N|$ nor $x(N)$ need improve monotonically, and the obvious potentials fail. The argument needs the precise structure of the new arcs (22): every new arc lies inside the interval $[s,t]$ of $\prec_1$, and that gives both the monotonicity of distances (20) and the strict lexicographic decrease (21). The choice rule for $t$ and $s$ ("largest") is what makes (21) hold. An arbitrary choice can cycle. Well-definedness also takes work: it combines (12) with a Carathéodory reduction over the hyperplane $x(V) = f(V)$.

Formalization scope

• Ground set and values. $V$ is Fin n and subsets are Finset (Fin n). Values are real; the paper allows any ordered field. "Largest" in the choice of $t$ and $s$ is the order of Fin n.
• Orders and states. A total order is a permutation $\sigma$ read as a position map: $u \prec v$ iff $\sigma(u) < \sigma(v)$. The order $\prec^{s,u}$ is characterized relationally (IsMoved). A state is a list of (order, weight) pairs.
• Distances. Distances take values in $\mathbb N \cup \{\infty\}$, with $\infty$ for unreachable vertices.
• Standing assumptions. Submodularity (the platform definition NonmonotoneSubmod.Shared.Submodular) and $f(\emptyset) = 0$ are the paper's standing assumptions of §2 and §4. Milestones that do not need $f(\emptyset)=0$ omit it.
• Iterations as a relation. An iteration is a relation Step that admits every choice the paper leaves open: any subroutine output $\delta$, any maximizing index, and any Carathéodory reduction. The reduced decomposition may only use orders $\prec_i$ ($i \ne 1$), each $\prec_1^{s,u}$ at most once, and $\prec_1$ only when $x'(t) = 0$.
• Not formalized. The value oracle, "strongly polynomial time" and the number of oracle calls are not formalized, because there is no machine model. Only the iteration count is.
• No trivial reading. A Step relation that is never satisfiable would make the bound vacuous. Part (ii) of the goal rules this out, and the goal does not mention $d$, $\alpha$, $\beta$ or the matrix of §3.
• Contributions welcome. Proofs of the milestones, general lemmas on greedy vectors and lower ideals (reusable for any base-polytope development), and a Carathéodory lemma for convex combinations in an affine hyperplane.

Selected references

• A. Schrijver, A combinatorial algorithm minimizing submodular functions in strongly polynomial time, J. Combin. Theory Ser. B 80 (2000) 346–355. https://doi.org/10.1006/jctb.2000.1989
• S. Iwata, L. Fleischer, S. Fujishige, A combinatorial strongly polynomial algorithm for minimizing submodular functions, J. ACM 48 (2001) 761–777. https://doi.org/10.1145/502090.502096
• M. Grötschel, L. Lovász, A. Schrijver, The ellipsoid method and its consequences in combinatorial optimization, Combinatorica 1 (1981) 169–197. https://doi.org/10.1007/BF02579273
• W. H. Cunningham, On submodular function minimization, Combinatorica 5 (1985) 185–192. https://doi.org/10.1007/BF02579361
• J. B. Orlin, A faster strongly polynomial time algorithm for submodular function minimization, Math. Program. 118 (2009) 237–251. https://doi.org/10.1007/s10107-007-0189-2

Motivation

Congestion games model situations in which agents choose sets of shared resources and the payoff of each resource depends only on how many agents use it: drivers choosing routes through road segments, jobs choosing machines, flows choosing links in a network. Rosenthal (A class of games possessing pure-strategy Nash equilibria, Int. J. Game Theory 2, 1973) showed that every such game has a pure-strategy Nash equilibrium, by exhibiting a single real function on strategy profiles whose changes track every player's unilateral payoff changes.

Monderer and Shapley (Potential Games, Games Econ. Behav. 14, 1996) isolated that property and called games having it potential games. Their Section 3 shows that the property characterizes congestion games: Rosenthal's argument gives Theorem 3.1 (every congestion game is a potential game), and Theorem 3.2 gives the converse up to a renaming of strategies. Potential games have since become a standard tool in algorithmic game theory (convergence of best-response dynamics, price of stability bounds, learning in games), and Theorem 3.2 is the reason that results proved for congestion games apply to all finite potential games.

Setting

A game in strategic form $\Gamma$ has a finite set of players $N = \{1, \dots, n\}$, for each player $i$ a strategy set $Y^i$, the profile set $Y = \times_{i\in N} Y^i$, and payoff functions $u^i : Y \to \mathbb{R}$. For a profile $y$ and $x \in Y^i$, $(y^{-i}, x)$ is $y$ with player $i$'s strategy replaced by $x$. The game is finite if every $Y^i$ is finite.

A function $P : Y \to \mathbb{R}$ is a potential for $\Gamma$ (condition (2.2) with unit weights) if

$$u^i(y^{-i}, x) - u^i(y^{-i}, z) = P(y^{-i}, x) - P(y^{-i}, z) \qquad \text{for all } i,\ y^{-i},\ x, z \in Y^i,$$

and $\Gamma$ is a potential game if it has a potential (IsPotential, IsPotentialGame).

A congestion model $C(N, M, (\Sigma^i)_{i\in N}, (c_j)_{j\in M})$ has players $N$, a finite set of facilities $M$, for every player a set $\Sigma^i$ of strategies, each a nonempty subset of $M$, and for every facility $j$ a vector $c_j$, where $c_j(k)$ is the payoff to each user of $j$ when exactly $k$ players use it. The associated congestion game has strategy sets $\Sigma^i$ and payoffs

$$v^i(A) = \sum_{j\in A^i} c_j\big(\sigma_j(A)\big), \qquad \sigma_j(A) = \#\{i \in N : j \in A^i\}. \tag{3.1}$$

Two games with the same players are isomorphic (IsIsomorphic) if there are bijections $g^i : Y^i_1 \to Y^i_2$ with $u^i_1(y) = u^i_2(g^1(y^1), \dots, g^n(y^n))$ for every player $i$ and profile $y$.

Formalization targets

Goal: Theorem 3.2

$$\text{Every finite potential game is isomorphic to a congestion game.}$$

Formally: for every finite set of players, finite strategy sets $Y^i$ and payoffs $u$ admitting a potential, there are $m \in \mathbb{N}$ and a congestion model on the facilities $\{1, \dots, m\}$, all of whose strategies are nonempty facility sets, whose congestion game is isomorphic to $\Gamma$.

Milestones

The milestones follow Appendix B of the paper.

1. Lemma B.1 (p. 139): with $x^r(j) = c_j(r)$ and $x(B) = \sum_{j\in B} x(j)$, $v^i(A) = x^1(A(i)\cap A(-i)^c) + x^2\big(\bigcup_{k\neq i}[A(i)\cap A(k)\cap A(-\{i,k\})^c]\big) + \cdots + x^n\big(\bigcap_{k} A(k)\big)$.
2. The invariance of $u^i - P$ (p. 141): $u^i(a^{-i}, a^i) - P(a^{-i}, a^i)$ does not depend on $a^i$.
3. The $M_1$ identity and (B.2) (p. 141): on the facility set $M = \times_i \{0,1\}^{K(i)}$, $A^1_{m_1}\cap\cdots\cap A^n_{m_n}\cap M_1 = \{\varepsilon(m)\}$, so $x^n(A^1_{m_1}\cap\cdots\cap A^n_{m_n}) = P(a^1_{m_1}, \dots, a^n_{m_n})$.
4. (B.6) (p. 141): $x^1(A^i_{m_i}\cap A(-i)^c) = x^1(\varepsilon(m^i)) = u^i(a) - P(a)$.

Significance

Theorems 3.1 and 3.2 together say that, up to renaming strategies, the finite potential games and the congestion games are the same class. Consequently any statement about finite congestion games that is invariant under isomorphism (existence of pure equilibria, convergence of improvement dynamics, the structure of equilibrium sets) holds for all finite potential games, and conversely any potential game can be realized as a resource-sharing model. The representation is also the starting point of the later literature on the number of facilities needed to represent potential games, which the paper itself begins with a remark at the end of Appendix B.

Theorem 3.1 is already machine-checked on the platform, as Rosenthal's potential identity PriceOfStability.Harmonic.rosenthal_potential_change (Proved); it is included in this mission as a reference item. Theorem 3.2 is proved in the paper but has no machine-checked proof that we know of. The mission adds a formal statement of the theorem, of isomorphism of games, of congestion games as games in strategic form, and of the explicit construction of Appendix B; and, once proved, a verified converse to Rosenthal's theorem.

Difficulty

The theorem is an explicit construction, and its difficulty is bookkeeping rather than a single hard idea. The facility set is a product of Boolean cubes, one per player; each player's strategy is the set of facilities with a 1 in a given coordinate; and the facility payoffs are defined only at load $1$ and load $n$, by two auxiliary vectors whose definitions involve a choice of representative. Showing that the resulting congestion game reproduces every payoff requires identifying, for every profile, exactly which facilities are used by one player and which by all players, and showing that the "load 1" facilities pick up precisely the part of $u^i$ that player $i$ cannot influence. The paper leaves the two key set identities as "it can be verified"; they are the milestones.

The construction as printed does not cover one player: with $n = 1$ the vectors $x^1$ and $x^n$ are the same vector, defined twice. The theorem is still true for one player, and the formal goal does not exclude it, so a complete proof must treat that case separately.

Formalization scope

• Players form a finite type ι with decidable equality; strategy sets are types Y i, finite in the goal ([∀ i, Fintype (Y i)]). $(y^{-i}, x)$ is Function.update y i x. No nonemptiness of the strategy sets and no lower bound on the number of players is assumed.
• The congestion model is the published CongestionPoA.AsymSum.CongestionGame ι M (reference item): strategies i is the finite family $\Sigma^i$ and latency j k is the paper's $c_j(k)$, an arbitrary real number. No sign change is made; the published names "latency" and "cost" are only names. Values of latency at $0$ and above $n$ never enter (3.1).
• The congestion game as a game in strategic form is congestionPayoff G, whose strategy set for player $i$ is the subtype of G.strategies i. Because the isomorphism maps onto that subtype, the strategies of a player are distinct facility sets.
• In the goal the facility set is Fin m for an existentially quantified $m$, and nonemptiness of every strategy, which is part of the definition of a congestion model on p. 133 but not of the published structure, is a separate conjunct. Dropping it, or replacing "congestion game" by an arbitrary game whose payoffs equal $u$, would make the goal a different, weaker statement; the formal goal does neither.
• The Appendix B construction (FacilityConstruction) indexes the coordinates of player $i$ by $Y^i$ itself instead of $K(i) = \{1, \dots, k(i)\}$; $m^i = (m_k)_{k\neq i}$ is passed as a full profile whose $i$-th coordinate is ignored; $x^n$ and $x^1$ select a representative by choice, the chosen $i$-th coordinate playing the role of the arbitrary $a^i$ in (B.4).
• Misprints corrected: in Lemma B.1, $x^r(j) = c_j(m)$ is read $c_j(r)$, and the "$\cdots$" as the general term $x^r(\bigcup_{S\ni i, |S| = r}[\bigcap_{k\in S}A(k)\cap A(-S)^c])$; in (B.6), $A(-i)$ is read $A(-i)^c$ and $P^i(a)$ as $P(a)$.

Contributions welcome: proofs of the milestones, a proof of the goal (by the paper's construction, with the one-player case handled separately, or by any other construction), and general lemmas about transporting potentials along isomorphisms.

Selected references

• D. Monderer and L. S. Shapley, Potential Games, Games and Economic Behavior 14 (1996), 124–143. https://doi.org/10.1006/game.1996.0044
• R. W. Rosenthal, A class of games possessing pure-strategy Nash equilibria, International Journal of Game Theory 2 (1973), 65–67. https://doi.org/10.1007/BF01737559
• E. Anshelevich, A. Dasgupta, J. Kleinberg, É. Tardos, T. Wexler and T. Roughgarden, The Price of Stability for Network Design with Fair Cost Allocation, SIAM Journal on Computing 38 (2008), 1602–1623. https://doi.org/10.1137/070680096 (source of the platform's Rosenthal potential identity)

Prove a deterministic $O(n^{1.999074})$ algorithm for integer 3SUM in the campaign's shared word-RAM model, improving the verified $1.999112$ bound.

A promising parameter choice is $c=22$, $\theta=0.11229$, $D=\lfloor n^{0.054}\rfloor$, and $g=\lceil D^{0.0343}\rceil$. Lean-checked arithmetic certificates give $\gamma>0.0686$, $q\le0.431369<0.4314$, and $0.054<R_c$. The predicted Exact Triangle saving is $\delta=0.0018522$, giving a 3SUM cutoff of $1.9990739$ and a strict margin below the target.

The algorithmic claim remains open. The milestones are to establish the faster inner solver, then verify the integer computations for $D$ and $g$ and prove the total Exact Triangle cost, including preprocessing and scans. The existing verified reductions and foundation definitions can then be reused. The numerical certificates alone do not prove the mission.

Why the longest increasing subsequence

Pick $N$ independent points $X_1, \dots, X_N$ uniformly in $[0,1]$ and let $L_N$ be the length of the longest increasing subsequence. Because the points are almost surely distinct, $L_N$ has the law of the longest increasing subsequence of a uniform random permutation of $\{1, \dots, N\}$. This is Ulam's problem, one of the most studied random combinatorial quantities. Hammersley (1972) showed $\mathbb E L_N / \sqrt N$ converges, and Vershik–Kerov and Logan–Shepp (1977) identified the limit as $2$. That leaves the size of the fluctuations of $L_N$ around its typical value.

Timeline.

• Frieze (1991, [F] in the paper) and Bollobás–Brightwell (1992, [B-B]) proved concentration of $L_N$ around its mean with martingale methods, on deviation scales larger than $N^{1/4}$.
• Talagrand (1995), Section 7.1, derived from his convex hull inequality a two-sided Gaussian-type bound around the median on the scale $\sqrt{M_N} \asymp N^{1/4}$, with explicit constants and no logarithmic loss. This is the target of the mission.
• Baik, Deift and Johansson (1999) showed that the true fluctuations are of order $N^{1/6}$, with Tracy–Widom limit law, so Talagrand's scale is not sharp. Its value is that it comes from a short, general principle.

Section 7.2 of the same paper applies the same idea to the longest common subsequence of two random words, a quantity tied to the edit distance used in genetics and speech recognition.

Setting

Let $\Omega = [0,1]$ and $N \ge 0$. For $x = (x_1, \dots, x_N) \in \Omega^N$, $L_N(x)$ is the largest integer $p$ for which there are indices $i_1 < \dots < i_p$ with $x_{i_1} \le \dots \le x_{i_p}$. For $a > 0$, the level set is $A(a) = \{x \in \Omega^N ;\ L_N(x) \le a\}$.

Fix a probability $\mu$ on $[0,1]$ without atoms (Lebesgue measure, for instance) and let $P = \mu^{\otimes N}$ be the product probability on $\Omega^N$; the coordinates are the random points $X_i$. A median of $L_N$ is a number $M$ with $P(L_N \le M) \ge 1/2$ and $P(L_N \ge M) \ge 1/2$.

The tool is Talagrand's convex hull distance. For $A \subseteq \Omega^N$ and $x \in \Omega^N$, let $U_A(x)$ be the set of $s \in \{0,1\}^N$ for which some $y \in A$ agrees with $x$ at every coordinate $i$ with $s_i = 0$; let $V_A(x)$ be its convex hull in $\mathbb R^N$; and let $f_c(A,x)$ be the Euclidean distance from $0$ to $V_A(x)$ (with $f_c(A,x) = +\infty$ if $A = \emptyset$).

A function $L_N : \Omega^N \to \mathbb N$ on an arbitrary probability space $(\Omega, \mu)$ is a configuration function if, for every $x$, some set $J$ of exactly $L_N(x)$ coordinates satisfies $L_N(y) \ge \operatorname{card}\{i \in J ;\ y_i = x_i\}$ for all $y$.

For two sequences $x = (x_1, \dots, x_N)$ and $y = (y_1, \dots, y_{N'})$, $L_{N,N'}(x;y)$ is the largest $p$ with $i_1 < \dots < i_p$, $j_1 < \dots < j_p$ and $x_{i_\ell} = y_{j_\ell}$ for all $\ell \le p$.

Formalization targets

Goal: Theorem 7.1.2 (p. 153)

For every median $M$ of $L_N$ and every $u > 0$,

$$P(L_N \ge M + u) \le 2\exp\Big(-\frac{u^2}{4(M+u)}\Big), \qquad P(L_N \le M - u) \le 2\exp\Big(-\frac{u^2}{4M}\Big).$$

Milestones

1. Lemma 7.1.1 (p. 153). For $a > 0$ and every $x$, $a \ge L_N(x) - f_c(A(a),x)\sqrt{L_N(x)}$; in particular $L_N(x) \ge a + v$ implies $f_c(A(a),x) \ge v/\sqrt{a+v}$.
2. Theorem 7.1.3 (p. 154). The two bounds of the goal hold for every configuration function on any product probability space.
3. Eq. (7.2.3) (p. 155). For the longest common subsequence $L(x)$ of the two halves of $x \in [0,1]^{N+N'}$: $a \ge L(x) - 2\sqrt2\, f_c(A(a),x)\sqrt{L(x)}$.
4. Theorem 7.2.1 (p. 154). For two independent i.i.d. sequences with common real law and a median $M$ of $L_{N,N'}$:

$$P(L_{N,N'} \ge M + u) \le 2\exp\Big(-\frac{u^2}{32(M+u)}\Big), \qquad P(L_{N,N'} \le M - u) \le 2\exp\Big(-\frac{u^2}{32M}\Big).$$

Significance

The result. Since $M_N$ is of order $\sqrt N$, the goal confines $L_N$ to a window of width of order $N^{1/4}$ around its median with Gaussian-type tails. For $u$ much larger than $M$ the upper bound becomes exponential in $u$, the natural tail of a quantity bounded by the size of a witnessing configuration. Theorem 7.1.3 isolates what is used: every integer quantity certified by a configuration of exactly its own size has the same concentration. This abstraction became the notion of certifiable functions used widely in random graph theory and probabilistic combinatorics (see the treatment of Talagrand's inequality in Alon–Spencer, The Probabilistic Method). For the longest common subsequence, the bound is useful when the alphabet is large and $M \ll N$, where it improves on Azuma's inequality.

Formalizing it. All four results are proved in the paper; none is formalized in Lean as far as a search of the Prove2Me corpus shows. A finite-alphabet certifiable-function inequality (Talagrand.certifiable_concentration) has been posed on the platform as an open statement; it uses a Lipschitz hypothesis and no median, so it is a relative of Theorem 7.1.3, not the same statement. The mission produces a general-$\Omega$ formalization of the configuration-function principle, its application to the continuous Ulam problem, and the common-subsequence variant.

Difficulty

The deterministic inequalities (Lemma 7.1.1, Eq. (7.2.3)) relate the Euclidean distance $f_c$, defined through a convex hull in $\mathbb R^N$, to purely combinatorial counts of disagreeing coordinates; this needs the infimum defining $f_c$ to be attained and a duality between the convex hull and its extreme points. The probabilistic step rests on Talagrand's convex hull inequality (Theorem 4.1.1, Eq. (4.1.2)), $\int \exp(f_c^2(A,x)/4)\, dP(x) \le 1/P(A)$, for a general product probability; that inequality is not in Mathlib. A bounded-difference (Azuma or McDiarmid) argument does not suffice: changing one point changes $L_N$ by at most $1$, which gives deviations of order $\sqrt N$, not $\sqrt M$. The point of the configuration property is that only the $L_N(x)$ coordinates of a witness matter.

Formalization scope

• Product space. $\Omega^N$ is Fin N → Ω (0-based), and $P$ is Measure.pi (fun _ => μ). For the goal, $\Omega$ is unitInterval and $\mu$ is any probability measure on it with $\mu\{t\} = 0$ for all $t$. Theorem 7.2.1 uses the product of Measure.pi measures on (Fin N → ℝ) × (Fin N' → ℝ) for a probability $\mu$ on $\mathbb R$. Eq. (7.2.3) lives on Fin (N + N') → unitInterval, with the first $N$ coordinates forming the first sequence.
• Increasing means weakly increasing ($\le$), as printed. Index sequences are strictly increasing maps Fin p → Fin N. $L_N$ and $L_{N,N'}$ take values in ℕ.
• Convex hull distance. $f_c$ takes values in ℝ≥0∞, with the Euclidean norm written out as $\sqrt{\sum_i s_i^2}$. Mathlib's default norm on Fin N → ℝ is the sup norm and would give a different, much weaker statement. The deterministic inequalities are stated in the rearranged form $L \le a + c\, f_c \sqrt L$ in $[0, +\infty]$.
• Median: $P(Z \le M) \ge 1/2$ and $P(Z \ge M) \ge 1/2$; the statements hold for every median.
• Measurability. The paper treats all functions as measurable. In Theorem 7.1.3 this convention is the explicit hypothesis that the configuration function is measurable. The concrete $L_N$ and $L_{N,N'}$ carry no hypothesis.
• Degenerate corner. When $M = 0$, Lean's division gives $u^2/(4M) = 0$, so the lower-tail bound reads "$\le 2$". The event $\{L \le -u\}$ is then empty, so no content is lost.
• No trivialization. Using the sup norm in $f_c$, using a real-valued infimum (which is $0$ on an empty $A(a)$), or putting the conclusion of Theorem 4.1.1 among the hypotheses would each make a statement trivial or empty. None of these is done.

The mission uses the shared definition of the convex hull distance from Section 4.1. A general-$\Omega$ proof of Eq. (4.1.2) and of the attainment of $f_c$ would be reusable for every Part II chapter of the paper. Contributions are welcome in particular for the deterministic Lemma 7.1.1 and Eq. (7.2.3), the measurability of $L_N$ and $L_{N,N'}$, and the reduction of Theorem 7.1.2 to Theorem 7.1.3.

Selected references

• M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publ. Math. IHÉS 81 (1995), 73–205. https://doi.org/10.1007/BF02699376
• A. Frieze, On the length of the longest monotone subsequence in a random permutation, Ann. Appl. Probab. 1 (1991), 301–305. https://doi.org/10.1214/aoap/1177005939
• B. Bollobás, G. Brightwell, The height of a random partial order: concentration of measure, Ann. Appl. Probab. 2 (1992), 1009–1018. https://projecteuclid.org/journals/annals-of-applied-probability/volume-2/issue-4
• A. M. Vershik, S. V. Kerov, Asymptotics of the Plancherel measure of the symmetric group and the limiting form of Young tables, Soviet Math. Dokl. 18 (1977), 527–531.
• J. Baik, P. Deift, K. Johansson, On the distribution of the length of the longest increasing subsequence of random permutations, J. Amer. Math. Soc. 12 (1999), 1119–1178. https://doi.org/10.1090/S0894-0347-99-00307-0
• N. Alon, J. H. Spencer, The Probabilistic Method, 4th ed., Wiley, 2016. https://doi.org/10.1002/9781119062042

Motivation

The concentration of measure phenomenon says that in a product probability space a set of probability not too small is "large" in the sense that most points lie within a small distance of it. M. Talagrand's 1995 memoir Concentration of measure and isoperimetric inequalities in product spaces develops this phenomenon through exponential moment bounds for distances to sets. Its Section 2.1 treats the Hamming distance on an arbitrary product space and recovers the bounds obtainable by martingale methods (McDiarmid, On the method of bounded differences, 1989).

Section 2.3, the subject of this mission, specialises to the two-point space $\{0,1\}^N$ with biased coordinates. This is the setting of the binomial law, of random subsets of a finite set, and of monotone properties of random graphs. Two things happen there that do not happen in general. First, the bias $p$ of the coordinates enters the bound through the variance $p(1-p)$, which gives sharper tails when $p$ is close to $0$ or $1$. Second, when one counts only the coordinates where $x$ has a $1$ and the point of $A$ has a $0$, and measures $A$ under a second, more heavily biased product measure, the exponential moment bound becomes independent of the dimension $N$. The paper calls this the first of its results that "apparently cannot be obtained via martingales". Bounds of this one-sided kind are the natural tool for upper tails of increasing functions on the biased cube, the regime of the binomial law near $Np_1$ when samples are drawn at rate $p<p_1$.

Setting

Let $\Omega=\{0,1\}$. For $p\in[0,1]$ let $\mu$ be the probability on $\Omega$ with $\mu(\{1\})=p$, $\mu(\{0\})=1-p$, and let $P=\mu^N$ be the product probability on $\Omega^N$, whose points are written $x=(x_1,\dots,x_N)$. For a set $A\subseteq\Omega^N$ and a point $x\in\Omega^N$, the Hamming distance from $x$ to $A$ is

$$f(A,x)=\min\big\{\operatorname{card}\{i\le N:\ x_i\neq y_i\}:\ y\in A\big\},$$

the least number of coordinates of $x$ that must be changed to land in $A$. The one-sided distance counts only changes from $1$ to $0$:

$$f^{+}(A,x)=\min\big\{\operatorname{card}\{i\le N:\ x_i=1,\ y_i=0\}:\ y\in A\big\}.$$

Both are $+\infty$ when $A$ is empty. A second probability $\mu_1$ on $\Omega$ has $p_1=\mu_1(\{1\})$, and $P_1=\mu_1^N$. For $\alpha>0$ and $t\ge 0$ the paper uses two constants,

$$b(\alpha,t,p)=((1-p)e^{t}+p)(p+(1-p)e^{-t/\alpha})^{\alpha}\quad(p\ge \tfrac12),\qquad b(\alpha,t,p)=b(\alpha,t,1-p)\quad(p\le\tfrac12),$$ $$a(\alpha,t)=\max\Big(1,\ (1-p+pe^{t})(p_1e^{-t/\alpha}+1-p_1)^{\alpha}\Big).$$

In the Lean development these are hammingDistToSet, oneSidedDistToSet, bConst, aConst, the measure productMeasure N p, and the integrand expMul t z $=e^{tz}$.

Formalization targets

Goal: Theorem 2.3.4

If $p_1>p$, then for every $N$, every $A\subseteq\Omega^N$, every $\alpha>0$ and every $t\ge 0$,

$$\int e^{t f^{+}(A,x)}\,dP(x)\le\frac{a(\alpha,t)^N}{P_1(A)^{\alpha}}.$$

For small $t$ one has $a(\alpha,t)=1$. When $0<p<p_1<1$ and $\alpha=1$, the paper's explicit threshold is $e^{t}\le p_1(1-p)/(p(1-p_1))$. At equality, the bound becomes $\int (p_1(1-p)/(p(1-p_1)))^{f^{+}(A,x)}dP\le 1/P_1(A)$, with no dependence on $N$. The main theorem also includes the endpoint cases $p=0$ and $p_1=1$ without using this ratio.

Milestones

1. Proposition 2.3.1. For $t\ge0$, $\alpha\ge1$: $\displaystyle\int e^{tf(A,x)}\,dP(x)\le \frac{b(\alpha,t,p)^N}{P(A)^\alpha}$.
2. Corollary 2.3.2, Eq. (2.3.4). There is a universal $K$ such that for $\alpha\ge1$, $0\le t\le1$:

$$\int e^{tf(A,x)}\,dP(x)\le\frac{1}{P(A)^\alpha}\exp N\Big[p(1-p)\Big(1+\frac1\alpha\Big)\frac{t^2}{2}+Kt^3\Big].$$

3. Corollary 2.3.2, Eq. (2.3.5). There is a universal $K$ such that for $(4p(1-p)N\log\frac1{P(A)})^{1/2}\le k\le p(1-p)N$:

$$P(\{f(A,x)\ge k\})\le\exp\Big(-\frac{1}{2p(1-p)N}\Big(k-\sqrt{2p(1-p)N\log\tfrac{1}{P(A)}}\Big)^2+\frac{Kk^3}{(p(1-p))^3N^2}\Big).$$

4. Lemma 2.3.5. If $a\le b\le 1$, then

$$\frac{1-p}{b^{\alpha}}+p\min\Big(\frac{1}{a^{\alpha}},\frac{e^{t}}{b^{\alpha}}\Big)\le\frac{a(\alpha,t)}{(ap_1+b(1-p_1))^{\alpha}}.$$

Milestones 1–3 concern the two-sided Hamming distance; milestone 4 is the one-coordinate inequality behind the goal.

Significance

The results. Proposition 2.3.1 and Corollary 2.3.2 give, for every set $A$ in the biased cube, a tail bound for the Hamming distance whose Gaussian part has the variance $p(1-p)N$ of the binomial law, not the worst case $N/4$. The paper notes that this matches the quality of the optimal isoperimetric inequalities that are known only for hereditary (monotone) sets. Theorem 2.3.4 is a statement with no dimension in it: it controls how many $1$s of a $\mu^N$-sample must be switched off to reach a set $A$ that is not small under the more biased $\mu_1^N$.

Formalizing it. These results are proved in the paper; the local Prove2Me index contains no machine-checked proof of these statements. Mathlib has the Bernoulli measure, finite products of measures and lower Lebesgue integrals, but no exponential moment bound for these distances to sets. A complete development would add reusable facts about biased Boolean products, their distance functions and exponential moments, and the uniform cubic error term in Corollary 2.3.2.

Difficulty

The obvious route to a Hamming-distance tail bound is a martingale (bounded differences) argument. It yields $e^{-2k^2/N}$-type bounds that do not see the bias $p$, and its variance proxy grows with $N$, so it gives no bound independent of $N$; the paper states that Theorem 2.3.4 apparently cannot be obtained this way. Theorem 2.3.4 measures $A$ under $P_1$ while the integral is under $P$, so a one-coordinate estimate must account for two different probabilities and keep the factor $a(\alpha,t)$ exactly equal to $1$ for small $t$. Lemma 2.3.5 must handle $a=0$ as well as interior values. Corollary 2.3.2 requires a cubic error bound uniform in $p\in[0,1]$ and $\alpha\ge1$.

Formalization scope

• $\Omega$ is Bool with $1$ = true; $P$ reuses the published TalagrandCore.bernPi Bernoulli product measure with p : unitInterval converted to a nonnegative real, over Fin N (0-based coordinates). Every subset of $\{0,1\}^N$ is measurable, so the paper's convention of ignoring measurability costs nothing here.
• Distances take values in ℝ≥0∞, with $f(\emptyset,x)=+\infty$; integrals are lower Lebesgue integrals ∫⁻ in $[0,\infty]$; $P(A)^{-\alpha}$ is computed in $[0,\infty]$, so $P(A)=0$ gives $+\infty$.
• Theorem 2.3.4 and Lemma 2.3.5 are stated for $\alpha>0$, the range under which Section 2.2 introduces the exponent $\alpha$ (the theorem's page does not restate it). Proposition 2.3.1 and Corollary 2.3.2 keep the page's $\alpha\ge 1$. The standing hypothesis $p_1>p$ appears as a binder.
• The universal constants of Corollary 2.3.2 are quantified before $p$, $N$, $A$, $\alpha$, $t$, $k$. In Eq. (2.3.5), $0<p<1$, $N\ge1$ and $P(A)>0$ are assumed, which is where the displayed formula is defined.
• A trivializing formalization is ruled out: the integrals are not Bochner integrals (which vanish on non-integrable functions), the empty set and $P_1(A)=0$ are handled through $+\infty$, not junk zeros, and the two different distances of the section carry different names.

The mission also imports the published TalagrandCore.bernPi definition for the Boolean product law. Reusable pieces include evaluation of $\int$ over $\{0,1\}$ under a Bernoulli measure and facts about product measures over Fin N. Contributions to any of the four milestones or the goal are welcome.

Selected references

• M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publ. Math. IHÉS 81 (1995), 73–205. https://doi.org/10.1007/bf02699376
• C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics, LMS Lecture Note Series 141 (1989), 148–188. https://doi.org/10.1017/CBO9781107359949.008
• M. Ledoux, The Concentration of Measure Phenomenon, AMS Mathematical Surveys and Monographs 89 (2001). https://doi.org/10.1090/surv/089

Motivation

A pseudorandom number generator replaces repeated random sampling with a deterministic update of a small state. Its useful lifetime depends on the length and structure of the resulting orbit. In Marsaglia and Zaman’s 1991 paper, the subtract-with-borrow generators use only digit subtraction and a one-bit borrow while attaining cycles that can be almost as long as the whole set of digit tuples. The mathematical question is exact: which fraction encodes an output sequence, when does an arbitrary seed enter a cycle, and how long is that cycle?

This mission concerns the paper’s first subtract-with-borrow rule, called Method 1 in §4.5. The paper also studies a second rule that reverses the order of the two subtracted digits. Its modulus and period analysis differ. The distinction matters because the same state format supports both rules while their arithmetic claims are different.

Setting

Choose an integer base $b\ge2$ and lags $0<s<r$. A state is a row of $r$ digits and one borrow bit, $(x_1,\ldots,x_r,c)$, where each $x_i$ is in $\{0,\ldots,b-1\}$ and $c\in\{0,1\}$. The leftmost digit $x_1$ is the oldest. One update discards it, shifts the remaining digits left, and appends a new digit. Put $t=x_{r+1-s}-x_1-c$. If $t\ge0$, the appended digit is $t$ and the new borrow is zero. If $t<0$, the appended digit is $t+b$ and the new borrow is one. Write this deterministic map as $f$.

The digits emitted after the seed obey $x_n=x_{n-s}-x_{n-r}-c$ modulo $b$, with $c$ updated at each step. The associated modulus is $m=b^r-b^s+1$. For $0\le k<m$, write $d_j(k/m)$ for the $j$th digit after the point in the base-$b$ expansion of $k/m$, with $j\ge1$. The digit stream is read in reverse order when it is matched to an expansion: the latest generated digit in a finite block is the first fractional digit. A state is strictly periodic when it is already on a cycle under $f$; otherwise it may pass through a transient before reaching one.

Two states have period one: $(0,\ldots,0,0)$ and $(b-1,\ldots,b-1,1)$. These are the trivial seeds. They are exceptions to the order-of-base period formula. A third useful object is the multiplicative order $\operatorname{ord}_m(b)$, the least positive $p$ for which $b^p\equiv1\pmod m$. Since $m\equiv1\pmod b$, the base is coprime to this modulus.

Formalization targets

Exact cycle period

For prime $m=b^r-b^s+1$ and any nontrivial seed $z$, the goal identifies the minimal state period after the transient:

$$\operatorname{period}_f\bigl(f^r(z)\bigr)=\operatorname{ord}_m(b).$$

The assertion includes both that $f^r(z)$ is on a cycle and that its period is exactly the order. It makes no primitive-root assumption. If $b$ is a primitive root modulo $m$, the right side specializes to $m-1=b^r-b^s$, the full period discussed in §3 of the paper.

Supporting results

The milestones state that the fractional digits of $k/m$ have least period $\operatorname{ord}_m(b)$ when $k$ and $b$ are coprime to $m$; that a primitive root yields digit period $m-1$; that the two trivial seeds are precisely the fixed points; and that every seed reaches a cycle after at most $r$ updates. They also formalize the reverse-digit relation for every finite generated block and the paper’s Method 1 inequalities that classify nontrivial seeds already on a cycle. These targets use the paper’s own claims in §§4.1, 4.3, and 4.5 rather than an arbitrary decomposition of the goal.

Significance

The result converts the orbit-length problem of a digit-and-borrow machine into a multiplicative-order calculation in a finite residue ring. A prime modulus and a primitive base produce a nontrivial cycle of length $m-1$; a nonprimitive base still has the exact order-of-base period. The seed classification separates states already on that cycle from states with an initial transient. These statements are what allow a proposed numerical parameter set to be assessed mathematically before the generator is used.

Marsaglia and Zaman proved these results in the cited paper. This mission asks for machine-checked Lean proofs of the statements, starting from an explicit finite-state update. The reusable output includes exact base-$b$ digit arithmetic, links between digit periods and multiplicative order, and methods for reasoning about the eventual cycles of finite-state digit generators. The present proposal consists of compiled statements and definitions; the theorem bodies are open proof targets.

Difficulty

Finiteness alone shows that every state eventually repeats, but it gives neither the bound of $r$ steps nor the exact cycle length. Likewise, observing that a generated digit block matches a prefix of some fraction does not by itself identify one period for the whole state orbit. The proof must keep track of the borrow bit and the direction in which the digit block is read. It must also show that a nontrivial seed does not collapse to one of the two fixed states. The source’s integer tableaux explain the arithmetic link, but turning their finite strings into a statement uniform over every seed and every block length is the main formalization challenge.

Formalization scope

Lean represents digits by Fin b, the borrow by Fin 2, and the row by a function on Fin r. Lean index zero is $x_1$, so the digit used in the update, $x_{r+1-s}$, has index $r-s$. The update branches on an ordinary integer comparison before any natural-number subtraction can truncate a negative value. The modulus is a natural number, and $0<s<r$ with $b\ge2$ makes $b^r-b^s$ an exact subtraction. The $j$th fractional digit is computed by an exact quotient and remainder; only $j\ge1$ has the mathematical meaning used in the theorems. The generated stream is one-based, and the first digit beyond the seed is $x_{r+1}$.

The paper’s “after a few iterations” is pinned to its stated upper bound “at most $r$.” Its “period” is the minimal positive state period of $f^r(z)$, not a mere period divisor or the period of an arbitrarily selected digit window. “Appropriately chosen” parameters mean a prime $m$ for the goal and exclusion of the two named fixed seeds. The reverse-digit milestone permits the numerator $k$ to depend on the finite endpoint, as the tableau argument does. No seed is excluded from the at-most-$r$ milestone.

The discussion on pp. 473–474 prints the Method 1 seed inequalities in the opposite direction from the Method 1 listing on p. 472. The Lean seed-classification milestone uses the p. 472 directions, which agree with the step map on p. 466 and with direct finite checks. The §5 claim that every five-tuple except the $100$ patterns $xyxyx$ appears once in the special $b=10,r=5,s=2$ full cycle is left for a later extension. The other subtraction order, its modulus $b^r-b^s-1$, and the paper’s large parameter certificates are outside this mission.

An encoding that merely asserts the existence of some period, allows an impossible seed hypothesis, or replaces the update by a different subtraction order would make the goal vacuous or change the result. The intended development needs Mathlib’s ZMod, multiplicative order, finite iterations, periodic points, and natural-number quotient and remainder. Contributions proving the numbered milestones, strengthening their arithmetic interfaces, or closing the goal are in scope.

Selected references

• G. Marsaglia and A. Zaman, A new class of random number generators, The Annals of Applied Probability 1(3), 462–480 (1991). DOI: 10.1214/aoap/1177005878.