Conondeterministic AND complexity

Minimize the native AND cost of a Boolean verifier over every finite number of auxiliary bits and every verifier whose universal quantification is the target. Both polarities of every primary and auxiliary bit are supplied for free. Constants and OR gates also have zero cost. This is a circuit-size measure; it is not verifier runtime or a bound on auxiliary bit count.

Main definitions

• Cslib.Circuits.Boolean.econondeterministicAndComplexity: minimum universal-verifier AND cost.

Main results

• Cslib.Circuits.Boolean.econondeterministicAndComplexity_le_cost: any verifier gives a bound.
• Cslib.Circuits.Boolean.le_econondeterministicAndComplexity_iff: lower bounds hold precisely when they hold for every verifier circuit and every number of auxiliary bits.

References

• B. P. Cavalar and I. C. Oliveira, Boolean Circuit Complexity and Two-Dimensional Cover Problems, Theorem 45, credited there to Karchmer.

noncomputable def Cslib.Circuits.Boolean.econondeterministicAndComplexity {n : ℕ} (f : BooleanFunction n) : ℕ∞

Minimum AND cost over all universally quantified verifiers. Constants, OR gates and positive/negative input literals are free; the auxiliary count is unrestricted.

theorem Cslib.Circuits.Boolean.econondeterministicAndComplexity_le_ecomplexityFrom {n : ℕ} {f : BooleanFunction n} {a : ℕ} (g : BooleanFunction (n + a)) (hg : forallGuess g = f) : econondeterministicAndComplexity f ≤ ecomplexityFrom Monotone.interpretation Monotone.andCost (single g) AltFormula.literals

A fixed universal verifier bounds the minimum over all verifier functions.

theorem Cslib.Circuits.Boolean.econondeterministicAndComplexity_le_cost {n : ℕ} {f : BooleanFunction n} {a : ℕ} (g : BooleanFunction (n + a)) (hg : forallGuess g = f) (c : Circuit Monotone.signature (n + a + (n + a)) 1) (hc : c.ComputesFrom Monotone.interpretation (single g) AltFormula.literals) : econondeterministicAndComplexity f ≤ ↑(c.program.cost Monotone.andCost)

Every concrete universal verifier bounds conondeterministic AND complexity.

theorem Cslib.Circuits.Boolean.le_econondeterministicAndComplexity_iff {n : ℕ} {f : BooleanFunction n} {k : ℕ∞} : k ≤ econondeterministicAndComplexity f ↔ ∀ (a : ℕ) (g : BooleanFunction (n + a)), forallGuess g = f → ∀ (c : Circuit Monotone.signature (n + a + (n + a)) 1), c.ComputesFrom Monotone.interpretation (single g) AltFormula.literals → k ≤ ↑(c.program.cost Monotone.andCost)

Lower bounds must hold for every auxiliary count and every implementing verifier circuit.