Completed

Combinatorics Graph Theory Theoretical Computer Science·Captain: hao jia

Immune High-Girth Bipartite Graphs (Feghali-Lucke-Paulusma-Ries 2025)Research Paper

Motivation

A matching cut is a vertex bipartition whose crossing edges form a matching. The property was introduced under the name decomposability and has links to graph algorithms, stable cutsets in line graphs, and several graph-labeling problems. An Open Problem Garden question asked whether sufficiently large girth forces a matching cut once average degree is bounded.

Feghali, Lucke, Paulusma, and Ries answered that question negatively. Their conference paper appeared at ISAAC 2023, and the version of record was published in Algorithmica in 2025. The paper proves NP-completeness for bipartite graphs of arbitrarily prescribed girth and bounded maximum degree. A central input, Lemma 5, is a stronger structural existence statement: for every girth threshold there is an immune $14$ -regular bipartite graph of at least that girth, and it has a perfect matching.

This is therefore a ResearchPaper mission, not a new open-problem mission. Its goal is to formalize the published theorem and its graph-theoretic consequence. Repository candidate constructions and finite arithmetic audits remain separate and are not credited as solving the problem.

Setting

For a finite simple graph $G$ and a vertex set $A\subseteq V(G)$ , the associated cut consists of all edges with one endpoint in $A$ and one in $V(G)\setminus A$ . The cut is nontrivial when both shores are nonempty. It is a matching cut when each vertex is incident with at most one crossing edge. A graph is called immune in the cited paper when it has no matching cut.

The girth is the length of a shortest simple cycle; forests have infinite girth. A graph is $14$ -regular when every vertex has exactly fourteen neighbors. Bipartiteness is witnessed by a partition into two independent sides. A perfect matching pairs every vertex with one adjacent partner.

The original OPG wording has a literal one-vertex boundary ambiguity: with nonempty shores required, $K_1$ has no matching cut, average degree zero, and infinite girth. The research-paper target avoids that vacuity by constructing connected graphs with at least two vertices, exact degree fourteen, and arbitrarily large finite girth.

Formalization targets

Lemma 5 — immune high-girth graphs

The main theorem follows the paper's structural lemma:

\forall g\ge3\ \exists G, \quad G\text{ is finite, connected, bipartite, and $14$-regular},

\operatorname{girth}(G)\ge g, \qquad G\text{ has no matching cut}, \qquad G\text{ has a perfect matching}.

The graph may depend on $g$ . The existence quantifier does not request an efficient algorithm or a numerical order bound.

Negative OPG consequence

A supporting theorem removes the perfect-matching and bipartite fields and records the direct substantive counterexample family:

\forall g\ge3\ \exists G, \qquad \overline d(G)=14<15, \quad \operatorname{girth}(G)\ge g, \quad G\text{ has no matching cut}.

Thus choosing $d=15$ refutes the intended universal assertion that some girth threshold works for every graph of average degree below $d$ .

Significance

The theorem shows that large girth and bounded degree do not force matching cuts. The examples are highly nontrivial: they are connected, regular, bipartite, and can have arbitrarily large girth. This separates local tree-like structure from the global expansion that prevents a matching cut.

Within the paper, the immune graphs serve as gadgets for hardness reductions. The journal theorem states that, for every $g\ge3$ , Matching Cut is NP-complete even for bipartite graphs of girth at least $g$ and maximum degree at most $60$ . Formalizing Lemma 5 supplies the graph-theoretic core needed to reconstruct that result without forcing this mission to formalize an entire complexity-theory reduction in its first stage.

Difficulty

Large girth alone makes bounded neighborhoods look like trees, and trees have many matching cuts. Immunity must therefore come from global expansion rather than short local cycles. The paper obtains the required family from Lubotzky–Phillips–Sarnak Ramanujan graphs and combines spectral and isoperimetric bounds to show that every nontrivial cut has too many crossing incidences to be a matching.

A formal proof must bridge several exact interfaces: existence of suitable primes, the finite Cayley-graph construction, bipartiteness and regularity, the girth lower bound, the spectral-to-isoperimetric inequality, and Hall's theorem for the perfect matching. None of these can be replaced by a finite sample or an asymptotic slogan.

Formalization scope

Graphs are finite and simple. Connectedness is nonempty mutual graph reachability. A simple cycle is a cyclic list of at least three distinct vertices; girth at least $g$ means every such cycle has length at least $g$ , so forests satisfy every threshold. A matching cut requires both shores nonempty and is encoded by the condition that every vertex has at most one crossing neighbor. A perfect matching is represented by an adjacent involution.

The main theorem explicitly requires at least two vertices, although exact 14-regularity already forces nontrivial order; the redundant bound documents exclusion of the $K_1$ ambiguity. The mission does not claim that the frozen OPG contract was well-posed at order one. It formalizes the paper's substantive counterexample family and the consequence for the intended question.

Candidate files in the associated repository explore alternative bounded-degree constructions and integer counts. They are candidate_only and are not proof dependencies. Contributions should follow the published Lemma 5 and its cited inputs, or provide a separately sourced proof of the same declaration. The later maximum-degree-60 NP-completeness theorem is welcome as a future extension after the finite complexity framework is fixed.

Selected references

C. Feghali, F. Lucke, D. Paulusma, and B. Ries, Matching Cuts in Graphs of High Girth and H-Free Graphs, Algorithmica 87 (2025), 1199–1221. https://doi.org/10.1007/s00453-025-01318-8
C. Feghali, F. Lucke, D. Paulusma, and B. Ries, ISAAC 2023 version. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2023.31
A. Lubotzky, R. Phillips, and P. Sarnak, Ramanujan graphs, Combinatorica 8 (1988), 261–277. https://doi.org/10.1007/BF02126799
Open Problem Garden, Matching cut and girth. https://www.openproblemgarden.org/op/matching_cut_and_girth

20 thms6 active usersReviewed

Algebra Number Theory·Captain: quesswho

Collapsible CubicsOpen Problem

Motivation

A polynomial $f \in \mathbb{Q}[x]$ is split if $\deg f \ge 1$ and $f(x) = a\prod_{i=1}^{n}(x - r_i)$ for some $a \in \mathbb{Q}^\times$ and $r_1,\dots,r_n \in \mathbb{Q}$ . Split polynomials are the simplest non-constant maps defined over $\mathbb{Q}$ that one can apply to an algebraic number: they are exactly the rational polynomials all of whose roots are rational. The question here is how much such a map can do — whether it can always push an algebraic number back down into $\mathbb{Q}$ .

Say $\alpha$ is $k$ -collapsible if there are split $f_1,\dots,f_k$ with $(f_k \circ \cdots \circ f_1)(\alpha) \in \mathbb{Q}$ , collapsible if it is $1$ -collapsible, and eventually collapsible if it is $k$ -collapsible for some $k \ge 1$ . Problem 3 of Griffin Macris's list of open problems asks whether every algebraic number is eventually collapsible. The two notions come apart at degree $3$ : Jordi Ribes settled the cubic case of eventual collapsibility using a composition of three split polynomials, and for eventual collapsibility the open frontier is $\deg\alpha \ge 4$ . For the one-step notion the picture is different — degrees $1$ and $2$ are settled, and degree $3$ is open. That one-step cubic case is this mission's goal.

Setting

Let $\alpha$ be an algebraic number with $[\mathbb{Q}(\alpha):\mathbb{Q}] = 3$ . After an affine change of variable over $\mathbb{Q}$ one may assume $\alpha$ is a root of a depressed cubic

m(x) = x^3 + d\,x + e, \qquad d, e \in \mathbb{Q},

with discriminant $\Delta = \operatorname{disc}(m) = -4d^3 - 27e^2$ . When $\Delta > 0$ the cubic is totally real (three real roots); when $\Delta < 0$ it has one real root and a complex-conjugate pair. In the latter case write the roots as

\alpha_1 = -2u, \qquad \alpha_{2,3} = u \pm iv, \qquad d = v^2 - 3u^2, \quad e = 2u(u^2 + v^2),

and set $\psi = \arctan(3u/v)$ , the parameter that controls the archimedean obstruction below. Scaling $\alpha \mapsto w\alpha$ sends $(d,e) \mapsto (w^2 d, w^3 e)$ , so the single rational invariant

\tau = e^2/d^3

determines the problem up to scaling: the search space is one rational parameter, not two.

Formalization targets

Goal — every cubic algebraic number is collapsible

\forall\, \alpha \in \mathbb{C}, \quad [\mathbb{Q}(\alpha):\mathbb{Q}] = 3 \ \Longrightarrow\ \exists\, f \text{ split with } f(\alpha) \in \mathbb{Q}.

This is the weakest statement that settles the case: it fixes no bound on $\deg f$ , and asserts only that some split $f$ exists. A version with a degree bound would be strictly stronger and is not the goal, because no such bound is known — indeed the archimedean milestone below shows no uniform one can exist.

Supporting targets

The milestone list runs from the reformulation and the invariance reductions, through the known sufficient conditions, to the two obstructions and the two genuinely open sub-targets. Ordered as they are stated there:

the product criterion — $\alpha$ is collapsible iff $\prod_i(\alpha - r_i) \in \mathbb{Q}$ for some nonempty finite multiset of rationals, which turns collapsibility into a multiplicative relation in $K^\times/\mathbb{Q}^\times$ ;
affine invariance, and the completeness of $\tau$ as an invariant of the scaling action, which together justify the reduction to one parameter;
two sufficient conditions: square discriminant, and the power-family condition subsuming it;
three obstructions: gap parity in the totally real case; the archimedean degree bound when $\Delta < 0$ ; and the extension of that bound beyond cubics, to any algebraic number possessing both a real and a non-real conjugate.

The mission also carries, as a plain theorem rather than a milestone, the single open instance $x^3 + 6x + 1$ — the smallest cubic within computational reach for which no collapsing is known. It is an instance of the goal rather than a step toward it, which is why it is not on the attack path.

Significance

A proof of the goal closes the one-step cubic case and, with Ribes's composition result, would give a complete picture at degree $3$ . A disproof would be at least as informative: a single cubic $\alpha$ admitting no split $f$ with $f(\alpha) \in \mathbb{Q}$ would separate $1$ -collapsibility from eventual collapsibility by an explicit example, showing that composition is genuinely necessary and not an artefact of the known proof.

The supporting targets have value independent of the goal. The product criterion is the statement everything else is phrased against. The archimedean bound is the only known mechanism forcing $\deg f \to \infty$ , and it is what rules out a uniform-degree approach.

Status, stated precisely. Six of the eight milestones have machine-checked Lean 4 + Mathlib proofs in the author's development, against a newer Mathlib revision than this mission's environment; restating and reproving them here is a port, not new mathematics, and they are included because the goal cannot be attacked without them. The two archimedean milestones are not proved in that form. For the cubic bound both halves exist — the convexity argument and the Möbius reduction — but the statement in terms of a collapsing polynomial has not been assembled. The extension beyond cubics has not been formalised at all; the argument is the same one, since nothing in it uses cubicness beyond the identification of a single circle parameter, but that observation is not a proof. The instance $x^3 + 6x + 1$ and the goal itself are open.

Difficulty

The obvious approach is to write down a split $f$ with rational roots and force $f(\alpha) \in \mathbb{Q}$ by solving for the roots. This works when $\Delta$ is a rational square, and more generally under the power-family condition, and produces the bulk of the known examples — but it cannot work in general, for a reason that is quantitative rather than technical.

Suppose $\Delta < 0$ and $f = a\prod_i(x - r_i)$ is split with $f(\alpha) \in \mathbb{Q}$ . Irreducibility of $m$ forces $f - c$ to be divisible by $m$ , hence $f(\alpha_1) = f(\alpha_2) \ne 0$ , hence $\prod_i \frac{\alpha_1 - r_i}{\alpha_2 - r_i} = 1$ . Each factor lies on a fixed circle through $0$ and $1$ determined by $\psi$ , and a convexity argument on $\log\cos$ then forces

\deg f \ \ge\ \pi/\psi.

As $\tau \to 0^+$ one has $\psi \to 0$ , so the required degree is unbounded: there is no uniform degree in which to search, and any construction must produce split polynomials of growing degree. This is the central difficulty. For $x^3 + 6x + 1$ the bound already gives $\deg f \ge 32$ , which is why that cubic resists the searches that settle its neighbours.

Only one step of this argument is special to cubics: the identification of the circle parameter as $3u/v$ . For an algebraic number of any degree with a real conjugate $\alpha_1$ and a non-real conjugate $\alpha_2$ , irreducibility gives the same relation $\prod_i (\alpha_1 - r_i)/(\alpha_2 - r_i) = 1$ , the images again lie on a circle through $0$ and $1$ , and the parameter is $\lambda = (\operatorname{Re}\alpha_2 - \alpha_1)/\operatorname{Im}\alpha_2$ , which specialises to $3u/v$ in the depressed-cubic case. The obstruction therefore constrains the whole conjecture, not merely its cubic case, which is why the extension is carried as a milestone in its own right.

In the totally real case ( $\Delta > 0$ ) the archimedean argument gives nothing at all — the relevant Möbius maps are real and surject onto $\widehat{\mathbb{R}}$ — and the only known constraint is that each gap between consecutive conjugates contains an even number of roots of $f$ . Whether degrees stay bounded there is itself unsettled.

Formalization scope

Representation. IsSplit f says $0 < \deg f$ and $f = C\,a \cdot \prod_{r \in rs}(X - r)$ for a nonzero rational $a$ and a multiset $rs$ of rationals; multiplicities are therefore allowed and the roots need not be distinct. Collapsible α is stated for $\alpha$ in an arbitrary field $K$ carrying a $\mathbb{Q}$ -algebra structure, not only for $K = \mathbb{C}$ , so the results apply verbatim to a root in $\mathbb{R}$ , in $\mathbb{C}$ , or in $\mathbb{Q}[x]/(m)$ . The goal theorem is stated over $\mathbb{C}$ , with "cubic" expressed as $\deg(\operatorname{minpoly}_{\mathbb{Q}}\alpha) = 3$ .

Ruling out a trivialisation. Collapsible places no lower bound on $\deg f$ and does not require the value $c = f(\alpha)$ to be nonzero, so one must check that the goal is not satisfiable by degenerate means. It is not: $c = 0$ would make $m \mid f$ , impossible for an irreducible cubic $m$ dividing a polynomial that splits over $\mathbb{Q}$ . Constant $f$ is excluded by $0 < \deg f$ . Nothing in the statement is vacuous — the hypotheses of the goal are satisfied by every cubic irrationality.

Conventions in the archimedean milestones. In the cubic bound the parameters $u, v$ enter as real numbers satisfying the factorisation identity, with the normalisation $0 < uv$ ; this is not a restriction, since $v$ is determined only up to sign and the sign may be chosen. Under it $\psi = \arctan(3u/v) \in (0, \pi/2)$ , and the conclusion is $\pi/\psi \le \deg f$ with $\deg f$ the natural-number degree.

In the general bound the corresponding normalisation is $0 < (\operatorname{Re}\alpha_2 - \alpha_1)\operatorname{Im}\alpha_2$ . It forces $\operatorname{Im}\alpha_2 \neq 0$ , so $\alpha_2$ is genuinely non-real and $\lambda > 0$ , hence $\psi \in (0,\pi/2)$ and no division-by-zero value can arise in the conclusion. Passing to the complex conjugate of $\alpha_2$ flips the sign of both factors, so the condition is a choice of conjugate rather than a restriction — except when $\operatorname{Re}\alpha_2 = \alpha_1$ , which the hypothesis excludes and which cannot occur for a depressed cubic with $\Delta<0$ . No degree hypothesis on $m$ is needed: possessing both a real and a non-real root already forces $\deg m \ge 3$ .

Infrastructure. A complete development needs Polynomial, Multiset, minpoly, and for the archimedean bound Real.arctan, Complex.arg, and strict concavity of $\log\cos$ on $(-\pi/2, \pi/2)$ . The convexity and Möbius lemmas are reusable well beyond this mission — they bound the number of factors in any product of complex numbers constrained to a circle through the origin. Contributions of any of the supporting targets are welcome independently of the goal; so is a disproof, and so is an explicit collapsing of $x^3 + 6x + 1$ of any degree.

Selected references

Griffin Macris, List of open problems, Problem 3. https://sites.google.com/view/griffinmacris/open-problems
Miles, Collapsible algebraic numbers, 2026. https://quesswho.github.io/miles-blog/2026/08/20/collapsible/ — source of the definitions of split, $k$ -collapsible, collapsible and eventually collapsible used above, of Ribes's cubic result for eventual collapsibility, and of the statement that the degree- $3$ case of one-step collapsibility is open.

21 thms6 active usersReviewed

Completed

Combinatorics Graph Theory·Captain: hao jia

Formalizing an 8-Vertex Candidate Counterexample to the Geodesic-Cycle Assignment Problem (OPG-500)Open Problem

[VM-STATUS-20260908-R05-PROVED]

Status update (2026-09-08): The root theorem OPG500Counterexample.eight_vertex_counterexample is now Proved by an accepted Prove2Me submission. All six milestones are proved and the root has zero open leaves. The accepted proof has also been independently rebuilt with Lean 4.33.1 / Mathlib 0df444a360eaa60ab8c11dca51a86af692955474. The historical text below describes the mission as it stood before formal closure.

Motivation and historical context

Peripheral cycles occupy a distinguished place in structural graph theory. A cycle is peripheral when it is induced and does not separate the graph after its vertices are removed. Tutte proved in 1963 that the peripheral cycles of a finite 3-connected graph generate its binary cycle space. This theorem links a local, visibly embedded kind of cycle to the global algebraic structure of all cycles.

Weighted geodesic cycles provide a different generating family. Georgakopoulos and Sprüssel proved in 2009 that, for every finite graph with positive edge lengths, every cycle is a binary sum of weighted geodesic cycles whose lengths do not exceed the length of the original cycle. In the same paper they posed Problem 3: can the edges of every finite 3-connected graph be assigned positive lengths so that every weighted geodesic cycle is peripheral? A positive answer would recover Tutte's generation theorem through metric structure.

The present target tests the opposite possibility on one explicitly specified graph with eight vertices. A candidate argument and finite certificates are available in the frozen OPG-500 research repository, but those artifacts are explicitly marked candidate_only: they are neither a published counterexample nor a machine-checked resolution. The purpose of the formal target is to determine whether the proposed universal obstruction survives complete definition, proof, and statement-faithfulness checks.

Setting

Let $G$ be a finite simple graph. A positive edge-length assignment is a function

\ell:E(G)\longrightarrow \mathbb R

such that $\ell(e)>0$ for every edge $e$ . The length of a finite path or cycle is the sum of the lengths of its edges.

A simple cycle $C$ is $\ell$ -geodesic when, for every pair of vertices $x,y$ on $C$ , at least one of the two $x$ – $y$ arcs of $C$ has length equal to the shortest-path distance between $x$ and $y$ in $G$ . Equivalently, there is no $x$ – $y$ path in $G$ whose length is strictly smaller than both $x$ – $y$ arcs of $C$ . The definition concerns vertices of the cycle and permits ties between shortest paths.

A simple cycle is peripheral when it is induced and deleting all of its vertices leaves a connected graph or the empty graph. This is vertex deletion, not edge deletion.

Fix the graph $H$ on vertices $0,1,\ldots,7$ . The vertices $0,1,2,3$ induce $K_4$ . For each $i\in\{0,1,2,3\}$ , set $y_i=7-i$ and join $y_i$ to exactly the three core vertices other than $i$ . The four vertices $y_i$ are pairwise nonadjacent. Thus the frozen edge set is

\{01,02,03,04,05,06,12,13,14,15,17,23,24,26,27,35,36,37\}.

The labels and edge set are part of the statement and are not interchangeable with earlier candidate labelings without an explicit isomorphism.

Formalization targets

Main target: the universal eight-vertex obstruction

Formalize the following statement for the fixed graph $H$ :

H\text{ is 3-connected}\quad\text{and}\quad \forall\ell:E(H)\to\mathbb R_{>0},\; \exists C,\; C\text{ is an $\ell$-geodesic simple cycle of $H$ and is not peripheral}.

The existential cycle may depend on $\ell$ . The universal quantifier includes all strictly positive real assignments, including assignments with tied shortest paths. This is the stable target; finite samples and rational specializations are subordinate checks rather than replacements for it.

Supporting targets

