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.

Main definitions

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

Main results

• Cslib.Circuits.Fusion.Cover.card_le_mul_cost: finite witness counting for a cover.
• Cslib.Circuits.Fusion.card_le_mul_program_cost: local bounds on evaluated gates suffice.
• Cslib.Circuits.Fusion.ceilDiv_card_le_circuit_cost: the bound for positive capacity.

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)

theorem Cslib.Circuits.Fusion.card_le_sum_failures {σ : Signature} {U : Type v} {W : Type w} {k : ℕ} {I : Interpretation σ U} {P : W → U → Prop} (atoms : Fin k → Atom σ U) (samples : Finset W) (hcover : ∀ t ∈ samples, ¬∀ (i : Fin k), (atoms i).Preserves I (P t)) : samples.card ≤ ∑ i : Fin k, ((atoms i).failures I P samples).card

The sampled witnesses are covered by the union of the atoms' failures.

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.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_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.