Native formulas for semi-ultrafilter certificates

Consistency violations are grouped by each of the three certificate bits per pair, costing one AND each. The fixed empty-set group costs none. Pair-preservation violations cost two ANDs each. Constants and OR gates are free, and the auxiliary labels and their negations are supplied as input literals. Thus the entire rejection test costs five ANDs per cover pair.

Main results

• Cslib.Circuits.Fusion.PairCertificate.exists_formula: compile the certificate test to a native monotone formula of five AND gates per pair from free primary and auxiliary literals.

References

• B. P. Cavalar and I. C. Oliveira, Boolean Circuit Complexity and Two-Dimensional Cover Problems, Theorem 45. The explicit factor five is obtained by the grouped certificate construction, rather than asserted as a constant in the cited characterization.

theorem Cslib.Circuits.Fusion.PairCertificate.exists_formula {U : Type u_1} {X : Type u_2} {n k : ℕ} (pairs : List (Set U × Set U)) (sources : Fin n → Set U) (input : X → Fin k → Bool) (x : X → Fin n → Bool) (y : X → Fin (size pairs) → Bool) (hx : ∀ (l : Fin n), ∃ (F : Formula Monotone.signature k), (∀ (z : X), F.eval Monotone.interpretation (input z) = true ↔ x z l = true) ∧ Formula.cost Monotone.andCost F = 0) (hy : ∀ (i : Fin (size pairs)) (b : Bool), ∃ (F : Formula Monotone.signature k), (∀ (z : X), F.eval Monotone.interpretation (input z) = true ↔ y z i = b) ∧ Formula.cost Monotone.andCost F = 0) : ∃ (F : Formula Monotone.signature k), (∀ (z : X), F.eval Monotone.interpretation (input z) = true ↔ Invalid pairs sources (x z) (y z) ∨ BreaksPair pairs (y z)) ∧ Formula.cost Monotone.andCost F = 5 * pairs.length

Compile consistency and pair-preservation violations using exactly five AND gates per pair. The primary source values and both polarities of each auxiliary label are supplied at zero cost.