一句话：在 Coq 中首次形式化多面体的面，证明面构成分级原子/余原子格并验证 Balinski 定理。
面在多面体的组合与计算性质中处于核心地位，但此前缺乏在证明助手中的形式化。本文在 Coq 中首次形式化多面体的面，工作建立在已有 Coq 多面体库之上，该库提供投影、凸包、线性映射像等基本构造与操作。作者还设计了一种特殊机制，可根据证明上下文自动引入多面体或面的合适表示，提升形式化可用性。借助该框架，作者证明了若干最重要的面组合性质：面构成一族分级、原子且余原子的格，并在区间子格下封闭；此外还形式化了 Balinski 关于 d 维多胞体邻接图 d-连通性的定理。
Faces play a central role in the combinatorial and computational aspects of polyhedra. In this paper, we present the first formalization of faces of polyhedra in the proof assistant Coq. This builds on the formalization of a library providing the basic constructions and operations over polyhedra, including projections, convex hulls and images under linear maps. Moreover, we design a special mechanism which automatically introduces an appropriate representation of a polyhedron or a face, depending on the context of the proof. We demonstrate the usability of this approach by establishing some of the most important combinatorial properties of faces, namely that they constitute a family of graded atomistic and coatomistic lattices closed under interval sublattices. We also prove a theorem due to Balinski on the $d$-connectedness of the adjacency graph of polytopes of dimension $d$.
@article{paperbot1701,
title = {Formalizing the Face Lattice of Polyhedra},
author = {Xavier Allamigeon and Ricardo D. Katz and Pierre-Yves Strub},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 2},
year = {2022},
doi = {10.46298/lmcs-18(2:10)2022}
}