Formally Certifying the Vertex Set of a Polyhedron Faster than Informal Enumeration

1 Introduction

• H-to-V conversion is a major bottleneck in applications including static analysis, neural-network verification, and dynamical-system analysis.Vertex enumeration also connects to polytope graph diameters and the polynomial Hirsch conjecture.Source: §1 · p. 1
• The method certifies whether an informally computed vertex list contains or equals a polytope’s vertex set, and can also certify its vertex-edge graph.Its input is an inequality description and a certificate built from lrslib output.Source: §1 · p. 2
• An abstract simplicial complex encodes tiles in candidate vertices’ normal cones, and an odd-covering criterion certifies that the tiles cover the whole space.The tiles may overlap and have arbitrary dimension, relaxing the requirements of a triangulation.Source: §1 · p. 2
• The checker is implemented in Rocq, but the odd-covering criterion and vertex-edge graph correctness arguments remain supported by paper proofs rather than formalization.The implementation also proves equivalence between high- and low-level checkers.Source: §1 · p. 2
• Experiments cover classical polytope families and 20- and 23-dimensional counterexamples to the Hirsch conjecture.The tested families include Birkhoff polytopes, cross-polytopes, cubes, cyclic polytopes, permutahedra, and hypersimplices.Source: §1 · p. 2
• The extracted checker is typically 1.5x to over 5x faster than lrslib vertex enumeration, and up to 50x faster.For the two Hirsch-conjecture counterexamples, Rocq checking takes 30 and 70 seconds, compared with more than an hour in prior graph-certification work.Source: §1 · p. 2
• Unlike prior graph certification, this checker need not verify the specific lexicographic triangulation, avoiding substantial numerical work such as matrix-rank tests.The earlier method of Allamigeon et al. [2023] certifies that specific triangulation.Source: §1 · p. 3
• Whether vertex-set exactness or completeness has a polynomial-time certification method remains open, despite both decision problems being in coNP.An earlier homological completeness criterion uses boundary-matrix ranks that can be exponential in size [Joswig and Ziegler 2004].Source: §1 · p. 3

2 Polyhedra and Normal Fans

• A polyhedron is defined by finitely many linear inequalities, while a bounded polyhedron is the convex hull of a finite point set and is called a polytope.Polyhedral cones likewise admit finite generating sets of vectors.Source: §2 · p. 4
• Faces are sets maximizing a linear function; vertices are zero-dimensional faces, and edges are one-dimensional faces that define the vertex-edge graph.The vertex-edge graph links vertices that lie on a common edge.Source: §2 · p. 4
• A point’s normal cone contains the linear-function vectors it maximizes, and is generated by the normals of inequalities active at that point.The normal fan is the finite collection of these cones, whose pairwise intersections are common faces.Source: §2 · p. 4
• For a nonempty polyhedron and a candidate set within it, being a polytope with all vertices included is equivalent to the candidate vertices’ normal cones covering R^d.This finite coverage condition discretizes the otherwise infinite set of linear functions to consider.Source: §2 · p. 4

3.1 Overview: the Role of Triangulations

• Candidate vertices are complete when their normal cones cover R^d; because these cones are invariant under positive scaling, the covering can be viewed on the unit sphere.The section illustrates the spherical view with the normal fan of a three-dimensional cross-polytope.Source: §3.1 · p. 4, Figure 2 · p. 6
• The earlier triangulation criterion requires each cone facet to belong to exactly two cones, one on each side, plus a vector interior to exactly one cone.It applies to a finite collection of d-dimensional simplicial cones covering R^d.Source: §3.1 · p. 5
• That earlier criterion requires solving a (d−1)×(d−1) linear system for every simplicial cone, so its numerical workload grows with the triangulation.The number of systems may be very large.Source: §3.1 · p. 5
• The criterion relaxes triangulation requirements: its incidence conditions use abstract-complex parity rather than geometric facet checks, and cells need not be d-dimensional or intersect only on boundaries.The conditions generalize the earlier triangulation criterion.Source: §3.1 · p. 5, §3.2 · p. 6

3.2 The Statement

• If every ridge lies in an even number of facets, a witness vector lies in an odd number of facet cones, and those cones are pointed, then every d-generic vector lies in an odd number of them.Under these conditions, the facet cones cover R^d.Source: §3.2 · pp. 6–7
• Along a generic path from the witness to a generic target, the number of containing facet cones changes by an even amount at each ridge crossing, preserving odd parity.The path has finitely many transversal intersections with (d−1)-dimensional cones.Source: §3.2 · p. 7

4.1 Vertex-Set Completeness

