Motivation

Packing congruent circles into a square is a classical problem in discrete geometry: for each natural number $n$, choose a common radius as large as possible while keeping all disks inside the square and preventing overlap. Every exact value requires two logically distinct achievements: an explicit configuration attaining the proposed radius and a proof that no configuration can do better.

The character of those proofs changes sharply with $n$. The first cases admit short geometric arguments; later cases use contact-graph analysis, specialized case divisions, or computer-assisted global optimization with interval arithmetic. Formalizing the resulting constants therefore provides a growing benchmark for extremal geometry, real algebra, finite configurations, and verified computation in Lean.

This is an open-ended formalization mission. It begins with the exact constants currently represented by theorem-backed milestones, but it is not restricted to a fixed terminal value of $n$. Further milestones may be added whenever an exact packing value and its rigorous optimality argument are identified and stated precisely enough for formalization.

Setting

A point is a pair of real coordinates. For points $p=(x,y)$ and $q=(x',y')$, squared Euclidean distance is

$$\operatorname{sqDist}(p,q)=(x-x')^2+(y-y')^2.$$

For a real radius $r$, a point lies in the inner square when both coordinates belong to the closed interval $[r,1-r]$. This is exactly the coordinate condition saying that a closed disk of radius $r$, centered at that point, is contained in the unit square.

The predicate $\operatorname{Packable}(n,r)$ requires $0\le r\le \tfrac12$ and a family of $n$ centers in the inner square such that the squared distance between every two distinctly indexed centers is at least $(2r)^2$. Equality is allowed, so tangent disks are admitted. Radius zero is also admitted.

Define

$$r_n=\sup\{r\in\mathbb R:\operatorname{Packable}(n,r)\}$$

and define the optimal covered-area fraction by

$$c_n=n\pi r_n^2.$$

It is often convenient to use the equivalent point-separation constant $d_n$, the greatest possible minimum pairwise distance among $n$ points in the unit square. The conversion is

$$r_n=\frac{d_n}{2(1+d_n)}, \qquad c_n=n\pi\left(\frac{d_n}{2(1+d_n)}\right)^2.$$

The Lean definitions use a supremum rather than assuming in advance that an optimal packing is attained.

Current exact-value milestones

The mission currently contains theorem-backed milestones for the following values:

$n$	Exact separation or area value	Proof character in the supplied notes
$2$	$d_2=\sqrt2$, hence $c_2=\pi(3-2\sqrt2)$	diagonal bound
$3$	$d_3=\sqrt6-\sqrt2$	minimum enclosing square of a triangle
$4$	$d_4=1$, hence $c_4=\pi/4$	convex hull and perimeter
$5$	$d_5=1/\sqrt2$	four-cell pigeonhole argument
$6$	$d_6=\sqrt{13}/6$	case-specific geometric proof
$7$	$d_7=4-2\sqrt3$	hand proof and later computer verification
$8$	$d_8=\sqrt{2-\sqrt3}$	case-specific geometric proof
$9$	$d_9=1/2$, hence $c_9=\pi/4$	classical geometric proof
$16$	$d_{16}=1/3$, hence $c_{16}=\pi/4$	theoretical grid-optimality proof
$25$	$d_{25}=1/4$, hence $c_{25}=\pi/4$	theoretical grid-optimality proof
$36$	$d_{36}=1/5$, hence $c_{36}=\pi/4$	theoretical grid-optimality proof

For rows stated using $d_n$, the corresponding milestone for $c_n$ uses the conversion formula above. The equalities are claims about the supremum-defined packing constants, not merely about the displayed candidate configurations.

An extensible mission

The milestone list is intended to grow. The supplied survey notes classify $n=2,\ldots,33$ and $n=36$ as rigorously solved in the cited literature, while distinguishing $n=34$ and $n=35$ as not rigorously closed in the cited 2021 account. Many of the computer-assisted cases do not have a simple radical expression in the supplied notes. Before such a case is linked to a Lean theorem, its primary source must provide a precise candidate value, algebraic characterization, certified enclosure, or optimal-configuration certificate that can be stated faithfully.

A new milestone should identify:

1. the precise value or exact characterization being formalized;
2. an attaining configuration or a certified existence argument;
3. a universal upper bound or global-optimality certificate;
4. the primary source and exact theorem, equation, or certificate location;
5. any trusted computational artifact and the arithmetic guarantees it requires.

Numerical evidence and strong bounds are valuable, but they must be labeled as bounds rather than exact-value milestones. Conversely, newly published exact results for larger $n$ may be added without changing the underlying definitions.

Proof obligations

Every exact-value milestone must connect the proposed value to Packable, r_n, and c_n. Constructing a configuration establishes only a lower bound. An upper-bound argument without attainability also does not establish equality. A complete proof must bridge both directions through the supremum definition.

The proof methods may include:

• elementary diameter, pigeonhole, convexity, or enclosing-shape arguments;
• normalization between disk centers and point-separation configurations;
• contact-graph and boundary-constraint analysis;
• finite case decompositions;
• interval arithmetic and formally checked branch-and-bound certificates;
• exact algebraic identities needed to convert $d_n$ into $r_n$ and $c_n$.

Shortcuts that redefine $r_n$, $d_n$, or $c_n$ to equal a desired answer are excluded. The constants must remain consequences of the common geometric model.

Mission structure

The root theorem CirclePackingConstants.c_all is the conjunction of the eleven exact-value milestones currently in the mission, covering $n=2,3,4,5,6,7,8,9,16,25,36$. Its proof sketch reduces the root directly to those milestone theorems, so the mission remains open until every current exact value is proved.

The milestone theorems remain separately reusable and independently auditable. When further exact values are added, a successor aggregate theorem can extend the conjunction and become the new root without replacing the shared definitions or invalidating earlier results.

This structure allows elementary cases, historical hand proofs, and computer-assisted certificates to progress independently while remaining part of one cumulative library of exact circle-packing constants.

Formalization scope

The Lean model uses ℝ × ℝ for points and an explicit coordinate formula for squared Euclidean distance. Disk containment is represented by inclusive coordinate inequalities. Nonoverlap is represented by a weak squared-distance inequality, so tangency is permitted. The indexing type is Fin n, and the definitions apply to every natural number, including zero.

The definition bundle contains only Point, sqDist, InInnerSquare, Packable, r_n, and c_n. Solvers may introduce normalization maps, separation bounds, explicit configurations, supremum lemmas, contact structures, certificate checkers, and radical or polynomial identities as auxiliary declarations.

Selected references

• User-supplied notes, Circles in squares: constants, proofs, and what is actually known, supplied September 12, 2026. The notes summarize the exact small-$n$ formulas, grid cases, historical proof taxonomy, and computer-assisted frontier used to organize this mission.
• J. Schaer and A. Meir, “On a geometric extremum problem,” Canadian Mathematical Bulletin 8 (1965), 21–27.
• J. Schaer, “The densest packing of nine circles in a square,” Canadian Mathematical Bulletin 8 (1965), 273–277.
• B. L. Schwartz, “Separating points in a square,” Journal of Recreational Mathematics 3 (1970), 195–204.
• J. B. M. Melissen, “Densest packing of six equal circles in a square,” Elemente der Mathematik 49 (1994), 27–31.
• M. C. Markot, “Improved interval methods for solving circle packing problems in the unit square,” Journal of Global Optimization 81 (2021), 773–803.
• Erich Friedman, Circles in Squares, Erich's Packing Center, for background tables and diagrams of candidate packings.

Motivation

The Hirsch conjecture, stated by Warren M. Hirsch in a 1957 letter to George Dantzig, asserts that the combinatorial diameter of a $d$-dimensional polytope with $n$ facets is at most $n-d$. The diameter is the largest number of edge steps needed to walk between two vertices of the polytope. The question matters to linear optimization: every edge-following pivot rule of the simplex method, starting at a vertex of the feasible region, needs at least as many pivots as the graph distance to an optimal vertex. A polynomial bound on polytope diameters is a necessary condition for a strongly polynomial simplex method, which is still unknown.

Timeline of the conjecture before the counterexample:

