Block weights and exact-weight certificates

The arithmetic of the construction of Lecomte and Ramakrishnan [LR26]: partitioning input bits preserves their total weight, a residue class partition has small blocks, and coprime modular certificates determine the exact weight. Complementing one block turns a difference of block weights into a symmetric function.

Main definitions

• Cslib.Circuits.Boolean.ShallowSymmetric.blockWeight: the weight of a block of a partition.
• Cslib.Circuits.Boolean.ShallowSymmetric.residueBlock: the partition into residue classes.

Main results

• Cslib.Circuits.Boolean.ShallowSymmetric.sum_blockWeight: block weights sum to the weight.
• Cslib.Circuits.Boolean.ShallowSymmetric.weight_eq_of_shiftTests: accepting tests modulo coprime moduli of product larger than n certify the exact weight.

References

• V. Lecomte, P. Ramakrishnan, Optimal Shallow Circuits for Majority

def Cslib.Circuits.Boolean.ShallowSymmetric.blockWeight {ι : Type u_1} {G : Type u_2} [Fintype ι] [DecidableEq G] (block : ι → G) (x : ι → Bool) (a : G) : ℕ

The weight of a partition block.

theorem Cslib.Circuits.Boolean.ShallowSymmetric.sum_blockWeight {ι : Type u_1} {G : Type u_2} [Fintype ι] [Fintype G] [DecidableEq G] (block : ι → G) (x : ι → Bool) : ∑ a : G, blockWeight block x a = BitString.weight x

Summing the block weights recovers the total weight.

def Cslib.Circuits.Boolean.ShallowSymmetric.residueBlock {n k : ℕ} (i : Fin n) : ZMod k

Round-robin partition into k residue classes.

theorem Cslib.Circuits.Boolean.ShallowSymmetric.card_residueBlock_le (n k : ℕ) (a : ZMod k) : Fintype.card { i : Fin n // residueBlock i = a } ≤ n / k + 1

Every residue block has at most n/k + 1 positions.

theorem Cslib.Circuits.Boolean.ShallowSymmetric.weight_pair_not_add {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (x : ι → Bool) (y : κ → Bool) : BitString.weight (Sum.elim x fun (j : κ) => !y j) + BitString.weight y = BitString.weight x + Fintype.card κ

A pair of blocks, with the second block complemented, has weight left + length(right) - right. The additive form avoids natural subtraction.

theorem Cslib.Circuits.Boolean.ShallowSymmetric.weight_eq_of_shiftTests {n : ℕ} {ι : Type u_1} [Fintype ι] (k : ι → ℕ) [∀ (i : ι), NeZero (k i)] (hc : Pairwise fun (i j : ι) => (k i).Coprime (k j)) (hn : n < ∏ i : ι, k i) (t : Fin (n + 1)) (x : BitString n) (s : (i : ι) → ZMod (k i) → ZMod (k i)) (hs : ∀ (i : ι), ShiftTest (↑↑t) (fun (a : ZMod (k i)) => ↑(blockWeight residueBlock x a)) (s i)) : BitString.weight x = ↑t

Modular certificates over coprime moduli larger in product than the input length certify the exact Hamming weight.