Exact consistency and the approximation interpretation of Fusion

The witnesses used for general set constructions require only acceptance of inputs true at the reference point. Oliveira's nonmonotone Fusion model instead requires exact agreement on both positive and negative literals [Oliveira2018Approximation, Definition 6]. These conditions are different even when both polarities are supplied.

The observation of a set at a witness changes membership only at the distinguished point. Under exact consistency it preserves supplied inputs. Unions have no positive error and intersections have no negative error; the positive intersection error is precisely failure to preserve the restricted pair. This is the local model bridge in Oliveira's Theorem 3. It does not prove the random-pair lemma or the fixed-distribution counting barrier.

Main definitions

• Cslib.Circuits.Fusion.Semifilter.IsConsistentWith: exact agreement with a bit vector on both literal polarities.
• Cslib.Circuits.Fusion.SemifilterWitness.IsExact: exact agreement on the supplied input family.
• Cslib.Circuits.Fusion.SemifilterWitness.observe: the set observed in one witness fiber of the extended model.

Main results

• Cslib.Circuits.Fusion.Semifilter.IsConsistentWith.unique: literals determine the consistent bit vector.
• Cslib.Circuits.Fusion.SemifilterWitness.observe_input: exact witnesses preserve all supplied inputs.
• Cslib.Circuits.Fusion.SemifilterWitness.inter_error: intersection errors are exactly the covering pairs.

References

• Igor Carboni Oliveira, Notes on the Method of Approximations and the Emergence of the Fusion Method, Definition 6 and Theorem 3.
• Alexander A. Razborov, On the method of approximations.

def Cslib.Circuits.Fusion.Semifilter.IsConsistentWith {U : Type u_1} {ι : Type u_2} (F : Semifilter U) (coordinates : U → ι → Bool) (point : ι → Bool) : Prop

Exact agreement on positive and negative coordinate literals. The carrier U can be the negative inputs, while point is a positive input outside this carrier.

theorem Cslib.Circuits.Fusion.Semifilter.IsConsistentWith.unique {U : Type u_1} {ι : Type u_2} {F : Semifilter U} {coordinates : U → ι → Bool} {point₁ point₂ : ι → Bool} (h₁ : F.IsConsistentWith coordinates point₁) (h₂ : F.IsConsistentWith coordinates point₂) : point₁ = point₂

A semifilter consistent with two bit vectors determines the same vector.

def Cslib.Circuits.Fusion.SemifilterWitness.IsExact {U : Type u_1} {n : ℕ} {target : Set U} {input : Fin n → Set U} {admissible : Semifilter ↑targetᶜ → Prop} (w : SemifilterWitness target input admissible) : Prop

Exact consistency strengthens the one-sided above field of a semifilter witness.

theorem Cslib.Circuits.Fusion.SemifilterWitness.isExact_iff {U : Type u_1} {n : ℕ} {target : Set U} {input : Fin n → Set U} {admissible : Semifilter ↑targetᶜ → Prop} (w : SemifilterWitness target input admissible) : w.IsExact ↔ ∀ (i : Fin n), ↑w.point ∉ input i → ¬w.filter (Subtype.val ⁻¹' input i)

Since acceptance of true inputs is already required, exactness is equivalent to rejection of every false input.

theorem Cslib.Circuits.Fusion.SemifilterWitness.isExact_of_isConsistentWith {n : ℕ} {ι : Type u_3} {target : Set (ι → Bool)} (indices : Fin n → ι) (polarities : Fin n → Bool) {admissible : Semifilter ↑targetᶜ → Prop} (w : SemifilterWitness target (fun (j : Fin n) => {x : ι → Bool | x (indices j) = polarities j}) admissible) (h : w.filter.IsConsistentWith Subtype.val ↑w.point) : w.IsExact

Exact coordinate consistency gives exactness for every supplied family of literals. The family can contain both polarities, repetitions, or only selected literals.

def Cslib.Circuits.Fusion.SemifilterWitness.observe {U : Type u_1} {n : ℕ} {target : Set U} {input : Fin n → Set U} {admissible : Semifilter ↑targetᶜ → Prop} (w : SemifilterWitness target input admissible) (s : Set U) : Set U

Observation in a single witness fiber of the extended approximation model. Away from its distinguished point, membership is unchanged.

@[simp]

theorem Cslib.Circuits.Fusion.SemifilterWitness.mem_observe_point {U : Type u_1} {n : ℕ} {target : Set U} {input : Fin n → Set U} {admissible : Semifilter ↑targetᶜ → Prop} (w : SemifilterWitness target input admissible) (s : Set U) : ↑w.point ∈ w.observe s ↔ w.filter (Subtype.val ⁻¹' s)

theorem Cslib.Circuits.Fusion.SemifilterWitness.observe_input {U : Type u_1} {n : ℕ} {target : Set U} {input : Fin n → Set U} {admissible : Semifilter ↑targetᶜ → Prop} (w : SemifilterWitness target input admissible) (h : w.IsExact) (i : Fin n) : w.observe (input i) = input i

Exact consistency makes every supplied input unchanged by observation.

theorem Cslib.Circuits.Fusion.SemifilterWitness.observe_inter_subset {U : Type u_1} {n : ℕ} {target : Set U} {input : Fin n → Set U} {admissible : Semifilter ↑targetᶜ → Prop} (w : SemifilterWitness target input admissible) (s t : Set U) : w.observe (s ∩ t) ⊆ w.observe s ∩ w.observe t

Observation accepts no more points of an intersection than the intersection of observations. Thus the approximation model has no negative intersection error.

theorem Cslib.Circuits.Fusion.SemifilterWitness.union_subset_observe {U : Type u_1} {n : ℕ} {target : Set U} {input : Fin n → Set U} {admissible : Semifilter ↑targetᶜ → Prop} (w : SemifilterWitness target input admissible) (s t : Set U) : w.observe s ∪ w.observe t ⊆ w.observe (s ∪ t)

Unions have no positive error in the observation model.

theorem Cslib.Circuits.Fusion.SemifilterWitness.inter_error {U : Type u_1} {n : ℕ} {target : Set U} {input : Fin n → Set U} {admissible : Semifilter ↑targetᶜ → Prop} (w : SemifilterWitness target input admissible) (s t : Set U) (x : U) : x ∈ (w.observe s ∩ w.observe t) \ w.observe (s ∩ t) ↔ x = ↑w.point ∧ ¬w.filter.PreservesPair (Subtype.val ⁻¹' s, Subtype.val ⁻¹' t)

Positive intersection errors occur exactly at the distinguished point and exactly when the restricted pair covers the witness semifilter.

theorem Cslib.Circuits.Fusion.SemifilterWitness.not_mem_observe_target {U : Type u_1} {n : ℕ} {target : Set U} {input : Fin n → Set U} {admissible : Semifilter ↑targetᶜ → Prop} (w : SemifilterWitness target input admissible) : ↑w.point ∉ w.observe target

The target's distinguished positive point is always an observation error.