OAI/Analysis/CircleDomains/Selection/SelectableProtrusionMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual gated law at a protrusion gives a compatible selectable mean test and an open exclusion containing the original sized map--disk pair. The circuit bound comes from the fixed exterior anchor.

  1. theorem OAI.CircleDomainRigidity.RecursiveCodeLaw.exists_selectable_protrusion_mean line 21