• The abstract simplicial complex generated by F organizes cones assigned to candidate vertices, and covering the space by those cones yields vertex-set completeness.Under T3, every ridge appears in an even number of facets; the special cone condition supplies the required distinguished interior point.Source: §4.1 · p. 8
• Verification takes O(poly(d,n)(#V + #F)) time, and for simple polytopes it is polynomial in dimension, inequality count, and vertex count.For simplicial polytopes, the paper also describes certifying the polar polytope as a potentially better approach when F is much larger than the vertex set.Source: §4.1 · pp. 8–9

4.2 Vertex Set and Vertex-Edge Graph

• Conditions T1–T6 certify that a full-dimensional polytope’s candidate set is exactly its vertex set.With T1–T5, the set contains all vertices and the polyhedron is a polytope; T6 additionally certifies that each candidate is a vertex.Source: §4.1 · p. 8, §4.2 · p. 9
• T1–T6 certify that the candidate graph contains the polytope’s vertex-edge graph, while T1–T7 certify that the graphs are equal.The containment result can certify lower bounds on polytope graph diameters.Source: §4.2 · p. 9

4.3 Building a Certificate from Lex-Feasible Bases

• The certificate uses lex-feasible bases as facets, maps each basis to its polytope vertex, and connects bases that differ by one element.The normal fan of the perturbed polytope is simplicial and refines the original normal fan; these certificate components satisfy T1–T3.Source: §4.3 · pp. 9–10
• Dual vectors and separation weights establish T4–T5, flags provide T6, and incomparable active-inequality sets establish T7.The T6 construction uses a chain of faces above each vertex; T7 follows from the incomparable active-inequality sets of adjacent vertices.Source: §4.3 · p. 10

5.1 Correctness Proof of the Certification Method

• The high-level correctness theorem establishes vertex-set equality after well-formedness, full-dimensionality, and checks T1–T6; the graph-certification correctness proof remains work-in-progress.The theorem extracts the polytope and candidate points from the certificate.Source: §5.1 · p. 11

5.2 Efficient Implementation and Refinement Proof

• A low-level checker uses computation-oriented types and is related to the high-level checker by reflection lemmas and one-way refinement proofs.The low-level certificate is a compact binary file loaded into Rocq; the same functions are extracted to native OCaml.Source: §5.2 · p. 11

5.3 Experimental Results

• Experiments cover Birkhoff polytopes, cross-polytopes, cubes, dual cyclic polytopes, permutahedra, hypersimplices, and two high-dimensional Hirsch counterexamples.The counterexamples are 20- and 23-dimensional, with 36,425 and 73,224 vertices, respectively.Source: §5.3 · pp. 11–12
• The benchmark pipeline post-processes lrslib output into a binary certificate, with generation taking less than 20% of lrslib time except for cubes, where it takes around 40%.Measurements compare checker time with single-threaded lrslib enumeration time and report certificate loading separately for the extracted checker.Source: §5.3 · p. 12, Table 2 · p. 13
• Rocq execution is 15× to more than 1000× faster than the graph-certification approach of Allamigeon et al. [2023] on benchmark instances.For the two Hirsch counterexamples, laptop checks take 31 and 72 seconds; the poly20dim21 certificate is 67 MB versus more than 1.2 GB in.Source: §5.3 · p. 12, Table 1 · p. 12
• Vertex-set certification is faster than lrslib enumeration on every instance, by factors of 1.7 to 50; full graph certification is faster by a factor of 1.25 in the worst case.The cross-polytope cases are extreme: their abstract simplicial complexes have 2^d! facets versus 2^d vertices.Source: §5.3 · p. 13

Conclusion

• Odd-covering relaxes triangulation requirements to certify polytope vertex sets and vertex-edge graphs, with a Rocq checker formally proved correct up to two ingredients.Those ingredients—the odd-covering criterion and the correctness argument for vertex-edge graph certification—have pen-and-paper proofs, with formalization left for future work.Source: §6 · p. 13
• The extracted OCaml checker is faster than lrslib for vertex enumeration, and the method improves prior graph-certification times by several orders of magnitude.The paper reports that formal guarantees come at a modest additional cost compared with informal computation.Source: §6 · p. 13

Future work

• The method is currently focused on polytopes; extending it to arbitrary polyhedra with vertices and extreme rays and to V-to-H conversion remains future work.The paper says these extensions do not require fundamentally new ideas.Source: §6 · p. 13
• The authors plan to replace the refinement proof between the high- and low-level checkers with one using dedicated refinement tools.The current proof was generated with AI assistance.Source: §6 · p. 13
• Tighter integration with lrslib could reuse its computations and reduce time spent generating and loading binary certificate files.The paper also suggests improving the lrslib-to-checker pipeline.Source: §6 · p. 13
• The authors identify edge condition T7 as a target for replacement by a flag-based criterion, but compactly sharing flags remains unresolved.They note that the potentially large number of edges makes compact representation necessary.Source: §6 · p. 13

Normal cones

• For a point in a polyhedron, its normal cone is generated by the normals of its active inequalities; on a face, this cone is constant across the relative interior.The active-inequality index set is likewise constant on the relative interior of a face.Source: A Properties of the Normal Fan · pp. 14–15

Face relations

• A face Q has a normal cone of dimension d − dim Q, and face containment reverses under the normal-cone relation.A vector in the relative interior of a face’s normal cone exposes that face as the set of maximizers of its linear function over P.Source: A Properties of the Normal Fan · p. 15

Normal fan support

• The union of all normal cones is the polar of the recession cone, and equals R^d exactly when P is a polytope.A point in the relative interior of a face’s normal cone cannot belong to the normal cone of a point outside that face.Source: A Properties of the Normal Fan · p. 15

Vertex completeness

• For a polytope, a candidate set contains every vertex exactly when its points’ normal cones cover R^d.The proof uses the fact that each true vertex has a normal cone with nonempty interior, which cannot overlap the normal cone of a different point at an interior vector.Source: A Properties of the Normal Fan · p. 15

Cone geometry

• A simplicial cone’s faces correspond to subsets of its generators, and its boundary is the union of the cones generated by its ridges.For a pure (d−1)-dimensional complex, the facets and ridges are its (d−1)- and (d−2)-dimensional faces.Source: B Odd-Covering Criterion: Extra… · p. 15

Generic paths

• A generic path meets (d−1)-dimensional cones only finitely often and transversally, so the sets of containing cones change only at isolated crossings.A linear path between d-generic vectors is generic when its endpoints satisfy the stated span-avoidance conditions.Source: B Odd-Covering Criterion: Extra… · p. 15

Parity argument

• Because the endpoint cone sets have the same parity along the path, odd coverage at one endpoint implies odd coverage at the other.The proof perturbs the starting vector when needed to ensure a generic path while preserving its initial cone set.Source: B Odd-Covering Criterion: Extra… · p. 16
• At each crossing, the symmetric difference of the endpoint cone sets is counted through incident ridges, yielding an even change in cardinality.The proof uses the fact that a generic crossing point lies in precisely two boundary cones of each relevant pointed cone.Source: B Odd-Covering Criterion: Extra… · p. 16

Homological argument

• The homological argument identifies a facet’s mod-2 local cycle as nontrivial exactly when the generic point lies in its cone.Summing these facet contributions makes the local class nontrivial precisely when the point lies in an odd number of cones.Source: B Odd-Covering Criterion: Extra… · pp. 16–17

Certificate graph

• The certificate graph is simple, and each facet has exactly d distinct neighbors; edges labeled by a ridge form a matching with an even number of incident vertices.The matching argument uses the ridge labels and the graph’s neighbor structure.Source: C Certification Method: Extra… · p. 17

Certificate construction

• The selected basis vectors form a full-dimensional simplicial cone containing the chosen generic vector, while the assigned candidate point is a vertex of P.The proof uses T4 and T5 to establish the cone’s rank and exclude the chosen vector from other cones.Source: C Certification Method: Extra… · p. 17

Vertex-set completeness

• The odd-covering criterion makes the assigned candidate points’ normal cones cover R^d, which establishes that the candidate set contains every vertex of P.The argument applies the criterion to cones assigned to each candidate and then invokes the normal-cone coverage characterization.Source: C Certification Method: Extra… · p. 18

Vertex-edge graph certification

• Across an edge of P, the parity argument finds a certificate-graph edge linking facets assigned to the two endpoint vertices.The proof uses a generic vector in the edge’s normal cone and the ridge-boundary structure of the mod-2 chain associated with a vertex.Source: C Certification Method: Extra… · pp. 18–19
• The proof of exact vertex-edge graph certification uses T7 to conclude that a candidate adjacent in the mapped graph is the corresponding polytope neighbor.T7 is applied after comparing the active inequalities at the candidate and at a vertex on an incident edge.Source: C Certification Method: Extra… · p. 19

Perturbation

• A perturbation of the inequalities gives each perturbed vertex a simplicial normal cone refining a cone of the original polyhedron’s normal fan.The construction also verifies graph-neighbor properties for the perturbed polytope using simplex pivots.Source: C Certification Method: Extra… · p. 19

• The n-Birkhoff polytope consists of n×n doubly stochastic matrices, has dimension (n−1)^2, and has n! permutation matrices as vertices.Source: D Description of the Instances · p. 19
• The d-dimensional cross-polytope is the unit ball for the 1-norm with 2d vertices, while the d-dimensional cube [0,1]^d also has 2^d vertices.Source: D Description of the Instances · p. 20
• With n=2d, the dual cyclic polytope has exponentially many vertices and maximizes vertex count among d-dimensional polytopes with n facets.Source: D Description of the Instances · p. 20
• The (k,n)-hypersimplex consists of points in [0,1]^n whose coordinates sum to k; for 0<k<n it has dimension n−1.Source: D Description of the Instances · p. 20
• The order-n permutahedron has dimension n−1 and n! vertices, given by permutations of (1,…,n).Source: D Description of the Instances · p. 20
• The Hirsch-conjecture counterexamples are 20- and 23-dimensional polytopes defined by 40 and 46 inequalities involving very large rationals.Source: D Description of the Instances · p. 20