PictureFullSeparator.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.genusZero_component_separator line 25

Source documentation

Uniform planar separator for an arbitrary (possibly empty or disconnected) literal genus-zero rotation system and every vertex carrier. All genus, component, radius, triangulation and tree obligations are proved.

theorem genusZero_component_separator (hG : M.GenusZero) (U : Finset M.GraphVertex) :
    ∃ S : Finset M.GraphVertex, S ⊆ U ∧ S.card ≤ 11*Nat.sqrt U.card ∧
      ∀ W : Finset M.GraphVertex, W ⊆ U → Disjoint W S →
        (M.underlyingGraph.induce (W : Set M.GraphVertex)).Preconnected →
        2*W.card ≤ U.card :=
…

theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.genusZero_balanced_separators line 34
Source documentation
The actual Lipton--Tarjan-style input required by the manuscript's recursive partition proof, proved from its finite genus-zero maps.
```
theorem genusZero_balanced_separators (hG : M.GenusZero) :
    HasBalancedSeparators M.underlyingGraph 11 :=
…
```

theorem OAI.HyperbolicObstruction.PictureSwitch.uniform_genusZero_cut_partition line 48

Source documentation

The planar-multigraph partition producer. K is chosen before EVERY finite dart type, genus-zero map and active carrier. The exact multigraph cut cost is retained, including loops/parallel copies and an arbitrary-degree protected exterior.

theorem uniform_genusZero_cut_partition (d : ℕ) (eta : ℝ) (heta : 0 < eta) :
    ∃ K : ℕ, 0 < K ∧ ∀ (D : Type u) [Fintype D] [DecidableEq D] (M : PictureMap D),
      M.GenusZero → ∀ U : Finset M.GraphVertex,
      (∀ v ∈ U, Nat.card {x : D // M.vertexClass x = v} ≤ d) →
      ∃ (I : Type) (_ : Fintype I) (part : M.GraphVertex → I),
        (∀ i, (U.filter (fun x => part x = i)).card ≤ K) ∧
        (Fintype.card (RelativeCutContact M (fun x => M.vertexClass x ∈ U)
          (part ∘ M.vertexClass)) : ℝ) ≤ eta * U.card := by
…

Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap, OAI.HyperbolicObstruction.PictureSwitch.RelativeCutContact