The planar threshold is at least 1/2

Besicovitch's set Π, the graph of g over [0, 1], is measurable and has positive finite length. It is purely unrectifiable: a Lipschitz curve meeting it in positive length would make g Lipschitz on a set of positive Lebesgue measure (LeanPool.Besicovitch.Example.Reduction), which is impossible (LeanPool.Besicovitch.Example.Zero). On the other hand its lower one-density is at least 1/2 at every interior point (LeanPool.Besicovitch.Example.LowerDensity), hence almost everywhere. So no threshold below 1/2 forces one-rectifiability in the plane, and sigmaOne ℝ² ≥ 1/2.

theorem LeanPool.Besicovitch.Example.hausdorffMeasure_besicovitchSet_pos : 0 < (MeasureTheory.Measure.hausdorffMeasure 1) besicovitchSet

Besicovitch's set has positive length.

theorem LeanPool.Besicovitch.Example.hausdorffMeasure_besicovitchSet_lt_top : (MeasureTheory.Measure.hausdorffMeasure 1) besicovitchSet < ⊤

Besicovitch's set has finite length.

theorem LeanPool.Besicovitch.Example.hausdorffMeasure_range_inter_besicovitchSet {K : NNReal} {f : ℝ → Plane} (hf : LipschitzWith K f) : (MeasureTheory.Measure.hausdorffMeasure 1) (Set.range f ∩ besicovitchSet) = 0

A Lipschitz curve meets Besicovitch's set in a null set.

theorem LeanPool.Besicovitch.Example.not_isCountablyOneRectifiable_besicovitchSet : ¬IsCountablyOneRectifiable besicovitchSet

Besicovitch's set is not countably one-rectifiable.

theorem LeanPool.Besicovitch.Example.ae_one_half_le_lowerOneDensity : ∀ᵐ (p : Plane) ∂(MeasureTheory.Measure.hausdorffMeasure 1).restrict besicovitchSet, ENNReal.ofReal (1 / 2) ≤ lowerOneDensity besicovitchSet p

Almost every point of Besicovitch's set has lower density at least 1/2.

theorem LeanPool.Besicovitch.Example.not_forcesOneRectifiability_of_lt_half {β : ℝ} (hβ : β < 1 / 2) : ¬ForcesOneRectifiability (EuclideanSpace ℝ (Fin 2)) (ENNReal.ofReal β)

No threshold below 1/2 forces one-rectifiability in the plane.

theorem LeanPool.Besicovitch.Example.one_half_le_sigmaOne_plane : 1 / 2 ≤ sigmaOne (EuclideanSpace ℝ (Fin 2))

The planar threshold is at least 1/2.