Computational Geometry

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

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)

1. Base case. Every $n$-triangulation with $3 \le n \le 5$ is a fan.
2. 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$.
3. 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$.
4. 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$.
5. 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

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

1. Proposition 2.4 with Remark 2.5: the closed form of $\sigma$ for simple cones.
2. Proposition 4.1: for primitive cones, $\sigma(K;c)=\prod_i(1-e^{\langle c,u_i\rangle})^{-1}$.
3. Proposition 2.7 (Brion), for integral simplices.
4. Corollary 4.2: $R(K,v,c)=Q_k(x;y)\prod_ix_i^{-1}$ with $\deg Q_k\le k$.
5. Primitive generators iff $\operatorname{Ind}K=1$ (§5).
6. Lemma 5.2: a short lattice vector $w$ with $\operatorname{Ind}K_j\le(\operatorname{Ind}K)^{(d-1)/d}$.
7. Lemma 5.3: at most $2^d$ cones of smaller index, with signs $\pm1$.
8. Theorem 5.4: decomposition into at most $(2^d)^T$ primitive cones.
9. The display in the proof of Theorem 5.4: $(2^d)^T\le C_1(d)(\log\operatorname{Ind}K)^{C_2(d)}$.
10. 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

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.

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

1. 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)}$.
2. 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$.
3. 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}$.
4. Signal image (pp. 22–23): the signal points are sent outside that region.
5. 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.
6. 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