OpenMeanCorrection.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Construct the single-valued quotient correction from the actual physical smoothing. The tolerance and all dust limits are derived here.

theorem OAI.CircleDomainRigidity.exists_open_mean_circle_correction line 19