Uniform aggregation of counting functions

Unary polynomial-time bounds permit a single verifier to aggregate an input-dependent number of factors or summands. Padding certificates with false bits preserves counts exactly. Signed products maintain two Boolean states, whose difference multiplies the signed contribution of each block. This gives variable powers of GapP functions, not just fixed subring powers.

Main results

• SharpP.sum_bits_mem, GapP.sum_bits_mem: sum over all words of a computed unary length.
• GapP.pow_mem_polyTime: an input-dependent unary exponent preserves GapP.

References

• S. Fenner, L. Fortnow, S. Kurtz, Gap-definable counting classes.

theorem Cslib.Complexity.SharpP.sum_bits_mem {α : Type} {enc : α ↪ List Bool} {f : α × List Bool → ℕ} {r : α → ℕ} (hf : f ∈ SharpP (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits)) (hr : Turing.MultiTapeTM.ComputableInPolyTime r enc Turing.MultiTapeTM.encUnary) : (fun (a : α) => ∑ w : Fin (r a) → Bool, f (a, List.ofFn w)) ∈ SharpP enc

Summing a uniform #P family over all words of a polynomial-time unary length preserves #P.

theorem Cslib.Complexity.GapP.sum_bits_mem {α : Type} {enc : α ↪ List Bool} {g : α × List Bool → ℤ} {r : α → ℕ} (hg : g ∈ GapP (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits)) (hr : Turing.MultiTapeTM.ComputableInPolyTime r enc Turing.MultiTapeTM.encUnary) : (fun (a : α) => ∑ w : Fin (r a) → Bool, g (a, List.ofFn w)) ∈ GapP enc

GapP is closed under summing over all words of a polynomial-time unary length.

@[reducible, inline]

abbrev Cslib.Complexity.SignedProduct.State : Type

Positive and negative acceptance flags for a partial product.

def Cslib.Complexity.SignedProduct.mul (s t : State) : State

Multiplication of signed Boolean flags; overlap cancels in their difference.

def Cslib.Complexity.SignedProduct.verifier {α : Type} (r k : α → ℕ) (V W : α × List Bool → Bool) (b : Bool) (x : α × List Bool) : Bool

Count products of signed row contributions by two ordinary verifiers.

theorem Cslib.Complexity.SignedProduct.count_sub {α : Type} (r k : α → ℕ) (V W : α × List Bool → Bool) (a : α) : ↑(acceptCount (verifier r k V W false) a (r a * k a)) - ↑(acceptCount (verifier r k V W true) a (r a * k a)) = (↑(acceptCount V a (k a)) - ↑(acceptCount W a (k a))) ^ r a

The difference of the row-product counts is the power of the original difference.

theorem Cslib.Complexity.GapP.pow_mem_polyTime {α : Type} {enc : α ↪ List Bool} {g : α → ℤ} {r : α → ℕ} (hg : g ∈ GapP enc) (hr : Turing.MultiTapeTM.ComputableInPolyTime r enc Turing.MultiTapeTM.encUnary) : (fun (a : α) => g a ^ r a) ∈ GapP enc

A GapP function raised to an input-dependent polynomial-time unary exponent is in GapP.