Motivation

Every algorithm in the first three chapters of Foster and Rakhlin's Foundations of Reinforcement Learning and Interactive Decision Making — ε-Greedy and UCB for the multi-armed bandit, Inverse Gap Weighting and SquareCB for contextual bandits — is a special case of the same two-step recipe: estimate a model of the world with an online regression oracle, then convert the estimate into a decision that trades exploration against exploitation. Chapter 4 asks whether this recipe can be made generic: given any structured decision-making problem, specified only by a function class $F$ and a decision space $\Pi$, is there a single quantity that governs the best achievable regret, the way $\sqrt{A/\gamma}$ governs the multi-armed bandit and $\sqrt{d/\gamma}$ governs the linear bandit? The chapter's answer is the Decision-Estimation Coefficient (DEC), introduced by Foster, Kakade, Qian, and Rakhlin [40] as a complexity measure that both upper- and lower-bounds achievable regret for a general decision-making protocol, unifying results that were previously proved from scratch, case by case, for each structured setting. This mission formalizes the chapter's central upper bound (Proposition 13) together with the machinery that makes it computable in two concrete cases — the multi-armed bandit (Proposition 14) and the linear bandit (Propositions 16–17).

Setting

Fix a finite decision space $\Pi$ and a class $F \subseteq \mathbb{R}^\Pi$ of candidate mean-reward functions, with a ground-truth $f^\star \in F$ (realizability). Over $T$ rounds, at each round $t$ the learner observes an estimate $\hat f_t$ produced by an online regression oracle, plays a decision distribution $p_t \in \Delta(\Pi)$ (possibly depending on $\hat f_t$ and the history), and the regret is

$$\mathrm{Reg} := \sum_{t=1}^T f^\star(\pi^\star) - \sum_{t=1}^T \mathbb{E}_{\pi \sim p_t}[f^\star(\pi)],$$

where $\pi^\star = \arg\max_\pi f^\star(\pi)$. The oracle's cumulative estimation error is assumed bounded: $\sum_{t=1}^T \mathbb{E}_{\pi \sim p_t}[(\hat f_t(\pi) - f^\star(\pi))^2] \le \mathrm{EstSq}(F,T,\delta)$ with probability at least $1-\delta$ (Definition 7). Writing $\pi_f := \arg\max_\pi f(\pi)$, the DEC game value at a reference model $\hat f$ and scale $\gamma > 0$ is the min-max quantity

$$\mathrm{dec}_\gamma(F, \hat f) := \min_{p \in \Delta(\Pi)} \max_{f \in F} \; \mathbb{E}_{\pi \sim p}\bigl[f(\pi_f) - f(\pi) - \gamma(f(\pi) - \hat f(\pi))^2\bigr],$$

and the DEC of $F$ itself is $\mathrm{dec}_\gamma(F) := \sup_{\hat f \in \mathrm{co}(F)} \mathrm{dec}_\gamma(F, \hat f)$. The Estimation-to-Decisions (E2D) algorithm plays, at each round, a $p_t$ certifying (i.e. attaining or beating) the value of this min-max game at $\hat f_t$.

Formalization targets

Goal — Proposition 13 (E2D regret bound)

$$\mathrm{Reg} \le \mathrm{dec}_\gamma(F) \cdot T + \gamma \cdot \mathrm{EstSq}(F, T, \delta)$$

with probability at least $1-\delta$, for any exploration parameter $\gamma > 0$. This is the weakest stable statement the chapter proves about E2D: it holds for an arbitrary function class and an arbitrary regression oracle, with no structural assumption on $F$ beyond realizability, and the chapter's later sections instantiate it rather than strengthen it.

Milestones

