MaskedCofiniteMetric.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Masked circle energy on a completion containing infinity

Only the closure of the tail needs smooth coordinate branches. This allows every mask boundary to stay inside the retained core, while the whole completed region may be unbounded in the finite chart.

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_spherical_metric_for_masked_cofinite_circles line 21
theorem OAI.CircleDomainRigidity.FiniteTransfer.tail_avoids_mask_boundaries line 50
Source documentation
Mask boundaries retained strictly inside the core cannot meet its tail closure. The finite union may therefore be removed from the smooth coordinate neighborhood used by the metric theorem.
```
theorem tail_avoids_mask_boundaries
    {n : ℕ} {Q K Ω : Set (ℝ × ℝ)}
    (hQΩ : Q ⊆ Ω) (M : Fin n → Set (ℝ × ℝ))
    (hboundary : ∀ i, frontier (M i) ⊆ interior K) :
    Q ∩ closure Kᶜ ⊆ Ω \ ⋃ i, frontier (M i) := by
…
```