The fixed-distribution counting barrier for Fusion

An explicit distribution on pairs covers each semifilter accepting the literals of a positive input with probability at least 1 / (8 * n + 8). Averaging against any fixed nonnegative weighted family of witnesses gives a pair of at least that relative mass. Consequently the reciprocal of a uniform bound on covered probability is at most 8 * n + 8.

This formalizes the conclusions of [Oliveira2018Approximation, Lemma 3 and Theorem 6], following [Raz89], by a direct cylinder argument adapted from their random-function proof. Exact literal consistency is not needed: acceptance of the matching literal for each coordinate suffices. The pair sampler is fixed before the witness is chosen. The conclusion bounds this fixed-distribution counting certificate, not pair-cover complexity or circuit complexity; certificates whose capacity constraint ranges only over a particular circuit's gate pairs are outside its scope.

For a random full truth table h and a positive input v, reveal the coordinates of the negative input one at a time, leaving the remaining coordinates fixed to v. When h(v) is true but the semifilter rejects the final truth set, some adjacent cylinders lose acceptance. Intersecting the previous cylinder with the matching literal gives a covering pair. A suffix bit flip shows that each cylinder has the same marginal law as a cylinder with zero suffix. Independently flipping the truth-table entry at v shows that the error probability is half the rejection probability, because v is outside the negative carrier. Pairing a random set with its complement accounts for the remaining probability. Union bounds and averaging give the stated constant. No efficient sampling or construction bound is asserted.

Main definitions

• Cslib.Circuits.Fusion.booleanPairSample: the fixed finite sampler, including the complementary-set case.

Main results

• Cslib.Circuits.Fusion.le_booleanPairSample_expect: the random-pair guarantee, with the sampling lemma proved.
• Cslib.Circuits.Fusion.exists_pair_weight_ge: weighted double counting against any finite witness family.
• Cslib.Circuits.Fusion.fixedDistribution_counting_bound: positivity of capacity and the reciprocal bound 8n+8.

References

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

def Cslib.Circuits.Fusion.booleanPairSample {n : ℕ} (target : Set (Fin n → Bool)) (level : Option (Fin n)) (b : Bool) (h : (Fin n → Bool) → Bool) : Set ↑targetᶜ × Set ↑targetᶜ

A fixed sampler for pairs over the negative inputs. Sample its three arguments independently and uniformly: a coordinate or the extra complement case, a polarity, and a full truth table. The sampler depends on the target, but not on any witness or distribution of witnesses.

theorem Cslib.Circuits.Fusion.le_booleanPairSample_expect {n : ℕ} {target : Set (Fin n → Bool)} (F : Semifilter ↑targetᶜ) (v : ↑target) (hv : ∀ (i : Fin n), F {x : ↑targetᶜ | ↑x i = ↑v i}) : 1 / (8 * ↑n + 8) ≤ Finset.univ.expect fun (level : Option (Fin n)) => Finset.univ.expect fun (b : Bool) => Finset.univ.expect fun (h : (Fin n → Bool) → Bool) => if ¬F.PreservesPair (booleanPairSample target level b h) then 1 else 0

Uniformly sampling the level, polarity, and full truth table covers every matching-literal semifilter with probability at least 1/(8n+8). The target may be arbitrary; existence of the positive point and semifilter provides the nontriviality needed by the proof.

theorem Cslib.Circuits.Fusion.exists_pair_weight_ge {n : ℕ} {target : Set (Fin n → Bool)} {W : Type u_1} [Fintype W] (F : W → Semifilter ↑targetᶜ) (v : W → ↑target) (hv : ∀ (w : W) (i : Fin n), (F w) {x : ↑targetᶜ | ↑x i = ↑(v w) i}) (μ : W → ℝ) (hμ : ∀ (w : W), 0 ≤ μ w) : ∃ (p : Set ↑targetᶜ × Set ↑targetᶜ), (∑ w : W, μ w) / (8 * ↑n + 8) ≤ ∑ w : W, μ w * if ¬(F w).PreservesPair p then 1 else 0

For any nonnegative weights on a finite family of matching-literal witnesses, some pair covers at least 1/(8n+8) of their total weight. No normalization is required.

theorem Cslib.Circuits.Fusion.fixedDistribution_counting_bound {n : ℕ} {target : Set (Fin n → Bool)} {W : Type u_1} [Fintype W] (F : W → Semifilter ↑targetᶜ) (v : W → ↑target) (hv : ∀ (w : W) (i : Fin n), (F w) {x : ↑targetᶜ | ↑x i = ↑(v w) i}) (μ : W → ℝ) (hμ : ∀ (w : W), 0 ≤ μ w) (hprob : ∑ w : W, μ w = 1) {d : ℝ} (hd : ∀ (p : Set ↑targetᶜ × Set ↑targetᶜ), (∑ w : W, μ w * if ¬(F w).PreservesPair p then 1 else 0) ≤ d) : 0 < d ∧ 1 / d ≤ 8 * ↑n + 8

A fixed probability distribution on matching-literal witnesses cannot give a reciprocal pair-capacity certificate larger than 8n+8. In particular its maximum covered probability is positive. This does not bound the minimum number of pairs covering the witnesses.