OAI/Analysis/CircleDomains/Modulus/SavedModelBarriers.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every saved source contour has an actual compact global barrier on every later finite circle model, with energy tending to zero in the saved stage. All witnesses come from the recursive construction.

  1. theorem OAI.CircleDomainRigidity.AppendingSequence.saved_model_barrier line 23