Negative errors of clique approximators

On the complete multipartite graph of a colouring c with r colours, a set of vertices has all edges inside exactly when c is injective on it (Cslib.Circuits.Clique.contains_ofColoring_iff). The approximate interpretation is wrong on such an input only when the approximator says true and the exact value is false. Disjunctions and conjunctions of sets make no such errors; only plucking does, when the colouring is injective on the core of a sunflower but on none of its petals.

For such a colouring, every petal contains two vertices of the same colour, one of them outside the core and so private to the petal. Choosing such a pair for every petal fixes the colour of one private vertex per petal in terms of the colours of the others, which leaves at most (w ^ 2) ^ p * r ^ (n - p) colourings (card_sunflowerBad_le). A plucking normalisation makes at most as many plucks as the family has sets (Cslib.relatesInSteps_pluckNormalForm), which bounds the errors of a gate (Cslib.Circuits.Monotone.Negative.scheme).

On the other hand, a nonempty approximator accepts at least half of the colourings when r is at least twice the number w ^ 2 of pairs inside a set (half_le_card_acceptedColorings).

Main definitions

• Cslib.Circuits.Monotone.Negative.collisionPairs, Cslib.Circuits.Monotone.Negative.Profile: collision pairs in a petal and profiles of collision pairs across a sunflower.
• Cslib.Circuits.Monotone.Negative.sunflowerBad, Cslib.Circuits.Monotone.Negative.pluckErrorCap: colourings injective on a sunflower core but on none of its petals, and the per-pluck negative error bound.
• Cslib.Circuits.Monotone.Negative.stepExceptions, Cslib.Circuits.Monotone.Negative.errorCost, Cslib.Circuits.Monotone.Negative.exceptions: negative errors of a step, per-operation negative error cost, and negative gate exceptions.
• Cslib.Circuits.Monotone.Negative.scheme: the approximation scheme on multipartite graphs.
• Cslib.Circuits.Monotone.Negative.acceptedColorings: colourings accepted by a family of vertex sets.

Main results

• Cslib.Circuits.Monotone.Negative.card_sunflowerBad_le: the colourings injective on the core of a sunflower but on none of its petals.
• Cslib.Circuits.Monotone.Negative.half_le_card_acceptedColorings: a nonempty approximator accepts many colourings.

References

• S. Jukna, Boolean Function Complexity: Advances and Frontiers, Chapter 9

Colourings bad for a sunflower

def Cslib.Circuits.Monotone.Negative.collisionPairs {n : ℕ} (K s : Finset (Fin n)) : Finset (Fin n × Fin n)

The ordered pairs of distinct vertices of s whose first vertex is outside K.

@[simp]

theorem Cslib.Circuits.Monotone.Negative.mem_collisionPairs {n : ℕ} {K s : Finset (Fin n)} {uv : Fin n × Fin n} : uv ∈ collisionPairs K s ↔ uv.1 ∈ s ∧ uv.1 ∉ K ∧ uv.2 ∈ s ∧ uv.1 ≠ uv.2

An ordered pair of vertices belongs to collisionPairs K s if and only if its first vertex lies in s \ K, its second vertex lies in s, and the two vertices are distinct.

@[reducible, inline]

abbrev Cslib.Circuits.Monotone.Negative.Profile {n : ℕ} (S : Finset (Finset (Fin n))) (K : Finset (Fin n)) : Type

A choice of a collision pair in every petal.

theorem Cslib.Circuits.Monotone.Negative.fst_injective {n : ℕ} {S : Finset (Finset (Fin n))} {K : Finset (Fin n)} (hS : IsSunflower S K) (π : Profile S K) : Function.Injective fun (s : ↥S) => (↑(π s)).1

In a sunflower, the first vertex of a collision pair is private to its petal.

def Cslib.Circuits.Monotone.Negative.sunflowerBad {n : ℕ} (r : ℕ) (S : Finset (Finset (Fin n))) (K : Finset (Fin n)) : Finset (Clique.Coloring n r)

The colourings injective on the core of a sunflower but on none of its petals.

def Cslib.Circuits.Monotone.Negative.pluckErrorCap (n r p w : ℕ) : ℕ

The number of negative errors charged to one pluck.

theorem Cslib.Circuits.Monotone.Negative.card_sunflowerBad_le {n r p w : ℕ} {S : Finset (Finset (Fin n))} {K : Finset (Fin n)} (hSp : S.card = p) (hS : IsSunflower S K) (hSw : ∀ s ∈ S, s.card ≤ w) : (sunflowerBad r S K).card ≤ pluckErrorCap n r p w

