Block weights and exact-weight certificates

The arithmetic of the Lecomte--Ramakrishnan construction: 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.

def Complexity.Shallow.weight {ι : Type u_1} [Fintype ι] (x : ι → Bool) : ℕ

Hamming weight on any finite set of coordinates.

Equations

• Complexity.Shallow.weight x = ∑ i : ι, (x i).toNat

theorem Complexity.Shallow.weight_le {ι : Type u_1} [Fintype ι] (x : ι → Bool) : weight x ≤ Fintype.card ι

theorem Complexity.Shallow.weight_not_add {ι : Type u_1} [Fintype ι] (x : ι → Bool) : (weight fun (i : ι) => !x i) + weight x = Fintype.card ι

Complementary strings have weights adding to their length.

def Complexity.Shallow.blockWeight {ι : Type u_1} {G : Type u_2} [Fintype ι] [DecidableEq G] (block : ι → G) (x : ι → Bool) (a : G) : ℕ

The weight of a partition block.

Equations

• Complexity.Shallow.blockWeight block x a = Complexity.Shallow.weight fun (i : { i : ι // block i = a }) => x ↑i

theorem Complexity.Shallow.sum_blockWeight {ι : Type u_1} {G : Type u_2} [Fintype ι] [Fintype G] [DecidableEq G] (block : ι → G) (x : ι → Bool) : ∑ a : G, blockWeight block x a = weight x

Summing the block weights recovers the total weight.

def Complexity.Shallow.residueBlock {n k : ℕ} (i : Fin n) : ZMod k

Round-robin partition into k residue classes.

Equations

• Complexity.Shallow.residueBlock i = ↑↑i

theorem Complexity.Shallow.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 Complexity.Shallow.weight_pair_not_add {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (x : ι → Bool) (y : κ → Bool) : weight (Sum.elim x fun (j : κ) => !y j) + weight y = 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 Complexity.Shallow.modEq_prod {ι : Type u_1} [Fintype ι] (k : ι → ℕ) (hc : Pairwise fun (i j : ι) => (k i).Coprime (k j)) {a b : ℕ} (h : ∀ (i : ι), a ≡ b [MOD k i]) : a ≡ b [MOD ∏ i : ι, k i]

Pairwise coprime modular equalities combine into equality modulo the product.

theorem Complexity.Shallow.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)) : weight x = ↑t

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