How tight is the four-hyperplane counterexample? Exact bounds for its polynomial system

Abstract

Soberón has settled the last open case of Grünbaum's 1960 equipartition problem by producing a mass in ℝ⁴ that no four hyperplanes equipartition. The computational core of that proof is a system of five polynomials f₀,…,f₄ in six variables, of degree at most 4 in each variable, attached to a quaternionic chart of SO(4): what the theorem needs is exactly that the five have no common zero on the box Q=[-1,1]⁶, and the source proves this with a subdivision certificate of 38 857 dyadic boxes checked in fixed-point interval arithmetic. We study that polynomial system as an object in its own right. First, the nonvanishing is re-verified in exact integer arithmetic inside a formal proof: the passage from the certificate to the conclusion — the power-to-Bernstein change of basis, de Casteljau subdivision, and the convexity bound on a box — is machine-checked, and the only thing computed rather than proved is the sign of 38 857 · 5⁶=607 140 625 integers. Second, we determine the size of the system: sup_(Q)absfₛ=3064 exactly for s=0,1,2,3, attained at explicit corners of Q, and sup_(Q)absf₄ ≤ 1440. The two constants are the exact maxima of the Bernstein coefficient arrays of the fₛ on Q; for f₄, and only for f₄, that bound is not attained, and its sup norm is left open. Third, with S=(3064,3064,3064,3064,1440) we show that the nonvanishing is tight: inf_(z ∈ Q) max_(0 ≤ s ≤ 4) absfₛ(z)/Sₛ ≤ 1/3064 ≈ 3.26 · 10⁻⁴, the value at the origin of the chart, where the five values are (-1,0,0,0,0). No point of {-1,0,1}⁶ does better, and unformalised searches get no further than 1/3187, so the constant is within about 4 zero by about three parts in ten thousand of its own scale — which is why a subdivision proof of it cannot be small. Every theorem and proposition here is machine-checked in Lean 4; the searches that calibrate the constant are not, and are labelled where they occur.

Open review

This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.

Archived files

1. Version 1 · current (opens in a new tab)

   Source snapshot 2026-08-30 15:34 UTC

   File fingerprint

   7f7885b169c4f0f13b18c8ffa12c5aa699214e8983fec367796030e054f89876