Finite certificates for semi-ultrafilter covers

A certificate labels both components and the intersection of each cover pair. A fixed additional empty set is rejected. Invalid labels are detected by a rejected superset of an accepted or required set, or two rejected sets covering the carrier. All pairs, including equal pairs and the fixed empty set, participate in these tests. A valid certificate extends to a semi-ultrafilter; if it also preserves every listed pair it contradicts a cover above a target point.

Main definitions

• Cslib.Circuits.Fusion.PairCertificate.sets: the three sets per pair and fixed empty set.
• Cslib.Circuits.Fusion.PairCertificate.Invalid: the grouped consistency violations.
• Cslib.Circuits.Fusion.PairCertificate.BreaksPair: failure of pair preservation.

Main results

• Cslib.Circuits.Fusion.PairCertificate.exists_filter_of_not_invalid: realize a valid certificate.

References

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

@[reducible, inline]

abbrev Cslib.Circuits.Fusion.PairCertificate.size {U : Type u_1} (pairs : List (Set U × Set U)) : ℕ

Three certificate bits per pair: its first set, second set and intersection.

def Cslib.Circuits.Fusion.PairCertificate.left {U : Type u_1} (pairs : List (Set U × Set U)) (i : Fin pairs.length) : Fin (size pairs)

The first-component certificate index.

def Cslib.Circuits.Fusion.PairCertificate.right {U : Type u_1} (pairs : List (Set U × Set U)) (i : Fin pairs.length) : Fin (size pairs)

The second-component certificate index.

def Cslib.Circuits.Fusion.PairCertificate.inter {U : Type u_1} (pairs : List (Set U × Set U)) (i : Fin pairs.length) : Fin (size pairs)

The intersection certificate index.

def Cslib.Circuits.Fusion.PairCertificate.sets {U : Type u_1} (pairs : List (Set U × Set U)) : Option (Fin (size pairs)) → Set U

A fixed empty set supplements the three sets for each pair.

def Cslib.Circuits.Fusion.PairCertificate.label {U : Type u_1} (pairs : List (Set U × Set U)) (y : Fin (size pairs) → Bool) : Option (Fin (size pairs)) → Bool

The fixed empty set has label false.

@[simp]

theorem Cslib.Circuits.Fusion.PairCertificate.sets_left {U : Type u_1} (pairs : List (Set U × Set U)) (i : Fin pairs.length) : sets pairs (some (left pairs i)) = (pairs.get i).1

@[simp]

theorem Cslib.Circuits.Fusion.PairCertificate.sets_right {U : Type u_1} (pairs : List (Set U × Set U)) (i : Fin pairs.length) : sets pairs (some (right pairs i)) = (pairs.get i).2

@[simp]

theorem Cslib.Circuits.Fusion.PairCertificate.sets_inter {U : Type u_1} (pairs : List (Set U × Set U)) (i : Fin pairs.length) : sets pairs (some (inter pairs i)) = (pairs.get i).1 ∩ (pairs.get i).2

def Cslib.Circuits.Fusion.PairCertificate.Invalid {U : Type u_1} (pairs : List (Set U × Set U)) {n : ℕ} (sources : Fin n → Set U) (x : Fin n → Bool) (y : Fin (size pairs) → Bool) : Prop

Consistency violations, grouped by a rejected set. The sources marked true must be accepted.

def Cslib.Circuits.Fusion.PairCertificate.BreaksPair {U : Type u_1} (pairs : List (Set U × Set U)) (y : Fin (size pairs) → Bool) : Prop

An accepted pair with rejected intersection.

theorem Cslib.Circuits.Fusion.PairCertificate.exists_filter_of_not_invalid {U : Type u_1} (pairs : List (Set U × Set U)) {n : ℕ} (sources : Fin n → Set U) (x : Fin n → Bool) (y : Fin (size pairs) → Bool) (h : ¬Invalid pairs sources x y) : ∃ (F : Semifilter U), F.IsUltra ∧ (∀ (i : Option (Fin (size pairs))), F (sets pairs i) ↔ label pairs y i = true) ∧ ∀ (l : Fin n), x l = true → F (sources l)

Every valid labeling is realized by a semi-ultrafilter accepting all required sources.

noncomputable def Cslib.Circuits.Fusion.PairCertificate.pointLabels {U : Type u_1} (pairs : List (Set U × Set U)) (u : U) (i : Fin (size pairs)) : Bool

A point supplies a consistent certificate, including when the pair list is empty.

@[simp]

theorem Cslib.Circuits.Fusion.PairCertificate.label_pointLabels {U : Type u_1} (pairs : List (Set U × Set U)) (u : U) (i : Option (Fin (size pairs))) : label pairs (pointLabels pairs u) i = true ↔ u ∈ sets pairs i

theorem Cslib.Circuits.Fusion.PairCertificate.not_invalid_pointLabels {U : Type u_1} (pairs : List (Set U × Set U)) {n : ℕ} (sources : Fin n → Set U) (x : Fin n → Bool) (u : U) (hx : ∀ (l : Fin n), x l = true → u ∈ sources l) : ¬Invalid pairs sources x (pointLabels pairs u)

Point membership has no consistency violation whenever all required sources contain it.

theorem Cslib.Circuits.Fusion.PairCertificate.not_breaksPair_pointLabels {U : Type u_1} (pairs : List (Set U × Set U)) (u : U) : ¬BreaksPair pairs (pointLabels pairs u)

Point membership preserves every intersection pair.

theorem Cslib.Circuits.Fusion.PairCover.invalid_or_breaksPair {X : Type u_1} {n : ℕ} {target : Set X} {input : Fin n → Set X} (c : PairCover target input Semifilter.IsUltra) (x : ↑target) (y : Fin (PairCertificate.size c.pairs) → Bool) : PairCertificate.Invalid c.pairs (fun (i : Fin n) => Subtype.val ⁻¹' input i) (fun (i : Fin n) => decide (↑x ∈ input i)) y ∨ PairCertificate.BreaksPair c.pairs y

Above a target point, every certificate either is inconsistent or breaks a cover pair.