OAI/Analysis/CircleDomains/Topology/NestedCollarMeanExclusion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A single physical chart bound works throughout the nested collars. The actual recursive law then supplies the small compact law at every sufficiently deep collar, with the prescribed start gate and the resulting mean exclusion.

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