• 1967, Klee and Walkup: the conjecture fails for unbounded polyhedra, and for bounded polytopes it is equivalent to the $d$-step conjecture (the case $n=2d$). They also proved it for $n-d\le 5$.
• 1992, Kalai and Kleitman: a quasi-polynomial upper bound $n^{\log_2 d+2}$ on the diameter.
• 2010, Santos: a counterexample in dimension 43 with 86 facets (arXiv:1006.2814, published in Ann. of Math. 176 (2012) 383–412). It is the subject of this mission.
• 2012, Matschke, Santos and Weibel: smaller 5-dimensional spindles, giving counterexamples in dimension 20 (arXiv:1202.4701).

The polynomial Hirsch conjecture, which asks only for a bound polynomial in $n$ and $d$, remains open.

Setting

A polytope in $\mathbb R^d$ is written as $\mathrm{Hpoly}(a,b)=\{x:\langle a_i,x\rangle\le b_i,\ i=1,\dots,n\}$. A facet presentation is one in which $\mathrm{Hpoly}(a,b)$ has nonempty interior and no inequality is redundant. For a bounded polytope it then has dimension $d$, and its $n$ inequalities correspond one to one to its facets. A step between two vertices crosses an edge (a one-dimensional face). The polytope is non-Hirsch when its diameter exceeds $n-d$.

A spindle (Santos, Definition 1.4) is a polytope with two distinguished vertices $u,v$ such that every facet contains exactly one of them. Its length is the graph distance from $u$ to $v$. The polar objects are prismatoids: polytopes with two parallel facets $Q^+,Q^-$ containing all vertices, whose width is the dual-graph distance between $Q^+$ and $Q^-$.

Santos's explicit object is the 5-prismatoid $Q$ whose vertices are the 48 rows of Table 1 of the paper: $1^+,\dots,24^+$ with $x_5=1$ and $1^-,\dots,24^-$ with $x_5=-1$. Its polar $Q^\Delta=\{x\in\mathbb R^5:\langle r,x\rangle\le1\ \text{for each row } r\}$ is a spindle with apices $e_5$ and $-e_5$. Table 2 of the paper lists the 322 facets of $Q$, which are the 322 vertices of $Q^\Delta$: $\pm e_5$ and the points $\frac1{c_0}(\pm c_1,\pm c_2,\pm c_3,\pm c_4,c_5)$ of twenty types $B,B',\dots,K,K'$ with sixteen sign patterns each. The symmetry group $\Sigma$ of $Q$ has order 64; its index-two subgroup $\Sigma^+$ preserves $Q^+$ and $Q^-$.

Formalization targets

Goal: Corollary 1.7

$$\exists\, a:\mathrm{Fin}\,86\to\mathbb R^{43},\ b\in\mathbb R^{86}:\quad \mathrm{Hpoly}(a,b)\ \text{nonempty, bounded, a facet presentation, and}\ \operatorname{diam}\mathrm{Hpoly}(a,b)>43.$$

The goal fixes the dimension (43) and the number of facets (86), as the paper does. It does not assert the exact diameter (44, remarked on p. 24).

Milestones

1. §3, first bullet (polar form): $Q^\Delta$ is a bounded 48-facet spindle with apices $\pm e_5$, the rows tight at $e_5$ being $1^+,\dots,24^+$.
2. Theorem 4.1(1) (polar form): the 322 points of Table 2 are distinct vertices of $Q^\Delta$; the letter classes are $\Sigma^+$-orbits and the six $\Sigma$-orbits are A ∪ L, B ∪ K, C ∪ J, D ∪ I, E ∪ H, F ∪ G.
3. Theorem 4.1(2) (polar form): $Q^\Delta$ has no other vertices.
4. Theorem 3.1 (polar form): the distance from $e_5$ to $-e_5$ in the graph of $Q^\Delta$ is exactly 6.
5. Theorem 1.6: a 5-spindle with 48 facets, 322 vertices and length exactly six exists.
6. Inductive step of Theorem 2.6 (polar form): a $d$-spindle with $n>2d$ facets and length at least $l$ yields a $(d+1)$-spindle with $n+1$ facets and length at least $l+1$.
7. Theorem 1.5 (strong $d$-step theorem): a $d$-spindle with $n$ facets and length at least $l$ yields an $(n-d)$-spindle with $2n-2d$ facets and length at least $l+n-2d$, non-Hirsch when $l>d$.

Significance

Corollary 1.7 settles the Hirsch conjecture in the negative. Theorem 1.5 is the reusable part: it turns any spindle whose length exceeds its dimension into a counterexample. That made the later search for small spindles (Matschke–Santos–Weibel) a finite, low-dimensional problem. Theorem 1.6 is the concrete certificate. Its claims about Tables 1 and 2 are finite statements about explicit rational data.

The result is proved, and several pieces are already formalized on Prove2Me. Hirsch.santos_counterexample (Proved) states that some polytope violates the bound $n-d$, with no dimension or facet count. Hirsch.strong_dstep_spindle (Proved) is the "in particular" clause of Theorem 1.5, counting inequalities rather than facets. Lemmas 2.2 and 2.4 of the paper are Proved in polar form (Hirsch.spindle_inward_row_push_graph, Hirsch.spindle_wedge_vertex_graph_projection), as is the bound $n\ge2d$ for spindles (Hirsch.spindle_n_ge_two_d). This mission adds the dimension-43, 86-facet statement with facets counted exactly, the general length bound $l+n-2d$ with the spindle structure preserved, and a machine-checkable account of Santos's specific spindle.

Difficulty

The obvious first idea for the 5-dimensional milestones is brute computation. This is feasible in principle but heavy in Lean. Showing that 322 given points are extreme requires exhibiting, for each, five linearly independent tight rows among 48. Showing that no other vertex exists requires a complete enumeration argument rather than a membership check. Exact distance 6 requires the full adjacency structure between the 322 vertices, not only a path.

For the general theorems, the difficulty is that the construction is a one-point suspension followed by a perturbation. Edges and facets of the new polytope must be controlled, with the face lattice changing only in a prescribed way. Diameter is not monotone under arbitrary perturbations, and in particular a walk can become shorter. Keeping the facet count exact (not merely the inequality count) adds an irredundancy argument at each step.

Formalization scope

Polytopes are H-presentations Hirsch.Hpoly a b with a : Fin n → EuclideanSpace ℝ (Fin d), from the platform definition Hirsch_model. "A $d$-polytope with $n$ facets" is boundedness plus IsFacetPresentation: nonempty interior and every row irredundant. Without this predicate, padding with redundant rows would change the bound $n-d$, and the statement would collapse to the platform's dimension-free Hirsch.santos_counterexample. Diameter and length use the platform's padded walks (Hirsch.DiamLE, Hirsch.Reach). "Length at least $L$" means no walk of fewer than $L$ steps, and "length exactly $L$" adds a walk of $L$ steps. The junk-valued Hirsch.gdist is never used.

All prismatoid statements of the paper (§3, Theorems 2.6, 3.1, 4.1) are stated for the polar spindle, which the paper licenses (pp. 6, 8, 9). Vertices of $Q$ become rows, facets of $Q$ become vertices, the width becomes the apex distance, and $Q^\pm$ become $\pm e_5$. Natural-number expressions $n-d$, $2n-2d$, $l+(n-2d)$ are faithful because spindles have $n\ge2d$. Theorem 1.5's "length $l$" is read as "length at least $l$", which is equivalent by monotonicity. Tables 1 and 2 are written entry by entry in Lean in the page's order.

Useful contributions include proofs of the finite Table 1/Table 2 facts by certified computation, reusable lemmas on one-point suspensions and on facet presentations under perturbation, and a proof of Corollary 1.7 from milestones 5 and 7.

Selected references

• F. Santos, A counterexample to the Hirsch conjecture, Ann. of Math. 176 (2012) 383–412; cited version arXiv:1006.2814v3. https://arxiv.org/abs/1006.2814 , https://doi.org/10.4007/annals.2012.176.1.7
• V. Klee and D. W. Walkup, The d-step conjecture for polyhedra of dimension d < 6, Acta Math. 117 (1967) 53–78. https://doi.org/10.1007/BF02395040
• G. Kalai and D. J. Kleitman, A quasi-polynomial bound for the diameter of graphs of polyhedra, Bull. Amer. Math. Soc. 26 (1992) 315–316. https://arxiv.org/abs/math/9204233
• B. Matschke, F. Santos and C. Weibel, The width of five-dimensional prismatoids, Proc. London Math. Soc. 110 (2015) 647–672. https://arxiv.org/abs/1202.4701

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

