Prove2Me

Get started

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

Combinatorics

630 missions · 350 completed

The mathematics of finite and discrete structures — counting the arrangements of a set, deciding when a configuration meeting prescribed constraints can exist, and characterizing the patterns such structures are forced to contain. It encompasses enumerative and extremal combinatorics, graph theory, design theory, and additive combinatorics, with deep ties to algebra, probability, and computer science.

Missions

Algebraic TopologyDiscrete Geometry·Captain: wurtle

A nine-dimensional counterexample to Borsuk's covering assertionResearch Paper

Motivation

In 1933 Borsuk asked whether every bounded set of positive diameter in Rd\mathbb R^d can be split into d+1d+1 pieces of strictly smaller diameter. The answer is yes in dimensions d≤3d\le3 and for smooth convex bodies, and a regular simplex shows that d+1d+1 pieces may be necessary. Kahn and Kalai showed in 1993 that the answer is no in high dimensions, and since then the question has been: in which dimensions does Borsuk's assertion first fail? The smallest known counterexample dimension measures how far our understanding of diameter partitions extends; it has been reduced from 13251325 to 6363 by combinatorial constructions, while the assertion is open in all dimensions between 44 and the current record.

Timeline

The source of this mission, an OpenAI preprint dated September 23, 2026, claims a counterexample in dimension 99.

Setting

For a bounded set YY of positive diameter, b(Y)b(Y) is the least number of subsets of strictly smaller diameter that cover YY (covers and partitions give the same number). Borsuk's assertion in Rd\mathbb R^d is that b(Y)≤d+1b(Y)\le d+1 for every such Y⊂RdY\subset\mathbb R^d.

Let Sym4(R)\mathrm{Sym}_4(\mathbb R) be the real symmetric 4×44\times4 matrices with the Frobenius norm ∥A∥F2=tr⁡(A2)=∑i,jAij2\|A\|_F^2=\operatorname{tr}(A^2)=\sum_{i,j}A_{ij}^2. The trace-one hyperplane {tr⁡A=1}\{\operatorname{tr}A=1\} in Sym4(R)\mathrm{Sym}_4(\mathbb R) is a 99-dimensional affine Euclidean space. For a unit vector u∈R4u\in\mathbb R^4, uuTuu^{\mathsf T} is the orthogonal projector onto the line Ru\mathbb Ru. Two such projectors are at distance 2\sqrt2 exactly when the lines are orthogonal.

Formalization targets

Goal: Theorem 1.1

The set

X={uuT:u∈R4, ∥u∥=1}⊂{A∈Sym4(R):tr⁡A=1}X=\{uu^{\mathsf T}:u\in\mathbb R^4,\ \|u\|=1\}\subset\{A\in\mathrm{Sym}_4(\mathbb R):\operatorname{tr}A=1\}

is compact, has Frobenius diameter 2\sqrt2, and cannot be covered by ten subsets of diameter strictly less than 2\sqrt2. Hence b(X)≥11>9+1b(X)\ge11>9+1 and Borsuk's assertion fails in dimension 99. The Lean statement OAI.BorsukNine.main_theorem is open on the platform.

Significance

The theorem lowers the smallest known counterexample dimension for Borsuk's conjecture from 6363 to 99, and the paper extends it to compact counterexamples in every dimension d≥9d\ge9 (Corollary 7.1). Unlike previous counterexamples, which are finite point sets built from codes or strongly regular graphs, the witness is a continuum: the image of real projective 33-space under the projector embedding. The theorem does not determine the smallest failing dimension (the assertion remains undecided in dimensions 44 to 88) or the exact value of b(X)b(X).

The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. A formal proof would combine metric geometry, an algebraic-topological degree argument and a finite combinatorial obstruction.

Difficulty

Previous counterexamples use finite sets where a counting argument (Frankl–Wilson type) forces many parts; such counting gives nothing for a 99-dimensional continuum. For XX, a cover by ten small sets corresponds to ten nonnegative functions on RP3\mathbb{RP}^3 summing to one, with orthogonal lines never sharing a positive coordinate. One would like to use the minimal number of vertices of a triangulation of RP3\mathbb{RP}^3 (Walkup: eleven), but the positive-support complex arising from such functions is not a triangulation, so its face structure has to be derived from the map itself.

Formalization scope

  • Vectors are EuclideanSpace ℝ (Fin 4); matrices are EuclideanSpace ℝ (Fin 4 × Fin 4), whose norm is the Frobenius norm. projector u has entries uiuju_iu_j.
  • projectorSet is the image of the unit sphere; traceOneSymmetric is the set of symmetric matrices of trace 11.
  • HasTenSmallCover: ten subsets of projectorSet covering it, each with Metric.diam < √2. Requiring the pieces to lie in XX loses no generality, and keeps Metric.diam away from its default value for unbounded sets.
  • The goal is the conjunction: IsCompact projectorSet, containment in traceOneSymmetric, Metric.diam projectorSet = √2, and ¬ HasTenSmallCover.

A complete development needs partitions of unity, mod-two degree of odd maps on spheres, local preimage counting, and a finite combinatorial case analysis on labelled supports. The finite combinatorial part (Sections 5–6) and Lemma 2.4 (reduction to strict gaps) are self-contained and welcome first contributions.

Selected references

2 thms1 active userReviewed
Complexity TheoryTheoretical Computer Science·Captain: wurtle

A Polynomial-Time 2-Approximation for Shortest Common SuperstringResearch Paper

Motivation: approximating the shortest common superstring

Given a finite collection S\mathcal S of strings, the shortest common superstring (SCS) problem asks for a shortest string TT that contains every member of S\mathcal S as a contiguous substring. It is a basic model of sequence assembly (reconstructing a long DNA sequence from overlapping fragments) and of data compression, and it is a standard test problem for approximation algorithms. Computing the optimum exactly is hard — Blum, Jiang, Li, Tromp and Yannakakis showed the problem is MAX SNP-hard, so it has no polynomial-time approximation scheme unless P = NP (Blum et al., J. ACM 1994) — so the natural question is the best constant factor achievable in polynomial time. For decades the target has been factor 22: the classical Greedy conjecture asserts that repeatedly merging the pair with maximum overlap achieves it.

Timeline

  • 1988 — Tarhio and Ukkonen propose the factor-22 conjecture for the maximum-overlap Greedy procedure (Theor. Comput. Sci. 1988).
  • 1994 — Blum, Jiang, Li, Tromp and Yannakakis give the first constant-factor algorithm a polynomial-time 33-approximation (J. ACM 1994).
  • 1997 — Breslauer, Jiang and Jiang use rotations of periodic strings to control overlaps (J. Algorithms 1997).
  • 1999 — Sweedyk obtains factor 5/25/2 (SIAM J. Comput. 1999).
  • 2013 — Mucha obtains 2+11/232+11/23 via Lyndon words (SODA 2013).
  • 2019/2020 — Golovnev, Kulikov, Logunov, Mihajlin and Nikolaev introduce the all-substrings hierarchical graph and the Collapsing conjecture (APPROX/RANDOM 2019; arXiv:1809.08669).
  • 2023 — Englert, Matsakis and Veselý obtain (14+67)/9<2.466(14+\sqrt{67})/9<2.466 (ISAAC 2023).
  • 2026 — Chukhin, Kulikov, Mihajlin and Smal report a 7/37/3-approximation (ECCC TR26-157); Shibata reports a counterexample to the Greedy conjecture with ratio at least 9/49/4 (arXiv:2609.01365).
  • 2026 — An OpenAI preprint, A Polynomial-Time 2-Approximation for Shortest Common Superstring (OpenAI Math Release, September 24, 2026), claims a deterministic polynomial-time algorithm with ratio 22. The preprint has not been peer reviewed and its theorem is not formally verified.

Setting

A string is a finite list of symbols; a string ss is a substring of TT if T=usvT=usv for some strings u,vu,v (the empty string is a substring of everything). For a finite list S\mathcal S of strings, a common superstring is a string TT having every s∈Ss\in\mathcal S as a substring, and

OPT(S)=min⁡{∣T∣:T is a common superstring of S},\mathrm{OPT}(\mathcal S)=\min\{|T| : T \text{ is a common superstring of }\mathcal S\},

where ∣T∣|T| counts symbols. The alphabet is unbounded: each symbol is given by an explicit binary label, and the input is measured by its total encoded bit length NN. An algorithm runs in polynomial time if its running time on a bit-level machine is bounded by a polynomial in NN.

In Lean (namespace OAI.Superstring), a symbol is List Bool, a word is a list of symbols, and an instance is a list of words. Substring containment is Mathlib's infix relation <:+:, opt S is the infimum of lengths of common superstrings, and HasPolynomialImplementation f asks for a Mathlib Turing.TM2ComputableInPolyTime certificate for f with respect to an explicit self-delimiting binary encoding of instances and outputs, with every stack alphabet finite.

Formalization targets

Goal: a polynomial-time 2-approximation (Theorem 1.1)

There is a function ff from instances to words, computable in polynomial time in the encoded input length, such that for every instance S\mathcal S

f(S) is a common superstring of Sand∣f(S)∣≤2 OPT(S).f(\mathcal S)\ \text{is a common superstring of } \mathcal S\qquad\text{and}\qquad |f(\mathcal S)|\le 2\,\mathrm{OPT}(\mathcal S).

The goal is published on the platform with status Open.

Significance

The result itself. Factor 22 has been the conjectured benchmark for SCS since 1988, and the best proved polynomial-time ratio before this preprint was 7/37/3 (reported in 2026). Theorem 1.1 reaches factor 22 with a new algorithm rather than with Greedy, which a 2026 preprint reports does not achieve factor 22.

Formalizing it. The statement mixes three components that are each easy to get subtly wrong on paper: the correctness of the output (contiguous coverage of every input), the ratio against the unrestricted optimum, and a running-time bound measured in bits, with symbols of arbitrary label length. The formal statement pins down all three with an explicit machine model. A complete formalization requires both the combinatorial ratio proof and a verified polynomial-time implementation on Mathlib's stack-machine model, which is substantial reusable infrastructure for complexity statements in Lean.

Difficulty

The classical approach builds the overlap (distance) graph, takes a minimum-weight cycle cover as a lower bound, and then opens and concatenates the cycles; the cost of joining cycles is what has kept ratios above 22. Greedy, the natural candidate for factor 22, is reported to fail. Any factor-22 algorithm needs a lower bound on OPT\mathrm{OPT} that is tight enough that the cost of connecting all the pieces can be charged to the lower bound a second time without double-counting, uniformly over periodic and highly repetitive inputs. The polynomial running time must also be established at the bit level, with symbols of unbounded encoded length.

Formalization scope

  • Instances are List (List (List Bool)): duplicates and empty strings are allowed, and symbols are arbitrary bit lists, so the alphabet is unbounded.
  • Coverage is contiguous substring containment (List.IsInfix), not subsequence containment.
  • opt is a natural-number sInf; the set is nonempty because the concatenation of all inputs is a common superstring, so the junk value is never used. The ratio is measured in symbols.
  • Polynomial time uses Mathlib's Turing.TM2ComputableInPolyTime for the encodings encodeInstance and encodeWord (prefix markers for list structure), together with finiteness of every stack alphabet, so the time bound is in input bits on a finite-alphabet machine. A function that is merely computable, or polynomial only in the number of symbols, does not satisfy the goal.
  • Needed infrastructure: the all-substrings graph and Euler tours, periodicity lemmas (Fine–Wilf), and a verified implementation on Mathlib's TM2 model. Contributions of reusable TM2 programming libraries are welcome.

Selected references

2 thms1 active userReviewed
Markov ChainTheoretical Computer Science·Captain: wurtle

An FPRAS for Cell-Bounded Contingency TablesResearch Paper

Motivation

A cell-bounded contingency table is a nonnegative integer matrix with prescribed row sums, column sums and an upper bound on each entry. Bounds of zero forbid entries (structural zeros), and bounds of one give bipartite graphs with prescribed degrees, so the model contains degree-constrained subgraph counting and perfect matchings (the permanent). Counting such tables is central to exact conditional inference in statistics and is equivalent to counting integer flows in bipartite networks. Exact counting is #P-complete even for two-row ordinary tables (Dyer, Kannan and Mount, 1997), so the target is a fully polynomial randomized approximation scheme (FPRAS): a randomized algorithm that, for any ε,δ∈(0,1)\varepsilon,\delta\in(0,1), returns a (1±ε)(1\pm\varepsilon)-approximation with probability at least 1−δ1-\delta in time polynomial in the input length, 1/ε1/\varepsilon and log⁡(1/δ)\log(1/\delta).

Timeline

  • 1986. Jerrum, Valiant and Vazirani relate approximate counting and sampling through self-reducibility.
  • 1995. Diaconis and Gangolli survey fixed-margin arrays (doi:10.1007/978-1-4612-0801-3_3).
  • 1997. Dyer, Kannan and Mount prove #P-completeness for two-row tables and give geometric methods for large margins; Morris improves the margin requirements in 2002 (doi:10.1002/rsa.10049).
  • 2000–2003. Dyer and Greenhill (two rows), Cryan and Dyer (fixed number of rows), Dyer (dynamic programming) give approximate counting for a bounded number of rows.
  • 2004. Jerrum, Sinclair and Vigoda's permanent algorithm yields an FPRAS for all 0/1 caps (doi:10.1145/1008731.1008738).
  • 2009–2010. Barvinok bounds weighted table counts within NO(m+n)N^{O(m+n)} (doi:10.1093/imrn/rnn133); Barvinok, Luria, Samorodnitsky and Yong give quasipolynomial randomized approximations for smooth margins (doi:10.1002/rsa.20301).
  • 2010. Cryan, Dyer and Randall give an FPRAS for integral flows with large tight capacities and for cell-bounded tables with a fixed number of rows, and list unrestricted approximation as open (doi:10.1137/060650544).
  • 2023. Brändén, Leake and Pak give capacity lower bounds via Lorentzian polynomials (doi:10.1007/s11856-022-2364-9); Guo and Jerrum count vertices of certain 0/1 polytopes (doi:10.1007/s00454-022-00406-8).

The source of this mission, an OpenAI preprint dated September 24, 2026, claims an FPRAS with no restriction on dimensions, margins or caps.

Setting

For positive integers m,nm,n, margins r∈Z≥0mr\in\mathbb Z_{\ge0}^m, c∈Z≥0nc\in\mathbb Z_{\ge0}^n with equal totals, and bounds b∈Z≥0m×nb\in\mathbb Z_{\ge0}^{m\times n},

Ω(r,c,b)={X∈Z≥0m×n: ∑jXij=ri, ∑iXij=cj, Xij≤bij},Z(r,c,b)=∣Ω(r,c,b)∣.\Omega(r,c,b)=\Bigl\{X\in\mathbb Z_{\ge0}^{m\times n}:\ \textstyle\sum_jX_{ij}=r_i,\ \sum_iX_{ij}=c_j,\ X_{ij}\le b_{ij}\Bigr\},\qquad Z(r,c,b)=|\Omega(r,c,b)|.

All numbers are written in binary, so a capacity can be exponentially larger than its description. LL denotes the total binary input length including the rational accuracy parameters ε,δ\varepsilon,\delta. The algorithm uses independent unbiased random bits and is charged for every bit operation.

Formalization targets

Goal: Theorem 1.1 (FPRAS)

One randomized algorithm, given (r,c,b)(r,c,b) and rational ε,δ∈(0,1)\varepsilon,\delta\in(0,1), outputs a nonnegative rational Z^\widehat Z with

Pr⁡[(1−ε)Z(r,c,b)≤Z^≤(1+ε)Z(r,c,b)]≥1−δ,\Pr\bigl[(1-\varepsilon)Z(r,c,b)\le\widehat Z\le(1+\varepsilon)Z(r,c,b)\bigr]\ge1-\delta,

outputs exactly 00 on every execution when Ω(r,c,b)=∅\Omega(r,c,b)=\emptyset, and performs at most poly(L,ε−1,log⁡δ−1)\mathrm{poly}(L,\varepsilon^{-1},\log\delta^{-1}) bit operations on every execution. Lean: OAI.ContingencyTables.counting, open on the platform.

Significance

The theorem would answer the question left open by Cryan, Dyer and Randall in 2010: approximate counting of cell-bounded tables (equivalently, integral flows in bipartite networks with arbitrary capacities) without any fixed-dimension, large-capacity, density or balance assumption, with polynomial cost on every execution and no oracle. It contains the 0/1 case handled by Jerrum–Sinclair–Vigoda and the fixed-row results as special cases, and via self-reduction it gives approximate samplers for integer flows. A companion preprint of the same family treats exact uniform sampling of uncapped tables. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.

Difficulty

Two regimes clash. Large capacities cannot be expanded into that many binary choices without exponential blow-up, so geometric (polytope volume) methods are needed for them; but those methods require every cell to be large. Small capacities need combinatorial Markov chains, which in turn must preserve exactly one unit of mass per table despite the multiplicities created by encoding a bounded integer by binary choices. Arbitrary mixtures of tiny and huge caps, zero caps and variable dimensions defeat each approach used alone.

Formalization scope

  • Algorithms are MatchingFPRAS.RandomMachines: a single finite transition table on an 8-symbol alphabet, one random bit per tick; time is counted in ticks (polynomially equivalent to bit operations).
  • Inputs are delimited binary encodings of m,n,r,c,bm,n,r,c,b and of ε,δ\varepsilon,\delta as reduced fractions (encodeCountingInput); outputs are encoded rationals.
  • count r c b is Fintype.card of bounded tables.
  • CountingStatement: one machine and constants C>0C>0, dd; with t=C(∣input∣+⌈1/ε⌉+⌈log⁡2⌈1/δ⌉⌉+1)dt=C(|\text{input}|+\lceil1/\varepsilon\rceil+\lceil\log_2\lceil1/\delta\rceil\rceil+1)^d, every tape of length tt halts with a rational q≥0q\ge0; if count = 0 every tape outputs 00; and the fraction of tapes with (1−ε)Z≤q≤(1+ε)Z(1-\varepsilon)Z\le q\le(1+\varepsilon)Z is at least 1−δ1-\delta.
  • m,n≥1m,n\ge1 and equal margin totals are hypotheses, as in the paper.

Needed infrastructure: randomized Turing machines, Markov chain mixing and Poincaré inequalities, log-concavity (Prékopa–Leindler), and network-flow feasibility. The machine model and encodings are shared with the exact-sampling mission of this family. Contributions formalizing Proposition 2.2 (contamination bound), Lemma 3.3 (log-concave tree marginals), Proposition 6.1 (weight evaluation) or Proposition 7.2 are welcome.

Selected references

2 thms1 active userReviewed
Markov ChainTheoretical Computer Science·Captain: wurtle

Exact Uniform Sampling of Contingency Tables with Arbitrary MarginsResearch Paper

Motivation

