The finite shallow-circuit construction

The modular tests of Lecomte and Ramakrishnan [LR26] are conjunctions of symmetric two-block comparisons after signed input substitution. Their output AND gates can be merged, retaining the depth of a comparison. A small covering family of these tests is then joined by one OR layer.

Main results

• Cslib.Circuits.Boolean.ShallowSymmetric.exists_pairComparison: one comparison of two blocks.
• Cslib.Circuits.Boolean.ShallowSymmetric.exists_exact_altFormula: the exact-weight tests.
• Cslib.Circuits.Boolean.ShallowSymmetric.exists_symmetric_altFormula_succ: one step of the depth induction.

References

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

theorem Cslib.Circuits.Boolean.ShallowSymmetric.exists_pairComparison {n k d B M : ℕ} (ih : ∀ m ≤ M, ∀ (a : ℕ → Bool), ∃ (f : AltFormula m (d + 2)), f.size ≤ B ∧ ∀ (x : BitString m), AltFormula.eval AltOp.and f x = a (BitString.weight x)) (hm : 2 * (n / k + 1) ≤ M) (i j si sj : ZMod k) : ∃ (f : AltFormula n (d + 2)), f.size ≤ B ∧ ∀ (x : BitString n), AltFormula.eval AltOp.and f x = decide (↑(blockWeight residueBlock x i) + si ≠ ↑(blockWeight residueBlock x j) + sj)

Lift a symmetric synthesis bound to one modular comparison of two blocks.

theorem Cslib.Circuits.Boolean.ShallowSymmetric.exists_test_altFormula {n d B M : ℕ} {ι : Type u_1} [Fintype ι] (k : ι → ℕ) [∀ (i : ι), NeZero (k i)] (ih : ∀ m ≤ M, ∀ (a : ℕ → Bool), ∃ (f : AltFormula m (d + 2)), f.size ≤ B ∧ ∀ (x : BitString m), AltFormula.eval AltOp.and f x = a (BitString.weight x)) (hm : ∀ (i : ι), 2 * (n / k i + 1) ≤ M) (t : ℕ) (s : (i : ι) → ZMod (k i) → ZMod (k i)) : ∃ (f : AltFormula n (d + 2)), f.size ≤ 2 + (∑ i : ι, k i ^ 2) * (B + 2) ∧ ∀ (x : BitString n), AltFormula.eval AltOp.and f x = true ↔ ∀ (i : ι), ShiftTest (↑t) (fun (a : ZMod (k i)) => ↑(blockWeight residueBlock x a)) (s i)

Synthesize a simultaneous modular test without increasing the comparison depth. The bound counts all ordered pairs, including harmless diagonal pairs.

theorem Cslib.Circuits.Boolean.ShallowSymmetric.exists_exact_altFormula {n d B M : ℕ} {ι : Type u_1} [Fintype ι] (k : ι → ℕ) [∀ (i : ι), NeZero (k i)] (hc : Pairwise fun (i j : ι) => (k i).Coprime (k j)) (hn : n < ∏ i : ι, k i) (ih : ∀ m ≤ M, ∀ (a : ℕ → Bool), ∃ (f : AltFormula m (d + 2)), f.size ≤ B ∧ ∀ (x : BitString m), AltFormula.eval AltOp.and f x = a (BitString.weight x)) (hm : ∀ (i : ι), 2 * (n / k i + 1) ≤ M) (t : Fin (n + 1)) : ∃ (f : AltFormula n (d + 3)), f.size ≤ 1 + (3 ^ ∑ i : ι, k i) * (n + 1) * (2 + (∑ i : ι, k i ^ 2) * (B + 2)) ∧ ∀ (x : BitString n), AltFormula.eval AltOp.or f x = true ↔ BitString.weight x = ↑t

Exact-weight circuits obtained by covering every valid input with modular tests and placing one OR above the test family.

theorem Cslib.Circuits.Boolean.ShallowSymmetric.exists_symmetric_altFormula_succ {n d B M : ℕ} {ι : Type u_1} [Fintype ι] (k : ι → ℕ) [∀ (i : ι), NeZero (k i)] (hc : Pairwise fun (i j : ι) => (k i).Coprime (k j)) (hn : n < ∏ i : ι, k i) (ih : ∀ m ≤ M, ∀ (a : ℕ → Bool), ∃ (f : AltFormula m (d + 2)), f.size ≤ B ∧ ∀ (x : BitString m), AltFormula.eval AltOp.and f x = a (BitString.weight x)) (hm : ∀ (i : ι), 2 * (n / k i + 1) ≤ M) (a : ℕ → Bool) (op : AltOp) : ∃ (f : AltFormula n (d + 3)), f.size ≤ 1 + (n + 1) * (1 + (3 ^ ∑ i : ι, k i) * (n + 1) * (2 + (∑ i : ι, k i ^ 2) * (B + 2))) ∧ ∀ (x : BitString n), AltFormula.eval op f x = a (BitString.weight x)

The explicit finite recurrence for symmetric functions, in both output polarities. The constants in the asymptotic theorem are extracted from this bound, after choosing the moduli.