Motivation

The simplex method for linear programming moves from vertex to vertex along the edges of a polyhedron. A lower bound on the number of pivots of any edge-following method is the graph diameter of the feasible polyhedron: the largest number of edges needed to connect two of its vertices. Whether this diameter is bounded by a polynomial in the dimension $d$ and the number $n$ of facets is the polynomial Hirsch conjecture, open since the 1950s. The original Hirsch conjecture, $n-d$, was refuted for unbounded polyhedra by Klee and Walkup (1967) and for bounded ones by Santos (2012) (doi:10.4007/annals.2012.176.1.7).

Timeline.

• 1964–1966. Klee proves that a three-dimensional polyhedron with $n$ facets, bounded or not, has diameter at most $n-3$ (doi:10.4153/CJM-1964-058-3, doi:10.1137/0113061, doi:10.2140/pjm.1966.17.249).
• 1967. Klee and Walkup show that the Hirsch bound fails for unbounded polyhedra in dimension four (doi:10.1007/BF02395039).
• 1992. Kalai and Kleitman prove the first subexponential bound, $n^{\log_2 d+2}$, for all polyhedra (doi:10.1090/S0273-0979-1992-00285-9, arXiv:math/9204233).
• 2010. Eisenbrand, Hähnle, Razborov and Rothvoss show that $n^{\log_2 d+1}$ holds for a broad combinatorial abstraction of polyhedra (doi:10.1287/moor.1100.0470).
• 2014. Todd sharpens the Kalai–Kleitman bound to $(n-d)^{\log_2 d}$ for all polyhedra, bounded or not (arXiv:1402.3579; SIAM J. Discrete Math. 28 (2014), doi:10.1137/140962310). This is the result of this mission.

Setting

A polyhedron $P\subseteq\mathbb R^d$ is the set of solutions of finitely many linear inequalities,

$$P=\operatorname{Hpoly}(a,b)=\{x\in\mathbb R^d:\ \langle a_i,x\rangle\le b_i,\ i=1,\dots,n\}.$$

It need not be bounded. A vertex of $P$ is a point $v$ for which some half-space $H$ satisfies $P\cap H=\{v\}$, equivalently an extreme point of $P$. Two vertices $v\neq w$ are adjacent when $P\cap H=[v,w]$ for some half-space $H$; the segment $[v,w]$ is then an edge. A path of length $k$ is a sequence of vertices $v=v_0,\dots,v_k=w$ with consecutive vertices adjacent, $\rho_P(v,w)$ is the least such $k$, and the diameter is $\delta(P)=\max\rho_P(v,w)$ over pairs of vertices. A $(d,n)$-polyhedron is a $d$-dimensional polyhedron with $n$ facets, and

$$\Delta(d,n)=\max\{\delta(P):\ P \text{ a } (d,n)\text{-polyhedron}\},$$

the maximum taken over bounded and unbounded polyhedra alike. All logarithms are to base 2.

Formalization targets

Goal: Theorem 1

$$\Delta(d,n)\le (n-d)^{\log d}\quad(1\le d\le n),\qquad \Delta(1,1)=0.$$

The goal fixes no constant beyond the paper's own exponent and leaves no case of $d$, $n$ or boundedness open.

Milestones, in the order the proof uses them

1. The identity $(n-d)^{\log d}=d^{\log(n-d)}$ (p. 2).
2. Two vertices on a common facet are at distance at most $\Delta(d-1,n-1)$ (p. 2, in the proof of Lemma 1).
3. Lemma 1 (Kalai–Kleitman): for $2\le d\le\lfloor n/2\rfloor$, $\Delta(d,n)\le\Delta(d-1,n-1)+2\Delta(d,\lfloor n/2\rfloor)+2$.
4. $\Delta(d,d)=0$.
5. $\Delta(1,n)\le 1$.
6. $\Delta(2,n)\le n-2$.
7. $\Delta(3,n)\le n-3$ (Klee), for unbounded polyhedra too.
8. If $n<2d$, then $\Delta(d,n)\le\Delta(d-1,n-1)$.
9. In the ten cases $d=4,\ 8\le n\le 11$; $d=5,\ 10\le n\le 12$; $d=6,\ 12\le n\le 13$; $d=7,\ n=14$, the bound $\lfloor (n-d)^{\log d}\rfloor$ satisfies the recursion of Lemma 1.
10. For $d\ge4$, $n-d\ge8$, $n\ge 2d$: $(d-1)^{\log(n-d)}+2(n/2-d)^{\log d}+2\le d^{\log(n-d)}$. For $n>2d$ this is the displayed inequality; at $n=2d$ the second power is zero, consistent with $\Delta(d,d)=0$.

Significance

The result. The bound $(n-d)^{\log d}$ is never larger than the Kalai–Kleitman bound. It equals the true value $n-d$ in dimensions 1 and 2, and it depends on $n$ only through the Hirsch quantity $n-d$. Since $(n-d)^{\log d}=d^{\log(n-d)}$, it is also symmetric under linear-programming duality, which exchanges the roles of $d$ and $n-d$. For fixed $n-d$ it is polynomial in $d$. It applies to the unbounded feasible regions that arise in practice in linear programming.

Formalizing it. The theorem has been proved since 2014. The platform has a proof of the bounded case only: Hirsch.todd_bound assumes $d\ge3$, a nonempty interior and Bornology.IsBounded. This mission's goal extends it to all polyhedra, bounded or not, and to $d=1,2$. That is the statement the paper proves, and the one an analysis of the simplex method on unbounded feasible regions needs. The unbounded form of Lemma 1 and the common-facet bound are open on the platform as items of the Kalai–Kleitman series and are reused here. Klee's unbounded three-dimensional bound has no formal proof on the platform: the published Hirsch.klee_three_dimensional_bound and Hirsch.dimension_three_bound cover bounded polyhedra only. The bounded recursion Hirsch.kalai_kleitman_recursion and the bounded facet reduction Hirsch.facet_reduction are proved and may serve as models.

Difficulty

Two steps are hard. The first is the unbounded case. Statements proved for polytopes do not transfer directly, because an unbounded polyhedron may have no vertices or a single one, unbounded edges (rays) that are not edges of the graph, and redundant or implicit-equality rows. Each geometric milestone must hold for these. The second is Klee's three-dimensional bound, which the paper cites without proof. Assuming boundedness to apply the published polytope versions is ruled out: Klee and Walkup showed that unbounded and bounded diameters differ from dimension four on, so the unbounded case carries content of its own. The arithmetic milestones are elementary but sensitive to edge values of $\log$ and the real power.

Formalization scope

All statements use the published definitions Hirsch.Hpoly, Hirsch.Adj and Hirsch.DiamLE (Hirsch_model). Vertices are Set.extremePoints ℝ. DiamLE P B says that any two extreme points are joined by a walk of exactly $B$ steps, each step staying put or crossing an edge. So the bound includes connectivity of the vertex–edge graph.

• Inequality reading. "$\Delta(d,n)\le B$" is stated as: for every $a:\mathrm{Fin}\,n\to\mathbb R^d$ and $b$, DiamLE (Hpoly a b) B. This ranges over all polyhedra given by $n$ inequalities in $\mathbb R^d$, including lower-dimensional, empty and redundant ones. It is equivalent to the paper's statement: a lower-dimensional polyhedron of dimension $d'$ with $n'$ facets has $n'-d'\le n-d$.
• No boundedness, nonemptiness or full-dimensionality is assumed anywhere.
• The logarithm is Real.logb 2 and the power is Real.rpow. A distance is at most $(n-d)^{\log d}$ exactly when it is at most the floor $\lfloor (n-d)^{\log d}\rfloor$, abbreviated toddBound d n in the milestone on the ten cases. The clause $\Delta(1,1)=0$ is a separate conjunct, because $0^0=1$ in Real.rpow.
• Disclosed additions: nonzero rows in the $n<2d$ step (as in the referenced Lemma 1 and the $d=2$ bound). In the general step, $n\ge2d$: the paper secures it by treating $n<2d$ first. The second power is written with base $n/2-d$; it equals the printed expression when $n>2d$ and takes the intended value zero when $n=2d$, where the printed logarithm is undefined.
• Natural-number subtraction appears in $n-3$ and $n-2$ (both harmless, since for small $n$ there are no vertices) and in $\mathbb R^{d-1}$ for facets.

