Support coverage by dictionary circuits

Interpret addition as finite-set union and a dictionary term as its prescribed support. Nonmembership of a target element is preserved by addition, so every covered target element must first appear at a dictionary gate. A local coverage bound therefore gives a weighted dictionary-cost lower bound. Shared gates are counted once; free supplied inputs must be disjoint from the target. The ambient support type may be infinite.

These are circuits of supports, with union as the operation. Applying the result to polynomial supports requires a separate semantic bridge; cancellation is not silently treated as union.

Main definitions

• Cslib.Circuits.SumOfTerms.supportInterpretation: dictionary supports with union gates.

Main results

• Cslib.Circuits.SumOfTerms.card_le_mul_dictionaryCost: weighted coverage bound for any wire.
• Cslib.Circuits.SumOfTerms.ceilDiv_card_le_termCost: term-count bound for any selected output.
• Cslib.Circuits.SumOfTerms.card_le_termCost_of_separated: one term per target element when each dictionary support meets the target in at most one element.

References

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

def Cslib.Circuits.SumOfTerms.supportInterpretation {T : Type u} {M : Type v} [DecidableEq M] (support : T → Finset M) : Interpretation (signature T) (Finset M)

Interpret dictionary terms by finite supports and addition by union.

@[simp]

theorem Cslib.Circuits.SumOfTerms.failures_support_add {T : Type u} {M : Type v} [DecidableEq M] (support : T → Finset M) (target : Finset M) (args : Fin 2 → Finset M) : { op := Op.add, arguments := args }.failures (supportInterpretation support) (fun (t : M) (s : Finset M) => t ∉ s) target = ∅

Union cannot introduce an element absent from both arguments.

@[simp]

theorem Cslib.Circuits.SumOfTerms.failures_support_term {T : Type u} {M : Type v} [DecidableEq M] (support : T → Finset M) (target : Finset M) (t : T) (args : Fin 0 → Finset M) : { op := Op.term t, arguments := args }.failures (supportInterpretation support) (fun (t : M) (s : Finset M) => t ∉ s) target = target ∩ support t

A nullary dictionary gate fails exactly at the target elements in its support.

theorem Cslib.Circuits.SumOfTerms.card_le_mul_dictionaryCost {T : Type u} {M : Type v} [DecidableEq M] {n g : ℕ} (p : Program (signature T) n g) (support : T → Finset M) (input : Fin n → Finset M) (target : Finset M) (hin : ∀ (i : Fin n), Disjoint target (input i)) (w : Wire n g) (hout : target ⊆ p.trace (supportInterpretation support) input w) (weight : T → ℕ) (capacity : ℕ) (hbound : ∀ (t : T), (target ∩ support t).card ≤ capacity * weight t) : target.card ≤ capacity * p.cost (dictionaryCost weight)

Covering a target disjoint from the supplied inputs costs enough to pay for its elements. Capacity zero is allowed: it forces the covered target to be empty.

theorem Cslib.Circuits.SumOfTerms.ceilDiv_card_le_termCost {T : Type u} {M : Type v} [DecidableEq M] {n m : ℕ} (c : Circuit (signature T) n m) (support : T → Finset M) (input : Fin n → Finset M) (target : Finset M) (hin : ∀ (i : Fin n), Disjoint target (input i)) (o : Fin m) (hout : target ⊆ c.eval (supportInterpretation support) input o) {capacity : ℕ} (hpos : 0 < capacity) (hbound : ∀ (t : T), (target ∩ support t).card ≤ capacity) : target.card ⌈/⌉ capacity ≤ c.program.cost termCost

If each dictionary support covers at most capacity target elements, divide the target size by that positive capacity and round up. Other circuit outputs are unrestricted.

theorem Cslib.Circuits.SumOfTerms.card_le_termCost_of_separated {T : Type u} {M : Type v} [DecidableEq M] {n m : ℕ} (c : Circuit (signature T) n m) (support : T → Finset M) (input : Fin n → Finset M) (target : Finset M) (hin : ∀ (i : Fin n), Disjoint target (input i)) (o : Fin m) (hout : target ⊆ c.eval (supportInterpretation support) input o) (hbound : ∀ (t : T), (target ∩ support t).card ≤ 1) : target.card ≤ c.program.cost termCost

A dictionary whose terms cover at most one target element needs at least target.card terms, even when terms are shared by several additions.