Borel contact-symplectic selector closure in four dimensions

Open

StickyKakeya4.selector_closure

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

contact-geometrygeometric-measure-theorykakeya

Every Borel set of valid marked lines that selects exactly one line in each unit direction and whose unmarked carrier has packing dimension $3$ has a unit front of Hausdorff dimension $4$ .

The Borel formulation is the composable closure interface: it matches the selector reduction and is obtained through finite-scale source extraction, the uniform source-hereditary estimate, and the Frostman upgrade.

Preamble

import Definitions.Def_sticky_kakeya4_core

open MeasureTheory Set

Formal statement

namespace StickyKakeya4

theorem selector_closure (selector : Set MarkedLine)
    (hmeasurable : MeasurableSet selector)
    (hvalid : ∀ line ∈ selector, IsValidLine line)
    (hselector : IsDirectionSelector selector)
    (hpacking : packingDim (lineCarrier selector) = 3) :
    dimH (unitFront selector) = 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 9.32 read together with Proposition 3.1 and the exact-selector formulation; Borel wording is the interface correction required by that reduction.

Read-back

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

For every measurable set $S$ of marked lines $(\theta,b,m)\in\mathbb R^4\times\mathbb R^4\times\mathbb R$ , assume that every member satisfies $\|\theta\|=1$ and $\langle b,\theta\rangle=0$ ; for every unit $\theta\in\mathbb R^4$ there exists a unique member of $S$ with that direction; and the custom packing dimension of the unmarked carrier $\{(\theta,b):\exists m,(\theta,b,m)\in S\}$ is exactly $3$ . Here packing dimension is the infimum of all $d\in[0,\infty]$ for which the carrier is covered by countably many sets whose custom upper Minkowski dimensions are at most $d$ , with upper Minkowski dimension defined through finite open-ball covering numbers at all sufficiently small positive radii. Then the Hausdorff dimension of

\{b+(m+t)\theta:(\theta,b,m)\in S,-\tfrac12\le t\le\tfrac12\}

is exactly $4$ .

View graph