OAI/Analysis/CircleDomains/Topology/ModelOuterCutoff.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A fixed target cutoff changes a source barrier only where the saved outer collar already vanishes. The sharper exterior remainder gives a nonempty transition annulus, independent of the finite test list.

  1. theorem OAI.CircleDomainRigidity.CompactScalarModel.exterior_decay_bound line 16
  2. theorem OAI.CircleDomainRigidity.CompactScalarModel.exterior_half_bound line 38
  3. theorem OAI.CircleDomainRigidity.CompactScalarModel.cutoff_preserves_inner_barrier line 47