Bad colourings of a sunflower. At most (w ^ 2) ^ p * r ^ (n - p) colourings are injective on the core of a sunflower with p petals of at most w vertices but on none of the petals.

Errors of plucking

noncomputable def Cslib.Circuits.Monotone.Negative.stepExceptions {n : ℕ} (r : ℕ) (F G : Finset (Finset (Fin n))) : Finset (Clique.Coloring n r)

The colourings accepted by G but not by F.

@[simp]

theorem Cslib.Circuits.Monotone.Negative.mem_stepExceptions {n r : ℕ} {F G : Finset (Finset (Fin n))} {c : Clique.Coloring n r} : c ∈ stepExceptions r F G ↔ Accepts G (Clique.ofColoring c) ∧ ¬Accepts F (Clique.ofColoring c)

A colouring belongs to stepExceptions r F G if and only if ofColoring c is accepted by G and rejected by F.

theorem Cslib.Circuits.Monotone.Negative.stepExceptions_subset {n : ℕ} (r : ℕ) (F G H : Finset (Finset (Fin n))) : stepExceptions r F H ⊆ stepExceptions r F G ∪ stepExceptions r G H

The negative exceptions between F and H are contained in the union of those between F and G and those between G and H.

theorem Cslib.Circuits.Monotone.Negative.card_stepExceptions_pluckNormalForm_le {n r p w : ℕ} (hp : 2 ≤ p) {F : Finset (Finset (Fin n))} (hF : ∀ s ∈ F, s.card ≤ w) : (stepExceptions r F (pluckNormalForm p F)).card ≤ F.card * pluckErrorCap n r p w

A plucking normalisation makes at most as many errors as pluckErrorCap n r p w times the number of sets of the family.

The approximation scheme

def Cslib.Circuits.Monotone.Negative.errorCost (n r p w : ℕ) : signature.Op → ℕ

The number of negative errors charged to each operation.

theorem Cslib.Circuits.Monotone.Negative.card_gateTerms_le {n r p w : ℕ} (op : Op) (A : Fin (signature.Arity op) → Approximator n p w) : (gateTerms w op fun (i : Fin (signature.Arity op)) => (A i).terms).card * pluckErrorCap n r p w ≤ errorCost n r p w op

The number of pre-plucked terms produced by op, multiplied by pluckErrorCap n r p w, is at most errorCost n r p w op.

noncomputable def Cslib.Circuits.Monotone.Negative.exceptions {n p w : ℕ} (r : ℕ) (op : Op) (A : Fin (signature.Arity op) → Approximator n p w) : Finset (Clique.Coloring n r)

The negative errors of a gate: those of plucking the sets produced at the gate.

theorem Cslib.Circuits.Monotone.Negative.gate_correct {n r p w : ℕ} [Fact (2 ≤ p)] (op : Op) (A : Fin (signature.Arity op) → Approximator n p w) (c : Clique.Coloring n r) (hc : c ∉ exceptions r op A) : (Approximator.interpretation op A).decode (Clique.ofColoring c) ≤ interpretation op fun (i : Fin (signature.Arity op)) => (A i).decode (Clique.ofColoring c)

Away from its exceptions, a gate is negatively correct on multipartite graphs.

noncomputable def Cslib.Circuits.Monotone.Negative.scheme {n r p w : ℕ} [Fact (2 ≤ p)] (hw : 2 ≤ w) : Approximation.Scheme interpretation Approximator.interpretation (fun (A : Approximator n p w) (c : Clique.Coloring n r) => A.decode (Clique.ofColoring c)) Clique.ofColoring Approximator.input

Negative errors. The approximation scheme on the complete multipartite graphs of colourings with r colours: the approximate value is at most the exact one away from the errors of plucking.

Approximators accept many colourings

noncomputable def Cslib.Circuits.Monotone.Negative.acceptedColorings {n : ℕ} (r : ℕ) (F : Finset (Finset (Fin n))) : Finset (Clique.Coloring n r)

The colourings accepted by a family of vertex sets.

theorem Cslib.Circuits.Monotone.Negative.half_le_card_acceptedColorings {n r w : ℕ} (hn : 0 < n) (hr : 2 * w ^ 2 ≤ r) {F : Finset (Finset (Fin n))} (hF : ∀ s ∈ F, s.card ≤ w) (hne : F.Nonempty) : r ^ n ≤ 2 * (acceptedColorings r F).card

Approximators accept many colourings. If r is at least twice w ^ 2, every nonempty family of sets of at most w vertices accepts at least half of the colourings.