Documentation

Complexity.Computability.Circuit.Boolean.ShallowSymmetric.ShiftTest

Shifted distinctness tests #

The counting argument of Lecomte and Ramakrishnan, Sections 3 and 4.

A test shifts one weight per group element and checks that all shifted weights are distinct. The prescribed sum of shifts makes this a one-sided certificate for the sum of the weights. For each valid weight vector, the accepting shifts are in bijection with permutations of the group, so there are exactly |G|!.

We sample from all |G| ^ |G| shifts and reject shifts with the wrong sum. The paper instead samples only shifts with the prescribed sum. This slightly weaker success density still gives the same exponential bound and avoids a conditional sampling space. The argument works for any finite abelian group; the circuit construction uses ZMod k.

Main definitions #

Main results #

References #

source
def Cslib.Circuits.Boolean.ShallowSymmetric.residueSum (G : Type u_2) [Fintype G] [AddCommGroup G] :
G

Sum of all residues of the finite group.

Instances For
    source
    def Cslib.Circuits.Boolean.ShallowSymmetric.ShiftTest {G : Type u_1} [Fintype G] [AddCommGroup G] (t : G) (w s : G → G) :
    Prop

    A shifted distinctness test certifying the target sum t.

    Instances For
      source
      theorem Cslib.Circuits.Boolean.ShallowSymmetric.ShiftTest.sound {G : Type u_1} [Fintype G] [AddCommGroup G] {t : G} {w s : G → G} (h : ShiftTest t w s) :
      ∑ i : G, w i = t

      Passing a shifted distinctness test certifies the sum of the weights.

      source
      theorem Cslib.Circuits.Boolean.ShallowSymmetric.shiftTest_perm {G : Type u_1} [Fintype G] [AddCommGroup G] {t : G} (w : G → G) (hw : ∑ i : G, w i = t) (e : Equiv.Perm G) :
      ShiftTest t w fun (i : G) => e i - w i

      For a valid weight vector, choosing a permutation determines the shifts.

      source
      noncomputable def Cslib.Circuits.Boolean.ShallowSymmetric.acceptingShiftsEquiv {G : Type u_1} [Fintype G] [AddCommGroup G] {t : G} (w : G → G) (hw : ∑ i : G, w i = t) :
      { s : G → G // ShiftTest t w s } ≃ Equiv.Perm G

      Accepting shifts are precisely permutations translated by the weight vector.

      Instances For
        source
        theorem Cslib.Circuits.Boolean.ShallowSymmetric.card_acceptingShifts {G : Type u_1} [Fintype G] [AddCommGroup G] {t : G} (w : G → G) (hw : ∑ i : G, w i = t) :
        Nat.card { s : G → G // ShiftTest t w s } = (Fintype.card G).factorial

        Exactly |G|! shifts accept each weight vector with the target sum.

        source
        theorem Cslib.Circuits.Boolean.ShallowSymmetric.exists_shiftTest_iff {G : Type u_1} [Fintype G] [AddCommGroup G] (t : G) (w : G → G) :
        (∃ (s : G → G), ShiftTest t w s) ↔ ∑ i : G, w i = t

        Some test accepts a weight vector exactly when its sum is the target.

        source
        theorem Cslib.Circuits.Boolean.ShallowSymmetric.shiftTest_iff_pairwise {G : Type u_1} [Fintype G] [AddCommGroup G] (t : G) (w s : G → G) :
        ShiftTest t w s ↔ ∑ i : G, s i = residueSum G - t ∧ ∀ (i j : G), i ≠ j → w i + s i ≠ w j + s j

        Distinctness is a conjunction of constraints involving only two weights.