A contingency table with margins r=(r1,…,rm)r=(r_1,\dots,r_m) and c=(c1,…,cn)c=(c_1,\dots,c_n) is a nonnegative integer matrix whose row sums are rr and column sums are cc. Such tables are the basic objects of categorical data analysis: conditional tests of independence (Fisher's exact test and its generalizations) compare an observed table with the uniform distribution on all tables with the same margins, and in practice this requires sampling uniformly from that set. The set is finite but can be exponentially large in the input size when margins are written in binary. Whether one can sample it (approximately or exactly) in time polynomial in both dimensions and in the bit length of the margins has been open since the 1990s.

Timeline

  • 1995. Diaconis and Gangolli survey enumeration and random generation of rectangular arrays with fixed margins (doi:10.1007/978-1-4612-0801-3_3).
  • 1997–2002. Dyer, Kannan and Mount sample dense tables via the transportation polytope; Morris improves the dense bounds (doi:10.1002/rsa.10049).
  • 2000. Dyer and Greenhill give polynomial-time approximate counting and sampling for two-rowed tables.
  • 2003. Kijima and Matsui give exact sampling for two rows by coupling from the past; Cryan and Dyer approximately count for a fixed number of rows (doi:10.1016/S0022-0000(03)00014-X); Dyer gives an exact dynamic-programming sampler for fixed row count.
  • 2006. Cryan, Dyer, Goldberg, Jerrum and Martin prove rapid mixing of the heat-bath chain for every fixed number of rows (doi:10.1137/S0097539703434243).
  • 2016. DeSalvo and Zhao give an exact divide-and-conquer sampler whose polynomial runtime is conditional on a conjecture (arXiv:1507.00070).
  • 2021. Arman, Gao and Wormald give linear-time exact generation for sparse margins with 5Δ4<N5\Delta^4<N, and report that no polynomial-time approximately uniform sampler for arbitrary margins was known (arXiv:2104.09413).
  • 2024. Göbel, Liu, Manurangsi and Pappik turn sufficiently accurate samplers into perfect samplers (arXiv:2410.00882).

The source of this mission, an OpenAI preprint dated September 24, 2026, claims both an almost-uniform and an exactly uniform sampler for arbitrary margins.

Setting

For nonnegative integer vectors r∈Z≥0mr\in\mathbb Z_{\ge0}^m, c∈Z≥0nc\in\mathbb Z_{\ge0}^n with common total N=∑iri=∑jcjN=\sum_ir_i=\sum_jc_j, let

Ω(r,c)={X∈Z≥0m×n: ∑jXij=ri, ∑iXij=cj}.\Omega(r,c)=\Bigl\{X\in\mathbb Z_{\ge0}^{m\times n}:\ \textstyle\sum_jX_{ij}=r_i,\ \sum_iX_{ij}=c_j\Bigr\}.

The input is (m,n,r,c)(m,n,r,c) with margins in binary, so its length is polynomial in mm, nn and log⁡(N+1)\log(N+1). An algorithm uses unbiased random bits. For laws on a finite set, TV(μ,ν)=12∑x∣μ(x)−ν(x)∣\mathrm{TV}(\mu,\nu)=\tfrac12\sum_x|\mu(x)-\nu(x)|.

Formalization targets

Milestone: Theorem 1.1(i) (almost-uniform, bounded time)

For each k≥1k\ge1, an algorithm halts on every execution in time poly(m,n,log⁡(N+1),k)\mathrm{poly}(m,n,\log(N+1),k) and outputs X∈Ω(r,c)X\in\Omega(r,c) with

TV(law(X), Unif Ω(r,c))≤2−k.\mathrm{TV}\bigl(\mathrm{law}(X),\ \mathrm{Unif}\,\Omega(r,c)\bigr)\le2^{-k}.

Goal: Theorem 1.1(ii) (exact uniform sampling)

An algorithm outputs X∈Ω(r,c)X\in\Omega(r,c) with

Pr⁡[X=Y]=1∣Ω(r,c)∣(Y∈Ω(r,c)),\Pr[X=Y]=\frac1{|\Omega(r,c)|}\quad(Y\in\Omega(r,c)),

terminates almost surely, and has expected running time poly(m,n,log⁡(N+1))\mathrm{poly}(m,n,\log(N+1)), with polynomials uniform over all margins. Lean: OAI.ContingencyTables.exactSampling, open on the platform.

Significance

The theorem would give the first unconditional polynomial-time exact uniform sampler for contingency tables with arbitrary dimensions and binary margins, with no positivity, sparsity, balance or fixed-dimension restriction, and with all random bits and integer arithmetic counted. It removes the fixed-row restriction of the Dyer–Greenhill and Cryan–Dyer line and the sparsity condition of Arman–Gao–Wormald. The exponents are deliberately large; the contribution is the existence of a polynomial algorithm. Exact time is polynomial in expectation, not on every run. A companion preprint of the same family gives an FPRAS for counting tables with cell bounds. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.

Difficulty

Markov-chain approaches mix rapidly for a fixed number of rows, but the bounds degrade with the row count. Geometric (polytope) methods need all margins to be large, and fail when some margins are tiny while others are huge, which is exactly the mixed regime that arbitrary binary margins allow. Making the sampler exact rather than approximate adds a separate difficulty: the residual-mixture correction requires that the actual output law of the approximate sampler can be computed, with cost polynomial in the accuracy bits.

Formalization scope

  • Algorithms are MatchingFPRAS.RandomMachines: a single finite transition table over an 8-symbol tape alphabet; each tick reads one random bit and either moves, writes or halts. Time is counted in ticks, polynomially equivalent to bit operations.
  • Inputs are binary encodings with delimiters (encodeNat, encodeMargins); outputs are row-major matrix encodings left on the tape (OutputsTable).
  • tableMass A input t X and haltMass A input t are the fractions of the 2t2^t random tapes of length tt that halt with output XX, respectively halt at all, within tt ticks.
  • ExactSamplingStatement: one machine and constants C>0C>0, dd such that for all m,n,r,cm,n,r,c with equal totals: every halted output is in Ω(r,c)\Omega(r,c); tableMass → 1/|Ω| for each table; haltMass → 1; and ∑t(1−haltMasst)\sum_t(1-\text{haltMass}_t), the expected running time, is at most C(m+n+⌈log⁡2(N+1)⌉+1)dC(m+n+\lceil\log_2(N+1)\rceil+1)^d.
  • BoundedSamplingStatement: every tape of length t=C(m+n+⌈log⁡2(N+1)⌉+k+1)dt=C(m+n+\lceil\log_2(N+1)\rceil+k+1)^d halts with a feasible table, and the TV distance to uniform is at most 2−k2^{-k}.
  • Dimensions m,nm,n vary freely (zero allowed); the machine is uniform, not one per size.

Needed infrastructure: randomized Turing machines and their output laws, Markov chain mixing (conductance, Poincaré inequalities), and log-concave sampling. Contributions formalizing Theorem 4.3 (graph Poincaré inequality), Theorem 5.1 (dense completion draw), Proposition 6.3 (law tabulation) or the Göbel–Liu–Manurangsi–Pappik correction are welcome.

Selected references

3 thms1 active userReviewed
Markov ChainTheoretical Computer Science·Captain: wurtle

Approximate counting of common bases of two matroidsResearch Paper

Motivation: counting common bases of two matroids

A matroid abstracts linear independence: a finite ground set with a family of "independent" subsets that is closed under subsets and satisfies the augmentation axiom. Its maximal independent sets, the bases, all have the same size, the rank. Matroid intersection, finding a common basis of two matroids, is one of the central polynomially solvable problems of combinatorial optimization (Edmonds, 1979). Counting common bases is much harder. It contains counting bases of a single matroid (take both matroids equal) and counting perfect matchings of a bipartite graph (take two partition matroids), and exact counting is #P-hard. The natural goal is therefore a fully polynomial randomized approximation scheme (FPRAS): an algorithm whose output is within relative error ϵ\epsilon with probability at least 1−δ1-\delta, in time polynomial in the input size, ϵ−1\epsilon^{-1} and log⁡δ−1\log\delta^{-1}. The matroids should be accessible only through independence oracles.

Background and timeline

  • 1979 — Edmonds gives a polynomial-time algorithm for matroid intersection (Ann. Discrete Math. 4).
  • 1992 — Feder and Mihail give sampling and approximate counting for balanced matroids (STOC 1992).
  • 2004 — Jerrum, Sinclair and Vigoda give an FPRAS for the permanent of nonnegative matrices, covering bipartite perfect matchings (J. ACM 51).
  • 2007 — Barvinok and Samorodnitsky obtain coarse logarithmic estimates via random weighting (Israel J. Math. 158).
  • 2016–2017 — Anari, Oveis Gharan and Rezaei prove rapid mixing for strongly Rayleigh distributions (COLT 2016); Anari and Oveis Gharan obtain exponential-factor approximations from real-stable polynomials (arXiv:1702.02937).
  • 2020 — Brändén and Huh develop Lorentzian polynomials (Ann. of Math. 192).
  • 2021 — Anari, Oveis Gharan and Vinzant give a deterministic 2O(r)2^{O(r)}-factor approximation for common bases of rank-rr matroids (Duke Math. J. 170); Cryan, Guo and Mousa ask for a rapidly mixing chain for common bases (Ann. Probab. 49).
  • 2023–2024 — Liu's dissertation records the FPRAS question for two arbitrary oracle matroids (Section 13.2, Problem 1, thesis); Anari, Liu, Oveis Gharan and Vinzant give an FPRAS for bases of a single matroid (Ann. of Math. 199).
  • 2026 — An OpenAI preprint, Approximate counting of common bases of two matroids (OpenAI Math Release, September 23, 2026), claims an independence-oracle FPRAS for common bases of two arbitrary matroids of equal rank. It has not been peer reviewed, and its proof is not formally verified.

Setting

Let M1,M2M_1,M_2 be matroids of the same rank rr on the ground set [n][n], supplied by exact independence oracles: a query is an nn-bit indicator of a subset, and the answer says whether it is independent. The quantity to estimate is

Z(M1,M2)=∣B(M1)∩B(M2)∣,Z(M_1,M_2)=\bigl|\mathcal B(M_1)\cap\mathcal B(M_2)\bigr|,

the number of common bases. The input also contains rationals ϵ,δ∈(0,1)\epsilon,\delta\in(0,1); ℓ\ell denotes the binary encoding length of n,r,ϵ,δn,r,\epsilon,\delta. Oracle calls are counted separately from the bit operations used to build queries and process answers.

Formalization targets

Goal: an FPRAS for common bases in the independence-oracle model (Theorem 1.1)

There is a single randomized oracle algorithm and a fixed polynomial pp such that, for all rank-rr matroids M1,M2M_1,M_2 on [n][n] and rational ϵ,δ∈(0,1)\epsilon,\delta\in(0,1), it outputs a nonnegative rational Z^\widehat Z with

Pr⁡[(1−ϵ)Z≤Z^≤(1+ϵ)Z] ≥ 1−δ,\Pr\bigl[(1-\epsilon)Z\le\widehat Z\le(1+\epsilon)Z\bigr]\ \ge\ 1-\delta,

the output is always 00 when Z=0Z=0, and on every execution the numbers of oracle calls and bit operations are at most p(n,ℓ,ϵ−1,log⁡δ−1)p(n,\ell,\epsilon^{-1},\log\delta^{-1}). The algorithm uses only independent fair random bits. The goal statement is published on the platform with status Open.

Significance

The result itself. Theorem 1.1 answers the question recorded by Liu (2023) and extends both the single-matroid FPRAS of Anari–Liu–Oveis Gharan–Vinzant and, in the bipartite-matching case, the permanent FPRAS of Jerrum–Sinclair–Vigoda. It needs no representation of either matroid and holds for unrestricted rank, whereas the previous oracle-model scheme was fully polynomial only for r=O(log⁡n)r=O(\log n). The source derives FPRASs and almost-uniform samplers for common independent sets of prescribed, unrestricted or maximum size, even for matroids of different ranks (Corollary 9.1).

Formalizing it. The Lean goal fixes a concrete machine model, so it states a complete complexity-theoretic claim with no informal "polynomial-time" left. A proof would combine Lorentzian-polynomial inequalities (Brändén–Huh), a transport inequality, a Markov-chain Poincaré bound, and simulated annealing with explicit bit accounting. Each layer is reusable: Mathlib has matroids, but no Lorentzian polynomials, no mixing-time theory of this kind and no randomized-algorithm framework.

Difficulty

For one matroid, the bases-exchange walk mixes rapidly because the basis generating polynomial is log-concave. The intersection of two matroids has no such structure: its common bases need not be connected by short exchanges, and the natural chain on transversals of the paired construction passes through states of exponentially small weight, so positivity and connectivity alone give no polynomial bound. Earlier approaches either lost exponential factors or needed real-stable polynomials that an independence oracle does not provide. The proof must balance defect classes, as in Jerrum–Sinclair–Vigoda, and establish a Poincaré inequality for observables from matroid-theoretic inequalities alone.

Formalization scope

  • Matroids are Mathlib Matroid (Fin n) with ground set univ and eRank = r for both. Oracles are functions Bool → (Fin n → Bool) → Bool, required to answer independence queries exactly.
  • The algorithm is one fixed Program k s for a register machine with k+8k+8 binary stacks: push/pop, fair coin, oracle query on an nn-bit register, and halt with output (register 6)/(register 7) as a rational. Inputs n,r,ϵ,δn,r,\epsilon,\delta are loaded in binary.
  • The resource bound is B=C(1+n+ℓ+⌈ϵ−1⌉+⌈log⁡2⌈δ−1⌉⌉)dB=C(1+n+\ell+\lceil\epsilon^{-1}\rceil+\lceil\log_2\lceil\delta^{-1}\rceil\rceil)^d with constants C>0,dC>0,d fixed before the instance. For every infinite bit stream, the run halts within BB steps with at most BB oracle calls and BB bit operations, outputs a nonnegative rational, and outputs 00 when Z=0Z=0.
  • The success probability is expressed by counting: at least (1−δ)2B(1-\delta)2^B of the 2B2^B bit strings of length BB lead to an output within relative error ϵ\epsilon of ZZ.
  • A trivializing reading is excluded: the program and constants come first and must work for every n,rn,r, matroid pair, oracle and ϵ,δ\epsilon,\delta.
  • Needed infrastructure: Lorentzian polynomials and the homogeneous Tutte inequalities, Markov chains on finite state spaces with Poincaré/variance bounds, annealing estimators, and correctness proofs for the register machine. Contributions on any layer are welcome.

Selected references

2 thms1 active userReviewed
Information TheoryTheoretical Computer Science·Captain: wurtle

Entropy and Face Dimension of the Perfect-Matching PolytopeResearch Paper

Motivation: how much randomness fits under prescribed edge probabilities?

Prescribing the probability xex_e that each edge belongs to a random perfect matching does not determine the distribution of the whole matching. The largest entropy compatible with those edge probabilities, H(x)H(x), measures how many matching choices can coexist with them, and it links three topics: lower bounds on the number of perfect matchings, convex-optimization approaches to approximate counting, and the facial geometry of the perfect-matching polytope. For bipartite graphs, Schrijver's permanent inequality (Schrijver 1998) and Gurvits' weighted Bethe inequality (Gurvits 2011) give the clean comparison H≥F−BH\ge F-B between HH and sums of one-coordinate entropies. For general graphs, odd cuts make such comparisons harder, and Anari, Oveis Gharan and Vinzant (2018) asked (FOCS version, Conjecture 6) whether the maximum binary-coordinate entropy over the polytope exceeds log⁡N(G)\log N(G) by only a linear function of the number of vertices.

Timeline

  • 1965 — Edmonds describes the perfect-matching polytope by degree equations, nonnegativity and odd-cut inequalities (Edmonds 1965).
  • 1982 — Naddef (Math. Program. 1982) and Edmonds, Pulleyblank and Lovász (Combinatorica 1982) determine the dimension of the perfect-matching polytope.
  • 1986 — Chung, Graham, Frankl and Shearer: Shearer's entropy inequality (JCTA 1986), which gives H≤FH\le F.
  • 1998–2011 — Schrijver's lower bound for regular bipartite graphs and Gurvits' Bethe-approximation form give H≥F−BH\ge F-B in the bipartite case.
  • 2011 — Esperet, Kardoš, King, Král' and Norine: exponentially many perfect matchings in bridgeless cubic graphs (Adv. Math. 2011).
  • 2018 — Anari, Oveis Gharan and Vinzant propose the entropy framework and the linear-error question (FOCS 2018).
  • 2022 — Ebrahimnejad, Nagda and Oveis Gharan count perfect matchings in regular expanding nonbipartite graphs (ITCS 2022).
  • 2026 — Abdi, Cornuéjols, Dadush and Dalirrooyfard bound the rank of tight odd cuts by 3m−13m-1 and give exponential lower counts for regular graphs of degree at least four with an odd-cut condition (Proc. LMS 2026). An OpenAI preprint, Entropy and Face Dimension of the Perfect-Matching Polytope (OpenAI Math Release, September 23, 2026), claims the pointwise bound F−(2−2/m)B≤H≤FF-(2-2/m)B\le H\le F and a positive answer to the Anari–Oveis Gharan–Vinzant question. The preprint has not been peer reviewed, and its main theorem is not formally verified.

Setting

Let GG be a finite loopless multigraph with vertex set VV, ∣V∣=2m≥2|V|=2m\ge2, and edge set EE (parallel edges are distinct coordinates). A perfect matching is a set of edges covering each vertex exactly once; M(G)\mathcal M(G) is the set of them and N(G)=∣M(G)∣N(G)=|\mathcal M(G)|. The perfect-matching polytope is

P(G)=conv⁡{1M:M∈M(G)}⊆RE.P(G)=\operatorname{conv}\{\mathbf 1_M: M\in\mathcal M(G)\}\subseteq\mathbb R^E .

For x∈P(G)x\in P(G) put, with natural logarithms and 0log⁡0=00\log 0=0,

H(x)=max⁡{−∑MpMlog⁡pM: p a probability law on M(G), ∑MpM1M=x},H(x)=\max\Big\{-\sum_M p_M\log p_M:\ p\text{ a probability law on }\mathcal M(G),\ \sum_M p_M\mathbf 1_M=x\Big\}, F(x)=−∑exelog⁡xe,B(x)=−∑e(1−xe)log⁡(1−xe).F(x)=-\sum_{e}x_e\log x_e,\qquad B(x)=-\sum_e(1-x_e)\log(1-x_e).

Formalization targets

The milestones are listed in attack order: the face of a triangle expansion (Lemma 5.1), the coefficient-eight nonlinear bound (Theorem B.1), deterministic approximate counting (Theorem 1.2) and its singleton-loop variant (Proposition C.1).

Goal: Theorem 1.1 (pointwise entropy bounds)

If GG has at least one perfect matching, then for every x∈P(G)x\in P(G)

F(x)−(2−2m)B(x)  ≤  H(x)  ≤  F(x).F(x)-\Big(2-\frac 2m\Big)B(x)\;\le\;H(x)\;\le\;F(x).

The bound holds on the whole polytope, boundary included. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The upper bound is Shearer's inequality; the content is the lower comparison with coefficient 2−2/m2-2/m, valid in nonbipartite graphs where the bipartite coefficient 11 fails (the source gives an eight-vertex counterexample, and Corollary 5.3 shows any universal coefficient is at least ln⁡3/(2ln⁡(3/2))\ln3/(2\ln(3/2))). Optimizing over xx gives log⁡N(G)≤max⁡P(G)(F+B)≤log⁡N(G)+3m−2\log N(G)\le\max_{P(G)}(F+B)\le\log N(G)+3m-2, answering the Anari–Oveis Gharan–Vinzant question. Plugging in uniform marginals gives N(G)≥e−2(m−1)kmN(G)\ge e^{-2(m-1)}k^m for graphs with kk edge-disjoint perfect matchings, and for kk-regular graphs whose odd cuts all have at least kk edges. The same entropy framework yields a deterministic polynomial-time algorithm approximating N(G)N(G) within a factor 512n512^n for graphs with binary edge multiplicities (Theorem 1.2).

Formalizing it. The goal is a finite-dimensional inequality about polytopes and entropies, accessible to Mathlib's convexity and analysis libraries. The milestones extend the mission to a certified polynomial-time counting algorithm in Mathlib's Turing-machine model, a rare example of a formally specified approximation algorithm for a #P-hard quantity.

Difficulty

Shearer's inequality gives the upper bound in one line, and in bipartite graphs the lower bound follows from permanent inequalities that have no analogue for general graphs. A direct convexity argument fails because HH is not differentiable across faces of P(G)P(G): at a boundary mean the maximum-entropy law lives on a lower-dimensional face, and its covariance is singular in the ambient edge space. The lower bound must therefore be proved face by face, and it needs the sharp geometric estimate ∣supp⁡x∣−dim⁡Fx≤3m−2|\operatorname{supp}x|-\dim F_x\le 3m-2 for the minimal face FxF_x containing xx; the earlier rank bound 3m−13m-1 would not give the coefficient 2−2/m2-2/m.

Formalization scope

  • Graphs are LooplessGraph V E: endpoint maps left right : E → V with left e ≠ right e, on finite types with decidable equality, so parallel edges are distinct elements of E. A perfect matching is a Finset E with exactly one edge at each vertex.
  • polytope G is the convex hull of matching indicator vectors in E → ℝ; maxMatchingEntropy G x is sSup of the entropies of probability vectors on matchings with mean x. On the polytope this set is nonempty, compact and bounded, so the sSup is the attained maximum; off the polytope it would be junk, which is why the hypothesis x ∈ G.polytope is required.
  • entropy uses Real.negMulLog, so 0log⁡0=00\log0=0; complementEntropy x is B(x)B(x).
  • Hypotheses: 0 < m, Fintype.card V = 2 * m, and a perfect matching exists. The coefficient is the real number 2 - 2 / m.
  • The counting milestones use Turing.TM2ComputableInPolyTime with finite alphabets, binary encodings of the vertex count and of positive multiplicity records, and require polynomially bounded output length.
  • Infrastructure needed: Edmonds' polytope description, faces and minimal faces of polytopes, exponential families and covariance, and polynomial-time computability of rational arithmetic in TM2. The polytope and entropy definitions are reusable for other counting missions.

Selected references

2 thms1 active userReviewed
Markov ChainTheoretical Computer Science·Captain: wurtle

A Fully Polynomial Randomized Approximation Scheme for Perfect Matchings in General GraphsResearch Paper

Motivation: approximately counting perfect matchings

A perfect matching of a graph is a set of edges covering every vertex exactly once. Finding one is easy — Edmonds (1965) gave a polynomial-time algorithm for general graphs — but counting them is hard: Valiant (1979) proved exact counting #P-complete already for bipartite graphs, where the count is the permanent of a 0–1 matrix. Exact counting is tractable only in special classes, such as planar graphs via Pfaffians (Kasteleyn 1963). The natural relaxation is a fully polynomial randomized approximation scheme (FPRAS): an algorithm that, with probability at least 1−δ1-\delta, returns the count within relative error ε\varepsilon, in time polynomial in the input size, 1/ε1/\varepsilon and log⁡(1/δ)\log(1/\delta). Whether perfect matchings in general (nonbipartite) graphs admit an FPRAS was explicitly raised by Jerrum and Sinclair in 1989 and has been a benchmark question in approximate counting since. Perfect-matching counts are partition functions of the monomer–dimer model, so the question also connects to statistical physics.

Timeline

  • 1963 — Kasteleyn: exact counting of perfect matchings in planar graphs (J. Math. Phys. 1963).
  • 1965 — Edmonds: polynomial-time maximum matching in general graphs (Canad. J. Math. 1965).
  • 1979 — Valiant: computing the permanent is #P-complete (TCS 1979).
  • 1986 — Jerrum, Valiant and Vazirani: equivalence of approximate counting and almost-uniform sampling for self-reducible problems (TCS 1986).
  • 1989 — Jerrum and Sinclair: FPRAS for the number of all matchings in any graph, and for perfect matchings when the near-perfect/perfect ratio is polynomially bounded; they raise the general question (SIAM J. Comput. 1989, Section 7(i)).
  • 2004 — Jerrum, Sinclair and Vigoda: FPRAS for the permanent of every nonnegative matrix, i.e. bipartite perfect matchings (J. ACM 2004); accelerated by Bezáková, Štefankovič, Vazirani and Vigoda (SIAM J. Comput. 2008).
  • 2018 — Štefankovič, Vigoda and Wilmes: graphs on which every chain of Jerrum–Sinclair–Vigoda type either gives perfect matchings exponentially small mass or mixes exponentially slowly (LATIN 2018).
  • 2020–2025 — Cai and Liu relate the problem to the eight-vertex model (ICALP 2020); Fei, Goldberg and Lu locate it among two-state spin systems (Inf. Comput. 2025).
  • 2026 — Further permanent speedups by Chen, Vigoda and Yang (arXiv:2608.26599) and Chen, Guo, Vigoda and Yang (arXiv:2609.20717); deterministic hafnian approximation for dense graphs by Yi (arXiv:2609.04079). An OpenAI preprint, A Fully Polynomial Randomized Approximation Scheme for Perfect Matchings in General Graphs (OpenAI Math Release, September 23, 2026), claims an FPRAS for every finite simple graph. The preprint has not been peer reviewed, and its main theorem is not formally verified.

Setting

A finite simple undirected graph GG on vertices {0,…,n−1}\{0,\dots,n-1\} is given by a set of edges, each written once as a pair (u,v)(u,v) with u<vu<v. A set M⊆EM\subseteq E is a perfect matching if every vertex lies in exactly one edge of MM, and

Z(G)=#{M⊆E:M is a perfect matching of G}.Z(G)=\#\{M\subseteq E: M\text{ is a perfect matching of }G\}.

(The graph with no vertices has Z=1Z=1; any graph with an odd number of vertices has Z=0Z=0.)

A randomized algorithm is modelled as a single fixed machine with a finite transition table over a finite tape alphabet, which at each step reads the current tape symbol and one fresh fair random bit, then writes, moves, or halts. The input is the graph in binary (number of vertices, number of edges, the sorted edge list) followed by the rationals ε\varepsilon and δ\delta in reduced form; the output is a rational number written on the tape when the machine halts.

Formalization targets

Goal: Theorem 1.1 (FPRAS for perfect matchings)

There are a machine AA and constants C>0C>0, dd such that for every graph GG and rationals 0<ε<10<\varepsilon<1, 0<δ<1/20<\delta<1/2, with t=C (∣input∣+⌈ε−1⌉+⌈log⁡2⌈δ−1⌉⌉+1)dt=C\,(|\mathrm{input}|+\lceil\varepsilon^{-1}\rceil+\lceil\log_2\lceil\delta^{-1}\rceil\rceil+1)^d:

  • on every random string of length tt, AA halts within tt steps with a nonnegative rational output Z^\widehat Z;
  • if Z(G)=0Z(G)=0, the output is 00 on every random string;
Pr⁡bits[(1−ε)Z(G)≤Z^≤(1+ε)Z(G)]  ≥  1−δ.\Pr_{\text{bits}}\big[(1-\varepsilon)Z(G)\le\widehat Z\le(1+\varepsilon)Z(G)\big]\;\ge\;1-\delta.

The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The theorem answers the Jerrum–Sinclair question affirmatively: perfect matchings in arbitrary graphs can be approximately counted as efficiently, up to polynomial factors, as in the bipartite case. The worst-case time bound holds for every execution, not just in expectation. Via standard reductions, the source also derives counting schemes for edge subsets with prescribed vertex degrees and for matchings of a fixed size (Corollary 10.1). The accompanying samplers for those families always return a feasible object and approximate the uniform law in total variation.

Formalizing it. The statement fixes a concrete machine model, input encoding and time bound, so a formal proof would certify both correctness of the estimator and the polynomial running time of an explicit algorithm — a level of rigor rarely reached for Markov-chain Monte Carlo results, whose analyses involve many interacting constants.

Difficulty

The natural approach extends the Jerrum–Sinclair–Vigoda Markov chain on perfect and near-perfect matchings, with weights learned while edge activities are gradually lowered. In general graphs this approach provably fails: Štefankovič, Vigoda and Wilmes constructed graphs on which every chain of that type, for any hole-dependent weights, has either exponentially small stationary mass on perfect matchings or exponentially slow mixing. Odd cycles (blossoms) are the reason the bipartite canonical-path arguments do not carry over. A solution needs a different state space and a different mixing analysis.

Formalization scope

  • GraphInput is a vertex count n and a Finset (Fin n × Fin n) of edges with strictly increasing endpoints, so loops and duplicate edges are excluded. Perfect G M requires M ⊆ edges and that each vertex is incident to exactly one edge of M; Z G is the number of such M.
  • The machine model is RandomMachine: a finite transition table on Fin 8 symbols, whose step consumes one random bit and performs a Turing.TM0 write or move, or halts. run folds tick over a list of t bits; halted configurations are absorbing.
  • encodeInput writes the vertex count, edge count and lexicographically sorted edges in binary, then encodeRat ε and encodeRat δ (reduced numerator with sign, denominator). Outputs requires that the machine has halted and the tape to the right of the head is exactly the encoding of the output rational.
  • The time bound is a fixed polynomial with natural ceilings; the success probability is the fraction of good tapes among all 2t2^t tapes.
  • The scheme must be uniform: one machine for all inputs, quantified before the graph. A trivializing reading is excluded because every tape must halt within the bound with a nonnegative output, and zero must be returned exactly when Z(G)=0Z(G)=0.
  • Infrastructure needed: a compiler-style layer turning structured randomized algorithms into RandomMachine transitions, Markov-chain spectral-gap bounds, and sampling-to-counting reductions. The machine model and encodings are reusable for other approximate-counting missions.

Selected references

2 thms1 active userReviewed
Functional AnalysisTheoretical Computer Science·Captain: wurtle

Finite-Circle Obstructions, Binary Codes, and Histogram Embeddings for Edit DistanceResearch Paper

Motivation

Edit distance ED(x,y)\mathrm{ED}(x,y), the least number of single-symbol insertions, deletions and substitutions turning xx into yy, is the standard distance on strings. Embedding strings into ℓ1\ell_1 with small distortion would make edit distance amenable to the fast nearest-neighbour and sketching tools available for ℓ1\ell_1, so the least achievable distortion is a central quantity in metric embedding theory. A single insertion shifts every later symbol, yet cyclically shifting a word costs only two edits; this tension between position and alignment is what makes edit distance hard to embed.

This preprint gives two independent constructions of binary word sets whose least ℓ1\ell_1 distortion is exp⁡(Ω(log⁡dlog⁡log⁡d))\exp(\Omega(\sqrt{\log d\log\log d})), two binary coding arguments that transfer large-alphabet constructions to binary, and a complete histogram embedding attaining the matching upper scale. Together they determine the exponential scale of the distortion.

Background

  • 1966, 1974. Levenshtein introduces insertion/deletion codes; Wagner and Fischer describe alignments by increasing traces.
  • 1995. Linial, London and Rabinovich develop finite metric embeddings into ℓ1\ell_1.
  • 1999. Schulman and Zuckerman construct asymptotically good codes for insertions and deletions.
  • 2003. Andoni, Deza, Gupta, Indyk and Raskhodnikova give binary sets with ℓ1\ell_1 distortion approaching 3/23/2.
  • 2006. Khot and Naor prove a (log⁡d)1/2−o(1)(\log d)^{1/2 - o(1)} lower bound by Fourier analysis of cuts.
  • 2007. Ostrovsky and Rabani prove the upper bound exp⁡(O(log⁡dlog⁡log⁡d))\exp(O(\sqrt{\log d\log\log d})) for fixed-length binary strings.
  • 2009. Krauthgamer and Rabani prove an Ω(log⁡d)\Omega(\log d) lower bound.
  • 2026. The OpenAI preprint Finite-Circle Obstructions, Binary Codes, and Histogram Embeddings for Edit Distance (dated September 27, 2026), a companion to Edit Distance in ℓ1\ell_1: Matching Bounds up to Constants in the Exponent, proves the results below. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

For a finite alphabet Σ\Sigma with ∣Σ∣≥2|\Sigma| \ge 2 and an integer d≥1d \ge 1, let Σ≤d\Sigma^{\le d} be the words of length at most dd, including the empty word. For an injective f:Σ≤d→ℓ1f : \Sigma^{\le d} \to \ell_1,

dist(f)=(max⁡x≠y∥f(x)−f(y)∥1ED(x,y))(max⁡x≠yED(x,y)∥f(x)−f(y)∥1),EΣ(d)=inf⁡fdist(f).\mathrm{dist}(f) = \Big(\max_{x\ne y}\frac{\|f(x)-f(y)\|_1}{\mathrm{ED}(x,y)}\Big)\Big(\max_{x\ne y}\frac{\mathrm{ED}(x,y)}{\|f(x)-f(y)\|_1}\Big), \qquad E_\Sigma(d) = \inf_f \mathrm{dist}(f).

The longest common subsequence LCS(x,y)\mathrm{LCS}(x,y) and the deficit rL(x,y)=L−LCS(x,y)r_L(x,y) = L - \mathrm{LCS}(x,y) for words of length LL are used in the coding results. A binary substitution c:Σ→{0,1}wc : \Sigma \to \{0,1\}^w replaces each letter by a codeword.

In Lean (OAI.FiniteCircle), editDistance is the least script length, lcs and deficit are as above, optimalDistortion is the infimum of distortion over injective maps into lp (fun _ : ℕ => ℝ) 1, E α d is the least distortion of words of length at most dd, and maskWord, excludedWord are the two finite-circle constructions with prime-period parameters.

Formalization targets

Goal: finiteCircle_fullMain

The conjunction of the paper's main statements, with common absolute constants:

  • Theorem 1.1. For d≥d0d \ge d_0 and every finite Σ\Sigma with ∣Σ∣≥2|\Sigma| \ge 2,
exp⁡(clog⁡dlog⁡log⁡d)≤EΣ(d)≤exp⁡(Clog⁡dlog⁡log⁡d),\exp\big(c\sqrt{\log d\log\log d}\big) \le E_\Sigma(d) \le \exp\big(C\sqrt{\log d\log\log d}\big),

and the same bounds for sup⁡∣Σ∣≥2EΣ(d)\sup_{|\Sigma| \ge 2} E_\Sigma(d).

  • Lower constructions (Sections 5–7): for each d≥d0d \ge d_0, both the mask construction and the excluded-prime construction, encoded in binary, give a set of words of one common length n≤dn \le d with least distortion at least exp⁡(clog⁡dlog⁡log⁡d)\exp(c\sqrt{\log d\log\log d}).
  • Theorem 4.1 (two binary substitutions): for every alphabet of A≥2A \ge 2 letters there are codes c:Σ→{0,1}wc : \Sigma \to \{0,1\}^w with w=O(log⁡2A)w = O(\log 2A) and a w rL(x,y)≤rwL(c(x),c(y))≤w rL(x,y)a\,w\,r_L(x,y) \le r_{wL}(c(x),c(y)) \le w\,r_L(x,y) for equal-length words, ED(c(x),c(y))≤w ED(x,y)\mathrm{ED}(c(x),c(y)) \le w\,\mathrm{ED}(x,y), plus the local separation property each construction needs.
  • Theorem 8.1 (uniform upper bound): a deterministic finite-dimensional map FF with ED(x,y)≤∥F(x)−F(y)∥1≤exp⁡(Clog⁡dlog⁡log⁡d) ED(x,y)\mathrm{ED}(x,y) \le \|F(x)-F(y)\|_1 \le \exp(C\sqrt{\log d\log\log d})\,\mathrm{ED}(x,y).

Significance

The result. The lower bounds reach the Ostrovsky–Rabani scale, so the order of log⁡EΣ(d)\log E_\Sigma(d) is log⁡dlog⁡log⁡d\sqrt{\log d\log\log d}; this improves the previous Ω(log⁡d)\Omega(\log d) lower bound to exp⁡(Ω(log⁡dlog⁡log⁡d))\exp(\Omega(\sqrt{\log d\log\log d})). The histogram embedding gives an explicit, alphabet-uniform upper bound including all shorter words.

Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. Unlike the companion paper, the upper bound here is proved in full (Section 8) rather than imported, so the goal is self-contained relative to the preprint. The edit-distance and distortion definitions are reusable across the edit-distance missions.

Difficulty

Lower bounds for edit distance must control every increasing matching of the two words, including matchings crossing the row boundaries used to construct them. A cheap translation of phases moves row lists at low edit cost, while a simultaneous half-turn at every leaf must be expensive; proving the latter for arbitrary alignments, and then showing that every ℓ1\ell_1 image must distort one of these comparisons, requires combining a combinatorial separation estimate with a Fourier argument on the finite phase space that forces large total frequency.

Formalization scope

  • Words are List α with Fintype α; the domain Σ≤d\Sigma^{\le d} is a subtype by length; the empty word is included.
  • distortion uses sSup over finite sets of ratios; optimalDistortion is sInf over injective maps into ℓ1(N)\ell_1(\mathbb N); exponentScale d = sqrt(log d · log log d) with natural logarithms.
  • The lower witnesses fix the paper's constructions (prime assignments MaskPrimes, ExcludedPrimes, depth parameters) and require a common positive length n≤dn \le d.
  • UniformUpper asks for a map into Fin M → ℝ with the ℓ1\ell_1 norm written as a finite sum.

The goal is not vacuous: a set with one element would have least distortion 00, so witnesses must be nontrivial, and both bounds are required uniformly.

Needed infrastructure: LCS and alignment combinatorics, cut decompositions of finite ℓ1\ell_1 metrics, Fourier analysis on finite cyclic groups, prime counting estimates, and random partition arguments for the upper bound. Contributions toward any component are welcome.

Selected references

2 thms1 active userReviewed
Functional AnalysisTheoretical Computer Science·Captain: wurtle

Edit Distance in l1: Matching Bounds up to Constants in the ExponentResearch Paper

Motivation

Edit distance ED(x,y)\mathrm{ED}(x,y) is the least number of single-symbol insertions, deletions and substitutions transforming a string xx into yy. It is the basic similarity measure for strings, but it is expensive to compute and awkward to index. A standard way around this is to embed strings into ℓ1\ell_1 so that ℓ1\ell_1 distances approximate edit distances; the quality of such a map is its distortion. Low-distortion embeddings give fast approximate nearest-neighbour search and sketching for edit distance, so the best possible distortion has been studied for two decades.

This preprint determines the exponential scale of the optimal distortion: for strings of length at most dd, it is exp⁡(Θ(log⁡d log⁡log⁡d))\exp(\Theta(\sqrt{\log d\,\log\log d})), uniformly over finite alphabets.

Background

  • 1966. Levenshtein studies codes correcting insertions, deletions and substitutions.
  • 1974. Wagner and Fischer describe edit scripts through increasing traces (alignments).
  • 1995. Linial, London and Rabinovich develop the geometry of finite metric embeddings into ℓ1\ell_1.
  • 2003. Andoni, Deza, Gupta, Indyk and Raskhodnikova give binary subsets with ℓ1\ell_1 distortion approaching 3/23/2.
  • 2006. Khot and Naor prove an Ω(log⁡d/log⁡log⁡d)\Omega(\sqrt{\log d/\log\log d}) lower bound via cuts and Fourier analysis of noisy shifts.
  • 2007. Ostrovsky and Rabani prove the upper bound exp⁡(O(log⁡dlog⁡log⁡d))\exp(O(\sqrt{\log d\log\log d})) for binary strings of length dd.
  • 2009. Krauthgamer and Rabani prove an Ω(log⁡d)\Omega(\log d) lower bound for binary strings of length dd.
  • 2026. The OpenAI preprint Edit Distance in ℓ1\ell_1: Matching Bounds up to Constants in the Exponent (dated September 27, 2026) proves a matching lower bound exp⁡(Ω(log⁡dlog⁡log⁡d))\exp(\Omega(\sqrt{\log d\log\log d})). It has not been peer reviewed; the Lean goal is open on this platform.

Setting

For a finite alphabet Σ\Sigma and d≥1d \ge 1, let Σ≤d\Sigma^{\le d} be the set of strings of length at most dd, including the empty string. Edit scripts may pass through strings of any length. Let ℓ1\ell_1 be the space of absolutely summable real sequences. Define

EΣ(d)=inf⁡f:Σ≤d↪ℓ1(max⁡x≠y∥f(x)−f(y)∥1ED(x,y))(max⁡x≠yED(x,y)∥f(x)−f(y)∥1),E_\Sigma(d) = \inf_{f:\Sigma^{\le d}\hookrightarrow \ell_1}\Big(\max_{x\ne y}\frac{\|f(x)-f(y)\|_1}{\mathrm{ED}(x,y)}\Big)\Big(\max_{x\ne y}\frac{\mathrm{ED}(x,y)}{\|f(x)-f(y)\|_1}\Big),

the infimum over injective maps with no restriction on dimension or computability.

In Lean (OAI.EditDistortion), edit x y is the least length of a Script true n x y of unit insertions, deletions and substitutions on List Alpha; L1 = lp (fun _ : ℕ => ℝ) 1; distortion ρ f is the product of the two maximal ratios for an embedding f : X ↪ L1; leastDistortion is the infimum over embeddings; E Alpha d applies this to {x : List Alpha // x.length ≤ d}; exponentScale c d = exp(c·sqrt(log d · log log d)).

Formalization targets

Goal: Theorem 1.1

There are absolute c,C>0c, C > 0 and d0d_0 such that for every d≥d0d \ge d_0 and every finite alphabet with ∣Σ∣≥2|\Sigma| \ge 2,

exp⁡(clog⁡d log⁡log⁡d)≤EΣ(d)≤exp⁡(Clog⁡d log⁡log⁡d).\exp\big(c\sqrt{\log d\,\log\log d}\big) \le E_\Sigma(d) \le \exp\big(C\sqrt{\log d\,\log\log d}\big).

The lower bound is witnessed by a finite set of binary strings of one common length at most dd, and the same two bounds hold for sup⁡2≤∣Σ∣<∞EΣ(d)\sup_{2 \le |\Sigma| < \infty} E_\Sigma(d).

Significance

The result. Theorem 1.1 shows that the Ostrovsky–Rabani embedding is optimal up to the constant in the exponent, closing the gap between Ω(log⁡d)\Omega(\log d) (Krauthgamer–Rabani) and exp⁡(O(log⁡dlog⁡log⁡d))\exp(O(\sqrt{\log d\log\log d})). It rules out any ℓ1\ell_1 embedding of edit distance with distortion exp⁡(o(log⁡dlog⁡log⁡d))\exp(o(\sqrt{\log d\log\log d})), which limits ℓ1\ell_1-based approaches to approximate edit-distance search.

Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. The upper bound relies on Ostrovsky and Rabani's fixed-length theorem (Theorem 5.1 in the preprint, taken from the literature) plus reductions proved in the preprint, so a full formalization also requires formalizing the Ostrovsky–Rabani embedding. The lower bound (Sections 2–4) is the new contribution.

Difficulty

Any lower bound must control every alignment of two strings, including matchings that cross the boundaries of the blocks used to build them, because an insertion or deletion shifts an entire suffix. Earlier Fourier-analytic arguments (Khot–Naor) and recursive constructions (Krauthgamer–Rabani) lose too much to reach the log⁡dlog⁡log⁡d\sqrt{\log d\log\log d} exponent; reaching it requires a construction whose combinatorial separation and an ℓ1\ell_1 displacement inequality match at that scale.

Formalization scope

  • Strings are List Alpha with Fintype Alpha, 2 ≤ card Alpha; the domain includes the empty string and all lengths up to dd.
  • Edit distance includes substitutions; edit is an sInf over script lengths, which is attained since scripts always exist.
  • distortion uses sSup over finitely many ratios (the domain is finite), so no default values arise; leastDistortion is sInf over all injective maps into ℓ1(N)\ell_1(\mathbb{N}).
  • BinaryWitness c d asks for a finite nonempty set of Boolean lists of common length n≤dn \le d whose least distortion is at least exponentScale c d; a singleton has least distortion 00, so the witness must be nontrivial.

The statement cannot be met trivially: both bounds are required with constants uniform in the alphabet.

Needed infrastructure: cut decompositions of finite ℓ1\ell_1 metrics, Fourier analysis on finite abelian groups, prime-number estimates (Rosser–Schoenfeld), and the Ostrovsky–Rabani construction. Contributions toward the displacement inequality (Proposition 2.2) or the recursive construction (Proposition 3.1) are welcome.

Selected references

2 thms1 active userReviewed
Discrete GeometryTheoretical Computer Science·Captain: wurtle

The Euclidean Steinitz–Bergström theoremResearch Paper

Motivation: keeping partial sums of vectors small

Given vectors v1,…,vNv_1,\dots,v_N in the Euclidean unit ball of Rd\mathbb R^d that sum to zero, can they always be reordered so that every partial sum stays in a ball whose radius depends only on dd? Steinitz's lemma, from his work on rearrangements of conditionally convergent vector series, says yes: in any norm, radius dd suffices (Grinberg–Sevast'yanov 1980). For the Euclidean norm, the expected answer is O(d)O(\sqrt d), the Euclidean Steinitz–Bergström conjecture. A closely related prefix discrepancy problem asks for signs εi∈{±1}\varepsilon_i\in\{\pm1\}, chosen once and for all, such that every signed prefix ∑i≤kεivi\sum_{i\le k}\varepsilon_iv_i is O(d)O(\sqrt d), independently of NN. Both questions are basic in discrepancy theory and combinatorial vector balancing, with applications to scheduling, rounding and the analysis of online and streaming algorithms.

Timeline

  • 1913 — Steinitz proves his rearrangement lemma for conditionally convergent vector series (historical account in Ambrus–Heck 2026, Section 2).
  • 1954 — Behrend discusses the expected square-root growth in Euclidean space (Canad. J. Math., p. 108).
  • 1980 — Grinberg and Sevast'yanov prove that partial sums can be kept within dd times the unit ball, for every norm (Funct. Anal. Appl.).
  • 1994–2023 — Chobanyan's transference principle relates rearrangements to signed sums (Probability in Banach Spaces 9, 1994), later in a finite positive-forward, negative-reverse form (Chobanyan et al., Bull. TICMI 2023).
  • 1998 / 2012 — Banaszczyk's Gaussian-measure balancing theorem (Random Structures Algorithms 1998) and his prefix bound O(d+log⁡N)O(\sqrt d+\sqrt{\log N}) for signed series and rearrangements (Random Structures Algorithms 2012).
  • 2021 — Bansal, Jiang, Meka, Singla and Sinha state the O(d)O(\sqrt d) prefix-signing question explicitly (Conjecture 6.3, arXiv:2111.07049).
  • 2026 — Ambrus and Heck record the conjecture and its attribution to Bergström (Conjecture 5) and reduce it to a relaxed problem (Mathematika); Dutta, Jha and Jiang give efficient bounds O(d+d1/4log⁡7/4N)O(\sqrt d+d^{1/4}\log^{7/4}N) (arXiv:2604.13355).
  • 2026 — An OpenAI preprint, The Euclidean Steinitz–Bergström theorem (OpenAI Math Release, September 24, 2026), claims the O(d)O(\sqrt d) bound for both problems with an absolute constant. It has not been peer reviewed, and its proof is not formally verified.

Setting

Work in Euclidean space Rd\mathbb R^d with norm ∥⋅∥2\|\cdot\|_2, and let v1,…,vNv_1,\dots,v_N satisfy ∥vi∥2≤1\|v_i\|_2\le1; repetitions and zero vectors are allowed. A prefix sum is ∑i=1k\sum_{i=1}^k for 0≤k≤N0\le k\le N (the empty sum is 00). For a zero-sum family, the Steinitz quantity

β(v1,…,vN)=min⁡π∈SN max⁡0≤k≤N∥∑i=1kvπ(i)∥2\beta(v_1,\dots,v_N)=\min_{\pi\in\mathfrak S_N}\ \max_{0\le k\le N}\Bigl\|\sum_{i=1}^kv_{\pi(i)}\Bigr\|_2

is the best achievable maximal prefix norm over all orderings. The Euclidean Steinitz constant S2(d)S_2(d) is its supremum over all such families.

Formalization targets

Goal: prescribed-order signing and Euclidean Steinitz with one absolute constant (Theorems 1.1 and 1.2)

There is an absolute constant CC such that for all d,N≥1d,N\ge1 and all v1,…,vN∈Rdv_1,\dots,v_N\in\mathbb R^d with ∥vi∥2≤1\|v_i\|_2\le1:

  1. (Theorem 1.1) there are signs εi∈{−1,1}\varepsilon_i\in\{-1,1\} with
max⁡0≤k≤N∥∑i=1kεivi∥2≤Cd;\max_{0\le k\le N}\Bigl\|\sum_{i=1}^k\varepsilon_iv_i\Bigr\|_2\le C\sqrt d ;
  1. (Theorem 1.2) if moreover ∑ivi=0\sum_iv_i=0, some permutation π\pi satisfies
max⁡0≤k≤N∥∑i=1kvπ(i)∥2≤Cd.\max_{0\le k\le N}\Bigl\|\sum_{i=1}^kv_{\pi(i)}\Bigr\|_2\le C\sqrt d .

The constant is not fixed. The simplex example in the source shows S2(d)≥12dS_2(d)\ge\tfrac12\sqrt d, so the order is optimal. The goal statement is published on the platform with status Open.

Significance

The result itself. Theorem 1.2 settles the Euclidean Steinitz–Bergström conjecture: S2(d)=Θ(d)S_2(d)=\Theta(\sqrt d). Theorem 1.1 settles the ℓ2\ell_2 prefix-discrepancy question of Bansal et al., removing the log⁡N\sqrt{\log N} term in Banaszczyk's bound. A single choice of signs controls all prefixes at once, unlike terminal balancing results that bound one sum. The source also derives finite-dimensional ℓp\ell_p Steinitz bounds and a colorful Steinitz theorem (Corollaries 8.1–8.2). The result is existential and gives no efficient algorithm.

Formalizing it. The statement is finite and elementary. The deduction of Theorem 1.2 from Theorem 1.1 is a short transference argument (Section 1.1 of the source), suitable as a first formalization step. The proof of Theorem 1.1 uses Gaussian measures of convex bodies, Dirichlet energies, Steiner symmetrization and Brownian survival estimates, which would make substantial reusable additions to Mathlib's probability and convex-geometry libraries.

Difficulty

Signing each prefix separately is easy, by terminal balancing results, but one common signing must work for all NN prefixes. Union bounds over prefixes and Banaszczyk's Gaussian-measure method lose a log⁡N\sqrt{\log N} factor, because the probability that a random walk stays in a ball of radius CdC\sqrt d for NN steps decays with NN. The proof must therefore control a single body of coefficients enforcing all prefix constraints, with bounds independent of the number of steps.

Formalization scope

  • Vectors live in EuclideanSpace ℝ (Fin d), indexed by Fin N, with d,N≥1d,N\ge1 and ∥vi∥≤1\|v_i\|\le1.
  • Prefixes are sums over {i:i<k}\{i : i < k\} for every natural k≤Nk\le N, so the empty prefix and the full sum are included.
  • SignedPrefixBound C asks for signs εi∈{−1,1}\varepsilon_i\in\{-1,1\} (as reals) with every signed prefix at most CdC\sqrt d. OrderingPrefixBound C asks, for zero-sum families, for a permutation π\pi with every reordered prefix at most CdC\sqrt d. The goal is ∃C, SignedPrefixBound C∧OrderingPrefixBound C\exists C,\ \mathrm{SignedPrefixBound}\,C\wedge\mathrm{OrderingPrefixBound}\,C; the same constant serves both, as stated in the source.
  • The quantifier order is the source's: CC is chosen before dd, NN and the vectors.
  • Needed infrastructure: Gaussian measures of symmetric convex bodies, Steiner symmetrization, Dirichlet energies of densities, Ornstein–Uhlenbeck/Brownian survival estimates, and the Chobanyan transference. Contributions proving the transference step (Theorem 1.1 ⇒ Theorem 1.2) or the lower-bound example are welcome.

Selected references

2 thms1 active userReviewed
Number Theory·Captain: wurtle

The additive indecomposability of the primesResearch Paper

Motivation

Goldbach-type problems ask which sets are sumsets of primes. The inverse Goldbach problem, due to Ostmann (1956), reverses the question: can the set of primes itself, up to finitely many changes, be written as a sumset A+B={a+b:a∈A, b∈B}A+B=\{a+b:a\in A,\ b\in B\} with both AA and BB having at least two elements? Ostmann conjectured that it cannot: the primes are asymptotically additively indecomposable. The problem is a clean test of how much additive structure the primes can carry, and it connects sieve theory (the primes avoid one residue class modulo each prime) with inverse questions for the large sieve.

Background

The source of this mission is an OpenAI preprint dated September 24, 2026.

Setting

Let N0={0,1,2,… }\mathbb N_0=\{0,1,2,\dots\} and let PP be the set of positive primes. For A,B⊆N0A,B\subseteq\mathbb N_0 the sumset is A+B={a+b:a∈A, b∈B}A+B=\{a+b:a\in A,\ b\in B\}. Two sets are asymptotically equal if their symmetric difference X△Y=(X∖Y)∪(Y∖X)X\triangle Y=(X\setminus Y)\cup(Y\setminus X) is finite. A decomposition is nontrivial if ∣A∣≥2|A|\ge2 and ∣B∣≥2|B|\ge2; the trivial decompositions {0}+P\{0\}+P are excluded.

Formalization targets

Goal: Theorem 1.1 (Ostmann's conjecture)

A,B⊆N0, ∣A∣≥2, ∣B∣≥2 ⟹ (A+B)△P is infinite.A,B\subseteq\mathbb N_0,\ |A|\ge2,\ |B|\ge2\ \Longrightarrow\ (A+B)\triangle P\ \text{is infinite}.

Milestone: Theorem 2.3 (two infinite summands)

There are no infinite A,B⊆N0 with (A+B)△P finite.\text{There are no infinite }A,B\subseteq\mathbb N_0\text{ with }(A+B)\triangle P\text{ finite}.

Theorem 2.3 is the core of the proof; Lemma 2.2 reduces Theorem 1.1 to it by a short sieve argument.

The goal OAI.Ostmann.inverseGoldbach is open on the platform.

Significance

Theorem 1.1 resolves Ostmann's conjecture. The conclusion controls both requirements of an eventual decomposition: if ∣A∣,∣B∣≥2|A|,|B|\ge2 and A+BA+B contains every sufficiently large prime, then A+BA+B contains infinitely many composite numbers. The proof does not go through the general inverse large-sieve conjecture of Green and Harper; it uses the simultaneous residue restrictions together with coverage of every large prime directly.

The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists. The statement is elementary, so the formal target is short; the difficulty is entirely in the proof.

Difficulty

Counting alone cannot work: sieve bounds put A(x)A(x) and B(x)B(x) near x\sqrt x, which is compatible with the lower bound A(x)B(x)≫x/log⁡xA(x)B(x)\gg x/\log x forced by covering the primes. The known necessary conditions (large intersections with quadratic images) fall short of the near-containment that Green and Harper's conditional route requires. The proof must turn the local information (modulo each prime pp, the images of AA and −B-B are disjoint) into a global contradiction: it rules out correlations with translated multiplicative characters of every order, compares a positive sumset statistic with its average over the primes, and handles residue indicators with no prescribed algebraic form via a finite-field comparison of binary trees. The paper runs to about 80 pages.

Formalization scope

  • primes = {n : ℕ | Nat.Prime n}; sumset A B is Mathlib's pointwise A + B on Set ℕ.
  • A.Nontrivial means AA has two distinct elements.
  • InverseGoldbach asserts Set.Infinite (sumset A B ∆ primes); TwoInfiniteSummandsImpossible uses EventuallyPrimeSumset A B := ∃ N, ∀ n ≥ N, n ∈ A + B ↔ n.Prime, which is equivalent to a finite symmetric difference.
  • OAI.Ostmann.main is the same statement as the goal without the definition file and is included as a reference item.

A complete development needs the additive large sieve (Montgomery–Vaughan), Gallagher's larger sieve, Mertens-type estimates, character sums over finite fields including the quadratic large sieve, prime number theorems in progressions with the exceptional character, and Fourier analysis on Fp\mathbb F_p. Contributions formalizing Lemma 2.1 (fixed shifts), Lemma 2.2 (finite summands), Lemma 2.4 (square-root bounds), Proposition 3.1, Corollary 4.2 (mixed-character decorrelation), Proposition 5.1 and Lemma 6.1 (tree comparison) are welcome.

Selected references

4 thms1 active userReviewed
Operations ResearchProbabilityRandom Matrix Theory·Captain: mikedeng1

Phase Transition of the Largest Eigenvalue for Nonnull Complex Sample Covariance Matrices 4: The Exponential Last Passage Time Has the Law of the Largest Sample EigenvalueResearch Paper

Motivation

Random growth models and random matrices share limit laws. The first exact instance was found by Johansson (Shape fluctuations and random matrices, Comm. Math. Phys. 2000), who showed that the last passage time of a lattice model with geometric or exponential weights has the law of the largest eigenvalue of a Laguerre (complex Wishart) random matrix. Baik, Ben Arous and Péché (Ann. Probab. 33 (2005)) extended the identity to weights whose rate depends on the row. On the matrix side this is a sample covariance matrix with a general population covariance Σ\Sigma; on the growth side it is a corner growth model, or a series of exponential queues, with inhomogeneous service rates.

The identity is the reason the paper's main result, the phase transition of the largest sample eigenvalue as a few population eigenvalues ("spikes") cross the critical value 1+γ−11 + \gamma^{-1}, is also a theorem about last passage percolation and tandem queues. In the queueing reading, a spike is a slow server, and the phase transition describes how slow a few servers must be before they change the centring and the fluctuation scale of the exit time.

Timeline:

  • 2000, Johansson: equal rates; the geometric and exponential last passage time has the law of the largest Laguerre eigenvalue (his Proposition 1.4 is the case π1=⋯=πN\pi_1 = \cdots = \pi_N of (307)).
  • 2001, Baryshnikov and, independently, Gravner, Tracy and Widom: the tandem-queue and GUE-minor descriptions of the same object.
  • 2005, Baik, Ben Arous and Péché: row-dependent rates πi\pi_i (Proposition 6.1), via the Robinson–Schensted–Knuth (RSK) formula for geometric weights (310) and a scaling limit.

Setting

Last passage time. Attach a real weight X(i,j)X(i,j) to every site of the grid {1,…,N}×{1,…,M}\{1,\ldots,N\}\times\{1,\ldots,M\}. An up/right path from (1,1)(1,1) to (N,M)(N,M) is a sequence of N+M−1N+M-1 sites starting at (1,1)(1,1), ending at (N,M)(N,M), each step adding (1,0)(1,0) or (0,1)(0,1). The last passage time is

L(N,M)=max⁡π:(1,1)↗(N,M)∑(i,j)∈πX(i,j).(306)L(N,M) = \max_{\pi:(1,1)\nearrow(N,M)} \sum_{(i,j)\in\pi} X(i,j). \qquad (306)

Exponential environment. Given positive numbers π1,…,πN\pi_1,\ldots,\pi_N, the X(i,j)X(i,j) are independent and X(i,j)X(i,j) is exponential of mean 1/(πiM)1/(\pi_iM), i.e. density πiMe−πiMx\pi_iMe^{-\pi_iMx} on x≥0x\ge0. All MM sites of row ii share one rate.

Sample covariance matrix. Let gkjg_{kj}, 1≤k≤M1\le k\le M, 1≤j≤N1\le j\le N, be independent standard complex Gaussians (real and imaginary parts independent N(0,1/2)N(0,1/2)). For a unitary UU and ℓj=πj−1\ell_j = \pi_j^{-1} (308), the samples y⃗k=U diag(ℓj) gk\vec y_k = U\,\mathrm{diag}(\sqrt{\ell_j})\,g_k are mean-zero complex Gaussian vectors with covariance Σ=U diag(ℓ) U∗\Sigma = U\,\mathrm{diag}(\ell)\,U^*, and

S=1M∑k=1My⃗ky⃗k ∗,λ1=largest eigenvalue of S.S = \frac1M\sum_{k=1}^M \vec y_k\vec y_k^{\,*}, \qquad \lambda_1 = \text{largest eigenvalue of } S.

Schur functions and geometric weights. For a partition λ\lambda, the Schur function sλ(x)s_\lambda(x) is the sum over semistandard Young tableaux TT of shape λ\lambda of ∏cxT(c)\prod_{c}x_{T(c)}. A geometric variable of parameter q∈[0,1)q\in[0,1) has P(Y=k)=(1−q)qk\mathbb P(Y = k) = (1-q)q^k.

Formalization targets

Goal: Proposition 6.1

For 1≤N≤M1\le N\le M, positive π1,…,πN\pi_1,\ldots,\pi_N and every unitary UU,

P(L(N,M)≤x)=P(λ1(M,N)≤x)for all x∈R.(309)\mathbb P\big(L(N,M)\le x\big) = \mathbb P\big(\lambda_1(M,N)\le x\big) \qquad \text{for all } x\in\mathbb R. \qquad (309)

The two sides are defined independently: one by a maximum over lattice paths of exponential weights, the other by the spectrum of a Gaussian random matrix.

Milestones

  1. The recurrence (313): for every array of weights and every site with a,b≥2a, b\ge2,
L(a,b)=max⁡{L(a−1,b),L(a,b−1)}+X(a,b).L(a,b) = \max\{L(a-1,b), L(a,b-1)\} + X(a,b).
  1. The Cauchy identity (311): ∑λsλ(x)sλ(y)=∏i,j(1−xiyj)−1\sum_\lambda s_\lambda(x)s_\lambda(y) = \prod_{i,j}(1-x_iy_j)^{-1} for xi,yj≥0x_i,y_j\ge0, xiyj<1x_iy_j<1.
  2. The geometric formula (310): for independent geometric weights Y(i,j)Y(i,j) of parameter xiyjx_iy_j, xi,yj∈[0,1)x_i,y_j\in[0,1),
P(G(N,M)≤n)=∏i,j(1−xiyj)∑λ:λ1≤nsλ(x)sλ(y).\mathbb P\big(G(N,M)\le n\big) = \prod_{i,j}(1-x_iy_j)\sum_{\lambda:\lambda_1\le n}s_\lambda(x)s_\lambda(y).
  1. The exponential formula (307): for M≥NM\ge N and distinct πi\pi_i,
P(L(N,M)≤x)=1C∫[0,x]Ndet⁡(e−Mπiξj)V(π)V(ξ)∏jξjM−N dξ.\mathbb P\big(L(N,M)\le x\big) = \frac1C\int_{[0,x]^N}\frac{\det(e^{-M\pi_i\xi_j})}{V(\pi)}V(\xi)\prod_{j}\xi_j^{M-N}\,d\xi.

Significance

The proposition makes every distributional statement about λ1\lambda_1 in the paper a statement about last passage percolation with row-dependent rates: the FkF_k (generalised Tracy–Widom) fluctuations at the critical spike value, the Gaussian fluctuations above it, and the fixed-dimension limit. Through (312)–(313) it also covers the exit time of MM customers from NN exponential servers in series, an operations research object. The geometric formula (310) is the entry point of the RSK method for exactly solvable growth models.

These results are proved in the literature; the paper cites (310) and (311) and derives (307) from them by a limit. None of them is machine-checked as far as this series knows. Formalizing them requires a Lean development of Schur functions, the Cauchy identity and the RSK correspondence on matrices with nonnegative integer entries, and of the Wishart eigenvalue density, each reusable well beyond this mission.

Difficulty

The recurrence (313) is elementary. Everything else is not. The geometric formula (310) needs the RSK bijection between nonnegative integer matrices and pairs of semistandard tableaux of the same shape, together with Schensted's theorem that the first row of the shape is the last passage time; neither is in Mathlib. The passage from (310) to (307) is a scaling limit xi=1−Mπi/Lx_i = 1 - M\pi_i/L, n=xLn = xL, L→∞L\to\infty, in which a sum over partitions must converge to a multiple integral. The matrix side needs the joint eigenvalue density of a complex Wishart matrix with general Σ\Sigma, which uses the Harish-Chandra–Itzykson–Zuber integral. A direct coupling of the two sides is not known; the identity is an equality of laws, proved by computing both.

Formalization scope

The development lives in the namespace SpikedWishart.LastPassage. Conventions:

  • Sites and indices are 0-based; the paper's (1,1)(1,1) and (N,M)(N,M) are (0,0)(0,0) and (N−1,M−1)(N-1,M-1), and N,M≥1N, M\ge1.
  • LL is defined as the maximum over paths (306), never by the recurrence (313), so (313) is a genuine statement.
  • The exponential law is Mathlib's expMeasure with rate πiM\pi_iM.
  • The sample model is mean zero, uncentred, with factor 1/M1/M and E∣g∣2=1\mathbb E|g|^2 = 1; this is the model of (59), (61) and (307), and the page's centring by the sample mean and S=(1/N)XX∗S = (1/N)XX^* are printed slips. The covariance is U diag(π−1)U∗U\,\mathrm{diag}(\pi^{-1})U^* for every unitary UU; specialising to diagonal Σ\Sigma would prove a special case.
  • N≤MN\le M is a disclosed addition to the goal, matching the page's "for M≥NM\ge N" in (307).
  • Proposition 6.1 prints L(M,N)L(M,N); the object is (306)'s L(N,M)L(N,M).
  • Schur functions are the tableau sum with variables extended by zero. The Cauchy identity is stated with the exponent −1-1 that the page omits. In (307) the constant CC is the integral of the same integrand over (0,∞)N(0,\infty)^N, and the πi\pi_i are distinct so that V(π)≠0V(\pi)\ne0; the goal has no distinctness hypothesis.

A formalization in which either side of (309) is defined through the other, or through (307), would be trivial and is excluded: both laws are defined from scratch. Contributions are welcome on RSK and Schur function infrastructure, on the Wishart density, and on the measurability of λ1\lambda_1.

Selected references

9 thms1 active userReviewed
Graph TheoryProbability·Captain: mikedeng1

Random Graphs with a Given Degree Sequence 5: Uniform Random Graphs with Degree Scaling Limit f in the Interior Converge a.s. to the Graph Limit e^{g(x)+g(y)}/(1+e^{g(x)+g(y)})Research Paper

Motivation

A standard way to build a random network with a prescribed degree sequence is to choose a graph uniformly at random from the set of all simple graphs with that degree sequence. The model arises in testing whether the exponential family with the degree sequence as sufficient statistic fits network data, in simulating networks with given degrees, and, for constant degrees, as the random regular graph (Blitzstein–Diaconis, Chatterjee–Diaconis–Sly). Quantities such as the expected number of triangles of such a graph are usually estimated by simulation.

For dense graphs, those whose number of edges is of order n2n^2, the Lovász–Szegedy theory of graph limits (Lovász–Szegedy 2006) describes a large graph by a symmetric function W:[0,1]2→[0,1]W:[0,1]^2\to[0,1]. Chatterjee, Diaconis and Sly identify this limit for uniformly random graphs with a given degree sequence. The answer is the limit of the β-model, a random graph with independent edges whose edge probabilities are eβi+βj/(1+eβi+βj)e^{\beta_i+\beta_j}/(1+e^{\beta_i+\beta_j}). The limit gives exact asymptotic formulas for subgraph counts without simulation.

Setting

Graphs and densities. For a finite simple graph HH on [k]={1,…,k}[k]=\{1,\dots,k\} and a simple graph GG on nn vertices, the homomorphism density is

t(H,G)=∣hom⁡(H,G)∣nk,t(H,G)=\frac{|\hom(H,G)|}{n^k},

where hom⁡(H,G)\hom(H,G) is the set of edge-preserving maps V(H)→V(G)V(H)\to V(G). For W:[0,1]2→RW:[0,1]^2\to\mathbb R,

t(H,W)=∫[0,1]k∏{i,j}∈E(H)W(xi,xj) dx1⋯dxk,t(H,W)=\int_{[0,1]^k}\prod_{\{i,j\}\in E(H)}W(x_i,x_j)\,dx_1\cdots dx_k,

with one factor per edge. Graphs GnG_n on nn vertices converge to the limit represented by WW if t(H,Gn)→t(H,W)t(H,G_n)\to t(H,W) for every finite simple graph HH.

Degree sequences and scaling limits. For each nn let dn=(d1n≥⋯≥dnn)d^n=(d^n_1\ge\dots\ge d^n_n) be the degree sequence of some simple graph on nn vertices. The sequence {dn}\{d^n\} has scaling limit ff, a nonincreasing function on [0,1][0,1], if

∣d1nn−f(0)∣+∣dnnn−f(1)∣+1n∑i=1n∣dinn−f ⁣(in)∣⟶0.\left|\frac{d^n_1}{n}-f(0)\right|+\left|\frac{d^n_n}{n}-f(1)\right|+\frac1n\sum_{i=1}^n\left|\frac{d^n_i}{n}-f\!\left(\frac in\right)\right|\longrightarrow0 .

D′[0,1]D'[0,1] is the set of nonincreasing functions on [0,1][0,1] that are left continuous on (0,1)(0,1). It carries the modified L1L^1 norm ∥f∥1′=∣f(0)∣+∣f(1)∣+∫01∣f∣\|f\|_{1'}=|f(0)|+|f(1)|+\int_0^1|f|. F⊆D′[0,1]\mathcal F\subseteq D'[0,1] is the set of all scaling limits of degree sequences.

The random graphs. GnG_n is chosen uniformly from the simple graphs on {1,…,n}\{1,\dots,n\} with degree sequence dnd^n. In a random graph with independent edges each pair {i,j}\{i,j\} is an edge with probability pijp_{ij}, independently of the other pairs. The β-model PβP_\beta is the case pij=eβi+βj/(1+eβi+βj)p_{ij}=e^{\beta_i+\beta_j}/(1+e^{\beta_i+\beta_j}).

Formalization targets

Goal: Theorem 1.1 (pp. 4–5)

If ff lies in the interior of F\mathcal F for ∥⋅∥1′\|\cdot\|_{1'}, there is a function g∈D′[0,1]g\in D'[0,1], unique on [0,1][0,1], such that

W(x,y)=eg(x)+g(y)1+eg(x)+g(y)satisfiesf(x)=∫01W(x,y) dy  for all x∈[0,1],W(x,y)=\frac{e^{g(x)+g(y)}}{1+e^{g(x)+g(y)}}\quad\text{satisfies}\quad f(x)=\int_0^1W(x,y)\,dy\ \ \text{for all }x\in[0,1],

and almost surely t(H,Gn)→t(H,W)t(H,G_n)\to t(H,W) for every finite simple graph HH.

Milestones (in the order the proof uses them)

  • Lemma 2.2 (p. 14): the fixed-point map φ\varphi of the β-model likelihood equations satisfies ∣φ(x)−φ(y)∣1≤2e2K∣x−y∣1|\varphi(x)-\varphi(y)|_1\le2e^{2K}|x-y|_1 when ∣x∣∞,∣y∣∞≤K|x|_\infty,|y|_\infty\le K.
  • §6.2, p. 30: for nonincreasing dd, the Erdős–Gallai slack E(B)\mathcal E(B) over sets of size kk is minimized at {1,…,k}\{1,\dots,k\}.
  • Lemma 6.1 (p. 26): for independent-edge random graphs, P(∣t(H,G)−Et(H,G)∣>ε)≤2e−Cε2n2\mathbb P(|t(H,G)-\mathbb E t(H,G)|>\varepsilon)\le2e^{-C\varepsilon^2n^2} with C=C(H)C=C(H).
  • Claim 6.3 (p. 27): integer margins close to the row and column sums of a matrix with entries in [δ,1−δ][\delta,1-\delta] are realized by a 0–1 contingency table.
  • Lemma 6.2 (p. 26): if δ≤pij≤1−δ\delta\le p_{ij}\le1-\delta and di=∑j≠ipijd_i=\sum_{j\ne i}p_{ij}, the independent-edge graph has degree sequence dd with probability at least 12δ n3/2+ε\tfrac12\delta^{\,n^{3/2+\varepsilon}} for large nn.
  • p. 34: conditioned on its degree sequence being dd, the β-model graph is uniform on graphs with degree sequence dd.

The proof also uses three results posed in sibling missions of this series: Proposition 1.2 (mission 4, the interior of F\mathcal F), Lemma 4.1 (mission 3, existence and boundedness of the MLE) and Theorem 1.5 (mission 1, geometric convergence of the iteration x↦φ(x)x\mapsto\varphi(x)). They are not restated here.

Significance

The theorem turns questions about a uniformly random graph with given degrees, a law with no independence, into questions about an explicit graphon. Every subgraph density, the limiting degree distribution, and every graph parameter continuous for the graph-limit topology of the uniform model is computed from WW. The function gg solves a continuum version of the β-model maximum-likelihood equations, which connects the combinatorial model with exponential-family statistics.

The result is proved in the paper, which is published in the Annals of Applied Probability (2011). To our knowledge it has no machine-checked proof. Formalizing it requires a Lean development of dense graph limits (homomorphism densities, graphon densities, graph-limit convergence), none of which exists in Mathlib. It also requires a bounded-differences concentration inequality, and a transfer argument from independent-edge models to models conditioned on degrees. Each of these is reusable beyond this mission.

Difficulty

The uniform measure on graphs with a fixed degree sequence has no independence, so concentration inequalities do not apply to it directly. The obvious route is to condition an independent-edge model on its degree sequence. This works only if the probability of the conditioning event is larger than the concentration bound, which is e−cn2e^{-cn^2}. A crude lower bound of δ(n2)\delta^{\binom n2} is too small. Lemma 6.2 supplies δn3/2+ε\delta^{n^{3/2+\varepsilon}}, and it needs a combinatorial completion step (Claim 6.3).

The second difficulty is analytic. The maximum-likelihood parameters βn\beta^n for different nn live in different dimensions. One must show that their step-function profiles converge in L1L^1 to a limit gg and that this gg solves the continuum equation at every point of [0,1][0,1], not only almost everywhere. Several steps of the paper's argument are only sketched. Among them are the almost-sure convergence of the β-model graphs to WW and the estimate fn(x)=d⌈nx⌉n/n+O(1/n)f_n(x)=d^n_{\lceil nx\rceil}/n+O(1/n) (pp. 33–34).

Formalization scope

  • Vertices are Fin n (the paper's vertex ii is i−1i-1), graphs are SimpleGraph (Fin n), and a test graph HH is a SimpleGraph (Fin k), which loses nothing because densities are invariant under relabelling.
  • Functions on [0,1][0,1] are ℝ → ℝ, and only their values on [0,1][0,1] matter. Uniqueness of gg is equality on [0,1][0,1].
  • t(H,W)t(H,W) takes one factor per unordered edge, and the integral is the Lebesgue integral over [0,1]k[0,1]^k.
  • Laws on graphs are finite sums of Dirac masses. The σ-algebra on SimpleGraph (Fin n) is discrete.
  • The interior of F\mathcal F is taken in D′[0,1]D'[0,1] for ∥⋅∥1′\|\cdot\|_{1'}, as the ball form "every h∈D′[0,1]h\in D'[0,1] with ∥h−f∥1′<ε\|h-f\|_{1'}<\varepsilon lies in F\mathcal F".
  • The paper does not say how the GnG_n for different nn are coupled. The goal quantifies over every probability space and every family of measurable GnG_n with the uniform marginals, so the almost-sure convergence holds for every joint law. The almost-sure event contains "for every HH".
  • Lemma 6.2's printed bound 12exp⁡(−log⁡(δ)n3/2+ε)\tfrac12\exp(-\log(\delta)n^{3/2+\varepsilon}) exceeds 11. The milestone states the intended bound 12exp⁡(log⁡(δ)n3/2+ε)\tfrac12\exp(\log(\delta)n^{3/2+\varepsilon}), with NN depending only on (δ,ε)(\delta,\varepsilon).
  • Constants are explicit quantifiers. In Lemma 6.1, C>0C>0 is chosen from HH before nn, pp and ε\varepsilon.

A formalization that replaces almost-sure convergence by convergence in expectation or in probability, that fixes a single coupling, or that asserts the existence of gg only almost everywhere states a weaker theorem and does not close this mission.

Welcome contributions include a general graph-limit library (densities, convergence, the counting lemma), McDiarmid's bounded-differences inequality for finitely many independent Bernoulli variables, the Gale–Ryser theorem in the form needed by Claim 6.3, and proofs of the milestones.

Selected references

14 thms1 active userReviewed
Graph TheoryStatistics·Captain: mikedeng1

Random Graphs with a Given Degree Sequence 2: The Closure of the β-Model Expected Degree Sequences Equals the Convex Hull of All Degree SequencesResearch Paper

Motivation

A degree sequence records how many neighbours each vertex of a graph has. In network statistics it is often the only summary of a graph that is observed or trusted, and the natural probability models for graphs in which "the degree sequence captures the information" are exponential families whose sufficient statistic is the degree sequence. Chatterjee, Diaconis and Sly (arXiv:1005.1136, Ann. Appl. Probab. 2011) call the resulting model the β-model and study its maximum likelihood theory and its use for sampling random graphs with a prescribed degree sequence.

For any exponential family, the first question about estimation is which values of the sufficient statistic can be matched by a parameter: the maximum likelihood equations say exactly "the expected statistic equals the observed one". Theorem 1.4 of the paper answers this for the β-model. Up to taking a closure, the expected degree sequences of the β-model fill the whole convex hull of the degree sequences. The paper notes that the result can also be derived from classical results on the mean space of exponential families (Barndorff-Nielsen 1978; Brown 1986; Wainwright and Jordan 2008, Theorem 3.3), and gives a self-contained proof in §3. Lemma 4.1 of the same paper uses Theorem 1.4 to show that the maximum likelihood estimator exists.

Setting

Fix n≥0n\ge 0 and the vertex set {1,…,n}\{1,\dots,n\}. A graph GG is undirected and simple: no loops and no multiple edges. Its degree sequence is d(G)=(d1,…,dn)∈Rnd(G)=(d_1,\dots,d_n)\in\mathbb R^n, and

D={d(G): G a simple graph on n vertices}\mathcal D=\{d(G):\ G\text{ a simple graph on }n\text{ vertices}\}

is the finite set of all degree sequences. Its convex hull conv⁡(D)\operatorname{conv}(\mathcal D) is a polytope in Rn\mathbb R^n.

For β∈Rn\beta\in\mathbb R^n, the β-model Pβ\mathbb P_\beta is the law of the random graph in which each pair {i,j}\{i,j\}, i≠ji\neq j, is an edge with probability

pij=eβi+βj1+eβi+βj,p_{ij}=\frac{e^{\beta_i+\beta_j}}{1+e^{\beta_i+\beta_j}},

independently of all other pairs. The expected degree sequences form the set

R={(Eβ[d1],…,Eβ[dn]): β∈Rn}.\mathcal R=\big\{\big(\mathbb E_\beta[d_1],\dots,\mathbb E_\beta[d_n]\big):\ \beta\in\mathbb R^n\big\}.

Two functions on Rn\mathbb R^n appear in the proof. The first is g=(g1,…,gn)g=(g_1,\dots,g_n) with

gi(x)=∑j≠iexi+xj1+exi+xj.g_i(x)=\sum_{j\neq i}\frac{e^{x_i+x_j}}{1+e^{x_i+x_j}}.

The second is, for each y∈Rny\in\mathbb R^n,

fy(x)=∑i=1nxiyi−log⁡∏1≤i<j≤n(1+exi+xj).f_y(x)=\sum_{i=1}^n x_iy_i-\log\prod_{1\le i<j\le n}\big(1+e^{x_i+x_j}\big).

The Lean development names these objects betaModel, D, R, g and fy in the namespace GivenDegreeSeq.MeanPolytope.

Formalization targets

Goal: Theorem 1.4 (p. 8)

conv⁡(D)=R‾for every n.\operatorname{conv}(\mathcal D)=\overline{\mathcal R}\qquad\text{for every }n.

The statement fixes no constants. The closure cannot be dropped: for n≥2n\ge2 the degree sequence 00 of the empty graph lies in D\mathcal D but not in R\mathcal R, because every expected degree is positive.

Milestones, in the order the proof uses them

  1. The probability formula (p. 6): Pβ\mathbb P_\beta is a probability measure, and
Pβ({G})=e∑iβidi∏i<j(1+eβi+βj).\mathbb P_\beta(\{G\})=\frac{e^{\sum_i\beta_id_i}}{\prod_{i<j}(1+e^{\beta_i+\beta_j})}.
  1. Expected degrees (p. 15): Ex[di]=gi(x)\mathbb E_x[d_i]=g_i(x), so R=g(Rn)\mathcal R=g(\mathbb R^n).
  2. The easy inclusion (p. 15): R‾⊆conv⁡(D)\overline{\mathcal R}\subseteq\operatorname{conv}(\mathcal D).
  3. A uniform bound (p. 16): fy(x)≤0f_y(x)\le 0 for all y∈conv⁡(D)y\in\operatorname{conv}(\mathcal D) and x∈Rnx\in\mathbb R^n.
  4. Smoothness (p. 16): fyf_y is twice differentiable and ∇2fy\nabla^2 f_y is uniformly bounded.
  5. Lemma 3.1 (pp. 14–15): if ff is twice differentiable, M=sup⁡f<∞M=\sup f<\infty and ∥∇2f∥op≤C\|\nabla^2 f\|_{\mathrm{op}}\le C, then
∣∇f(x)∣2≤2C(M−f(x)),|\nabla f(x)|^2\le 2C\big(M-f(x)\big),

and ∇f(xk)→0\nabla f(x_k)\to0 along some sequence. 7. The gradient (p. 16): ∇fy(x)=y−g(x)\nabla f_y(x)=y-g(x).

Significance

The theorem describes the mean space of the β-model. Its interior contains every degree sequence that lies strictly inside the polytope, and for these sequences maximum likelihood estimation is well posed. The paper's consistency result (Theorem 1.3) and the existence part of Lemma 4.1 start from this description. The polytope conv⁡(D)\operatorname{conv}(\mathcal D) is studied in its own right; its extreme points are the degree sequences of threshold graphs (Mahadev and Peled 1995).

Theorem 1.4 is proved, and as far as this mission's authors know it is not machine-checked anywhere. Formalizing it means turning the paper's short proof into a complete argument. That includes the steps the page dismisses as easy: the exponential-family formula for the independent-edge law, the expectation computation, the Hessian bound for fyf_y, and the passage from a sequence of approximate critical points to the closure. Lemma 3.1, a descent-type gradient bound for a function bounded above, is a general fact of real analysis and is independent of graphs.

Difficulty

The inclusion R‾⊆conv⁡(D)\overline{\mathcal R}\subseteq\operatorname{conv}(\mathcal D) is direct: an expectation is an average. The reverse inclusion is the content. For yy in the interior of the polytope, one would like to find xx with g(x)=yg(x)=y by maximizing the concave function fyf_y. For yy on the boundary of the polytope, however, fyf_y need not attain its supremum. So the argument cannot rely on the existence of a maximizer, and it has to produce points xkx_k with g(xk)→yg(x_k)\to y without ever solving g(x)=yg(x)=y. Compactness arguments on β\beta fail for the same reason: the relevant sequences xkx_k are unbounded.

Formalization scope

  • Graphs and measure. Vertices are Fin n, so the paper's vertex ii is the index i−1i-1. Graphs are SimpleGraph (Fin n), a finite type. Its σ-algebra is Mathlib's SimpleGraph.instMeasurableSpace, under which every set of graphs on Fin n is measurable.
  • The law and its expectations. Pβ\mathbb P_\beta is the finite sum of Dirac masses weighted by the independent-edge product over pairs i<ji<j. R\mathcal R is defined through Bochner expectations under Pβ\mathbb P_\beta, not as the range of gg. Defining R\mathcal R as g(Rn)g(\mathbb R^n) would erase the link to the probability model and is ruled out.
  • Vector spaces. D\mathcal D and R\mathcal R are subsets of Fin n → ℝ, whose product topology is the Euclidean topology, so the closure is unambiguous. Gradients and Hessians are taken on EuclideanSpace ℝ (Fin n). There "twice differentiable" means that ff and its Fréchet derivative are differentiable, and the Hessian norm is the norm of the second Fréchet derivative, which equals the L2L^2 operator norm of the Hessian matrix.
  • No size hypothesis. The goal holds for every nn; for n≤1n\le1 both sides are {0}\{0\}.
  • Readings of the page.
    • On p. 15 the paper prints log⁡∑1≤i<j≤n(1+exi+xj)\log\sum_{1\le i<j\le n}(1+e^{x_i+x_j}) in fyf_y. The formalization uses log⁡∏\log\prod, the only reading under which "taking logs, we get fd(x)≤0f_d(x)\le0" and ∇fy=y−g\nabla f_y=y-g hold. The milestone text keeps the printed version.
    • The "Lemma 11" of p. 16 is Lemma 3.1.
    • The probability-measure property of Pβ\mathbb P_\beta is stated as a conjunct of milestone 1.
    • The differentiability of fyf_y is stated alongside the Hessian bound in milestone 5.

Contributions of any milestone are welcome. Lemma 3.1 and the gradient identity are self-contained calculus. The probability formula and the expected-degree identity are finite computations on graphs.

Selected references

10 thms1 active userReviewed
Linear OptimizationOperations ResearchOptimization·Captain: mikedeng1

Robust Branch-and-Cut-and-Price for the Capacitated Vehicle Routing Problem: The Integer Points of P1 ∩ P2 Are Exactly the CVRP Solutions, and the Dantzig–Wolfe Master Describes P1 ∩ P2Research Paper

Motivation

The capacitated vehicle routing problem (CVRP) asks for KK delivery routes from a depot that serve every client exactly once without exceeding a vehicle capacity, at minimum total length. It was introduced by Dantzig and Ramser in 1959 and is the reference problem of the vehicle routing literature: most exact methods for richer routing models (time windows, heterogeneous fleets, split deliveries) are first developed and benchmarked on it.

Exact CVRP algorithms are driven by the lower bound of a linear relaxation. Two families dominated before 2005. Branch-and-cut works with the edge variables xex_e and the rounded capacity inequalities (Lysgaard, Letchford and Eglese 2004, among others); its bound degrades as the number of vehicles grows. Lagrangean and column-generation methods work with q-routes, walks from the depot of bounded total demand that may revisit clients (Christofides, Mingozzi and Toth 1981). Fukasawa, Longo, Lysgaard, Poggi de Aragão, Reis, Uchoa and Werneck combine the two in one linear program over the intersection of the two polytopes, priced by column generation with every cut written on the edge variables. According to the abstract, the resulting branch-and-cut-and-price solves to optimality all instances from the literature with up to 135 vertices. The design is called robust because cuts are written on the edge variables xx and therefore never change the structure of the pricing problem.

This mission formalizes the formulation itself (§2 of the paper) and the two exact facts of its column generation (§3.1).

Setting

Let G=(V,E)G=(V,E) be an undirected graph on V={0,1,…,n}V=\{0,1,\dots,n\}. Vertex 00 is the depot; V+={1,…,n}V_+=\{1,\dots,n\} are the clients, client ii having a positive demand did_i. Each edge has a length ℓe\ell_e. There are KK vehicles of capacity CC, both positive integers.

A list of clients r=(r1,…,rm)r=(r_1,\dots,r_m) describes the closed walk 0→r1→⋯→rm→00\to r_1\to\cdots\to r_m\to 0. Its edge incidence qe(r)q^e(r) is the number of times the walk traverses ee (a one-client walk 0→j→00\to j\to 0 traverses {0,j}\{0,j\} twice); its load is dr1+⋯+drmd_{r_1}+\cdots+d_{r_m}, with repetitions.

  • A CVRP route visits pairwise distinct clients with load at most CC; a CVRP solution is a family R=(R1,…,RK)R=(R_1,\dots,R_K) of routes visiting every client exactly once. Its edge vector is χ(R)e=∑kqe(Rk)\chi(R)_e=\sum_kq^e(R_k).
  • A q-route without 2-cycles is a walk of load at most CC that may revisit clients but contains no subpath i→j→ii\to j\to i with i≠0i\ne 0.

For S⊆VS\subseteq V, δ(S)\delta(S) is the set of edges with one end in SS, x(δ(S))=∑e∈δ(S)xex(\delta(S))=\sum_{e\in\delta(S)}x_e, and k(S)=⌈d(S)/C⌉k(S)=\lceil d(S)/C\rceil. The paper's constraints on x∈REx\in\mathbb R^{E} and on weights λj≥0\lambda_j\ge 0 of the q-routes jj are

x(δ({i}))=2  (i∈V+)  (1),x(δ({0}))=2K  (2),x(δ(S))≥2k(S)  (S⊆V+)  (3),xe≤1  (e∈E∖δ({0}))  (4),∑jqjeλj=xe  (e∈E)  (5),∑jλj=K  (6).\begin{aligned} &x(\delta(\{i\}))=2\ \ (i\in V_+)\ \ (1), && x(\delta(\{0\}))=2K\ \ (2), && x(\delta(S))\ge 2k(S)\ \ (S\subseteq V_+)\ \ (3),\\ &x_e\le 1\ \ (e\in E\setminus\delta(\{0\}))\ \ (4), && \textstyle\sum_jq^e_j\lambda_j=x_e\ \ (e\in E)\ \ (5), && \textstyle\sum_j\lambda_j=K\ \ (6). \end{aligned}

P1P_1 is {x≥0:(1)–(4)}\{x\ge0:(1)\text{–}(4)\}; P2P_2 is the set of x≥0x\ge 0 satisfying (1) together with some λ≥0\lambda\ge0 satisfying (5), (6); the Explicit Master P3P_3 is the projection onto xx of the system (1)–(6) with one λ\lambda. The Dantzig–Wolfe Master (DWM) is the LP in λ\lambda alone obtained by substituting (5) into (1)–(4), giving the rows (8)–(11), with objective (7) ∑j∑eℓeqjeλj\sum_j\sum_e\ell_eq^e_j\lambda_j. The bounds are Li=min⁡x∈Piℓ⊤xL_i=\min_{x\in P_i}\ell^\top x.

Formalization targets

Goal: the formulation theorem

For a loop-free graph with positive demands and capacity, and arbitrary lengths:

x∈P3∩ZE  ⟺  x=χ(R) for a CVRP solution R,P3={Qλ:λ DWM-feasible},L1, L2 ≤ L3 ≤ OPT,x\in P_3\cap\mathbb Z^{E}\iff x=\chi(R)\ \text{for a CVRP solution }R, \qquad P_3=\{Q\lambda:\lambda\ \text{DWM-feasible}\}, \qquad L_1,\,L_2\ \le\ L_3\ \le\ \mathrm{OPT},

with (7) equal to ℓ⊤Qλ\ell^\top Q\lambda. The bounds are stated in lower-bound form: every lower bound of ℓ⊤x\ell^\top x over P1P_1 or P2P_2 is one over P3P_3, and every lower bound over P3P_3 is at most the cost of every solution.

Milestones

  1. P3=P1∩P2P_3=P_1\cap P_2 (p. 5).
  2. Every CVRP route is a q-route without 2-cycles (p. 2).
  3. Validity of (1)–(4): χ(R)∈P1\chi(R)\in P_1, with ℓ⊤χ(R)\ell^\top\chi(R) the cost of RR (p. 4).
  4. Validity of (5)–(6): χ(R)∈P2\chi(R)\in P_2, with the routes of RR as columns (p. 4).
  5. Every integer point of P1P_1 is χ(R)\chi(R) for a solution RR (p. 4).
  6. Constraint (6) is implied by (2) and (5) (p. 5).
  7. The DWM (8)–(11) is (1)–(4) on x=Qλx=Q\lambda (p. 5).
  8. A generic cut ∑eaexe≥b\sum_ea_ex_e\ge b becomes ∑j(∑eaeqje)λj≥b\sum_j(\sum_ea_eq^e_j)\lambda_j\ge b (p. 5).
  9. Every integer point of P2P_2 is χ(R)\chi(R) for a solution RR (p. 4).
  10. The reduced cost of a column is ∑ecˉeqe\sum_e\bar c_eq^e (§3.1, p. 6).
  11. Scaling: a q-route for demands ⌈dv/g⌉\lceil d_v/g\rceil and capacity ⌊C/g⌋\lfloor C/g\rfloor is a q-route for (d,C)(d,C) (§3.1, p. 7).

Significance

The formulation theorem is what makes the algorithm exact: integer points of P3P_3 are solutions, so branching on xx terminates at an optimum, and P3P_3 is a relaxation, so L3L_3 is a valid bound that dominates both classical bounds. The DWM description is what makes it computable: P3P_3 is optimized by column generation over q-routes, and milestones 8 and 10 show that any cut on xx can be added without changing the pricing problem, which remains a shortest q-route problem with edge costs cˉe\bar c_e.

The paper proves none of these claims formally; most are stated in a sentence, and milestone 9 is stated with "It can be shown" and no proof. To our knowledge none of them has a machine-checked proof. A formal development produces a library of walks, edge incidences, cut values and column families on a general graph that later missions on branch-cut-and-price (subset-row cuts, ng-routes, other routing variants) can import.

Difficulty

Most items are linear-algebra bookkeeping on finite sums, but they require a working theory of walks: edge incidences along a closed walk, the cut value of an incidence vector, and the fact that a walk from the depot crosses every client set an even number of times. The integrality statements (milestones 5 and 9 and goal part 1) are the hard part: an integer vector satisfying degree constraints need not come from routes through the depot, and the statements must exclude every other structure. For P2P_2 there are no capacity cuts at all, so the capacity of the routes must be recovered from the columns, and the paper states this case without proof. The obvious reduction "an integer point of P2P_2 is an integer combination of q-routes" fails: λ\lambda may be fractional even when xx is integral.

Formalization scope

Vertices are Fin (n+1) with depot 0; edges are Sym2 (Fin (n+1)); the graph is an edge set E assumed loop-free where needed. Edge vectors are functions on all unordered pairs that vanish off E, which encodes x∈R∣E∣x\in\mathbb R^{|E|}. Demands dd, KK and CC are natural numbers; positive demands, K>0K>0 and C>0C>0 (the paper's standing assumptions, p. 1) are carried by the integrality statements and the goal, while ℓ≥0\ell\ge0 is used by no statement and is omitted. Loads count repeated visits. The cut value x(δ(S))x(\delta(S)), the demand d(S)d(S) and k(S)=⌈d(S)/C⌉k(S)=\lceil d(S)/C\rceil are the published definitions LysgaardCVRP.Shrink.cut, .demand and .roundedCapacityBound. The matrix QQ is replaced by finitely supported weights on client lists ranging over all q-routes without 2-cycles. L1,L2,L3L_1,L_2,L_3 and OPT are never real infima, since P3P_3 is empty for infeasible instances.

Three trivializations are ruled out by construction: P3P_3 is defined from the Explicit Master display, not as P1∩P2P_1\cap P_2; a CVRP solution is defined by its routes, not as an integer point of a polytope; and the columns are not a fixed finite list, which would turn P2P_2 into a restricted master.

The strictness of "CVRP routes ⊊\subsetneq q-routes" (p. 2) depends on the instance and is not stated. Contributions of reusable lemmas on walks and cut values of incidence vectors are welcome, as are proofs of any milestone.

Selected references

  • R. Fukasawa, H. Longo, J. Lysgaard, M. Poggi de Aragão, M. Reis, E. Uchoa and R. F. Werneck, Robust branch-and-cut-and-price for the capacitated vehicle routing problem, Mathematical Programming 106 (2006); accepted manuscript. https://doi.org/10.1007/s10107-005-0644-x
  • N. Christofides, A. Mingozzi and P. Toth, Exact algorithms for the vehicle routing problem, based on spanning tree and shortest path relaxations, Mathematical Programming 20 (1981). https://doi.org/10.1007/BF01589353
  • J. Lysgaard, A. N. Letchford and R. W. Eglese, A new branch-and-cut algorithm for the capacitated vehicle routing problem, Mathematical Programming 100 (2004). https://doi.org/10.1007/s10107-003-0481-8
  • G. B. Dantzig and J. H. Ramser, The truck dispatching problem, Management Science 6 (1959). https://doi.org/10.1287/mnsc.6.1.80
17 thms1 active userReviewed
Graph Theory·Captain: mikedeng1

Random Graphs with a Given Degree Sequence 4: A Continuum Erdős–Gallai Condition Characterizes the Interior of the Set of Degree-Sequence Scaling LimitsResearch Paper

Motivation

A uniformly random simple graph with a prescribed degree sequence is a basic null model in network science, statistics and combinatorics: it is what a network "looks like" when nothing but its degrees is known. Chatterjee, Diaconis and Sly (arXiv:1005.1136, Ann. Appl. Probab. 2011) show that when the normalized degree sequences converge to a limiting profile ff, these random graphs converge almost surely to an explicit graph limit (their Theorem 1.1). That theorem has a hypothesis: ff must lie in the interior of the set F\mathcal F of all possible limiting degree profiles. A hypothesis of that kind is only useful if it can be checked, and the paper's Proposition 1.2 supplies the check, in the form of a continuum version of the Erdős–Gallai criterion (Erdős and Gallai, Mat. Lapok 1960), the classical test for whether a list of integers is the degree sequence of a simple graph.

This mission formalizes Proposition 1.2 and the steps of its proof in §5 of the paper, together with the Erdős–Gallai criterion itself, which the paper cites and uses in both directions.

Setting

A degree sequence on nn vertices is a vector d=(d1,…,dn)\mathbf d=(d_1,\dots,d_n) of nonnegative integers for which some simple graph (undirected, no loops, no multiple edges) on vertices 1,…,n1,\dots,n has deg⁡(i)=di\deg(i)=d_i for every ii. Such sequences are written in nonincreasing order d1≥d2≥⋯≥dnd_1\ge d_2\ge\cdots\ge d_n.

The space D′[0,1]D'[0,1] consists of the functions ff on [0,1][0,1] that are nonincreasing and left continuous at every point of (0,1)(0,1). It carries the modified L1L^1 norm

∥f∥1′:=∣f(0)∣+∣f(1)∣+∫01∣f(x)∣ dx.\|f\|_{1'}:=|f(0)|+|f(1)|+\int_0^1|f(x)|\,dx.

Suppose that for every nn a degree sequence dn=(d1n≥⋯≥dnn)\mathbf d^n=(d^n_1\ge\cdots\ge d^n_n) on nn vertices is given. The sequence {dn}\{\mathbf d^n\} has scaling limit ff, a nonincreasing function on [0,1][0,1], if

lim⁡n→∞(∣d1nn−f(0)∣+∣dnnn−f(1)∣+1n∑i=1n∣dinn−f(in)∣)=0.(2)\lim_{n\to\infty}\Bigl(\Bigl|\tfrac{d^n_1}{n}-f(0)\Bigr|+\Bigl|\tfrac{d^n_n}{n}-f(1)\Bigr|+\frac1n\sum_{i=1}^n\Bigl|\tfrac{d^n_i}{n}-f\bigl(\tfrac in\bigr)\Bigr|\Bigr)=0.\qquad(2)

The set F\mathcal F consists of the f∈D′[0,1]f\in D'[0,1] that arise as scaling limits of degree sequences. Its interior is taken in D′[0,1]D'[0,1] with the topology of ∥⋅∥1′\|\cdot\|_{1'}: ff is interior if every h∈D′[0,1]h\in D'[0,1] with ∥h−f∥1′<ε\|h-f\|_{1'}<\varepsilon lies in F\mathcal F, for some ε>0\varepsilon>0.

For f∈D′[0,1]f\in D'[0,1] and x∈[0,1]x\in[0,1] the paper defines

Gf(x):=∫x1min⁡{f(y),x} dy+x2−∫0xf(y) dy.G_f(x):=\int_x^1\min\{f(y),x\}\,dy+x^2-\int_0^x f(y)\,dy.

At x=k/nx=k/n, n2Gf(x)n^2G_f(x) approximates the slack k(k−1)+∑i>kmin⁡{di,k}−∑i≤kdik(k-1)+\sum_{i>k}\min\{d_i,k\}-\sum_{i\le k}d_i in the kk-th Erdős–Gallai inequality.

In Lean these objects are IsGraphic, InDprime, norm1', Gf, HasScalingLimit, setF and InteriorF, in the namespace GivenDegreeSeq.Interior.

Formalization targets

Goal: Proposition 1.2 (p. 5)

A function f:[0,1]→[0,1]f:[0,1]\to[0,1] in D′[0,1]D'[0,1] belongs to the interior of F\mathcal F if and only if

  1. there are constants c1>0c_1>0 and c2<1c_2<1 with c1≤f(x)≤c2c_1\le f(x)\le c_2 for all x∈[0,1]x\in[0,1], and
  2. for each x∈(0,1]x\in(0,1],
∫x1min⁡{f(y),x} dy+x2−∫0xf(y) dy>0.\int_x^1\min\{f(y),x\}\,dy+x^2-\int_0^x f(y)\,dy>0.

Milestones

  • Remark 1 (Erdős–Gallai criterion). Nonnegative integers d1≥⋯≥dnd_1\ge\cdots\ge d_n form a degree sequence if and only if ∑idi\sum_i d_i is even and, for each 1≤k≤n1\le k\le n,
∑i=1kdi≤k(k−1)+∑i=k+1nmin⁡{di,k}.\sum_{i=1}^k d_i\le k(k-1)+\sum_{i=k+1}^n\min\{d_i,k\}.
  • Continuity of GfG_f on [0,1][0,1] for f∈D′[0,1]f\in D'[0,1] (p. 23).
  • Necessity: every f∈Ff\in\mathcal F has Gf≥0G_f\ge 0 on [0,1][0,1], and takes values in [0,1][0,1] (p. 23).
  • Membership: every f∈D′[0,1]f\in D'[0,1] satisfying (i) and (ii) belongs to F\mathcal F (pp. 23–24).
  • Stability: for f,f′∈D′[0,1]f,f'\in D'[0,1] and 0≤x≤10\le x\le1, ∣Gf(x)−Gf′(x)∣≤∥f−f′∥1′|G_f(x)-G_{f'}(x)|\le\|f-f'\|_{1'} (p. 24).

Significance

Proposition 1.2 turns the hypothesis of the paper's graph-limit theorem into two explicit conditions on ff. With it, for example, the constant profile f≡pf\equiv p with 0<p<10<p<1, the degree profile of the Erdős–Rényi graph G(n,p)G(n,p), is seen to be interior (Remark 3, p. 6). The proposition also describes which limiting degree profiles are robust under small perturbations: away from the boundary given by the continuum Erdős–Gallai inequality and the trivial bounds 00 and 11.

The Erdős–Gallai criterion is a standard tool for degree sequences, threshold graphs and network models. To the knowledge of this mission it is formalized neither in Mathlib nor on the platform, and a proof of it here is reusable well beyond this paper. The continuum objects D′[0,1]D'[0,1], ∥⋅∥1′\|\cdot\|_{1'}, scaling limits and F\mathcal F are shared with the companion mission on the graph-limit theorem (mission 5 of this series). The proposition is proved in the paper; none of it has a machine-checked proof.

Difficulty

The obvious argument passes the Erdős–Gallai inequalities to the limit and back. Going to the limit is routine. Coming back is not, for two reasons. First, the discrete inequalities must hold for every 1≤k≤n1\le k\le n, and near k=0k=0 the normalized slack Gf(k/n)G_f(k/n) tends to 00, so positivity of GfG_f alone gives nothing for k=o(n)k=o(n). The bounds c1>0c_1>0 and c2<1c_2<1 of condition (i) are what control this range. Second, the approximating integer sequences must satisfy the parity condition and stay nonincreasing, while still converging in the sense of (2).

For openness, the interior must be taken under ∥⋅∥1′\|\cdot\|_{1'}, and positivity of GhG_h near x=0x=0 has to be recovered for every nearby hh from condition (i), not from uniform convergence alone. In the converse direction, perturbations must stay inside D′[0,1]D'[0,1], which constrains how ff may be modified near a zero of GfG_f.

Formalization scope

  • Functions on [0,1][0,1] are ℝ → ℝ. Only their values on [0,1][0,1] enter D′[0,1]D'[0,1], ∥⋅∥1′\|\cdot\|_{1'}, GfG_f, (2) and F\mathcal F. Integrals are interval integrals. Every f∈D′[0,1]f\in D'[0,1] is monotone, hence bounded and integrable on [0,1][0,1].
  • Vertices are Fin n, so the paper's dind^n_i is d n ⟨i-1,_⟩ and the paper's f(i/n)f(i/n) is f ((i+1)/n). Degree sequences are vectors in Fin n → ℕ realized by a SimpleGraph (Fin n) and are nonincreasing.
  • The bracket in (2) has no meaning at n=0n=0 and is set to 00 there. The sequence {dn}\{\mathbf d^n\} is indexed by all nn, not by a subsequence.
  • The interior is the ball formulation in D′[0,1]D'[0,1] under ∥⋅∥1′\|\cdot\|_{1'}, and the balls range only over h∈D′[0,1]h\in D'[0,1]. The plain L1L^1 topology would be wrong: it ignores the endpoint values, and no ff would be interior. ∥⋅∥1′\|\cdot\|_{1'} is a genuine norm on D′[0,1]D'[0,1], so the ball form is the topological interior.
  • The goal keeps the page's hypothesis f([0,1])⊆[0,1]f([0,1])\subseteq[0,1], although the "only if" direction makes it redundant.
  • The scaling-limit set F\mathcal F requires every dn\mathbf d^n to be graphic. Dropping that requirement trivializes the problem, because every nonincreasing [0,1][0,1]-valued function would then be a limit and the proposition would be false. The definitions here exclude it.

Infrastructure needed: the Erdős–Gallai theorem for finite sequences (both directions); Riemann-sum approximation of integrals of monotone functions; an integer-rounding construction with a parity fix. Proofs of the Erdős–Gallai criterion, and of the analytic lemmas on D′[0,1]D'[0,1], are welcome independently of the goal.

Selected references

  • S. Chatterjee, P. Diaconis, A. Sly, Random graphs with a given degree sequence, Ann. Appl. Probab. 21(4) (2011) 1400–1435; arXiv:1005.1136v5. https://arxiv.org/abs/1005.1136 — DOI https://doi.org/10.1214/10-AAP728
  • P. Erdős, T. Gallai, Gráfok előírt fokú pontokkal (Graphs with points of prescribed degree), Mat. Lapok 11 (1960) 264–274.
  • N. V. R. Mahadev, U. N. Peled, Threshold Graphs and Related Topics, Annals of Discrete Mathematics 56, North-Holland, 1995.
10 thms1 active userReviewed
Graph TheoryOperations Research·Captain: mikedeng1

On Metric Generators of Graphs 3: A Connected Minimum T-Join Exists Exactly When μ_G|T Is a Tree Metric Whose Minimal Realization Is a T′-Join Embedding Isometrically in GResearch Paper

Motivation

A TT-join of a graph GG is a set of edges FF such that exactly the vertices of a prescribed even set TT have odd degree in FF. Minimum TT-joins are a classical object of combinatorial optimization: they contain shortest paths (∣T∣=2|T|=2), Chinese postman tours and perfect matchings as special cases, and their duality with TT-cuts connects them to integral multiflows. Whether the minimum size τ(G,T)\tau(G,T) of a TT-join equals the maximum number ν(G,T)\nu(G,T) of disjoint TT-cuts has been studied extensively; equality always holds in bipartite graphs (Seymour 1981).

Sebő and Tannier (Math. Oper. Res. 2004) study the number of connected components of a minimum TT-join, motivated by the observation that a minimum TT-join with few components yields a large integral packing of TT-cuts. Deciding whether some minimum TT-join has at most kk components is NP-complete in general (their Theorem 5). This mission formalizes the opposite end, k=1k=1: Theorem 6 characterizes exactly when a minimum TT-join can be chosen connected, in terms of the shortest-path metric of GG restricted to TT. The result first appeared in the authors' IPCO paper Connected joins in graphs (2001); the 2004 article derives it from its theory of isometric embeddings.

Setting

All graphs are finite, simple, undirected and connected. For vertices x,yx,y of GG, μG(x,y)\mu_G(x,y) is the number of edges of a shortest xx–yy path. For T⊆V(G)T\subseteq V(G), μG∣T\mu_G|_T is the restriction of μG\mu_G to pairs of vertices of TT.

For an edge set F⊆E(G)F\subseteq E(G), deg⁡F(v)\deg_F(v) is the number of edges of FF at vv; FF is a TT-join if deg⁡F(v)\deg_F(v) is odd exactly when v∈Tv\in T. A minimum TT-join has the fewest edges among all TT-joins; a minimal one has no proper subset that is a TT-join. V(F)V(F) is the set of endpoints of edges of FF; FF is connected (a tree) when the graph (V(F),F)(V(F),F) is connected (a tree), and μF\mu_F is the distance in (V(F),F)(V(F),F).

An isometry from (X,μ)(X,\mu) to (Y,ν)(Y,\nu) is a map ff with ν(f(x),f(y))=μ(x,y)\nu(f(x),f(y))=\mu(x,y) for all x,yx,y. A metric μ\mu on a finite set XX is a tree metric if there is a tree AA (unit edge lengths) and an isometry gg from (X,μ)(X,\mu) to AA; the pair (A,g)(A,g) is a realization. A realization is inclusionwise minimal if no proper subtree of AA contains g(X)g(X). A tree AA is an SS-join if its vertices of odd degree are exactly those of SS.

Formalization targets

Goal: Theorem 6

For GG connected and TT nonempty of even cardinality,

∃ F minimum connected T-join  ⟺  {μG∣T is a tree metric, and for its minimal realization (A,g), T′:=g(T):A is a T′-join,∃ φ:V(A)→V(G) isometry with φ(g(t))=t (t∈T).\exists\,F\ \text{minimum connected }T\text{-join} \iff \begin{cases}\mu_G|_T \text{ is a tree metric, and for its minimal realization }(A,g),\ T':=g(T):\\ A \text{ is a } T'\text{-join},\\ \exists\,\varphi:V(A)\to V(G)\ \text{isometry with } \varphi(g(t))=t\ (t\in T).\end{cases}

The conditions are required of every minimal realization; all of them are isomorphic.

Milestones

  1. (p. 389) A minimal TT-join is the edge-disjoint union of ∣T∣/2|T|/2 paths pairing the vertices of TT.
  2. (p. 391) In every realization of μ\mu, the distance from g(x)g(x) to the g(y)g(y)–g(z)g(z) path equals 12(μ(x,y)+μ(x,z)−μ(y,z))\tfrac12(\mu(x,y)+\mu(x,z)-\mu(y,z)).
  3. (p. 391) A tree metric has an inclusionwise minimal realization, unique up to an isomorphism respecting the realization maps.
  4. (Lemma 2, p. 392) A connected TT-join FF is minimum if and only if FF is a tree and μF=μG\mu_F=\mu_G on V(F)V(F).
  5. (p. 392) If AA is a T′T'-join and φ\varphi an isometry from AA to GG extending g−1g^{-1}, the image of AA under φ\varphi is a TT-join that is a tree with μF=μG\mu_F=\mu_G on V(F)V(F).

Significance

Theorem 6 turns the existence of a connected minimum TT-join, a question about all TT-joins of GG, into conditions on the finite metric μG∣T\mu_G|_T alone plus one isometric embedding of a tree into GG. Tree metrics can be recognized and their minimal realization constructed efficiently (Buneman 1974), and the embedding problem is the one solved in §2 of the paper, since T′T' contains all leaves of AA. The authors deduce that connected minimum TT-joins can be found in polynomial time, which contrasts with the NP-completeness of the same question for kk components. A consequence stated in the paper: if the minimal realization of μG∣T\mu_G|_T is not a T′T'-join, then no minimum TT-join is connected.

The result is proved in the paper. No machine-checked version of Theorem 6, of Lemma 2, or of the uniqueness of minimal tree realizations is known to exist; Mathlib has graph distances, trees and walks, but neither TT-joins nor tree metrics. The mission produces these definitions and a formal proof of the characterization; the complexity consequence is out of scope.

Difficulty

The central difficulty is in the necessity direction. A connected minimum TT-join FF is itself a minimal realization of μG∣T\mu_G|_T (Lemma 2), so FF satisfies the conditions; but the conditions concern the minimal realization, and transferring them from FF to an arbitrary minimal realization requires that minimal realizations are unique up to a label-preserving isomorphism. That uniqueness (milestone 3) is the step where the obvious approach stops: it is a statement about all trees realizing a metric, not about the graph GG.

Formalization scope

  • Graphs are SimpleGraph V with [Fintype V] [DecidableEq V]; G.Connected is a hypothesis of every statement about GG (SimpleGraph.dist is 00 on unreachable pairs). Distances are natural numbers (SimpleGraph.dist).
  • Edge sets are Finset (Sym2 V). Connectivity, the tree property and μF\mu_F refer to the graph with edge set FF induced on V(F)V(F), not on all of VV.
  • "Minimum" is "∣F∣≤∣F′∣|F|\le|F'| for every TT-join F′F'", never an infimum over N\mathbb N.
  • A realization is a tree on Fin N together with a map g:X→g:X\to Fin N; this avoids quantifying over a universe. A tree metric must satisfy μ(x,y)=0⇒x=y\mu(x,y)=0\Rightarrow x=y.
  • "The unique minimal realization" is encoded by quantifying over all inclusionwise minimal realizations. A goal that only asks for some minimal realization satisfying the conditions is a different, weaker statement (its necessity half needs no uniqueness) and is not this mission's target.
  • T≠∅T\neq\emptyset is added: for T=∅T=\emptyset the minimum TT-join is empty and its connectivity is only a convention.
  • "ff is the inverse of gg and φ\varphi extends ff" is encoded as φ(g(t))=t\varphi(g(t))=t. Isometries preserve all distances, not only adjacency.
  • Halving and subtraction (milestone 2) are multiplied out.

Reusable beyond this mission: the TT-join vocabulary, the path decomposition of minimal TT-joins, and tree metrics with the uniqueness of minimal realizations. Contributions to any milestone are welcome, as are alternative proofs of milestone 3.

Selected references

9 thms1 active userReviewed
Complexity TheoryGraph TheoryOperations Research·Captain: mikedeng1

On Metric Generators of Graphs 2: The Gadget Graph of a 3-Dimensional Matching Instance Has a Minimum T-Join With at Most q Components Exactly When a Matching ExistsResearch Paper

Motivation

Let GG be a connected graph and TT a set of vertices of even cardinality. A TT-join is a set of edges FF in which exactly the vertices of TT have odd degree. A TT-cut is a cut δ(X)\delta(X) with ∣X∩T∣|X\cap T| odd. Write τ(G,T)\tau(G,T) for the minimum size of a TT-join and ν(G,T)\nu(G,T) for the maximum number of pairwise disjoint TT-cuts. Every TT-cut meets every TT-join, so ν(G,T)≤τ(G,T)\nu(G,T)\le\tau(G,T). When equality holds is a central question of combinatorial optimization because of its links to integral multiflows. Seymour (1981) proved equality for all TT in bipartite graphs. Middendorf and Pfeiffer (1998) showed that deciding equality is NP-complete.

Korach and Penn (1992) proved that a minimum TT-join FF with kk connected components satisfies

τ(G,T)−k+1 ≤ ν(G,T) ≤ ∣F∣.\tau(G,T)-k+1\ \le\ \nu(G,T)\ \le\ |F|.

So a minimum TT-join with few components certifies a large packing of TT-cuts, and a connected one certifies ν=τ\nu=\tau. Sebő and Tannier (Math. Oper. Res. 2004) therefore study the problem MTSC: given GG, TT and an integer kk, is there a minimum TT-join with at most kk connected components? They show it can be solved in polynomial time for k=1k=1 and is NP-complete in general (their Theorem 5). The hardness proof reduces three-dimensional matching (3DM) to MTSC. This mission formalizes the correctness of that reduction.

Setting

Three-dimensional matching. An instance consists of three pairwise disjoint sets WW, XX, YY, each of cardinality qq, and a set of triples H⊆W×X×YH\subseteq W\times X\times Y. A matching is a subset M⊆HM\subseteq H in which every element of W∪X∪YW\cup X\cup Y occurs in exactly one triple.

The graph GG. Take a further set ZZ of qq points and put T:=W∪X∪Y∪ZT:=W\cup X\cup Y\cup Z, so ∣T∣=4q|T|=4q. The graph GG has as vertices the points of TT, the triples of HH, and one new vertex pabp_{ab} for every unordered pair {a,b}\{a,b\} of distinct points of TT. Its edges are:

  1. a paba\,p_{ab} and pab bp_{ab}\,b for every such pair, so any two points of TT are joined by a path of length 2;
  2. hwhw, hxhx, hyhy and hzhz for every h=(w,x,y)∈Hh=(w,x,y)\in H and every z∈Zz\in Z.

There are no other edges. In Lean, GG is gadget q H and TT is gadgetT q H.

TT-joins and components. For F⊆E(G)F\subseteq E(G) and a vertex vv, deg⁡F(v)\deg_F(v) is the number of edges of FF at vv. FF is a TT-join (IsTJoin) if deg⁡F(v)\deg_F(v) is odd exactly for v∈Tv\in T. It is a minimum TT-join (IsMinTJoin) if no TT-join of GG is smaller. The connected components of FF are those of the graph (V(F),F)(V(F),F), where V(F)V(F) is the set of endpoints of edges of FF. Their number is numComponents F.

Formalization targets

Goal: the Claim in the proof of Theorem 5 (p. 391)

∃ F minimum T-join of G with at most q components  ⟺  ∃ M⊆H a matching.\exists\,F \text{ minimum } T\text{-join of } G \text{ with at most } q \text{ components}\quad\iff\quad \exists\,M\subseteq H \text{ a matching.}

This statement is quantified over every qq and every HH, and it is the full mathematical content of the reduction.

Milestones (p. 391, in the order the proof uses them)

  1. Every TT-join FF of GG has ∣F∣≥4q|F|\ge 4q, with equality iff each t∈Tt\in T lies in exactly one edge of FF.
  2. If MM is a matching, ZZ can be indexed as {zm:m∈M}\{z_m: m\in M\}, and for every such indexing ⋃m=(w,x,y)∈M{mw,mx,my,mzm}\bigcup_{m=(w,x,y)\in M}\{mw,mx,my,mz_m\} is a minimum TT-join with exactly qq components.
  3. Every minimum TT-join FF has ∣F∣=4q|F|=4q, and each t∈Tt\in T lies in exactly one edge of FF.
  4. Every minimum TT-join has at least qq components. It has exactly qq iff each component contains a vertex of HH and exactly one vertex of each of WW, XX and YY.

Significance

The result. The Claim shows that minimizing the number of components of a minimum TT-join is NP-hard. A Korach–Penn certificate for a large packing of TT-cuts therefore cannot in general be found by optimizing the component count. This sets the k=1k=1 case, which Sebő and Tannier solve in polynomial time through isometric embeddings of tree metrics, apart from the general case.

Formalizing it. The Claim is proved in the paper, in one paragraph. No machine-checked version is known, and the platform has no TT-join library. The mission produces a reusable vocabulary for TT-joins, minimum TT-joins and the components of an edge set, together with a checked proof that a concrete gadget is correct. One sentence of the published argument is false as written (see Difficulty); a formal proof settles the conclusion independently of it.

Difficulty

The direction from a matching to a TT-join is a direct verification. The converse has to control an arbitrary minimum TT-join: its size, the shape of each of its components, and how the components meet WW, XX and YY. A first reading of the printed proof suggests that every vertex outside TT that carries edges of FF is adjacent to at most one vertex of each of WW, XX, YY. This is false for the inner vertex of a path joining two vertices of the same class, and the construction joins every pair of points of TT, including pairs inside WW. Such components really occur in minimum TT-joins, so the count of components has to cover them as well. The stated conclusion (at least qq components, with equality only in the matching-like configuration) remains true.

On the Lean side, the components of an edge set are not the components of the graph with that edge set on all vertices: there every untouched vertex would be a component, and the Claim would become false.

Formalization scope

  • 3DM. WW, XX, YY are three copies of {0,…,q−1}\{0,\dots,q-1\} (Fin q), so their disjointness holds by construction. HH and MM are finite sets of triples in Fin q × Fin q × Fin q. IsMatching q M requires each element of each class to be the corresponding coordinate of exactly one triple of MM, and M⊆HM\subseteq H is a separate hypothesis. A covering-only or at-most-one version would be a different problem.
  • The graph. Its vertex type has three kinds of vertices: TT-vertices (i,j)(i,j) with class i∈{0,1,2,3}i\in\{0,1,2,3\} (W,X,Y,ZW,X,Y,Z), one midpoint per non-diagonal unordered pair of TT-vertices, and one vertex per element of HH. The adjacency is exactly the two bullets of p. 390. The graph is fixed by the definition, not described by properties.
  • TT-joins. Edges are unordered pairs (Sym2) and FF is a Finset of edges of GG. Parity uses deg⁡F\deg_F. Minimality is "∣F∣≤∣F′∣|F|\le|F'| for all TT-joins F′F'", never an infimum on N\mathbb N.
  • Components. A component of FF is a component of the graph with edge set FF that contains an endpoint of an edge of FF. Isolated vertices are never counted, and the empty edge set has 00 components.
  • The degenerate case q=0q=0 is included: the graph is empty, F=∅F=\emptyset is a minimum TT-join with 00 components, and M=∅M=\emptyset is a matching.
  • Not formalized. Membership of MTSC in NP, polynomial-time computability of the construction, and NP-completeness itself. The platform has no complexity-theory substrate. The Claim is the mathematical statement those rest on.
  • Ruled out. The Claim must not be weakened to "exactly qq components" or to minimality among TT-joins with few components, and components must not be counted on the whole vertex type. Each of these changes the statement.

Contributions welcome: proofs of the milestones, general lemmas on TT-joins (a TT-join in a graph where TT is independent has at least ∣T∣|T| edges), and lemmas on the components of an edge set, which are reusable well beyond this mission.

Selected references

  • A. Sebő, E. Tannier, On Metric Generators of Graphs, Mathematics of Operations Research 29(2):383–393, 2004. https://doi.org/10.1287/moor.1030.0070
  • E. Korach, M. Penn, Tight integral duality gap in the Chinese postman problem, Mathematical Programming 55:183–191, 1992.
  • P. D. Seymour, On odd cuts and plane multicommodity flows, Proceedings of the London Mathematical Society 42:178–192, 1981.
  • M. Middendorf, F. Pfeiffer, On the complexity of the edge-disjoint path problem, Combinatorica (cited by Sebő and Tannier as 1998, vol. 8, pp. 103–116) — NP-completeness of deciding ν=τ\nu=\tau.
  • M. R. Garey, D. S. Johnson, Computers and Intractability, W. H. Freeman, San Francisco, 1979 — NP-completeness of 3DM.
  • A. Frank, A survey on T-joins, T-cuts, and conservative weightings, in Combinatorics, Paul Erdős is Eighty, Vol. 2, 1996, pp. 213–252.
  • Related platform item, not reused: UnrelatedSched.ThreeHalves.ThreeDimMatching (Lenstra–Shmoys–Tardos) encodes 3DM with an indexed family of triples and the covering form of a matching, a different encoding from the paper's set HH with "exactly one".
8 thms1 active userReviewed
Graph TheoryOperations Research·Captain: mikedeng1

On Metric Generators of Graphs 1: An Isometry Given on a Strong Metric Generator T of H, With H − T a Forest, Extends to All of H Exactly When H Has a Representation in GResearch Paper

Motivation

A set of vertices TT of a graph is a metric generator when every vertex is determined by its vector of distances to the elements of TT. The minimum size of such a set is the metric dimension, studied in graph theory since the 1970s and surveyed by Chartrand, Eroh, Johnson and Oellermann (Discrete Appl. Math. 2000). Metric generators also appear in combinatorial search, where identifying a vertex from distance queries is the same as weighing false coins.

Sebő and Tannier (Math. Oper. Res. 2004) ask a converse question. Suppose an isometric copy of TT is already placed inside a second graph GG. When does that placement extend to an isometric embedding of the whole graph HH into GG? With T=∅T=\emptyset the question contains clique detection and is NP-hard (p. 385), so the interest lies in hypotheses on TT that make it tractable. The paper's answer, Theorem 4, is the tool behind its main application: deciding whether a graph has a connected minimum TT-join (§3.2), a question raised by Frank (1996).

Setting

All graphs are finite, simple, undirected and connected. For a graph GG, μG(x,y)\mu_G(x,y) is the number of edges of a shortest path between xx and yy.

  • A vertex tt distinguishes xx and yy if μG(t,x)≠μG(t,y)\mu_G(t,x)\neq\mu_G(t,y). A set T⊆V(G)T\subseteq V(G) is a metric generator if any two distinct vertices are distinguished by some t∈Tt\in T.
  • A set S⊆V(G)S\subseteq V(G) is a strong metric generator if for every pair x,yx,y there is s∈Ss\in S such that some shortest path from ss to xx passes through yy, or some shortest path from ss to yy passes through xx.
  • An isometry from HH to GG is a map φ:V(H)→V(G)\varphi:V(H)\to V(G) with μG(φ(u),φ(v))=μH(u,v)\mu_G(\varphi(u),\varphi(v))=\mu_H(u,v) for all u,vu,v. An isometry f:(T,μH∣T)→Gf:(T,\mu_H|_T)\to G is a map defined on T⊆V(H)T\subseteq V(H) that preserves the distances between elements of TT; φ\varphi extends ff if φ(t)=f(t)\varphi(t)=f(t) for t∈Tt\in T.
  • H−TH-T is the subgraph of HH induced on V(H)∖TV(H)\setminus T.
  • Nonempty sets Cu⊆V(G)C_u\subseteq V(G) (u∈V(H)u\in V(H)) represent HH in GG with respect to TT if (i) μG(f(t),x)=μH(t,u)\mu_G(f(t),x)=\mu_H(t,u) for all t∈Tt\in T and x∈Cux\in C_u, and (ii) whenever uv∈E(H)uv\in E(H) and x∈Cux\in C_u, some y∈Cvy\in C_v is adjacent to xx in GG.
  • The candidate procedure starts from Cu(0)={v:μG(f(t),v)=μH(t,u) ∀t∈T}C^{(0)}_u=\{v:\mu_G(f(t),v)=\mu_H(t,u)\ \forall t\in T\} and C(0)=⋃uCu(0)C^{(0)}=\bigcup_u C^{(0)}_u. It then repeatedly deletes from C(i)C^{(i)} every xx that lies in some Cu(i)C^{(i)}_u but has no neighbour in Cv(i)C^{(i)}_v for some neighbour vv of uu, and sets Cu(i+1)=Cu(i)∩C(i+1)C^{(i+1)}_u=C^{(i)}_u\cap C^{(i+1)}. Finally Cu∗:=Cu(n)C^*_u:=C^{(n)}_u with n=∣V(G)∣n=|V(G)|.

In Lean these are IsMetricGenerator, IsStrongMetricGenerator, IsIsometry, IsIsometryOn, Extends, Represents, candSet, cand and cStar in the namespace MetricGenerators.IsometryExt.

Formalization targets

Goal: Theorem 4 (p. 388)

Let TT be a strong metric generator of HH with H−TH-T a forest, and f:(T,μH∣T)→Gf:(T,\mu_H|_T)\to G an isometry. Then

∃ fˉ isometry H→G extending f  ⟺  ∃ (Cu)u∈V(H) representing H in G w.r.t. T,\exists\,\bar f \text{ isometry } H\to G \text{ extending } f\iff \exists\,(C_u)_{u\in V(H)} \text{ representing } H \text{ in } G \text{ w.r.t. } T,

and if fˉ\bar f exists, (Cu∗)u(C^*_u)_u is a representation with Cu⊆Cu∗C_u\subseteq C^*_u for every representation (Cu)u(C_u)_u, so it is the unique inclusionwise maximal one.

Milestones

  1. A strong metric generator is a metric generator (p. 386).
  2. The Cu(0)C^{(0)}_u are pairwise disjoint and Ct(0)={f(t)}C^{(0)}_t=\{f(t)\} for t∈Tt\in T (p. 387).
  3. C(0)⊇C(1)⊇⋯C^{(0)}\supseteq C^{(1)}\supseteq\cdots stabilizes after at most ∣V(G)∣|V(G)| steps (p. 387).
  4. In a representation, Ct={f(t)}C_t=\{f(t)\} and the CuC_u are pairwise disjoint (p. 387).
  5. Lemma 1 (p. 387): in a representation, for all u,vu,v and x∈Cux\in C_u,
μH(u,v)=μG(x,Cv):=min⁡y∈CvμG(x,y).\mu_H(u,v)=\mu_G(x,C_v):=\min_{y\in C_v}\mu_G(x,y).
  1. Every representation satisfies Cu⊆Cu∗C_u\subseteq C^*_u (proof of Theorem 4, p. 388).

A further theorem states the criterion behind Corollary 1 (p. 389): an extension exists iff every Cu∗C^*_u is nonempty.

Significance

Theorem 4 turns a global question (does an isometric embedding with prescribed values on TT exist?) into a local one about adjacencies among candidate sets, and the procedure C(i)C^{(i)} settles it in at most ∣V(G)∣|V(G)| rounds. In §3.2 of the paper the theorem is applied to a tree HH with TT its set of leaves (all but one leaf forms a strong metric generator, Theorem 3), and this yields the characterization and polynomial-time recognition of graphs with a connected minimum TT-join. Without the forest hypothesis the characterization fails: Figure 2 of the paper gives a representation, with a triangle in H−TH-T, for which no extension exists.

The result is proved in the paper. To our knowledge none of it has a machine-checked proof: Mathlib has graph distances (SimpleGraph.dist), acyclicity and induced subgraphs, but no metric generators, no isometry-extension results and no metric dimension. A formal proof would provide that vocabulary and a verified decision criterion. It would also be the first step towards formalizing the TT-join application of the same paper.

Difficulty

The necessity half and the maximality of C∗C^* are bookkeeping. The difficulty is sufficiency: from a representation one must build an actual isometry. The obvious idea is to pick any cu∈Cuc_u\in C_u for every uu, but this fails: two independently chosen candidates for adjacent vertices need not be adjacent, and condition (ii) only guarantees some adjacent partner. The choices must be coordinated along H−TH-T. Even with coordinated choices, the distance between images must be bounded above along every shortest path of HH, including paths that leave one component of H−TH-T, pass through TT, and return. Figure 2 shows that without the forest hypothesis no such choice need exist. Lemma 1 supplies the matching lower bound, and its proof needs the strong generator property, not just the metric-generator property.

Formalization scope

  • Vertex types are Fintypes; graphs are SimpleGraphs, and both HH and GG are assumed Connected in every statement. SimpleGraph.dist is N\mathbb N-valued and equals 00 on unreachable pairs, so connectivity is load-bearing.
  • TT is a Finset of vertices of HH; ff is a function on the subtype of TT, so it has no values outside TT.
  • "A shortest path from ss to xx contains yy" is encoded as μ(s,x)=μ(s,y)+μ(y,x)\mu(s,x)=\mu(s,y)+\mu(y,x), which is equivalent in a connected graph.
  • An isometry preserves all distances; a graph homomorphism is not an isometry.
  • H−TH-T is H.induce (↑T)ᶜ, and "forest" is IsAcyclic. T=V(H)T=V(H) is allowed.
  • Candidate sets are Sets; the recursion follows the page's union form, and C∗C^* is the stage ∣V(G)∣|V(G)|.
  • The nonemptiness of every CuC_u is part of Represents. Without it the empty family would represent every HH and the right-hand side of the goal would be trivially true. "Unique inclusionwise maximal" is stated as "a representation containing every representation".
  • Lemma 1's minimum is stated as attained plus a lower bound, without sInf.
  • No complexity statement (polynomial time, NP ∩ coNP) is formalized.

Reusable infrastructure: metric generators and strong metric generators of graphs, isometries between graph metrics, and lemmas relating SimpleGraph.dist to shortest paths through a vertex. Contributions are welcome on any milestone and on general SimpleGraph.dist lemmas they need.

Selected references

  • A. Sebő and E. Tannier, On Metric Generators of Graphs, Mathematics of Operations Research 29(2):383–393, 2004. https://doi.org/10.1287/moor.1030.0070
  • G. Chartrand, L. Eroh, M. A. Johnson and O. R. Oellermann, Resolvability in graphs and the metric dimension of a graph, Discrete Applied Mathematics 105:99–113, 2000. https://doi.org/10.1016/S0166-218X(00)00198-0
  • A. Frank, A survey on T-joins, T-cuts, and conservative weightings, in Combinatorics, Paul Erdős is Eighty, Vol. 2, Bolyai Society Mathematical Studies, 1996, pp. 213–252.
9 thms1 active userReviewed
Graph TheoryProbability·Captain: mikedeng1

The Diameter of a Scale-Free Random Graph: For m ≥ 2, Almost Every G_mⁿ Is Connected with Diameter Between (1−ε) log n/log log n and (1+ε) log n/log log nResearch Paper

Motivation

Barabási and Albert (Science 1999) proposed preferential attachment as a mechanism behind the heavy-tailed degree distributions observed in the web graph and other networks: vertices arrive one at a time and attach to existing vertices with probability proportional to their degree. Empirical work on such networks reported that typical distances are very small compared with their size. The original description left the model underdetermined (the joint law of the mm edges of a new vertex was not specified), so its distances could not be analysed as stated.

Bollobás and Riordan (Combinatorica 2004) fixed a precise version of the model, the LCD model, and determined its diameter: for m≥2m\ge2 edges per vertex it is asymptotically log⁡n/log⁡log⁡n\log n/\log\log n. For m=1m=1 the graph is a forest (with loops), and a result of Pittel states essentially that its diameter is of order log⁡n\log n. Together with the degree-sequence analysis of Bollobás, Riordan, Spencer and Tusnády (Random Struct. Alg. 2001), the paper is one of the first rigorous results on a scale-free random graph model.

Setting

The process G1NG_1^N. Vertices are 1,…,N1,\dots,N. Vertex tt sends a single edge to a vertex gt∈{1,…,t}g_t\in\{1,\dots,t\}, chosen given the past with

P(gt=i)=dG1t−1(i)2t−1 (i<t),P(gt=t)=12t−1,\mathbb P(g_t=i)=\frac{d_{G_1^{t-1}}(i)}{2t-1}\ (i<t),\qquad \mathbb P(g_t=t)=\frac1{2t-1},

where dG1t−1(i)d_{G_1^{t-1}}(i) is the degree of ii in the graph built so far (a loop counts twice). Loops (gt=tg_t=t) are allowed.

The graph GmnG_m^n. Run G1mnG_1^{mn} and identify the vertices (k−1)m+1,…,km(k-1)m+1,\dots,km into a single vertex kk, for k=1,…,nk=1,\dots,n. The resulting random graph on [n][n] is Gmn∈GmnG_m^n\in\mathcal G_m^n. The paper's graph has loops and multiple edges; its diameter is the largest graph distance between two vertices of the underlying simple graph.

Almost every. For fixed mm, a.e. GmnG_m^n has a property if its probability tends to 11 as n→∞n\to\infty. All logarithms are natural.

The endpoint model (for the upper bound). Let r1,…,rmnr_1,\dots,r_{mn} be independent with density 2x2x on (0,1)(0,1) (M2(0,1)M_2(0,1)), R1≤⋯≤RmnR_1\le\dots\le R_{mn} their sorted values, Wi=RmiW_i=R_{mi}, W0=0W_0=0, wi=Wi−Wi−1w_i=W_i-W_{i-1}. Given 0<W1<⋯<Wn<10<W_1<\dots<W_n<1, the random graph G(W1,…,Wn)G(W_1,\dots,W_n) joins each vertex ii to li,1l_{i,1} and li,2l_{i,2}, independent with PL(li,j=k)=wk/Wi\mathbb P_L(l_{i,j}=k)=w_k/W_i for k≤ik\le i. The events E1,…,E5E_1,\dots,E_5 (Lemma 7) say that the WiW_i follow the profile i/n\sqrt{i/n} and that the spacings wiw_i are neither too small nor too large in specified ranges.

Formalization targets

Goal: Theorem 1

For fixed m≥2m\ge2 and ε>0\varepsilon>0, a.e. GmnG_m^n is connected and

(1−ε)log⁡nlog⁡log⁡n≤diam⁡(Gmn)≤(1+ε)log⁡nlog⁡log⁡n.(1-\varepsilon)\frac{\log n}{\log\log n}\le\operatorname{diam}(G_m^n)\le(1+\varepsilon)\frac{\log n}{\log\log n}.

Lower bound (§4)

  • Lemma 2: P(gj=i)=O((ij)−1/2)\mathbb P(g_j=i)=O((ij)^{-1/2}) and P(gj=i,gk=i)=O(i−1(jk)−1/2)\mathbb P(g_j=i,g_k=i)=O(i^{-1}(jk)^{-1/2}) with absolute constants.
  • Lemma 3: events ⋂{gjs=is}\bigcap\{g_{j_s}=i_s\} with disjoint sets of targets are negatively correlated.
  • Lemma 4: P(S⊂G1N)≤Ce(S)∏ij∈E(S)1/ij\mathbb P(S\subset G_1^N)\le C^{e(S)}\prod_{ij\in E(S)}1/\sqrt{ij} for graphs SS with at most one earlier and two later neighbours per vertex.
  • Theorem 5: for every m≥1m\ge1, a.e. GmnG_m^n has diam⁡(Gmn)>log⁡n/log⁡(3Cm2log⁡n)\operatorname{diam}(G_m^n)>\log n/\log(3Cm^2\log n), CC the constant of Lemma 4.

Upper bound (§§5–8)

  • Lemma 6: Chernoff–Janson tails for sums of independent Bernoulli variables.
  • Lemma 7: P(Er)→1\mathbb P(E_r)\to1 for r=1,…,5r=1,\dots,5.
  • The coupling of §6: G(W)G(W) with Wi=RmiW_i=R_{mi} is stochastically dominated by GmnG_m^n in the subgraph order, i.e. P(G(W)∈P)≤P(Gmn∈P)\mathbb P(G(W)\in\mathcal P)\le\mathbb P(G_m^n\in\mathcal P) for every property P\mathcal P preserved under adding edges.
  • Lemma 10 and Lemma 8: under E1,…,E5E_1,\dots,E_5, every vertex reaches a useful vertex (i≤n/(log⁡n)5i\le n/(\log n)^5, wi≥(log⁡n)2/nw_i\ge(\log n)^2/n) by a descending path of length at most 8log⁡log⁡n8\log\log n, with probability 1−o(1)1-o(1).
  • Lemma 12 (a deterministic growth estimate) and Lemma 11: a useful vertex is joined to vertex 11 by a path of length at most (1/2+ε)log⁡n/log⁡log⁡n(1/2+\varepsilon)\log n/\log\log n with probability 1−o(n−1)1-o(n^{-1}).
  • The display of p. 29: under E1,…,E5E_1,\dots,E_5, PL(diam⁡G(W)>(1+ε/2)log⁡n/log⁡log⁡n+16log⁡log⁡n)=o(1)\mathbb P_L\big(\operatorname{diam}G(W)>(1+\varepsilon/2)\log n/\log\log n+16\log\log n\big)=o(1).

Significance

The theorem shows that the diameter of this scale-free graph is smaller by a factor log⁡log⁡n\log\log n than that of a classical random graph with the same constant average degree, and identifies m=1m=1 versus m≥2m\ge2 as the dividing line. It made the "small world" claims about the Barabási–Albert model precise for one exact version of it, and the LCD representation and the endpoint model introduced here were used in later work on preferential attachment.

The result is proved in the paper; nothing here is open. The work of the mission is formalizing the known proof. As far as is known, no machine-checked development of preferential-attachment graphs exists in Mathlib or elsewhere. A complete development would supply a reusable probability space for the attachment process, a Chernoff–Janson inequality for heterogeneous Bernoulli sums, a negative-correlation lemma for the process, and order-statistic estimates for i.i.d. samples, each of independent use.

Difficulty

The lower bound is a first-moment count of short paths, but the edges of G1NG_1^N are not independent: an earlier edge into a vertex raises the chance of later ones. Lemmas 2–4 show that small subgraphs still appear with probability comparable to an independent model with edge probabilities C/ijC/\sqrt{ij}; Lemma 3 requires a description of the process in which the needed independence is visible.

The upper bound is the hard half. A naive breadth-first expansion from a vertex fails: the weight of the next neighbourhood has the right mean but a very skewed distribution, and vertices near the end of the ordering have few early neighbours. The paper replaces the process by a conditionally independent model given the sorted endpoints WiW_i, controls the WiW_i globally (Lemma 7), handles late vertices separately (Lemmas 8–10), and runs a weighted expansion with a growing blow-up factor (Lemmas 11–12). Each step needs uniformity in WW: every o(⋅)o(\cdot) must depend on nn only.

Formalization scope

Vertices are stored as Fin N (0-based) and statements read 1-based labels through the accessors tgt and lab. A sequence (gt)(g_t) is a dependent function (t : Fin N) → Fin (t+1), its probability is the product of the exact conditional factors (1+#{s<t:gs=gt})/(2t−1)(1+\#\{s<t: g_s=g_t\})/(2t-1), and probabilities are finite weighted sums. G1NG_1^N, GmnG_m^n and G(W)G(W) are Mathlib simple graphs: loops and multiple edges are dropped, which does not change connectivity or distances. The model is the paper's: not uniform attachment, not mm independent choices per vertex, and with the self-loop term.

diam⁡\operatorname{diam} in the goal is SimpleGraph.diam, which is 00 on a disconnected graph; the goal therefore keeps connectivity explicit, as the page does. Every other diameter bound uses "every two vertices are joined by a walk of length ≤x\le x", and lower bounds use its negation, so a disconnected graph never satisfies an upper bound by default. Hidden constants follow the paper's quantifier order: the constants of Lemmas 2 and 4 come before every index; each o(⋅)o(\cdot) of §§7–8 is a function δ(n)→0\delta(n)\to0 chosen before WW (a bound chosen after WW would make these statements nearly empty); "for nn sufficiently large" is ∃N0\exists N_0 before WW or ff. Theorem 5 assumes the bound of Lemma 4 for its constant CC. Every statement about G(W)G(W) assumes 0=W0<W1<⋯<Wn<10=W_0<W_1<\dots<W_n<1. Lemma 7 is stated as "the probability of the complement tends to 00" under the product law of M2(0,1)M_2(0,1); the coupling is stated as the equivalent stochastic-domination inequality for every property preserved under adding edges.

Not formalized: Lemma 9 (a conditional bound given the history of a breadth-first exploration), the LCD representation of G1nG_1^n (§2), and Theorem 13 (m=1m=1), which the paper states without proof.

Contributions welcome: proofs of any milestone, the identity P(gj=i)=μj−1,i/(2j−1)\mathbb P(g_j=i)=\mu_{j-1,i}/(2j-1) with μt,i=∏s=it(1+1/(2s−1))\mu_{t,i}=\prod_{s=i}^t(1+1/(2s-1)), the LCD representation, and general lemmas about the attachment process and Bernoulli tails.

Selected references

15 thms1 active userReviewed
Graph Theory·Captain: mikedeng1

Graph Minors XXIII. Nash-Williams' Immersion Conjecture: In Every Infinite Sequence of Finite Graphs, Some Graph Is Immersed in a Later OneResearch Paper

Motivation

A well-quasi-order is a reflexive, transitive relation in which every infinite sequence x1,x2,…x_1,x_2,\dots contains a pair i<ji<j with xi≤xjx_i\le x_j. Showing that a class of finite combinatorial objects is well-quasi-ordered by a containment relation is a standard way to prove that every property closed under that containment is characterised by finitely many forbidden objects. The best-known instance is the Graph Minor Theorem (Wagner's conjecture), completed by Robertson and Seymour in Graph Minors XX (JCTB 92, 2004).

Nash-Williams proposed the analogous conjecture for a different containment, immersion, in which edges of the smaller graph are mapped to edge-disjoint paths of the larger graph. Graph Minors XXIII (JCTB 100, 2010) proves it by deriving a general well-quasi-ordering theorem for labelled hypergraphs from the machinery of Graph Minors XX.

Timeline.

  • 1963 (published 1964): Nash-Williams conjectures that finite graphs are well-quasi-ordered by immersion ([Theory of Graphs and Its Applications, Smolenice 1963, pp. 83–84]).
  • 1965: Nash-Williams proposes a second, "strong" immersion conjecture, in which the image paths may not pass through images of non-incident vertices (Proc. Cambridge Philos. Soc. 61).
  • 2004: Graph Minors XX proves Wagner's conjecture: finite graphs are well-quasi-ordered by minors.
  • 2010: Graph Minors XXIII proves the (weak) immersion conjecture together with a labelled hypergraph generalisation. The paper states that it does not prove the strong conjecture.

Setting

All graphs and hypergraphs are finite. A graph GG has a vertex set V(G)V(G), an edge set E(G)E(G), and for each edge an unordered pair of ends; an edge with equal ends is a loop, and several edges may have the same ends (parallel edges). A graph is loopless if no edge is a loop. A path has at least one vertex and no repeated vertices; a circuit has at least one edge and no repeated vertices, so a loop and a pair of parallel edges are circuits.

An immersion of HH in GG is a map α\alpha on V(H)∪E(H)V(H)\cup E(H) such that α\alpha is injective on vertices; every non-loop edge ee with ends u,vu,v goes to a path α(e)\alpha(e) of GG with ends α(u),α(v)\alpha(u),\alpha(v); every loop at vv goes to a circuit α(e)\alpha(e) of GG through α(v)\alpha(v); and α(e)\alpha(e), α(f)\alpha(f) share no edge when e≠fe\ne f.

A hypergraph GG has finite sets V(G)V(G), E(G)E(G) and an incidence relation; V(e)V(e) is the set of ends of the edge ee, of any size. Write KVK_V for the complete graph on VV. A collapse of GG to HH maps each vertex vv of HH to a non-null connected subgraph η(v)\eta(v) of KV(G)K_{V(G)}, pairwise vertex-disjoint, and each edge ee of HH injectively to an edge η(e)\eta(e) of GG, so that η(e)\eta(e) meets η(v)\eta(v) whenever ee is incident with vv, and every edge xyxy of every η(v)\eta(v) is covered by some edge of GG incident with both xx and yy. The transpose of a graph GG is the hypergraph with vertex set E(G)E(G), edge set V(G)V(G) and the same incidence.

A quasi-order Ω\Omega is an ideal of Ω′\Omega' if it is a sub-quasi-order closed downwards in Ω′\Omega'; a shadow is a tuple (Ω∞,m,Ωm,…,Ω1,R2,R1)(\Omega_\infty,m,\Omega_m,\dots,\Omega_1,R_2,R_1) of well-quasi-orders and finite sets, ordered lexicographically (Section 3 of the paper).

Formalization targets

Goal: Nash-Williams' immersion conjecture (1.1)

∀ (Gi)i≥1 finite graphs:∃ j>i≥1,  Gi is immersed in Gj.\forall\,(G_i)_{i\ge1}\text{ finite graphs}:\quad \exists\, j>i\ge1,\ \ G_i \text{ is immersed in } G_j .

Milestones, in the order the proof uses them

  • 3.1 No sequence Ω1,Ω2,…\Omega_1,\Omega_2,\dots with Ω1\Omega_1 a well-quasi-order and Ωi+1\Omega_{i+1} a proper ideal of Ωi\Omega_i for all ii.
  • 3.2 No sequence of shadows with Σi+1<Σi\Sigma_{i+1}<\Sigma_i for all ii.
  • 1.6 For a well-quasi-order Ω\Omega and hypergraphs GiG_i with edge labels ϕi\phi_i, distinguished edges MiM_i of at most kk ends and orderings μi(e)\mu_i(e) of their ends, some j>ij>i admit a collapse η\eta of GjG_j to GiG_i with ϕi(e)≤ϕj(η(e))\phi_i(e)\le\phi_j(\eta(e)), η(e)∈Mj  ⟺  e∈Mi\eta(e)\in M_j\iff e\in M_i, and preserving the orderings.
  • 1.4 The same with Mi=∅M_i=\emptyset: ϕi(e)≤ϕj(η(e))\phi_i(e)\le\phi_j(\eta(e)) for all edges.
  • 1.2 For every sequence of hypergraphs there is a collapse of some GjG_j to some earlier GiG_i.
  • 1.3 For loopless graphs G,HG,H, a collapse of the transpose of GG to the transpose of HH yields an immersion of HH in GG.
  • 1.5 Vertex-labelled loopless graphs: an immersion α\alpha of GiG_i in GjG_j with ϕi(v)≤ϕj(α(v))\phi_i(v)\le\phi_j(\alpha(v)).
  • 1.7 (off the goal's path) A labelled form of Wagner's conjecture for directed graphs with loops.

Significance

The immersion theorem implies that every class of finite graphs closed under taking immersions is characterised by finitely many excluded immersions. Theorem 1.6 is stronger than both 1.1 and Wagner's conjecture: it handles hypergraphs, labels from an arbitrary well-quasi-order and ordered edges, which is the form in which the Graph Minors machinery is reused by later work.

All results here are proved in the paper. None of them has a machine-checked proof: Mathlib has well-quasi-orders and Higman's lemma, but not the Graph Minor Theorem or any notion of graph immersion. The value of this mission is a faithful formal statement of the immersion theorem and of the reductions the paper performs in Section 1 (1.3 and the passage from 1.6 to 1.4, 1.5 and 1.1), each of which can be formalized independently of Graph Minors XX, plus the order-theoretic lemmas 3.1 and 3.2.

Difficulty

The reductions in Section 1 (1.3, and the passages from 1.6 to 1.4, 1.5 and 1.1) are short on paper but require a working library of multigraph walks, paths and circuits, which Mathlib does not have for graphs with loops and parallel edges. The real difficulty is 1.6, which the paper derives from a theorem on patchworks of Graph Minors XX (its 2.2) together with tangle results of Graph Minors X, and therefore rests on the structure theory of the whole Graph Minors series. No route around that theory is known: when the hypergraphs are loopless graphs, a collapse of GjG_j to GiG_i makes GiG_i a minor of GjG_j, so already 1.2 contains Wagner's conjecture. Nor does 1.2 alone give 1.1: loops cannot be routed through the transpose construction of 1.3, and the paper handles them by counting loops at each vertex as a label from the well-quasi-order N\mathbb N, which is why the labelled forms 1.4–1.6 are needed.

Formalization scope

A graph is Graph V E with ends : E → Sym2 V; a hypergraph is Hypergraph V E with inc : E → V → Prop; each lives on its own finite types, and a sequence is a family indexed by ℕ (from 00; the paper's j>i≥1j>i\ge1 becomes i<ji<j). Paths and circuits are walks with vertex and edge lists; the ends of a path are unordered. An immersion is the structure GraphImmersion H G; a collapse of GG to HH is Collapse G H, whose branch sets are Subgraphs of ⊤ : SimpleGraph V(G) (Mathlib's Subgraph.Connected includes non-emptiness). Well-quasi-orders are Mathlib's WellQuasiOrdered on a type with a preorder for 1.4–1.7, and QO.IsWQO on subsets of an ambient type for 3.1–3.2, where quasi-orders are compared by inclusion. Directed graphs for 1.7 are DirGraph V E with heads and tails.

Three trivializing formalizations are excluded: the collapse keeps condition (iv), so branch sets cannot use arbitrary pairs of vertices; immersion paths are edge-disjoint, not vertex-disjoint (which would give topological minors, not a well-quasi-order); and each graph lives on its own type, never all on one fixed finite type, which would make the goal a pigeonhole statement. Strong immersion is not stated.

Contributions welcome: proofs of 3.1, 3.2 and 1.3, the reductions 1.6 ⇒ 1.4 ⇒ 1.2 and 1.4 + 1.3 ⇒ 1.5 ⇒ 1.1, and library material on multigraph walks, paths and circuits, which is reusable beyond this mission. A proof of 1.6 would require formalizing the Graph Minors series.

Selected references

12 thms1 active userReviewed
ProbabilityTheoretical Computer Science·Captain: mikedeng1

On Lattices, Learning with Errors, Random Linear Codes, and Cryptography 4: A Random Subset Sum of l Uniform Elements of a Finite Abelian Group Is on Average Within √(|G|/2^l) of UniformResearch Paper

Motivation

Regev's On Lattices, Learning with Errors, Random Linear Codes, and Cryptography (J. ACM 56(6), 2009, Article 34; doi:10.1145/1568318.1568324) introduced the Learning with Errors (LWE) problem and built a public-key cryptosystem on it. The source for this mission is that published J. ACM article. The paper's main theorem, a quantum reduction from worst-case lattice problems to LWE, is outside this series; this mission formalizes a self-contained piece of finite combinatorics from §5.

In the cryptosystem the public key is a list of mm LWE samples, and a bit is encrypted by adding up a uniformly random subset of them. Semantic security rests on one fact: if the public key were truly uniform, the sum of a random subset of it would be close to uniform, so the ciphertext would carry no information about the bit. Claim 5.3 (p. 34:36) makes this precise for an arbitrary finite abelian group GG. It is a special case of the leftover hash lemma of Impagliazzo and Zuckerman (1989), in which the family of functions b↦∑ibigib \mapsto \sum_i b_i g_i indexed by g∈Glg \in G^l is a universal hash family. Variants of the same statement appear in the security proofs of most lattice-based encryption schemes that use random subset sums, including the dual-Regev and GPV-style constructions.

Setting

Let GG be a finite abelian group, written additively, with ∣G∣|G| elements, and let l≥0l \ge 0 be an integer. For g=(g1,…,gl)∈Glg = (g_1, \dots, g_l) \in G^l and b=(b1,…,bl)∈{0,1}lb = (b_1, \dots, b_l) \in \{0,1\}^l the subset sum ∑ibigi\sum_i b_i g_i is the sum of the gig_i with bi=1b_i = 1 (the empty subset gives 00). The distribution of the sum of a uniformly random subset of g1,…,glg_1, \dots, g_l is

Pg(h)=12l ∣{ b∈{0,1}l∣∑ibigi=h }∣,h∈G.P_g(h) = \frac{1}{2^l}\,\bigl|\{\, b \in \{0,1\}^l \mid \textstyle\sum_i b_i g_i = h \,\}\bigr|, \qquad h \in G.

The paper defines the statistical distance of two densities as ∫∣φ1−φ2∣\int |\varphi_1 - \varphi_2|, with range [0,2][0,2], and notes that the same definition applies to discrete random variables (p. 34:14). The distance of PgP_g from the uniform distribution on GG is therefore

Δ(g)=∑h∈G∣Pg(h)−1∣G∣∣,\Delta(g) = \sum_{h \in G} \Bigl| P_g(h) - \frac{1}{|G|} \Bigr|,

with no factor 12\tfrac12. Expectations and probabilities over gg refer to a uniform choice of g1,…,gl∈Gg_1, \dots, g_l \in G, that is, the uniform distribution on all ∣G∣l|G|^l tuples, repetitions allowed: Expg[F(g)]=∣G∣−l∑g∈GlF(g)\mathrm{Exp}_g[F(g)] = |G|^{-l}\sum_{g \in G^l} F(g).

In Lean these objects are RegevLWE.SubsetSum.subsetSum, P, statDistUniform and expectG.

Formalization targets

Goal: Claim 5.3

Expg[Δ(g)]≤∣G∣2landPr⁡g[Δ(g)>∣G∣/2l4]≤∣G∣2l4.\mathop{\mathrm{Exp}}_g\bigl[\Delta(g)\bigr] \le \sqrt{\frac{|G|}{2^l}} \qquad\text{and}\qquad \Pr_g\Bigl[\Delta(g) > \sqrt[4]{|G|/2^l}\Bigr] \le \sqrt[4]{\frac{|G|}{2^l}}.

Both sentences of the claim are in the goal. The second is what the security proof (Lemma 5.4, p. 34:37) uses: for all but a ∣G∣/2l4\sqrt[4]{|G|/2^l} fraction of public keys, the random subset sum is within ∣G∣/2l4\sqrt[4]{|G|/2^l} of uniform. The constants are exactly as printed.

Milestones

  1. The ℓ2\ell_2 norm as a collision probability (p. 34:36). For every gg, with b,b′b, b' independent and uniform in {0,1}l\{0,1\}^l,
∑hPg(h)2=Pr⁡b,b′[∑ibigi=∑ibi′gi]≤12l+Pr⁡b,b′[∑ibigi=∑ibi′gi∣b≠b′].\sum_{h} P_g(h)^2 = \Pr_{b,b'}\Bigl[\textstyle\sum_i b_i g_i = \sum_i b'_i g_i\Bigr] \le \frac{1}{2^l} + \Pr_{b,b'}\Bigl[\textstyle\sum_i b_i g_i = \sum_i b'_i g_i \Bigm| b \neq b'\Bigr].
  1. Collisions of distinct subsets (p. 34:37). For any b≠b′b \neq b', Pr⁡g[∑ibigi=∑ibi′gi]=1/∣G∣\Pr_g[\sum_i b_i g_i = \sum_i b'_i g_i] = 1/|G|.
  2. Expected ℓ2\ell_2 norm (p. 34:37). Expg[∑hPg(h)2]≤1/2l+1/∣G∣\mathrm{Exp}_g[\sum_h P_g(h)^2] \le 1/2^l + 1/|G|.
  3. Cauchy–Schwarz and the ℓ2\ell_2 identity (p. 34:37), pointwise in gg:
∑h∣Pg(h)−1∣G∣∣≤∣G∣1/2(∑h(Pg(h)−1∣G∣)2)1/2,∑h(Pg(h)−1∣G∣)2=∑hPg(h)2−1∣G∣.\sum_h \Bigl|P_g(h) - \frac{1}{|G|}\Bigr| \le |G|^{1/2}\Bigl(\sum_h \Bigl(P_g(h) - \frac{1}{|G|}\Bigr)^2\Bigr)^{1/2}, \qquad \sum_h \Bigl(P_g(h) - \frac{1}{|G|}\Bigr)^2 = \sum_h P_g(h)^2 - \frac{1}{|G|}.

Significance

The result. Claim 5.3 is the step in the security proof of Regev's cryptosystem that removes the public key from the picture: once the key is replaced by uniform samples (by the LWE assumption), the claim shows that an encryption is statistically close to uniform, independently of the encrypted bit. The parameter choice m≥(1+ϵ)(n+1)log⁡pm \ge (1+\epsilon)(n+1)\log p of Lemma 5.4 is exactly what makes ∣G∣/2m|G|/2^m negligible for G=Zpn×ZpG = \mathbb{Z}_p^n \times \mathbb{Z}_p. Without the claim the cryptosystem would have a hardness assumption but no reduction from it.

Formalizing it. The claim is proved, with a complete argument in the paper; nothing here is open. To our knowledge no machine-checked proof of this statement, or of the leftover hash lemma for subset-sum hash families over a general finite abelian group, exists in Mathlib or on the platform. A formal proof gives a reusable, constant-exact statement of the subset-sum leftover hash lemma with the paper's normalization of statistical distance. The four milestones are standard facts about finite averages and collision probabilities that recur in many cryptographic security proofs.

Difficulty

There is no deep step; the work is in organizing finite counting arguments without loss. Two points need care. The collision fact Pr⁡g[∑ibigi=∑ibi′gi]=1/∣G∣\Pr_g[\sum_i b_i g_i = \sum_i b'_i g_i] = 1/|G| holds for every pair b≠b′b \neq b' only because the coefficients bi−bi′b_i - b'_i lie in {−1,0,1}\{-1, 0, 1\}: for a general linear form over a group with torsion, a nonzero coefficient vector need not give a uniformly distributed sum, so an argument that treats the coefficients as arbitrary integers fails. And passing from the ℓ2\ell_2 bound to the expected ℓ1\ell_1 distance requires the exchange of expectation and square root in the right direction (concavity), which is easy to misapply. The bound must hold for every finite abelian group and every ll, including l=0l = 0 and ∣G∣=1|G| = 1, with no asymptotic slack.

Formalization scope

  • GG is any type with [AddCommGroup G] [Fintype G] [DecidableEq G]; l:Nl : ℕ, and l=0l = 0 is allowed (then PgP_g is the point mass at 00 and the claim holds). No hypothesis is added to the paper's statement: ∣G∣≥1|G| \ge 1 holds for every group.
  • {0,1}l\{0,1\}^l is encoded as Fin l → Bool; gg ranges over all functions Fin l → G, so the uniform choice of gg is over all ∣G∣l|G|^l tuples with repetition, not over ll-element subsets of GG.
  • Every expectation and probability is an exact finite average with real values: Expg[F]=∣G∣−l∑gF(g)\mathrm{Exp}_g[F] = |G|^{-l}\sum_g F(g), and Pr⁡g[E]\Pr_g[E] is the number of tuples satisfying EE divided by ∣G∣l|G|^l. Probabilities over (b,b′)(b, b') are counts over the (2l)2(2^l)^2 pairs; the conditional probability given b≠b′b \neq b' divides by (2l)2−2l(2^l)^2 - 2^l. At l=0l = 0 the paper's conditional probability is undefined; Lean's convention 0/0=00/0 = 0 makes milestone 1 read 1≤11 \le 1 there, which is consistent with the paper.
  • The statistical distance is ∑h∣Pg(h)−1/∣G∣∣\sum_h |P_g(h) - 1/|G||, without 12\tfrac12. A formalization with the 12\tfrac12-normalized total variation distance would state a weaker result (half the bound) and is excluded. "More than" in the second sentence is strict, "at most" is ≤\le. The fourth root is Real.sqrt (Real.sqrt x).
  • Milestone 4 states only the first two steps of the paper's final chain (the Cauchy–Schwarz inequality and the identity), pointwise in gg; the remaining two steps (Jensen for the square root and the substitution of milestone 3) are part of the goal. Its milestone text quotes the whole chain for context.
  • No definitions beyond the four above are needed, and no measure theory. Proofs of the milestones, and alternative proofs of the goal (for instance via Fourier analysis on GG), are welcome.

Selected references

  • O. Regev, On Lattices, Learning with Errors, Random Linear Codes, and Cryptography, Journal of the ACM 56(6), Article 34, 2009. doi:10.1145/1568318.1568324
  • R. Impagliazzo and D. Zuckerman, How to Recycle Random Bits, Proc. 30th IEEE FOCS, 248–253, 1989. doi:10.1109/SFCS.1989.63486
  • J. Håstad, R. Impagliazzo, L. A. Levin and M. Luby, A Pseudorandom Generator from any One-way Function, SIAM Journal on Computing 28(4), 1364–1396, 1999. doi:10.1137/S0097539793244708
6 thms1 active userReviewed
Graph TheoryLinear OptimizationOperations Research+1·Captain: mikedeng1

Approximating Minimum Bounded Degree Spanning Trees to within One of Optimal 2: Under Lower and Upper Degree Bounds, Iterative Rounding Finds a Connecting Tree of LP Cost within A_v − 1 and B_v + 1Research Paper

Motivation

Network design problems often ask for a cheap spanning tree in which no vertex is overloaded: in multicast and overlay networks the degree of a node bounds the number of copies it must forward, and in physical networks it bounds the number of ports. The minimum bounded degree spanning tree problem asks for a minimum-cost spanning tree whose degrees respect given bounds. Deciding whether a graph has a spanning tree of maximum degree 2 is already the Hamiltonian path problem, so exact solutions are out of reach, and the question becomes how little the bounds and the cost must be relaxed.

Some problems also impose lower bounds: a vertex that must serve as a hub, or a leaf-avoidance requirement, asks for degree at least AvA_v. Singh and Lau (STOC 2007) showed that the iterative rounding method they used for upper bounds extends to both kinds at once: a spanning tree of cost at most the LP optimum whose degree at every vertex lies in [Av−1, Bv+1][A_v-1,\,B_v+1].

Timeline. Fürer and Raghavachari (1994) found a spanning tree of maximum degree at most Δ∗+1\Delta^*+1 in the unweighted case. For costs, Goemans (FOCS 2006) obtained cost at most OPT with degrees at most Bv+2B_v+2. Singh and Lau (STOC 2007) improved this to Bv+1B_v+1, which is the best possible additive violation unless P = NP, and gave the extension to lower and upper bounds formalized here. The journal version appeared in J. ACM 62(1), 2015.

Setting

Let G=(V,E)G=(V,E) be a finite simple graph with edge costs ce∈Rc_e\in\mathbb R; no sign or triangle inequality is assumed. Let FF be a forest on VV with no edge in common with EE. A set H⊆EH\subseteq E is an FF-tree if H∪FH\cup F is a spanning tree of VV, and dH(v)d_H(v) is the number of edges of HH at vv. Integer lower bounds AvA_v are given on U⊆VU\subseteq V and integer upper bounds BvB_v on W⊆VW\subseteq V. The minimum bounded degree connecting tree problem asks for a cheapest FF-tree with Av≤dH(v)A_v\le d_H(v) on UU and dH(v)≤Bvd_H(v)\le B_v on WW; with F=∅F=\varnothing it is the spanning-tree problem.

The supernodes are the vertex sets of the components of (V,F)(V,F), isolated vertices included, and I(F)\mathcal I(F) is the family of unions of supernodes. For S⊆VS\subseteq V, E(S)E(S) and F(S)F(S) are the edges with both endpoints in SS, δ(S)\delta(S) the edges with exactly one endpoint in SS, and x(D)=∑e∈Dxex(D)=\sum_{e\in D}x_e. The linear relaxation LP-MBDCT(G,A,B,U,W,F)(G,\mathcal A,\mathcal B,U,W,F) minimizes ∑ecexe\sum_e c_ex_e subject to

x(E(V))=∣V∣−∣F(V)∣−1,x(E(S))≤∣S∣−∣F(S)∣−1 (S∈I(F)),Av≤x(δ(v)) (v∈U),x(δ(v))≤Bv (v∈W),x≥0.x(E(V))=|V|-|F(V)|-1,\quad x(E(S))\le|S|-|F(S)|-1\ (S\in\mathcal I(F)),\quad A_v\le x(\delta(v))\ (v\in U),\quad x(\delta(v))\le B_v\ (v\in W),\quad x\ge0.

MBDCT Algorithm2 (Figure 5 of the paper) repeats: if FF is a spanning tree, stop; otherwise take a basic optimal solution x∗x^*, delete the edges with xe∗=0x^*_e=0, move one edge with xe∗=1x^*_e=1 (if any) into FF and lower AA and BB by one at its endpoints, and otherwise remove from UU and WW one vertex whose support degree is at most two.

Formalization targets

Goal: Theorem 5.2

For every well-formed instance whose LP is feasible, MBDCT Algorithm2

  1. has a terminating run;
  2. makes at most ∣V∣−∣F∣−1+∣U∪W∣|V|-|F|-1+|U\cup W| iterations on every run;
  3. returns only FF-trees H⊆EH\subseteq E with
c(H)≤∑e∈Ecexe for every feasible x,Av−1≤dH(v) (v∈U),dH(v)≤Bv+1 (v∈W).c(H)\le\sum_{e\in E}c_ex_e\ \text{for every feasible }x,\qquad A_v-1\le d_H(v)\ (v\in U),\qquad d_H(v)\le B_v+1\ (v\in W).

The statement fixes no constants beyond the paper's ±1\pm1, and it is uniform over every choice of basic optimal solution, 1-edge and removed vertex.

Milestones

In the order the proof uses them: Lemma 5.3 (a basic solution is determined by a laminar family of tight sets and tight lower and upper degree rows, with ∣E∗∣=∣L∣+∣TU∣+∣TW∣|E^*|=|\mathcal L|+|T_U|+|T_W|); Claims 5.4, 5.7, 5.8 and 5.9 (special supernodes, cut sizes, the value x∗(D(S))=r−1x^*(D(S))=r-1 on the edges between the rr members of SS, and when a set is special); Lemma 5.6 (every set of L\mathcal L keeps at least three tokens, exactly three only if it is special or VV); and Lemma 5.1 (a basic solution has an edge with xe∗=1x^*_e=1 or a vertex of U∪WU\cup W with support degree two).

Significance

The theorem gives, in one algorithm, a tree that is no more expensive than the LP lower bound and whose degrees miss both bounds by at most one. For the pure upper-bound problem it implies the (1,Bv+1)(1,B_v+1) guarantee, which cannot be improved to BvB_v unless P = NP, since a Hamiltonian path is the case Bv≡2B_v\equiv 2. With lower bounds it also covers prescribed minimum degrees.

The result is proved in the paper; no machine-checked proof of it, or of any iterative rounding analysis, is known to exist. No platform item treats bounded-degree spanning trees or iterative rounding; the nearest related item is the open Williamson–Shmoys minimum-degree spanning tree local-search goal, which concerns a different, unweighted problem. Formalizing this mission requires the extreme-point structure of the spanning tree polytope with degree constraints (uncrossing to a laminar family), the token counting argument, and the induction over the algorithm's recursion, all of which are reusable for other iterative rounding results.

Difficulty

The obvious argument rounds an optimal LP solution once. It fails: an optimal vertex may be entirely fractional, and no single rounding keeps both the cost and the degrees. The algorithm instead re-solves the LP after each change, and its correctness rests on Lemma 5.1, that every extreme point of the current LP has an integral edge or a vertex with support degree two. That lemma is a counting statement about extreme points: the rank bound ∣E∗∣=∣L∣+∣TU∣+∣TW∣|E^*|=|\mathcal L|+|T_U|+|T_W| from a laminar basis must be contradicted by a token distribution. With upper bounds only, every set of the laminar family can collect four tokens. With lower bounds a set may collect only three, and the proof must characterize those sets (special sets, Definition 5.5) and show by linear independence that the remaining cases cannot occur. A second difficulty is that the guarantee concerns the final tree after many iterations, so the degree accounting must survive the changes of AA, BB, UU, WW and FF along the run.

Formalization scope

Vertices form a Fintype; edges are elements of Sym2 V with no loops, and EE, FF are finite sets of edges with FF acyclic and disjoint from EE. LP vectors are functions on Sym2 V that vanish off EE. Right-hand sides are computed in R\mathbb R, degree bounds are integers, and the subtour rows range over nonempty S∈I(F)S\in\mathcal I(F) (at S=∅S=\varnothing the literal row 0≤−10\le-1 would make the LP empty). A basic solution is a feasible xx that is the only vector on EE satisfying with equality every constraint tight at xx, including the tight rows xe=0x_e=0. Supernodes are never contracted: the paper's contraction of a supernode with one active vertex is a proof device, and all of §5.1's notions are stated on the original instance.

The paper's loose phrases are made explicit as follows.

  • "Polynomial time" becomes the iteration bound; the LP is solved by an oracle that returns any basic optimal solution. The ellipsoid method and the separation oracle are out of scope.
  • "The algorithm returns" becomes three claims: a run exists, every run is bounded, and every returned set satisfies the guarantee. The guarantee alone would hold vacuously for a relation that can get stuck.
  • "Cost at most the cost of the optimal LP solution" becomes c(H)≤c⋅xc(H)\le c\cdot x for every feasible xx.
  • "Distribute the tokens" (Lemma 5.6) becomes a counting inequality on the surplus of tokens.
  • Claim 5.9's "contains exactly three special members" means that SS has exactly three members, all of them special.
  • Figure 5's Step 4 is guarded by "no edge was picked in Step 3", as the paper's text under Lemma 5.1 states.
  • "FF is not a spanning tree" and LP feasibility are explicit hypotheses where the paper leaves them implicit.

Two trivializations are ruled out. Existence of a cheap tree with degrees in [Av−1,Bv+1][A_v-1,B_v+1] is not the target: the statement is about the algorithm's outputs and quantifies over all of them. And a run that never terminates does not satisfy the goal, which requires a run to exist and every run to be bounded.

Contributions are welcome at every level: the laminar uncrossing argument (Lemma 5.3), which is reusable for any spanning-tree LP with degree rows; the counting claims; and the invariants of the recursion.

Selected references

12 thms1 active userReviewed
Graph TheoryLinear OptimizationOperations Research+1·Captain: mikedeng1

Approximating Minimum Bounded Degree Spanning Trees to within One of Optimal 1: Iterative Rounding Finds a Spanning Tree of Cost at Most the LP Optimum with Every Degree at Most B_v + 1Research Paper

Motivation

A network designer may need a cheap connection that keeps the number of links at each site within a local capacity. The minimum bounded-degree spanning tree problem asks for the cheapest spanning tree of a weighted, undirected graph whose vertex degrees respect prescribed upper bounds. The capacity constraints matter in settings where a low-cost tree alone can overload a few hubs. They also make the optimization problem difficult: even with unit edge weights and a bound of two at every vertex, feasibility includes the Hamiltonian path problem. Singh and Lau study the useful relaxation in which the returned tree may exceed each degree bound by one while its cost stays no greater than the best tree satisfying every original bound Singh–Lau 2007.

The weighted result settled the bounded-degree form of a conjecture discussed in their paper. Goemans had obtained a cost-preserving degree guarantee of Bv+2B_v+2; an earlier unweighted local-search result attained a +1+1 degree allowance but did not cover arbitrary real costs. Singh and Lau's Theorem 1.2 gives the +1+1 allowance in the weighted setting, without assuming nonnegative costs or triangle inequalities Singh–Lau 2007, pp. 661–662. The platform's open WilliamsonShmoys.minimum_degree_tree_local_search_approximation concerns the related unweighted minimum-degree local-search problem, with a different objective and guarantee.

Setting

Let VV be a finite vertex set and EE a finite set of unordered, non-loop edges. A spanning tree T⊆ET\subseteq E connects every vertex without a cycle. Every edge ee has a real cost cec_e, so c(T)=∑e∈Tcec(T)=\sum_{e\in T}c_e. Each vertex vv has an integer upper bound BvB_v on its tree degree dT(v)d_T(v). A feasible original solution has dT(v)≤Bvd_T(v)\le B_v for all vv.

The paper studies a broader connecting-tree problem. A forest FF is already selected; its connected components, including isolated vertices, are supernodes. The remaining graph has edges EE disjoint from FF. A set H⊆EH\subseteq E is an FF-tree if H∪FH\cup F is a spanning tree. Degree bounds are active only at vertices in W⊆VW\subseteq V, and dH(v)d_H(v) counts edges of HH, not edges of FF. The initial spanning-tree problem is the case F=∅F=\varnothing and W=VW=V Singh–Lau 2007, p. 665.

For an edge set QQ and vertex set SS, write Q(S)Q(S) for edges of QQ with both endpoints in SS, and δE(v)\delta_E(v) for edges of EE incident to vv. The LP-MBDCT relaxation has a nonnegative variable xex_e for each e∈Ee\in E. It requires x(E)=∣V∣−∣F∣−1x(E)=|V|-|F|-1, requires x(E(S))≤∣S∣−∣F(S)∣−1x(E(S))\le |S|-|F(S)|-1 for every nonempty union SS of supernodes, and requires x(δE(v))≤Bvx(\delta_E(v))\le B_v for v∈Wv\in W. Its objective is ∑e∈Ecexe\sum_{e\in E}c_ex_e. At F=∅F=\varnothing, W=VW=V, this is the spanning-tree LP in equations (1)–(5) Singh–Lau 2007, pp. 662, 665.

Formalization targets

Theorem 1.2: bounded-degree spanning trees

For every feasible initial LP, the paper's Figure 4 algorithm has a terminating run. Every possible run returns a spanning tree TT satisfying

dT(v)≤Bv+1(v∈V),c(T)≤∑e∈Ecexefor every LP-feasible x.d_T(v)\le B_v+1\quad(v\in V),\qquad c(T)\le\sum_{e\in E}c_ex_e\quad\text{for every LP-feasible }x.

In particular, c(T)c(T) is at most the cost of every spanning tree satisfying the original bounds, and thus at most the original optimum. Every run has at most 2∣V∣−12|V|-1 iterations. The cost comparison against every LP-feasible vector states the stronger bound used by Theorem 4.2 Singh–Lau 2007, pp. 661, 666.

Theorem 4.2 and its milestones

The connecting-tree theorem makes the same cost and degree guarantee for an arbitrary feasible state (E,B,W,F)(E,B,W,F), with dH(v)≤Bv+1d_H(v)\le B_v+1 only for v∈Wv\in W. The attack path follows the paper's numbered results: Lemma 4.3 describes tight constraints by a laminar family, Claim 4.5 classifies vertices with one excess token, Lemma 4.6 bounds tokens inside a laminar subtree, and Lemma 4.1 says each nonterminal basic solution has either a unit-valued edge or a removable degree constraint. Theorem 4.2 then supplies the general guarantee Singh–Lau 2007, pp. 666–667.

Significance

The result allows one unit of violation at each local degree bound while preserving the cost benchmark exactly. It applies even when negative edge costs make standard multiplicative cost ratios awkward. The connecting-tree statement is useful beyond the initial instance because it covers a forest already accumulated and a subset of degree constraints still active.

This mission formalizes the known 2007 result as an open Lean proof target; the paper proves the mathematics, while the declarations here currently have no machine-checked proofs. A completed development would provide a reusable account of a spanning-tree LP with forest contraction, basic solutions defined by tight rows, and a finite relational algorithm with all choices exposed. These objects could support the paper's lower-and-upper-bound extension and other iterative-rounding results.

Difficulty

Rounding an arbitrary fractional edge upward can increase cost beyond the LP benchmark. Restricting the algorithm to edges with value exactly one protects that benchmark, but a nonterminal basic solution need not present a unit-valued edge. The central structural question is then whether some active degree constraint can be removed with only a one-unit effect on the final degree. The tight subtour rows and degree rows overlap, so counting edges from the support alone is insufficient; Lemmas 4.3–4.6 resolve the dependency and token-counting issues that make the direct argument fail Singh–Lau 2007, pp. 666–667.

Formalization scope

Lean represents edges as Sym2 V in finite sets, excluding diagonal edges. It represents LP vectors on all unordered pairs but requires zero values outside the current edge set. A forest is acyclic on the full vertex set. A compatible subtour set is a union of its connected components. Subtour right-hand sides are real numbers, so subtraction does not truncate at zero; the empty set is excluded because the literal row would make the LP infeasible. Degree bounds are integers so the algorithm's decrements are total. A basic feasible solution is determined uniquely by its tight equality rows among vectors supported on the current edge set. Linear independence in Lemma 4.3 is checked on the positive support.

Figure 4 is a relation because the LP optimum, a unit-valued edge, and a qualifying vertex may each be chosen in several ways. Its edge and vertex tests are mandatory when their conditions hold. The vertex test uses the support before deleting the selected edge and bounds after decrementing its endpoints, following the printed order. “The algorithm returns” is represented by existence of a run, an iteration bound on every step chain, and guarantees for every returned set. “Cost at most the LP optimum” means cost no greater than the objective at every feasible LP vector. “Polynomial time” is represented by the iteration count; the ellipsoid LP solver and separation-oracle complexity are outside this mission. Lemma 4.6's token distribution is expressed as its explicit counting inequality.

The goal asserts the Figure 4 output and its LP cost guarantee. Bare existence of a tree with cost at most the optimum and degrees at most Bv+1B_v+1 would be witnessed by an original optimal tree and would lose the algorithmic theorem. A return guarantee without run existence would hold vacuously for a stuck relation. Contributions that prove the stated structural lemmas, establish the LP oracle's basic-optimum availability, or close the algorithm invariant are within scope. No existing platform item treats this bounded-degree LP and iterative-rounding algorithm under these conventions; the plain minimum-spanning-tree LP definition uses a different edge representation and no forest or degree constraints.

Selected references

  • Mohit Singh and Lap Chi Lau, Approximating Minimum Bounded Degree Spanning Trees to within One of Optimal, Proceedings of the 39th ACM Symposium on Theory of Computing (STOC), 2007, pp. 661–670. DOI: 10.1145/1250790.1250887.
8 thms1 active userReviewed
Graph Theory·Captain: mikedeng1

Graph Minors. X. Obstructions to Tree-Decomposition IV: Mutually Distinguishable Tangles Have a Tree-Decomposition Separating Them by Their DistinctionsResearch Paper

Why tangles need to be organised into a tree

Robertson and Seymour introduced tangles in Graph Minors. X (J. Combin. Theory Ser. B 52 (1991) 153–190) as the precise obstruction to tree-decompositions of small width: a graph has a tangle of large order exactly when it has no tree-decomposition of small width. A tangle points to a highly connected region of a graph without naming its vertices, by designating for every low-order separation which side is the "small" one. Large grids, large clique minors and surface embeddings with high representativity all induce tangles.

A graph usually contains several such regions. The structure theory of the Graph Minors series needs to look at all of them at once: to decompose a graph along a tree so that each highly connected region sits at its own node, and any two regions are separated as cheaply as possible. Section 10 of the paper provides that decomposition, and its later versions ("tree of tangles" theorems) have become a standard tool in structural graph theory, in matroid theory and in abstract separation systems (see Diestel, Hundertmark and Lemanczyk, Profiles of separations: in graphs, matroids and beyond, Combinatorica 39 (2019), and Carmesin, Diestel, Hundertmark and Stein, Connectivity and tree structure in finite graphs, Combinatorica 34 (2014)). This mission formalizes the original 1991 statement for hypergraphs.

Setting

A hypergraph GG has a finite vertex set V(G)V(G), a finite edge set E(G)E(G) and an incidence relation; an edge may have any number of ends. A subhypergraph is given by a vertex set and an edge set, closed under taking ends of its edges; ∪\cup, ∩\cap, ⊆\subseteq act on both sets. A separation is a pair (A,B)(A,B) of subhypergraphs with A∪B=GA\cup B=G and E(A∩B)=∅E(A\cap B)=\emptyset; its order is ∣V(A∩B)∣|V(A\cap B)|.

A tangle of order θ≥1\theta\ge1 is a set T\mathcal T of separations of order <θ<\theta such that (i) of every separation (A,B)(A,B) of order <θ<\theta, one of (A,B)(A,B), (B,A)(B,A) is in T\mathcal T; (ii) no three members (Ai,Bi)(A_i,B_i) of T\mathcal T satisfy A1∪A2∪A3=GA_1\cup A_2\cup A_3=G; (iii) V(A)≠V(G)V(A)\neq V(G) for (A,B)∈T(A,B)\in\mathcal T. Two tangles are indistinguishable if one contains the other, and a separation (A,B)(A,B) distinguishes T1\mathcal T_1 from T2\mathcal T_2 if (A,B)∈T1(A,B)\in\mathcal T_1 and (B,A)∈T2(B,A)\in\mathcal T_2.

A tree-decomposition (T,τ)(T,\tau) assigns a subhypergraph τ(t)\tau(t) to each node of a tree TT, so that the τ(t)\tau(t) cover GG, are pairwise edge-disjoint, and τ(t)∩τ(t′′)⊆τ(t′)\tau(t)\cap\tau(t'')\subseteq\tau(t') whenever t′t' lies on the path from tt to t′′t''. An edge ee of TT, with components T1,T2T_1,T_2 of T∖eT\setminus e, makes the separations (G1e,G2e)(G^e_1,G^e_2) and (G2e,G1e)(G^e_2,G^e_1), where Gie=⋃t∈V(Ti)τ(t)G^e_i=\bigcup_{t\in V(T_i)}\tau(t). Two separations cross unless one of four nestings holds (A1⊆A2A_1\subseteq A_2 and B2⊆B1B_2\subseteq B_1, or the analogous three); a set of separations is laminar if no two members cross.

A tie-breaker λ\lambda maps separations into a linearly ordered set so that (i) λ(A,B)=λ(C,D)\lambda(A,B)=\lambda(C,D) exactly when (A,B)=(C,D)(A,B)=(C,D) or (A,B)=(D,C)(A,B)=(D,C); (ii) λ(A∪C,B∩D)≤λ(A,B)\lambda(A\cup C,B\cap D)\le\lambda(A,B) or λ(A∩C,B∪D)<λ(C,D)\lambda(A\cap C,B\cup D)<\lambda(C,D); (iii) separations of smaller order get smaller λ\lambda-order. Given λ\lambda, the (T1,T2)(\mathcal T_1,\mathcal T_2)-distinction is the separation of minimum λ\lambda-order distinguishing T1\mathcal T_1 from T2\mathcal T_2. A separation (A,B)(A,B) is λ\lambda-robust if for every separation (C,D)(C,D) of the hypergraph AA, one of (C,B∪D)(C,B\cup D), (D,B∪C)(D,B\cup C) has λ\lambda-order at least λ(A,B)\lambda(A,B), and doubly λ\lambda-robust if (B,A)(B,A) is λ\lambda-robust too.

Formalization targets

Goal: (10.3), p. 181

Let T1,…,Tn\mathcal T_1,\dots,\mathcal T_n, n≥1n\ge1, be mutually distinguishable tangles in GG (each with its own order) and λ\lambda a tie-breaker. Then there is a tree-decomposition (T,τ)(T,\tau) with V(T)={t1,…,tn}V(T)=\{t_1,\dots,t_n\} such that

(i)ti∈V(T1) ⟹ (⋃t∈V(T1)τ(t), ⋃t∈V(T2)τ(t))∉Tifor every e∈E(T),\text{(i)}\quad t_i\in V(T_1)\ \Longrightarrow\ \Bigl(\textstyle\bigcup_{t\in V(T_1)}\tau(t),\ \bigcup_{t\in V(T_2)}\tau(t)\Bigr)\notin\mathcal T_i\quad\text{for every } e\in E(T),

and (ii) for i≠ji\neq j, each edge of the tit_i–tjt_j path in TT whose separations have the smallest λ\lambda-order on that path makes the (Ti,Tj)(\mathcal T_i,\mathcal T_j)- and (Tj,Ti)(\mathcal T_j,\mathcal T_i)-distinctions, the first with tjt_j's side first.

Milestones

  • (9.1), p. 177: the separations made by the edges of a tree-decomposition form a laminar set, and every laminar set is the set made by the edges of some tree-decomposition, each member by a unique edge.
  • (9.2), p. 178: every hypergraph has a tie-breaker.
  • (9.3), p. 179: a strict form of the second tie-breaker axiom, with two degenerate exceptions.
  • (9.4), p. 180: doubly λ\lambda-robust separations do not cross.
  • (10.1), p. 180: two tangles are distinguished by some separation if and only if neither contains the other.
  • (10.2), p. 181: the (T1,T2)(\mathcal T_1,\mathcal T_2)-distinction is doubly λ\lambda-robust.

Significance

The theorem gives a single decomposition for all tangles at once: any family of pairwise distinguishable tangles is displayed by a single tree-decomposition, with each tangle "living" at its own node (property (i)) and every pair separated by its cheapest distinction (property (ii)). The paper derives from it that a hypergraph has at most ∣V(G)∣|V(G)| maximal tangles ((10.4), p. 184), and Section 11 uses the same machinery to build tree-decompositions whose pieces "almost" carry a local structure, a step used in the later Graph Minors papers.

None of these statements is formalized in any proof assistant as far as a search of the Prove2Me library shows; the platform has simple-graph tree-decompositions with vertex bags (from Graph Minors V), which are a different object from the hypergraph tree-decompositions here. The mission produces machine-checked statements of the tangle-tree theorem in its original hypergraph form, together with the lemma chain the authors use. The remaining work is a formal proof of each item; (9.1) is "left to the reader" in the paper and therefore needs an argument written from scratch.

Difficulty

The naive approach takes, for every pair of tangles, a separation of minimum order distinguishing them, and tries to arrange these separations in a tree. That fails: minimum-order distinguishing separations for different pairs may cross, and no tree-decomposition makes two crossing separations. Ties among minimum-order separations must be broken consistently across all pairs at once, and even a laminar family of distinctions does not obviously yield a tree whose nodes correspond one-to-one to the tangles, as property (i) and V(T)={t1,…,tn}V(T)=\{t_1,\dots,t_n\} demand.

Formalization scope

  • Hypergraphs are a structure with an incidence relation on types V, E; every theorem assumes [Finite V] [Finite E] (the paper's "all hypergraphs in this paper are finite", p. 154). Subhypergraphs are pairs of a vertex set and an edge set closed under ends.
  • A tangle carries its order as a parameter: IsTangle G θ 𝒯 includes θ≥1\theta\ge1. In (10.3) the tangles have independent orders θi\theta_i.
  • The tree of a tree-decomposition is a SimpleGraph on Fin n that is a tree. In the goal, node ii is tit_i, which encodes V(T)={t1,…,tn}V(T)=\{t_1,\dots,t_n\} with the tit_i distinct; the hypothesis n≥1n\ge1 is the paper's.
  • A tie-breaker is a function on all pairs of subhypergraphs into an arbitrary type Λ\Lambda with a linear order; its axioms constrain only its values on separations. The goal quantifies over every such Λ\Lambda, not just the paper's R3\mathbb R^3.
  • (10.3)(ii) is stated with an explicit orientation (the one forced by (i)) and for every edge minimising the λ\lambda-order on the path.
  • (10.1) and (10.2) are stated for hypergraphs; §10 opens with "tangles in a graph GG", but (10.3) applies them to hypergraphs and their proofs do not use edge sizes.
  • A trivializing formalization would make the tie-breaker axioms unsatisfiable, so that (9.3)–(10.3) hold vacuously; (9.2) is part of the mission precisely to rule this out.
  • The definitions of hypergraph, tangle and tree-decomposition are shared with the other missions of the series, Graph Minors. X. Obstructions to Tree-Decomposition I (tangle number equals max⁡(β,γ)\max(\beta,\gamma)), II (branch-width and tree-width), III (the grid tangle) and V (pervasive classes of designs). The laminar/tie-breaker layer is reusable for any tree-of-tangles statement. Contributions welcome: proofs of the milestones in any order, and a formal proof of (9.1).

Selected references

13 thms1 active userReviewed