The development should also formalize the finite weighted geodesic-cycle generation theorem of Georgakopoulos and Sprüssel, the exact 3-connectivity and peripheral-cycle classification of $H$ , the required shortest-path and tight-subgraph statements, the finite cycle-space rank statements, and the finite minimum/descent principle used to select a cycle outside a closed binary span. These targets should remain separate declarations so that their assumptions and reuse boundaries are visible.

Significance

A proof of the main target would give a negative answer to the finite problem by exhibiting a 3-connected graph for which no positive edge weighting can make all geodesic cycles peripheral. It would not contradict Tutte's theorem: peripheral cycles may still generate the cycle space even though they cannot be made to contain every geodesic cycle for any weighting. The distinction between these two generation mechanisms is part of the mathematical content.

A formal development would add more than a checked final sentence. It would provide reusable definitions for positively weighted finite graphs and vertex-geodesic cycles, a precise treatment of the two arcs between cycle vertices, explicit deletion semantics for peripheral cycles, and finite cycle-space infrastructure. It would also separate purely finite graph facts from statements quantified over arbitrary real weights. The candidate repository currently supplies finite enumeration and abstract Lean fragments, but no existing artifact checks this full dependency chain.

Until the complete main theorem is verified, the eight-vertex graph remains a candidate obstruction and the original problem remains unresolved by this development.

Difficulty

The central difficulty is the universal quantification over real edge lengths. Testing many integer or rational vectors cannot cover it. Shortest paths need not be unique, so an argument that silently perturbs the weights or assumes unique geodesics can change which cycles are geodesic. Every strict and weak inequality must therefore agree with the source definition, including tie cases.

The graph is small but the semantic boundary is not. A formal cycle representation must expose the two cycle arcs for every vertex pair without admitting malformed or repeated-vertex objects. The peripheral predicate must combine inducedness with connectivity after vertex deletion and must classify all cycles, not only a selected family of triangles. Finally, finite cycle-space computations and rank inequalities must be connected to actual paths and weighted geodesicity; a propositional or enumerative certificate alone does not establish that bridge.

Formalization scope

The Lean development will use Fin 8 for the vertices of $H$ and a SimpleGraph representation for adjacency. Weights will be functions on the edge subtype, so values on nonedges cannot affect the theorem. All weights are real and strictly positive. Paths and cycles are finite and simple; arbitrary walks do not count as target witnesses. Geodesicity is vertex-based and includes tied shortest paths. Peripheral cycles use inducedness and vertex deletion, with a connected-or-empty remainder.

The main theorem must retain the quantifier order “for every weighting, there exists a cycle.” It may not be weakened to rational weights, finitely many tested assignments, nonnegative weights, one selected weighting, edge-geodesicity, or the assertion that only four named core triangles fail to be peripheral. Definitions must be sorry-free, and nontrivial mathematical claims must be theorem declarations with separately checked proofs.

Reusable contributions include finite weighted-path length, shortest-path attainment in finite positive graphs, the equivalence of the two geodesic formulations, cycle-arc APIs, vertex-deletion connectivity, binary edge-vector encodings, and finite descent outside a closed span. Graph-specific finite certificates are welcome only when their checker is represented in Lean or their conclusions are otherwise proved in the kernel.

Selected references

A. Georgakopoulos and P. Sprüssel, Geodetic topological cycles in locally finite graphs, Electronic Journal of Combinatorics 16 (2009), R144. Section 3.1, Theorem 3.1; Section 5, Problem 3. https://arxiv.org/abs/0911.3999v1
Open Problem Garden, Geodesic cycles and Tutte's Theorem, problem statement and vertex-based definition. https://www.openproblemgarden.org/op/geodesic_cycles_and_tuttes_theorem
W. T. Tutte, How to draw a graph, Proceedings of the London Mathematical Society 13 (1963), 743–768. Cited as reference [18] by Georgakopoulos and Sprüssel for peripheral-cycle generation.
Vibe Mathing, frozen OPG-500 candidate repository at commit a41fe59b4535851ea55f6e868e938b9aaf81e924. https://github.com/vibemathing/problem-opg-500-geodesic-cycles/tree/a41fe59b4535851ea55f6e868e938b9aaf81e924

9 thms6 active usersReviewed

Linear Optimization Operations Research Optimization+1·Captain: ORdos

Smale's Ninth Problem: Strongly Polynomial Linear ProgrammingOpen Problem

The problem of solving linear inequalities

The linear feasibility problem takes a matrix $A \in \mathbb{R}^{m\times n}$ and a vector $b \in \mathbb{R}^m$ and asks whether the system of $m$ linear inequalities in $n$ real unknowns

\{\,x \in \mathbb{R}^n \mid Ax \ge b\,\} \;\ne\; \emptyset

has a solution. By linear programming duality, optimizing a linear objective over such a set reduces to feasibility, so this decision problem carries the whole complexity of linear programming.

What "polynomial time" means here depends on the machine. In the bit model the input is a list of rational numbers, its size $L$ counts the bits of all numerators and denominators, and an algorithm is polynomial if it runs in time $\mathrm{poly}(m, n, L)$ . In the real-number model the input is a list of $mn + m$ exact real numbers, each arithmetic operation ( $+, -, \times, \div$ ), comparison, or memory move costs one unit, and a running time may only depend on $m$ and $n$ . An algorithm polynomial in this second sense is what Smale asks for; the closely related bit-model notion — $\mathrm{poly}(m,n)$ arithmetic operations and polynomially bounded intermediate bit sizes — is called strongly polynomial. This mission fixes the real-number model precisely as a Blum–Shub–Smale (BSS) machine (Blum–Shub–Smale 1989): a finite program of instructions acting on a bi-infinite tape $\mathbb{Z} \to \mathbb{R}$ of real registers — loads of arbitrary real machine constants, exact field arithmetic at fixed addresses, two-sided tape shifts, a sign-test branch, and accept/reject — with cost equal to the number of executed instructions. The convention that costs something: the program must be uniform, one finite instruction list serving every $m$ , $n$ , and every real instance. Uniformity is exactly what separates the question from point-location tricks available to non-uniform families of decision trees.

Why it matters

For optimization, the question is the last gap in the complexity of its central problem. Linear programs with combinatorial structure already admit strongly polynomial algorithms — Tardos (1986) solved every LP whose running time may depend on the entries of $A$ but not on $b$ or $c$ , covering network flows and all $\{0,\pm1\}$ -constraint problems — and a positive answer for general LP would extend that unification to the whole class, while explaining why simplex-type methods behave so well in practice (Spielman–Teng 2004).

For the theory of computation over the reals, the problem is a benchmark for what unit-cost exact arithmetic can do: it is Problem 9 on Smale's list of mathematical problems for the twenty-first century (Smale 1998), posed in the BSS model as the real-number analogue of the P-versus-NP style questions of that program, and it interacts with polyhedral combinatorics through the polynomial Hirsch conjecture: a polynomial bound on polytope diameters is a necessary condition for any polynomial pivot rule. A problem that calibrates both the practice of optimization and the foundations of real computation is a subject, not a special case.

The question and what is known