Trivializing encodings are excluded: no Bornology.IsBounded hypothesis; no definition of $\Delta$ by sSup over $\mathbb N$, which would be $0$ on unbounded families; no use of Hirsch.gdist, which is $0$ when no walk exists; and no dropping of the $\Delta(1,1)=0$ clause.

Contributions are welcome on every milestone. A complete development needs facial structure of unbounded polyhedra (facets as polyhedra one dimension lower, tight rows at vertices), the relaxation argument of Lemma 1, Klee's three-dimensional argument, and real-power and logarithm estimates. The facet machinery and Klee's bound are reusable for any diameter result on unbounded polyhedra.

Selected references

• M. J. Todd, An improved Kalai–Kleitman bound for the diameter of a polyhedron, SIAM J. Discrete Math. 28 (2014); arXiv:1402.3579v2. arXiv:1402.3579, doi:10.1137/140962310
• G. Kalai and D. J. Kleitman, A quasi-polynomial bound for the diameter of graphs of polyhedra, Bull. Amer. Math. Soc. 26 (1992), 315–316. doi:10.1090/S0273-0979-1992-00285-9
• V. Klee, Diameters of polyhedral graphs, Canad. J. Math. 16 (1964), 602–614. doi:10.4153/CJM-1964-058-3
• V. Klee, Paths on polyhedra I, J. SIAM 13 (1965), 946–956. doi:10.1137/0113061
• V. Klee, Paths on polyhedra II, Pacific J. Math. 17 (1966), 249–262. doi:10.2140/pjm.1966.17.249
• V. Klee and D. W. Walkup, The d-step conjecture for polyhedra of dimension d < 6, Acta Math. 117 (1967), 53–78. doi:10.1007/BF02395039
• F. Eisenbrand, N. Hähnle, A. Razborov, T. Rothvoss, Diameter of polyhedra: limits of abstraction, Math. Oper. Res. 35 (2010), 786–794. doi:10.1287/moor.1100.0470
• F. Santos, A counterexample to the Hirsch conjecture, Ann. of Math. 176 (2012), 383–412. doi:10.4007/annals.2012.176.1.7

Motivation

Loop quantum gravity (LQG) is a proposal for a quantum theory of the gravitational field in which space itself is built from discrete quanta. Its kinematics rests on two mathematical facts that C. Rovelli's review Loop quantum gravity: the first 25 years (Class. Quantum Grav. 28 (2011) 153002, arXiv:1012.4707) singles out. First, the spin–geometry theorem of Penrose, in the extended form based on a theorem of Minkowski (1897): the angular-momentum vectors attached to the links around a node of a spin network, once they satisfy the closure (gauge-invariance) relation, are exactly the data of a flat polyhedron, so every quantum of space carries a geometry (§2.1). Second, the discreteness of geometric spectra: areas take values $8\pi\gamma\hbar G\sum_n\sqrt{j_n(j_n+1)}$ with half-integer spins $j_n$, with a strictly positive area gap (§2.1, §2.3, §4.3), which the review calls "the most solid result in loop gravity".

Timeline. Minkowski proved the existence and uniqueness of a convex polyhedron with prescribed face normals and areas in 1897. Penrose introduced spin networks and the spin–geometry theorem around 1971. The discreteness of area and volume in LQG was found by Rovelli and Smolin (1995), with the full area spectrum computed by Ashtekar–Lewandowski and others in 1995–1997.

Setting

Work in Euclidean three-space $\mathbb E^3=\mathbb R^3$ with its standard inner product $\langle\cdot,\cdot\rangle$. Given finitely many vectors $u_1,\dots,u_v\in\mathbb E^3$ and real numbers $h_1,\dots,h_v$, the half-space polyhedron is

$$P(u,h)=\{x\in\mathbb E^3:\ \langle u_l,x\rangle\le h_l\ \text{for all } l\},$$

and its $l$-th face is $F_l=P(u,h)\cap\{x:\langle u_l,x\rangle=h_l\}$. The area of a set lying in a plane orthogonal to a nonzero vector $u$ is its two-dimensional Lebesgue measure, computed as the measure of its orthogonal projection onto the plane $u^\perp$. For a nonzero vector $n$, $\hat n=n/\|n\|$ is its direction.

On the quantum side, a node of a spin network with $v$ links carries vectors $\vec L_1,\dots,\vec L_v$ (the left-invariant derivative operators), subject to the closure relation $\sum_l \vec L_l=0$ (eq. (6)). The review's classical content is: the $\vec L_l$ behave as the area-weighted normals of a polyhedron, whose face areas are $|\vec L_l|$ and whose volume (for $v=4$) is given by the triple product (eq. (10)). Spins $j\in\{0,\tfrac12,1,\tfrac32,\dots\}$ label links; the quantity $\sqrt{j(j+1)}$ is the square root of the $SU(2)$ Casimir. The area spectrum (eq. (26)) is the set of numbers $8\pi\gamma\hbar G\sum_n\sqrt{j_n(j_n+1)}$ over finite families of spins, with $\gamma$ the Barbero–Immirzi parameter, $\hbar$ the reduced Planck constant and $G$ Newton's constant.

Formalization targets

Goal: Minkowski's theorem in the form of the spin–geometry theorem

For nonzero $n_1,\dots,n_v\in\mathbb E^3$ with pairwise distinct directions $\hat n_l$, spanning $\mathbb E^3$, and with $\sum_l n_l=0$:

$$\exists\,h:\ P(\hat n,h)\ \text{bounded, with nonempty interior, and}\ \operatorname{area}(F_l)=\|n_l\|\ \ \forall l,$$

and any two such polyhedra are translates of each other.

Milestones (in the order of the review)

1. Eq. (6), closure: for a bounded polyhedron with nonempty interior and distinct unit normals $u_l$, $\sum_l \operatorname{area}(F_l)\,u_l=0$.
2. Eq. (10), tetrahedron volume: with face area vectors $L_1,L_2,L_3$ of three faces through a vertex, $V^2=\tfrac29\,|L_1\cdot(L_2\times L_3)|$.
3. Eq. (13), area gap: $\min\{\sqrt{j(j+1)}: j\in\{\tfrac12,1,\tfrac32,\dots\}\}=\tfrac{\sqrt3}{2}$.
4. Eq. (18), area gap in physical units: the least positive element of the area spectrum is $8\pi\hbar G\gamma\,\tfrac{\sqrt3}{2}$.
5. Eq. (26), discreteness: for $\gamma,\hbar,G>0$ the area spectrum has only finitely many elements below any bound.

Significance

The goal theorem is the precise mathematical content behind the statement that "the algebraic structure of the momentum operators determines the existence of a metric at each node and therefore equips each quantum of space with a geometry" (§2.1). Its necessity half (milestone 1) is the classical counterpart of the gauge-invariance constraint (6); its sufficiency and uniqueness halves are what allow LQG states to be read as quantum polyhedra and underlie the "twisted geometry" and polyhedral-volume constructions. The spectral milestones encode the review's discrete-geometry claims in the elementary, operator-free form in which they are stated in eqs. (13), (18) and (26).

All statements here are known theorems; none is open. A search of Mathlib (at the revision used to check these statements) found no theory of convex polytopes, facet areas, the Brunn–Minkowski inequality, or Minkowski's theorem for polyhedra.

Difficulty

The necessity direction (closure) is a divergence-theorem or projection argument, but requires relating the facets of an H-described polytope to its boundary. The existence direction of Minkowski's theorem is a variational argument (maximize volume subject to a linear constraint on support numbers) whose difficulty lies in showing that the optimum has all prescribed faces with positive area; uniqueness is classically deduced from the equality case of the Brunn–Minkowski (or Minkowski mixed-volume) inequality. The spectral milestones are elementary.

Formalization scope

