OAI/Analysis/RieszRectifiability/Restart/ActiveSurfaceCharts.lean

Active-cell chart predicates

Input charts parametrize a larger tangential disk and capture the surface near an active cell. Surface charts retain exact tangential coordinates on a smaller disk together with quantitative normal slope, height, and local image bounds. These predicates package the geometric data used to propagate charts through the active projection construction.