• Lemma 9 (Decoupling), general form: for any distribution $\nu$ over a finite model class and any $\bar f$, $\mathbb{E}_{f\sim\nu}[f(\pi_f) - \bar f(\pi_f)] \le \sqrt{A \cdot \mathbb{E}_{f\sim\nu}\mathbb{E}_{\pi\sim p}[(f(\pi)-\bar f(\pi))^2]}$ — the estimation-to-decisions bridge the whole chapter's approach rests on, decoupling the model index from the played decision.
• Proposition 14 (IGW minimizes the DEC): for the multi-armed bandit ($\Pi=[A]$, $F=\mathbb{R}^A$), Inverse Gap Weighting is the exact minimizer of the DEC game, giving $\mathrm{dec}_\gamma(F) = (A-1)/(4\gamma)$ — the first concrete computation of an abstract quantity, recovering Chapter 3's rate from Proposition 13 alone.
• Proposition 16 (G-optimal design): existence, for any compact full-dimensional-span set $Z \subseteq \mathbb{R}^d$, of a distribution $p$ with $\sup_{z\in Z}\langle \Sigma_p^{-1}z,z\rangle \le d$ — the classical convex-analysis primitive Proposition 17 needs.
• Proposition 17 (DEC for linear bandits): combining the G-optimal design with inverse gap weighting gives $\mathrm{dec}_\gamma(F) \lesssim d/\gamma$ for the linear bandit function class, leading via Proposition 13 to a $\sqrt{dT}$ regret bound.

Significance

The Decision-Estimation Coefficient is, in the book's own words, "the main result" of this line of work: Foster, Kakade, Qian, and Rakhlin [40] show it is not merely an upper bound but (in a suitable localized form, developed further in Chapter 6) a tight characterization of the minimax regret for structured bandits and, more generally, for the interactive decision-making protocol the rest of the book studies. Proposition 13 is the mechanism that makes this useful in practice: it reduces regret analysis for a new structured problem to a single, purely convex-analytic computation of $\mathrm{dec}_\gamma(F)$, in place of a bespoke exploration argument. Propositions 14–17 are the demonstration that this reduction is not vacuous — they recompute, via the DEC alone, the two rates (multi-armed and linear bandit) that earlier chapters of the book derived by direct, setting-specific arguments, and the match is exact. Formalizing this chapter therefore captures the book's unifying abstraction itself, not just one more instance of it. No formalization of the Decision-Estimation Coefficient, in any form, currently exists on the platform (see Formalization scope).

Difficulty

The obvious formalization mistake is to state Proposition 13's conclusion with $\mathrm{dec}_\gamma(F)$ left as an unconstrained free real-number parameter satisfying only the inequality the theorem asserts — a formalization under which the "theorem" would be a triviality about an arbitrary real number, since nothing about the actual min-max game would ever be checked. The chapter's content is precisely the opposite: that this specific minimax quantity can be computed (Proposition 14) or bounded via a concrete strategy (Proposition 17), and — as Chapter 6 shows for a lower bound outside this chunk's scope — that no smaller quantity would do. A second difficulty is proof-theoretic rather than notational: the book's own proof of Proposition 13 bounds regret by an unconstrained supremum over all reference functions $\hat f : \Pi \to \mathbb{R}$, and only identifies this with the official, $\mathrm{co}(F)$-restricted $\mathrm{dec}_\gamma(F)$ of Eq. (4.16) via Proposition 24 — a fact stated on p. 80, outside this chapter's numbered range, whose own proof the book defers to an exercise. A formalization that quietly imports Proposition 24 to close this gap would rest the goal theorem on an unverified fact; this mission instead states the hypothesis the book's own text uses to motivate restricting to $\mathrm{co}(F)$ in the first place (online estimation algorithms produce $\hat f_t \in \mathrm{co}(F)$), so the goal is faithful to what is actually established within the chapter's own pages.

Formalization scope

