Papers With

← All papers
First page of Integrality, smoothness and normality bounds for cube-truncated Hadamard simplices

Integrality, smoothness and normality bounds for cube-truncated Hadamard simplices

Nikita Lebedev

math.CO Sep 26, 2026 · v1 math.MG
formalization combinatorics geometry
Read PDF arXiv abstract Code
TL;DR
A Lean 4 companion (using Mathlib) formally verifies all 17 numbered results on integrality, smoothness, and normality of cube-truncated Hadamard simplices.
Abstract
Santos asked when intersections of dilated Hadamard simplices with cubes are integral, smooth, or normal, in a prescribed affine lattice. We construct a nonintegral example in dimension eleven and prove that no smaller-dimensional example exists. We characterize smoothness completely and show that every smooth member of this family is normal. An explicit example in dimension fifteen shows that integrality alone does not imply normality. For Sylvester simplices of order at least sixteen, we establish a sharp uniform integrality bound and construct counterexamples immediately below it. We also obtain sufficient normality bounds for general Hadamard simplices and stronger bounds for the Sylvester family. The proofs use integer decomposition for boxes with separated corner cuts and rounding under three signed slab constraints. All numbered results have formal counterparts verified in Lean.
Problem

Santos asked when intersections of dilated Hadamard simplices with cubes are integral, smooth, or normal within a prescribed affine lattice, relevant to Oda's normality conjecture. The behavior of these cube-truncated Hadamard simplices across parameters was not fully classified.

Approach

The authors construct explicit examples and prove structural results about corner-cut boxes with strictly separated corners, establishing integrality and the integer decomposition property. They use integer decomposition and rounding arguments under signed slab constraints, including a three-slab feasibility lemma based on half-integral inverses of small sign matrices. All numbered results have formal counterparts verified in Lean 4 (Mathlib commit 5ed29652), covering polytopes, affine lattices, facet normals, and decomposition degrees.

Results

A nonintegral Hadamard simplex example exists in dimension eleven and none smaller. Smoothness is characterized completely, every smooth member is normal, and integrality alone does not imply normality (dimension-fifteen example). For Sylvester simplices of order at least sixteen, a sharp uniform integrality bound is established with counterexamples just below it.