Negative errors in the monotone CLIQUE approximation

The negative test graphs are complete multipartite graphs represented by vertex colorings. A term accepts exactly when its vertices receive distinct colors. If a sunflower pluck accepts its core but none of its petals, every petal supplies a collision involving a private petal vertex. Choosing one such collision per petal leaves one independently determined coordinate per petal, yielding the integral bound

width ^ (2 * petals) * colors ^ (n - petals).

The proof is a direct finite-cardinality count.

theorem Algebraic.Monotone.Clique.Negative.contains_coloringAssignment_iff {n r : ℕ} (coloring : Coloring n r) (vertices : Finset (Fin n)) : Contains (coloringAssignment coloring) vertices ↔ Set.InjOn coloring ↑vertices

A coloring graph contains a clique term exactly when the coloring is injective on the term's vertices.

def Algebraic.Monotone.Clique.Negative.collisionPairs {n : ℕ} (core petal : Finset (Fin n)) : Finset (Fin n × Fin n)

Ordered collision witnesses whose first endpoint is outside the core.

Equations

• Algebraic.Monotone.Clique.Negative.collisionPairs core petal = {pair ∈ (petal \ core) ×ˢ petal | pair.1 ≠ pair.2}

@[simp]

theorem Algebraic.Monotone.Clique.Negative.mem_collisionPairs {n : ℕ} (pair : Fin n × Fin n) (core petal : Finset (Fin n)) : pair ∈ collisionPairs core petal ↔ pair.1 ∈ petal ∧ pair.1 ∉ core ∧ pair.2 ∈ petal ∧ pair.1 ≠ pair.2

@[reducible, inline]

abbrev Algebraic.Monotone.Clique.Negative.Profile {n : ℕ} (petals : Finset (Finset (Fin n))) (core : Finset (Fin n)) : Type

One collision choice for every petal.

Equations

• Algebraic.Monotone.Clique.Negative.Profile petals core = ((petal : ↥petals) → ↥(Algebraic.Monotone.Clique.Negative.collisionPairs core ↑petal))

theorem Algebraic.Monotone.Clique.Negative.card_profile_le {n width : ℕ} (petals : Finset (Finset (Fin n))) (core : Finset (Fin n)) (bounded : ∀ petal ∈ petals, petal.card ≤ width) : Fintype.card (Profile petals core) ≤ (width ^ 2) ^ petals.card

There are at most width^(2*petals.card) collision profiles.

def Algebraic.Monotone.Clique.Negative.selected {n : ℕ} {petals : Finset (Finset (Fin n))} {core : Finset (Fin n)} (profile : Profile petals core) : Finset (Fin n)

The private (first) vertices selected by a collision profile.

Equations

• Algebraic.Monotone.Clique.Negative.selected profile = Finset.image (fun (petal : ↥petals) => (↑(profile petal)).1) Finset.univ

theorem Algebraic.Monotone.Clique.Negative.selectedVertex_injective {n : ℕ} {petals : Finset (Finset (Fin n))} {core : Finset (Fin n)} (sunflower : Sunflower.IsSunflowerWithCore petals core) (profile : Profile petals core) : Function.Injective fun (petal : ↥petals) => (↑(profile petal)).1

Distinct sunflower petals select distinct private vertices.

theorem Algebraic.Monotone.Clique.Negative.second_not_selected {n : ℕ} {petals : Finset (Finset (Fin n))} {core : Finset (Fin n)} (sunflower : Sunflower.IsSunflowerWithCore petals core) (profile : Profile petals core) (petal : ↥petals) : (↑(profile petal)).2 ∉ selected profile

A selected collision's dependency (its second endpoint) is never itself selected by the profile.

def Algebraic.Monotone.Clique.Negative.profileColorings {n : ℕ} (r : ℕ) {petals : Finset (Finset (Fin n))} {core : Finset (Fin n)} (profile : Profile petals core) : Finset (Coloring n r)

Colorings satisfying every equality selected by one profile.

Equations

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

@[simp]

theorem Algebraic.Monotone.Clique.Negative.mem_profileColorings {n r : ℕ} (coloring : Coloring n r) {petals : Finset (Finset (Fin n))} {core : Finset (Fin n)} (profile : Profile petals core) : coloring ∈ profileColorings r profile ↔ ∀ (petal : ↥petals), coloring (↑(profile petal)).1 = coloring (↑(profile petal)).2

