Universal verifiers from semi-ultrafilter covers

A cover of length t yields a native universal verifier with 3t auxiliary bits and exactly 5t binary AND gates. The verifier rejects precisely valid, pair-preserving certificates. True primary inputs have no such certificate by the cover property; false inputs supply their point-membership certificate. The construction includes empty covers and constant functions.

Main results

• Cslib.Circuits.Fusion.PairCover.exists_forallGuess: the universal verifier with exact cost.
• Cslib.Circuits.Fusion.conondeterministicAndComplexity_bounds: minimum universal-verifier AND complexity lies between semi-ultrafilter cover complexity and five times that measure.

References

• B. P. Cavalar and I. C. Oliveira, Boolean Circuit Complexity and Two-Dimensional Cover Problems, Theorem 45, credited there to Karchmer. The explicit factor five follows from the grouped certificate construction formalized here.

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

A cover of length t yields a verifier with 3t auxiliary bits and exactly 5t AND gates. Constants, OR gates and supplied positive/negative literals are free. No nonempty-target, nonempty-complement or positive-length assumption is imposed.

theorem Cslib.Circuits.Fusion.pairCoverComplexity_le_econondeterministicAndComplexity {n : ℕ} (f : BooleanFunction n) : pairCoverComplexity {x : BitString n | f x = true} (fun (i : Fin (n + n)) => {x : BitString n | Boolean.AltFormula.literals x i = true}) Semifilter.IsUltra ≤ Boolean.econondeterministicAndComplexity f

The semi-ultrafilter bound applies after minimizing over all auxiliary counts and verifiers.

theorem Cslib.Circuits.Fusion.econondeterministicAndComplexity_le_pairCoverComplexity {n : ℕ} (f : BooleanFunction n) : Boolean.econondeterministicAndComplexity f ≤ 5 * pairCoverComplexity {x : BitString n | f x = true} (fun (i : Fin (n + n)) => {x : BitString n | Boolean.AltFormula.literals x i = true}) Semifilter.IsUltra

A semi-ultrafilter cover gives a universal verifier at most five times as costly.

theorem Cslib.Circuits.Fusion.conondeterministicAndComplexity_bounds {n : ℕ} (f : BooleanFunction n) : have ρ := pairCoverComplexity {x : BitString n | f x = true} (fun (i : Fin (n + n)) => {x : BitString n | Boolean.AltFormula.literals x i = true}) Semifilter.IsUltra; ρ ≤ Boolean.econondeterministicAndComplexity f ∧ Boolean.econondeterministicAndComplexity f ≤ 5 * ρ

Linear semi-ultrafilter characterization of conondeterministic AND complexity, with explicit factors one and five and unrestricted finite auxiliary input counts.