Sunflower plucking for clique approximators

A bounded-width clique approximator is a finite family of vertex sets. A sunflower pluck removes all petals and inserts their common core. This can only enlarge the accepted graph set, and it strictly decreases the number of terms when there are at least two petals.

Repeated plucking therefore terminates. The resulting normal form has at most Sunflower.bound petals width terms, and the number of plucks is at most the cardinality of the starting family.

@[reducible, inline]

abbrev Algebraic.Monotone.Clique.Plucking.Family (n : ℕ) : Type

A finite family of finite vertex sets.

Equations

• Algebraic.Monotone.Clique.Plucking.Family n = Finset (Finset (Fin n))

def Algebraic.Monotone.Clique.Plucking.Bounded {n : ℕ} (width : ℕ) (family : Family n) : Prop

A family is a bounded-width clique DNF.

Equations

• Algebraic.Monotone.Clique.Plucking.Bounded width family = ∀ set ∈ family, set.card ≤ width

structure Algebraic.Monotone.Clique.Plucking.Step {n : ℕ} (petalCount : ℕ) (before after : Family n) : Type

One sunflower replacement.

• petals : Family n

  The sunflower terms removed by this step.

• core : Finset (Fin n)

  The common core inserted by this step.

• petals_subset : self.petals ⊆ before

  Every removed petal belonged to the starting family.

• petals_card : Finset.card self.petals = petalCount

  The selected sunflower has the requested number of petals.

• sunflower : Sunflower.IsSunflowerWithCore self.petals self.core

  Distinct selected petals have exactly the recorded core in common.

• result : after = insert self.core (before \ self.petals)

  The result removes all petals and inserts their core.

theorem Algebraic.Monotone.Clique.Plucking.core_subset_of_sunflower {n petalCount : ℕ} (two_le : 2 ≤ petalCount) {petals : Family n} {core petal : Finset (Fin n)} (petalsCard : Finset.card petals = petalCount) (sunflower : Sunflower.IsSunflowerWithCore petals core) (present : petal ∈ petals) : core ⊆ petal

A sunflower core lies in each petal when there are at least two petals.

theorem Algebraic.Monotone.Clique.Plucking.Step.card_lt {n petalCount : ℕ} (two_le : 2 ≤ petalCount) {before after : Family n} (step : Step petalCount before after) : Finset.card after < Finset.card before

One pluck strictly reduces family cardinality.

theorem Algebraic.Monotone.Clique.Plucking.Step.bounded {n petalCount : ℕ} (two_le : 2 ≤ petalCount) {before after : Family n} (step : Step petalCount before after) {width : ℕ} (bounded : Bounded width before) : Bounded width after

Bounded width is preserved by one pluck.

theorem Algebraic.Monotone.Clique.Plucking.Step.acceptance_mono {n petalCount : ℕ} (two_le : 2 ≤ petalCount) {before after : Family n} (step : Step petalCount before after) {assignment : Fin (edgeCount n) → Bool} (accepted : ∃ set ∈ before, Contains assignment set) : ∃ set ∈ after, Contains assignment set

A pluck preserves every graph accepted by the starting family.

inductive Algebraic.Monotone.Clique.Plucking.Reduction (petalCount : ℕ) {n : ℕ} : ℕ → Family n → Family n → Prop

A proof-relevant sequence of exactly steps plucks.

• refl {petalCount n : ℕ} (family : Family n) : Reduction petalCount 0 family family
• step {petalCount n : ℕ} {before middle after : Family n} {steps : ℕ} : ∀ (a : Step petalCount before middle), Reduction petalCount steps middle after → Reduction petalCount (steps + 1) before after

theorem Algebraic.Monotone.Clique.Plucking.Reduction.steps_le_card {n petalCount : ℕ} (two_le : 2 ≤ petalCount) {steps : ℕ} {before after : Family n} (reduction : Reduction petalCount steps before after) : steps ≤ Finset.card before

A reduction has at most one step per starting term.

