The six-point bound for the planar density threshold

This file contains the analytic bridge from the finite six-point property to the upper bound on the planar rectifiability threshold. The finite property itself remains the sole geometric input.

theorem LeanPool.Besicovitch.BesicovitchPairCondition.sigmaOne_plane_le {s : ℝ} (hpair : BesicovitchPairCondition s) (hs : 0 < s) (hs_one : s < 1) : sigmaOne (EuclideanSpace ℝ (Fin 2)) ≤ s

A positive subunit parameter satisfying the Besicovitch pair condition bounds the planar rectifiability threshold.

theorem LeanPool.Besicovitch.SixPointFiniteProperty.forcesOneRectifiability_of_gt {s : ℝ} (hfinite : SixPointFiniteProperty s) (hs : 0 < s) (hs_one : s < 1) {gamma : ℝ} (hs_gamma : s < gamma) : ForcesOneRectifiability (EuclideanSpace ℝ (Fin 2)) (ENNReal.ofReal gamma)

The finite six-point property at a positive subunit parameter forces one-rectifiability at every larger threshold.

theorem LeanPool.Besicovitch.SixPointFiniteProperty.sigmaOne_plane_le {s : ℝ} (hfinite : SixPointFiniteProperty s) (hs : 0 < s) (hs_one : s < 1) : sigmaOne (EuclideanSpace ℝ (Fin 2)) ≤ s

The finite six-point property at a positive subunit parameter bounds the planar rectifiability threshold by that parameter.

theorem LeanPool.Besicovitch.sigmaOne_plane_le_barS_of_sixPointFiniteProperty (hfinite : SixPointFiniteProperty barS) : sigmaOne (EuclideanSpace ℝ (Fin 2)) ≤ barS

The desired planar bound follows from the finite six-point property at the certified endpoint.