Bounded-width clique approximators

An approximator is a finite disjunction of clique indicators. OR takes the union of term families. AND replaces a pair of clique indicators by the clique on their combined nontrivial vertex sets; terms wider than width are discarded, and the result is sunflower-normalized.

The special cases in joinTerms identify zero- and one-vertex indicators with the Boolean constant true. This is essential: blindly adjoining a singleton to another term would introduce edges that were not present in the conjunction.

@[reducible, inline]

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

A finite family of clique-indicator vertex sets.

Equations

• Algebraic.Monotone.Clique.Approx.Family n = Algebraic.Monotone.Clique.Plucking.Family n

def Algebraic.Monotone.Clique.Approx.Accepts {n : ℕ} (family : Family n) (assignment : Fin (edgeCount n) → Bool) : Prop

A clique DNF accepts a graph when one of its terms is contained.

Equations

• Algebraic.Monotone.Clique.Approx.Accepts family assignment = ∃ vertices ∈ family, Algebraic.Monotone.Clique.Contains assignment vertices

@[instance_reducible]

noncomputable instance Algebraic.Monotone.Clique.Approx.instDecidableAccepts {n : ℕ} (family : Family n) (assignment : Fin (edgeCount n) → Bool) : Decidable (Accepts family assignment)

Equations

• Algebraic.Monotone.Clique.Approx.instDecidableAccepts family assignment = Classical.propDecidable (Algebraic.Monotone.Clique.Approx.Accepts family assignment)

noncomputable def Algebraic.Monotone.Clique.Approx.decode {n : ℕ} (family : Family n) (assignment : Fin (edgeCount n) → Bool) : Bool

Boolean semantics of a clique DNF.

Equations

• Algebraic.Monotone.Clique.Approx.decode family assignment = decide (Algebraic.Monotone.Clique.Approx.Accepts family assignment)

@[simp]

theorem Algebraic.Monotone.Clique.Approx.decode_eq_true {n : ℕ} (family : Family n) (assignment : Fin (edgeCount n) → Bool) : decode family assignment = true ↔ Accepts family assignment

@[simp]

theorem Algebraic.Monotone.Clique.Approx.decode_eq_false {n : ℕ} (family : Family n) (assignment : Fin (edgeCount n) → Bool) : decode family assignment = false ↔ ¬Accepts family assignment

noncomputable def Algebraic.Monotone.Clique.Approx.inputTerm {n : ℕ} (input : Fin (edgeCount n)) : Finset (Fin n)

The two endpoints of an input edge.

Equations

• Algebraic.Monotone.Clique.Approx.inputTerm input = {(↑((Algebraic.Monotone.Clique.edgeEquiv n).symm input)).1, (↑((Algebraic.Monotone.Clique.edgeEquiv n).symm input)).2}

noncomputable def Algebraic.Monotone.Clique.Approx.inputFamily {n : ℕ} (input : Fin (edgeCount n)) : Family n

The one-term approximator for an input variable.

Equations

• Algebraic.Monotone.Clique.Approx.inputFamily input = {Algebraic.Monotone.Clique.Approx.inputTerm input}

theorem Algebraic.Monotone.Clique.Approx.contains_inputTerm_iff {n : ℕ} (assignment : Fin (edgeCount n) → Bool) (input : Fin (edgeCount n)) : Contains assignment (inputTerm input) ↔ assignment input = true

The input term denotes exactly its edge variable.

@[simp]

theorem Algebraic.Monotone.Clique.Approx.decode_inputFamily {n : ℕ} (assignment : Fin (edgeCount n) → Bool) (input : Fin (edgeCount n)) : decode (inputFamily input) assignment = assignment input

def Algebraic.Monotone.Clique.Approx.joinTerms {n : ℕ} (left right : Finset (Fin n)) : Finset (Fin n)

Zero- and one-vertex clique indicators are the Boolean constant true. When conjoining terms, discard such a vacuous side; otherwise take the union.

Equations

• Algebraic.Monotone.Clique.Approx.joinTerms left right = if left.card ≤ 1 then right else if right.card ≤ 1 then left else left ∪ right

def Algebraic.Monotone.Clique.Approx.rawOr {n : ℕ} (left right : Family n) : Family n

Raw OR before truncation and plucking.

Equations

• Algebraic.Monotone.Clique.Approx.rawOr left right = left ∪ right

def Algebraic.Monotone.Clique.Approx.rawAnd {n : ℕ} (left right : Family n) : Family n

Raw approximate AND before truncation and plucking.

Equations

• Algebraic.Monotone.Clique.Approx.rawAnd left right = Finset.image (fun (pair : Finset (Fin n) × Finset (Fin n)) => Algebraic.Monotone.Clique.Approx.joinTerms pair.1 pair.2) (left ×ˢ right)

def Algebraic.Monotone.Clique.Approx.truncate {n : ℕ} (width : ℕ) (family : Family n) : Family n

Discard terms wider than width.

Equations

• Algebraic.Monotone.Clique.Approx.truncate width family = {set ∈ family | set.card ≤ width}

def Algebraic.Monotone.Clique.Approx.gateFamily {n : ℕ} (width : ℕ) (op : AndOr.Op) (arguments : Fin 2 → Family n) : Family n

The bounded raw family produced at a gate, before normalization.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Monotone.Clique.Approx.gateFamily_bounded {n : ℕ} (width : ℕ) (op : AndOr.Op) (arguments : Fin 2 → Family n) : Plucking.Bounded width (gateFamily width op arguments)

Gate preprocessing enforces the width bound before normalization.

