Shifted distinctness tests

The counting argument of Victor Lecomte and Prasanna Ramakrishnan, Optimal Shallow Circuits for Majority, arXiv:2609.34029v1, 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.

def Complexity.Shallow.residueSum (G : Type u_2) [Fintype G] [AddCommGroup G] : G

Sum of all residues of the finite group.

Equations

• Complexity.Shallow.residueSum G = ∑ a : G, a

def Complexity.Shallow.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.

Equations

• Complexity.Shallow.ShiftTest t w s = (∑ i : G, s i = Complexity.Shallow.residueSum G - t ∧ Function.Injective fun (i : G) => w i + s i)

theorem Complexity.Shallow.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.

theorem Complexity.Shallow.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.

noncomputable def Complexity.Shallow.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.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.Shallow.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.

theorem Complexity.Shallow.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.

theorem Complexity.Shallow.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.