The pair condition forces rectifiability

The Besicovitch pair condition rules out a positive straight purely unrectifiable set whose lower density is strictly above the pair-condition parameter.

theorem LeanPool.Besicovitch.BesicovitchPairCondition.forcesOneRectifiability {sigma gamma : ℝ} (hpairCondition : BesicovitchPairCondition sigma) (hsigma : 0 < sigma) (hsigma_one : sigma < 1) (hsigma_gamma : sigma < gamma) : ForcesOneRectifiability (EuclideanSpace ℝ (Fin 2)) (ENNReal.ofReal gamma)

The Besicovitch pair condition at sigma < 1 forces rectifiability at every strictly larger density threshold.