noncomputable def Algebraic.Monotone.Clique.Approx.interpretation {n : ℕ} (petalCount : ℕ) (two_le : 2 ≤ petalCount) (width : ℕ) : Interpretation AndOr.signature (Family n)

The bounded-width approximate interpretation of binary AND/OR.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Monotone.Clique.Approx.interpretation_bounded {n : ℕ} (petalCount : ℕ) (two_le : 2 ≤ petalCount) (width : ℕ) (op : AndOr.Op) (arguments : Fin 2 → Family n) : Plucking.Bounded width (interpretation petalCount two_le width op arguments)

Every approximate gate result has bounded width.

theorem Algebraic.Monotone.Clique.Approx.interpretation_card_le {n : ℕ} (petalCount : ℕ) (two_le : 2 ≤ petalCount) (width : ℕ) (op : AndOr.Op) (arguments : Fin 2 → Family n) : Finset.card (interpretation petalCount two_le width op arguments) ≤ Sunflower.bound petalCount width

Every approximate gate result has at most the sunflower bound many terms.

theorem Algebraic.Monotone.Clique.Approx.inputFamily_bounded {width n : ℕ} (two_le_width : 2 ≤ width) (input : Fin (edgeCount n)) : Plucking.Bounded width (inputFamily input)

Input approximators have bounded width once the width is at least two.

@[simp]

theorem Algebraic.Monotone.Clique.Approx.inputFamily_card {n : ℕ} (input : Fin (edgeCount n)) : Finset.card (inputFamily input) = 1

Input approximators have one term.

structure Algebraic.Monotone.Clique.Approx.NormalFamily (n petalCount width : ℕ) : Type

A normalized approximator packages the two invariants needed for uniform local error bounds: bounded term width and bounded family cardinality.

• family : Family n

  The underlying clique DNF.

• bounded : Plucking.Bounded width self.family

  Every term respects the approximation width.

• card_le : Finset.card self.family ≤ Sunflower.bound petalCount width

  The family respects the elementary sunflower cardinality bound.

theorem Algebraic.Monotone.Clique.Approx.one_le_sunflower_bound (petalCount width : ℕ) (two_le_petals : 2 ≤ petalCount) : 1 ≤ Sunflower.bound petalCount width

The elementary sunflower bound is nonzero.

noncomputable def Algebraic.Monotone.Clique.Approx.normalInput {n : ℕ} (petalCount width : ℕ) (two_le_petals : 2 ≤ petalCount) (two_le_width : 2 ≤ width) (input : Fin (edgeCount n)) : NormalFamily n petalCount width

Input variables, viewed as normalized one-term approximators.

Equations

• Algebraic.Monotone.Clique.Approx.normalInput petalCount width two_le_petals two_le_width input = { family := Algebraic.Monotone.Clique.Approx.inputFamily input, bounded := ⋯, card_le := ⋯ }

noncomputable def Algebraic.Monotone.Clique.Approx.normalInterpretation {n : ℕ} (petalCount : ℕ) (two_le_petals : 2 ≤ petalCount) (width : ℕ) : Interpretation AndOr.signature (NormalFamily n petalCount width)

Gate evaluation on normalized approximators.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.Monotone.Clique.Approx.normalDecode {n petalCount width : ℕ} (family : NormalFamily n petalCount width) (assignment : Fin (edgeCount n) → Bool) : Bool

Boolean semantics of a normalized approximator.

Equations

• Algebraic.Monotone.Clique.Approx.normalDecode family assignment = Algebraic.Monotone.Clique.Approx.decode family.family assignment

@[simp]

theorem Algebraic.Monotone.Clique.Approx.normalDecode_eq_true {n petalCount width : ℕ} (family : NormalFamily n petalCount width) (assignment : Fin (edgeCount n) → Bool) : normalDecode family assignment = true ↔ Accepts family.family assignment

@[simp]

theorem Algebraic.Monotone.Clique.Approx.normalDecode_input {n : ℕ} (petalCount width : ℕ) (two_le_petals : 2 ≤ petalCount) (two_le_width : 2 ≤ width) (assignment : Fin (edgeCount n) → Bool) (input : Fin (edgeCount n)) : normalDecode (normalInput petalCount width two_le_petals two_le_width input) assignment = assignment input

theorem Algebraic.Monotone.Clique.Approx.contains_of_contains_joinTerms {n : ℕ} (assignment : Fin (edgeCount n) → Bool) (left right : Finset (Fin n)) (contains : Contains assignment (joinTerms left right)) : Contains assignment left ∧ Contains assignment right

A joined term implies both input terms on every graph.

theorem Algebraic.Monotone.Clique.Approx.contains_joinTerms_cliqueAssignment {n : ℕ} (clique left right : Finset (Fin n)) (leftContains : Contains (cliqueAssignment clique) left) (rightContains : Contains (cliqueAssignment clique) right) : Contains (cliqueAssignment clique) (joinTerms left right)

On a minimal positive clique graph, conjoining two accepted terms is represented exactly by joinTerms.

theorem Algebraic.Monotone.Clique.Approx.accepts_rawOr_iff {n : ℕ} (assignment : Fin (edgeCount n) → Bool) (left right : Family n) : Accepts (rawOr left right) assignment ↔ Accepts left assignment ∨ Accepts right assignment

Raw OR has exactly Boolean-OR semantics.

theorem Algebraic.Monotone.Clique.Approx.accepts_left_right_of_accepts_rawAnd {n : ℕ} (assignment : Fin (edgeCount n) → Bool) (left right : Family n) (accepted : Accepts (rawAnd left right) assignment) : Accepts left assignment ∧ Accepts right assignment

Raw approximate AND implies exact Boolean AND on every graph.