Extending consistent semi-ultrafilter certificates

A family of rejected sets determines the largest upward family that rejects all of them: a set is accepted exactly when it is contained in no rejected set. If the empty set is rejected and no two rejected sets cover the universe, this family is a semi-ultrafilter. The condition includes equal pairs and the empty set, so it also handles the empty carrier without an implicit nonemptiness assumption.

Main definitions

• Cslib.Circuits.Fusion.Semifilter.ofRejected: the maximal extension avoiding rejected sets.

Main results

• Cslib.Circuits.Fusion.Semifilter.isUltra_ofRejected: the extension is a semi-ultrafilter.
• Cslib.Circuits.Fusion.Semifilter.ofRejected_apply_iff: its exact acceptance criterion.

References

• B. P. Cavalar and I. C. Oliveira, Boolean Circuit Complexity and Two-Dimensional Cover Problems, Theorem 45, credited there to Karchmer. This elementary extension construction is used to verify a finite certificate for the converse direction.

def Cslib.Circuits.Fusion.Semifilter.ofRejected {U : Type u_1} (rejected : Set (Set U)) (hempty : ∅ ∈ rejected) (hunion : ∀ s ∈ rejected, ∀ t ∈ rejected, s ∪ t ≠ Set.univ) : Semifilter U

The maximal upward family avoiding each rejected set, under the conditions that make it proper and nonempty. The union condition includes a rejected set paired with itself.

@[simp]

theorem Cslib.Circuits.Fusion.Semifilter.ofRejected_apply_iff {U : Type u_1} (rejected : Set (Set U)) (hempty : ∅ ∈ rejected) (hunion : ∀ s ∈ rejected, ∀ t ∈ rejected, s ∪ t ≠ Set.univ) (s : Set U) : (ofRejected rejected hempty hunion) s ↔ ∀ t ∈ rejected, ¬s ⊆ t

Acceptance is exactly the absence of a rejected superset.

theorem Cslib.Circuits.Fusion.Semifilter.isUltra_ofRejected {U : Type u_1} (rejected : Set (Set U)) (hempty : ∅ ∈ rejected) (hunion : ∀ s ∈ rejected, ∀ t ∈ rejected, s ∪ t ≠ Set.univ) : (ofRejected rejected hempty hunion).IsUltra

Two rejected supersets of complementary sets would cover the universe.

theorem Cslib.Circuits.Fusion.Semifilter.not_ofRejected_of_mem {U : Type u_1} (rejected : Set (Set U)) (hempty : ∅ ∈ rejected) (hunion : ∀ s ∈ rejected, ∀ t ∈ rejected, s ∪ t ≠ Set.univ) {s : Set U} (hs : s ∈ rejected) : ¬(ofRejected rejected hempty hunion) s

Every prescribed rejection is respected.

theorem Cslib.Circuits.Fusion.Semifilter.exists_isUltra_of_labels {U : Type u_1} {ι : Type u_2} (sets : ι → Set U) (labels : ι → Bool) (zero : ι) (hzero : sets zero = ∅) (hlabel : labels zero = false) (hmono : ∀ (i j : ι), sets i ⊆ sets j → labels i = true → labels j = true) (hcover : ∀ (i j : ι), sets i ∪ sets j = Set.univ → labels i = true ∨ labels j = true) : ∃ (F : Semifilter U), F.IsUltra ∧ (∀ (i : ι), F (sets i) ↔ labels i = true) ∧ ∀ (s : Set U), F s ↔ ∀ (i : ι), labels i = false → ¬s ⊆ sets i

Consistent acceptance labels extend to a semi-ultrafilter. The index includes a prescribed empty rejected set; no finiteness or nonempty-carrier assumption is needed.