theorem Algebraic.Monotone.Clique.Plucking.Reduction.bounded {n petalCount : ℕ} (two_le : 2 ≤ petalCount) {steps : ℕ} {before after : Family n} (reduction : Reduction petalCount steps before after) {width : ℕ} (bounded : Bounded width before) : Bounded width after

Bounded width is preserved throughout a reduction.

theorem Algebraic.Monotone.Clique.Plucking.Reduction.acceptance_mono {n petalCount : ℕ} (two_le : 2 ≤ petalCount) {steps : ℕ} {before after : Family n} (reduction : Reduction petalCount steps before after) {assignment : Fin (edgeCount n) → Bool} (accepted : ∃ set ∈ before, Contains assignment set) : ∃ set ∈ after, Contains assignment set

Acceptance is monotone throughout a reduction.

theorem Algebraic.Monotone.Clique.Plucking.exists_terminal {n : ℕ} (petalCount : ℕ) (two_le : 2 ≤ petalCount) (family : Family n) : ∃ (steps : ℕ) (terminal : Family n), Reduction petalCount steps family terminal ∧ ¬Sunflower.ContainsSunflower petalCount terminal

Every finite family reduces to a sunflower-free family.

noncomputable def Algebraic.Monotone.Clique.Plucking.normalize {n : ℕ} (petalCount : ℕ) (two_le : 2 ≤ petalCount) (family : Family n) : Family n

A chosen terminal sunflower-free normal form.

Equations

• Algebraic.Monotone.Clique.Plucking.normalize petalCount two_le family = Classical.choose ⋯

noncomputable def Algebraic.Monotone.Clique.Plucking.normalizeSteps {n : ℕ} (petalCount : ℕ) (two_le : 2 ≤ petalCount) (family : Family n) : ℕ

Number of plucks in the chosen normalization.

Equations

• Algebraic.Monotone.Clique.Plucking.normalizeSteps petalCount two_le family = Classical.choose ⋯

theorem Algebraic.Monotone.Clique.Plucking.reduction_normalize {n : ℕ} (petalCount : ℕ) (two_le : 2 ≤ petalCount) (family : Family n) : Reduction petalCount (normalizeSteps petalCount two_le family) family (normalize petalCount two_le family)

The chosen normal form comes with a reduction certificate.

theorem Algebraic.Monotone.Clique.Plucking.normalize_sunflowerFree {n : ℕ} (petalCount : ℕ) (two_le : 2 ≤ petalCount) (family : Family n) : ¬Sunflower.ContainsSunflower petalCount (normalize petalCount two_le family)

The chosen normal form is sunflower-free.

theorem Algebraic.Monotone.Clique.Plucking.normalizeSteps_le_card {n : ℕ} (petalCount : ℕ) (two_le : 2 ≤ petalCount) (family : Family n) : normalizeSteps petalCount two_le family ≤ Finset.card family

Normalization uses at most one pluck per starting term.

theorem Algebraic.Monotone.Clique.Plucking.normalize_bounded {n : ℕ} (petalCount : ℕ) (two_le : 2 ≤ petalCount) (family : Family n) {width : ℕ} (bounded : Bounded width family) : Bounded width (normalize petalCount two_le family)

Normalization preserves bounded width.

theorem Algebraic.Monotone.Clique.Plucking.normalize_card_le {n : ℕ} (petalCount : ℕ) (two_le : 2 ≤ petalCount) (family : Family n) {width : ℕ} (bounded : Bounded width family) : Finset.card (normalize petalCount two_le family) ≤ Sunflower.bound petalCount width

A bounded normal form has at most the elementary sunflower bound many terms.

theorem Algebraic.Monotone.Clique.Plucking.normalize_acceptance_mono {n : ℕ} (petalCount : ℕ) (two_le : 2 ≤ petalCount) (family : Family n) {assignment : Fin (edgeCount n) → Bool} (accepted : ∃ set ∈ family, Contains assignment set) : ∃ set ∈ normalize petalCount two_le family, Contains assignment set

Normalization preserves acceptance.