Three theorems, with computer-aided proofs, on three-dimensional faces and quotients of polytopes (Q1580762)

The authors prove three theorems: 1. There is a finite list of three-dimensional polytopes such that every rational 9-polytope contains a three-dimensional face in the list. 2. Every nine-dimensional polytope has the three-dimensional simplex as a quotient. 3. Every 5-polytope contains a three-dimensional quotient with at most eight vertices. The proof relies on the computer program FLAGTOOL which computes all (known) relations between the flag numbers of general \(d\)-polytopes for small dimensions.