Computational Geometry

Linear Optimization Operations Research Theoretical Computer Science·Captain: mikedeng1

Linear Programming in Linear Time When the Dimension Is Fixed: Fixed-Dimension LP Feasibility Decided in Linear Time on the Real RAMResearch Paper

Motivation

A linear program asks for a point $x\in\mathbb{R}^d$ minimizing $c^Tx$ subject to $n$ linear inequalities $\sum_{j=1}^d a_{ij}x_j\ge b_i$ . Many problems in computational geometry and statistics are linear programs with few variables and very many constraints: separating two point sets by a line or plane, fitting a line in the Chebyshev ( $L_\infty$ ) norm, finding the smallest disk or ball containing a point set (a related convex problem). For these problems the number of variables $d$ is a small constant, and what matters is how the running time grows with $n$ .

Nimrod Megiddo showed that for every fixed $d$ the problem can be solved in time $C(d)\cdot n$ (J. ACM 31(1), 1984).

Timeline.

1983. Megiddo (SIAM J. Comput. 12) and, independently, Dyer (SIAM J. Comput. 13 (1984)) give linear-time algorithms for $d=2$ and $d=3$ .
1984. Megiddo extends the method to every fixed $d$ , with $C(d)<2^{2^{d+2}}$ (the paper formalized here).
1988–1991. Clarkson (J. ACM 42 (1995), conference version 1988) gives a randomized algorithm with expected time $O(d^2n)+d^{O(\sqrt d)}\log n$ . Seidel (Discrete Comput. Geom. 6 (1991)) gives a simple randomized $O(d!\,n)$ algorithm.
1992–1996. Matoušek, Sharir and Welzl and, independently, Kalai give subexponential randomized bounds. Chazelle and Matoušek derandomize the linear dependence with $C(d)=d^{O(d)}$ (J. Algorithms 21 (1996)).

Setting

Fix $d$ . An instance is a matrix $A\in\mathbb{R}^{n\times d}$ and a vector $b\in\mathbb{R}^n$ , and its feasible region is the polyhedron $P(A,b)=\{x\in\mathbb{R}^d: Ax\ge b\}$ . Here $n$ is the number of constraints and $d$ the number of variables.

The model of computation is the real RAM. A program is a finite list of instructions acting on real registers, integer pointer registers and a memory $\mathbb{Z}\to\mathbb{R}$ . It performs exact $+,-,\times,/$ on reals at unit cost, tests the sign of a real, sets, copies, increments, decrements and compares pointers, and loads and stores through pointers. The input is the standard encoding of $(A,b)$ in memory: the numbers $n$ and $d$ , then $A$ row by row, then $b$ . A program decides an instance within $T$ steps with output $\beta\in\{\text{accept},\text{reject}\}$ if it halts on that output after at most $T$ steps.

Megiddo's method rests on multidimensional search. There is an unknown point $x^*\in\mathbb{R}^d$ and an oracle that, for any hyperplane $\{x: a^Tx=b\}$ , answers whether $a^Tx^*<b$ , $=b$ or $>b$ . Given hyperplanes $H_i=\{a_i^Tx=b_i\}$ with $a_i\ne0$ , the question is how many oracle calls determine the position of $x^*$ relative to all of them. A search strategy is a ternary decision tree: inner nodes are hyperplane queries, leaves carry outputs, and the tree is built from the data alone. For linear programming, $x^*$ is an optimal solution, or a minimizer of the infeasibility function $f(x)=\max_i(b_i-a_i^Tx)$ when the system is infeasible. The oracle is implemented by solving problems in $d-1$ variables.

Formalization targets

Goal: linear-time feasibility on the real RAM

\forall d\ \exists R\ \exists C\ \forall n\ \forall A\in\mathbb{R}^{n\times d},\,b\in\mathbb{R}^n:\quad R\text{ decides within }C\,(n+1)\text{ steps whether } \{x: Ax\ge b\}\neq\emptyset.

The program and the constant depend on $d$ only. No explicit form of $C(d)$ is fixed.

Milestones

One query settles half of $n$ hyperplanes on the line ( $A(1)=1$ , $B(1)=\tfrac12$ ).
$v(\epsilon)=(1,\epsilon,\dots,\epsilon^{d-1})$ is orthogonal to some $a_i$ for at most $n(d-1)$ values of $\epsilon$ , so there is a basis in which all $a_{ij}\ne0$ .
For hyperplanes of opposite slopes in the $(x_1,x_2)$ plane, the answers for $H^{(1)}_{ik}$ and $H^{(2)}_{ik}$ settle one of $H_i$ , $H_k$ .
A linearly dependent pair of opposite slopes has $a_{i1}=a_{k1}=0$ , and the middle hyperplane settles one of them.
Approach I: $2^{d-1}$ queries settle at least $\lfloor 2^{1-2^d}n\rfloor$ hyperplanes.
$C(d)\log n$ queries settle all $n$ hyperplanes.
If a hyperplane contains no optimal point, all optimal points lie on one side of it.
The oracle, Case I: at an optimum relative to $\{x_d=0\}$ , two auxiliary systems decide the side or certify global optimality.
The oracle, Case II: at a minimizer of $f$ on $\{x_d=0\}$ , systems (1) and (2) decide the side or certify infeasibility.

Significance

The result. For every fixed dimension, linear programming is solvable in time linear in the number of constraints. The algorithm is also strongly polynomial in fixed dimension: its operation count does not depend on the bit size of the data. Deciding whether the optimum is at most $t$ is feasibility of $Ax\ge b$ together with $-c^Tx\ge-t$ , so the goal also covers the decision form of optimization. The prune-and-search technique of the paper, which discards a constant fraction of the constraints per round, became a standard tool of computational geometry.

Formalizing it. The result is proved and classical. The platform already has the cases $d=1$ (linear time) and $d=2$ (quadratic time, by Fourier–Motzkin elimination) on the same machine and input encoding (SmaleNinth.real_ram_decides_one_variable_lp_linear, SmaleNinth.real_ram_decides_two_variable_lp_quadratic). No machine-checked proof of the general statement is known. The work consists of the query-complexity layer (milestones 1–6), the convex-analytic correctness of the oracle (milestones 7–9), and a real-RAM implementation with a step count linear in $n$ , including linear-time median selection. Alternative proofs, for example through Clarkson's or Seidel's algorithms made deterministic, are welcome for the goal.

Difficulty

The obvious approach is to find the optimum by testing constraints one by one or by eliminating variables. Fourier–Motzkin elimination produces $\Theta(n^2)$ constraints after one step. Pivoting methods have no known bound linear in $n$ . The key difficulty is to discard a constant fraction of the constraints using only a constant number of recursive calls in dimension $d-1$ , when no single hyperplane test gives information about more than one constraint. The multidimensional search layer gives this, and it is where the pairing of hyperplanes by slope and the degenerate cases (dependent pairs, zero coefficients) have to be handled exactly. At the machine level, the step count must stay linear in $n$ for a fixed program, so every median selection and every recursive call must be implemented within the budget, with the recursion depth depending on $d$ only.

Formalization scope

Machine and input. The machine is the platform's real RAM SmaleNinth.RAMProgram with RAMDecidesInTime, and the input convention is SmaleNinth.encodeLP (published definitions, reused unchanged). No instruction is added: there is no LP, median, floor or sort primitive. Time is the number of machine steps.
Quantifier order. $\forall d\ \exists R\ \exists C\ \forall n, A, b$ . The bound is $C(n+1)$ in the number $n$ of constraints, so that the machine can halt at $n=0$ . The paper's $C(d)<2^{2^{d+2}}$ counts unspecified units of "effort" with an unquantified $\theta(nd)$ term, and it is not transferred to machine steps. Where a milestone's proof fixes a constant exactly, the constant is stated: $2^{d-1}$ queries and $\lfloor n/2^{2^d-1}\rfloor$ settled hyperplanes in milestone 5.
Feasibility only. The machine outputs accept or reject. Returning an optimizer, "unbounded", or a minimizer of $f$ is not part of the goal. The case $d=0$ is included.
Query trees. Nodes are queries compare (a ⬝ᵥ x) b and nothing else, leaves hold fixed values, and correctness is required for every $x$ . A tree over arbitrary tests of $x$ would make milestones 5 and 6 empty, and it is excluded by the definition.
Indices. The paper's $x_1,x_2$ are indices 0, 1 of Fin (d + 2), and its $x_d$ is Fin.last d of Fin (d + 1).
Corrections. Two passages of §4 are stated in corrected form. The Case I auxiliary objective includes the $\pm c_d$ term of the direction. In Case II, feasibility of (1) puts improvement in $\{x_d>0\}$ , where the page's last sentence says $\{x_d<0\}$ . The pairing claim carries $a_{k1}a_{i2}-a_{k2}a_{i1}\ne0$ , the hypothesis its argument uses, since linear independence alone does not give it.
Not included. Approach II and its bound $O(n(\log n)^{d^2})$ , the remarks on slowly growing $d$ , the randomized variants, and the applications of §1.
Reusable parts. The query-tree definition and milestones 1–6 apply to any prune-and-search problem with a hyperplane oracle. The oracle lemmas (7–9) are statements about convex piecewise-linear functions and polyhedra.

Selected references

N. Megiddo, Linear programming in linear time when the dimension is fixed, J. ACM 31(1):114–127, 1984. https://doi.org/10.1145/2422.322418
N. Megiddo, Linear-time algorithms for linear programming in $R^3$ and related problems, SIAM J. Comput. 12(4):759–776, 1983. https://doi.org/10.1137/0212052
M. E. Dyer, Linear time algorithms for two- and three-variable linear programs, SIAM J. Comput. 13(1):31–45, 1984. https://doi.org/10.1137/0213003
K. L. Clarkson, Las Vegas algorithms for linear and integer programming when the dimension is small, J. ACM 42(2):488–499, 1995. https://doi.org/10.1145/201019.201036
R. Seidel, Small-dimensional linear programming and convex hulls made easy, Discrete Comput. Geom. 6:423–434, 1991. https://doi.org/10.1007/BF02574699
B. Chazelle, J. Matoušek, On linear-time deterministic algorithms for optimization problems in fixed dimension, J. Algorithms 21(3):579–597, 1996. https://doi.org/10.1006/jagm.1996.0046

16 thms5 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Rounding of Polytopes in the Real Number Model of Computation: Barycentric Coordinate Descent Finds a (1+ε)n-Rounding Ellipsoid of m Points in O(n(1/ε + ln n + ln ln m)) IterationsResearch Paper

Motivation

Many algorithms for convex bodies need the body to be well rounded: sandwiched between two concentric ellipsoids whose size ratio is controlled by the dimension. The ellipsoid method, volume and integration algorithms, and preconditioning for linear programming use such roundings. For a polytope given by its vertices $a_1,\dots,a_m \in \mathbb{R}^n$ , John's theorem guarantees an ellipsoid $E$ with

n^{-1}E \subseteq \operatorname{conv}\{a_1,\dots,a_m\} \subseteq E,

the minimum-volume circumscribed (Löwner–John) ellipsoid scaled about its centre; for centrally symmetric sets the factor improves to $\sqrt n$ . The associated D-optimal design problem is a convex optimization problem. Khachiyan (1996) uses this connection to obtain a finite approximation algorithm.

Khachiyan shows that barycentric coordinate descent (BCD) computes a $(1+\varepsilon)n$ -rounding in $O(mn^2(\varepsilon^{-1} + \ln n + \ln\ln m))$ arithmetic operations. For fixed dimension and tolerance, this is linear in the number of points; the iteration bound depends on that number only through $\ln\ln m$ . Khachiyan (1996)

The paper builds on the Kiefer–Wolfowitz optimality conditions (1960). Later work revisits the method's complexity and variants; see Todd and Yıldırım (2007).

Setting

Let $a_1,\dots,a_m \in \mathbb{R}^n$ and let $S$ be the unit simplex of weights $p \ge 0$ , $\sum_i p_i = 1$ . For $p \in S$ write

A(p) = \sum_{i=1}^m p_i\, a_i a_i^{\mathsf T}, \qquad F(p) = \ln\det A(p), \qquad w_j(p) = a_j^{\mathsf T}A(p)^{-1}a_j ,

and let $S_F = \{p \in S \mid \det A(p) > 0\}$ . Maximizing $F$ over $S$ is the D-optimal design problem (2.3); $F^*$ is its optimal value. A point $p \in S_F$ satisfies the $\varepsilon$ -relaxed optimality conditions (2.10) if $w_j(p) \le (1+\varepsilon)n$ for every $j$ ; the accuracy $\varepsilon(p) = \max_j w_j(p)/n - 1$ is the least such $\varepsilon$ .

The BCD method starts at $p_0 = (1/m,\dots,1/m)$ and repeats

p_{k+1} = (1-\tau)\,p_k + \tau\, e_r, \qquad \tau = \frac{\varepsilon(p_k)}{w_r(p_k) - 1},

where $r$ is an index with largest $w_r(p_k)$ and $e_r$ is the $r$ th vertex of $S$ : it moves weight towards the worst-covered point by the exact line-search step.

For a centrally symmetric set ( $\mathcal A = -\mathcal A$ ) the ellipsoid $E_p = \{x \mid x^{\mathsf T}A(p)^{-1}x \le 1\}$ is the candidate rounding. For a general set the method runs on the lift $\mathcal A' = \{\pm(a_j;1)\} \subset \mathbb{R}^{n+1}$ , and the rounding ellipsoid $E$ is the intersection of $\sqrt{1 + (1+\varepsilon)n}\,E'_p$ with the hyperplane $\{y = 1\}$ , where $E'_p$ is the ellipsoid (3.4) of the block matrix with blocks $\sum_j p_j a_j a_j^{\mathsf T}$ , $\sum_j p_j a_j$ and $1$ , and $p_j$ aggregates the weights of $\pm(a_j;1)$ .

Formalization targets