theorem Algebraic.Monotone.Clique.Negative.card_profileColorings_le {n : ℕ} (r : ℕ) {petals : Finset (Finset (Fin n))} {core : Finset (Fin n)} (sunflower : Sunflower.IsSunflowerWithCore petals core) (profile : Profile petals core) : (profileColorings r profile).card ≤ r ^ (n - petals.card)

Fixing one private collision coordinate per petal leaves at most colors^(n-petals) colorings.

theorem Algebraic.Monotone.Clique.Negative.exists_collisionPair_of_not_injective {n r : ℕ} (coloring : Coloring n r) (core petal : Finset (Fin n)) (coreInjective : Set.InjOn coloring ↑core) (petalNotInjective : ¬Set.InjOn coloring ↑petal) : ∃ (pair : ↥(collisionPairs core petal)), coloring (↑pair).1 = coloring (↑pair).2

Failure of injectivity on a petal, together with injectivity on the core, supplies a collision whose first endpoint is private to the petal.

def Algebraic.Monotone.Clique.Negative.sunflowerBad {n : ℕ} (r : ℕ) (petals : Finset (Finset (Fin n))) (core : Finset (Fin n)) : Finset (Coloring n r)

Colorings that accept a sunflower core but reject every petal.

Equations

• Algebraic.Monotone.Clique.Negative.sunflowerBad r petals core = {coloring : Algebraic.Monotone.Clique.Coloring n r | Set.InjOn coloring ↑core ∧ ∀ petal ∈ petals, ¬Set.InjOn coloring ↑petal}

@[simp]

theorem Algebraic.Monotone.Clique.Negative.mem_sunflowerBad {n r : ℕ} (coloring : Coloring n r) (petals : Finset (Finset (Fin n))) (core : Finset (Fin n)) : coloring ∈ sunflowerBad r petals core ↔ Set.InjOn coloring ↑core ∧ ∀ petal ∈ petals, ¬Set.InjOn coloring ↑petal

def Algebraic.Monotone.Clique.Negative.profileCover {n : ℕ} (r : ℕ) (petals : Finset (Finset (Fin n))) (core : Finset (Fin n)) : Finset (Coloring n r)

Union of the equality classes associated with all collision profiles.

Equations

• Algebraic.Monotone.Clique.Negative.profileCover r petals core = Finset.univ.biUnion (Algebraic.Monotone.Clique.Negative.profileColorings r)

def Algebraic.Monotone.Clique.Negative.pluckErrorCap (n r petalCount width : ℕ) : ℕ

Integral error cap for one petalCount-sunflower pluck.

Equations

• Algebraic.Monotone.Clique.Negative.pluckErrorCap n r petalCount width = (width ^ 2) ^ petalCount * r ^ (n - petalCount)

theorem Algebraic.Monotone.Clique.Negative.card_sunflowerBad_le {n : ℕ} (r petalCount width : ℕ) (petals : Finset (Finset (Fin n))) (core : Finset (Fin n)) (petalsCard : petals.card = petalCount) (sunflower : Sunflower.IsSunflowerWithCore petals core) (bounded : ∀ petal ∈ petals, petal.card ≤ width) : (sunflowerBad r petals core).card ≤ pluckErrorCap n r petalCount width

Direct finite count for the bad colorings of one bounded sunflower.

noncomputable def Algebraic.Monotone.Clique.Negative.stepExceptions {n : ℕ} (r : ℕ) (before after : Approx.Family n) : Finset (Coloring n r)

Colorings newly accepted by one concrete family transition.

Equations

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

@[simp]

theorem Algebraic.Monotone.Clique.Negative.mem_stepExceptions {n r : ℕ} (coloring : Coloring n r) (before after : Approx.Family n) : coloring ∈ stepExceptions r before after ↔ Approx.Accepts after (coloringAssignment coloring) ∧ ¬Approx.Accepts before (coloringAssignment coloring)

theorem Algebraic.Monotone.Clique.Negative.stepExceptions_subset_sunflowerBad {n r petalCount : ℕ} {before after : Approx.Family n} (step : Plucking.Step petalCount before after) : stepExceptions r before after ⊆ sunflowerBad r step.petals step.core

