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. Target elements may carry natural-number masses, and 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.sum_le_mul_dictionaryCost: witness-mass bound for any wire.
• Cslib.Circuits.SumOfTerms.ceilDiv_sum_le_termCost: term-count bound from witness masses.
• Cslib.Circuits.SumOfTerms.card_le_mul_dictionaryCost: the unit-mass coverage bound.
• 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.sum_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) (mass : 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), ∑ x ∈ target ∩ support t, mass x ≤ capacity * weight t) : ∑ x ∈ target, mass x ≤ capacity * p.cost (dictionaryCost weight)

Covering a target disjoint from the supplied inputs pays for its total witness mass. Capacity zero is allowed: it forces the covered target's mass to be zero.

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_sum_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) (mass : 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), ∑ x ∈ target ∩ support t, mass x ≤ capacity) : (∑ x ∈ target, mass x) ⌈/⌉ capacity ≤ c.program.cost termCost

If each dictionary support has target mass at most a positive capacity, divide the total target mass by that capacity and round up. Other circuit outputs are unrestricted.

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.