An orthogonality inequality in $\mathbb{RP}^{n-1}$ and the double-cap conjecture
Allen Ibiapina, Carlos Gomes, Alan Pio, Samuel Belo, Ernandes Ferreira
math.MG
Oct 20, 2026 · v1
TL;DR
The main neighborhood inequality and double-cap theorem, with rigidity, are machine-checked in Lean 4 (LeanShadow repository) via a different, largely AI-assisted proof.
Abstract
The orthogonal neighborhood of a set in real projective space is the union of the hyperplanes perpendicular to its points. We prove that caps minimize neighborhood measure among measurable sets of fixed measure in $\mathbb{RP}^{n-1}$, for $n \geq 3$, with rigidity up to null sets. This yields the double-cap conjecture: a measurable subset of $S^{n-1}$ containing no orthogonal pair has measure at most that of two opposite open caps of radius $π/4$. The argument combines compactness of the Funk transform, rotation comparisons, and projective variations. We also obtain qualitative stability and determine the measurable fractional chromatic number of the spherical orthogonality graph. AI played an assistive role in preparing this paper. The formalization and verification workflow for a separate Lean 4 proof of the main inequality and double-cap result, based on a different argument, were carried out almost entirely using AI-assisted tools.
Problem
The orthogonal neighborhood of a set in real projective space is the union of the hyperplanes perpendicular to its points. The question is whether caps minimize neighborhood measure among all measurable sets of fixed measure. A positive answer would settle Witsenhausen's double-cap conjecture on orthogonal-pair-free subsets of the sphere.
Approach
The paper proves the neighborhood inequality in RP^{n-1} for n >= 3. It uses compactness of the Funk transform to obtain optimal avoiding pairs, then constrains these pairs through rotation comparisons and first- and second-order projective variations. Density-one representatives handle null-set subtleties. A separate Lean 4 formalization, based on a different argument and produced with AI-assisted tools, machine-checks the main inequality and the double-cap result.
Results
Caps minimize neighborhood measure, with rigidity up to null sets. A measurable subset of S^{n-1} with no orthogonal pair has measure at most that of two opposite caps of radius π/4. Further results are qualitative stability, sharp bounds for avoiding pairs, and the measurable fractional chromatic number of the orthogonality graph.
