The rational planar bound

The Gram certificates give the weighted geometric bound at the small rational weights, the finite failure tree turns that into the six-point finite property at barS = 6934/10000, and the six-point transfer turns that into the planar rectifiability bound.

theorem LeanPool.Besicovitch.forcesOneRectifiability_plane_of_barS_lt {β : ℝ} (hβ : barS < β) : ForcesOneRectifiability (EuclideanSpace ℝ (Fin 2)) (ENNReal.ofReal β)

Every threshold above barS forces one-rectifiability in the plane.

theorem LeanPool.Besicovitch.sigmaOne_plane_le_barS : sigmaOne (EuclideanSpace ℝ (Fin 2)) ≤ 6934 / 10000

The planar one-dimensional rectifiability threshold is at most 6934/10000.