Goal: Theorem 2 (p. 317)

There is a universal constant $C$ such that for every $n \ge 1$ , every $\mathcal A = \{a_1,\dots,a_m\}$ with affine hull $\mathbb{R}^n$ , every $\varepsilon > 0$ and every BCD run on $\mathcal A'$ , some iterate $p_k$ with

k \le C(n+1)\Big(\frac1\varepsilon + \ln(n+1) + \ln\ln(2m)\Big)

meets the stopping test with $\varepsilon' = \frac{n}{n+1}\varepsilon$ and yields an ellipsoid $E$ with

[(1+\varepsilon)n]^{-1}E \subseteq \operatorname{conv}(\mathcal A) \subseteq E,

the shrinking taken about the centre of $E$ .

The centrally symmetric case: Theorem 1 (p. 314)

For centrally symmetric full-dimensional $\mathcal A$ , $n \ge 2$ : within $C\,n(\varepsilon^{-1} + \ln n + \ln\ln m)$ iterations,

E_{p_k} \subseteq \operatorname{conv}(\mathcal A) \subseteq \sqrt{(1+\varepsilon)n}\;E_{p_k}.

Milestones

Lemma 1 ( $\sum_j p_j w_j(p) = n$ ), existence of a maximizer, the line identity (2.6), the Kiefer–Wolfowitz conditions (2.9), Lemma 2(i)–(ii) (relaxed optimality gives value and rounding guarantees), Lemma 3 (the per-step increase and the gap bound), the three steps (2.25), (2.27) and the halving bound of the proof of Lemma 4, Lemma 4 (the iteration bound), the rank-one update of $A(p_k)^{-1}$ , Theorem 1, and Lemma 5 (from the lift back to $\mathcal A$ ). Three further items complete §4: Lemma 2(iii), the slicing property (4.1) and Theorem 3 (approximating the Löwner ellipsoid to relative volume accuracy $\varepsilon$ ).

Significance

The result gives a rounding of a vertex-described polytope at nearly the cost of reading the input, using only rank-one updates; the same iteration approximates the minimum-volume enclosing ellipsoid, a basic primitive in statistics (D-optimal design, outlier detection), computational geometry (core sets) and convex optimization (initialization of interior-point and ellipsoid methods). The doubly logarithmic dependence on $m$ is what makes the method practical for large point sets, and the analysis is the template for the later Frank–Wolfe-type analyses of minimum-volume ellipsoid algorithms.

