Projection-body volume for four-dimensional polytopes with at most six facets

For every convex four-dimensional polytope K with nonempty interior and at most six actual facets, we prove V_4(ΠK) ≤ (160/3)V_4(K)^3, with equality precisely for simplices. The projection body is normalized by h_{ΠK}(u) = V_3(K projected onto u-perpendicular) for unit u. Under the identified stipulated source interfaces, an attained simplex-section maximum reduces the six-facet case to a signed sum of four independent exponential variables. Log-concavity and Laplace comparison and a two-bracket identity reduce the estimate to ten explicit polynomial certificates. Repeated knots, zero coefficients and nonsimple polytopes are included. No claim is made for seven or more facets, general four-dimensional bodies or dimensions five through eight.

AI-assisted preprint by Myeongjin Kang, with no affiliation. Internal AI review is not external journal peer review or worldwide-priority certification. Identified OpenAI source inputs at revision fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb are stipulated true. Lean verifies scoped supporting results only, not the full theorem. Original prose: CC BY 4.0; original code and Lean: MIT; third-party rights preserved. See the supporting archive for precise assumptions, coverage, provenance and corrections.