OAI/Analysis/CircleDomains/Topology/LocalPlaneCorrection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A physical smoothing error on a finite quotient chart descends to a bounded correction. Its dust-distance tolerance forces it to vanish at every dust point, including along approaches from other charts.

  1. theorem OAI.CircleDomainRigidity.exists_local_plane_correction line 20