OAI/Geometry/HyperbolicGroups/PlanarPartitionBridge.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.PlanarRecursion.CutPartition.Label line 22
2. def OAI.HyperbolicObstruction.PlanarRecursion.CutPartition.finiteLabel line 23
3. lemma OAI.HyperbolicObstruction.PlanarRecursion.CutPartition.finiteLabel_small line 27
4. theorem OAI.HyperbolicObstruction.PictureSwitch.uniform_relative_cut_partition line 47

   Source documentation

   Full uniform partition-to-multigraph-cut bridge. The required planar separator producer remains EXPLICIT in the hypothesis; this theorem proves all its downstream recursion, finite labeling and parallel-edge accounting. The cutoff is chosen before the graph, its dart type, and its active carrier.

   theorem uniform_relative_cut_partition (c : ℝ) (d : ℕ) (eta : ℝ)
       (hc : 0 ≤ c) (heta : 0 < eta) :
       ∃ K : ℕ, 0 < K ∧ ∀ (D : Type u) [Fintype D] [DecidableEq D] (M : PictureMap D),
         HasBalancedSeparators M.underlyingGraph c → ∀ 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