Every item fixes a finite decision space (Fin A, Fin n, or a generic Fintype S) and states the DEC as the literal sInf-of-sSup transcription of the min-max game (Eqs. (4.15)–(4.16)), never as an opaque bound — this is the trivializing formalization the chunk's own reading of the chapter rules out (see Difficulty). piStar : (S → ℝ) → S is a hypothesized global maximizer selector throughout, constrained to be a genuine argmax only on the function class in scope (F or Set.univ), matching how the book treats $\pi_f$ as a fixed but arbitrary tie-breaking choice. The goal theorem (Proposition 13) adds the explicit hypothesis hfhat : ∀ t, fhat t ∈ convexHull ℝ F, replacing an appeal to the out-of-range Proposition 24 (see Difficulty); this is the one place this mission's statement is not a line-by-line transcription of the book's own displayed proof steps, and it is recorded here and in MODERATION_NOTES.md. Proposition 14's and Proposition 17's $\lesssim$ are replaced by the explicit constants the book's own proofs establish ($(A-1)/(4\gamma)$ exactly, and $(4d+1)/(2\gamma)$ respectively — the latter obtained by summing the three terms the proof of Proposition 17 isolates). Proposition 14's Lean statement splits the book's single equality $\mathrm{dec}_\gamma(F,\hat f) = (A-1)/(4\gamma)$ into an upper bound on the literal decGf, a lower bound restricted to full-support distributions, and IGW's own exact game value, because the book's min over the whole simplex is not provable as a literal Lean equality: a distribution with a zero-weight arm makes the inner supremum genuinely unbounded, and Lean's total Real.sSup returns a junk value smaller than $(A-1)/(4\gamma)$ there (caught in moderation, MODERATION_NOTES.md); the three-conjunct statement recovers exactly the book's real content without asserting that false literal equality. Lemma 9 is restated inside FoundationsRL.Structured rather than imported from the Chapter 2 mission, since draft items across chunks cannot import one another; its source citation still points to its original location (p. 32). Proposition 16 is not drafted: the platform's existing BanditAlgorithm.kiefer_wolfowitz_equivalence (Lattimore & Szepesvári, Theorem 21.1) states the identical existence claim — compact set with full-dimensional span, a design with G-value at most $d$ — as one clause of a larger equivalence, and is reused as a reference item rather than redrafted. Proposition 22 (primal/dual DEC equivalence, §4.4) is deliberately excluded: the book states it "under mild regularity conditions" it does not pin down in the statement itself, which is exactly the kind of unquantified hypothesis this series' faithfulness standard excludes from a goal or milestone. Contributions extending this mission with Chapter 6's lower bound (matching $\mathrm{dec}_\gamma(F)$ from below, establishing tightness) or with a formalization of Proposition 24 itself (removing this mission's hfhat hypothesis) are welcome.

Selected references

• D. Foster, S. Kakade, J. Qian, and A. Rakhlin, The Statistical Complexity of Interactive Decision Making, arXiv:2112.13487, 2021. https://arxiv.org/abs/2112.13487
• D. Foster and A. Rakhlin, Foundations of Reinforcement Learning and Interactive Decision Making, arXiv:2312.16730, 2023. https://arxiv.org/abs/2312.16730
• T. Lattimore and C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020.
• J. Kiefer and J. Wolfowitz, The Equivalence of Two Extremum Problems, Canadian Journal of Mathematics, 1960.

Call $A \subseteq \mathbb{Z}/2^n\mathbb{Z}$ cube-free if no triple $x, y, z$ has all seven of $x$, $y$, $z$, $x+y$, $y+z$, $z+x$, $x+y+z$ inside $A$. The triple is unconstrained, so a degenerate one counts. Write $f(n)$ for the largest size of a cube-free subset.

The conjecture. $f(n) \le \frac{5}{8} 2^n$ for every $n$.

This is Conjecture 5.1 of Jason Long and Adam Zsolt Wagner, The largest projective cube-free subsets of $\mathbb{Z}_{2^n}$, arXiv:1810.01225. It has been open since October 2018, and a 2026 journal paper still names it as conjectured: Yuchen Meng, On Cube-Free Problems, Electron. J. Combin. 33(1) (2026) #P1.16.

The constant is attained

The bound is sharp, and the extremal set is explicit: $A = \{v : v \bmod 8 \in \{1,3,4,5,7\}\}$, the odd residues together with those congruent to 4 mod 8. Its size is $2^{n-1} + 2^{n-3} = \frac{5}{8} 2^n$. In the layer language of Long and Wagner this is $C_3 = L_1 \cup L_3$.