Every fresh false positive of a pluck lies in the corresponding sunflower bad-coloring set.

theorem Algebraic.Monotone.Clique.Negative.card_stepExceptions_le {n width r petalCount : ℕ} {before after : Approx.Family n} (step : Plucking.Step petalCount before after) (bounded : Plucking.Bounded width before) : (stepExceptions r before after).card ≤ pluckErrorCap n r petalCount width

One bounded pluck introduces at most pluckErrorCap negative errors.

theorem Algebraic.Monotone.Clique.Negative.stepExceptions_trans_subset {n : ℕ} (r : ℕ) (before middle after : Approx.Family n) : stepExceptions r before after ⊆ stepExceptions r before middle ∪ stepExceptions r middle after

Fresh errors across a composite transition lie in the union of the fresh errors of its two pieces.

theorem Algebraic.Monotone.Clique.Negative.card_reductionExceptions_le {n petalCount : ℕ} (r width : ℕ) {steps : ℕ} {before after : Approx.Family n} (reduction : Plucking.Reduction petalCount steps before after) (two_le_petals : 2 ≤ petalCount) (bounded : Plucking.Bounded width before) : (stepExceptions r before after).card ≤ steps * pluckErrorCap n r petalCount width

A bounded reduction has at most one pluck cap per step. The exception set is defined extensionally, avoiding any elimination of proof-relevant reductions into data.

noncomputable def Algebraic.Monotone.Clique.Negative.normalizeExceptions {n : ℕ} (petalCount : ℕ) (two_le_petals : 2 ≤ petalCount) (r : ℕ) (family : Approx.Family n) : Finset (Coloring n r)

Negative exceptions accumulated by the chosen normalizer.

Equations

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

theorem Algebraic.Monotone.Clique.Negative.acceptance_of_normalize_away {n : ℕ} (petalCount : ℕ) (two_le_petals : 2 ≤ petalCount) (r : ℕ) (family : Approx.Family n) (coloring : Coloring n r) (fresh : coloring ∉ normalizeExceptions petalCount two_le_petals r family) (accepted : Approx.Accepts (Plucking.normalize petalCount two_le_petals family) (coloringAssignment coloring)) : Approx.Accepts family (coloringAssignment coloring)

Normalization is negatively sound away from its recorded exceptions.

theorem Algebraic.Monotone.Clique.Negative.card_normalizeExceptions_le {n : ℕ} (petalCount : ℕ) (two_le_petals : 2 ≤ petalCount) (r width : ℕ) (family : Approx.Family n) (bounded : Plucking.Bounded width family) : (normalizeExceptions petalCount two_le_petals r family).card ≤ Finset.card family * pluckErrorCap n r petalCount width

A bounded family pays at most one pluck cap per initial term.

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

The bounded raw family normalized by one gate.

Equations

• Algebraic.Monotone.Clique.Negative.gateFamily width op arguments = Algebraic.Monotone.Clique.Approx.gateFamily width op fun (input : Fin 2) => (arguments input).family

def Algebraic.Monotone.Clique.Negative.operationCost (n r petalCount width : ℕ) : OperationCost AndOr.signature

Per-operation negative error cost.

Equations

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

noncomputable def Algebraic.Monotone.Clique.Negative.exceptions {n : ℕ} (petalCount : ℕ) (two_le_petals : 2 ≤ petalCount) (r width : ℕ) (op : AndOr.Op) (arguments : Fin 2 → Approx.NormalFamily n petalCount width) : Finset (Coloring n r)

Concrete negative exceptions are precisely the false positives introduced while normalizing the gate's truncated raw family.

Equations

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

theorem Algebraic.Monotone.Clique.Negative.card_exceptions_le {n : ℕ} (petalCount : ℕ) (two_le_petals : 2 ≤ petalCount) (r width : ℕ) (op : AndOr.Op) (arguments : Fin 2 → Approx.NormalFamily n petalCount width) : (exceptions petalCount two_le_petals r width op arguments).card ≤ operationCost n r petalCount width op

