Block comparison is symmetric after input negation

This is the recursive step in Section 4 of Lecomte and Ramakrishnan, Optimal Shallow Circuits for Majority. The difference of two block weights is, up to a constant, the weight of their concatenation after complementing the second block. Signed input substitution costs no gates and no depth.

theorem Complexity.Shallow.exists_pairComparison {n k d B M : ℕ} (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 : 2 * (n / k + 1) ≤ M) (i j si sj : ZMod k) : ∃ (f : Layer n (d + 2)), f.size ≤ B ∧ ∀ (x : BitString n), Layer.eval AndOrOp.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.