The finite shallow-circuit construction

Lecomte and Ramakrishnan's modular tests 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.

theorem Complexity.Shallow.exists_test_layer {n d B M : ℕ} {ι : Type u_1} [Fintype ι] (k : ι → ℕ) [∀ (i : ι), NeZero (k i)] (ih : ∀ m ≤ M, ∀ (a : ℕ → Bool), ∃ (f : Layer m (d + 2)), f.size ≤ B ∧ ∀ (x : BitString m), Layer.eval AndOrOp.and f x = a (weight x)) (hm : ∀ (i : ι), 2 * (n / k i + 1) ≤ M) (t : ℕ) (s : (i : ι) → ZMod (k i) → ZMod (k i)) : ∃ (f : Layer n (d + 2)), f.size ≤ 2 + (∑ i : ι, k i ^ 2) * (B + 2) ∧ ∀ (x : BitString n), Layer.eval AndOrOp.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 Complexity.Shallow.exists_exact_layer {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 : Layer m (d + 2)), f.size ≤ B ∧ ∀ (x : BitString m), Layer.eval AndOrOp.and f x = a (weight x)) (hm : ∀ (i : ι), 2 * (n / k i + 1) ≤ M) (t : Fin (n + 1)) : ∃ (f : Layer n (d + 3)), f.size ≤ 1 + (3 ^ ∑ i : ι, k i) * (n + 1) * (2 + (∑ i : ι, k i ^ 2) * (B + 2)) ∧ ∀ (x : BitString n), Layer.eval AndOrOp.or f x = true ↔ weight x = ↑t

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

theorem Complexity.Shallow.exists_symmetric_layer_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 : Layer m (d + 2)), f.size ≤ B ∧ ∀ (x : BitString m), Layer.eval AndOrOp.and f x = a (weight x)) (hm : ∀ (i : ι), 2 * (n / k i + 1) ≤ M) (a : ℕ → Bool) (op : AndOrOp) : ∃ (f : Layer 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), Layer.eval op f x = a (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.