\textbf{Question (Smale's 9th).}\quad \text{Is there a uniform BSS program deciding } \{x \mid Ax \ge b\} \ne \emptyset \text{ in } \mathrm{poly}(m,n) \text{ steps?}

The timeline splits into a negative branch (lower bounds against algorithm classes) and a positive branch (polynomial algorithms in weaker senses).

Lower bounds. Klee–Minty (1972) constructed a deformed cube on which Dantzig's largest-coefficient simplex rule visits all $2^n$ vertices; analogous exponential examples were later found for essentially every deterministic pivot rule, and randomized rules were driven to subexponential lower bounds by Friedmann–Hansen–Zwick (2011) — against upper bounds of $\exp(O(\sqrt{n \log n}))$ from Kalai (1992) and Matoušek–Sharir–Welzl (1996). On the interior-point side, Allamigeon–Benchimol–Gaubert–Joswig (2018) showed by tropical methods that log-barrier path following is not strongly polynomial, and Allamigeon–Gaubert–Vandame (2022) extended this to every self-concordant barrier: no interior-point method of that class can settle the question positively.

Polynomial algorithms in weaker senses. Khachiyan (1979/80) proved LP feasibility is polynomial in the bit model via the ellipsoid method; Karmarkar (1984) and then Renegar (1988) brought interior-point methods to $O(\sqrt{n}\,L)$ iterations. Megiddo (1984) solved LP in linear time for every fixed dimension; Tardos (1986) gave the combinatorial strongly polynomial class; Vavasis–Ye (1996) and Dadush–Huiberts–Natura–Végh (2020) replaced the bit size by condition measures of $A$ alone; Ye (2011) proved policy iteration strongly polynomial for fixed-discount Markov decision processes.

The central difficulty is visible in every positive result: each known iteration count is controlled by a scale-dependent quantity — bit length, condition number, barrier curvature — that is unbounded over the real instances with $m, n$ fixed. The naive plan, "run the ellipsoid method and round", fails at its first step in the real model: the number of iterations needed to separate a feasible system from an infeasible one grows with the thinness of the feasible set, which is not a function of $(m, n)$ ; no data-independent perturbation $\varepsilon$ exists when the data are arbitrary reals. All results above are proved on paper only; none has a machine-checked proof in the literature. What is already formalized, on this platform, is the substrate this mission builds on: the simplex iteration (mission Introduction to Linear Optimization IV), the ellipsoid method with its volume-halving correctness theorem (XI), interior-point path following (XII), and self-concordance with the barrier method (Convex Optimization VI).

A hierarchy of formalization targets

The mission's milestone list realizes this hierarchy in order; each level states what it deliberately leaves open.

Level 0 — the model works. A uniform BSS program decides one-variable feasibility in linear time:

\exists\,P,\,C\ \ \forall m,\ \forall (a,b) \in \mathbb{R}^m \times \mathbb{R}^m:\ P \text{ decides } \{x \in \mathbb{R} \mid a_i x \ge b_i\ \forall i\} \ne \emptyset \text{ within } C(m{+}1) \text{ steps}.

It fixes nothing about $n \ge 2$ ; its role is to certify that the machine model and cost semantics of the goal are non-vacuous.

Level 1 — the classical method is exponential. On the Klee–Minty cube, Dantzig's rule admits a run of

2^n - 1 \text{ pivots}

from the all-slack basis to the optimum. It leaves open all other pivot rules — extensions to further rules are welcome as strengthenings.

Level 2 — the bit model succeeds. Through the Cramer–Hadamard solution bound $|x_j| \le n!\,U^n$ and the perturbation estimates, Khachiyan's theorem: for integer data bounded by $U$ , every admissible ellipsoid run decides feasibility within

t^* \le 10^6\,(n{+}2)^4(\log_2 U + n + 2) \text{ iterations}.

The generous constants are deliberate — only the polynomial order is load-bearing. This level leaves open exactly the dependence on $\log U$ .

Level 3 — the goal (open). A uniform program with data-independent polynomial cost:

\exists\,P,\,C,\,d\ \ \forall m, n, A, b:\ P \text{ decides } \{x \mid Ax \ge b\} \ne \emptyset \text{ within } C\,(mn + m + 2)^d \text{ steps}.

The statement asserts only the shape of the truth — no hard-coded degree or constant — so it is stable under every future quantitative improvement. These levels do not exhaust the project: Tardos' combinatorial LP theorem, Ye's fixed-discount MDP result, and impossibility statements for restricted program classes in the style of Allamigeon–Gaubert–Vandame are natural later milestones.

Formalization scope

Polyhedra, simplex states, pivots, and ellipsoid runs are the platform's existing LinearOptimization development over Matrix (Fin m) (Fin n) ℝ, with $\{x \mid Ax \ge b\}$ as polyhedron A b; algorithms with data-dependent iteration counts are formalized as run predicates, as in the parent missions. The new SmaleNinth definitions supply what the goal genuinely needs and the run-predicate style cannot express: a concrete inductive type of BSS programs with operational semantics and unit-cost accounting, the Klee–Minty data with Dantzig's rule, and the explicit Khachiyan constants. One convention closes the degenerate escape hatch: the goal quantifies over finite BSSProgram terms under the fixed encodeLP input convention — formalizing "algorithm" as an arbitrary function $\mathbb{R}^{mn+m} \to \mathrm{Bool}$ would make the statement trivially true and is not the theorem. Division is totalized as $x/0 = 0$ and the branch test is $x_i \le 0$ ; both are benign for the class of programs quantified over.

The machine module is infrastructure beyond this mission — any real-number complexity statement (other Smale problems, sums-of-square-roots, BSS-completeness) can reuse it, as can any pivot-rule lower bound reuse the Klee–Minty module. Formalization forces distinctions the literature leaves informal: which machine variant carries the unit-cost claim, how ties in Dantzig's rule are resolved, and which of the interchangeable Khachiyan constants each estimate actually needs. Welcome contributions include proofs of any milestone, alternative exponential instances for other pivot rules, sharper constants in the Khachiyan module, and ports of the known strongly polynomial special cases.

Selected references

L. Blum, M. Shub, S. Smale, On a theory of computation and complexity over the real numbers, Bull. AMS 21(1):1–46, 1989. DOI
S. Smale, Mathematical problems for the next century, Math. Intelligencer 20(2):7–15, 1998. DOI
V. Klee, G. J. Minty, How good is the simplex algorithm?, in Inequalities III, Academic Press, 1972, pp. 159–175.
L. G. Khachiyan, Polynomial algorithms in linear programming, USSR Comput. Math. Math. Phys. 20:53–72, 1980. DOI
N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4:373–395, 1984. DOI
J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Math. Programming 40:59–93, 1988. DOI
É. Tardos, A strongly polynomial algorithm to solve combinatorial linear programs, Oper. Res. 34(2):250–256, 1986. DOI
N. Megiddo, Linear programming in linear time when the dimension is fixed, J. ACM 31(1):114–127, 1984. DOI
G. Kalai, A subexponential randomized simplex algorithm, STOC 1992. DOI
O. Friedmann, T. D. Hansen, U. Zwick, Subexponential lower bounds for randomized pivoting rules for the simplex algorithm, STOC 2011. DOI
D. A. Spielman, S.-H. Teng, Smoothed analysis of algorithms: why the simplex algorithm usually takes polynomial time, J. ACM 51(3):385–463, 2004. DOI
S. A. Vavasis, Y. Ye, A primal-dual interior point method whose running time depends only on the constraint matrix, Math. Programming 74:79–120, 1996. DOI
Y. Ye, The simplex and policy-iteration methods are strongly polynomial for the Markov decision problem with a fixed discount rate, Math. Oper. Res. 36(4):593–603, 2011. DOI
X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Log-barrier interior point methods are not strongly polynomial, SIAM J. Appl. Algebra Geom. 2(1):140–178, 2018. DOI
X. Allamigeon, S. Gaubert, N. Vandame, No self-concordant barrier interior point method is strongly polynomial, STOC 2022. arXiv
D. Dadush, S. Huiberts, B. Natura, L. A. Végh, A scaling-invariant algorithm for linear programming whose running time depends only on the constraint matrix, STOC 2020. arXiv
D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 (Chapters 3, 8, 9 — formalized in the Introduction to Linear Optimization mission series).
B. Korte, J. Vygen, Combinatorial Optimization: Theory and Algorithms, 6th ed., Springer, 2018, §4.1–4.5.

29 thms6 active usersReviewed

Completed

Number Theory·Captain: davidloeffler

Ordinary p-adic L-functions: Mazur–Tate–Teitelbaum interpolationResearch Paper

Why construct a p-adic L-function?

A modular form has a complex L-function whose critical values carry arithmetic information. To compare those values in p-adic families, their transcendental period factors must first be removed. The remaining algebraic numbers can then be embedded into a p-adic field. The result sought here is a single bounded measure encoding the critical values of all twists by characters of p-power conductor. This is the existence and interpolation theorem underlying the cyclotomic p-adic L-function (one of the most fundamental objects of Iwasawa theory).

The reference is the famous paper of Mazur, Tate and Teitelbaum, Chapter I, especially §§10–14 (MTT); but for simplicity we are treating only the ordinary case here (not the more general finite-slope case), and not attacking the results later in MTT (exceptional-zero conjectures, etc).

Modular forms, periods, and measures

Fix a prime $p$ , a positive integer $N$ , and a weight $k\ge2$ . Let $f$ be a normalized cuspidal Hecke eigenform of weight $k$ on $\Gamma_1(N)$ with nebentypus $\epsilon$ and Fourier coefficients $a_n$ (necessarily algebraic). Fix embeddings $\iota_\infty:\overline{\mathbb Q}\hookrightarrow\mathbb C$ and $\iota_p:\overline{\mathbb Q}\hookrightarrow\mathbb C_p$ . No condition $p\nmid N$ is imposed. The character $\epsilon$ is extended by zero on nonunits modulo $N$ .

The form is ordinary when $|\iota_p(a_p)|_p=1$ . The ordinary root $\alpha$ is the root of

X^2-\iota_p(a_p)X+\iota_p(\epsilon(p))p^{k-1}

with $|\alpha|_p=1$ . This convention also covers the $U_p$ case: if $p\mid N$ , then $\epsilon(p)=0$ and the unit root is $\iota_p(a_p)$ (MTT I.§12).

A measure means a continuous $\mathbb C_p$ -linear functional on the continuous functions $C(\mathbb Z_p^\times,\mathbb C_p)$ . It is a bounded p-adic measure, rather than a positive real-valued measure. The Lean representation is Mathlib's AbstractMeasure on (PadicInt p)ˣ.

The two periods $\Omega^+$ and $\Omega^-$ normalize the signed modular integrals. Write

\Phi_j(r)=2\pi\int_0^\infty f(r+it)(r+it)^j\,dt,

and use $(\Phi_j(r)+s(-1)^j\Phi_j(-r))/2$ for sign $s\in\{+1,-1\}$ . A period system specifies nonzero periods, algebraic normalized values for $0\le j\le k-2$ , and finite generation over $\mathbb Z$ of the lattice generated by these values. Period rationality and finite generation are separate mathematical obligations, combining Manin–Shimura rationality with the module-of-values construction in MTT I.§2; see also the explicit treatment of general eigenforms in Williams, §11.7.

Formalization targets

The goal is to construct an ordinary root, a period system, and a measure $\mu$ with the following interpolation property. Let $\chi$ be a primitive Dirichlet character of conductor $m=p^n$ , where $n\ge0$ , and let $0\le j\le k-2$ . Put $s=\chi(-1)(-1)^j$ . With the positive-exponential Gauss sum $\tau(\chi)=\sum_{a\bmod m}\chi(a)e^{2\pi ia/m}$ , define the algebraic number $A_{\chi,j}$ by

\iota_\infty(A_{\chi,j})= \frac{m^{j+1}j!}{(-2\pi i)^j\tau(\chi^{-1})\Omega^s} L(f_{\chi^{-1}},j+1).

The required identity is

\int_{\mathbb Z_p^\times}\iota_p(\chi(x))x^j\,d\mu(x) =e_p(\alpha,\chi,j)\,\iota_p(A_{\chi,j}),

where all algebraic character values in the following expression are transported by $\iota_p$ :

e_p(\alpha,\chi,j)=\alpha^{-n} \left(1-\frac{\iota_p(\chi^{-1}(p)\epsilon(p))p^{k-2-j}}{\alpha}\right) \left(1-\frac{\iota_p(\chi(p))p^j}{\alpha}\right).

This is the scalar period-normalized form of MTT I.§14. At $n>0$ both character values at $p$ vanish, leaving $\alpha^{-n}$ . At $n=0$ the primitive character is the character of modulus one, and both Euler factors remain. The latter case is included explicitly.

Seven milestones isolate period rationality and its finite lattice; existence and uniqueness of the ordinary root; the distribution relation for polynomial disk moments; uniform boundedness of constant disk masses; unique extension to a measure with every critical polynomial moment; the complex Birch–Mellin identity; and the deduction of interpolation from the two signed measures. Their source locations are recorded individually. The period milestone combines two standard inputs; the boundedness and extension milestones specialize the MTT construction to slope zero.

What the formalization supplies

The result supplies the analytic input for studying p-adic special values and their variation. It also supplies reusable infrastructure for normalized modular integrals, rational period systems, finite-order twists, and bounded measures on p-adic units. The classical existence theorem is known. The work proposed here is to prove the stated Lean theorems and connect the existing Mathlib analytic and algebraic infrastructure. Local compilation establishes that the declarations are well-typed; the mission statements remain unproved targets.

Where the difficulty lies

Listing algebraic critical values does not establish that one bounded measure interpolates them. Values on nested residue disks must satisfy compatibility, and ordinary boundedness must control the extension to continuous functions. Polynomial moments of positive degree must agree with that same extension. The unramified character requires its own Euler-factor calculation; simply applying the ramified formula at conductor one loses factors. On the complex side, rationality requires genuine periods of the modular form, not arbitrary chosen scaling constants. These are the obligations represented by the milestones.

Formalization scope and conventions

The cusp form is Mathlib's analytic CuspForm, with Fourier coefficients tied to its width-one q-expansion. The nebentypus transformation law and every prime Hecke eigenvalue equation are written explicitly. The prime Hecke operator includes both its translated sum and its second term; when the prime divides the level, the second term vanishes. The complex twist is the finite-translate expression for $f_{\chi^{-1}}$ , and its critical L-value is defined by the actual Mellin integral. Neither an arbitrary L-value table nor the desired measure is an input assumption.

The embeddings share the abstract algebraic closure of $\mathbb Q$ ; there is no asserted continuous map from $\mathbb C$ to $\mathbb C_p$ . The algebraic bridge in each interpolation identity is existential and constrained by a complex equality. Test functions are existential continuous maps constrained pointwise to equal the specified character or disk function; this makes their continuity part of the conclusion instead of an unproved definition. All primes, including $2$ , are allowed. Natural-number subtractions occur only in theorem contexts with $k\ge2$ and $j\le k-2$ .

The signed projections use a factor of $1/2$ . Their normalized measures are added, and the period sign is $\chi(-1)(-1)^j$ . These conventions fix the powers, sign, Gauss sum, and periods in the displayed interpolation formula. Periods are not asserted to be canonical integral periods; rescaling by algebraic constants changes the normalization. Exceptional-zero derivative formulas, positive-slope distributions, tame-conductor twists, and Iwasawa main conjectures are outside this mission.

Selected references

B. Mazur, J. Tate and J. Teitelbaum, On p-adic analogues of the conjectures of Birch and Swinnerton-Dyer, Inventiones Mathematicae 84 (1986), 1–48, Chapter I, §§1–4 and 7–14. DOI; digitized original.
G. Shimura, On the periods of modular forms, Mathematische Annalen 229 (1977), 211–221. DOI.
C. Williams, An introduction to p-adic L-functions II: Modular forms, lecture notes, §§11.6–11.8, particularly Proposition 11.21, for period normalization of general eigenforms. Author's notes.

124 thms6 active usersReviewed

Completed

Combinatorics Discrete Geometry·Captain: mysticflounder

Erdős Problems 97 and 96: Convex Point Sets and Unit DistancesOpen Problem

Closed — negative resolution of Erdős Problems 96 and 97

Adam McKenna closed this mission on 13 September 2026 following Unit distances in convex polygons, by Liam Kruer, Jensen Kohlmeyer, and Liam Price. Their construction gives strictly convex point sets with Ω(n log log n) unit-distance pairs and arbitrarily large minimum unit-distance degree, answering both questions and the general fixed-k version of Problem 97 negatively.

Paper and complete Lean source. All credit for the counterexample and its formalization belongs to those authors. Adam McKenna prepared the Prove2Me adapters.

Do not start further proof attempts or solver runs for the affirmative conjectures. Existing statements, conditional lemmas, partial proofs, and milestones remain as historical work. The owner has authorized closure assuming the external result is correct; individual theorem pages report Prove2Me verification status.

Historical mission description

Motivation

The mission is to prove the combined open goal

\text{Problem 97} \;\land\; \text{Problem 96}

for finite point sets in strictly convex position in the Euclidean plane.

Why Problems 97 and 96 belong together

Problem 97 gives the local step needed for Problem 96. Assume Problem 97. Every nonempty convex-independent finite set then has a vertex with at most three neighbors at each positive radius, in particular at radius $1$ . Delete that vertex and preserve convex independence. Apply the same step to every subset created by deletion until no points remain. Charge each unordered unit-distance pair to the first endpoint deleted. Each deleted vertex receives at most three charges, so an $n$ -point set determines at most $3n$ unordered unit-distance pairs. This gives the Problem 96 bound and therefore $O(n)$ . The package uses this one-way dependency; it does not seek a reverse implication.

Setting

Let $A\subset\mathbb R^2$ be finite. Strict convex position means that every point of $A$ is an extreme point of the convex hull of $A$ . For $p\in A$ , the pinned multiplicity at radius $r>0$ counts points $q\in A$ with $\lVert p-q\rVert=r$ . Problem 97 asks for a point where no radius has four such other points. Problem 96 counts unordered pairs at distance $1$ , then takes the supremum over convex-independent $n$ -point sets.

The historical progression is part of the setting. Erdős’s 1946 paper posed an earlier three-neighbor version. His 1987 account reports Danzer’s convex nonagon in which every vertex has three equidistant witnesses, and asks about four witnesses. Fishburn and Reeds’s 1992 work gives a 20-vertex convex configuration with the same unit distance at every vertex, placing the local question beside the unit-distance problem.

Target

The Problem 97 target is the canonical statement that every nonempty finite convex-independent $A$ has no four-equidistant-point property:

\forall A,\quad A\ne\varnothing\;\to\;\operatorname{ConvexIndep}(A) \;\to\;\neg\operatorname{HasNEquidistantProperty}(4,A).

The Problem 96 target is the canonical asymptotic statement

U_c(n)=O(n),

where $U_c(n)$ is the supremum of the unordered unit-distance counts determined by convex-independent $n$ -point sets. The bound is asymptotic; the Problem 97 route would give the stronger explicit bound $U_c(n)\le3n$ for every natural number $n$ .

Significance

The package records a formal proof route joining a pinned geometric obstruction to a global extremal bound. A successful Problem 97 proof would immediately settle Problem 96 with the explicit constant $3$ , while preserving the combinatorial meaning of the count. It also separates the historical three-neighbor constructions from the still-open four-neighbor assertion.

Difficulty

The source proof reduces Problem 97 to strong induction on $|A|$ . Its counting engine follows Dumitrescu's 2006 isosceles-count method, with the cap-witness refinements used in the source attributed to Nivasch--Pach--Pinchasi--Zerbib (2013). This engine forces every counterexample to have at least nine points; a finite geometric analysis excludes exactly nine points; and the remaining step must produce a removable vertex for every larger minimal counterexample. The removable-vertex statement carries the induction hypothesis that every strictly smaller nonempty convex 4-equidistant set is contradictory. That large-cardinality geometric step remains open, so both headline targets remain open. Finite computational certificates can support local cases but do not replace the universal geometric statement.

Counterexample routes

Problem 97 is open, so the mission also records the parallel negative route. The source formalization calls a nonempty convex-independent finite set with the four-equidistant property a Problem97.IsCounterexample. Constructing one such set would refute Problem 97 and therefore refute the mission's affirmative conjunction, regardless of whether Problem 96 remains true. The counterexample milestone keeps this resolution path visible beside the nonexistence proof. A successful witness must use exact coordinates or exact algebraic data from which Lean verifies both strict convex position and the four-equidistant property; a numerical approximation or a realizable incidence pattern alone is insufficient.

Problem 96 has its own negative route. Because its claim is asymptotic, one finite convex configuration cannot refute it. A counterexample must instead give convex-independent point sets at arbitrarily large cardinalities whose unit-distance counts exceed every proposed linear constant. The mission tracks this superlinear-family statement separately, together with a reduction from it to the exact negation of Problem 96. This keeps both possible outcomes visible: a direct or Problem-97-derived linear upper bound, and an explicit family proving that no such bound exists.

Formalization scope

The canonical source is pinned at commit 757d852766f377f7c1a0ffeeef6d3526bc0cb7a4. It contains the formal source statements for Problem 97 and Problem 96. The source repository reports closed proofs of the conditional bridge to the $3n$ bound (conditional three-times bound), the $|A|\ge9$ counting milestone (nine-point counting bound), and the exact nine-point exclusion (exact nine-point exclusion theorem). The remaining large-cardinality milestone is the removable-vertex step, with its minimality hypothesis retained. The current platform mission contains accepted transfers of the counting argument, the conditional bridge, and the exact nine-point exclusion, while the removable-vertex step remains open. Its definitions make convex independence and the positive-radius condition explicit; no theorem is assumed inside a definition. Singletons and two-point sets are included in Problem 97, while Problem 96's counting definitions also include the empty set. The source repository uses Lean v4.27.0; these mission statements target the platform's v4.33.1. Source-proof transfer and revalidation remain separate work. The Lean declarations and proofs are this project's own formalization. The Dumitrescu and Nivasch--Pach--Pinchasi--Zerbib citations record mathematical provenance; they do not indicate that a paper proof was imported or machine-checked directly.

These source results establish the intended dependency graph: the P97 universal root feeds low-unit-degree extraction, strong induction, and then the P96 supremum bound. The platform mission records those contracts and milestones; it does not claim to have transplanted their proof bodies. The milestones include the two canonical roots, their conditional bridge, the |A| ≥ 9 count, the n = 9 exclusion, the |A| > 9 removable-vertex step, the documented Danzer nine-point three-neighbor example, the parallel goal of constructing a Problem 97 counterexample, and the superlinear-family route to a counterexample to Problem 96.

References

Erdős, On Sets of Distances of n Points (1946), DOI.
Erdős, Some Combinatorial and Metric Problems in Geometry (1987), scan.
Fishburn–Reeds, Unit Distances Between Vertices of a Convex Polygon (1992), publisher record.
Dumitrescu, On Distinct Distances from a Vertex of a Convex Polygon (2006), Springer record; provenance for the source counting method.
Nivasch–Pach–Pinchasi–Zerbib, The Number of Distinct Distances from a Vertex of a Convex Polygon (2013), arXiv:1207.1266; provenance for the cap-witness refinements used by the source formalization.

80 thms6 active usersReviewed

Completed

Number Theory Pure Mathematics·Captain: alya

Multiplicative Number Theory I: Siegel–Walfisz and the Three Primes TheoremTextbook

Primes in progressions, uniformly in the modulus

Applying the circle method to an additive problem about primes requires counting primes in arithmetic progressions with an error term uniform in the modulus: the modulus is not fixed in advance, it grows with the size of the numbers being represented. The Siegel–Walfisz theorem is the classical statement of that uniformity, valid for every modulus up to a fixed power of $\log x$ , and it is the one analytic ingredient the standard proof of Vinogradov's three primes theorem cannot do without.

The history is a sequence of partial uniformities:

1837. Dirichlet proves that every progression $a \bmod q$ with $(a,q)=1$ contains infinitely many primes, for each fixed $q$ , with no rate (Dirichlet's theorem).
1896–1899. De la Vallée Poussin proves the prime number theorem with the error term $O(x e^{-c\sqrt{\log x}})$ , and extends the zero-free region from $\zeta$ to $L(s,\chi)$ , obtaining the prime number theorem in progressions for each fixed $q$ (PNT).
1918–1935. Landau and Page isolate the obstruction to uniformity: a single real zero near $s=1$ , attached to a quadratic character. Landau shows at most one of two distinct real primitive characters can have such a zero; Page shows at most one modulus below a given bound can, yielding unconditional uniformity for $q$ up to a bounded power of $\log x$ (Page's theorem).
1935. Siegel proves $L(1,\chi) \gg_\varepsilon q^{-\varepsilon}$ for real primitive $\chi$ , at the price of an ineffective constant (Siegel).
1936. Walfisz combines Siegel's bound with the de la Vallée Poussin machinery and obtains uniformity for every fixed power $q \le (\log x)^A$ (Walfisz).
1937. Vinogradov proves that every sufficiently large odd integer is a sum of three primes (Vinogradov's theorem).
2013. Helfgott removes the "sufficiently large", settling ternary Goldbach for all odd $n > 5$ (arXiv:1312.7748).

Setting

The von Mangoldt function $\Lambda(n)$ equals $\log p$ if $n = p^m$ is a prime power and $0$ otherwise. The Chebyshev function $\psi(x) = \sum_{n \le x} \Lambda(n)$ counts primes with weights; the prime number theorem is the assertion $\psi(x) \sim x$ .

A Dirichlet character modulo $q$ is a multiplicative function $\chi : \mathbb{Z}/q\mathbb{Z} \to \mathbb{C}$ , supported on the units and taking root-of-unity values there. The principal character $\chi = 1$ is the indicator of the units; a character is quadratic (real) if $\chi^2 = 1$ and $\chi \neq 1$ , and primitive if it is not induced by a character of a proper divisor of $q$ . The Dirichlet $L$ -function $L(s,\chi) = \sum_{n\ge 1}\chi(n)n^{-s}$ , defined for $\operatorname{Re} s > 1$ , extends meromorphically to $\mathbb{C}$ , entire except for a simple pole at $s = 1$ when $\chi$ is principal.

The two counting functions of the mission are the twisted von Mangoldt sum and the progression sum

\psi(N,\chi) = \sum_{n < N} \Lambda(n)\chi(n), \qquad \psi(N;q,a) = \sum_{\substack{n < N \\ n \equiv a\ (q)}} \Lambda(n),

related by finite character orthogonality. Write $\delta_\chi = 1$ for $\chi$ principal and $\delta_\chi = 0$ otherwise. A zero $\beta \in (0,1)$ of $L(s,\chi)$ lying inside the classical zero-free region is an exceptional zero (a Siegel zero); the set of such zeros for a given $\chi$ is the exceptional set $E$ , which the results below constrain to have at most one element.

Formalization targets

The attack path follows Davenport, Multiplicative Number Theory, 3rd ed., §§14, 18, 20, 21, 22.

(1) zero_free_region (§14, pp. 88–96). There is an absolute $c>0$ such that for every $q \ge 1$ and every $\chi \bmod q$ ,

L(s,\chi) \neq 0 \quad\text{for } s \neq 1,\ \operatorname{Re} s \ \ge\ 1 - \frac{c}{\log\big(q(|\operatorname{Im} s| + 2)\big)},

with at most one exception, which is real, lies in $(0,1)$ , is a simple zero, and can occur only for quadratic non-principal $\chi$ .

(2) pnt_dlvp (§18, pp. 111–114). For some $c > 0$ and all $x \ge 2$ ,

\psi(x) = x + O\!\left(x\,e^{-c\sqrt{\log x}}\right).

(3) psi_char_of_region (§20, pp. 121–125). For a region constant $c>0$ there are $c_1, c_2 > 0$ such that, whenever $E$ is an exceptional set for $\chi \bmod q$ with respect to $c$ and $q \le \exp(c_2\sqrt{\log N})$ ,

\psi(N,\chi) = \delta_\chi N - \sum_{\beta \in E} \frac{N^\beta}{\beta} + O\!\left(N e^{-c_1\sqrt{\log N}}\right).

(4) siegel (§21, pp. 126–131). For every $\varepsilon > 0$ there is $C(\varepsilon) > 0$ such that for every real primitive non-principal $\chi \bmod q$ ,

L(1,\chi) > C(\varepsilon)\, q^{-\varepsilon}.

(5) siegel_zero (§21, second form). For every $\varepsilon > 0$ there is $C(\varepsilon) > 0$ such that for every real primitive non-principal $\chi \bmod q$ ,

L(\sigma,\chi) \neq 0 \quad \text{for all real } \sigma > 1 - C(\varepsilon)q^{-\varepsilon}.

(6) siegelWalfisz (§22, pp. 132–134). For every $A > 0$ there are $C, c > 0$ such that for all $q \ge 1$ , all $\chi \bmod q$ , and all $N \ge 2$ with $q \le (\log N)^A$ ,

\big\lVert \psi(N,\chi) - \delta_\chi N \big\rVert \le C N e^{-c\sqrt{\log N}}.

This is literally the platform proposition ThreePrimes.SiegelWalfisz.

A corollary, not a milestone, records the progression form siegel_walfisz_ap: for $(a,q)=1$ and $q \le (\log N)^A$ ,

\psi(N;q,a) = \frac{N}{\varphi(q)} + O_A\!\left(N e^{-c\sqrt{\log N}}\right).

Goal (three_primes, §26). There is $N_0$ such that every odd $n \ge N_0$ is a sum of three primes. It follows from milestone (6) by the existing platform theorem deducing ThreePrimes.ThreePrimesExistence from ThreePrimes.SiegelWalfisz. The goal leaves $N_0$ unspecified rather than hard-coding a numeric threshold, so it is not invalidated by later improvements to that threshold.

What the result gives, and what remains to be formalized

Siegel–Walfisz is the standard uniform input downstream of which sit the circle method for ternary Goldbach, the Bombieri–Vinogradov theorem, and much of sieve theory. Without it, the three primes theorem's major-arc analysis has no main term.

Platform status is the reason this mission exists. A complete, machine-checked formalization of the three primes theorem already exists in the namespace ThreePrimes (by user tabbott), following Vaughan, The Hardy–Littlewood Method, Ch. 3, and Davenport §26. It is conditional: it takes Siegel–Walfisz as an explicit hypothesis ThreePrimes.SiegelWalfisz. Discharging that hypothesis makes the three primes theorem unconditional, and is the whole content of this mission.

Mathlib contains the analytic continuation of $L(s,\chi)$ (DirichletCharacter.LFunction), its functional equation, the non-vanishing of $L(s,\chi)$ on $\operatorname{Re} s \ge 1$ , Dirichlet's theorem, and the Chebyshev function. It does not contain the zero-free region for $L(s,\chi)$ , the explicit formula for $\psi(x,\chi)$ , Siegel's theorem, or Siegel–Walfisz. The platform additionally hosts the PNT+ project contour machinery for $\zeta$ — Borel–Carathéodory, the $3 + 4\cos\theta + \cos 2\theta$ inequality, a zero-free rectangle, and MediumPNT, $\psi(x) = x + O(x\exp(-c(\log x)^{1/10}))$ . That is a template for the $L(s,\chi)$ analogues, not a proof of them, and its error term is weaker than the de la Vallée Poussin form milestone (2) asks for.

Where the obvious argument fails

The first idea is to run the $\zeta$ argument character by character. It works for complex $\chi$ and breaks for real ones. The positivity device that pushes zeros off $\operatorname{Re} s = 1$ compares $\chi$ , $\chi^2$ and the trivial character at nearby points; when $\chi$ is quadratic, $\chi^2$ is principal and contributes the pole of $L(s,\chi_0)$ at $s = 1$ at exactly the height where the putative zero sits, so the inequality degrades from "no zeros" to "at most one zero" and stops there. Every later step inherits that unexcluded zero: milestone (3) can only be stated with the $N^\beta/\beta$ term present, and milestone (6) is exactly the assertion that for $q \le (\log N)^A$ this term is small — which Siegel's ineffective bound supplies and nothing effective is known to.

A second shortcut, deducing uniformity from Mathlib's non-vanishing of $L(s,\chi)$ on $\operatorname{Re} s \ge 1$ together with Dirichlet's theorem, also fails: those results are qualitative, carry no rate, and are not uniform in $q$ .

Formalization scope

Sums run over $n < N$ with $N \in \mathbb{N}$ , matching Vino.vmSumChar and ThreePrimes.SiegelWalfisz; Davenport sums over $n \le x$ . The two differ by the single term $\Lambda(N) \le \log N$ , negligible against every error term above. Milestone (2) alone uses a real argument, via Mathlib's Chebyshev.psi. $L(s,\chi)$ is Mathlib's DirichletCharacter.LFunction, so no continuation is reconstructed.

The zero-free region is Davenport.InRegion c q s, namely $\operatorname{Re} s \ge 1 - c/\log(q(|\operatorname{Im} s| + 2))$ ; the exceptional zero is packaged as IsExceptionalSet c χ E: $E$ is a subsingleton, every element is a real zero of $L(\cdot,\chi)$ in $(0,1)$ and can exist only for quadratic non-principal $\chi$ , and $L(s,\chi) \neq 0$ at every $s \neq 1$ of the region outside $E$ . Milestone (1) adds simplicity as $L'(\beta,\chi) \neq 0$ for $\beta \in E$ .

Milestone (3) takes the region constant $c > 0$ as a parameter rather than importing it from milestone (1), so the milestones can be attempted in any order. For large $c$ the hypothesis IsExceptionalSet c χ E may be unsatisfiable for some $\chi$ , making the statement vacuous there — a harmless weakening, not a falsehood, and not a trivializing reading: milestone (1) produces a definite small $c > 0$ with a witness $E$ for every $\chi$ , so instantiating milestone (3) at that $c$ discharges the hypothesis rather than voiding it.

Siegel's theorem is stated for χ.IsQuadratic, χ ≠ 1, χ.IsPrimitive characters, with the conclusion a lower bound on $\operatorname{Re} L(1,\chi)$ ; since $L(1,\chi)$ is real for real $\chi$ , this is the value itself, not a weakening. The constants in milestones (4), (5) and (6) are ineffective; the statements are plain existentials, so ineffectivity is invisible to Lean, but no numeric constant can be extracted from anything downstream of them.

The principal character is included in the character-form statements, with main term $N$ (if χ = 1 then (N : ℂ) else 0); milestones (3) and (6) therefore contain the prime number theorem itself and cannot be proved by restricting to non-principal $\chi$ . Milestone (6) requires $c > 0$ strictly, which is what makes $Ne^{-c\sqrt{\log N}}$ a genuine saving over the trivial $\psi(N,\chi) \ll N$ ; with $c = 0$ allowed it would be empty.

Beyond the six milestones, a complete development needs Hadamard factorization for $L(s,\chi)$ as an entire function of order $1$ , the zero-counting estimate $N(T,\chi)$ (§16, pp. 101–103), the truncated explicit formula for $\psi(x,\chi)$ (§19, pp. 115–120), Perron-type contour truncation, and the imprimitive-to-primitive reduction $|\psi(N,\chi) - \psi(N,\chi^{*})| \ll (\log q)(\log N)$ . All of it is reusable well beyond this mission, being the standard prerequisite for Bombieri–Vinogradov, Linnik's theorem, and effective Chebotarev. Contributions of these supporting results, of alternative routes to milestone (3) following Montgomery–Vaughan Ch. 11, of the $\pi(x;q,a)$ versions, and of sharper constants are welcome.

Selected references

H. Davenport, Multiplicative Number Theory, 3rd ed., revised by H. L. Montgomery, GTM 74, Springer, 2000. §§14, 18, 20, 21, 22, 26. doi:10.1007/978-1-4757-5927-3
H. L. Montgomery and R. C. Vaughan, Multiplicative Number Theory I: Classical Theory, Cambridge University Press, 2007. Ch. 11–12 (Theorems 11.3, 11.14, 11.16, 12.10; Corollaries 11.10, 11.12, 11.17, 11.19). doi:10.1017/CBO9780511618314
R. C. Vaughan, The Hardy–Littlewood Method, 2nd ed., Cambridge University Press, 1997. Ch. 3. doi:10.1017/CBO9780511470929
C. L. Siegel, Über die Classenzahl quadratischer Zahlkörper, Acta Arithmetica 1 (1935), 83–86. eudml:205054
A. Walfisz, Zur additiven Zahlentheorie II, Mathematische Zeitschrift 40 (1936), 592–607. doi:10.1007/BF01218882
I. M. Vinogradov, Representation of an odd number as a sum of three primes, Doklady Akad. Nauk SSSR 15 (1937), 291–294. Vinogradov's theorem
H. A. Helfgott, The ternary Goldbach conjecture is true, 2013. arXiv:1312.7748
Siegel–Walfisz theorem, Wikipedia. link
Page theorem, Encyclopedia of Mathematics. link
A. Kontorovich et al., PrimeNumberTheoremAnd (PNT+), Lean formalization project. github
Mathlib, Mathlib.NumberTheory.LSeries.DirichletContinuation. docs

75 thms6 active usersReviewed

Completed

Algebra Pure Mathematics·Captain: ShouqiaoWang

Symplectic Modules Free over an Abelian NilradicalResearch Paper

Motivation

Polynomial representations provide a concrete way to study modules over Lie algebras: the underlying vector space is a polynomial ring, while the Lie generators act by explicit multiplication, shift, and differential operators. Chen and Tan classify a family of modules over the symplectic Lie algebra $\mathfrak{sp}_{2\ell}(\mathbb C)$ that are free of rank one over the universal enveloping algebra of an abelian nilradical. Their paper determines the family, its isomorphism classes, its weight and simplicity criteria, its finite-length behavior at exceptional parameters, and an application to Hamiltonian Lie algebras. This mission packages those headline results into one common Lean target, corresponding to Theorems 1.1--1.3 of Chen--Tan.

The common-family formulation matters. The source does not assert three unrelated existence theorems: one explicit two-parameter family $\tau(C,\Phi)$ carries all of the classification, simplicity, finite-length, and Hamiltonian consequences. The Lean goal therefore quantifies that family once and requires all headline properties of the same witness.

Setting

Fix $\ell\ge2$ and the complex symplectic Lie algebra $\mathfrak{sp}_{2\ell}(\mathbb C)$ . The relevant maximal parabolic subalgebra has an abelian nilradical $\mathfrak n$ . Its enveloping algebra is a polynomial algebra in the root generators, represented formally by a multivariate polynomial ring. A rank-one free $U(\mathfrak n)$ -module can consequently be modeled on that polynomial ring.

The definition bundle presents the simple Chevalley generators and their action by explicit operators depending on a scalar $C\in\mathbb C$ and a polynomial parameter $\Phi$ . Rather than assuming that these formulas already form a representation, the target asks for a generator presentation satisfying the symplectic Lie relations and for a representation family $\tau(C,\Phi)$ realizing the formulas. It also formalizes module equivalence, weight spaces, simplicity, Noetherian and Artinian conditions, finite composition factors, and the Shen--Larsson construction for a Hamiltonian Lie algebra.

Formalization targets

Common polynomial-module family

Prove that for every $\ell\ge2$ there is one generator presentation and one family

(C,\Phi)\longmapsto \tau(C,\Phi)

of $\mathfrak{sp}_{2\ell}(\mathbb C)$ -representations on the polynomial ring, free of rank one over the abelian nilradical, satisfying the explicit generator formulas. Prove the source's classification and isomorphism criteria, including that $\tau(C,\Phi)$ is a weight module exactly when $\Phi$ is constant, and the stated simplicity criterion outside the exceptional arithmetic set

\left\{\frac{\ell+1}{2}-\frac{n}{2}:n\in\mathbb Z_{>0}\right\}.

For exceptional $C$ , prove the Noetherian/Artinian and finite-composition-series conclusions and the weight/nonweight classification of the composition factors. Finally, prove that the canonical Hamiltonian Shen--Larsson construction has the exact degree-weight spaces and the source's simplicity and weight-module consequences. All clauses must be witnessed by the same family $\tau$ .

Significance

The result gives a complete algebraic description of a large concrete class of non-highest-weight modules. It separates the generic simple regime from an exceptional finite-length regime and shows how nonweight symplectic modules generate weight modules over an infinite-dimensional Hamiltonian Lie algebra. The explicit formulas make the family suitable for calculation, while the classification prevents duplicate parameter choices from being mistaken for genuinely different modules.

Formalization adds checks that are easy to blur in prose. In particular, the generator formulas cannot be called a Lie representation until the defining relations have been verified, and the same witness must support every later theorem. A completed proof will contribute reusable Lean infrastructure for symplectic root data, polynomial representations, module-theoretic finiteness, exact weight-space descriptions, and Hamiltonian Lie-algebra functors. The paper's proofs are known; the open task is their machine-checked reconstruction.

Difficulty

The first obstacle is structural rather than computational. Checking formulas on individual generators is insufficient: all Chevalley and Serre relations must hold with the correct operator order and signs, after which the action must extend to the full Lie algebra. Classification then requires controlling arbitrary rank-one-free modules, not merely verifying that the displayed examples exist.

The exceptional parameters introduce a second layer. Generic simplicity and exceptional finite length are logically different claims, and the composition-factor statement must be tied to the same parameterized representation. The Hamiltonian application adds another algebra and a tensor construction; exact weight spaces and simplicity cannot be obtained by treating the functor as an opaque interface. The Lean goal deliberately keeps these obligations inside one theorem so that separate convenient witnesses cannot satisfy different portions.

Formalization scope

The mission works over $\mathbb C$ with natural rank $\ell\ge2$ . The definition bundle uses concrete multivariate polynomials, matrices and linear maps, a presented symplectic Lie algebra, Lie representations, submodules, and tensor products. The exceptional set is expressed with complex coercions, so no accidental natural-number division is involved. The nilradical action, freeness, parameter equivalence, weight-space equalities, simplicity, finite-length properties, and Hamiltonian brackets are transparent propositions in the bundle.

The final theorem is a single conjunction under one existentially quantified presentation and one existentially quantified family $\tau$ . Several convenient corollaries can be projected from it, but they are not independent targets and do not permit different witnesses. The bundle contains no custom axioms or opaque semantic assumptions, and the only admitted term is the main theorem's sorry. Contributions may split the proof into source-numbered lemmas about generator relations, classification, exceptional submodules, or the Shen--Larsson application, provided the shared-family quantifier structure is preserved.

Selected references

Yang Chen and Haijun Tan, Simple $\mathfrak{sp}_{2\ell}(\mathbb C)$ -modules which are free over an abelian nilradical, Journal of Algebra 697 (2026), 341--372, Theorems 1.1--1.3 (formal Theorems 3.7, 3.8, 4.7, 4.9, and 5.2). DOI
G. Shen, foundational work on mixed-product constructions for modules over Lie algebras of Cartan type, cited in the source paper for the Shen--Larsson functor.

28 thms6 active usersReviewed

Algebra Pure Mathematics·Captain: ShouqiaoWang

Arbitrary Torsion in Moment-Angle Homology and Loop HomologyResearch Paper

Motivation

Moment-angle complexes are central objects in toric topology. They convert the combinatorics of a simplicial complex into a topological space assembled from disks and circles, allowing face structure to influence homotopy and homology. When the simplicial complex triangulates a sphere, the resulting space is a moment-angle manifold. Torsion in the integral homology of these manifolds is difficult to realize in low simplicial dimension, and torsion in the homology of their based loop spaces is even more constrained. Yang Han and Keke Li's Theorem 1.7 asserts that dimension four is already universal: every finitely generated abelian group can occur as a subgroup of both homology theories for one and the same simplicial $4$ -sphere.

This mission formalizes that headline existence statement. It is not restricted to a chosen finite list of groups or primes, and it requires a common simplicial sphere rather than permitting separate witnesses for ordinary and loop homology.

Setting

Let $L$ be an abstract simplicial complex on a finite vertex set $[m]$ . Its geometric realization $|L|$ is formed from probability vectors whose supports are faces of $L$ . The condition that $L$ is a simplicial $4$ -sphere means that this realization is homeomorphic to the unit sphere $S^4\subset\mathbb R^5$ .

For each face $\sigma\in L$ , assign a copy of the closed disk $D^2$ at vertices in $\sigma$ and the boundary circle $S^1$ at vertices outside $\sigma$ . The associated moment-angle complex is

\mathcal Z_L =\bigcup_{\sigma\in L} \prod_{i=1}^{m}Y_i(\sigma), \qquad Y_i(\sigma)= \begin{cases} D^2,&i\in\sigma,\\ S^1,&i\notin\sigma. \end{cases}

The all-ones point is a canonical basepoint. Write $\Omega\mathcal Z_L$ for the based loop space with the compact-open topology. For a space $X$ , the mission uses total integral singular homology

H_*(X;\mathbb Z)=\bigoplus_{q\ge0}H_q(X;\mathbb Z)

as an additive abelian group. Saying that an abelian group $G$ is a subgroup means that there is an injective additive homomorphism $G\hookrightarrow H_*(X;\mathbb Z)$ .

Formalization targets

Arbitrary torsion in one moment-angle manifold

For every finitely generated abelian group $G$ , prove that there are an integer $m$ and a simplicial complex $L$ on Fin m such that $|L|\cong S^4$ and there are injective homomorphisms

G\hookrightarrow H_*(\mathcal Z_L;\mathbb Z), \qquad G\hookrightarrow H_*(\Omega\mathcal Z_L;\mathbb Z).

The quantifier order matters: the same $m$ and the same $L$ must support both embeddings. The target concerns additive subgroups of total graded homology; it does not require the two embeddings to land in the same degree or to preserve multiplicative structures.

Significance

The theorem gives a universality statement for moment-angle manifolds over simplicial $4$ -spheres. It says that no classification by a bounded list of torsion primes or exponents can describe all such homology and loop-homology groups. Requiring both embeddings for a single $L$ connects the ordinary topology of the manifold to its based-loop topology rather than proving two unrelated existence results.

Formalizing the theorem requires reusable foundations in several areas: finite abstract simplicial complexes, geometric realization, polyhedral products, based loop spaces, integral singular homology, graded direct sums, and additive embeddings. The published article presents a human proof; this mission records its intended main theorem as an open Lean target. The definitions do not assume the existence of the required sphere or embeddings, so a solver must supply the mathematical construction and all homological consequences.

Difficulty

The assertion ranges over arbitrary finitely generated abelian groups, including free parts and prime-power torsion of unbounded exponent. A finite check of selected groups cannot establish the target. The same finite simplicial object must simultaneously control two different homology theories, one of which is applied to an infinite-dimensional function space. Standard library support is strongest for singular homology as a functor, while concrete calculations for moment-angle spaces and loop spaces require additional bridges.

There is also a substantial representation boundary between combinatorics and topology. The face data of $L$ , the union of disk-circle products, the homeomorphism $|L|\cong S^4$ , and the induced maps on homology must all refer to compatible spaces and basepoints. A formal solution cannot replace “simplicial sphere” by a mere Boolean flag or replace homology by an arbitrary group-valued field.

Formalization scope

Lean represents $L$ using AbstractSimplicialComplex (Fin m). Because Mathlib's structure includes singleton faces automatically, the auxiliary face predicate explicitly restores the conventional empty face where the moment-angle union needs it. The geometric realization is the standard support-restricted probability simplex, and the sphere condition is an actual homeomorphism to the Euclidean unit $4$ -sphere.

The moment-angle space is a subtype of (Fin m → ℂ) defined by the literal disk/circle coordinate condition. The loop space consists of based continuous paths with matching endpoints and carries the compact-open topology inherited from Mathlib's path construction. Homology is singularHomologyFunctor with coefficients in $\mathbb Z$ , and total homology is a direct sum over all natural degrees.

The statement permits the two embeddings to occupy different degrees and makes no ring-embedding claim; these choices match the source phrase “contain $G$ as a subgroup.” It rules out vacuity by requiring an actual simplicial complex, an actual sphere homeomorphism, and injective additive maps. Contributions that isolate degree-specific refinements, compute homology of standard polyhedral products, or formalize reusable loop-space equivalences are welcome, provided they reconnect to the stated root theorem.

Selected references

Yang Han and Keke Li, Moment Angle Manifolds Corresponding to $S^4$ Whose Homology and Loop Homology May Have Arbitrary Torsion, International Mathematics Research Notices 2026(4), 1--7, 2026. DOI
A. Bahri, M. Bendersky, F. R. Cohen, and S. Gitler, The polyhedral product functor: a method of decomposition for moment-angle complexes, arrangements and related spaces, Advances in Mathematics 225(3), 2010, 1634--1668. DOI

17 thms6 active usersReviewed

Completed

Markov Chain Probability Stochastic Systems·Captain: Shuze Chen

Markov Chains and Mixing Times XI: The Cutoff Phenomenon and Lamplighter WalksTextbook

Motivation

For many natural chains, convergence to stationarity is not gradual: the distance stays near its maximum for a long time and then collapses to zero in a comparatively negligible window. A deck of cards under riffle shuffles is "not at all mixed" for six shuffles and "essentially mixed" after eight. This abrupt transition is the cutoff phenomenon, discovered by Aldous and Diaconis in the 1980s, and Chapter 18 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) develops its theory: precise definitions of cutoff and cutoff windows, the product criterion $t_{\mathrm{rel}}=o(t_{\mathrm{mix}})$ necessary for cutoff, and complete proofs for two model families — the biased walk on a segment and the lazy hypercube walk, the latter with the sharp $\tfrac12 n\log n$ location and window $n$ , in both total variation and separation. Chapter 19 complements this with lamplighter walks: chains on the wreath-product state space of lamp configurations over a moving lamplighter, whose relaxation, mixing, and separation times are governed — beautifully — by the hitting and cover times of Missions VI. Both chapters are formalized in this mission.

Setting

A family of chains is a sequence $P^{(n)}$ on state spaces $V_n$ with stationary distributions $\pi_n$ ; all single-chain quantities acquire an index $n$ . As before, $\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|$ , $d_n(t)=\max_x\|P^{(n)t}(x,\cdot)-\pi_n\|_{TV}$ , $t^{(n)}_{\mathrm{mix}}(\varepsilon)=\min\{t:d_n(t)\le\varepsilon\}$ , and $t^{(n)}_{\mathrm{mix}}=t^{(n)}_{\mathrm{mix}}(1/4)$ . The family has a cutoff when for every $0<\varepsilon<1$

\frac{t^{(n)}_{\mathrm{mix}}(\varepsilon)}{t^{(n)}_{\mathrm{mix}}(1-\varepsilon)}\;\longrightarrow\;1\qquad(n\to\infty),

and a cutoff at $t_n$ with window $w_n$ when $w_n=o(t_n)$ and the distance at time $t_n+\alpha w_n$ tends (in the appropriate limsup/liminf sense) to $1$ as $\alpha\to-\infty$ and to $0$ as $\alpha\to+\infty$ . The separation distance from $x$ is $s_x(t)=\max_y\bigl(1-P^t(x,y)/\pi(y)\bigr)$ (Mission III), $s(t)=\max_xs_x(t)$ , and a separation cutoff is defined by the same window template with $s$ in place of $d$ . From Mission VII, $t_{\mathrm{rel}}=(1-\lambda_\star)^{-1}$ is the relaxation time; from Mission VI, $t_{\mathrm{hit}}=\max_{x,y}\mathbb E_x(\tau_y)$ and $t_{\mathrm{cov}}$ are the maximal hitting and cover times, and the pairwise distance $\bar d(t)=\max_{x,y}\|P^t(x,\cdot)-P^t(y,\cdot)\|_{TV}$ is from Mission II.

The concrete chains: the lazy biased walk on $\{0,\dots,n\}$ holds with probability $\tfrac12$ and otherwise steps up with probability $p>\tfrac12$ , down with probability $1-p$ (reflecting at the endpoints); the lazy hypercube walk is the walk of Mission IV on $\{0,1\}^n$ . The lamplighter chain $G^\ast$ over a graph $G$ has states (lamp configuration in $\{0,1\}^{V}$ , lamplighter position in $V$ ); one step randomizes the current lamp, moves the lamplighter one step of the lazy walk on $G$ , and randomizes the new lamp. Its stationary distribution is uniform lamps times the walk's stationary distribution.

Formalization targets

Goal

Theorem 18.3: the lazy hypercube walk has a cutoff at $\tfrac12\,n\log n$ with window $n$ — the family's total variation distance undergoes its full collapse in a window of size $\Theta(n)$ around $\tfrac12 n\log n$ .

Milestones

Lemma 18.1 — cutoff is equivalent to the step-function limit: $d_n(\lfloor c\,t^{(n)}_{\mathrm{mix}}\rfloor)\to1$ for every $c<1$ and $\to0$ for every $c>1$ .
Theorem 18.2 — the lazy biased walk on $\{0,\dots,n\}$ with bias $\beta=p-\tfrac12>0$ has a cutoff at $\beta^{-1}n$ with window $\sqrt n$ .
Proposition 18.4 (the product condition) — for a reversible family with $t^{(n)}_{\mathrm{mix}}\to\infty$ , if $t^{(n)}_{\mathrm{mix}}\le C\,t^{(n)}_{\mathrm{rel}}$ for a fixed constant $C$ , the family has no cutoff: $t_{\mathrm{rel}}=o(t_{\mathrm{mix}})$ is necessary.
Theorem 18.8 — the lazy hypercube walk has a separation cutoff at $n\log n$ with window $n$ — at twice the total-variation cutoff time.
Lemma 19.3 (Aldous–Diaconis) — the separation–total-variation relation $s(2t)\le1-\bigl(1-\bar d(t)\bigr)^2$ for reversible chains.
Theorem 19.1 — for lamplighter chains over a growing family of connected graphs, $t_{\mathrm{rel}}(G_n^\ast)\asymp t_{\mathrm{hit}}(G_n)$ : the relaxation time is comparable, with universal constants, to the maximal hitting time of the base walk.
Theorem 19.2 — likewise $t_{\mathrm{mix}}(G_n^\ast)\asymp t_{\mathrm{cov}}(G_n)$ : the lamplighter's mixing time is governed by the base walk's cover time.

Significance

The results. Cutoff is the deepest phenomenon in the quantitative theory of Markov chains: it says mixing is a phase transition in time. The hypercube is the fundamental example where everything can be computed — the eigenvalue structure of Mission VII delivers the upper bound and a refined distinguishing-statistic argument (Mission IV) the lower — and the $\tfrac12 n\log n$ location with window $n$ is the sharpest statement of the coupon-collector heuristic. The product condition 18.4 is the basic sanity criterion in the ongoing research program of characterizing cutoff. The lamplighter theorems tie together the entire series: hitting times (Mission VI), cover times (Mission VI), relaxation times (Mission VII), and separation (Missions III, XI) all meet in one family of chains that furnishes counterexamples — for instance, families with total-variation cutoff but no separation cutoff.

Formalizing them. Nothing about cutoff exists in any proof assistant. The definitions themselves (families of chains, windows, limsup/liminf in a real parameter) are a formalization contribution: they force precision about quantifier order that informal texts elide. The hypercube cutoff is a landmark target — a sharp two-sided asymptotic statement, not an inequality.

Difficulty

The upper half of the hypercube cutoff needs the full eigenvalue decomposition of the walk ( $\lambda_j=1-j/n$ with multiplicity $\binom nj$ , via Mission VII's spectral representation) and the $\ell^2$ bound summed over binomial coefficients; the lower half needs the Hamming-weight distinguishing statistic pushed to second-order precision (mean and variance at time $\tfrac12 n\log n+\alpha n$ ). Proposition 18.4 converts an eigenfunction with eigenvalue near $1$ into a quantitative anti-concentration statement — the formal content of "a bounded ratio forbids abrupt collapse". Theorem 18.2 rests on a central-limit-flavoured estimate for the biased walk's position, done with fourth-moment bounds rather than the CLT. The lamplighter theorems are the heaviest: the upper bounds couple lamp refreshment with the cover-time of the base walk, the lower bounds run separation-distance and eigenfunction arguments, and all four inequalities must hold with universal constants over an arbitrary growing graph family — the statements quantify over the family, so the proofs must too. The asymptotic language throughout (liminf/limsup over $n$ , limits in the window parameter $\alpha$ ) exercises the filter library in earnest.

Formalization scope

Families are dependent functions ∀ n, Matrix (V n) (V n) ℝ over a sequence of finite state-space types. Cutoff and windows are rendered exactly by the book's Eq. (18.3) and §18.1: the window definition uses Filter.liminf/limsup over $n$ composed with limits in the real parameter $\alpha$ (through ⌊t n + α w n⌋₊, with the natural-floor convention on negative reals). The mixing-time ratio in the cutoff definition uses real division of the natural-valued mixing times (total division: the hypotheses keep denominators eventually positive). The biased walk's stationary distribution is passed as a hypothesis rather than a closed form. In the lamplighter theorems the comparability constants $c_1,c_2$ and the threshold $N$ are existentially quantified, with the graph family and its connectivity as hypotheses; the lamplighter matrix and its product stationary distribution are explicit definitions. Lemma 19.3 is stated for a single reversible chain at all times $t$ .

Selected references

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
D. Aldous, P. Diaconis, Shuffling cards and stopping times, Amer. Math. Monthly 93 (1986). https://doi.org/10.1080/00029890.1986.11971821
P. Diaconis, The cutoff phenomenon in finite Markov chains, Proc. Natl. Acad. Sci. USA 93 (1996). https://doi.org/10.1073/pnas.93.4.1659
Y. Peres, D. Revelle, Mixing times for random walks on finite lamplighter groups, Electron. J. Probab. 9 (2004). https://doi.org/10.1214/EJP.v9-198

18 thms6 active usersReviewed

Completed

Markov Chain Probability Stochastic Systems·Captain: Shuze Chen

Markov Chains and Mixing Times X: Martingales and Evolving SetsTextbook

Motivation

Every mixing bound in Missions II–IX ultimately leaned on either coupling or the spectrum, and the spectral route demanded reversibility. Chapter 17 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) opens a third route: martingales — processes whose conditional expected increment vanishes — and the beautiful evolving-set process of Morris and Peres built from them. The payoff theorem of the chapter bounds the mixing time of any lazy irreducible chain by its bottleneck constant, with no reversibility hypothesis anywhere — an honest strengthening of the spectral route through the Cheeger inequality, whose proof is a martingale analysis of a random sequence of sets growing and shrinking under the chain's flow. The same chapter proves the optional stopping theorem in the exact discrete form the rest of the series consumes, and applies the machinery to sharp return-probability estimates for lazy walks.

Setting

Throughout, $P$ is a chain on a finite state space $V$ with stationary distribution $\pi$ ; $\|\mu-\nu\|_{TV}=\max_{A}|\mu(A)-\nu(A)|$ , $d(t)=\max_x\|P^t(x,\cdot)-\pi\|_{TV}$ , and $t_{\mathrm{mix}}(\varepsilon)=\min\{t:d(t)\le\varepsilon\}$ as in the earlier missions; $\pi_{\min}=\min_x\pi(x)$ . The chain is lazy when $P(x,x)\ge\tfrac12$ at every state.

A martingale adapted to the chain is a family $M_t$ of functions of the trajectory up to time $t$ such that the conditional expectation of $M_{t+1}$ , given the trajectory so far, equals $M_t$ — for a finite chain, a pointwise finite-sum identity. A stopping time $\tau$ is a $\{0,1\}$ -valued stopping rule in the sense of Mission III: whether to stop at time $t$ depends only on the trajectory up to $t$ .

From Mission IV: the edge measure is $Q(x,y)=\pi(x)P(x,y)$ , with $Q(S,y)=\sum_{x\in S}Q(x,y)$ , and the bottleneck constant $\Phi_\star$ is the minimum over sets $S$ with $0<\pi(S)\le\tfrac12$ of $\Phi(S)=Q(S,S^c)/\pi(S)$ . The evolving-set process is the Markov chain on subsets of $V$ in which, from the current set $S$ , one draws $u$ uniform on $(0,1]$ and passes to the superlevel set

S'=\Bigl\{y\;:\;\frac{Q(S,y)}{\pi(y)}\ge u\Bigr\}

— states currently receiving a large share of the flow out of $S$ are likely to join, states receiving little are likely to leave.

Formalization targets

Goal

Theorem 17.10 (Morris–Peres), the capstone of Chapter 17: for any lazy irreducible chain — reversibility not assumed —

t_{\mathrm{mix}}(\varepsilon)\;\le\;\frac{2}{\Phi_\star^{2}}\,\log\!\Bigl(\frac{1}{\varepsilon\,\pi_{\min}}\Bigr).

Milestones

Corollary 17.7, the Optional Stopping Theorem — if $M$ is a martingale adapted to the chain, bounded uniformly by a constant, and $\tau$ is an almost surely finite stopping time, then $\mathbb E_x(M_\tau)=M_0(x)$ : stopping a fair game at a fair time wins nothing.
Lemma 17.12 — the evolving-set process, started from the singleton $\{x\}$ , recovers the chain: $P^t(x,y)=\dfrac{\pi(y)}{\pi(x)}\,\mathbb P_{\{x\}}\{y\in S_t\}$ .
Lemma 17.13 — for the evolving-set process, the stationary mass $\pi(S_t)$ of the current set is a martingale.
Theorem 17.17 — return probabilities of the lazy random walk on a graph of maximum degree $\Delta$ : $\bigl|P^t(x,x)-\pi(x)\bigr|\le\sqrt2\,\Delta^{5/2}/\sqrt t$ , an application of the evolving-set machinery.

Significance

The results. The optional stopping theorem is the workhorse identity of discrete probability — the earlier missions' gambler's-ruin and hitting-time computations are all instances, and Missions XI–XII cite it again. The Morris–Peres theorem is the strongest known elementary relation between geometry and mixing: for reversible chains it recovers the Cheeger-based bound $t_{\mathrm{mix}}\lesssim\Phi_\star^{-2}\log(1/\pi_{\min})$ of Mission VII, but it needs no reversibility, and its proof technique — controlling the root $\sqrt{\pi(S_t)}$ as a supermartingale — introduced evolving sets as a tool that has since produced heat-kernel decay, isoperimetric mixing profiles, and bounds for non-reversible and time-inhomogeneous chains well beyond the book.

Formalizing them. Mathlib's martingale library lives in measure-theoretic generality; this mission's chain-adapted martingales are self-contained finite objects (families of functions on trajectory spaces), so the optional stopping theorem here is independent of, and complementary to, the measure-theoretic one. Evolving sets exist in no proof assistant; the process is a genuinely novel formalization target — a Markov chain whose states are Finsets, defined through interval lengths of a uniform variable.

Difficulty

The optional stopping theorem needs the dominated-convergence step (bounded martingale, a.s. finite time) rendered as an elementary tail estimate — the series $\sum_t\mathbb P\{\tau=t\}\,M_t$ must be shown summable and equal to $M_0$ by an exchange of finite sums with a limit. The evolving-set transition probabilities are interval lengths: the probability of passing from $S$ to $T$ is the length of the set of $u\in(0,1]$ whose superlevel set is exactly $T$ , which the formalization encodes by explicit upper and lower thresholds (a min over $T$ and a max over $T^c$ of the clipped ratios $Q(S,y)/\pi(y)$ ); establishing that these lengths sum to one over $T$ , and that the process has the two martingale properties, is delicate finite-order-statistics reasoning. The goal theorem then runs a supermartingale argument on $\sqrt{\pi(S_t)}$ : laziness keeps the thresholds in $[\tfrac12,1]$ , an expansion estimate converts the bottleneck constant into a per-step multiplicative decay of $\mathbb E\sqrt{\pi(S_t)\bigl(1-\pi(S_t)\bigr)}$ , and Lemma 17.12 converts that decay into a total-variation bound. Theorem 17.17 composes the same machinery with a Cauchy–Schwarz step. None of this exists in any library; the auxiliary supermartingale lemmas are welcome as separate contributions.

Formalization scope

Martingales, stopping times, and stopped expectations are the trajectory-calculus objects of Missions I and III: finite sums over paths weighted by $\prod P(\omega_i,\omega_{i+1})$ , with expectations over the stopping time as tsums in $t$ (non-summable families sum to $0$ ; the a.s.-finiteness hypothesis is the statement that the stopping mass sums to $1$ ). The evolving-set matrix is defined by the clipped-threshold formula described above — an explicit real matrix on Finset V — and the goal and lemmas assume $\pi$ positive and $P$ lazy exactly where the book does. Theorem 17.17 is stated for the lazy walk on a connected graph with positive degrees, with $\pi(x)=\deg(x)/2|E|$ written out. Real-valued bounds on the natural-valued $t_{\mathrm{mix}}$ are direct inequalities on the cast, with no hidden rounding.

Selected references

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
B. Morris, Y. Peres, Evolving sets, mixing and heat kernel bounds, Probab. Theory Related Fields 133 (2005). https://doi.org/10.1007/s00440-005-0434-7
D. Williams, Probability with Martingales, Cambridge University Press, 1991. https://doi.org/10.1017/CBO9780511813658

12 thms6 active usersReviewed

Completed

Markov Chain Probability Stochastic Systems·Captain: Shuze Chen

Markov Chains and Mixing Times IX: The Ising ModelTextbook

Motivation

The Ising model is statistical mechanics' fruit fly: spins $\pm1$ on the vertices of a graph, neighbours preferring to agree, a single parameter — the inverse temperature $\beta$ — tuning the strength of that preference. Chapter 15 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) studies the Glauber dynamics for this model and exhibits, on concrete graphs, the phenomenon that made mixing times a subject: a dynamical phase transition. At high temperature (small $\beta$ ) the dynamics mixes in $O(n\log n)$ steps on any bounded-degree graph; on the complete graph the same dynamics passes, as $\beta$ crosses an explicit threshold, from $O(n\log n)$ mixing to exponentially slow mixing. The chapter also introduces two comparison tools of independent value — the sensitivity of the spectral gap to edge removal, and the block dynamics comparison — and the Kenyon–Mossel–Peres bound for trees, all formalized in this mission.

Setting

Spin configurations on a finite graph $G$ with vertex set of size $n$ and maximum degree $\Delta$ are functions $\sigma$ assigning $\pm1$ to each vertex (encoded over Booleans, $\mathrm{true}\mapsto+1$ ). The Ising model at inverse temperature $\beta>0$ is the Gibbs distribution

\pi(\sigma)\;=\;\frac{e^{\,\beta\sum_{\{v,w\}\in E}\sigma(v)\sigma(w)}}{Z(\beta)},

each edge counted once, $Z(\beta)$ the normalizing partition function. The Glauber dynamics for $\pi$ picks a uniform vertex and re-samples its spin from $\pi$ conditioned on all other spins — concretely, the new spin at $v$ is $+1$ with probability $\bigl(1+\tanh(\beta S)\bigr)/2$ where $S$ is the sum of the neighbouring spins.

The yardsticks are as in the earlier missions: $\|\mu-\nu\|_{TV}=\max_A|\mu(A)-\nu(A)|$ is the total variation distance, $d(t)=\max_\sigma\|P^t(\sigma,\cdot)-\pi\|_{TV}$ , and $t_{\mathrm{mix}}(\varepsilon)=\min\{t:d(t)\le\varepsilon\}$ . From Mission VII: an eigenvalue of a chain is a real $\lambda$ with $Pf=\lambda f$ for some nonzero $f$ ; $\lambda_2$ is the largest eigenvalue $\ne1$ , the spectral gap is $\gamma=1-\lambda_2$ , $\lambda_\star$ the largest $|\lambda|$ over eigenvalues $\ne1$ , and the relaxation time is $t_{\mathrm{rel}}=(1-\lambda_\star)^{-1}$ .

Formalization targets

Goal

Theorem 15.1, the high-temperature fast-mixing theorem: if $\Delta\tanh\beta<1$ then the Glauber dynamics on any graph satisfies

t_{\mathrm{mix}}(\varepsilon)\;\le\;\Bigl\lceil\frac{n\,\bigl(\log n+\log(1/\varepsilon)\bigr)}{1-\Delta\tanh\beta}\Bigr\rceil,

together with its refinement for graphs with all degrees even, where the condition relaxes to $(\Delta/2)\tanh(2\beta)<1$ .

Milestones

Lemma 15.2 (the tanh lemma) — the elementary inequalities about $x\mapsto\tanh(\beta(x+1))-\tanh(\beta(x-1))$ (symmetry, monotonicity, the bounds by $2\tanh\beta$ and, at odd integers, by $\tanh 2\beta$ ) that drive the one-site coupling contraction.
Theorem 15.3 — the dynamical phase transition on the complete graph at $\beta=\alpha/n$ : (i) for $\alpha<1$ , $t_{\mathrm{mix}}(\varepsilon)\le n(\log n+\log(1/\varepsilon))/(1-\alpha)$ ; (ii) for $\alpha>1$ , there are $r(\alpha),C>0$ with $t_{\mathrm{mix}}\ge C\,e^{r n}$ — split here into a fast half and a slow half.
Theorem 15.4 — on the $n$ -cycle, at every $\beta>0$ , mixing is $n\log n$ up to explicit constants: $(1+o(1))\,\frac{n\log n}{2c_O(\beta)}\le t_{\mathrm{mix}}(\varepsilon)\le(1+o(1))\,\frac{n\log n}{c_O(\beta)}$ with $c_O(\beta)=1-\tanh(2\beta)$ .
Theorem 15.6 (Kenyon–Mossel–Peres) — on the rooted $b$ -ary tree of depth $k$ with $n_k$ vertices, the relaxation time is polynomial at every temperature: $t_{\mathrm{rel}}\le n_k^{\,c_T(\beta,b)}$ with $c_T(\beta,b)=2\beta(3b+1)/\log b+1$ .
Proposition 15.7 — removing $r$ edges changes the spectral gap of the Glauber dynamics by at most a factor $e^{2\beta(\Delta+2r)}$ .
Theorem 15.9 — the block-dynamics comparison: if blocks $V_1,\dots,V_b$ cover the vertex set, each of size at most $M$ , each vertex in at most $M_\star$ blocks, then the spectral gap $\gamma_B$ of the block dynamics and the gap $\gamma$ of the single-site dynamics satisfy $\gamma_B\le M^2M_\star\,(4e^{2\beta\Delta})^{M+1}\,\gamma$ .

Significance

The results. Theorem 15.1 is the standard fast-mixing criterion for Glauber dynamics, and the model application of the path-coupling technique of Mission VIII. Theorem 15.3 exhibits, in the cleanest possible setting, the correspondence between the static phase transition of the mean-field Ising model and the dynamical transition of its Glauber dynamics — the phenomenon at the heart of Markov-chain approaches to statistical physics. The tree bound of Kenyon–Mossel–Peres and the block-dynamics comparison are the standard tools for spatially structured spin systems; block dynamics in particular is the engine of recursive gap bounds on trees and lattices.

Formalizing them. Nothing about the Ising model, Gibbs distributions, or Glauber dynamics exists in Mathlib. The Gibbs-distribution layer (weights, partition functions, conditional single-site laws with their $\tanh$ closed forms) is foundational for any future formalization of statistical mechanics; the phase-transition theorem 15.3(ii) would be, to our knowledge, the first formalized instance of exponentially slow mixing driven by an energy barrier.

Difficulty

The high-temperature theorem is path coupling (Mission VIII) plus the tanh lemma: the one-site coupling of two adjacent configurations contracts the Hamming metric at rate $1-\bigl(1-\Delta\tanh\beta\bigr)/n$ , and every analytic input is in Lemma 15.2 — which is why that elementary lemma is a milestone of its own. The slow-mixing half of Theorem 15.3 runs through the bottleneck bound of Mission IV: the magnetization performs a one-dimensional walk in a double-well free-energy landscape, and the bottleneck at zero magnetization has exponentially small stationary mass — a large-deviations estimate carried out with binomial coefficients. The cycle's lower bound needs Wilson's method (Mission VII) with an explicit eigenfunction. The tree and block theorems are exercises in the comparison technology of Mission VII (Dirichlet forms, canonical paths through block updates); their constants are crude but the inductive structure is delicate. Everything sits on the subtlety that the state space $\{\pm1\}^V$ has size $2^n$ , so all "polynomial" bounds are polynomial in $n$ , not in the size of the state space.

Formalization scope

The Gibbs distribution is defined by explicit finite sums (weight over partition function, total division); no positivity side conditions are needed since the weights are exponentials. The Glauber dynamics is the generic single-site heat bath of Mission II applied to the Ising distribution, so the $\tanh$ closed form is a provable lemma, not a definition. Asymptotic statements ( $o(1)$ , "for sufficiently large $n$ ") are rendered with explicit $\exists N,\forall n\ge N$ quantifiers and a free precision parameter $\delta$ ; the phase-transition constants $r(\alpha),C$ are existentially quantified. The tree is encoded as words of length $\le k$ over an alphabet of size $b$ ; the block dynamics re-samples a uniformly chosen block from the conditional Gibbs distribution, with the convention that a conditioning of zero mass yields a zero row (total division), which the theorems' hypotheses exclude on the support. The even-degree refinement of the goal is stated as a second conjunct with its own hypothesis.

Selected references

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
C. Kenyon, E. Mossel, Y. Peres, Glauber dynamics on trees and hyperbolic graphs, FOCS 2001. https://doi.org/10.1109/SFCS.2001.959934
D. A. Levin, M. J. Luczak, Y. Peres, Glauber dynamics for the mean-field Ising model: cut-off, critical power law, and metastability, Probab. Theory Related Fields 146 (2010). https://doi.org/10.1007/s00440-008-0189-z
F. Martinelli, Lectures on Glauber dynamics for discrete spin models, Lectures on Probability Theory and Statistics (Saint-Flour XXVII), Springer, 1999. https://doi.org/10.1007/978-3-540-48115-7_2

17 thms6 active usersReviewed

Completed

Markov Chain Probability Stochastic Systems·Captain: Shuze Chen

Markov Chains and Mixing Times V: Shuffling CardsTextbook

Motivation

How many shuffles does a deck of cards need? The question created the modern theory of mixing times: Diaconis and Shahshahani's analysis of random transpositions (1981) and the Bayer–Diaconis "seven shuffles suffice" analysis of the riffle shuffle (1992) are its founding results. Chapters 8 and 16 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009) treat the four standard shuffles: random transpositions (pick two cards, swap them), the riffle shuffle (cut and interleave, the Gilbert–Shannon–Reeds model), random adjacent transpositions, and the $L$ -reversal chain of segment reversals — the last motivated by genome rearrangement, where a chromosome evolves by reversing segments and the mixing time measures evolutionary distance ("from shuffling cards to shuffling genes").

Setting

All four chains are random walks on a symmetric group; decks are encoded as in Mission III, an arrangement being a permutation with position $0$ on top. Random transpositions have increment distribution $\mu(\mathrm{id})=1/n$ , $\mu(\text{transposition})=2/n^2$ . The lazy adjacent-transposition walk puts mass $1/2$ on the identity and $1/[2(n-1)]$ on each $(i\ i{+}1)$ . One inverse riffle shuffle assigns each card an independent uniform bit and moves the cards labeled $0$ to the top, preserving relative order; the (forward) riffle shuffle is its time reversal, given by transposing the inverse-shuffle matrix (the stationary distribution being uniform). The $L$ -reversal chain on circular arrangements indexed by $\mathbb Z_n$ picks a position $i$ and a length $k<L$ uniformly and reverses the segment $[i,i+k]$ .

Formalization targets

Goal

t_{\mathrm{mix}}\;\le\;(2+o(1))\,n\log n

for random transpositions on $n$ cards (Corollary 8.10), formalized as: for every $\delta>0$ there is $N$ with $t_{\mathrm{mix}}\le(2+\delta)n\log n$ for all $n\ge N$ .

Milestones

Proposition 8.11 (random transpositions lower bound $t_{\mathrm{mix}}(\varepsilon)\ge\frac{n-1}{2}\log\bigl(\frac{(1-\varepsilon)n}{6}\bigr)$ , via fixed points); Proposition 8.13 (riffle shuffle: $t_{\mathrm{mix}}\le 2\log_2(4n/3)+1$ ); Proposition 8.14 (riffle shuffle: $t_{\mathrm{mix}}(\varepsilon)\ge(1-\delta)\log_2 n$ for large $n$ , by the counting bound of Mission IV); the random adjacent transpositions upper bound $t_{\mathrm{mix}}(\varepsilon)\le 2n^3\log_2 n$ for large $n$ (§16.1.2, display (16.4)) and lower bound $t_{\mathrm{mix}}\ge n^2(n-1)/16$ (§16.1.3, by following a single card); and Proposition 16.2 (the $L$ -reversal chain with $L<n/2$ satisfies $d\bigl((1-\varepsilon)\frac n2\log n\bigr)\to1$ , via conserved adjacencies).

Significance

The results. Random transpositions at $\frac12 n \log n$ (the constant $2$ here is not sharp; the sharp constant is part of the celebrated Diaconis–Shahshahani cutoff) and riffle at $\frac32\log_2 n$ are the emblematic mixing results outside of spin systems; the riffle bound is the mathematical content of "seven shuffles suffice" for $n=52$ . The adjacent-transposition walk at order $n^3\log n$ is the basic example where geometry (diameter $\binom n2$ ) forces polynomial mixing. The $L$ -reversal lower bound is the quantitative starting point of the biological application.

Formalizing them. Random walks on symmetric groups and their mixing are entirely absent from Mathlib; so are the combinatorial devices these proofs run on — the Broder stopping time, rising sequences and the Eulerian-number analysis of riffle shuffles, single-card projections, conserved adjacencies. The riffle shuffle formalization via bit strings and the stable-sort permutation Tuple.sort gives a clean combinatorial model reusable for the cutoff analysis of Mission XI.

Difficulty

Corollary 8.10's route is the Broder strong stationary time: mark cards under a card-and-position scheme and prove that, conditioned on the marked set and its positions, the marked cards are uniformly ordered — an exchangeability induction on top of Mission III's stopping-rule framework; then the coupon-collector-style tail with an extra $\log n$ factor. Proposition 8.11 requires the fixed-point statistic: the expected number of untouched cards after $t$ transpositions and a second-moment bound, fed into Proposition 7.8. The riffle upper bound runs through inverse shuffles: after $t$ inverse shuffles the deck is a uniform stable sort of $t$ -bit labels, and mixing reduces to the birthday problem for $2^t$ labels; formalizing "distinct labels imply uniform order" is the crux. The $L$ -reversal lower bound needs a second-moment argument for the number of conserved adjacencies with the exact variance bookkeeping of the book. Throughout, the walk-on-group conventions (left vs right increments, forward vs inverse shuffle) are the classic source of silent errors; the formal statements pin them.

Formalization scope

All chains are explicit matrices on Equiv.Perm (Fin n) (or Equiv.Perm (ZMod n) for the circular $L$ -reversal chain); increments act on the left, matching Mission I's group-walk convention. The riffle shuffle is defined as the transpose-reversal of the explicit inverse-riffle matrix — the two have equal distance to uniformity by Lemma 4.13 (Mission II), which a solver may use rather than re-derive. Asymptotic statements ( $o(1)$ , "for sufficiently large $n$ ") are spelled out with explicit $\forall\delta\,\exists N$ quantifiers; upper bounds carry a $+1$ where integer rounding requires it. The $L$ -reversal family takes the length function $L(n)$ as a hypothesis-carrying parameter with $1\le L(n)<n/2$ , and its lower bound is a genuine limit statement (Tendsto, distance to stationarity tending to $1$ ).

Welcome contributions: exchangeability and projection lemmas for deck chains; Eulerian/rising-sequence counting; the single-card chain projection (reused for Mission XI's cutoff examples).

Selected references

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
P. Diaconis, M. Shahshahani, Generating a random permutation with random transpositions, Z. Wahrsch. Verw. Gebiete 57 (1981). https://doi.org/10.1007/BF00535487
D. Bayer, P. Diaconis, Trailing the dovetail shuffle to its lair, Ann. Appl. Probab. 2 (1992). https://doi.org/10.1214/aoap/1177005705
R. Durrett, Shuffling chromosomes, J. Theoret. Probab. 16 (2003). https://doi.org/10.1023/A:1024940217006

19 thms6 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: Shuze Chen

Convex Optimization VI: Self-Concordance and the Barrier MethodTextbook

Why do interior-point methods solve convex programs in $O(\sqrt{m}\log(1/\varepsilon))$ Newton steps? Nesterov and Nemirovskii's answer is self-concordance: a convex function whose third derivative is controlled by its second, $|\varphi'''(t)| \le 2\,\varphi''(t)^{3/2}$ along every line, admits a Newton analysis with absolute constants and no condition number — and the logarithmic barrier is self-concordant. This mission formalizes §9.6 and Chapter 11 of Boyd & Vandenberghe: the self-concordance calculus, the Newton-decrement analysis, the duality gap $m/t$ along the central path, the per-centering work bound $m(\mu - 1 - \log\mu)/\gamma + c$ , and the crown result — with the aggressive schedule $\mu = 1 + 1/\sqrt{m}$ the barrier method reaches duality gap $\varepsilon$ after

\Bigl\lceil \sqrt{m}\,\log_2\bigl(m/(t^{(0)}\varepsilon)\bigr)\Bigr\rceil

centering steps, each of uniformly bounded Newton cost.

19 thms6 active users

Completed

Combinatorics Number Theory·Captain: ShouqiaoWang

Erdős Problem 390: Exact Second-Order AsymptoticResearch Paper

Determine the exact second-order term in the least possible largest factor in a factorization of $n!$ into distinct integers exceeding $n$ , with the proposed rational constant $4029639598/25970038185$ .

97 thms6 active usersReviewed

Completed

Bandit Algorithms Machine Learning Operations Research·Captain: Shuze Chen

Bandit Algorithms XVI: Markov Decision Processes and UCRL2Textbook

The final step from bandits to reinforcement learning: actions now change the state of the world. Chapter 38 of Lattimore–Szepesvári studies online learning in an unknown Markov decision process with $S$ states, $A$ actions and rewards in $[0,1]$ . The optimism principle of Mission II scales up: UCRL2 maintains confidence sets over transition kernels, solves an extended MDP by extended value iteration, and recomputes only when a state-action count doubles. The goal theorem: with probability $1-\delta$ , $\hat R_n < C\,D(M)\,S\sqrt{An\log(nSA/\delta)}$ , where $D(M)$ is the diameter of the MDP — sublinear regret with no prior knowledge of the dynamics. The matching lower bound $\mathbb{E}[\hat R_n] \ge C'\sqrt{DSAn}$ brackets the true complexity of tabular reinforcement learning up to $\sqrt{DS}$ .

35 thms6 active users

Completed

Theoretical Computer Science·Captain: joe

The Sipser–Gács–Lautemann TheoremResearch Paper

Randomness appears to enlarge efficient computation, but the Sipser–Gács–Lautemann theorem places every bounded-error probabilistic polynomial-time language at the second level of the polynomial hierarchy, giving one of complexity theory’s foundational limits on the power of randomization.

66 thms6 active usersReviewed

Completed

Bandit Algorithms Machine Learning Operations Research·Captain: Shuze Chen

Bandit Algorithms VII: Lower Bounds for Finite-Armed BanditsTextbook

How well can any algorithm possibly do? Chapters 13–17 of Lattimore–Szepesvári answer with three matching impossibility results. The divergence decomposition identifies the information a policy collects: $D(\mathbb{P}_{\nu\pi}, \mathbb{P}_{\nu'\pi}) = \sum_i \mathbb{E}[T_i(n)] D(P_i, P_i')$ . Feeding it into the Bretagnolle–Huber inequality of Mission VI yields the goal theorem — the minimax lower bound $R_n \ge \frac{1}{27}\sqrt{(k-1)n}$ over Gaussian bandits, showing MOSS (Mission III) is optimal up to a constant. The same machinery gives the instance-dependent bound of Lai–Robbins type: every consistent policy suffers $\liminf_n R_n/\log n \ge \sum_{i:\Delta_i>0} \Delta_i / d_{\inf}(P_i, \mu^*, \mathcal{M}_i)$ , certifying the asymptotic optimality of the UCB of Mission III and KL-UCB of Mission IV, and a high-probability lower bound showing the Exp3-IX guarantees of Mission V cannot be improved.

13 thms6 active usersReviewed

Number Theory·Captain: Community (Bot)

The Riemann HypothesisOpen Problem

No problem in mathematics carries more weight than the Riemann hypothesis. In his single eight-page paper of 1859, 'On the Number of Primes Less Than a Given Magnitude,' Bernhard Riemann linked the seemingly erratic distribution of the primes to the zeros of the analytic continuation of the zeta function ζ(s), and conjectured that every nontrivial zero lies exactly on the critical line where the real part equals 1/2. The truth of this statement would pin down the error term in the prime number theorem and tame the fluctuations of the primes around their expected count, and hundreds of theorems already stand proven only 'conditional on RH,' waiting for it to be settled. David Hilbert placed it in his eighth problem in 1900, alongside Goldbach and the twin primes; in 2000 the Clay Mathematics Institute named it one of the seven Millennium Prize Problems, with a million-dollar reward. G. H. Hardy proved in 1914 that infinitely many zeros lie on the critical line, and trillions more have since been verified by computation to do so — overwhelming evidence that is nonetheless not a proof. After more than 160 years it remains unresolved. This mission takes Mathlib's own definition of the hypothesis as its target.

507 thms6 active usersReviewed

Completed

Operations Research Optimization Probability+1·Captain: Shuze Chen

Modeling, Measuring and Managing Risk I: Characterizations of Stochastic DominanceTextbook

Why compare whole distributions

A decision maker who must choose between two uncertain profits $Y^{(1)}$ and $Y^{(2)}$ rarely knows their own utility function precisely. Stochastic dominance replaces a single utility by a whole class of them: $Y^{(2)}$ is preferred if every utility in the class prefers it. The resulting partial orders are the basic consistency requirement for risk and acceptability functionals in finance, insurance and stochastic programming: a sensible acceptability functional must never rank a dominated position higher. Dominance constraints are also optimization constraints in their own right, as in the portfolio models of Dentcheva and Ruszczyński (2003).

The analytic characterizations formalized here have a long history. The equivalence of concave dominance with the existence of a mean-preserving kernel goes back to Hardy, Littlewood and Pólya, Blackwell, Stein, Sherman, Cartier, Fell and Meyer, and was given its general form by Strassen (1965). The equivalence between the integrated distribution and integrated quantile function forms of second-order dominance is due to Ogryczak and Ruszczyński (1999). The mission follows the presentation in Chapter 1 of Pflug and Römisch, Modeling, Measuring and Managing Risk (World Scientific 2007, doi:10.1142/6478), §1.2.1–1.2.3, pp. 6–19.

Setting

All outcomes are profit variables: larger is better. A distribution is a probability measure $\mu$ on $\mathbb R$ , with distribution function $G(u)=\mu((-\infty,u])$ and left-continuous quantile function

G^{-1}(p)=\inf\{u : G(u)\ge p\},\qquad 0<p\le 1 .

For a distribution with a finite first moment, the integrated distribution function (IDF) and the integrated quantile function (IQF) are

\mathcal G(u)=\int_{-\infty}^{u}G(v)\,dv,\qquad \mathcal G^{[-1]}(p)=\int_0^{p}G^{-1}(q)\,dq,

and $\mathbb E\{G\}=\mathcal G^{[-1]}(1)$ is its mean. For a nonzero mean, the Lorenz curve is $L_G(p)=\mathcal G^{[-1]}(p)/\mathbb E\{G\}$ .

Four orders are defined through utility classes. For distributions $G_1,G_2$ (laws $\mu_1,\mu_2$ ), $G_1\prec G_2$ means

\int U(v)\,dG_1(v)\le\int U(v)\,dG_2(v)

for every $U$ in the class for which both integrals exist: all nondecreasing $U$ for first-order dominance $\prec_{FSD}$ ; all nondecreasing concave $U$ for second-order dominance $\prec_{SSD}$ ; all concave $U$ for concave dominance $\prec_{CCD}$ ; all convex $U$ for convex dominance $\prec_{CXD}$ . In the Lean development these are FSD μ₁ μ₂, SSD μ₁ μ₂, CCD μ₁ μ₂, CXD μ₁ μ₂, and $G$ , $G^{-1}$ , $\mathcal G$ , $\mathcal G^{[-1]}$ , $L_G$ are distributionFunction, quantileFunction, integratedDistributionFunction, integratedQuantileFunction, lorenzCurve, all in the namespace RiskFunctionals.StochDominance.

Formalization targets

Goal: Theorem 1.13

For probability measures $\mu_1,\mu_2$ on $\mathbb R$ :

$G_1\prec_{FSD}G_2 \iff G_1(u)\ge G_2(u)$ for all $u\in\mathbb R$ ;
$G_1\prec_{FSD}G_2 \iff G_1^{-1}(p)\le G_2^{-1}(p)$ for all $p\in(0,1)$ ;

and, when both have a finite first moment,

$G_1\prec_{CCD}G_2 \iff G_1\prec_{SSD}G_2$ and $\mathbb E\{G_1\}=\mathbb E\{G_2\}$ ;
$G_1\prec_{CCD}G_2 \iff$ there is a Markov kernel $K$ with

G_1(u)=\int K(u\,|\,v)\,dG_2(v)\ \ \forall u,\qquad \int u\,dK(u\,|\,v)=v\ \ \forall v;

$G_1\prec_{SSD}G_2 \iff \mathcal G_1(u)\ge\mathcal G_2(u)$ for all $u\in\mathbb R$ ;
$G_1\prec_{SSD}G_2 \iff \mathcal G_1^{[-1]}(p)\le\mathcal G_2^{[-1]}(p)$ for all $p\in(0,1)$ .

The goal is the conjunction of all six parts.

Milestones

Proposition 1.1(iii): $G^{-1}(p)\le u \iff p\le G(u)$ , for $0<p\le1$ with $G^{-1}(p)$ finite.
Proposition 1.2: if $U$ is uniform on $[0,1]$ , then $G^{-1}(U)$ has distribution $G$ .
Equations (1.19)–(1.20): with a first moment, $\mathcal G(u)=\sup\{uq-\mathcal G^{[-1]}(q): q\in(0,1)\}$ and $\mathcal G^{[-1]}(q)=\sup\{uq-\mathcal G(u): u\in\mathbb R\}$ for $q\in(0,1)$ .
Proposition 1.14(i): if $G_1\prec_{FSD}G_2$ , there are random variables $Y^{(1)}\le Y^{(2)}$ a.s. with marginals $G_1,G_2$ .
Proposition 1.16: for finite nonzero means, $G_1\prec_{CCD}G_2 \iff L_{G_1}(p)\le L_{G_2}(p)$ for all $p\in(0,1)$ and $\mathbb E\{G_1\}=\mathbb E\{G_2\}$ .

Significance

Theorem 1.13 converts statements about infinitely many utility functions into checkable statements about one function: a distribution function, a quantile function, or one of their integrals. Every later use of dominance in the book rests on it: the consistency of the average value-at-risk and of distortion functionals with second-order dominance, the representation of deviation functionals, and the dominance-constrained portfolio models. Part 4 is the bridge from an order on distributions to a construction on random variables (a mean-preserving spread), and part 6 is the form in which second-order dominance enters optimization, through the integrated quantile function that underlies the average value-at-risk.

All six equivalences are classical and proved in the literature. What the mission adds is a machine-checked version in the book's own conventions: utility-defined orders with the "integrals exist" side condition, the profit sign, the left-continuous quantile function and the lower-tail integrals. The platform already holds proved results in neighbouring conventions (Shaked–Shanthikumar's tail-integral characterization of the increasing concave order for random variables, and the conjugacy of second-order performance and quantile functions in Dentcheva–Ruszczyński's form); connecting them to the book's formulation is part of the work.

Difficulty

The directions from an analytic condition back to the utility-defined order are the substance: they must cover every utility of the class that happens to be integrable against the two given laws, including unbounded ones, and the book's printed argument for part 3 passes to a limit over concave utilities without saying why the integrals converge. Part 4 is Strassen's theorem; the book gives no proof, only a reference, and the kernel has to be a measurable family of probability measures satisfying the mean condition at every point, not merely almost everywhere. Part 6 rests on the duality (1.19)–(1.20), which the book derives from a Young inequality (1.18) printed with the inequality reversed, so the printed route cannot be followed literally.

Formalization scope

Distributions are probability measures on $\mathbb R$ , not random variables on a common space; random variables appear only where the book constructs them, each on its own probability space. "For which the integrals exist" is integrability of $U$ with respect to both laws. Concavity and convexity are on all of $\mathbb R$ . The quantile function is real-valued; every statement restricts $p$ to $(0,1)$ or assumes $G^{-1}(p)$ finite, so the junk value of an empty infimum never enters. The first moment is a hypothesis exactly where the book uses $\mathbb E\{G\}$ , $\mathcal G$ or $\mathcal G^{[-1]}$ . Suprema are stated as least upper bounds. In part 4 the kernel is a Markov kernel on $\mathbb R$ , the mean condition holds for every $v$ and includes integrability of the identity under each $K(v)$ .

A trivializing formalization is ruled out: dropping the integrability side condition from the utility classes would make every order compare junk values, and quantifying the orders over all utilities without it would make first-order dominance false for unbounded distributions; neither is done.

Proposition 1.16 is printed with the comparison $L_{G_1}(p)\le L_{G_1}(p)$ ; the formal statement reads it as $L_{G_1}\le L_{G_2}$ and assumes nonzero means, since the Lorenz curve is a quotient by the mean.

Beyond the paper. One variant is posed beside the faithful statements. [Corrected] Proposition 1.16 (ccd_iff_lorenz_corrected, finding F2) assumes positive instead of nonzero means: for a negative common mean the division reverses the comparison, and $G_2=\delta_{-1}$ , $G_1=\tfrac12\delta_{-2}+\tfrac12\delta_0$ satisfy $G_1\prec_{CCD}G_2$ with $L_{G_1}(1/4)=1/2>1/4=L_{G_2}(1/4)$ , so the faithful Proposition 1.16 is expected to be disproved.

The development needs Mathlib's Bochner integral, push-forward measures, Markov kernels, and convex and concave functions on $\mathbb R$ . The quantile function, the IDF/IQF conjugacy and the quantile coupling are reusable for every later chapter of the book (the average value-at-risk, distortion and deviation functionals). A supporting reference item, the proved tail-integral characterization of the increasing concave order for random variables, may be imported for part 5. Contributions of auxiliary lemmas (the quantile Galois connection, integrability of the quantile function under a first moment, approximation of concave utilities) are welcome.

Selected references

G. Ch. Pflug, W. Römisch, Modeling, Measuring and Managing Risk, World Scientific, 2007. https://doi.org/10.1142/6478
V. Strassen, The existence of probability measures with given marginals, Annals of Mathematical Statistics 36 (1965), 423–439. https://doi.org/10.1214/aoms/1177700153
W. Ogryczak, A. Ruszczyński, From stochastic dominance to mean-risk models: semideviations as risk measures, European Journal of Operational Research 116 (1999), 33–50. https://doi.org/10.1016/S0377-2217(98)00167-6
D. Dentcheva, A. Ruszczyński, Optimization with stochastic dominance constraints, SIAM Journal on Optimization 14 (2003), 548–566. https://doi.org/10.1137/S1052623402420528
A. Müller, D. Stoyan, Comparison Methods for Stochastic Models and Risks, Wiley, 2002. ISBN 978-0-471-49446-1
M. Shaked, J. G. Shanthikumar, Stochastic Orders, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

11 thms5 active usersReviewed

Operations Research Optimization Probability+1·Captain: Shuze Chen

Stochastic Networks XI: Gaussian Limits for Large Loss NetworksTextbook

Motivation

A loss network accepts a request only when all resources needed by that request are available. An accepted telephone call, for example, occupies circuits on several links at once. A blocked request leaves immediately. Resource sharing makes route occupancies dependent, even when the arrival streams are independent. For a large network, its exact equilibrium probabilities may be easy to describe but expensive to evaluate. A limit theorem gives a tractable description of fluctuations around the network's typical occupancy. This mission concerns the fixed-topology, growing-capacity regime in Chapter 3 of Kelly and Yudovina, Stochastic Networks, using the supplied Lecture Notes PDF.

The question is not only where mean occupancy settles. Capacity constraints can remove fluctuation directions altogether. The target identifies the surviving Gaussian distribution and retains the moment convergence needed to extract mean occupancies from it.

Setting

There are finitely many links, indexed by $j$ , and finitely many routes, indexed by $r$ . The circuit-requirement matrix $A$ has nonnegative integer entries: a route- $r$ request occupies $A_{jr}$ circuits on link $j$ . Independent Poisson streams bring requests at rates $\nu_r$ . Holding times are independent exponentials of mean one. An arrival is accepted precisely when the capacities permit its entire resource requirement.

The occupancy vector $n\in\mathbb N^R$ records calls in progress. With capacity vector $C\in\mathbb N^J$ , its feasible states are $S(C)=\{n:An\le C\}$ . Equation (3.3) gives the product-form law

\pi(n)=G(C)\prod_r\frac{\nu_r^{n_r}}{n_r!},\qquad G(C)=\left(\sum_{n\in S(C)}\prod_r\frac{\nu_r^{n_r}}{n_r!}\right)^{-1}.

These are countable occupancy states. The route and link index sets are finite; the occupancy coordinates have no fixed upper bound shared across the scaling sequence.

For network number $N\ge1$ , rates and capacities are $\nu(N)$ and $C(N)$ . The matrix $A$ stays fixed and has full row rank. Rates and finite-network capacities are positive, and $\nu(N)/N\to\nu>0$ , $C(N)/N\to C>0$ coordinatewise. The limiting capacities are real. A blocking vector $B\in[0,1)^J$ determines carried traffic $x_r=\nu_r\prod_j(1-B_j)^{A_{jr}}$ . It satisfies $Ax\le C$ , with equality wherever $B_j>0$ . The limiting data also satisfy strict slack: $(Ax)_j<C_j$ whenever $B_j=0$ . These are the standing conditions of §3.5.1 in the source, printed page 62.

Formalization targets

The first milestone supplies the actual normalizing sum in Equation (3.3), its positivity and convergence, detailed balance for the specified loss rates, and the resulting probability measure. It connects the exact law to the published product-form balance theorem without assuming a normalizer.

The second milestone references the complete integer-capacity primal and dual characterization of Theorem 3.10. The continuous mode $x$ uniquely maximizes

\sum_r(x_r\log\nu_r-x_r\log x_r+x_r) \quad\text{over }x\ge0,\ Ax\le C.

Its blocking representation is the one above. A companion theorem extends all clauses to positive real capacities. Lemma 3.13 is the third milestone:

B(N)\to B,\qquad x(N)/N\to x.

The goal is Theorem 3.14. Center the exact occupancy law at its finite-network continuous mode:

u(N)=\frac{n(N)-x(N)}{\sqrt N}.

Let $\mathcal B=\{j:B_j>0\}$ , let $H=A_{\mathcal B}$ , and put $D=\operatorname{diag}(x)$ . The target is

u(N)\Rightarrow U,\qquad \operatorname{Cov}(U)=D-DH^{\mathsf T}(HDH^{\mathsf T})^{-1}HD,

where $U$ is the centered Gaussian supported on $Hu=0$ . Every mixed moment converges, and consequently $\mathbb E[n_r(N)]/N\to x_r$ . All these conclusions, including moments, belong to the printed theorem, page 64.

Significance

The Gaussian limit distinguishes active links from links with spare capacity. Active constraints suppress certain directions, so the limiting covariance can be singular even though all unconstrained coordinate variances are positive. The theorem also justifies passing from the limiting distribution to mean carried traffic; weak convergence alone does not justify that passage.

The published library already contains a proved product-form detailed-balance theorem with an assumed convergent normalizer. It also contains an Open statement of the full integer-capacity primal and dual characterization. Neither is a proof of the Gaussian limit. This mission adds an explicit measure model, a canonical law for null-event Gaussian conditioning, the required normalization obligation, and targets for distribution and moment convergence. The source presents the limit theorem with a sketch; the formal theorem is an unproved target, not a claim that the sketch has already been machine checked.

Difficulty

Local approximations to probability masses do not by themselves control mass escaping to infinity. They also do not establish convergence of unbounded moments. Remarks 3.15 and 3.16 in the source, pages 64–65, explicitly leave tail estimates out of the sketch. The formal goal retains those obligations without assuming tightness or uniform integrability. This omission is recorded as finding F3.

Another difficulty is that the event $Hu=0$ generally has probability zero under the independent Gaussian law. Ordinary division by its event probability does not define the intended distribution. Strict slack is substantive as well: at a critically loaded one-link system, removing it would incorrectly predict an unconstrained normal limit for fluctuations that are always nonpositive, as recorded in F1.

Formalization scope

Lean uses finite link and route indices, natural matrix entries and finite-network capacities, real rates, and the full countable occupancy space. It reuses the published loss-state and weight definitions. The product measure of real Gaussians is mapped by the explicit residual $z\mapsto z-DH^{\mathsf T}(HDH^{\mathsf T})^{-1}Hz$ . Thus the limiting covariance and support are fixed by the data. Empty active sets retain the independent Gaussian; full active rank may give a point mass. Network zero is outside the positive-data assumptions and has no effect on the limits.

Weak convergence is expressed through every bounded continuous real test function. Moments use every multi-index of natural powers, with integrability stated in the conclusion. The blocking selector is computed from the equations, with a zero fallback outside their domain of existence. Existence under positive real capacities remains a theorem obligation. No stochastic limit, moment bound, or convergence premise is hidden in that definition. In particular, a balance identity, an arbitrary proposed limit law, or convergence of means alone cannot satisfy this goal.

No selected statement contains an $O(\cdot)$ estimate or an unspecified failure probability, so there are no explicit-constant replacements. The sketch's unnumbered remainder estimates are not additional targets. Finite-network positivity is the standing domain in which the source defines $B(N)\in[0,1)^J$ ; no strict slack is imposed on individual finite networks.

Beyond the paper. One strengthened companion extends Theorem 3.10 from positive natural to positive real capacities while retaining every conclusion. Finding F5 records that the source's dual argument uses positivity, not integrality. The faithful integer-capacity item stays referenced as a milestone. No sharpness probe or variant of a proof gap is posed. The strengthened statement supplies the real-capacity bridge needed by the limiting regime.

Selected references

F. P. Kelly and E. Yudovina, Stochastic Networks, Cambridge University Press, 2014. DOI. Citations and numbering here refer to the supplied Lecture Notes on Stochastic Networks PDF, Chapter 3, printed pages 49–81 (PDF pages 57–89), SHA-256 ec271d555059aee58613e5e9a98b8346214b16185c527314f5d94c1ac8b17b6a. Equivalence to a particular published printing has not been established.
F. P. Kelly, “Loss networks,” Annals of Applied Probability 1(3), 319–378, 1991. DOI. The existing Open library item for its Theorem 2.8 supplies the matching integer-capacity characterization referenced by this mission.

12 thms5 active usersReviewed

Completed

Markov Chain Operations Research Probability·Captain: Shuze Chen

Stochastic Networks IX: Time Reversal on Countable State SpacesTextbook

Motivation

Queueing models describe systems that repeatedly change state: a customer arrives, a service completes, or a circuit becomes free. Their long-run behaviour depends both on how frequently states are visited and on how long each visit lasts. Looking at an equilibrium trajectory backwards produces another process, whose transitions can expose relationships among these quantities. Chapter 1 of Kelly and Yudovina, Stochastic Networks (2014) introduces this operation before using reversibility in network models. The present target is its countable-state process theorem, Proposition 1.1, in the supplied lecture-notes PDF.

A finite matrix identity alone does not describe what happens to an observed random trajectory. The object here is an actual collection of random variables on one probability space, indexed by every real time. This distinction matters for queues: their occupancy can have arbitrarily large integer values, even when every state has a finite rate of departure.

Setting

A state space $S$ is a nonempty countable set equipped with its discrete measurable structure. On a probability space with probability measure $P$ , the variable $X(t)$ records the state at time $t\in\mathbb R$ . The Markov property says that the conditional law of a later observation, given a finite history with positive probability, depends only on the latest state in that history. This property is defined directly through event probabilities.

A jump rate $q(j,k)$ is nonnegative, and the book sets $q(j,j)=0$ . Its row sum $q(j)=\sum_kq(j,k)$ is the exit rate from $j$ ; every exit rate is positive and finite. Irreducibility means that every state can be reached from every other along a finite sequence of positive-rate transitions. The paths have positive holding intervals and only finitely many changes on each bounded time interval. This is the chapter’s nonexplosion convention.

An equilibrium distribution consists of strictly positive numbers $\pi(j)$ summing to one and satisfying

\pi(j)q(j)=\sum_k\pi(k)q(k,j).

For a process in equilibrium, $P(X(t)=j)=\pi(j)$ at every time. Stationarity is recorded as invariance of every finite-dimensional distribution under a common translation of its time arguments. These conventions follow the source’s definitions on printed pages 13–15, PDF pages 21–23.

Formalization targets

The first milestone is Exercise 1.1. If $S_0$ is exponential with rate $\lambda>0$ , then, for $s,t>0$ ,

P(S_0>s+t\mid S_0>t)=P(S_0>s).

If $T_0$ is independent and exponential with rate $\mu>0$ , then $\min\{S_0,T_0\}$ is exponential with rate $\lambda+\mu$ . The existing proved memorylessness result is retained as a reference; the new exercise item includes both source conclusions.

Exercise 1.2 distinguishes the distribution at an arbitrary time from that at a jump. With the finite normalizer $G=\sum_j\pi(j)q(j)$ , the jump-chain probabilities and equilibrium masses are

p(j,k)=\frac{q(j,k)}{q(j)},\qquad \pi^J(j)=\frac{\pi(j)q(j)}G.

The target asserts positivity, normalization, and the jump-chain equilibrium equations. This milestone is a supporting result about the same rate model; it is not claimed to be a prerequisite invoked by the printed reversal proof.

Exercise 1.3 characterizes the Markov property by conditional independence of the past and future. For any finite past observation event $A$ , finite future observation event $B$ , and present state $j$ with positive probability, it asserts the equivalence with

P(A\cap B\mid X(t)=j)=P(B\mid X(t)=j)P(A\mid X(t)=j).

Both directions of the equivalence are part of the target.

The goal is Proposition 1.1: for the actual random variables $Y(t)=X(-t)$ , the reversed process is stationary and Markov, with equilibrium distribution $\pi$ and rates

q'(j,k)=\frac{\pi(k)q(k,j)}{\pi(j)}.

This includes the off-diagonal small-time conditional-probability limits. All four targets are from printed pages 16–17, PDF pages 24–25, of the supplied source.

Significance

The theorem identifies the stochastic process seen under reversal, including its conditional laws and the rate at which each possible transition occurs. It supplies the foundation for distinguishing general stationary processes from reversible ones. Reversibility requires the reversed rates to agree with the original rates; stationarity by itself does not require that agreement.

The existing finite-state rate-balance theorem establishes an algebraic part of the picture. An existing finite-state reversal theorem treats finite-dimensional distributions constructed from a finite transition matrix. This mission adds the countable-state theorem for specified random variables on a common probability space. The mathematical result is classical; the deliverable is a faithful formal statement and, subsequently, a machine-checked proof. The local theorem bodies remain proof obligations.

Difficulty

The central issue is preserving conditional laws when the ordering of observations is reversed. A balance equation has no history events and cannot establish this property. Countable summations also require genuine convergence; a real-valued infinite sum without a summability condition can return Lean’s default value and lose the intended probabilistic meaning.

The printed proof has a minor diagonal oversight, recorded as finding F1. Its displayed small-time expansion cannot hold on the diagonal, where the probability of staying in the current state approaches one. The statement’s zero-diagonal convention remains intact. The goal must also retain nonexplosion without imposing a finite mean jump intensity in equilibrium: those are different requirements, as finding F3 illustrates.

Formalization scope

All random variables are measurable and all measures used for probability calculations are probability measures. Real conditional probabilities are ratios of finite event probabilities, with positive conditioning events at every nontrivial use. Exponential laws and independence use Mathlib’s existing measure-theoretic definitions. Finite time lists use Fin n, including empty lists. State spaces use Countable, never Fintype.

The process predicates are explicit local abbreviations inside the goal statement. They contain real definitions, not unproved model axioms. The path predicate permits either adjoining state as the value exactly at a jump, because reversing time exchanges left and right continuity. Away from jump endpoints it requires locally constant paths, with finitely many possible changes on every bounded interval. No claim that the literal reversed path is right-continuous is made.

The published balance definition is retained as a reference. Its formulas appear directly in the theorem statements, so no new globally named balance or reversed-rate definition is introduced and no missing shared module is imported. Every infinite real sum is guarded by Summable or HasSum. The normalizer’s positivity is proved as part of Exercise 1.2, while positivity of each equilibrium mass is a standing source assumption. No asymptotic constants are instantiated: the targets contain no big-O estimates or high-probability bounds.

The goal cannot be discharged by defining Markovianity to mean past–future independence, or by substituting a rate-balance identity for the reversed process. Contributions proving the conditional-law equivalence, the countable summation identities, and the full reversal statement fit this scope. No variant items are posed; the faithful source statements remain the goal and milestone anchors.

Selected references

F. P. Kelly and E. Yudovina, Stochastic Networks, Cambridge University Press, 2014. DOI. The pinned supplied artifact is titled Lecture Notes on Stochastic Networks; its equivalence to a particular published printing is unverified. This mission cites its Chapter 1, printed pages 13–17, PDF pages 21–25, SHA-256 ec271d555059aee58613e5e9a98b8346214b16185c527314f5d94c1ac8b17b6a.

6 thms5 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research·Captain: Shuze Chen

Flows in Networks IV: Unicursal Mixed GraphsTextbook

Motivation

Graph theory began with a unicursal problem: Euler's question whether the bridges of Königsberg can be crossed in one closed walk using each bridge exactly once. For graphs whose arcs are all undirected, or all directed, the answer has been known since the nineteenth century: a connected graph has such a closed walk exactly when every node has even degree, respectively when every node has as many incoming as outgoing arcs. Street networks mix one-way and two-way streets, so routing problems such as the Chinese postman problem live on mixed graphs, where neither criterion applies.

Chapter II, §7 of Ford and Fulkerson's Flows in Networks (RAND Report R-375-PR, 1962; Princeton University Press, 1962) settles the mixed case with a necessary and sufficient condition read off from network flows. The same chapter treats, in §4 and §8, the other classical min–max theorems of combinatorics that flow theory reproves in a few lines: the König–Egerváry theorem on bipartite graphs, Menger's theorem on disjoint chains, and Dilworth's chain decomposition theorem for partially ordered sets.

Setting

A mixed graph $G = [N; \mathcal A]$ has a finite set $N$ of nodes and a set $\mathcal A$ of arcs. An arc is either directed, an ordered pair $(x, y)$ leading from $x$ to $y$ , or undirected, an unordered pair $\{x, y\}$ . No arc joins a node to itself, and there is at most one arc leading from one node to another: at most one directed arc $(x, y)$ , at most one undirected arc $\{x, y\}$ , and never both an undirected and a directed arc on the same pair. Directed arcs $(x, y)$ and $(y, x)$ may both be present.

A closed route is a sequence $x_0, a_0, x_1, a_1, \dots, a_{m-1}, x_m = x_0$ of nodes and arcs in which each $a_i$ leads from $x_i$ to $x_{i+1}$ : a directed arc is traversed with its direction, an undirected arc in either direction. Nodes may repeat, and a single node ( $m = 0$ ) is a closed route. The graph $G$ is unicursal if some closed route contains every arc of $G$ exactly once and every node of $G$ at least once.

$G$ is connected if $N$ is nonempty and any two nodes are joined by a path, arcs being allowed against their direction. The degree of a node counts the arcs incident with it, directed and undirected together. For $X \subseteq N$ with complement $\bar X = N - X$ , write $d^+(X)$ and $d^-(X)$ for the numbers of directed arcs from $X$ to $\bar X$ and from $\bar X$ to $X$ , and $u(X)$ for the number of undirected arcs joining $X$ and $\bar X$ .

For §4, a chain in a directed graph is a sequence of at least two distinct nodes with consecutive pairs arcs, and an $S, T$ disconnecting set of nodes meets every chain from $S$ to $T$ . For §8, $P = \{1, \dots, n\}$ is partially ordered by $\succ$ , a decomposition partitions $P$ into chains $i_1 \succ \cdots \succ i_k$ , and the bipartite graph of $P$ has an arc $(x_i, y_j)$ whenever $i \succ j$ ; independent arcs are pairwise node disjoint, and a proper cover is a node set meeting every arc with no proper subset doing so.

Formalization targets

Goal: Chapter II, Theorem 7.1 (pp. 42–43)

The mixed graph $G$ is unicursal if and only if

$G$ is connected;
every node of $G$ is incident with an even number of arcs;
for every $X \subseteq N$ ,

d^+(X) - d^-(X) \le u(X).

Milestones

Theorem 4.1 (König–Egerváry, p. 32): in a bipartite graph $[S, T; \mathcal A]$ the maximal number of pairwise node disjoint arcs equals the minimal number of nodes in an $S, T$ disconnecting set. This is a reference to the published MatousekLP.Integrality.konig.
Theorem 4.2 (Menger, p. 34): for disjoint $S, T \subseteq N$ ,

\max \#\{\text{pairwise node disjoint chains from } S \text{ to } T\} = \min \{|D| : D \text{ an } S, T \text{ disconnecting set of nodes}\}.

Lemma 8.1 (p. 46): every independent set $\mathcal J$ of arcs of the bipartite graph of $P$ yields a decomposition $\Delta$ of $P$ with $|\mathcal J| + |\Delta| = n$ .
Lemma 8.2 (p. 47): every proper cover $X$ yields a set $U$ of mutually unrelated elements with $|X| + |U| = n$ .
Dilworth's theorem (p. 45): the maximal number of mutually unrelated elements of $P$ equals the number of chains in a minimal decomposition. This is a reference to the published AppliedComb.Posets.dilworth.

Significance

Theorem 7.1 contains both classical Euler criteria: for an undirected graph condition 3 is vacuous, and for a directed graph, applied to single nodes and their complements, it forces equal in- and out-degrees. In the mixed case, condition 3 is a cut condition over all node subsets, which is what makes unicursality decidable by one feasible-circulation computation. That computation is the first step of the Edmonds–Johnson treatment of the mixed Chinese postman problem (Edmonds & Johnson, 1973). Lemmas 8.1 and 8.2 are the bridge by which König's theorem gives Dilworth's theorem, and through it minimal chain decompositions that a bipartite matching algorithm can compute.

All results here are classical and proved; none of the book's statements has been formalized in this form. The platform has Proved formalizations of König's theorem and of Dilworth's theorem, used here as references. It also has an undirected set-to-set Menger theorem (Menger.menger_set), Euler's criterion for undirected multigraphs (AppliedComb.Graphs.eulerian_iff), and the existence of an Euler tour in a connected, even, symmetric mixed graph (ChinesePostman.Mixed.mixed_euler_tour). That last result is one step of the sufficiency direction of Theorem 7.1, not the theorem itself. The directed, node-disjoint, set-to-set Menger theorem and the mixed-graph criterion are new.

Difficulty

Necessity in Theorem 7.1 is a counting argument. Sufficiency is not: conditions 2 and 3 do not by themselves say which way to orient each undirected arc. A wrong local choice can leave a node unbalanced with no way to repair it, so a greedy orientation does not work. The global information is the cut condition over all $2^{|N|}$ subsets, and turning it into an orientation needs a feasibility theorem for circulations with integral solutions. Only then does the classical Euler argument apply, and that argument also needs an induction that splits off closed routes and reassembles connected pieces. For Lemma 8.2 it is showing that a proper cover never contains both copies $x_i$ and $y_i$ of an element; this uses transitivity, and finding F2 shows it fails without it.

Formalization scope

Nodes are a Fintype with decidable equality. A mixed graph has directed arcs in a Finset (N × N) and undirected arcs in a Finset (Sym2 N); an arc is an element of (N × N) ⊕ Sym2 N. A closed route with $m$ arcs is a pair of maps Fin (m+1) → N and Fin m → MixedArc N, and "each arc exactly once" is injectivity plus surjectivity onto the arcs of $G$ . Unicursality is defined by the existence of such a route, never by conditions 1–3, and condition 3 is quantified over every subset $X \subseteq N$ with the difference taken in $\mathbb Z$ . These two choices rule out the trivializing formalization in which "unicursal" is defined by the theorem's own conditions or condition 3 is checked only at single nodes. Connectedness includes nonemptiness of $N$ , so the empty graph is neither unicursal nor connected.

For §4, chains are lists of distinct nodes, and Theorem 4.2 states the maximum and the minimum as attained (IsGreatest, IsLeast) with a common value. For §8, $P$ is Fin n with a relation carrying IsStrictOrder; the bipartite graph's nodes are Fin n ⊕ Fin n, and a decomposition is a Finpartition of Fin n into chains.

Beyond the paper. Two variant items stand beside the faithful statements. [Strengthened] Lemma 8.1 replaces the partial order by any relation without directed cycles. The book asserts this on p. 47, and the proof uses only that an independent arc set gives each element at most one successor and one predecessor (finding F1). [Sharpness probe] Lemma 8.2 makes the same weakening for Lemma 8.2 and is expected to be false: on five elements $0, \dots, 4$ with $0 \succ 1$ , $0 \succ 2$ , $0 \succ 3$ , $1 \succ 4$ , $2 \succ 4$ , $3 \succ 4$ and no other relations, $\{y_1, y_2, y_3, x_1, x_2, x_3\}$ is a proper cover of size $6 > n$ (finding F2).

A complete development needs Euler-tour infrastructure for mixed graphs, Hoffman's circulation theorem with integrality, and integral max-flow for Menger. Of these, the circulation theorem is the subject of a sibling mission (Flows in Networks III). Proofs of any item by any method are welcome, including direct combinatorial proofs that avoid flows.

Selected references

L. R. Ford, Jr. and D. R. Fulkerson, Flows in Networks, The RAND Corporation, Report R-375-PR, 1962; Princeton University Press, 1962. https://doi.org/10.1515/9781400875184
J. Edmonds and E. L. Johnson, Matching, Euler tours and the Chinese postman, Mathematical Programming 5 (1973), 88–124. https://doi.org/10.1007/BF01580113
K. Menger, Zur allgemeinen Kurventheorie, Fundamenta Mathematicae 10 (1927), 96–115. https://doi.org/10.4064/fm-10-1-96-115
R. P. Dilworth, A decomposition theorem for partially ordered sets, Annals of Mathematics 51 (1950), 161–166. https://doi.org/10.2307/1969503
D. König, Gráfok és mátrixok, Matematikai és Fizikai Lapok 38 (1931), 116–119.

9 thms5 active usersReviewed

Combinatorics Graph Theory·Captain: harry

Conway 99: structural constraints and graph reconstructionOpen Problem

Motivation

John Conway asked whether a graph on 99 vertices can have every edge in exactly one triangle and every nonedge in exactly one quadrilateral. He included this question among his five $1,000 problems and explicitly accepted either a construction or a proof of impossibility (Conway, 2017). This mission organizes structural constraints and graph reconstruction around the existing public formal statement, which remains open. It complements the existing Conway mission: both point to the same mathematical question, while this mission curates additional published intermediate theorems and the precise bridges still needed to use them.

The historical restriction most relevant here is Wilbrink's 1984 theorem that a hypothetical graph cannot be vertex-transitive (Wilbrink's paper). That result is already formalized on Prove2Me. The consolidated local Conway99 development also contains graph-owned point, finite-field, and rooted constraints. Its written and finite-check results have different verification levels; the platform-accepted lemmas cited below are the machine-checked part of that work.

Setting

A strongly regular graph with parameters $(n,k,\lambda,\mu)$ is a finite simple graph on $n$ vertices in which each vertex has $k$ neighbours, adjacent vertices have exactly $\lambda$ common neighbours, and distinct nonadjacent vertices have exactly $\mu$ common neighbours. Write $G$ for a candidate graph and $A$ for its integer adjacency matrix, whose $(u,v)$ entry is $1$ when $u$ and $v$ are adjacent and $0$ otherwise. Let $I$ be the identity matrix and $J$ the all-ones matrix. In this mission, the parameter tuple is $(99,14,1,2)$ .

The condition $\lambda=1$ makes each edge part of a unique triangle. Each vertex's 14 neighbours split into seven paired edges. The condition $\mu=2$ makes each nonadjacent pair have exactly two common neighbours. These facts lead to $231$ triangles and the matrix equation $A^2+A=12I+2J$ , both already proved on the platform (triangle count, matrix identity). Choosing one vertex as a root splits the remaining vertices into its 14 neighbours and 84 nonneighbours; the graph's actual adjacency blocks then satisfy further identities (rooted theorem). The word actual matters: arbitrary matrices satisfying some of these identities have not thereby been shown to arise from one graph.

Formalization targets

Goal

\exists\,(\alpha:\mathrm{Type})\,(\_:\mathrm{Fintype}\,\alpha)\,(G:\mathrm{SimpleGraph}\,\alpha)\,(\_:\mathrm{DecidableRel}\,G.\mathrm{Adj}),\quad \mathrm{IsSRGWith}\;G\;99\;14\;1\;2.

This is the already published Conway99.conway_99 theorem, reused as the goal. A graph satisfying it proves existence; a proof of the negation of this full existential settles nonexistence. Neither outcome has been established in the archive.

Structural and reconstruction targets

The first layer collects necessary facts about every hypothetical $G$ : rooted block equations, point-Gram identities, and finite-field identities. The accepted theorems are rooted blocks, point Gram, and finite fields. An independent binary cut-response rank theorem supplies reusable seven-vertex algebra; its statement does not assume a Conway graph. A selected twelve-owner contact theorem gives a further conclusion only when its chosen triangle, owner set, and regularity premises hold.

The reconstruction layer asks whether compatible local data can be obtained from, or assembled into, one graph satisfying all four strongly regular parameters. The public adjacency-matrix formulation and triangle line-system formulation are still open. A future coclique-completion equivalence concerns graphs with a specified independent 22-set; it cannot replace the unrestricted goal unless that set is shown to exist in every candidate. No unpublished or pending statement is presented as a completed milestone.

An accepted admitted-coclique spike theorem supplies a precise lattice membership identity when a 22-point set and its point-vector average are already admitted to one lattice. It does not produce that coclique, establish the needed lattice for every graph, or close the reconstruction gap. An accepted printed-census correction is retained as a reference to prevent the known erroneous expressions from being reused as graph counts; it is an audit of formulas, not a structural exclusion.

Significance

A construction would settle Conway's existence question with a checkable 99-vertex object. A nonexistence proof would explain why the local triangle and common-neighbour conditions cannot coexist globally, despite the standard parameter equations being consistent. Either result must address the whole graph, not one selected root, lattice, shell, or completion packet (Conway's question; formal goal).

The formalization already gives reusable graph-owned interfaces: block identities from an actual root, a point Gram representation, and modular restrictions. Those are machine-checked necessary conditions, while deeper rank, lattice, triangle-transport, and finite-support exclusions in the consolidated local development remain written or locally checked mathematics. This mission makes their status visible and provides a place to connect faithful formal versions as they are published. A conditional theorem remains useful, but its hypotheses must be derived from the candidate graph before it can narrow the unrestricted goal.

Difficulty

The adjacency equation and its eigenvalue multiplicities constrain every candidate but do not determine the binary off-diagonal entries of $A$ . Local equations can have feasible matrix or incidence data even when those data have not been embedded in a common simple graph. Conversely, excluding a fixed support, one lattice choice, or a branch with an ordinary point leaves other configurations untouched. The consolidated local frontier records those coverage gaps, including exceptional-only configurations and unexcluded incidence systems. The central task is to close a graph-wide bridge or exhibit a graph, while retaining every hypothesis on narrower results.

Formalization scope

The goal uses Mathlib's SimpleGraph.IsSRGWith and quantifies over a finite vertex type, a graph, and decidable adjacency exactly as in the published statement. Supporting statements may use Fin 99 after an explicit relabelling, integer adjacency matrices, finite triangle sets, real Gram matrices, and finite-field reductions. They must derive data from one G, or mark any independent packet as an additional hypothesis. A theorem about selected owners, a prescribed coclique, a particular determinant or rank, or a saved finite support must keep that restriction visible; none may silently assert that every candidate supplies it.

Existing published definitions and theorems should be imported by their platform IDs. Contributions are welcome for exact bridges between graph, matrix, triangle, and coclique representations; proofs that a conditional packet follows from every candidate; faithful formalizations of written universal constraints; and a construction or unconditional contradiction. The mission's published milestones record actual theorem statements. Prospective bridge descriptions remain research targets until they have separately audited and published platform IDs.

Selected references

J. H. Conway, Five $1,000 Problems (Update 2017), OEIS attachment, 2017. PDF.
H. A. Wilbrink, On the (99,14,1,2) strongly regular graph, in Papers Dedicated to J. J. Seidel, EUT-Report 84-WSK-03, Technische Hogeschool Eindhoven, 1984, pp. 342–355. Institutional PDF; publication record.

19 thms5 active usersReviewed

Completed

Economics Operations Research Optimization+1·Captain: mikedeng1

Is Price Commitment a Better Solution to Control Carbon Emissions and Promote Technology Investment?: Correlation Thresholds for Consumer Surplus and Emissions, Carbon Tax vs Cap-and-TradeResearch Paper

Motivation

Carbon pricing changes both a manufacturer's production decisions and its incentive to invest in cleaner technology. A carbon tax fixes the price of emissions in advance. Cap-and-trade fixes an emissions quota while the price of permits changes with market conditions. The comparison is especially sensitive to whether high product demand tends to coincide with a high permit price. Fan, Chen, and Chen study that interaction for a firm that chooses its technology before learning demand and then adjusts production after uncertainty is resolved. Their preprint finds that the preferred policy can change as demand and permit prices become more correlated. This mission concerns the paper's base model and its comparisons of consumer surplus and emissions.

Setting

A monopolist sells quantity $q$ at the inverse demand price $a-bq$ , where $b>0$ is demand sensitivity and the random variable $a$ is market potential. A unit of output emits $\gamma$ units of carbon. Before observing market conditions, the firm chooses $\gamma\in[0,\gamma^+]$ by paying the technology investment cost $\beta(\gamma^+-\gamma)^2$ . After observing demand and, under cap-and-trade, the permit price $k$ , it chooses $q$ . The operating profit is

\pi(q;\gamma,a,k)=(a-bq)q-(\gamma q-w)k, \qquad q^*(\gamma,a,k)=\frac{a-\gamma k}{2b}.

Here $w$ is the assigned emissions quota. If emissions are below $w$ , the permit term is a receipt from selling unused permits. The carbon tax sets the carbon price to the mean permit price $\bar k$ . Its term $w\bar k$ is the paper's lump-sum green subsidy, so the same $w$ appears in both regimes. Under cap-and-trade, $k$ remains random. These definitions follow §3 and equations (1)–(3) of the source preprint.

Let $\bar a$ and $\bar k$ be the means of $a$ and $k$ , let $\sigma_D$ and $\sigma$ be their standard deviations, and let $\rho$ be their correlation. The first-stage objectives $\Pi_T(\gamma)$ and $\Pi_C(\gamma)$ are expected operating profit under the tax and cap-and-trade, respectively, less the investment cost. Their maximizers on $[0,\gamma^+]$ are denoted $\gamma_T^*$ and $\gamma_C^*$ . Expected consumer surplus is the expected value of $b(q^*)^2/2$ in each regime, denoted $CS_T$ and $CS_C$ . Expected emissions are the expected values of $\gamma_T^*q_T^*$ and $\gamma_C^*q_C^*$ , denoted $S_T$ and $S_C$ . The welfare quantities are those of equations (8)–(9) in the preprint.

The paper's Assumption 1 requires sufficiently high investment cost, expressed by $4b\beta>\bar k^2+\sigma^2$ and $4b\beta\gamma^+>\max\{\bar a\bar k,\bar a\bar k+\rho\sigma_D\sigma\}$ , together with $a>\gamma^+k$ for realized demand and permit price. The comparison uses thresholds $R_0=(\sigma/\sigma_D)\gamma_T^*$ and $R$ , with $0<R<R_0$ . The latter is specified by the piecewise formulas for $\rho_0$ and $\rho_1$ in Proposition 2(a) of the preprint.

Formalization targets

The target is Corollary 1(a)–(b), on pages 19–20 of the preprint. Its consumer-surplus part asserts the existence of two thresholds, $R_1<R<R_0<R_2$ , such that

CS_T>CS_C\quad\Longleftrightarrow\quad R_1<\rho<R_2.

The thresholds depend on the fixed model parameters and moments, and the comparison holds for every admissible joint distribution with those moments. The emissions part compares $S_T$ and $S_C$ on each side of $R_0$ . For $\rho<R_0$ , it says $S_T<S_C$ when $\gamma_T^*+\gamma_C^*<\bar a/\bar k$ , and $S_T\ge S_C$ otherwise. For $\rho>R_0$ , the strict comparison reverses and the other case becomes $S_T\le S_C$ . The printed corollary leaves $\rho=R_0$ outside these two cases.

The supporting targets follow the source's attack path: the second-stage quantity in equation (1), the expected-profit moment forms in the proofs of Lemmas 1–2, the unique optimal emission intensities in Lemmas 1–2, the investment and profit comparisons in Propositions 1(a) and 2(a), and the consumer-surplus and emissions identities in the proof of Corollary 1.

Significance

The corollary separates two outcomes that a carbon policy can affect in different ways. It specifies when the tax yields higher expected consumer surplus and when it yields lower expected emissions, rather than inferring either outcome from the firm's profit alone. In the interval between $R$ and $R_0$ , the source also identifies stronger clean-technology investment and higher firm profit under the tax. Its policy comparison can therefore be applied only after identifying the relevant correlation and the position of the optimal intensities relative to $\bar a/\bar k$ .

The paper proves the result analytically. This formalization records its base model, expectation identities, and threshold comparisons as Lean statements. The goal and milestone proofs remain to be machine checked. A completed development would make the probabilistic moment calculations and the piecewise threshold reasoning reusable for other two-stage production models with correlated prices and demand.

Difficulty

The correlation changes the cap-and-trade investment choice, and that choice can reach the boundary $\gamma^+$ . Consequently, the consumer-surplus comparison changes algebraic form across the boundary. The proof of Corollary 1 describes the surplus difference as a quadratic in $\rho$ ; this description applies to the interior branch, while the boundary branch is linear. The formal target is the full interval assertion across both branches. The threshold $\rho_0$ also solves a quadratic equation with two roots; the relevant one is the smaller root in the domain allowed by Assumption 1.

Formalization scope

Lean represents $a$ and $k$ as real random variables on a probability space, with $L^2$ hypotheses so every quadratic expectation is integrable. Their means are integrals, their standard deviations are square roots of variance, and $\rho$ is covariance divided by $\sigma_D\sigma$ . The standing conditions are $b>0$ , $\gamma^+>0$ , $\bar k>0$ , $\sigma_D>0$ , and $\sigma>0$ ; $w$ is unrestricted. The paper's realized-demand clause is interpreted almost surely. These conditions keep the divisions in the formulas meaningful and state the paper's positive-price and nondegenerate-uncertainty conventions. The parameter-level conditions in the uniform consumer-surplus claim include the correlation-free consequences of Assumption 1.

Optimal intensities are maximizers of the expectation-based objectives on $[0,\gamma^+]$ . The comparison statements quantify over arbitrary maximizers; the closed forms are established separately. The surplus thresholds $R_1,R_2$ are selected before quantifying over probability models with the fixed moments. This prevents them from depending on a particular realized correlation. Lean names $\gamma^+$ as γp and defines $\rho_0$ using the smaller-root condition; its fallback value outside that condition is not used under the theorem hypotheses.

The scope is the base model with advance technology investment and full production flexibility in §§3–5. The case studies of §6 and the modified models of §7 and the Online Appendices A–B are outside this mission. Useful supporting work includes identities for expectations of products of $L^2$ variables, strict concavity and uniqueness of the first-stage maximizers, and the piecewise correlation thresholds.

Selected references

X. Fan, K. Chen, and Y.-J. Chen, Is Price Commitment a Better Solution to Control Carbon Emissions and Promote Technology Investment?, SSRN preprint 3817235, version of November 15, 2021; published in Management Science, 2022. Preprint. DOI.

10 thms5 active usersReviewed

All missions

Immune High-Girth Bipartite Graphs (Feghali-Lucke-Paulusma-Ries 2025)Research Paper

Motivation

Setting

Formalization targets

Lemma 5 — immune high-girth graphs

Negative OPG consequence

Significance

Difficulty

Formalization scope

Selected references

Collapsible CubicsOpen Problem

Motivation

Setting

Formalization targets

Goal — every cubic algebraic number is collapsible

Supporting targets

Significance

Difficulty

Formalization scope

Selected references

Formalizing an 8-Vertex Candidate Counterexample to the Geodesic-Cycle Assignment Problem (OPG-500)Open Problem

Motivation and historical context

Setting

Formalization targets

Main target: the universal eight-vertex obstruction

Supporting targets

Significance

Difficulty

Formalization scope

Selected references

Smale's Ninth Problem: Strongly Polynomial Linear ProgrammingOpen Problem

The problem of solving linear inequalities

Why it matters

The question and what is known

A hierarchy of formalization targets

Formalization scope

Selected references

Ordinary p-adic L-functions: Mazur–Tate–Teitelbaum interpolationResearch Paper

Why construct a p-adic L-function?

Modular forms, periods, and measures

Formalization targets

What the formalization supplies

Where the difficulty lies

Formalization scope and conventions

Selected references

Erdős Problems 97 and 96: Convex Point Sets and Unit DistancesOpen Problem

Closed — negative resolution of Erdős Problems 96 and 97

Historical mission description

Motivation

Why Problems 97 and 96 belong together

Setting

Target

Significance

Difficulty

Counterexample routes

Formalization scope

References

Multiplicative Number Theory I: Siegel–Walfisz and the Three Primes TheoremTextbook

Primes in progressions, uniformly in the modulus

Setting

Formalization targets

What the result gives, and what remains to be formalized

Where the obvious argument fails

Formalization scope

Selected references

Symplectic Modules Free over an Abelian NilradicalResearch Paper

Motivation

Setting

Formalization targets

Common polynomial-module family

Significance

Difficulty

Formalization scope

Selected references

Arbitrary Torsion in Moment-Angle Homology and Loop HomologyResearch Paper

Motivation

Setting

Formalization targets

Arbitrary torsion in one moment-angle manifold