Sticky Kakeya theorem in four dimensions

Open

StickyKakeya4.sticky_kakeya_four_dimensional

by sensei · Sep 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

contact-geometrygeometric-measure-theorykakeya

Let $\Gamma$ be a compact full-direction family of valid marked oriented lines in $\mathbb R^4$ whose unmarked carrier has packing dimension $3$ . Then the union of its marked unit segments has full Hausdorff dimension:

\dim_{\mathrm H}K_\Gamma=4.

The proof interface factors through the Borel selector reduction and the corrected Borel selector closure.

Preamble

import Definitions.Def_sticky_kakeya4_core

open MeasureTheory Set

Formal statement

namespace StickyKakeya4

theorem sticky_kakeya_four_dimensional (lines : Set MarkedLine)
    (hsticky : IsStickyDatum lines) :
    dimH (unitFront lines) = 4 := by sorry

end StickyKakeya4

Source

Chenxi Cai, source manuscript https://cchx0000.github.io/papers/sticky-kakeya-contact-symplectic/sticky-kakeya-contact-symplectic.pdf, Theorem 1.2.

Read-back

What the Lean code literally says, in plain math · gpt-5

For every set $L$ of marked lines $\ell=((v_\ell,a_\ell),m_\ell)$ in $\mathbb R^4$ , assume that $L$ is compact; every $\ell\in L$ satisfies $\lVert v_\ell\rVert=1$ and $\langle a_\ell,v_\ell\rangle=0$ ; and every unit vector $\theta\in\mathbb R^4$ is the direction of at least one member of $L$ , with no uniqueness requirement. Also assume that the custom packing dimension of the unmarked carrier $\mathcal C_L=\{(v_\ell,a_\ell):\ell\in L\}$ is exactly $3$ . This packing dimension is the infimum of all $d\in[0,\infty]$ for which $\mathcal C_L$ is contained in a countable union of sets of custom upper Minkowski dimension at most $d$ ; upper Minkowski dimension is the infimum of finite $q\in[0,\infty]$ admitting a finite $K\in[0,\infty]$ such that, for all sufficiently small $r>0$ , the finite open-ball covering number satisfies $N(S,r)\le K(\operatorname{ofReal}r)^{-q_{\mathbb R}}$ . Under these hypotheses, the Hausdorff dimension of

F_L=\{a_\ell+(m_\ell+t)v_\ell:\ell\in L,-\tfrac12\le t\le\tfrac12\}

is exactly $4$ .

View graph