Documentation

Complexitylib.Algebraic.LowerBound.Monotone.Clique.LowerBound

A parameterized monotone CLIQUE circuit lower bound #

This file combines the positive truncation scheme and the negative plucking scheme. Both evaluate the same bounded-width approximator on the shared DAG, so a small positive-error budget forces the final family to be nonempty while the negative density lemma forces that same family to make many errors.

The main result is an explicit, division-free dichotomy. It is useful both for exact finite parameter choices and for later asymptotic specialization.

source
@[reducible, inline]
abbrev Algebraic.Monotone.Clique.LowerBound.positiveGateCap (n k petalCount width : ℕ) :
ℕ

Uniform positive error cap per circuit gate.

Equations
Instances For
    source
    def Algebraic.Monotone.Clique.LowerBound.negativeGateCap (n r petalCount width : ℕ) :
    ℕ

    A common upper bound for the two negative per-operation costs.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def Algebraic.Monotone.Clique.LowerBound.outputFamily {n : ℕ} (petalCount : ℕ) (two_le_petals : 2 ≤ petalCount) (width : ℕ) (two_le_width : 2 ≤ width) (circuit : Circuit AndOr.signature (edgeCount n) 1) :
      Approx.NormalFamily n petalCount width

      The approximator produced at the output of a circuit.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Algebraic.Monotone.Clique.LowerBound.outputFamily_nonempty (n k petalCount width : ℕ) (two_le_petals : 2 ≤ petalCount) (two_le_width : 2 ≤ width) (width_succ_le_k : width + 1 ≤ k) (circuit : Circuit AndOr.signature (edgeCount n) 1) (computes : ∀ (assignment : Fin (edgeCount n) → Bool), circuit.eval AndOr.boolInterpretation assignment 0 = function n k assignment) (budgetSmall : positiveGateCap n k petalCount width * circuit.size < n.choose k) :
        Finset.Nonempty (outputFamily petalCount two_le_petals width two_le_width circuit).family

        If the positive local-error budget is smaller than the number of minimal positive clique graphs, the output approximator contains a term.

        source
        theorem Algebraic.Monotone.Clique.LowerBound.acceptedColorings_card_le_negativeCost (n k petalCount width : ℕ) (kPositive : 0 < k) (two_le_petals : 2 ≤ petalCount) (two_le_width : 2 ≤ width) (circuit : Circuit AndOr.signature (edgeCount n) 1) (computes : ∀ (assignment : Fin (edgeCount n) → Bool), circuit.eval AndOr.boolInterpretation assignment 0 = function n k assignment) :
        (Negative.acceptedColorings (k - 1) (outputFamily petalCount two_le_petals width two_le_width circuit).family).card ≤ circuit.cost (Negative.operationCost n (k - 1) petalCount width)

        The accepted negative colorings of the circuit's output approximator are contained in the negative scheme's global failure set.

        source
        theorem Algebraic.Monotone.Clique.LowerBound.circuitSize_dichotomy (n k petalCount width : ℕ) (nPositive : 0 < n) (kPositive : 0 < k) (two_le_petals : 2 ≤ petalCount) (two_le_width : 2 ≤ width) (width_succ_le_k : width + 1 ≤ k) (colorsLarge : 2 * width ^ 2 ≤ k - 1) (circuit : Circuit AndOr.signature (edgeCount n) 1) (computes : ∀ (assignment : Fin (edgeCount n) → Bool), circuit.eval AndOr.boolInterpretation assignment 0 = function n k assignment) :
        n.choose k ≤ positiveGateCap n k petalCount width * circuit.size ∨ (k - 1) ^ n ≤ 2 * negativeGateCap n (k - 1) petalCount width * circuit.size

        Razborov's bounded-width approximation dichotomy in explicit finite form. Every monotone circuit computing k-CLIQUE must exhaust either the positive truncation budget or the negative plucking budget.

        source
        theorem Algebraic.Monotone.Clique.LowerBound.sizeBound_lt_circuitSize (n k petalCount width sizeBound : ℕ) (nPositive : 0 < n) (kPositive : 0 < k) (two_le_petals : 2 ≤ petalCount) (two_le_width : 2 ≤ width) (width_succ_le_k : width + 1 ≤ k) (colorsLarge : 2 * width ^ 2 ≤ k - 1) (positiveBudget : positiveGateCap n k petalCount width * sizeBound < n.choose k) (negativeBudget : 2 * negativeGateCap n (k - 1) petalCount width * sizeBound < (k - 1) ^ n) (circuit : Circuit AndOr.signature (edgeCount n) 1) (computes : ∀ (assignment : Fin (edgeCount n) → Bool), circuit.eval AndOr.boolInterpretation assignment 0 = function n k assignment) :
        sizeBound < circuit.size

        Any size bound below both error thresholds is smaller than the circuit.