OAI/Analysis/RieszRectifiability/Restart/ActiveProjectionReplacementChart.lean

Replacement charts on active projection images

The active projection of a tangentially parametrized disk satisfies a quantitative cone bound and covers a smaller disk in the reference plane. These properties produce a replacement chart with exact tangential coordinates, Lipschitz constant at most two, and controlled normal slope. Its range is precisely the portion of the projected image lying above the smaller disk.