Besicovitchs-1-2
For a Borel set $E\subset\mathbb{R}^2$ of finite length, the lower density $\Theta^1_*(E,x)=\liminf_{r\downarrow0}\mathcal{H}^1(E\cap B(x,r))/2r$ records how much of $E$ a small ball around $x$ sees. If the lower density is large enough at almost every point, $E$ is forced to be countably $1$-rectifiable, and $\sigma_1(\mathbb{R}^2)$ denotes the smallest threshold for which that is true. Besicovitch's $1/2$-conjecture, still open, is that this threshold is exactly $\tfrac12$.
This is a machine-checked proof that $\tfrac12\le\sigma_1(\mathbb{R}^2)\le 0.6934$.
registered Palomar PALOMAR-2026-09-02-000011
Everything else is on GitHub.