theorem Algebraic.Monotone.Clique.Negative.gate_correct {n : ℕ} (petalCount : ℕ) (two_le_petals : 2 ≤ petalCount) (r width : ℕ) (op : AndOr.Op) (arguments : Fin 2 → Approx.NormalFamily n petalCount width) (coloring : Coloring n r) (fresh : coloring ∉ exceptions petalCount two_le_petals r width op arguments) : Approx.normalDecode (Approx.normalInterpretation petalCount two_le_petals width op arguments) (coloringAssignment coloring) ≤ AndOr.boolInterpretation op fun (input : Fin (AndOr.signature.Arity op)) => Approx.normalDecode (arguments input) (coloringAssignment coloring)

A normalized gate is negatively correct away from the colorings charged to its plucking normalization.

noncomputable def Algebraic.Monotone.Clique.Negative.scheme (n r petalCount width : ℕ) (two_le_petals : 2 ≤ petalCount) (two_le_width : 2 ≤ width) : Approximation.Scheme AndOr.boolInterpretation (Approx.normalInterpretation petalCount two_le_petals width) (fun (family : Approx.NormalFamily n petalCount width) (coloring : Coloring n r) => Approx.normalDecode family (coloringAssignment coloring)) (fun (coloring : Coloring n r) => coloringAssignment coloring) (Approx.normalInput petalCount width two_le_petals two_le_width)

The complete negative-side local approximation scheme.

Equations

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

def Algebraic.Monotone.Clique.Negative.injectiveColorings {n : ℕ} (r : ℕ) (vertices : Finset (Fin n)) : Finset (Coloring n r)

Colorings injective on a fixed vertex term.

Equations

• Algebraic.Monotone.Clique.Negative.injectiveColorings r vertices = {coloring : Algebraic.Monotone.Clique.Coloring n r | Set.InjOn coloring ↑vertices}

def Algebraic.Monotone.Clique.Negative.nonInjectiveColorings {n : ℕ} (r : ℕ) (vertices : Finset (Fin n)) : Finset (Coloring n r)

Colorings with a collision on a fixed vertex term.

Equations

• Algebraic.Monotone.Clique.Negative.nonInjectiveColorings r vertices = {coloring : Algebraic.Monotone.Clique.Coloring n r | ¬Set.InjOn coloring ↑vertices}

theorem Algebraic.Monotone.Clique.Negative.card_nonInjectiveColorings_le {n : ℕ} (r width : ℕ) (vertices : Finset (Fin n)) (bounded : vertices.card ≤ width) : (nonInjectiveColorings r vertices).card ≤ width ^ 2 * r ^ (n - 1)

A width-bounded term has at most width² * colors^(n-1) noninjective colorings. This is the one-petal specialization of the profile count.

theorem Algebraic.Monotone.Clique.Negative.card_injective_add_nonInjective {n : ℕ} (r : ℕ) (vertices : Finset (Fin n)) : (injectiveColorings r vertices).card + (nonInjectiveColorings r vertices).card = r ^ n

Injective and noninjective colorings partition the full coloring space.

theorem Algebraic.Monotone.Clique.Negative.half_colorings_injective {n : ℕ} (nPositive : 0 < n) (r width : ℕ) (colorsLarge : 2 * width ^ 2 ≤ r) (vertices : Finset (Fin n)) (bounded : vertices.card ≤ width) : r ^ n ≤ 2 * (injectiveColorings r vertices).card

When the color set is at least twice the ordered-pair budget, at least half of all colorings are injective on every bounded term.

noncomputable def Algebraic.Monotone.Clique.Negative.acceptedColorings {n : ℕ} (r : ℕ) (family : Approx.Family n) : Finset (Coloring n r)

Colorings accepted by a clique DNF family.

Equations

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

@[simp]

theorem Algebraic.Monotone.Clique.Negative.mem_acceptedColorings {n r : ℕ} (coloring : Coloring n r) (family : Approx.Family n) : coloring ∈ acceptedColorings r family ↔ Approx.Accepts family (coloringAssignment coloring)

theorem Algebraic.Monotone.Clique.Negative.half_colorings_accepted {n : ℕ} (nPositive : 0 < n) (r width : ℕ) (colorsLarge : 2 * width ^ 2 ≤ r) (family : Approx.Family n) (bounded : Plucking.Bounded width family) (nonempty : Finset.Nonempty family) : r ^ n ≤ 2 * (acceptedColorings r family).card

Every nonempty bounded clique DNF accepts at least half of all negative colorings under the large-color hypothesis.