PackingOptions.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Soundness of the manuscript's weighted packing test. Radius index zero denotes a singleton; index r+1 denotes its exterior radius-r ball.

def OAI.CycleClique.Construction.packingRegion line 13
def OAI.CycleClique.Construction.PackingCompatible line 18
theorem OAI.CycleClique.Construction.PackingCompatible.symm line 23

theorem OAI.CycleClique.Construction.packingRegions_separated line 39

Source documentation

Compatibility gives both vertex disjointness and anticompleteness, with the singleton case handled separately from positive intervals.

theorem packingRegions_separated {G : SimpleGraph V} {X : Finset V} {x y : V} {r s : ℕ}
    (hx : x ∈ X) (hy : y ∈ X) (hxy : x ≠ y)
    (hcompat : PackingCompatible G (X : Set V) x r y s) :
    Disjoint (packingRegion G X x r) (packingRegion G X y s) ∧
    ∀ u ∈ packingRegion G X x r, ∀ v ∈ packingRegion G X y s, ¬ G.Adj u v := by
…

Mentions: OAI.CycleClique.Construction.PackingCompatible, OAI.CycleClique.Construction.packingRegion

theorem OAI.CycleClique.Construction.packing_test line 114

Source documentation

The weights of every compatible family with distinct bases sum to at most the ambient independence bound.

theorem packing_test {ι : Type*} [Fintype ι] {G : SimpleGraph V} {k : ℕ}
    (hbound : IndependenceBound G k) (X : Finset V)
    (base : ι → V) (radius weight : ι → ℕ)
    (hbase : Function.Injective base) (hX : ∀ i, base i ∈ X)
    (hweight : ∀ i, HasIndependent (G.induce (packingRegion G X (base i) (radius i) : Set V))
      (weight i))
    (hcompat : ∀ i j, i ≠ j →
      PackingCompatible G (X : Set V) (base i) (radius i) (base j) (radius j)) :
    ∑ i, weight i ≤ k := by
…

Mentions: OAI.CycleClique.Construction.IndependenceBound, OAI.CycleClique.Construction.HasIndependent, OAI.CycleClique.Construction.packingRegion, OAI.CycleClique.Construction.PackingCompatible