Semi-ultrafilter bounds for universally quantified circuits

For a Boolean verifier, choose a rejecting auxiliary assignment for each false primary input. A semi-ultrafilter above a true primary input selects auxiliary reference bits by accepting one side of each auxiliary coordinate. The verifier accepts this fused reference, but rejects every chosen counterexample. Pulling its AND pairs back gives a cover with exactly its AND count.

The quantifier is the existing Boolean.forallGuess. Verifiers are native monotone circuits with positive and negative input literals supplied for free; constants and OR gates have zero AND cost. This module proves the cover lower-bound direction of the conondeterministic characterization, not its converse.

Main definitions

• Cslib.Circuits.Boolean.forallGuess: the existing universal quantifier on auxiliary bits.

Main results

• Cslib.Circuits.Fusion.exists_pairCover_forallGuess: extract a cover of exact AND cost.
• Cslib.Circuits.Fusion.pairCoverComplexity_forallGuess_le_cost: semi-ultrafilter cover complexity bounds every native universal verifier's AND count.

References

• B. P. Cavalar and I. C. Oliveira, Boolean Circuit Complexity and Two-Dimensional Cover Problems, Theorem 45, credited there to Karchmer.
• Adapted from LowerBound/Fusion/Conondeterministic.lean in S. Schlesinger, Algebraic circuit formalizations in Complexitylib.

theorem Cslib.Circuits.Fusion.exists_pairCover_forallGuess {n a : ℕ} (g : BooleanFunction (n + a)) (c : Circuit Monotone.signature (n + a + (n + a)) 1) (hc : c.ComputesFrom Monotone.interpretation (single g) Boolean.AltFormula.literals) : ∃ (cover : PairCover {x : BitString n | Boolean.forallGuess g x = true} (fun (i : Fin (n + n)) => {x : BitString n | Boolean.AltFormula.literals x i = true}) Semifilter.IsUltra), cover.pairs.length = c.program.cost Monotone.andCost

A universally quantified verifier gives a cover of exactly the same AND cost.

theorem Cslib.Circuits.Fusion.pairCoverComplexity_forallGuess_le_cost {n a : ℕ} (g : BooleanFunction (n + a)) (c : Circuit Monotone.signature (n + a + (n + a)) 1) (hc : c.ComputesFrom Monotone.interpretation (single g) Boolean.AltFormula.literals) : pairCoverComplexity {x : BitString n | Boolean.forallGuess g x = true} (fun (i : Fin (n + n)) => {x : BitString n | Boolean.AltFormula.literals x i = true}) Semifilter.IsUltra ≤ ↑(c.program.cost Monotone.andCost)

Semi-ultrafilter cover bounds apply to native universally quantified verifiers, with no loss in the number of AND gates and any number of auxiliary bits.

theorem Cslib.Circuits.Fusion.pairCoverComplexity_forallGuess_le_ecomplexityFrom {n a : ℕ} (g : BooleanFunction (n + a)) : pairCoverComplexity {x : BitString n | Boolean.forallGuess g x = true} (fun (i : Fin (n + n)) => {x : BitString n | Boolean.AltFormula.literals x i = true}) Semifilter.IsUltra ≤ ecomplexityFrom Monotone.interpretation Monotone.andCost (single g) Boolean.AltFormula.literals

The cover lower bound also holds for the minimum AND cost of implementing the verifier.