OAI/Analysis/CircleDomains/Selection/ProtrusionMeanExclusion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual marked-component protrusion and its recursive law produce an inner mean exclusion. All map regularity and distance hypotheses are derived from the conformal limit and the separated protrusion balls.

  1. theorem OAI.CircleDomainRigidity.RecursiveCodeLaw.eventually_protrusion_mean line 19