Lean represents $\mathbb E^3$ as EuclideanSpace ℝ (Fin 3). A polyhedron is given by a finite family of normals and support numbers (halfspacePolyhedron), faces by polyhedronFace, and face area by planarArea, the Haar (Lebesgue) measure of the orthogonal projection onto the plane orthogonal to the normal, valued in $[0,\infty]$; areas are compared as extended reals so that an infinite area cannot be confused with $0$. Unit normals are obtained as $n/\|n\|$ (unitDir). The cross product is Mathlib's crossProduct transported to EuclideanSpace. Spins are encoded as $k/2$ with $k\in\mathbb N$, and the area spectrum sums over finite multisets of spins.

The goal excludes trivializing readings: the spanning and distinct-direction hypotheses are the classical non-degeneracy conditions of Minkowski's theorem (without them the existence claim is false), and the conclusion demands a bounded polyhedron with nonempty interior, so empty or flat polyhedra do not count. The review's eq. (10) omits numerical constants; the milestone uses the exact Euclidean constant $2/9$. The operator-theoretic statements of the review (spectra of area and volume operators on $L^2(SU(2)^L/SU(2)^N)$) are out of scope; only their stated numerical content is formalized.

Reusable infrastructure: H-polytopes in $\mathbb R^3$, facet areas, the closure identity, and the Brunn–Minkowski equality case. Contributions of general convex-geometry lemmas are welcome.

Selected references

• C. Rovelli, Loop quantum gravity: the first 25 years, Class. Quantum Grav. 28 (2011) 153002. https://doi.org/10.1088/0264-9381/28/15/153002 (arXiv:1012.4707)
• H. Minkowski, Allgemeine Lehrsätze über die konvexen Polyeder, Nachr. Ges. Wiss. Göttingen (1897) 198–219.
• E. Bianchi, P. Doná, S. Speziale, Polyhedra in loop quantum gravity, Phys. Rev. D 83 (2011) 044035. https://arxiv.org/abs/1009.3402
• A. D. Alexandrov, Convex Polyhedra, Springer (2005).

Motivation

The simplex method and every other edge-following linear programming algorithm moves from vertex to vertex of the feasible region along its edges. The number of steps such an algorithm needs in the worst case is at least the combinatorial diameter of the feasible polyhedron: the largest distance, counted in edges, between two of its vertices. Klee and Walkup introduced the two functions that measure this worst case, $\Delta(d,n)$ for polyhedra and $\Delta_b(d,n)$ for bounded polyhedra of dimension $d$ with $n$ facets, and wrote that $\Delta(d,n)$ "represents, in a sense, the number of iterations required to solve the 'worst' linear program of $n$ inequalities in $d$ variables using the 'best' edge-following algorithm" (Klee and Walkup 1967, p. 54).

The Hirsch conjecture, reported by Dantzig in 1963, asserted $\Delta(d,n)\le n-d$. Its diagonal cases $\Delta(d,2d)\le d$ and $\Delta_b(d,2d)\le d$ are the general and the bounded $d$-step conjectures.

Timeline.

• 1957–1963: W. M. Hirsch's conjecture, reported in Dantzig's Linear Programming and Extensions (1963, pp. 160, 168), with the claim that it holds for $m\le 4$.
• Before 1967: Klee determines $\Delta(3,n)=n-3$ and $\Delta_b(3,n)=\lfloor 2n/3\rfloor-1$ and settles $\Delta_b(d,n)$ for $n\le d+4$ (Canad. J. Math. 16 and the papers cited as [9], [12], [13] by Klee and Walkup, p. 55).
• 1967: Klee and Walkup (Acta Math. 117) prove $\Delta_b(5,10)=5$, show that $\Delta_b(d,2d)\le d$ for all $d$ is equivalent to the bounded Hirsch conjecture, and disprove the unbounded conjecture with $\Delta(4,8)=5$.
• 2012: Santos disproves the bounded Hirsch conjecture with a 43-dimensional polytope with 86 facets (Ann. Math. 176). The bounded $d$-step conjecture therefore fails for some $d$, and the smallest failing $d$ is unknown; it is at least 6.

Setting

A polyhedron in $\mathbb R^d$ is a nonempty set $P=\{x:\langle a_i,x\rangle\le b_i,\ i=1,\dots,n\}$; a polytope is a bounded polyhedron. $P$ is a $d$-polyhedron with $n$ facets when it has nonempty interior and none of the $n$ inequalities is redundant; then the rows are in bijection with the facets, and row $i$ is tight at $v$ exactly when $v$ lies on the $i$-th facet. The vertices of $P$ are its extreme points. Two vertices $u\ne v$ span an edge when the segment $[u,v]$ is an extreme subset of $P$. A path of length $l$ is a sequence of $l$ edges $[x_0,x_1],\dots,[x_{l-1},x_l]$, and $\delta_P(x,y)$ is the least length of a path from $x$ to $y$. Then

$$\Delta_b(d,n)=\max\{\delta_P(x,y): P\text{ a }d\text{-polytope with }n\text{ facets},\ x,y\text{ vertices of }P\}.$$

$P$ is simple when every vertex lies on exactly $d$ facets. A face is $P$ itself or the intersection of $P$ with a supporting hyperplane, never $\emptyset$; its dimension is that of its affine hull. A $(k_1,\dots,k_r)$-path from $x$ to $y$ is a sequence of faces $K_1,\dots,K_r$ with $x\in K_1$, $y\in K_r$, $\dim K_i=k_i$ and $K_i\cap K_{i+1}\ne\emptyset$. A $d$-dimensional Dantzig figure $(P,x,y)$ is a $d$-polyhedron $P$ with $2d$ facets and two vertices $x,y$ such that exactly $d$ facets are incident to $x$ and the other $d$ to $y$. A $d$-polytope $Q$ has property A when it has between $2d$ and $2d+2$ facets and the following holds: if its facets are split into two classes $\mathfrak X,\mathfrak Y$ of at most $d+1$ facets each, and both sets $X$, $Y$ of vertices all of whose facets lie in $\mathfrak X$, respectively $\mathfrak Y$, are nonempty, then some vertex of $X$ is joined to some vertex of $Y$ by a path of length at most $d$.

Formalization targets

Goal: 4.3 THEOREM

$$\Delta_b(5,10)=5.$$

In two halves: every $5$-polytope with $10$ facets satisfies $\delta_P(x,y)\le 5$ for all vertices $x,y$, and some $5$-polytope with $10$ facets has two vertices with $\delta_P(x,y)>4$.

Milestones, in the order the proof uses them

1. 2.8 THEOREM (bounded part): $\Delta_b(d,n)$ is attained by two vertices of a simple $d$-polytope with $n$ facets, and for $n\ge 2d$ by two vertices on no common facet. For $n=2d$ this is a bounded simple Dantzig figure.
2. 3.4 PROPOSITION (a): every simple Dantzig figure admits a $(k_1,1,k_3)$-path for positive $k_1+1+k_3=d$.
3. 3.1 PROPOSITION: (a) facial paths in all $d$-dimensional simple Dantzig figures, (b) facet-avoiding facial paths in simple $d$-polytopes with $2d+1$ facets, and (c) facet-avoiding $(1,k_1,\dots,k_r)$-paths in bounded $(d+1)$-dimensional figures are equivalent.
4. 3.4 PROPOSITION (b): every bounded simple Dantzig figure admits a $(1,k_2,1,k_4)$-path for positive $1+k_2+1+k_4=d$.
5. Remark after 3.4: adjacent terms of a facial path in a simple figure merge into their sum.
6. Remark after 3.4, p. 68: bounded simple Dantzig figures of dimension $d\ge 2$ admit $(1,d-2,1)$-paths.
7. 4.1 PROPOSITION: if the middle face $Q$ of a $(1,d-2,1)$-path $([x,x'],Q,[y',y])$ has property A, then $\delta_P(x,y)\le d$.
8. 4.2 LEMMA: every simple $3$-polytope with $6$, $7$ or $8$ facets has property A.

Significance

The result. By the paper's reductions, $\Delta_b(d,2d)\le d$ for a given $d$ is equivalent to the bounded Hirsch bound $\Delta_b(d',d'+d)\le d$ for every $d'$. So 4.3 gives $\Delta_b(d,n)\le n-d$ for all $n\le d+5$, which is the column $n-d=5$ of the paper's Fig. 2. Since Santos's counterexample, the smallest $d$ with $\Delta_b(d,2d)>d$ is a well-defined open number. This theorem was the first to show it is at least $6$; later computer-assisted work treated further small cases, including the bounded $6$-step case (Bremner and Schewe 2011). Santos's construction starts from exactly the reduction to Dantzig figures (the "strong $d$-step theorem" for spindles) that this paper uses.

