MeasuredPlaneComparison.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Upper growth and a lower ball-mass bound provide uniformly separated joint support anchors for two affine planes. A small joint squared fitting error then yields a quantitative comparison of the planes, with distortion controlled by the anchor span-condition constant.

theorem OAI.RieszRectifiability.exists_measured_plane_comparison_width line 19