What is known

The conjecture holds for unions of layers. That is Long-Wagner Theorem 1.10 at $d = 3$, and it is the largest class on which the conjectured constant is proved.

For arbitrary sets the best published unconditional bound is $f(n) < \frac{2}{3} 2^n$. Meng calls this bound "quite trivial" and gives it in one paragraph for every cyclic group, so it should not be read as progress toward $5/8$. The residual gap is exactly $\frac{2}{3} - \frac{5}{8} = \frac{1}{24}$, that is $2^n/24$ elements.

Small values are $f(1) = 1$, $f(2) = 2$, $f(3) = 5$, $f(4) = 10$, $f(5) = 20$, $f(6) = 40$, $f(7) = 80$, matching $2^{n-1} + 2^{n-3}$ from $n = 3$ on.

State those values honestly. They come from solver searches, Gurobi in Long and Wagner for $n \le 7$ and an independent SAT reproduction. The SAT half that matters, the unsatisfiability of "a cube-free set of size 81 exists at $n = 7$", is a solver claim with no proof certificate checked and no kernel check behind it. The witness half is verified: a set of exactly 80 elements was produced and re-checked cube-free. So $f(7) \ge 80$ is solid and $f(7) \le 80$ is not certified. Nothing in this mission rests on either.

What the items are

The goal item is the conjecture itself, for $n \ge 4$, and it is open. Every other item is a milestone that is proved mathematics, and the two closed instances $n = 4$ and $n = 5$ are stated separately because they are the only cases of the goal that a proof assistant has actually settled here.

The chain runs: the base case mod 8 by exhaustion, monotonicity under subsets, the bridge between the membership form and the Finset form of the forbidden configuration, sharpness, the odd-residue tight case, the layer-union theorem, the two-thirds bound, and then $n = 4$ and $n = 5$.

Notes on the formalization

Six definitions live in one definition item, Def_Z2nCubeFreeLayers: HasCube, CubeFree, config, ConfigFree, layerIdx and IsLayerUnion. layerIdx is written through the 2-adic valuation rather than through a congruence, because the congruence form leaves $0$ in no layer at all and needs the last layer special-cased.

CubeFree and ConfigFree are two encodings of the same condition and they are not definitionally equal, because config collapses duplicates on a degenerate triple. Their equivalence is a milestone rather than an assumption.

The Lagrange spectrum describes the asymptotic quality of rational approximation to irrational real numbers. The Markov spectrum is defined through minima of indefinite binary quadratic forms. Freiman determined the exact starting point of the maximal half-line contained in each spectrum.

This mission aims to formalize his theorem that this half-line is $[c_F,\infty)$, where

$$c_F=\frac{2221564096+283748\sqrt{462}}{491993569} =4.527829566160879\ldots.$$

The formalization must establish membership of every real number at least $c_F$, including the endpoint, and show that no half-line starting below $c_F$ is contained in either spectrum.

The sources are Freiman's Russian monograph and an accompanying detailed reconstruction of its proof, with an English translation, exact computational certificates, and verification scripts. The project follows Freiman's continued fraction construction, incorporating the corrections and supplementary arguments established in the report.

The intended result is a complete Lean 4 proof. Its scope includes the equivalence of the classical and continued fraction definitions of the spectra, the infinite constructions that realize spectral values, and the exact finite calculations used in the argument.

Source material

• Proof report (PDF) — the complete argument, exact certificate appendices and corrected English translation of Freiman's Russian text. Download PDF.
• Verification package (ZIP) — the report, its LaTeX sources, the Russian source, certificate data, verification programs and reproduction instructions. Download ZIP.

Start with README.md and PROOF_GUIDE.md in the package. The files formalization/MISSION.md and formalization/MILESTONES.md describe the scope and proposed stages of the formalization. For reproducing the report, use the PDF and sources contained in the ZIP.

References to the report in the individual source fields use its printed page numbers.

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

[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

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.

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.

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

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.

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

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