Formalizing it. The result has been proved since 1967; no machine-checked proof of $\Delta_b(5,10)=5$ exists. The platform has the Hirsch bound in dimension $\le 3$ (Hirsch.dimension_three_bound, Hirsch.klee_three_dimensional_bound), the Klee–Walkup wedge reduction at the level of inequality descriptions (Hirsch.balanced_hpoly_transfer), products (Hirsch.diamLE_prod) and Santos's counterexample. The mission adds the facial-path calculus of §3 and the property-A argument of §4. Both are reusable in any later formal treatment of small $d$-step cases.

Difficulty

The obvious approach, a direct case analysis of $5$-polytopes with $10$ facets, is out of reach: there are far too many combinatorial types, and nothing bounds the search. The paper first reduces to simple polytopes, and the reduction itself (2.8) rests on a perturbation lemma (2.6) whose proof is deferred to a separate paper by Walkup: simplicity must be gained without shrinking any distance. The facial-path results then pass between bounded and unbounded figures through truncation and the wedge (3.1), and a statement about all unbounded $d$-dimensional figures is what yields one about bounded $(d+1)$-dimensional ones. Finally the $(d-2)$-face $Q$ must be shown to have property A. That property fails for some simple polytopes of classes $(4,10)$ and $(5,11)$ (p. 69), so 4.2 depends on the dimension being $3$ and on the facet count being at most $8$. Its proof uses Euler's relation and Balinski's theorem that the graph of a $3$-polytope is $3$-connected (posed on the platform as Balinski61.Connectivity.disjoint_paths_between_vertices).

Formalization scope

Polyhedra are Hirsch.Hpoly a b with a : Fin n → EuclideanSpace ℝ (Fin d); edges and walks are Hirsch.Adj and Hirsch.Reach from the published Hirsch_model and Hirsch_walk. The conventions are:

• "$d$-polyhedron with $n$ facets" is a facet presentation: nonempty interior and no redundant row. The rows are exactly the facets; a statement over arbitrary inequality systems would count redundant rows as facets and is not the paper's.
• $\delta_P(x,y)\le L$ is Hirsch.Reach P L x y, a walk of $L$ steps that may stand still. $\Delta_b(5,10)=5$ is an upper bound for every polytope plus a witness, never a supremum of reals. A version proving only the upper bound, or only the lower bound, is not the goal.
• Simple means pointed with exactly $d$ tight rows at every vertex. On a facet presentation this is equivalent to the paper's "exactly $d$ edges at each vertex".
• Faces are nonempty sets $\{x\in P:\langle a_i,x\rangle=b_i,\ i\in I\}$, and dimension is the dimension of the affine span. A Dantzig figure has Fin (2 * d) rows.
• Property A is defined for a bounded face $Q$ of dimension $m$: its facets are the $(m-1)$-faces of $P$ inside $Q$, and the path runs in $Q$. This keeps 4.1, where $Q$ is a $(d-2)$-face of a polytope in $\mathbb R^d$, and 4.2, where $Q=P$, under one notion. Facet counts use Set.encard.
• Explicit readings: 2.8's "$\Delta_b$ can be realized as the distance … of a simple polytope" is stated polytope by polytope ($\delta_P(u,v)\le\delta_{P'}(x,y)$). Only the $\Delta_b$ sentences of 2.8 are stated. 3.4's joint hypothesis on $k_1,\dots,k_4$ is split by part. The merging remark carries the needed hypothesis $k_i+k_{i+1}\le d$. The printed "3.5 implies" on p. 67 is read as 3.4.

