OAI/Analysis/RieszRectifiability/Restart/OriginalADUniformRestartSurfacePieces.lean

Uniform surface pieces at restart roots

Uniform surface ball charts for an AD-regular measure furnish selected surface data at every bad-beta restart root. The flatness threshold is fixed before the loss tolerance, and the chart Lipschitz bound is shared across all roots. Core admissibility passes to descendants, allowing the local chart's weighted Hausdorff-measure loss estimate to supply HasUniformRestartSurfacePieces.