Counting failures in a fusion cover

Every witness in a finite sample fails at some atom of a cover. The union bound therefore turns per-atom failure estimates into circuit-cost lower bounds. The witness type need not be finite, and the estimates are required only on the actual extracted atoms. In particular, restricted circuit clients may use their local degree, width or liveness hypotheses.

Witnesses may carry natural-number masses. Clearing denominators represents any finite nonnegative rational weighting this way. Unit masses recover the cardinality bounds. This is weighted union counting; it does not remove the fixed-distribution barrier for bounds over all Boolean gate pairs proved in Complexity/Computability/Circuit/Fusion/Sampling.lean.

Main definitions

• Cslib.Circuits.Fusion.Atom.failures: sampled witnesses at which preservation fails.

Main results

• Cslib.Circuits.Fusion.Cover.sum_le_mul_cost: weighted finite witness counting for a cover.
• Cslib.Circuits.Fusion.sum_le_mul_program_cost: local bounds on evaluated gates suffice.
• Cslib.Circuits.Fusion.ceilDiv_sum_le_circuit_cost: the bound for positive capacity.
• Cslib.Circuits.Fusion.Cover.card_le_mul_cost, Cslib.Circuits.Fusion.card_le_mul_program_cost, Cslib.Circuits.Fusion.ceilDiv_card_le_circuit_cost: the unit-mass specializations.

References

• Adapted from LowerBound/Fusion/Counting.lean in S. Schlesinger, Algebraic circuit formalizations in Complexitylib.

noncomputable def Cslib.Circuits.Fusion.Atom.failures {σ : Signature} {U : Type v} {W : Type w} (a : Atom σ U) (I : Interpretation σ U) (P : W → U → Prop) (samples : Finset W) : Finset W

Witnesses in samples at which the atom fails to preserve the candidate invariant.

@[simp]

theorem Cslib.Circuits.Fusion.Atom.mem_failures {σ : Signature} {U : Type v} {W : Type w} {I : Interpretation σ U} {P : W → U → Prop} {a : Atom σ U} {samples : Finset W} {t : W} : t ∈ a.failures I P samples ↔ t ∈ samples ∧ ¬a.Preserves I (P t)

A witness t belongs to a.failures I P samples if and only if t ∈ samples and a does not preserve P t under I.

theorem Cslib.Circuits.Fusion.Cover.sum_le_mul_cost {σ : Signature} {U : Type v} {W : Type w} {I : Interpretation σ U} {P : W → U → Prop} (c : Cover I P) (samples : Finset W) (mass : W → ℕ) (weight : σ.Op → ℕ) (capacity : ℕ) (hbound : ∀ (i : Fin c.size), ∑ t ∈ (c.atoms i).failures I P samples, mass t ≤ capacity * weight (c.atoms i).op) : ∑ t ∈ samples, mass t ≤ capacity * c.cost weight

Local failure-mass estimates bound the total mass of any finite sample of witnesses. Operation costs and witness masses are independent; capacity zero and zero masses are allowed.

theorem Cslib.Circuits.Fusion.Cover.card_le_mul_cost {σ : Signature} {U : Type v} {W : Type w} {I : Interpretation σ U} {P : W → U → Prop} (c : Cover I P) (samples : Finset W) (weight : σ.Op → ℕ) (capacity : ℕ) (hbound : ∀ (i : Fin c.size), ((c.atoms i).failures I P samples).card ≤ capacity * weight (c.atoms i).op) : samples.card ≤ capacity * c.cost weight

Local failure estimates on a cover bound any finite sample of its witnesses. This multiplicative form also applies when capacity is zero.

theorem Cslib.Circuits.Fusion.sum_le_mul_program_cost {σ : Signature} {U : Type v} {W : Type w} {n g : ℕ} (p : Program σ n g) (I : Interpretation σ U) (P : W → U → Prop) (samples : Finset W) (mass : W → ℕ) (input : Fin n → U) (hin : ∀ t ∈ samples, ∀ (i : Fin n), P t (input i)) (hfail : ∀ t ∈ samples, ∃ (w : Wire n g), ¬P t (p.trace I input w)) (weight : σ.Op → ℕ) (capacity : ℕ) (hbound : ∀ (k : Fin g), ∑ t ∈ (programAtoms p I input k).failures I P samples, mass t ≤ capacity * weight (p.lines k).op) : ∑ t ∈ samples, mass t ≤ capacity * p.cost weight

Count weighted failures using only the actual evaluated gates. No estimate for other semantic configurations is required, and supplied inputs must satisfy every sampled invariant.

theorem Cslib.Circuits.Fusion.card_le_mul_program_cost {σ : Signature} {U : Type v} {W : Type w} {n g : ℕ} (p : Program σ n g) (I : Interpretation σ U) (P : W → U → Prop) (samples : Finset W) (input : Fin n → U) (hin : ∀ t ∈ samples, ∀ (i : Fin n), P t (input i)) (hfail : ∀ t ∈ samples, ∃ (w : Wire n g), ¬P t (p.trace I input w)) (weight : σ.Op → ℕ) (capacity : ℕ) (hbound : ∀ (k : Fin g), ((programAtoms p I input k).failures I P samples).card ≤ capacity * weight (p.lines k).op) : samples.card ≤ capacity * p.cost weight

Count a finite sample of failed invariants using bounds on the actual evaluated gates. No estimate for other semantic configurations is required.

theorem Cslib.Circuits.Fusion.ceilDiv_sum_le_circuit_cost {σ : Signature} {U : Type v} {W : Type w} {n m : ℕ} (c : Circuit σ n m) (I : Interpretation σ U) (P : W → U → Prop) (samples : Finset W) (mass : W → ℕ) (input : Fin n → U) (hin : ∀ t ∈ samples, ∀ (i : Fin n), P t (input i)) (hfail : ∀ t ∈ samples, ∃ (o : Fin m), ¬P t (c.eval I input o)) (weight : σ.Op → ℕ) {capacity : ℕ} (hpos : 0 < capacity) (hbound : ∀ (k : Fin c.size), ∑ t ∈ (programAtoms c.program I input k).failures I P samples, mass t ≤ capacity * weight (c.program.lines k).op) : (∑ t ∈ samples, mass t) ⌈/⌉ capacity ≤ c.program.cost weight

Divide total witness mass by a positive failure capacity and round up. Each witness may fail at a different designated output, and shared gates are charged once.

theorem Cslib.Circuits.Fusion.ceilDiv_card_le_circuit_cost {σ : Signature} {U : Type v} {W : Type w} {n m : ℕ} (c : Circuit σ n m) (I : Interpretation σ U) (P : W → U → Prop) (samples : Finset W) (input : Fin n → U) (hin : ∀ t ∈ samples, ∀ (i : Fin n), P t (input i)) (hfail : ∀ t ∈ samples, ∃ (o : Fin m), ¬P t (c.eval I input o)) (weight : σ.Op → ℕ) {capacity : ℕ} (hpos : 0 < capacity) (hbound : ∀ (k : Fin c.size), ((programAtoms c.program I input k).failures I P samples).card ≤ capacity * weight (c.program.lines k).op) : samples.card ⌈/⌉ capacity ≤ c.program.cost weight

A positive capacity converts the local counting bound into a rounded-up cost bound. Each witness may fail at a different output, and shared gates are charged once.