The results are proved in the paper; none of them has a machine-checked proof. The platform has the Löwner–John ellipsoid itself (existence, uniqueness, John's $n$ -rounding) and the concavity of $\ln\det$ , but no algorithmic statement about it. This mission produces a verified iteration bound for a concrete method, together with the D-optimal design identities (Lemma 1, (2.6), (2.9)) and the rank-one update, which are reusable for any later formalization of optimal design or of Frank–Wolfe methods on the simplex.

Difficulty

The accuracy $\varepsilon_k$ need not decrease at every step, so a bound based on per-step improvement in $\varepsilon_k$ fails. The determinant objective and the geometric rounding condition are different quantities: controlling one must be shown to control the other, including the inner inclusion of the ellipsoid. For a general set, the lift changes the dimension and the relevant ellipsoid is a slice at $y=1$ ; the inner inclusion for this slice needs a separate geometric justification.

Formalization scope

Points are vectors Fin n → ℝ; $\mathcal A$ is the range of a family a : Fin m → Fin n → ℝ (repetitions allowed). The definitions take any finite index, so they apply both to $\mathcal A$ and to the lift, indexed by Fin m ⊕ Fin m. $S$ is Mathlib's stdSimplex. $F$ uses Real.log, which returns $0$ rather than $-\infty$ on singular matrices, so every comparison of values of $F$ is restricted to $S_F$ and $F^*$ is the supremum over $S_F$ . Ellipsoids are the published LinearOptimization.ellipsoid; scaled ellipsoids about the origin use the pointwise scalar multiple, and shrinking a non-centred ellipsoid is the homothety about its centre.

Standing assumptions are hypotheses: in §2, central symmetry (2.1), full dimension (2.2) and $n \ge 2$ (p. 309); in §3, full dimension (3.1) and $n \ge 1$ . Items that do not need them drop them. The BCD run is a predicate on sequences that allows any maximizing index at every step, with no tolerance parameter; the tolerance enters only through the stopping test.

Each $O(\cdot)$ is a universal constant $C > 0$ quantified before the dimension, the points, $\varepsilon$ and the run. The paper counts arithmetic operations; the formal statements bound the index of an iterate meeting the stopping test, and the $O(nm)$ cost per iteration and the $O(mn^2)$ initialization are not formalized. The goal's bound is stated in the lifted parameters $(n+1, 2m)$ , which agrees with the page's up to the constant and stays positive at $n = 1$ .

The goal assumes nothing about the run beyond its definition: the stopping test, the positive definiteness of $A(p_k)$ , the rounding inclusions and the iteration bound are all conclusions. A statement in which the constant may depend on the instance, or in which a shrunken ellipsoid is scaled about the origin, would be a different, trivial or false, theorem.

Contributions welcome: the determinant and inverse identities ((2.6), Lemma 1, the rank-one update) are self-contained linear algebra; Lemma 2 needs the KKT characterisation of the minimum-volume ellipsoid; Lemma 5 is finite-dimensional convex geometry.

Selected references

L. G. Khachiyan, Rounding of polytopes in the real number model of computation, Mathematics of Operations Research 21(2):307–320, 1996. https://doi.org/10.1287/moor.21.2.307
J. Kiefer, J. Wolfowitz, The equivalence of two extremum problems, Canadian Journal of Mathematics 12:363–366, 1960. https://doi.org/10.4153/CJM-1960-030-4
L. G. Khachiyan, M. J. Todd, On the complexity of approximating the maximal inscribed ellipsoid for a polytope, Mathematical Programming 61:137–159, 1993. https://doi.org/10.1007/BF01582144
M. J. Todd, E. A. Yıldırım, On Khachiyan's algorithm for the computation of minimum-volume enclosing ellipsoids, Discrete Applied Mathematics 155:1731–1744, 2007. https://doi.org/10.1016/j.dam.2007.02.013

21 thms4 active usersReviewed

Discrete Geometry Graph Theory·Captain: hao jia

Uniform Obstacle Bounds for Planar Graphs (OPG-37357)Open Problem

Motivation

An obstacle representation turns a graph into a visibility system: vertices are points in the plane, and nonedges are blocked by polygonal obstacles. The obstacle number asks for the minimum number of obstacles needed. OPG-37357 records two different questions for planar graphs. The first asks whether one obstacle can ever be insufficient. The second asks whether some universal constant bounds the ordinary obstacle number of every planar graph.

The status of the two parts is different. Berman, Chappell, Faudree, Gimbel, Hartman, and Williams proved in 2017 that explicit planar graphs, including the icosahedron and their graphs $X_4$ and $X_6$ , have ordinary obstacle number two. Thus the first question has a published positive answer. The universal-constant question remains the research target here. A separate invariant called planar or plane obstacle number requires a crossing-free visibility drawing; results for that invariant must not be substituted for the ordinary obstacle number used by this mission.

Setting

A finite simple graph $G$ has a $k$ -obstacle drawing when its vertices are placed injectively as points in $\mathbb R^2$ and there are $k$ pairwise disjoint closed connected polygonal obstacles such that

uv\in E(G) \quad\Longleftrightarrow\quad [p(u),p(v)]\text{ meets no obstacle}.

Graph vertices lie outside every obstacle. The ordinary obstacle number $\operatorname{obs}(G)$ is the least such $k$ . The drawing itself may contain crossings between visible graph edges; planarity is a property of the abstract input graph, not an extra constraint on the obstacle drawing.

The Lean model represents a polygonal obstacle as a connected finite union of closed filled triangles. This gives a compact polygonal region with exact real-coordinate segment incidence. Straight-line planarity of the abstract graph is represented separately.

Formalization targets

The two-part OPG record

The source records both

\exists\text{ finite planar }G,\ \operatorname{obs}(G)>1

and

\exists k\in\mathbb N\ \forall\text{ finite planar }H, \ \operatorname{obs}(H)\le k.

The first assertion is known in the literature and appears as a published-result milestone. The second is open and is therefore the mission's main theorem. Together they preserve the two-part source without presenting the whole record as unresolved.

Published first part

A milestone formalizes the stronger published statement

\exists\text{ finite planar }G, \qquad \operatorname{obs}(G)\le2 \quad\text{and}\quad \operatorname{obs}(G)\not\le1.

This captures ordinary obstacle number exactly two without hard-coding one graph before its adjacency data and lower-bound certificate are formalized.

Universal bound

The open milestone asks for a single natural number $k$ , chosen before the graph, that works for every finite planar graph. The number of obstacle corners is not bounded by this theorem; only the number of connected polygonal obstacles is.

Significance

The published first part establishes that planarity alone does not force a one-obstacle representation. The second part asks whether planar graphs nevertheless have uniformly bounded visibility complexity. A positive answer would produce a common finite obstacle budget independent of graph order; a negative answer would require a family of planar graphs with unbounded ordinary obstacle number.

Formalization is especially useful because several nearby notions differ by one word but have different known bounds: ordinary versus plane obstacle number, arbitrary polygonal versus convex obstacles, and fixed-placement versus freely chosen drawings. The mission's definitions make those choices explicit and provide reusable segment-obstacle semantics for later geometric graph formalizations.

Difficulty

A finite combinatorial graph does not come with a canonical visibility drawing. Even when one starts with an arbitrary connected blocking set, replacing it by one bounded simple polygon requires compactness, component, incidence, and polygonal-neighborhood arguments. Conversely, lower bounds must quantify over every possible placement and obstacle, not merely refute a selected coordinate drawing.

Counting results for unrestricted graphs do not automatically preserve planarity. Bounds for planar obstacle number impose a crossing-free drawing and therefore answer a different question. The known two-obstacle examples close only the existential first part and give no universal $k$ .

Formalization scope

All graph vertex types are finite. Obstacles are closed connected polygonal regions represented by finite triangle unions; they are pairwise disjoint and avoid graph vertices. Visibility uses the full closed segment, so tangency or boundary contact blocks a nonedge. The planarity witness is independent of the obstacle drawing. Empty and one-vertex graphs remain in the universal quantifier and should be handled without division or nonemptiness assumptions.

The repository's fixed-placement polygonization argument and finite arrangement code are candidate_only. They may motivate supporting lemmas, but they neither prove the unrestricted obstacle-drawing completeness theorem nor settle the universal bound. Contributions are welcome on exact geometry primitives, the published two-obstacle construction and lower bound, conversions between connected blockers and polygonal obstacles, and the universal root. A proof for the plane invariant, convex invariant, one fixed drawing, or a finite order cutoff must be labeled at that narrower scope.

Selected references

L. W. Berman, G. G. Chappell, J. R. Faudree, J. Gimbel, C. Hartman, and G. I. Williams, Graphs with Obstacle Number Greater than One, JGAA 21(6), 2017. https://doi.org/10.7155/jgaa.00452
J. Gimbel, P. Ossona de Mendez, and P. Valtr, Obstacle Numbers of Planar Graphs, Graph Drawing 2017. https://arxiv.org/abs/1706.06992
M. Balko, S. Chaplick, R. Ganian, S. Gupta, M. Hoffmann, P. Valtr, and A. Wolff, Bounding and Computing Obstacle Numbers of Graphs, SIAM Journal on Discrete Mathematics 38(2), 2024. https://arxiv.org/abs/2206.15414
Open Problem Garden / UnsolvedMath, OPG-37357. https://www.unsolvedmath.com/problems/OPG-37357

6 thms4 active usersReviewed

Operations Research Probability·Captain: mikedeng1

Concentration of Measure and Isoperimetric Inequalities in Product Spaces XII: The Euclidean Traveling Salesman Problem — P(|L_N − M| ≥ t) ≤ K e^{−t²/K} for N Uniform Points in the SquareTextbook

Motivation

The Euclidean traveling salesman problem asks for the shortest closed route through a finite set of points in the plane. Even when the points are placed independently and uniformly in a square, finding an individual shortest route is computationally difficult. A separate probabilistic question is whether the optimal length varies much from one random sample to another. In Chapter 11 of Talagrand's 1995 paper, this question motivates a concentration theorem for the tour length and for other geometric functionals with the same local regularity property.

The result is useful because a bound on fluctuations can be applied without computing the distribution of the optimal tour length. It separates the typical size of the length, which may need other geometric estimates, from the chance of a substantial deviation. The paper develops a more general concentration method for product spaces; the geometric chapter shows how its estimates can control an optimization problem whose response to changing one sample point depends strongly on the local configuration.

Setting

Let $Q=[0,1]^2$ , and let $X_1,\ldots,X_N$ be independent points uniformly distributed in $Q$ , with $N\ge1$ . A configuration is the finite set $F=\{X_1,\ldots,X_N\}$ ; repeated sample locations are represented once in $F$ . For any finite $F\subseteq Q$ , write $T(F)$ for the length of a shortest closed tour visiting every point of $F$ . The tour length of the random sample is $T_N=T(F)$ . The empty set and a singleton have tour length zero.

The main theorem concerns a functional $L$ on all finite subsets of $Q$ . A level $k\ge1$ dyadic square $C$ has side $2^{-k}$ . Say that $L$ has regularity constant $K_0>0$ when, for every finite $F$ and every finite $G\subseteq C$ , if a point of $F$ lies within Euclidean distance $2^{-k+2}$ of $C$ , then

L(F)\le L(F\cup G)\le L(F)+K_0,2^{-k}\sqrt{|G|}.

The first inequality is monotonicity under adding points. The second limits the added cost when the new points lie in a small square near an existing point. Lemma 11.2.1 says that the shortest tour functional $T$ has this property with a universal constant. In particular, the functional in the main theorem is not an arbitrary real function on samples: it must obey this condition for every admissible square and pair of finite sets.

A median $M$ of $L(F)$ is any real number for which both $P(L(F)\le M)$ and $P(L(F)\ge M)$ are at least one half. The theorem applies to every median. This convention avoids selecting one median when the distribution has more than one.

For the intermediate geometric estimates, $k_0$ is the largest integer with $2^{2k_0}\le N$ . Given a deviation parameter $t$ , $k_1$ is the integer selected by the criterion (11.1.9) after the paper sets the auxiliary Poisson intensity to $N/8$ . The number $m_k$ counts level $k$ squares that contain at most $N2^{-2k-6}$ distinct sample points. An isolation weight $\alpha(x)$ records the largest scale between $k_1$ and $k_0$ at which the square containing $x$ contains at most $N2^{-2k-7}$ sample points, and equals $2^{-k_0}$ if no such scale exists.

Formalization targets

Gaussian concentration for regular geometric functionals

For each fixed $K_0>0$ , there is a constant $K>0$ , independent of $N$ and $L$ , such that every measurable $L$ with the regularity property above satisfies, for all $t\ge0$ ,

P\bigl(|L(F)-M|\ge t\bigr)\le K\exp(-t^2/K).

This is Theorem 11.2.2, the goal. Its constant may depend on the fixed regularity constant $K_0$ . Lemma 11.2.1 makes the tour length a direct instance. The milestone list also includes the quantitative sparse-square estimate of Proposition 11.1.4, the isolation-weight bound of Proposition 11.2.3, and the deterministic insertion estimate of Proposition 11.2.5. These retain the paper's specified thresholds and the dependency of their constants.

Significance

For $T_N$ , the result supplies a tail bound whose scale does not grow with the number of sample points. It says that the shortest tour length lies near a median with a Gaussian-form upper bound on the probability of a deviation. It does not identify the median or give an algorithm for finding the optimal tour. The abstract form also covers other finite-set functionals once their local regularity condition is established.

The paper proves these claims in ordinary mathematics. This mission asks for machine-checked proofs of the stated concentration, geometric occupancy, and tour-insertion results. The reusable outputs include a finite-set model of Euclidean tours and a precise interface for local regularity; the dyadic occupancy and isolation-weight definitions can support later sections on other geometric structures. No machine-checked proof of these specific chapter results is claimed here.

Difficulty

A naive bounded-differences estimate treats the effect of changing a sample point as if a single fixed worst-case insertion cost applied everywhere. That loses the paper's uniform fluctuation scale: a point can be unusually isolated, and its insertion cost can be much larger than the cost near a typical dense cluster. The central problem is to keep track of those irregular locations while retaining a bound uniform in $N$ . The chapter's dyadic-square counts and isolation weights make this difficulty explicit in the statements.

Formalization scope

Points are pairs of real coordinates constrained to $[0,1]$ , represented as functions on Fin 2. Their distance is the Euclidean $\ell^2$ distance, defined explicitly; the default norm on a Lean function space would give a different metric. The random sample is a product of coordinatewise uniform probability measures. $F$ is the set of distinct sampled locations, so ties have a defined value. Tour length is the minimum cyclic tour cost over the finite set, using the published generic metric-TSP tour model as its base.

Dyadic squares are closed in the local regularity condition. For the single square assigned to a point in the definition of $\alpha$ , the implementation uses half-open cells, with the right endpoint $1$ assigned to the final cell. This resolves only grid-line ties, which have probability zero under the stated sample law. Counts use distinct locations, as does the paper's set $F$ . All probability inequalities are compared in the extended nonnegative reals. The event bound is written with ENNReal.ofReal; a negative formal lower bound represents the paper's trivial probability lower bound. The main theorem explicitly assumes measurability of the sample functional, following the paper's convention that all relevant functions are measurable. Theorems in Section 11.1 retain $t\ge1$ and $t\le\sqrt N/K$ ; the main theorem covers every $t\ge0$ .

The formalization must not replace the square's uniform law by an arbitrary distribution, use a supremum-norm tour, or place the existential constant after $N$ or $L$ . Contributions toward the goal may develop measure-theoretic facts about the product law, finite Euclidean tours, dyadic occupancy bounds, or the insertion estimate. Those interfaces have uses beyond this chapter.

Selected references

Michel Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publications Mathématiques de l'IHÉS 81 (1995), 73–205. DOI: 10.1007/BF02699376.

7 thms3 active usersReviewed

Completed

Combinatorics Discrete Geometry Graph Theory·Captain: mikedeng1

A Combinatorial Theorem in Plane Geometry: Every n-Triangulation Can Be Partitioned into at Most ⌊n/3⌋ FansResearch Paper

Motivation

In a conversation reported by Chvátal, Victor Klee asked for the smallest number $f(n)$ such that every region bounded by a simple closed $n$ -gon is dominated by $f(n)$ points: every point of the region sees one of them along a segment inside the region. In the picturesque language that gave the problem its name, $f(n)$ is the number of guards needed to watch any art gallery with $n$ walls. A comb-shaped polygon (Figure 1 of the paper) shows $f(n) \ge \lfloor n/3 \rfloor$ .

V. Chvátal's three-page note (J. Combin. Theory Ser. B 18 (1975) 39–41) proves the matching upper bound by reducing it to a purely combinatorial statement about triangulated polygons: every such triangulation splits into at most $\lfloor n/3\rfloor$ fans, and a fan is watched by a single guard. The combinatorial theorem is the result this mission formalizes.

Timeline.

1973: Klee poses the question to Chvátal (the paper reports the conversation; the year is O'Rourke's).
1975: Chvátal proves $f(n) = \lfloor n/3\rfloor$ via the fan partition theorem, by induction on $n$ with a four-case analysis.
1978: S. Fisk gives the short proof by 3-colouring the vertices of the triangulation (J. Combin. Theory Ser. B 24 (1978) 374); the smallest colour class is a set of at most $\lfloor n/3\rfloor$ vertices meeting every triangle.
1987 onwards: J. O'Rourke's monograph Art Gallery Theorems and Algorithms (Oxford University Press, 1987) makes the theorem the starting point of a large literature on guarding problems.

Setting

An $n$ -triangulation (p. 39) is a planar graph $G$ with $n$ vertices such that one face is bounded by an $n$ -gon and every other face by a triangle. Its vertices are labelled $0, 1, \dots, n-1$ in their cyclic order around the $n$ -gon, and indices are taken mod $n$ ; the sides of the $n$ -gon are the pairs $\{a, a+1\}$ . Every other edge of $G$ is inner; it is a diagonal $\{a, b\}$ of the $n$ -gon. Two diagonals cross when their endpoints are distinct and alternate around the polygon.

Combinatorially, an $n$ -triangulation requires $n\ge 3$ and is the same thing as a set $D$ of diagonals that pairwise do not cross and is maximal with this property. Its triangles are the 3-element vertex sets all of whose pairs are edges of $G$ ; there are $n - 2$ of them, and they are the bounded faces.

Two triangles are adjacent when they share an edge. A set $F$ of triangles is dual-connected when any two of its members are joined by a chain of adjacent members; such an $F$ is a sub-polygon of $G$ , a $k$ -triangulation with $k = |F| + 2$ , whose inner edges are the edges shared by two of its triangles. Following the paper, a $k$ -triangulation is a fan if one of its vertices, the centre, meets all $k-3$ of its inner edges. A partition of $G$ into fans is a family of fans, pairwise disjoint as sets of triangles, covering all triangles of $G$ . Fans may share vertices and edges.

Formalization targets

Goal: Chvátal's theorem (p. 39)

For every $n \ge 3$ and every $n$ -triangulation $G$ there is a partition of $G$ into $m$ fans with

m \le \left\lfloor \frac{n}{3} \right\rfloor .

Milestones (the claims of the proof, pp. 40–41, in attack order)

Base case. Every $n$ -triangulation with $3 \le n \le 5$ is a fan.
Least span. For $n \ge 6$ , let $k$ be the least integer with $k \ge 4$ such that $G$ has an inner edge $\{j, j+k\}$ . Then $k \le 6$ .
The cut. An inner edge $\{j, j+k\}$ with $2 \le k \le n-2$ cuts $G$ into a $(k+1)$ -triangulation $G_1$ on $j, \dots, j+k$ and an $(n-k+1)$ -triangulation $G_2$ on $j+k, \dots, j$ , whose triangles together are those of $G$ .
The four cases. If $4 \le k \le 6$ and every inner edge $\{a,b\}$ of $G_1$ (relabelled $0,\dots,k$ , $a<b$ ) has $b - a \le 3$ , then $G_1$ is a fan or one of three explicit configurations (cases (2)–(4) of the paper), up to the mirror image $i \mapsto k - i$ .
Tightness. For every $n \ge 3$ some $n$ -triangulation admits no partition into fewer than $\lfloor n/3\rfloor$ fans:

\forall n\ge 3\ \exists G\ \forall P:\quad |P| \ge \lfloor n/3\rfloor .

The goal's only constant is the paper's $\lfloor n/3 \rfloor$ , which milestone 5 shows is best possible.

Significance

The result. The fan partition is a strengthening of the guard bound: the centres of the fans form a set of at most $\lfloor n/3\rfloor$ vertices meeting every triangle, but the partition also says that the triangles split into star-shaped pieces, each visible from one vertex. With the existence of triangulations of simple polygons it yields $f(n) \le \lfloor n/3 \rfloor$ , the art gallery theorem; with Figure 1 it gives $f(n) = \lfloor n/3\rfloor$ .

Formalizing it. The theorem has been proved since 1975, and the platform already has Fisk's consequence: ProofsInTheBook.Chapter36.chapter36 and chapter36_artgallery_combinatorial (Proofs from THE BOOK, Chapter 36) prove that an inductively built family of triangles has a hitting set of at most $n/3$ vertices, and ProofsInTheBook.PolygonGeometryDischarge.artGallery_strict_of_residue proves a geometric guard bound conditional on two assumed inputs. Neither states the fan partition, which is strictly stronger than a hitting set, and neither uses the cyclic labelling of a triangulated polygon. This mission asks for a machine-checked proof of Chvátal's own theorem and of the claims of his proof, on a reusable encoding of triangulated polygons (cyclic labels, non-crossing diagonals, triangles, cutting along a diagonal) that other results on polygon triangulations can build on.

Difficulty

The induction itself is short on paper; the work is in what the paper calls easy. Cutting $G$ along a diagonal and relabelling each piece cyclically must be shown to produce triangulations again, with the triangles split exactly between the two pieces; this is a statement about non-crossing chords that has no counterpart in Mathlib. The case analysis "it is easy to verify that we have one of the following four cases" is an enumeration of all triangulations of a 5-, 6- or 7-gon whose diagonals have span at most 3, and its exhaustiveness (including the mirror images of (2) and (4)) is precisely what the four inductive constructions rely on. The constructions then enlarge one fan of a smaller triangulation, so the induction must be carried out for partitions of arbitrary triangulations, with fans that share edges.

Formalization scope

Encoding of "planar graph". Mathlib has no planar embeddings. An $n$ -triangulation is encoded as the labelled $n$ -cycle on Fin n (vertex $i$ is the paper's $i+1$ ) plus a finset D : Finset (Sym2 (Fin n)) of diagonals that pairwise do not cross and is maximal. Maximality is binding: without it the empty set would "triangulate" every polygon and the goal would hold vacuously.
Triangles are the 3-element vertex sets whose pairs are all edges; in a triangulated polygon every 3-cycle bounds an inner face.
"Partitioned into fans" means a finset of fans, pairwise disjoint as sets of triangles, covering all triangles. A fan must be nonempty, dual-connected, and have a centre on all of its inner edges (edges shared by two of its triangles). Dropping dual-connectedness would turn the goal into Fisk's hitting-set bound; dropping the centre would let the whole triangulation be one "fan". Both clauses are stated.
"[n/3]" is the floor, n / 3 in ℕ. The goal assumes only $n \ge 3$ .
"The least $k \ge 4$ such that $G$ has an edge $(j, j+k)$ " is read over inner edges, with the minimality stated explicitly; read over all edges, a side of span $n-1$ would make the claim trivial for $n = 6, 7$ .
"Cuts $G$ into" is stated for every inner edge of span $2 \le k \le n-2$ (the paper's $4 \le k \le 6$ is a special case), as the pulled-back diagonal sets being triangulations and the triangles splitting between the pieces.
"Mirror image" is the relabelling $i \mapsto k - i$ of $G_1$ (Fin.rev); the four cases are an explicit disjunction on the diagonal set of $G_1$ . The minimality of $k$ enters as the hypothesis that inner edges of $G_1$ have span at most 3.
"Cannot be improved" is stated combinatorially, for the theorem itself; the paper argues it through Figure 1.
Not formalized: Klee's function $f(n)$ , Figure 1's lower bound and the corollary $f(n) \le \lfloor n/3\rfloor$ (p. 41). They need simple polygons in the plane, their interiors, visibility and the existence of triangulations, none of which is available unconditionally.

All definitions are in one file, ChvatalArtGallery.FanPartition.Triangulation; the triangle and cut machinery is reusable for any result on triangulated polygons. Proofs of the milestones, general lemmas on non-crossing diagonal sets (the count $|D| = n-3$ , existence of ears, the dual tree), and alternative proofs of the goal are all welcome.

Selected references

V. Chvátal, A combinatorial theorem in plane geometry, J. Combin. Theory Ser. B 18 (1975) 39–41. https://doi.org/10.1016/0095-8956(75)90061-1
S. Fisk, A short proof of Chvátal's watchman theorem, J. Combin. Theory Ser. B 24 (1978) 374. https://doi.org/10.1016/0095-8956(78)90059-X
J. O'Rourke, Art Gallery Theorems and Algorithms, Oxford University Press, 1987. https://www.science.smith.edu/~jorourke/books/ArtGalleryTheorems/
M. Aigner, G. M. Ziegler, Proofs from THE BOOK, Springer, Chapter "How to guard a museum". https://doi.org/10.1007/978-3-662-57265-8

7 thms3 active usersReviewed

Completed

Combinatorics Discrete Geometry Operations Research·Captain: mikedeng1

A Polynomial Time Algorithm for Counting Integral Points in Polyhedra When the Dimension is Fixed: The Lattice-Point Count of an Integral Simplex Is a Short Signed Sum over Primitive ConesResearch Paper

Counting lattice points in fixed dimension

How many integral points does a polytope contain? The question arises in integer programming, where it measures the size of a feasible set, in combinatorics, where many enumeration problems are lattice-point counts in a polytope (contingency tables, magic squares, flows), in the representation theory of Lie groups, and in the analysis of loop nests in compilers. Counting is #P-hard when the dimension is part of the input, so the natural question is whether the count can be computed in polynomial time when the dimension $d$ is fixed.

Timeline:

1899. In dimension $2$ , Pick's formula leads to a polynomial algorithm.
1983. Lenstra shows that integer feasibility is decidable in polynomial time for fixed $d$ (Lenstra 1983). Deciding whether a lattice point exists does not count them.
1988, 1992. Brion proves that the exponential sum over the lattice points of a rational polytope is the sum of the exponential sums of its vertex cones.
1991. Dyer gives polynomial algorithms in dimensions $3$ and $4$ , based on Dedekind sums (Dyer 1991).
1994. Barvinok proves that for every fixed $d$ the number of lattice points of an integral simplex, and hence of a rational polyhedron, can be computed in polynomial time (Barvinok 1994). The algorithm was later implemented (LattE, barvinok) and is the standard method.

Setting

Points of $\mathbb{R}^d$ have real coordinates and $\langle c,x\rangle=\sum_l c_lx_l$ . For integral vectors $u_1,\dots,u_k\in\mathbb{Z}^d$ , the rational cone they generate is $\operatorname{co}\{u_1,\dots,u_k\}=\{\sum_i\lambda_iu_i:\lambda_i\ge0\}$ . The generators are simple if they are linearly independent, and primitive if moreover they form a basis of the lattice $\mathbb{Z}^d\cap\operatorname{Lin}\{u_1,\dots,u_k\}$ .

The index $\operatorname{Ind}K$ of the cone given by simple generators is the number of integral points in the semi-open parallelepiped $\Pi=\{\sum_i\alpha_iu_i:0\le\alpha_i<1\}$ . It equals $1$ exactly for primitive generators.

The exponential sum of $K$ is $\sigma(K;c)=\sum_{x\in K\cap\mathbb{Z}^d}e^{\langle c,x\rangle}$ . Where it converges it has the closed form

\sigma(K;c)=\Bigl(\sum_{x\in\Pi\cap\mathbb{Z}^d}e^{\langle c,x\rangle}\Bigr)\prod_{i=1}^k\frac{1}{1-e^{\langle c,u_i\rangle}},

and this closed form defines $\sigma$ at every regular point, i.e. every $c$ with $\langle c,u_i\rangle\ne0$ for all $i$ .

An integral simplex is $\Delta=\operatorname{conv}\{v_1,\dots,v_{k+1}\}$ with affinely independent $v_j\in\mathbb{Z}^d$ . Its supporting cone at a vertex $v$ is $K_v=\{u:v+\delta u\in\Delta\text{ for all sufficiently small }\delta>0\}$ . A signed decomposition $K=\sum_i\varepsilon_iK_i$ with integers $\varepsilon_i$ means $\chi_K=\sum_i\varepsilon_i\chi_{K_i}$ on all of $\mathbb{R}^d$ . The constant term of the Laurent expansion of $f$ at $t=0$ is the coefficient of $t^0$ in the expansion of $f$ around its pole at $0$ .

Formalization targets

Goal: the short signed formula (Theorem 1.2, mathematical content)

For $d\ge2$ and every integral simplex $\Delta\subseteq\mathbb{R}^d$ there are, for each vertex $v_j$ , primitive cones $K_{j,i}$ and integers $\varepsilon_{j,i}$ with $K_{v_j}=\sum_i\varepsilon_{j,i}K_{j,i}$ and at most $(2^d)^{T_j}$ terms. Here $T_j$ is the smallest integer

T_j\ge\frac{-\log\log1.9+\log\log\operatorname{Ind}_j}{\log d-\log(d-1)},

and $\operatorname{Ind}_j$ is the index of the edge vectors at $v_j$ . Moreover, for every $c$ orthogonal to no generator of any $K_{j,i}$ ,

\#(\Delta\cap\mathbb{Z}^d)=\sum_j\sum_i\varepsilon_{j,i}\,R(K_{j,i},v_j,c),

where $R(K,v,c)$ is the constant term at $t=0$ of $t\mapsto e^{t\langle c,v\rangle}\sigma(K;tc)$ .

Milestones

Proposition 2.4 with Remark 2.5: the closed form of $\sigma$ for simple cones.
Proposition 4.1: for primitive cones, $\sigma(K;c)=\prod_i(1-e^{\langle c,u_i\rangle})^{-1}$ .
Proposition 2.7 (Brion), for integral simplices.
Corollary 4.2: $R(K,v,c)=Q_k(x;y)\prod_ix_i^{-1}$ with $\deg Q_k\le k$ .
Primitive generators iff $\operatorname{Ind}K=1$ (§5).
Lemma 5.2: a short lattice vector $w$ with $\operatorname{Ind}K_j\le(\operatorname{Ind}K)^{(d-1)/d}$ .
Lemma 5.3: at most $2^d$ cones of smaller index, with signs $\pm1$ .
Theorem 5.4: decomposition into at most $(2^d)^T$ primitive cones.
The display in the proof of Theorem 5.4: $(2^d)^T\le C_1(d)(\log\operatorname{Ind}K)^{C_2(d)}$ .
Lemma 6.1: some $c(t)=(1,t,\dots,t^{d-1})$ , $t\in\{0,\dots,m(d-1)\}$ , is orthogonal to none of $m$ nonzero vectors.

Significance

The goal is the reason Barvinok's algorithm is polynomial. For fixed $d$ , the number of terms is bounded by a polynomial in $\log\operatorname{Ind}K$ , which is polynomial in the input size. Each term is an explicit rational function of inner products (Corollary 4.2). The identity therefore turns lattice-point counting into the evaluation of a short sum. Its consequences include polynomial-time counting for rational polyhedra in fixed dimension, polynomial-time computation of Ehrhart quasi-polynomials, and the theory of short rational generating functions (Barvinok–Woods), which underlies algorithms for parametric integer programming.

The result is proved and classical. As far as known it has not been machine-checked: Mathlib has convex cones, Minkowski's convex body theorem and lattices, but no signed cone decompositions, no generating functions of cones and no Brion identity. The mission produces a formal account of the algorithm's correctness and of the size of its output. Its milestones are statements of independent use: the closed form of cone generating functions, Brion's identity for simplices, and the index-reduction lemma.

Difficulty

The obvious approach is to triangulate the supporting cones into unimodular (primitive) cones. This fails: a cone of index $\operatorname{Ind}K$ may need about $\operatorname{Ind}K$ unimodular cones in any triangulation, which is exponential in the input size. The step that makes the count small is signed decomposition. Signed decomposition uses cones that are not contained in $K$ , combined with signs $\pm1$ , and controls the index through the geometry of numbers rather than through a subdivision of $K$ . The second difficulty is that $c=0$ , where the exponential sum equals the count, is a singular point of every $\sigma(K_i;\cdot)$ . The count is recovered as a constant term of a Laurent expansion, so every identity has to be valid as an identity of meromorphic functions on regular points, and not only where the series converge.

Formalization scope

Points of $\mathbb{R}^d$ are Fin d → ℝ, integral vectors Fin d → ℤ used through their real cast, and $\langle\cdot,\cdot\rangle$ is dotProduct. A cone is given by its generator list, because index, parallelepiped and the closed form of $\sigma$ depend on the generators. Logarithms are natural, and $|u|$ is the sup norm.
Theorem 1.2 is represented by its mathematical content. The paper's statement is "there exists a polynomial time algorithm". No machine model is formalized. The goal is the identity proved on p. 778, with the count of the proof of Theorem 5.4 (p. 777). The algorithmic clauses of Lemmas 5.2, 5.3, 6.1 and Theorem 5.4 are each replaced by the existence statement of the object the algorithm constructs. Lemma 5.3(c), whose constant is unquantified, is omitted.
Over $\mathbb{R}$ . The paper uses $c\in\mathbb{C}^d$ only to speak of meromorphic functions. Here $c$ is real, $\sigma$ is defined by its closed form, and regularity means $\langle c,u_i\rangle\ne0$ for every generator. The constant term is a predicate: $t^Nf(t)$ agrees near $0$ with a real-analytic function whose $N$ -th Taylor coefficient is the value.
Added hypotheses. These are $d\ge2$ wherever $T$ appears, $k\ge1$ in Lemma 5.2, $d\ge1$ in Lemma 5.3, $u_i\ne0$ in Lemma 6.1, and $\operatorname{Ind}K\ge2$ in the display bound. $T=0$ when the index is $1$ . Brion's identity is stated for integral simplices, the only case the proof uses.
Trivializations ruled out. $\sigma$ is never an infinite sum, which would take a junk value off its convergence region. "Primitive" means a lattice basis and not mere linear independence; with the weaker notion the decomposition is trivial. Decompositions hold for every $x\in\mathbb{R}^d$ , not only on $\mathbb{Z}^d$ . The halfspace of Lemma 5.2 is linear, since an affine one would make it vacuous.
Infrastructure. A complete development needs generating functions of simplicial cones, Brion's theorem for simplices, the identity theorem for rational functions in $e^{c_1},\dots,e^{c_d}$ , Minkowski's theorem on a sublattice, and inclusion–exclusion for triangulations. Each is reusable beyond this mission, and contributions of any of these pieces are welcome.

Selected references

A. I. Barvinok, A polynomial time algorithm for counting integral points in polyhedra when the dimension is fixed, Mathematics of Operations Research 19(4), 1994, 769–779. https://doi.org/10.1287/moor.19.4.769
M. Brion, Points entiers dans les polyèdres convexes, Annales scientifiques de l'École Normale Supérieure 21(4), 1988, 653–663. https://doi.org/10.24033/asens.1572
M. Dyer, On counting lattice points in polyhedra, SIAM Journal on Computing 20(4), 1991, 695–707. https://doi.org/10.1137/0220044
H. W. Lenstra Jr., Integer programming with a fixed number of variables, Mathematics of Operations Research 8(4), 1983, 538–548. https://doi.org/10.1287/moor.8.4.538
R. P. Stanley, Enumerative Combinatorics, Vol. 1, Wadsworth & Brooks/Cole, 1986, §4.6. https://doi.org/10.1007/978-1-4615-9763-6
A. Barvinok, K. Woods, Short rational generating functions for lattice point problems, Journal of the AMS 16(4), 2003, 957–979. https://doi.org/10.1090/S0894-0347-03-00428-4

16 thms3 active usersReviewed

Completed

Theoretical Computer Science·Captain: wurtle

Generalization of Hinging PlanesResearch Paper

A continuous piecewise linear (CPWL) function is one assembled from finitely many flat pieces glued along flat seams. Every ReLU network computes such a function, and every such function is computed by some ReLU network. Questions about how deep a network must be are therefore questions about the internal structure of CPWL functions.

In 1993 Breiman built such functions from hinges: maxima of two affine maps. Sums of hinges approximate anything, but from two dimensions up they fail to represent most CPWL functions exactly. Wang and Sun (2005) widened the maxima, proving that every CPWL function on ℝⁿ is a signed sum of maxima of at most n+1 affine maps. Twenty years on it remains the workhorse structural fact, reducing any question about a network to a question about a single max gate and underpinning every known upper bound on the depth of exact representation.

That includes the newest one: at STOC 2026, Bakaev et al disproved the short standing conjecture that ⌈log₂(n+1)⌉ hidden layers are necessary, showing ⌈log₃(n−1)⌉+1 suffice. In this mission we deliver a machine-checked proof of the Wang and Sun theorem so future formalizations of network expressivity can invoke it rather than reprove it. Note that we take as given the lattice representation of Tarela and Martínez, independently proved by Ovchinnikov, which writes any CPWL function as a max of mins of its affine pieces. That is the one external ingredient the argument consumes, and our definition of CPWL builds it in.

3 thms3 active users

Completed

Algebraic Topology Machine Learning Probability·Captain: mikedeng1

Persistence-Based Clustering in Riemannian Manifolds: With High Probability the Algorithm Returns as Many Clusters as the Density Has d₂-Prominent PeaksResearch Paper

Motivation

Mode-seeking clustering groups data points by the peak of an underlying probability density that they "flow up" to. Methods of this kind (mean-shift, graph-based hill climbing) are widely used, but their output depends heavily on noise: a density estimated from finitely many samples has many spurious local maxima, and each of them becomes a cluster. Chazal, Guibas, Oudot and Skraba (INRIA RR-6968, 2009; journal version J. ACM 60(6), 2013, doi:10.1145/2535927) combine graph-based hill climbing with topological persistence. Persistence measures how prominent each peak is, and peaks of low prominence are merged into their neighbours. The paper's main guarantee says when this algorithm recovers the right number of clusters from random samples. It holds on Riemannian manifolds that may be non-compact, and the clustering method is now known as ToMATo.

Setting

Let $\mathbb X$ be an $m$ -dimensional Riemannian manifold, possibly with boundary, with geodesic distance $d_{\mathbb X}$ and $m$ -dimensional Hausdorff measure $\mathcal H^m$ . The strong convexity radius $\varrho_c(\mathbb X)$ is the infimum over $x$ of the largest $r$ such that any two points of the closed ball $B_{\mathbb X}(x,r)$ are joined by a unique shortest path, and that path stays in the ball. Let $f:\mathbb X\to\mathbb R$ be a probability density with respect to $\mathcal H^m$ that is $c$ -Lipschitz, and write $\mathbb F^\alpha=f^{-1}([\alpha,+\infty))$ for its superlevel sets.

Persistence diagram. As $\alpha$ decreases from $+\infty$ to $-\infty$ , path components of $\mathbb F^\alpha$ are born at peaks of $f$ and die when they merge into an older component. The 0-th persistence diagram $D_0f$ records each component as a point $(p_x,p_y)$ of the extended plane $\overline{\mathbb R}^2$ , with birth $p_x$ and death $p_y\le p_x$ ; a component that never dies has $p_y=-\infty$ . The prominence of the peak is $p_x-p_y$ . The diagonal is added with infinite multiplicity. $f$ is tame when this structure is of finite type. For $d_2>d_1\ge0$ , $D_0f$ is $(d_1,d_2)$ -separated when every off-diagonal point either has prominence $<d_1$ (noise), or has prominence $\ge d_2$ and birth $>d_2$ (signal).

Algorithm. The input is $n$ sample points $x_1,\dots,x_n$ , the values $f(x_i)$ , the matrix of distances $d_{\mathbb X}(x_i,x_j)$ and parameters $\delta,\tau$ . The Rips graph $R_\delta$ joins two points at distance $\le\delta$ . The algorithm processes the points by decreasing $f$ and keeps a union-find structure whose entries are rooted at their highest point. When a point is processed, every neighbouring entry whose root is less than $\tau$ higher than the point is merged into the point's entry. The point's own entry is then merged into the neighbouring entry with the highest root, if its own root is less than $\tau$ higher than the point. The output is the set of final entries whose root has value $\ge\tau$ .

Sampling quantities. $\mathcal N_r(A)$ is the least number of closed geodesic balls of radius $r$ covering $A$ , and $\mathcal V_r(A)=\inf_{x\in A}\mathcal H^m(B_{\mathbb X}(x,r))$ .

Formalization targets

Goal: Theorem 4.8 (p. 22)

Assume $\varrho_c(\mathbb X)>0$ , $f$ is a tame $c$ -Lipschitz density, $D_0f$ is $(d_1,d_2)$ -separated, $0<\delta<\min\{\varrho_c(\mathbb X),\frac{d_2-d_1}{5c}\}$ and $\tau\in(d_1+2c\delta,\,d_2-3c\delta)$ . Then for $n$ i.i.d. samples from $f$ ,

\Pr\big[\#\text{clusters}\ne\#\{\text{peaks of prominence}\ge d_2\}\big]\le\mathcal N_{\delta/8}(\mathbb F^{c\delta})\,e^{-n\frac34c\delta\,\mathcal V_{\delta/8}(\mathbb F^{c\delta})}.

Milestones

Lemma 4.3 (p. 17): for $\varepsilon>0$ and $\alpha>c\varepsilon$ , the sample is a geodesic $\varepsilon$ -sample of $\mathbb F^\alpha$ except with probability at most $\mathcal N_{\varepsilon/2}(\mathbb F^\alpha)e^{-n(\alpha-c\varepsilon)\mathcal V_{\varepsilon/2}(\mathbb F^\alpha)}$ .
Theorem 4.5 (p. 19): if a finite $L$ is a geodesic $\delta/4$ -sample of $\mathbb F^\alpha$ , there is a multi-bijection between $D_0f$ and the diagram $D_0\mathcal R^f_\delta(L)$ of the upper-star Rips filtration. Above $\alpha$ it moves points by at most $c\delta$ , and in the lower-right quadrant it moves births by at most $c\delta$ .
Noise image (proof of Thm 4.8, p. 22): the noise points are sent into $\Delta^N_{d_1+2c\delta}\cup\Lambda^W_{d_1+2c\delta}$ .
Signal image (pp. 22–23): the signal points are sent outside that region.
Partition and count (p. 23): for $\tau$ in the range, $D_0\mathcal R^f_\delta(L)$ has exactly as many points in $\Delta^S_\tau\cap\Lambda^E_\tau$ as $D_0f$ has peaks of prominence $\ge d_2$ ; for the tame $D_0f$ both counts are finite.
Algorithm output (p. 23, with §3): for $\tau>0$ the algorithm returns exactly one cluster per point $q$ of the Rips diagram with $q_x-q_y\ge\tau$ and $q_x\ge\tau$ .

Significance

The theorem gives a sample-complexity guarantee for a practical clustering algorithm, with an explicit failure probability. It needs neither compactness of the manifold nor a density bounded away from zero; dense sampling of one superlevel set is enough. The separation hypothesis is a signal-to-noise condition, and it tells the user which range of $\tau$ recovers the true number of clusters.

On the formalization side, the paper's results are proved on paper, but nothing about them is machine-checked. Of the steps, the paper proves Lemma 4.3 and the region analysis. Theorem 4.5 rests on the Rips-filtration analysis of Chazal–Guibas–Oudot–Skraba, SODA 2009, the interleaving and stability results of Chazal et al., SoCG 2009, and the paper's Lemma 4.6. The algorithm-output step (milestone 6) is asserted in the paper, not proved. The mission therefore asks for formal proofs of all six steps. A by-product is the first library of 0-dimensional persistence diagrams, multi-bijections and Rips filtrations on the platform.

Difficulty

The probabilistic step is a union bound over a minimal cover, but it has a gap. Covering balls need not be centred in $\mathbb F^\alpha$ , while $\mathcal V$ is an infimum over balls centred in $\mathbb F^\alpha$ , so the comparison between the two is not justified on a general manifold. Theorem 4.5 is the hardest step. The obvious route, a bottleneck stability theorem, does not apply, because the sample covers only one superlevel set and not $\mathbb X$ . This is why the conclusion distinguishes the quadrant above $\alpha$ , where both coordinates are controlled, from the quadrant below, where only births are. Milestone 6 is a correctness proof for a union-find procedure with ties: entries are not path components, because prominent entries stay separate after their components meet.

Formalization scope

Manifold. $\mathbb X$ is a metric space carrying Mathlib's Riemannian manifold structure (IsRiemannianManifold, a ModelWithCorners for the boundary), so $d_{\mathbb X}$ is dist.
Measures and probability. $\mathcal H^m$ is Mathlib's unnormalized Hausdorff measure of dimension $\dim E$ ; the statements are invariant under rescaling it. Samples are product measures on Fin n → X. "With probability at least $1-B$ " is an upper bound $B\in[0,\infty]$ on the outer measure of the failure event. $e^{-aV}$ uses $e^{-\infty}=0$ and $0\cdot\infty=0$ .
Convexity radius. It is computed in $[0,+\infty]$ , with shortest paths as isometric embeddings of $[0,d(y,y')]$ .
Diagrams. A diagram's multiplicities are computed from the rank function of the filtration, so they are not free data.
Tameness is pinned in a 0-dimensional form: finitely many path components at each level, finitely many critical values, and empty superlevel sets at high levels.
Multi-bijections are bijections between copies of points, the diagonal contributing countably many copies of each of its points.
Separation is imposed on off-diagonal points only. On the diagonal the literal definition is unsatisfiable when $d_1=0$ .
Algorithm. It runs Procedures 1–2 with an explicit union-find state, over every processing order compatible with the sort. The upper star of a point is its set of neighbours processed earlier.
Added hypotheses. $c>0$ in Theorem 4.8 and milestones 3–5 (the paper divides by $c$ ), and $\tau>0$ in milestone 6.

No formalization in which the number of clusters is defined as a count of diagram points, or in which the diagram is a free parameter, is acceptable: either one empties the goal. The running-time and memory claims of §3, the basin approximation of Theorem 4.9 and the Morse-theoretic material of §2.3 are out of scope. Lemma 4.3 is stated as printed, with covering balls centred anywhere, and its proof gap is an open risk that Theorem 4.8 inherits.

Contributions are welcome on every milestone. The persistence-diagram layer (rank functions, multiplicities, multi-bijections) and the union-find correctness proof are reusable beyond this mission.

Selected references

F. Chazal, L. J. Guibas, S. Y. Oudot, P. Skraba, Persistence-Based Clustering in Riemannian Manifolds, INRIA Research Report RR-6968, 2009. https://inria.hal.science/inria-00389390
F. Chazal, L. J. Guibas, S. Y. Oudot, P. Skraba, Persistence-Based Clustering in Riemannian Manifolds, Journal of the ACM 60(6), 2013. https://doi.org/10.1145/2535927
F. Chazal, D. Cohen-Steiner, M. Glisse, L. J. Guibas, S. Y. Oudot, Proximity of Persistence Modules and their Diagrams, Proc. 25th ACM Symposium on Computational Geometry, 2009. https://doi.org/10.1145/1542362.1542407
D. Cohen-Steiner, H. Edelsbrunner, J. Harer, Stability of Persistence Diagrams, Discrete & Computational Geometry 37, 2007. https://doi.org/10.1007/s00454-006-1276-5
F. Chazal, L. J. Guibas, S. Y. Oudot, P. Skraba, Analysis of Scalar Fields over Point Cloud Data, SODA 2009. https://doi.org/10.1137/1.9781611973068.112

41 thms2 active usersReviewed

Dynamic Programming Operations Research Optimization·Captain: mikedeng1

Economic Lot Sizing: An O(n log n) Algorithm That Runs in Linear Time in the Wagner-Whitin Case 1: The Threshold Rule on Efficient Periods Picks an Optimal Next Production PeriodResearch Paper

Motivation

Economic lot sizing asks how to meet a known sequence of demands while deciding when to set up production and how much to carry forward. It is a basic deterministic inventory problem: a setup has a fixed cost, production has a per-unit cost, and inventory may be held for later demand. Recomputing every possible next production period in the standard backward dynamic program takes a quadratic number of candidate comparisons. Wagelmans, Van Hoesel and Kolen use the geometry of cumulative-demand points to identify which candidates can affect the minimum. Their Section 2 gives the threshold rule targeted here. Wagelmans, Van Hoesel and Kolen (1992)

The paper notes independent related work by Aggarwal and Park and by Federgruen and Tzur. The published Prove2Me items for Federgruen and Tzur formalize a forward recursion and its minimal optimal predecessor lists. They address the same planning problem through different state variables; the backward value and efficient periods of this mission are new objects. Wagelmans, Van Hoesel and Kolen (1992), p. S145

Setting

A planning horizon consists of periods $1,\dots,n$ , with $n\ge1$ , and an extra terminal period $n+1$ . In period $i$ , a known demand $d_i\ge0$ must be met without backlogging. The final demand is positive, $d_n>0$ ; a trailing zero-demand period could otherwise be deleted. A production setup costs $f_i\ge0$ , and every unit produced in that period has a marginal cost $c_i\in\mathbb R$ . The sign of $c_i$ is unrestricted. Holding costs have been absorbed into these transformed marginal costs, as in Section 1 of the paper. Define the remaining demand $D(t)=\sum_{j=t}^{n}d_j$ , with $D(n+1)=0$ . If production at $i$ covers demand until the next production period $t$ , then $D(i)-D(t)$ units are produced. Wagelmans, Van Hoesel and Kolen (1992), pp. S146–S147

The backward value $G(t)$ starts at $G(n+1)=0$ and follows Equation (1). At positive demand, it minimizes $f_i+c_i[D(i)-D(t)]+G(t)$ over $i<t\le n+1$ . When $d_i=0$ , skipping setup and using $G(i+1)$ is an additional choice. The paper identifies $G(t)$ with the optimal cost from $t$ onward using the cited zero-inventory property. This mission takes Equation (1) as the definition of $G$ ; it does not formalize the separate equivalence with the original production-plan formulations. Wagelmans, Van Hoesel and Kolen (1992), p. S147

For a fixed $i$ , plot the finite points $(D(t),G(t))$ for $i<t\le n+1$ . Their lower convex envelope is a piecewise linear graph. Its endpoints and places where its slope changes are breakpoints; the corresponding period indexes form the efficient set $E_i$ . Write $\operatorname{succ}_i(t)$ for the next larger index in $E_i$ . The consecutive-point ratio is $r_i(t)=[G(t)-G(\operatorname{succ}_i(t))]/[D(t)-D(\operatorname{succ}_i(t))]$ . These objects have no optimization over production policies hidden in their definitions. Wagelmans, Van Hoesel and Kolen (1992), pp. S147–S150

Formalization targets

Efficient candidates

Proposition 1 says every candidate outside $E_i$ can be removed without changing the minimum:

\min_{i<t\le n+1}\{c_i[D(i)-D(t)]+G(t)\}=\min_{t\in E_i}\{c_i[D(i)-D(t)]+G(t)\}.

The endpoint and slope claims establish the geometry used in this reduction. Proposition 2 compares neighboring efficient periods using $r_i(t)$ and $c_i$ . Wagelmans, Van Hoesel and Kolen (1992), pp. S147–S149

Threshold rule and backward value

The selected period is the first efficient index whose ratio falls below the current marginal cost, with the terminal period as fallback:

q(i)=\min\bigl(\{n+1\}\cup\{t\in E_i:t<n+1,\ r_i(t)<c_i\}\bigr).

The goal asserts that the full candidate minimum is attained there and that the algorithm's resulting assignment equals $G(i)$ :

\min_{i<t\le n+1}\{c_i[D(i)-D(t)]+G(t)\}=c_i[D(i)-D(q(i))]+G(q(i)),

G(i)=\begin{cases}f_i+c_i[D(i)-D(q(i))]+G(q(i)),&d_i>0,\\ \min\{G(i+1),f_i+c_i[D(i)-D(q(i))]+G(q(i))\},&d_i=0.\end{cases}

This states the mathematical choice and value; it does not assert a time bound. Wagelmans, Van Hoesel and Kolen (1992), pp. S149–S150

Significance

The result reduces a finite dynamic-programming minimum to the vertices of a lower envelope and gives an explicit threshold for choosing a minimizing vertex. It explains which future production period the backward recursion may select even when marginal costs are negative or some intermediate demands are zero. The paper uses ordered slopes to implement the selection efficiently; a solver proving the statements here establishes the mathematical correctness of that selection independently of a particular list representation. Wagelmans, Van Hoesel and Kolen (1992), pp. S148–S150

The paper's result is proved in print. The Lean statements are open proof obligations in this proposal. A complete development would add reusable finite lower-envelope facts, including vertex dominance and the order of adjacent slopes, as well as a machine-checked treatment of the zero-demand tie convention. The previously published forward-algorithm items do not supply these backward-recursion facts.

Difficulty

A candidate point can have a smaller value $G(t)$ than a neighboring point yet still fail to minimize $c_i[D(i)-D(t)]+G(t)$ for a given $c_i$ . Comparing raw values alone therefore cannot identify the selected period. The lower envelope must retain exactly the points that can support a line of slope $c_i$ , and their consecutive ratios must be ordered. Zero demand creates repeated abscissae; without a representative rule, a ratio may have denominator zero and the successor is ambiguous. Wagelmans, Van Hoesel and Kolen (1992), pp. S147–S150

Formalization scope

Periods are natural numbers starting at $1$ ; $n+1$ is the terminal sentinel. Demands, setup costs, marginal costs and values are real numbers. Finite minima use attained Finset.inf', with nonempty domains. The effective score omits the common setup cost $f_i$ . No sign restriction is imposed on $c_i$ . The efficient set is determined by a finite chord test for lower-envelope vertices: points on a chord are excluded, and at identical abscissa and height the earliest period is retained. This makes explicit the paper's zero-demand replacement convention on p. S150. The successor is used only on nonsentinel efficient periods; there its denominator is positive. Wagelmans, Van Hoesel and Kolen (1992), pp. S147–S150

The algorithm's printed Iterations use $d_{1n}$ where $d_{in}$ is required; the Lean statement uses $D(i)-D(q(i))=d_{i,q(i)-1}$ , matching the preceding display and the numerical table. The zero-demand branch explicitly includes skipping setup. The selector is the ratio-threshold rule, rather than an argmin, and the efficient set is the actual lower-envelope vertex set rather than all periods. A finite zero-demand example and Tables I–II are used as verification data. The paper's $O(n\log n)$ bound, the binary-search implementation, the amortized list updates, the $O(n)$ Wagner–Whitin specialization and the final production-plan construction are outside this mission: they require additional algorithm-state and cost-model statements. Wagelmans, Van Hoesel and Kolen (1992), pp. S149–S152

Selected references

A. Wagelmans, S. Van Hoesel and A. Kolen, Economic Lot Sizing: An O(n log n) Algorithm That Runs in Linear Time in the Wagner-Whitin Case, Operations Research 40, Supplement 1 (1992), S145–S156. DOI: 10.1287/opre.40.1.S145

8 thms2 active usersReviewed

Linear algebra Machine Learning·Captain: mikedeng1

Turning Big Data into Tiny Data: Constant-Size Coresets for k-Means, PCA, and Projective Clustering II: An SVD Coreset of at Most 2(j + ⌈j/ε⌉ − 1) Weighted Points for Affine j-SubspacesResearch Paper

Motivation

Principal component analysis (PCA) asks for the $j$ -dimensional affine subspace that best fits a cloud of $n$ points in $\mathbb R^d$ in the least-squares sense. When $n$ is very large, or the points arrive as a stream or are spread over many machines, one wants to replace the data by a small summary on which the cost of every candidate subspace can still be evaluated, up to a factor $1+\varepsilon$ . Such a summary is a coreset. Coresets for the $j$ -subspace problem are the building block of the streaming and distributed PCA and projective clustering algorithms of Feldman, Schmidt and Sohler (SIAM J. Comput. 49(3), 2020), whose sizes depend on $j$ and $\varepsilon$ only, not on $n$ or $d$ .

For linear subspaces (through the origin) the paper's Theorem 17 gives a deterministic coreset of $m=O(j/\varepsilon)$ points read off the singular value decomposition. Data are rarely centred, though, and subtracting the mean before the computation does not survive the union of coresets with different means (p. 616). Section 4 of the paper repairs this: Theorem 19 gives a coreset for affine $j$ -subspaces whose points already carry the mean, at the price of doubling the size and weighting the points. This mission formalizes Theorem 19.

Setting

A data set of $n$ points in $\mathbb R^d$ is a matrix $A\in\mathbb R^{n\times d}$ whose rows $A_{i*}$ are the points. For a nonempty set $C\subseteq\mathbb R^d$ and a point $p$ , $\operatorname{dist}(p,C)=\inf_{c\in C}\|p-c\|_2$ . The cost of $C$ is

\operatorname{dist}^2(A,C)=\sum_{i=1}^n\operatorname{dist}^2(A_{i*},C),

and for weights $w_1,\ldots,w_r\ge0$ on the rows of $S\in\mathbb R^{r\times d}$ the weighted cost is $\sum_i w_i\operatorname{dist}^2(S_{i*},C)$ . The squared Frobenius norm is $\|M\|_F^2=\sum_{i,k}M_{ik}^2$ .

A singular value decomposition (SVD) of $A$ is a factorization $A=U\Sigma V^T$ with $U\in\mathbb R^{n\times n}$ and $V\in\mathbb R^{d\times d}$ orthogonal and $\Sigma\in\mathbb R^{n\times d}$ rectangular diagonal with nonnegative, nonincreasing diagonal entries $\sigma_1\ge\sigma_2\ge\cdots$ . $\Sigma^{(m)}$ keeps the first $m$ diagonal entries and sets the rest to $0$ ; the $m$ -rank approximation is $A^{(m)}=U\Sigma^{(m)}V^T$ (Definition 1).

The mean row is $\mu(A)=\frac1n\sum_iA_{i*}$ and the centred matrix is $A'=A-\mathbb 1\cdot\mu(A)$ , whose rows are $A_{i*}-\mu(A)$ .

Algorithm 1, subspace-Coreset $(A,j,\varepsilon)$ , sets $m=\min\{n,d,j+\lceil j/\varepsilon\rceil-1\}$ , returns the matrix $S$ of the first $m$ rows of $\Sigma^{(m)}V^T$ (all other rows are zero), the weights $w_i=1$ , and $\Delta=\|A-A^{(m)}\|_F^2$ .

Algorithm 2, affine- $j$ -subspace-Coreset $(A,j,\varepsilon)$ , runs Algorithm 1 on $A'$ , obtaining $(S',\Delta)$ with $m=|S'|$ , and returns

S=\mathbb 1\cdot\mu(A)+\sqrt{\frac mn}\cdot\begin{bmatrix}S'\\-S'\end{bmatrix}\in\mathbb R^{2m\times d},\qquad w=\Bigl(\frac n{2m},\ldots,\frac n{2m}\Bigr),

together with $\Delta$ .

Formalization targets

Goal: Theorem 19 (p. 617)

Let $n\ge1$ , $j\in[1,d-1]$ and $\varepsilon>0$ , and let $(S,\Delta,w)$ be the output of Algorithm 2 for any SVD of $A'$ . Then $S\in\mathbb R^{(2m)\times d}$ , $m\le j+\lceil j/\varepsilon\rceil-1$ , $\Delta\ge0$ , and for every affine $j$ -dimensional subspace $C$ of $\mathbb R^d$ ,

\operatorname{dist}^2(A,C)\le\sum_{i=1}^{2m}w_i\operatorname{dist}^2(S_{i*},C)+\Delta\le(1+\varepsilon)\operatorname{dist}^2(A,C).

Milestones

Theorem 17 (p. 615): for any SVD of $A$ , the output of Algorithm 1 satisfies $\operatorname{dist}^2(A,L)\le\sum_{i=1}^m\operatorname{dist}^2(S_{i*},L)+\Delta\le(1+\varepsilon)\operatorname{dist}^2(A,L)$ for every $j$ -dimensional linear subspace $L$ .
Lemma 18 (p. 616): if $\mu(M)=\vec0$ , $L$ is a linear $j$ -subspace and $t\in L^\perp$ , then $\operatorname{dist}^2(M,t+L)=\operatorname{dist}^2(M,L)+n\|t\|^2$ .
Display (7) (p. 618): with $S''=\sqrt{m/n}\,[S';-S']$ , $\operatorname{dist}^2(A',L)\le\frac n{2m}\operatorname{dist}^2(S'',L)+\Delta\le(1+\varepsilon)\operatorname{dist}^2(A',L)$ for every linear $j$ -subspace $L$ .

Theorem 17 rests on Corollary 16 and Claim 3 of the paper; those are milestones of the companion mission Turning Big Data into Tiny Data … I and are not posed again here.

Significance

The result. Theorem 19 gives a deterministic summary of $2m\le2(j+\lceil j/\varepsilon\rceil-1)$ weighted points and one scalar that preserves the cost of every affine $j$ -subspace within $1+\varepsilon$ , for arbitrary data, with no assumption on the mean. Because its points carry the mean, coresets of different data sets can be merged, which the merge-and-reduce streaming constructions of the paper's later sections need. Any $(1+\varepsilon')$ -approximate PCA solution computed on the coreset is then a $(1+\varepsilon)(1+\varepsilon')$ -approximate solution for the full data.

Formalizing it. The theorem is proved in the paper; no machine-checked proof of it, or of any coreset theorem, exists on the platform. A complete development would produce the cost identities for sums of squared distances to linear and affine subspaces in Lean, the effect of centring and orthogonal translation on these costs, and the use of the SVD truncation as a summary, all of which are reusable for other PCA, low-rank approximation and projective clustering results.

Difficulty

The obvious construction, centring the data, computing the linear coreset of the centred data and adding the mean back, fails: the linear coreset $S'$ need not have mean $\vec0$ , and translating a subspace by $t\perp L$ changes the cost of a point set by a multiple of $\|t\|^2$ that depends on the number of points (p. 617). The paper's construction has to match both the mean and the total weight of the original data while keeping the linear-subspace guarantee, and the formal proof has to carry this through the reduction of an arbitrary affine subspace to a linear one plus an orthogonal translation. Beneath it lies Theorem 17, which needs the SVD-based estimate of the companion mission (Corollary 16) and the passage from the $n$ -row matrix $A^{(m)}=U\Sigma^{(m)}V^T$ to the $m$ nonzero rows of $\Sigma^{(m)}V^T$ . Distances to subspaces in Lean are infima over sets, so the identities $\operatorname{dist}^2(A,L)=\|AY\|_F^2$ for an orthonormal basis $Y$ of $L^\perp$ must themselves be established.

Formalization scope

Representation. Points are rows of Matrix (Fin n) (Fin d) ℝ, read as points of EuclideanSpace ℝ (Fin d). $\operatorname{dist}$ is Metric.infDist. Linear $j$ -subspaces are Submodules of finrank $j$ ; affine ones are AffineSubspaces whose direction has finrank $j$ , and $t+L$ is AffineSubspace.mk' t L. The SVD and $A^{(m)}$ are the published ProjLikeRetr.FixedRank.IsSVD and truncSVD. Every statement holds for an arbitrary SVD; none is chosen.
Pinned hypotheses and readings.
1. The page's " $\Delta>0$ " (Theorems 17 and 19) is false when $\operatorname{rank}A'\le m$ , for instance when all points coincide; the statements claim $\Delta\ge0$ .
2. $n\ge1$ is added to Theorem 19 and (7), since Algorithm 2 divides by $n$ .
3. "subspace-Coreset $(P,j,\varepsilon)$ " is read with $P=A$ .
4. Theorem 17's $S\in\mathbb R^{m\times d}$ is the first $m$ rows of $\Sigma^{(m)}V^T$ , as the text before it says, although Algorithm 1, line 3 writes the whole matrix.
5. Lemma 18's "affine $j$ -dimensional subspace $L$ " is a linear subspace: the lemma uses $L^\perp$ , and the proof of Theorem 19 applies it to linear $L$ .
6. Theorem 19's affine subspace $C$ is also required to be nonempty; this follows from $j\ge1$ and guards against Mathlib's convention that the distance to $\emptyset$ is $0$ .
Conventions. $m\le j+\lceil j/\varepsilon\rceil-1$ is written $m+1\le j+\lceil j/\varepsilon\rceil$ . Diagonal positions of $\Sigma$ are 0-based in Lean. The $2m$ output rows are $\mu+\sqrt{m/n}\,S'_{i*}$ followed by $\mu-\sqrt{m/n}\,S'_{i*}$ . Weights are the real number $n/(2m)$ with $m=|S'|$ , not the cap $j+\lceil j/\varepsilon\rceil-1$ .
Not trivializable. The goal quantifies over affine, not linear, subspaces; the coreset is built from an SVD of the centred matrix $A'$ and $\Delta$ is the residual of $A'$ , so neither the mean nor the centring can be dropped; and no hypothesis is vacuous (any data matrix with any of its SVDs satisfies them).
Not formalized. The running-time clauses (" $O(\min\{nd^2,dn^2\})$ time") and §4.1 (weighted inputs).
Welcome contributions. Lemmas computing $\operatorname{dist}^2$ to subspaces via orthogonal projections, invariance of these costs under orthogonal maps, and the cost identity for symmetric point sets.

Selected references

D. Feldman, M. Schmidt, C. Sohler, Turning Big Data into Tiny Data: Constant-Size Coresets for k-Means, PCA, and Projective Clustering, SIAM J. Comput. 49(3):601–657, 2020. https://doi.org/10.1137/18M1209854
P.-A. Absil, J. Malick, Projection-like Retractions on Matrix Manifolds, SIAM J. Optim. 22(1):135–158, 2012 (source of the published SVD definition used here). https://doi.org/10.1137/100802529

7 thms1 active userReviewed

Linear algebra Machine Learning·Captain: mikedeng1

Turning Big Data into Tiny Data: Constant-Size Coresets for k-Means, PCA, and Projective Clustering I: The Rank-m SVD Truncation Plus Its Residual Preserves the Cost of Every j-Dimensional ShapeResearch Paper

Motivation

Large data sets make clustering and subspace fitting expensive because a candidate solution must be evaluated against every input point. A dimensionality reduction replaces the data by a lower-rank matrix whose costs approximate those of the original input for an entire class of candidate solutions. Feldman, Schmidt, and Sohler study reductions that retain enough information for $k$ -means, principal component analysis, and projective clustering. Their journal paper identifies a rank truncation and one residual scalar that preserve the fitting cost of every shape lying in a low-dimensional linear subspace Feldman, Schmidt, and Sohler (2020), Theorem 22.

The published article also records that some coreset sizes in its 2013 conference version were incorrect. This mission uses the 2020 journal statement and its page numbering throughout. The authors cite earlier SVD-based approximations to $k$ -means on p. 613, while their Theorem 22 gives a uniform cost guarantee for arbitrary nonempty shapes contained in a $j$ -dimensional subspace Feldman, Schmidt, and Sohler (2020), pp. 603, 613, 620.

Setting

The input is a real matrix $A\in\mathbb R^{n\times d}$ . Its $n$ rows are points in $\mathbb R^d$ . For a nonempty set of candidate locations or shapes $C\subseteq\mathbb R^d$ , let $\operatorname{dist}(a_i,C)$ be the infimum of Euclidean distances from row $a_i$ to points of $C$ . The shape cost is

\operatorname{dist}^2(A,C)=\sum_{i=1}^{n}\operatorname{dist}(a_i,C)^2.

The set $C$ need not be closed and need not be a subspace. For example, it can be a finite set of cluster centers. The restriction is that all of its points lie in some linear subspace of dimension $j$ . This matches the paper's shape class in §5; the affine case is treated separately Feldman, Schmidt, and Sohler (2020), pp. 619–620.

Fix a singular value decomposition $A=U\Sigma V^T$ , where $U$ and $V$ are orthogonal and the diagonal entries of the rectangular matrix $\Sigma$ are nonnegative and nonincreasing. The entry $\sigma_i$ is indexed from one. The rank- $m$ truncation $A^{(m)}=U\Sigma^{(m)}V^T$ keeps the first $m$ diagonal entries and sets the rest to zero. Its squared Frobenius residual is $\Delta=\|A-A^{(m)}\|_F^2$ . The corrected cost of $C$ is $\operatorname{dist}^2(A^{(m)},C)+\Delta$ Feldman, Schmidt, and Sohler (2020), Definition 1 and §2.

Formalization targets

Linear subspace estimates

The milestones first record the matrix Pythagorean identity, the $j\sigma_{m+1}^2$ projection and residual bounds, and the lower bound on the cost of a linear $j$ -subspace. They then state the residual-corrected approximation in Corollary 16:

\|AY\|_F^2\le\|A^{(m)}Y\|_F^2+\Delta\le(1+\varepsilon)\|AY\|_F^2, \qquad m\ge\lceil j/\varepsilon\rceil+j-1.

Here $Y$ has $d-j$ orthonormal columns spanning the complement of the candidate subspace. Corollary 20, Corollary 21, and display (9) connect these linear estimates to costs of general sets $C$ Feldman, Schmidt, and Sohler (2020), pp. 604, 613–615, 619–620.

Goal: uniform shape-cost preservation

The goal is Theorem 22. For $1\le j\le d-1$ , $0<\varepsilon\le1$ , and $\lceil8j/\varepsilon^2\rceil-1\le m\le\min\{n,d\}-1$ , every nonempty $C$ contained in a linear $j$ -dimensional subspace satisfies

\left|\bigl(\operatorname{dist}^2(A^{(m)},C)+\|A-A^{(m)}\|_F^2\bigr) -\operatorname{dist}^2(A,C)\right| \le\varepsilon\operatorname{dist}^2(A,C).

The quantifier over $C$ makes this a guarantee for every admissible candidate on the same reduced data, rather than a statement about one selected optimum Feldman, Schmidt, and Sohler (2020), Theorem 22, p. 620.

Significance

The theorem preserves objective values after replacing $A$ by a rank- $m$ matrix and one number. For a fixed $j$ and accuracy parameter, the rank threshold depends on $j$ and $\varepsilon$ , with no direct dependence on the number of points $n$ or ambient dimension $d$ except the upper bound on feasible $m$ . In the paper, the result leads to a guarantee for $k$ -means candidates, since $k$ centers span a linear subspace of dimension at most $k$ Feldman, Schmidt, and Sohler (2020), Corollary 23, p. 621.

The result is proved in the paper, but this mission's Lean theorems are posed with sorry; they do not yet have machine-checked proofs. A completed development would connect a reusable rectangular SVD model, matrix projection identities, infimum distances to arbitrary nonempty sets, and a uniform cost inequality. The SVD definition is already published in the platform library; the row-cost and singular-value conventions here supply the interface needed for this paper Feldman, Schmidt, and Sohler (2020), §§2, 3, 5.

Difficulty

The linear subspace bound compares a projection cost with a tail sum of squared singular values. The paper recalls that fact in §3 without proving it, so the formal development needs a suitable singular-value inequality or a derivation from existing matrix approximation results. For general shapes $C$ , a bound on the cost of one linear subspace does not by itself control the distance from each projected point to every point of $C$ . The remaining milestones state the projection error, the squared-distance perturbation bound, and the Pythagorean cost split that address that gap Feldman, Schmidt, and Sohler (2020), pp. 613, 619–621.

The proof printed after Theorem 22 invokes earlier corollaries under a stronger rank threshold than the theorem states. The mission keeps the printed theorem threshold, whose claim remains valid; a formal proof must bridge that discrepancy Feldman, Schmidt, and Sohler (2020), pp. 620–621.

Formalization scope

Matrices are Matrix (Fin n) (Fin d) ℝ, and rows are points of EuclideanSpace ℝ (Fin d). Squared Frobenius norm is an explicit finite sum of squared entries. Shape cost sums squared Metric.infDist values over rows. Since Mathlib assigns a real default value to distance from the empty set while the paper assigns infinity, every theorem about a general shape $C$ requires C.Nonempty. This is the page's own requirement for Theorem 22 and Corollary 21, and is also needed for display (9).

The SVD and its truncation use the published ProjLikeRetr.FixedRank.IsSVD and truncSVD. Every SVD statement quantifies over an arbitrary valid triple $(U,\Sigma,V)$ ; tied singular values do not fix a unique truncation. The local $\sigma_i$ is one-based, while truncSVD m keeps zero-based diagonal positions below $m$ . Orthonormal columns of $X$ satisfy $X^TX=I$ , their orthogonal complement has $d-j$ columns, and projection in ambient coordinates is $AXX^T$ . Theorem 22 quantifies over arbitrary nonempty $C$ contained in a linear $j$ -subspace; it does not restrict $C$ to subspaces or replace linear containment by affine containment.

The integer inequalities in Lean use additive forms such as $\lceil8j/\varepsilon^2\rceil\le m+1$ to avoid truncated natural-number subtraction. The theorem retains the printed $m$ threshold, including the proof gap described above. Running-time clauses are outside the mission's mathematical statements. Contributions are welcome toward the singular-value lower bound, the projection and infimum-distance identities, and the final uniform inequality; the matrix and distance definitions are reusable in the companion affine-subspace mission.

Selected references

Dan Feldman, Melanie Schmidt, and Christian Sohler, Turning Big Data into Tiny Data: Constant-Size Coresets for k-Means, PCA, and Projective Clustering, SIAM Journal on Computing 49(3):601–657, 2020. DOI: 10.1137/18M1209854.

11 thms1 active userReviewed

Combinatorics Discrete Geometry·Captain: wurtle

A power saving for planar halving linesResearch Paper

Motivation

Given $n$ points in the plane with no three on a line, a halving line is a line through two of the points that leaves exactly half of the remaining points on each side. How many halving lines can an $n$ -point set have? The question is the middle case of the $k$ -set problem: count the $k$ -element subsets that a line can cut off. It controls the complexity of levels in line arrangements, and through them the running time of many algorithms in computational geometry (levels, ham-sandwich cuts, $k$ -th order Voronoi diagrams).

The gap between the bounds is one of the best known in discrete geometry: the upper bound has been $O(n^{4/3})$ since 1998, while the best constructions give only $n\,e^{\Omega(\sqrt{\log n})}$ .

Timeline

1971, 1973. Lovász, and Erdős–Lovász–Simmons–Straus, prove the $O(n^{3/2})$ upper bound and construct sets with $\Omega(n\log n)$ halving lines.
1992. Pach, Steiger and Szemerédi improve the upper bound by an iterated-logarithm factor (doi:10.1007/BF02187829).
1998. Dey proves that the number of $k$ -sets is $O(n(k+1)^{1/3})$ , hence $O(n^{4/3})$ halving lines, using convex chains and the crossing lemma (doi:10.1007/PL00009354).
2001, 2008. Tóth constructs sets with $n\,e^{\Omega(\sqrt{\log n})}$ halving lines (doi:10.1007/s004540010022); Nivasch simplifies the construction and improves the constant (doi:10.1090/conm/453/08804).
2009. Pinchasi relates changes between balanced cuts to measure concentration in the plane (doi:10.1145/1542362.1542393).
2024. Alonso, López and Rodrigo improve a lower-order term while keeping the exponent $4/3$ (doi:10.3390/sym16070936).

The source of this mission is an OpenAI preprint dated September 25, 2026, which claims the first power saving below $4/3$ .

Setting

Let $P=(P_1,\dots,P_n)$ be distinct points of $\mathbb R^2$ with no three collinear. For $i\ne j$ , the orientation $\operatorname{orient}(P_i,P_j,P_l)$ is the usual $2\times2$ determinant; its sign says on which side of the line $P_iP_j$ the point $P_l$ lies. For even $n$ , an unordered pair $\{i,j\}$ is a halving pair if exactly $(n-2)/2$ points lie strictly on each side of the line $P_iP_j$ ; $h(P)$ is the number of halving pairs.

A configuration is generic if moreover its $x$ -coordinates are distinct, the slopes of the $\binom n2$ segments $P_iP_j$ are distinct, and no point where two of these segments properly cross lies on a third segment. Fix a rank $0\le k\le n$ . For a slope $s$ , mark the $k$ points with smallest value of $y-sx$ . As $s$ increases from $-\infty$ to $+\infty$ , the marked set changes by exchanging one point for another; each change is a switch, and $S_k(P)$ is the total number of switches. A switch at rank $k$ happens at the slope of $P_iP_j$ exactly when $k-1$ points lie strictly below the line $P_iP_j$ . At the middle rank, switches are halving pairs.

Formalization targets

Goal: Theorems 1.1 and 1.2

\exists\,\varepsilon>0,\ C,\ n_0:\quad h(P)\le C\,n^{4/3-\varepsilon}\quad\text{for all even } n\ge n_0 \text{ and all } P \text{ with no three collinear};

\exists\,\varepsilon>0,\ C:\quad S_k(P)\le C\,n^{4/3-\varepsilon}\quad\text{for all } n\ge1,\ \text{generic } P,\ 0\le k\le n.

The Lean statement OAI.PlanarHalving.power_bounds is the conjunction of these two clauses and is open on the platform. Neither $\varepsilon$ nor $C$ is specified, so the goal asserts only the shape of the improvement and survives any later numerical sharpening.

Significance

A power saving $n^{4/3-\varepsilon}$ is the first improvement of the exponent in Dey's bound since 1998. The uniform version over all ranks gives, through shallow cuttings, a $k$ -sensitive bound $O(n(k+1)^{1/3-\varepsilon_0})$ for planar $k$ -sets and for the complexity of the $k$ -level in an arrangement of lines (Corollary 1.3). The saving is non-quantitative: the paper's compactness argument gives no numerical $\varepsilon$ .

The result is proved in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. Formalizing it would certify a long compactness argument (limiting measures, rank coordinates, differentiation of monotone functions) whose ineffective nature makes informal checking hard.

Difficulty

Dey's argument decomposes the halving graph into convex chains and applies the crossing lemma; both ingredients are tight on their own, so a power saving must show that configurations nearly attaining the crossing-lemma bound cannot exist. The bound must also hold uniformly over all ranks $k$ , because restricting a block of switches to the points that take part in it changes the rank. Since the lower-bound constructions are far below $n^{4/3}$ , there is no extremal example to guide the argument.

Formalization scope

Points are ℝ × ℝ, configurations are P : Fin n → Point; GeneralPosition P is injectivity plus nonvanishing orient for every triple of distinct indices.
halvingCount P counts pairs i < j with sideCount P i j = (n-2)/2 and sideCount P j i = (n-2)/2, where sideCount counts points with strictly positive orientation. Natural-number division is harmless because $n$ is even.
Generic P adds distinct first coordinates, distinct slopes of index pairs, and the condition that no proper crossing of two determined open segments lies on a third closed segment.
switchCount P k counts pairs i < j with 0 < k < n and exactly k - 1 points strictly below the line through P i, P j in the order $y-sx$ . Ranks $0$ and $n$ therefore contribute zero, as in the paper.
slope divides by the $x$ -difference; the generic hypothesis makes it nonzero.

A complete development needs the crossing lemma, convex-chain decompositions of the rotating-line process, weak compactness of finite Borel measures, the Radon–Nikodym and Lebesgue differentiation theorems, Rademacher-type differentiability of monotone functions, and planar Jordan-curve separation. Contributions formalizing Dey's $O(n^{4/3})$ bound, Theorem 2.1 (uniform activity packing) and Proposition 8.1 (the fixed-scale recurrence) are welcome.

Selected references

OpenAI, A power saving for planar halving lines, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-power-saving-for-planar-halving-lines-September-25-2026/main.pdf
T. K. Dey, Improved bounds for planar $k$ -sets and related problems, Discrete Comput. Geom., 1998. https://doi.org/10.1007/PL00009354
J. Pach, W. Steiger, E. Szemerédi, An upper bound on the number of planar $k$ -sets, Discrete Comput. Geom., 1992. https://doi.org/10.1007/BF02187829
P. Erdős, L. Lovász, A. Simmons, E. G. Straus, Dissection graphs of planar point sets, in A Survey of Combinatorial Theory, 1973.
L. Lovász, On the number of halving lines, Ann. Univ. Sci. Budapest. Eötvös Sect. Math., 1971.
G. Tóth, Point sets with many $k$ -sets, Discrete Comput. Geom., 2001. https://doi.org/10.1007/s004540010022
G. Nivasch, An improved, simple construction of many halving edges, Contemp. Math. 453, 2008. https://doi.org/10.1090/conm/453/08804
R. Pinchasi, Halving lines and measure concentration in the plane, SoCG 2009. https://doi.org/10.1145/1542362.1542393
E. Alonso, M. López, J. Rodrigo, An improvement of the upper bound for the number of halving lines of planar sets, Symmetry, 2024. https://doi.org/10.3390/sym16070936

2 thms1 active userReviewed

Discrete Geometry Theoretical Computer Science·Captain: mikedeng1

An Optimal Algorithm for Approximate Nearest Neighbor Searching in Fixed Dimensions: Priority Search in a BBD-Tree Visits at Most ⌈1 + 6d/ε⌉^d Leaf CellsResearch Paper

Motivation

Nearest neighbor searching asks for a data structure that stores $n$ points $S\subset\mathbb R^d$ and, given a query point $q$ , returns a point of $S$ closest to $q$ . It underlies classification, vector quantization, data compression, pattern recognition and similarity search in databases. In dimension $d\ge 3$ , exact methods either use space growing like $n^{\lceil d/2\rceil}$ or answer queries in time close to linear in $n$ , so practical systems settle for an approximate answer: a point whose distance to $q$ is within a factor $1+\varepsilon$ of the true nearest distance.

Arya, Mount, Netanyahu, Silverman and Wu (J. ACM 45 (1998), 891–923) gave the first structure for this problem that is simultaneously of linear size, built in $O(dn\log n)$ time, and answers $(1+\varepsilon)$ -approximate queries in $O(c_{d,\varepsilon}\log n)$ time for any fixed $d$ , with $c_{d,\varepsilon}\le d\lceil 1+6d/\varepsilon\rceil^d$ . The structure, the balanced box-decomposition tree (BBD-tree), and the priority search on it became the basis of the ANN library of Mount and Arya.

Timeline. Arya and Mount (SODA 1993) studied approximate nearest neighbor queries in fixed dimensions; the conference version of this paper (SODA 1994) gave an optimal algorithm; the journal version (1998), which the paper itself describes as differing from the conference version by a single balanced structure without auxiliary data structures (p. 897), is the one formalized here. Later work, for example by Har-Peled, Indyk and Motwani (2012), addressed the exponential dependence on $d$ .

Setting

Points are vectors in $\mathbb R^d$ . For an integer $m\ge1$ the $L_m$ distance is $\operatorname{dist}_m(x,y)=(\sum_i|x_i-y_i|^m)^{1/m}$ , and for $m=\infty$ it is $\max_i|x_i-y_i|$ . A rectangle is a product $\prod_i[\ell_i,h_i]$ of closed intervals; its size is the length of its longest side. A box is a rectangle with positive sides whose aspect ratio, longest over shortest side, is at most $3$ .

A cell consists of an outer box $b_O$ and an optional inner box $b_I$ ; as a point set it is $b_O$ , or the closure of $b_O\setminus b_I$ . Its size is the size of $b_O$ . The inner box must be sticky for the outer one: in every coordinate, each of the two gaps between the inner and the outer interval is either $0$ or at least the width of the inner interval.

A BBD-tree subdivides a root box by two operations. A fair split cuts a cell by a hyperplane $x_i=t$ into a low and a high child; a shrink cuts it by a shrinking box $b$ into an inner child (outer box $b$ ) and an outer child (outer box unchanged, inner box $b$ ). Throughout, every box has aspect ratio at most $3$ , a parent's inner box lies entirely within one child (within the inner child of a shrink), and inner boxes are sticky. The cells at the leaves are the leaf cells; they cover the root box and have disjoint interiors.

The distance from $q$ to a cell $c$ is $\operatorname{dist}_m(q,c)=\inf_{x\in c}\operatorname{dist}_m(q,x)$ . Each leaf cell $c_j$ carries an associated data point $p_j$ in its outer box. The search enumerates the leaf cells $c_0,c_1,\dots$ in nondecreasing order of distance from $q$ , processes each by comparing its point with the closest point $p$ seen so far, and terminates at the first cell whose distance from $q$ exceeds $\operatorname{dist}_m(q,p)/(1+\varepsilon)$ . The goal bounds $N$ , the number of cells that did not cause termination, which is the count the paper's proof bounds ("the number of cells visited up until termination", p. 912).

Formalization targets

Goal: Lemma 5 (p. 911)

For every valid BBD-tree, every Minkowski metric $1\le m\le\infty$ , every $\varepsilon>0$ , every query point and every sorted enumeration of the leaf cells,

N\le\Big\lceil 1+\frac{6d}{\varepsilon}\Big\rceil^d.

Milestones

The packing constraint (Lemma 4, p. 908): for $r,s>0$ , the number of leaf cells of size at least $s$ meeting an open $L_m$ ball of radius $r$ is at most

\Big\lceil 1+\frac{6r}{s}\Big\rceil^d.

Its proof has three stated steps, each a milestone: an $L_m$ ball of radius $r$ lies in an axis-parallel cube of side $2r$ ; at most $\lceil1+6r/s\rceil^d$ interior-disjoint boxes of side at least $s/3$ meet such a ball; and the leaf cells of size at least $s$ meeting the ball can be replaced by as many interior-disjoint boxes of size at least $s$ meeting it. The proof of Lemma 5 contributes two more: the $L_m$ diameter of a rectangle is at most $d$ (indeed $d^{1/m}$ ) times its longest side, and every visited cell has size at least $r\varepsilon/d$ , where $r$ is the distance to the last cell that did not cause termination.

A companion statement records the correctness of the termination rule: the closest point processed is a $(1+\varepsilon)$ -approximate nearest neighbor.

Significance

Lemma 5 is the explicit content of the query bound of Theorem 1(i): each visited cell costs $O(d\log n)$ time to enumerate and process, so the query takes $O(d\lceil1+6d/\varepsilon\rceil^d\log n)$ time, with no dependence on $n$ beyond the logarithm. Lemma 4 is the property of the subdivision on which this rests, and it is used again for the $k$ -nearest-neighbor variant (Lemma 6) and for approximate range searching with the same tree.

The results are proved on paper and widely cited; none has a machine-checked proof. The mission produces checked versions of the packing constraint and of the cell-count bound for an abstract BBD-tree, defined by its invariants rather than by a particular construction algorithm, so that any construction meeting the invariants inherits the bound. It also exposes two places where the printed argument needs care: the open versus closed ball in Lemma 4, and the step in Lemma 5 that applies Lemma 4 to cells within distance $r$ of $q$ , which touch the closed ball of radius $r$ .

Difficulty

The counting step of Lemma 4 is asserted on the page ("the densest packing of axis-aligned rectangles of side length at least $s/3$ is realized by a regular grid"), and a formal argument must replace that sentence with a genuine counting argument. The replacement step is the geometric core: the outer box of a leaf cell with an inner box overlaps every leaf cell inside that inner box, so outer boxes cannot be counted directly, and without stickiness many nested inner boxes could crowd against one face of a cell. Applying Lemma 4 inside Lemma 5 is not immediate either: the visited cells lie within distance $r$ of $q$ , so they meet the closed ball, while Lemma 4 concerns the open ball, and a naive enlargement of the radius changes the ceiling exactly when $6d/\varepsilon$ is an integer.

Formalization scope

Points are Fin d → ℝ, the metric index $m$ is an element of ℕ∞ with $1\le m$ , and the $L_m$ distance is defined explicitly by the formula above. Rectangles are pairs of corner vectors; boxes have positive sides and aspect ratio at most $3$ . A cell's point set is the closure of the outer box minus the inner box, as the paper's "cells are considered to be closed" requires; an inner box equal to its outer box is excluded. A BBD-tree is an inductive tree of splits and shrinks with a validity predicate expressing the §2.1 invariants relative to the root cell; the root may be any box rather than the paper's hypercube, and the construction algorithms of §2.2–§2.5 are not formalized.

The enumeration is a list of (leaf cell, associated point) pairs that is a permutation of the leaf cells, sorted by distance from $q$ , with each point in its cell's outer box. A cell is processed before its own termination test, and $N$ counts the cells processed before the cell whose test fires (all cells if none fires). Lemma 4 and its counting step use the open ball of property (d). Theorem 1's $O(\cdot)$ time and space claims, Lemmas 1–3 on the construction, and the $k$ -nearest-neighbor Lemma 6 are out of scope.

This convention follows the proof of Lemma 5, which takes $r$ to be the distance to "the last leaf cell that did not cause the algorithm to terminate" and bounds the cells up to that one. If the cell whose test fires is also counted, the printed bound can be exceeded by one: a valid one-dimensional tree with $\varepsilon=6$ needs three processed cells against $\lceil 1+6d/\varepsilon\rceil^d=2$ . The formal goal therefore states the bound for the cells that did not cause termination, which is what the proof establishes; consequently at most $\lceil 1+6d/\varepsilon\rceil^d+1$ cells are processed in total.

The goal must not be trivialized: the enumeration must contain every leaf cell (an empty enumeration would give $N=0$ ), it must be sorted, cells must be closed sets rather than outer boxes minus open inner boxes (which leaves isolated boundary points and makes the goal false), and no size bound or packing fact may be assumed in the goal.

Contributions welcome: proofs of the milestones in any order, general lemmas on $L_m$ distances and interior-disjoint boxes (reusable beyond this mission), and a construction of valid BBD-trees from the paper's midpoint or middle-interval rules.

Selected references

S. Arya, D. M. Mount, N. S. Netanyahu, R. Silverman, A. Y. Wu, An optimal algorithm for approximate nearest neighbor searching in fixed dimensions, J. ACM 45(6):891–923, 1998. https://doi.org/10.1145/293347.293348
S. Arya, D. M. Mount, Approximate nearest neighbor queries in fixed dimensions, Proc. 4th ACM-SIAM SODA, 271–280, 1993 (reference [Arya and Mount 1993b] of the main paper, https://doi.org/10.1145/293347.293348).
S. Arya, D. M. Mount, N. S. Netanyahu, R. Silverman, A. Y. Wu, An optimal algorithm for approximate nearest neighbor searching in fixed dimensions, Proc. 5th ACM-SIAM SODA, 573–582, 1994 (reference [Arya et al. 1994] of the main paper).
D. M. Mount, S. Arya, ANN: A library for approximate nearest neighbor searching. https://www.cs.umd.edu/~mount/ANN/
S. Har-Peled, P. Indyk, R. Motwani, Approximate nearest neighbor: towards removing the curse of dimensionality, Theory of Computing 8:321–350, 2012. https://doi.org/10.4086/toc.2012.v008a014

8 thms1 active userReviewed

Computational Geometry

Missions

Linear Programming in Linear Time When the Dimension Is Fixed: Fixed-Dimension LP Feasibility Decided in Linear Time on the Real RAMResearch Paper

Motivation

Setting

Formalization targets

Goal: linear-time feasibility on the real RAM

Milestones

Significance

Difficulty

Formalization scope

Selected references

Rounding of Polytopes in the Real Number Model of Computation: Barycentric Coordinate Descent Finds a (1+ε)n-Rounding Ellipsoid of m Points in O(n(1/ε + ln n + ln ln m)) IterationsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 317)

The centrally symmetric case: Theorem 1 (p. 314)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Uniform Obstacle Bounds for Planar Graphs (OPG-37357)Open Problem

Motivation

Setting

Formalization targets

The two-part OPG record

Published first part

Universal bound

Significance

Difficulty

Formalization scope

Selected references

Concentration of Measure and Isoperimetric Inequalities in Product Spaces XII: The Euclidean Traveling Salesman Problem — P(|L_N − M| ≥ t) ≤ K e^{−t²/K} for N Uniform Points in the SquareTextbook

Motivation

Setting

Formalization targets

Gaussian concentration for regular geometric functionals

Significance

Difficulty

Formalization scope

Selected references

A Combinatorial Theorem in Plane Geometry: Every n-Triangulation Can Be Partitioned into at Most ⌊n/3⌋ FansResearch Paper

Motivation

Setting

Formalization targets

Goal: Chvátal's theorem (p. 39)

Milestones (the claims of the proof, pp. 40–41, in attack order)

Significance

Difficulty

Formalization scope

Selected references

A Polynomial Time Algorithm for Counting Integral Points in Polyhedra When the Dimension is Fixed: The Lattice-Point Count of an Integral Simplex Is a Short Signed Sum over Primitive ConesResearch Paper

Counting lattice points in fixed dimension

Setting

Formalization targets

Goal: the short signed formula (Theorem 1.2, mathematical content)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Generalization of Hinging PlanesResearch Paper

Persistence-Based Clustering in Riemannian Manifolds: With High Probability the Algorithm Returns as Many Clusters as the Density Has d₂-Prominent PeaksResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.8 (p. 22)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Economic Lot Sizing: An O(n log n) Algorithm That Runs in Linear Time in the Wagner-Whitin Case 1: The Threshold Rule on Efficient Periods Picks an Optimal Next Production PeriodResearch Paper

Motivation

Setting

Formalization targets

Efficient candidates

Threshold rule and backward value