CutoffCore.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The physical core containing the entire cutoff transition

Taking the complement of the open one-plateau of the cutoff gives a compact spherical subset of the original domain. Choosing all disk closures off this larger core guarantees genuine staircase collars.

def OAI.CircleDomainRigidity.FiniteTransfer.realChartDomain line 20
theorem OAI.CircleDomainRigidity.FiniteTransfer.isOpen_realChartDomain line 23
theorem OAI.CircleDomainRigidity.FiniteTransfer.isCompact_compl_realChartDomain line 26
theorem OAI.CircleDomainRigidity.FiniteTransfer.sphericalCore_mono line 31
def OAI.CircleDomainRigidity.FiniteTransfer.cutoffCore line 38
theorem OAI.CircleDomainRigidity.FiniteTransfer.isCompact_cutoffCore line 41
theorem OAI.CircleDomainRigidity.FiniteTransfer.infty_mem_cutoffCore line 44
theorem OAI.CircleDomainRigidity.FiniteTransfer.cutoffCore_subset_domain line 47
theorem OAI.CircleDomainRigidity.FiniteTransfer.sphericalCore_subset_cutoffCore line 60
theorem OAI.CircleDomainRigidity.FiniteTransfer.boundary_in_one_plateau_of_disjoint_cutoffCore line 70
Source documentation
A filling closure off the cutoff core has its whole boundary in the open region where the modification is exactly the staircase.
```
theorem boundary_in_one_plateau_of_disjoint_cutoffCore
    (H : ℂ ≃ₜ ℂ) (χ : (ℝ × ℝ) → ℝ)
    (hdisj : Disjoint (((↑) : ℂ → Sphere) '' closure (jordanInterior H)) (cutoffCore χ)) :
    ∀ z ∈ frontier (jordanInterior H), Complex.equivRealProdCLM z ∈ interior {x | χ x = 1} := by
…
```
Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.jordanInterior, OAI.CircleDomainRigidity.FiniteTransfer.cutoffCore