Positive errors in the monotone CLIQUE approximation

On a minimal positive k-clique graph, sunflower plucking is harmless. The only possible local error is an AND whose two accepted terms join to more than width vertices and are therefore truncated. Such an error forces the positive clique to contain one fixed (width + 1)-set. This file packages that observation as a local approximation scheme and proves its exact finite counting bound.

def Algebraic.Monotone.Clique.Positive.containingCliques (n k : ℕ) (vertices : Finset (Fin n)) : Finset (CliqueSet n k)

Positive k-cliques containing a prescribed vertex set.

Equations

• Algebraic.Monotone.Clique.Positive.containingCliques n k vertices = {clique : Algebraic.Monotone.Clique.CliqueSet n k | vertices ⊆ ↑clique}

@[simp]

theorem Algebraic.Monotone.Clique.Positive.mem_containingCliques {n k : ℕ} (clique : CliqueSet n k) (vertices : Finset (Fin n)) : clique ∈ containingCliques n k vertices ↔ vertices ⊆ ↑clique

theorem Algebraic.Monotone.Clique.Positive.card_containingCliques {n k : ℕ} (vertices : Finset (Fin n)) (vertices_le_k : vertices.card ≤ k) : (containingCliques n k vertices).card = (n - vertices.card).choose (k - vertices.card)

The subtype presentation of CliqueSet does not change the usual binomial count of supersets.

theorem Algebraic.Monotone.Clique.Positive.card_containingCliques_of_wide {width k n : ℕ} (width_succ_le_k : width + 1 ≤ k) (vertices : Finset (Fin n)) (wide : width < vertices.card) : (containingCliques n k vertices).card ≤ (n - (width + 1)).choose (k - (width + 1))

If vertices is wider than the approximation width, the number of positive cliques containing it is bounded by the standard binomial cap.

def Algebraic.Monotone.Clique.Positive.pairExceptions (n k width : ℕ) (pair : Finset (Fin n) × Finset (Fin n)) : Finset (CliqueSet n k)

A wide pair contributes all positive cliques containing its joined term; a narrow pair contributes no exceptions.

Equations

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

def Algebraic.Monotone.Clique.Positive.andExceptions (n k width : ℕ) (left right : Approx.Family n) : Finset (CliqueSet n k)

Fresh positive errors at an approximate AND gate.

Equations

• Algebraic.Monotone.Clique.Positive.andExceptions n k width left right = (left ×ˢ right).biUnion (Algebraic.Monotone.Clique.Positive.pairExceptions n k width)

@[simp]

theorem Algebraic.Monotone.Clique.Positive.mem_pairExceptions {n k width : ℕ} (clique : CliqueSet n k) (pair : Finset (Fin n) × Finset (Fin n)) : clique ∈ pairExceptions n k width pair ↔ width < (Approx.joinTerms pair.1 pair.2).card ∧ Approx.joinTerms pair.1 pair.2 ⊆ ↑clique

theorem Algebraic.Monotone.Clique.Positive.card_andExceptions_le {width k n : ℕ} (width_succ_le_k : width + 1 ≤ k) (left right : Approx.Family n) : (andExceptions n k width left right).card ≤ Finset.card left * Finset.card right * (n - (width + 1)).choose (k - (width + 1))

One AND gate has at most one binomial cap per term pair.

def Algebraic.Monotone.Clique.Positive.errorCap (n k petalCount width : ℕ) : ℕ

Uniform positive error budget for normalized families.

Equations

• Algebraic.Monotone.Clique.Positive.errorCap n k petalCount width = Algebraic.Sunflower.bound petalCount width ^ 2 * (n - (width + 1)).choose (k - (width + 1))

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

Per-operation positive error cost. OR gates introduce no truncation error; an AND gate is charged the uniform pair bound.

Equations

• Algebraic.Monotone.Clique.Positive.operationCost n k petalCount width Algebraic.AndOr.Op.and = Algebraic.Monotone.Clique.Positive.errorCap n k petalCount width
• Algebraic.Monotone.Clique.Positive.operationCost n k petalCount width Algebraic.AndOr.Op.or = 0

def Algebraic.Monotone.Clique.Positive.exceptions {petalCount : ℕ} (n k width : ℕ) (op : AndOr.Op) (arguments : Fin 2 → Approx.NormalFamily n petalCount width) : Finset (CliqueSet n k)

Concrete positive exceptions for one normalized gate application.

Equations

• Algebraic.Monotone.Clique.Positive.exceptions n k width Algebraic.AndOr.Op.and arguments = Algebraic.Monotone.Clique.Positive.andExceptions n k width (arguments 0).family (arguments 1).family
• Algebraic.Monotone.Clique.Positive.exceptions n k width Algebraic.AndOr.Op.or arguments = ∅

theorem Algebraic.Monotone.Clique.Positive.boolInterpretation_mono (op : AndOr.Op) (exactArguments approxArguments : Fin 2 → Bool) (ordered : ∀ (input : Fin 2), exactArguments input ≤ approxArguments input) : AndOr.boolInterpretation op exactArguments ≤ AndOr.boolInterpretation op approxArguments

Binary Boolean AND and OR preserve pointwise Boolean order.

theorem Algebraic.Monotone.Clique.Positive.or_gate_correct {n k : ℕ} (petalCount : ℕ) (two_le_petals : 2 ≤ petalCount) (width : ℕ) (arguments : Fin 2 → Approx.NormalFamily n petalCount width) (clique : CliqueSet n k) : (AndOr.boolInterpretation AndOr.Op.or fun (input : Fin (AndOr.signature.Arity AndOr.Op.or)) => Approx.normalDecode (arguments input) (cliqueAssignment ↑clique)) ≤ Approx.normalDecode (Approx.normalInterpretation petalCount two_le_petals width AndOr.Op.or arguments) (cliqueAssignment ↑clique)

Normalized OR is positively correct on every minimal clique graph.

theorem Algebraic.Monotone.Clique.Positive.and_gate_correct {n k : ℕ} (petalCount : ℕ) (two_le_petals : 2 ≤ petalCount) (width : ℕ) (two_le_width : 2 ≤ width) (arguments : Fin 2 → Approx.NormalFamily n petalCount width) (clique : CliqueSet n k) (fresh : clique ∉ andExceptions n k width (arguments 0).family (arguments 1).family) : (AndOr.boolInterpretation AndOr.Op.and fun (input : Fin (AndOr.signature.Arity AndOr.Op.and)) => Approx.normalDecode (arguments input) (cliqueAssignment ↑clique)) ≤ Approx.normalDecode (Approx.normalInterpretation petalCount two_le_petals width AndOr.Op.and arguments) (cliqueAssignment ↑clique)

Away from andExceptions, normalized AND is positively correct.

def Algebraic.Monotone.Clique.Positive.scheme (n k petalCount width : ℕ) (two_le_petals : 2 ≤ petalCount) (two_le_width : 2 ≤ width) (width_succ_le_k : width + 1 ≤ k) : Approximation.Scheme AndOr.boolInterpretation (Approx.normalInterpretation petalCount two_le_petals width) (fun (family : Approx.NormalFamily n petalCount width) (clique : CliqueSet n k) => Approx.normalDecode family (cliqueAssignment ↑clique)) (fun (clique : CliqueSet n k) => cliqueAssignment ↑clique) (Approx.normalInput petalCount width two_le_petals two_le_width)

The complete positive-side local approximation scheme.

Equations

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