The paper cites two inputs without proving them: Lemma 2.6 (Walkup's simple perturbation) and Balinski's theorem. A complete development needs face lattices of H-polyhedra, wedges and truncations, and the planar-graph arguments of 4.2. The face and facial-path layer is reusable for the companion mission on $\Delta(4,8)=5$ and for other diameter problems. Contributions are welcome at every milestone, including proofs of 2.6.

Selected references

• V. Klee and D. W. Walkup, The d-step conjecture for polyhedra of dimension d < 6, Acta Mathematica 117 (1967), 53–78. https://doi.org/10.1007/BF02395040
• G. B. Dantzig, Linear Programming and Extensions, Princeton University Press, 1963.
• V. Klee, Diameters of polyhedral graphs, Canadian Journal of Mathematics 16 (1964), 602–614. https://doi.org/10.4153/CJM-1964-058-5
• M. L. Balinski, On the graph structure of convex polyhedra in n-space, Pacific Journal of Mathematics 11 (1961), 431–434. https://doi.org/10.2140/pjm.1961.11.431
• F. Santos, A counterexample to the Hirsch conjecture, Annals of Mathematics 176 (2012), 383–412. https://doi.org/10.4007/annals.2012.176.1.7
• D. Bremner and L. Schewe, Edge-graph diameter bounds for convex polytopes with few facets, Experimental Mathematics 20 (2011), 229–237. https://doi.org/10.1080/10586458.2011.564966

Motivation

The simplex method solves a linear program by walking along the edges of the feasible polyhedron, from vertex to vertex. However cleverly a pivot rule chooses its steps, it cannot reach the optimum in fewer steps than the graph distance from the starting vertex. The largest possible graph diameter of a polyhedron therefore bounds from below the worst-case number of pivots of every pivot rule, and whether that diameter is polynomial in the size of the problem is one of the basic open questions of linear optimization (Klee–Kleinschmidt 1987).

Timeline.

• 1957: Hirsch conjectures that a $d$-dimensional polyhedron with $n$ facets has graph diameter at most $n-d$ (reported in Dantzig, Linear Programming and Extensions, 1963).
• 1967: Klee and Walkup show the conjecture false for unbounded polyhedra, with the lower bound $n-d+[d/5]$ for $n\ge2d$ (Acta Math. 1967).
• 1967–1970: Barnette proves $\Delta(d,n)\le n3^{d-3}$, and Larman improves it to $n2^{d-3}$ (Proc. LMS 1970); both are linear in $n$ but exponential in $d$.
• 1990–1992: Kalai proves a subexponential bound, and then Kalai and Kleitman prove the quasi-polynomial bound $n^{\log d+2}$ that is the subject of this mission (Bull. AMS 1992, arXiv:math/9204233).
• 2012: Santos disproves the Hirsch conjecture for bounded polytopes (Ann. Math. 2012). Whether a polynomial bound holds remains open; the best general upper bounds known are refinements of the exponent of the Kalai–Kleitman bound.

Setting

A polyhedron in $\mathbb R^d$ is the solution set of finitely many linear inequalities,

$$P=\{x\in\mathbb R^d:\ \langle a_i,x\rangle\le b_i,\ i=1,\dots,n\},\qquad a_i\in\mathbb R^d,\ b_i\in\mathbb R .$$

It may be bounded or unbounded, and empty. Its vertices are its extreme points. Two distinct vertices $u,v$ are adjacent when the segment $[u,v]$ is an edge of $P$, a one-dimensional face; unbounded one-dimensional faces (rays) are not edges. The graph $G(P)$ consists of these vertices and edges, and its diameter $\delta(P)$ is the largest graph distance between two vertices. Kalai and Kleitman write $\Delta(d,n)$ for the largest diameter of the graph of a $d$-dimensional polyhedron with $n$ facets.

For a set $F$ of row indices, the relaxation $Q_F$ is the polyhedron obtained from $P$ by ignoring the inequalities with index outside $F$. A walk of $B$ steps is a sequence $w_0,\dots,w_B$ of points in which each step stays put or crosses an edge; "diameter at most $B$" means that any two vertices are joined by such a walk, which includes connectivity of the graph.

Formalization targets

Goal: Theorem 1

$$\Delta(d,n)\le n^{\log d+2}.$$

Stated for polyhedra given by inequalities: for all $d,n$ and all $a\in(\mathbb R^d)^n$, $b\in\mathbb R^n$, the graph of $P$ is connected and has diameter at most $\lfloor n^{\log_2 d+2}\rfloor$. No nonemptiness, boundedness or full-dimensionality is assumed.

Milestones, in the order the proof uses them

1. If a vertex $\omega$ of $P$ satisfies with equality only rows in $F$, then $\omega$ is a vertex of $Q_F$ (published).
2. If an edge of $Q_F$ starts at a point of $P$ and is not an edge of $P$, then it meets the hyperplane of an ignored row at a vertex of $P$ adjacent to its start, or at its start (published).
3. The claim $k_v\le\Delta(d,[n/2])$: if every vertex within distance $k$ of $v$ lies only on rows of $F$, and $G(Q_F)$ has diameter at most $B$, then every vertex within distance $k$ of $v$ is within distance $B$ of $v$.
4. The facet step: any two vertices of a face $\{x\in P:\langle a_i,x\rangle=b_i\}$ with $a_i\ne0$ are joined, inside that face, by a walk of at most $\Delta(d-1,n-1)$ edges.
5. The recursion $\Delta(d,n)\le\Delta(d-1,n-1)+2\Delta(d,[n/2])+2$, for polyhedra with nonzero rows.
6. The arithmetic: $N(d,n)=\lfloor n^{\log_2 d+2}\rfloor$ satisfies $N(d-1,n-1)+2N(d,\lfloor n/2\rfloor)+2\le N(d,n)$ for $d\ge2$, $n\ge d+1$.

Significance

The bound is polynomial in $n$ for each fixed $d$, and $n^{O(\log d)}$ overall. Before it, every bound was exponential in $d$ or subexponential in $n$. It remains, up to improvements of the exponent, the best known upper bound on the diameter of polyhedra, and thus the best known limit on how badly an optimal pivot rule must behave. Its proof is also the template for the later abstractions of the problem (connected layer families, subset partition graphs) in which the polynomial Hirsch question is studied.

The bounded case is already formalized on the platform: Hirsch.kalai_kleitman_bound states the theorem for nonempty bounded polytopes and is Proved, together with the bounded forms of the recursion (Hirsch.kalai_kleitman_recursion), of the facet step (Hirsch.facet_reduction, Hirsch.facet_walk) and of the zero-row reduction (Hirsch.diamLE_of_nonzero_rows), and the one-step relaxation lemma Hirsch.relaxation_no_new_neighbours. Kalai and Kleitman state Theorem 1 for all polyhedra: their introduction contrasts unbounded polyhedra (where Hirsch fails) with bounded ones. This mission formalizes the theorem as the paper states it, including unbounded polyhedra, where the bounded proofs do not apply as written. The combinatorial abstraction of the same bound (EHRR10.KalaiKleitman.diameter_le_kalai_kleitman, for the Eisenbrand–Hähnle–Razborov–Rothvoß model) is a different object and is not reused.

Difficulty

The bounded argument relies on compactness: faces are polytopes, every relaxation used in the induction is again a polytope, and the facet of a polytope is a polytope of one dimension less. The relaxation $Q_F$ contains $P$ and is typically unbounded even when $P$ is bounded, and for an unbounded polyhedron a face on a facet hyperplane can be unbounded or have no vertices at all. Each step must therefore hold for general polyhedra: that a shortest walk in $G(Q_F)$ between two vertices of the ball uses only edges of $P$, and that the graph of a face, identified with a polyhedron in $\mathbb R^{d-1}$, sits inside $G(P)$. The "maximal positive number $k_v$" of the paper need not exist, and the proof must handle the two cases (no radius qualifies; every radius qualifies) separately. Zero rows are allowed in the goal and must be removed before the recursion applies, since a zero row with $b_i=0$ is tight everywhere.

Formalization scope

Lean represents $\mathbb R^d$ as EuclideanSpace ℝ (Fin d) and the polyhedron as Hirsch.Hpoly a b with a : Fin n → ℝ^d, b : Fin n → ℝ, from the published definition Hirsch_model, which also supplies adjacency Hirsch.Adj (the segment is an extreme subset) and the diameter predicate Hirsch.DiamLE. The mission commits to these explicit readings:

• "$\Delta(d,n)\le N$" is ∀ a b, DiamLE (Hpoly a b) N over $n$ inequalities in $\mathbb R^d$. This is equivalent to the facet formulation, since a $d$-dimensional polyhedron is cut out by its facet inequalities and a polyhedron given by $n$ inequalities in $\mathbb R^d$ has dimension at most $d$ and at most $n$ facets.
• "log" is $\log_2$ (Real.logb 2), the power is the real power, and the integer bound is its floor ⌊·⌋₊, which is equivalent because distances are natural numbers.
• "$[n/2]$" is $\lfloor n/2\rfloor$ (ℕ division); "at most $n/2$ facets" is a row set of cardinality at most $\lfloor n/2\rfloor$.
• An ignored row is replaced by the vacuous inequality $\langle0,x\rangle\le1$, which keeps the index type Fin n.
• Walks have exactly $B$ steps with stationary steps allowed, so "$B$ steps" means "at most $B$ edges".
• The paper's $k_v$ is not defined; milestone 3 quantifies over every radius with the ball property.
• Milestones 4 and 5 assume nonzero rows; the goal does not.

A statement with a boundedness or nonemptiness hypothesis, with the graph diameter measured by a distance function whose value on unreachable pairs is $0$, or with the bound read with Nat.log or the natural logarithm, is not the target. Contributions welcome: proofs of the general-polyhedron facet step and of milestone 3, a general zero-row reduction, the arithmetic of milestone 6, and the base cases $d\le1$ and $n\le d$.

Selected references

• G. Kalai and D. J. Kleitman, A quasi-polynomial bound for the diameter of graphs of polyhedra, Bull. Amer. Math. Soc. 26 (1992), 315–316. https://doi.org/10.1090/S0273-0979-1992-00285-9 (arXiv:math/9204233)
• V. Klee and D. W. Walkup, The d-step conjecture for polyhedra of dimension d < 6, Acta Math. 117 (1967), 53–78. https://doi.org/10.1007/BF02395040
• V. Klee and P. Kleinschmidt, The d-step conjecture and its relatives, Math. Oper. Res. 12 (1987), 718–755. https://doi.org/10.1287/moor.12.4.718
• D. G. Larman, Paths on polytopes, Proc. London Math. Soc. (3) 20 (1970), 161–178. https://doi.org/10.1112/plms/s3-20.1.161
• F. Santos, A counterexample to the Hirsch conjecture, Ann. of Math. 176 (2012), 383–412. https://doi.org/10.4007/annals.2012.176.1.7

Why the simplex method needs smoothed analysis

The simplex method solves linear programs quickly in practice, yet for most pivot rules there are inputs on which it takes exponentially many steps (Klee and Minty, 1972). Smoothed analysis, introduced by Spielman and Teng (JACM 2004), explains the gap: it measures the expected running time when every constraint row of a worst-case input is perturbed by a small random amount of size $\sigma$. For the shadow vertex pivot rule, the running time is controlled by a purely geometric quantity, the number of edges of a random polygon, and the smoothed complexity of the method is essentially an upper bound on that number.

Timeline (bounds on the expected shadow size of smoothed unit LPs, as surveyed in §1.1 of the paper). Borgwardt (1987) proved $\Theta(d^{1.5}\sqrt{\log n})$ for rows drawn from a centered Gaussian, asymptotically as $n\to\infty$; this is the case $\bar a_i=0$ of the model below. Spielman and Teng (2004) gave the first smoothed bound, $O(d^3n\sigma^{-6}+d^6n\log^3 n)$. Deshpande and Spielman (FOCS 2005) improved the dependence on $\sigma$ to $O(dn^2\log n\,\sigma^{-2}+d^2n^2\log^2 n)$. Vershynin (SIAM J. Comput. 2009) reduced the dependence on $n$ to polylogarithmic, $O(d^3\sigma^{-4}+d^5\log^2 n)$. Dadush and Huiberts (arXiv:1711.05667, STOC 2018, SIAM J. Comput. 2020) proved $O(d^2\sqrt{\log n}\,\sigma^{-2}+d^{2.5}\log n\,\sigma^{-1}+d^{2.5}\log^{1.5}n)$ for Gaussian perturbations by a simpler argument, which also gives bounds for Laplace perturbations.

Setting

Fix dimensions $n\ge d\ge3$ and a shadow plane, a two-dimensional linear subspace $W\subseteq\mathbb R^d$, chosen independently of the randomness. The constraint vectors $a_1,\dots,a_n\in\mathbb R^d$ are independent, and $a_i\sim N_d(\bar a_i,\sigma)$ is Gaussian with center $\bar a_i$, $\|\bar a_i\|\le1$, and standard deviation $\sigma>0$ in every coordinate, i.e. with density $(2\pi\sigma^2)^{-d/2}e^{-\|x-\bar a_i\|^2/(2\sigma^2)}$.

Let $Q=\operatorname{conv}(a_1,\dots,a_n)$. The shadow polygon is $Q\cap W$. An edge of a convex set $K$ is a segment $[u,v]$, $u\ne v$, which is an extreme subset of $K$; $|\operatorname{edges}(K)|$ is the number of edges. The number of pivots of the shadow vertex method on the unit LP $\{x:Ax\le\mathbf1\}$ between two objectives spanning $W$ is at most $|\operatorname{edges}(Q\cap W)|$ (the paper's Lemma 11 and Theorem 12).

The proof passes through general row distributions with density $\mu$ and mean $y$, described by four parameters: the log-Lipschitz constant $L$ ($\mu(x)\le e^{L\|x-x'\|}\mu(x')$); the line variance $\tau^2$ (the least variance of $\mu$ restricted to a line); the $n$-th deviation $r_n$ (the least $r$ with $\int_r^\infty\Pr[|(X-y)^\mathsf T\theta|\ge t]\,dt\le r/n$ for all unit $\theta$); and the cutoff radius $R_{n,d}$ (the least $R$ with $\Pr[\|X-y\|\ge R]\le 1/(d\binom nd)$). The Gaussian is not log-Lipschitz; the Laplace–Gaussian distribution $LG_d(\bar a,\sigma,r)$, whose density equals the Gaussian one inside the ball of radius $r\sigma$ around $\bar a$ and decays like $e^{-\|x-\bar a\|r/\sigma}$ outside, replaces it.

Formalization targets

Goal: Theorem 13 with explicit constants

$$\mathbb E\big[|\operatorname{edges}(\operatorname{conv}(a_1,\dots,a_n)\cap W)|\big]\le 3+\frac{128\pi e^2 d^2\sqrt{\log n}}{\sigma^2}\big(1+4\sigma\sqrt{d\log n}\big)\big(1+16\sigma\sqrt{\log n}\big).$$

The paper states $O(d^2\sqrt{\log n}\,\sigma^{-2}+d^{2.5}\log n\,\sigma^{-1}+d^{2.5}\log^{1.5}n)$; the constant above is the one its proof produces (Theorem 22's proof, Lemma 45, Lemma 46).

Intermediate targets (milestones)

• the parametrized shadow bound (Theorem 22), $\mathbb E|\operatorname{edges}|\le 2+8\pi e^2d^{1.5}(L/\tau)(1+R_{n,d})(1+4r_n)$;
• its ingredients: the edge-counting reduction (Lemma 25), the perimeter bound $2\pi(1+4r_n)$ (Lemmas 19, 26), the conditioning on bounded diameter (Lemma 29), the chord combination calculus (Lemmas 35, 36), and the two expected-length bounds (Lemmas 39, 40, 41), together with the trade-off $LR(1/2)\ge d/3$ (Lemma 21);
• the Gaussian specialisation: Laplace–Gaussian tails (Lemma 44), its parameters (Lemma 45), and the comparison with the Gaussian (Lemma 46).

Significance

The bound gives the best known smoothed complexity of a simplex method, with only $\sqrt{\log n}$ dependence on the number of constraints. Section 4 of the paper turns it into a complete two-phase shadow vertex algorithm with $O(d^2\sqrt{\log n}\,\sigma^{-2}+d^3\log^{1.5}n)$ expected pivots. The parametrized Theorem 22 applies to any perturbation family with bounded parameters, so it also yields shadow bounds for Laplace and other noise models.

The result is proved; it has not been machine-checked. A formalization adds a verified chain from four distributional parameters to a polygon edge count. The intermediate statements have independent value: an expected-perimeter bound for random polygons, the deterministic chord-length identity for simplices, and tail estimates for the Laplace–Gaussian distribution.

Difficulty

The expected number of edges is a sum, over all $\binom nd$ index sets, of the probability that their simplex meets $W$ in an edge; there are far too many terms for per-set estimates to give a bound polylogarithmic in $n$. The paper's route (inspired by Kelner and Spielman) instead compares the expected perimeter with the expected length of an edge, and the hard part is a lower bound on the expected length of an edge conditioned on it appearing. That conditioning is on a probability-zero configuration (the simplex lying in a fixed hyperplane), and its analysis needs Blaschke's change of variables, the shape decomposition of the simplex, and log-Lipschitz shifts of densities. On the Gaussian side, the density is not log-Lipschitz, which forces the Laplace–Gaussian detour and a comparison of edge counts under two different laws.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d), $[n]$ is Fin n, $\log$ is the natural logarithm. The Gaussian is the published SmoothedSimplex.Shadow.gaussian, the edge relation is the published Hirsch.Adj, and the rows' joint law is Measure.pi. Edges are segments counted once; the perimeter is the sum of edge lengths. Expectations are lower Lebesgue integrals in $[0,\infty]$, and every edge-count bound also asserts almost-everywhere measurability of the count, so the integral is a genuine expectation. Conditional expectations are stated multiplied out (no division by a probability), and the parameters of Definitions 15–18 are upper-bound predicates (lower bound for the line variance), which is how every statement of the paper uses them.

Hypotheses added relative to the page, each implicit there: $\sigma>0$; $L,\tau>0$ and $R,r\ge0$ in Theorem 22; positivity of log-Lipschitz densities; the standing $n\ge d\ge3$ of §3 in Lemma 44. Lemmas 39 and 41 are stated on the explicit conditional densities that the paper derives in Lemma 37, instead of through regular conditional distributions; Lemma 39 takes the conclusion $d/3\le LR$ of Lemma 21 as a hypothesis, as its proof uses it. Two printed slips are corrected: Lemma 46's formula is stated for $\operatorname{conv}(a_1,\dots,a_n)\cap W$, as its sentence and proof have it, and Lemma 35 refers to Definition 33 (not 34).

The goal mentions only Gaussian rows, $W$, and the edge count of $\operatorname{conv}(a)\cap W$. It cannot be trivialized by an unsatisfiable parameter hypothesis or a bound on edge lengths, since it has neither; and it counts edges of the polygon, not of the polytope $\operatorname{conv}(a)$.

A complete development needs: Gaussian and Laplace–Gaussian tail bounds; measurability of the edge count of a random polygon; the perimeter monotonicity of convex sets; Blaschke's change of variables (Theorem 7 of the paper, quoted from Blaschke 1935), which Mathlib does not have; and the regular conditioning of Lemmas 32, 37 and 38. The Blaschke formula, the perimeter facts for convex polygons, and the tail bounds are reusable well beyond this mission. Contributions to any milestone, or to these supporting results as separate theorems, are welcome.

Selected references

• D. Dadush, S. Huiberts, A Friendly Smoothed Analysis of the Simplex Method, SIAM J. Comput. 49(5), 2020 (STOC 2018); preprint arXiv:1711.05667v4, 2019. https://arxiv.org/abs/1711.05667
• D. A. Spielman, S.-H. Teng, Smoothed analysis of algorithms: Why the simplex algorithm usually takes polynomial time, J. ACM 51(3), 2004. https://doi.org/10.1145/990308.990310
• R. Vershynin, Beyond Hirsch Conjecture: Walks on Random Polytopes and Smoothed Complexity of the Simplex Method, SIAM J. Comput. 39(2), 2009. https://doi.org/10.1137/070683386
• A. Deshpande, D. A. Spielman, Improved smoothed analysis of the shadow vertex simplex method, FOCS 2005 (cited as [DS05] in the paper).
• V. Klee, G. J. Minty, How good is the simplex algorithm?, in Inequalities III, Academic Press, 1972 (cited as [KM70] in the paper).