OAI/Analysis/RieszRectifiability/Restart/ActiveRegionHighMatchedProjection.lean

Matched projections above the first stopping scale

When the stopping scale is at least the first descendant scale, the root plane provides both a quantitative forward flatness bound and a projected disk in a small ball of the limit surface. The argument uses finite-stage stabilization and residual estimates for a transported affine-plane chart.