Hamming-far functions that share their computation

Two distinct coordinate projections x_i and x_j differ on half of the inputs, and so do their shifts g_i = f + x_i and g_j = f + x_j by any common Boolean function f (Cslib.BitString.two_mul_hammingDist_add_proj). Statistically the shifts are as far apart as two independent random functions, yet they share almost all of their computation. In the De Morgan basis, where an exclusive or costs four gates:

• each shift costs at most four gates more than f (Cslib.Circuits.Boolean.complexity_add_proj_le);
• all m shifts x ↦ f x + x_{i o} together cost at most C(f) + 4 m: compute f once, then one exclusive or per output (Cslib.Circuits.Boolean.complexity_add_projs_le);
• the computational Hamming distance of two shifts is that of the two projections (Cslib.Circuits.Boolean.circuitDist_add_proj), which lies between five and eight for distinct projections (Cslib.Circuits.Boolean.five_le_circuitDist_proj, Cslib.Circuits.Boolean.circuitDist_proj_le).

Statistical disagreement therefore does not certify computational independence, while the computational distance Cslib.Circuits.Boolean.circuitDist sees the shared part. Pairwise computational distance alone still says nothing about direct sums.

Main results

• Cslib.Circuits.Boolean.complexity_add_proj_le: one shift costs at most four more gates.
• Cslib.Circuits.Boolean.complexity_add_projs_le: m shifts cost at most C(f) + 4 m.
• Cslib.Circuits.Boolean.circuitDist_add_proj, Cslib.Circuits.Boolean.circuitDist_proj_le, Cslib.Circuits.Boolean.five_le_circuitDist_proj: shifts are at computational distance between five and eight.

References

• S. Jukna, Boolean Function Complexity: Advances and Frontiers

theorem Cslib.Circuits.Boolean.complexity_add_proj_le {n : ℕ} (f : BooleanFunction n) (i : Fin n) : complexity interpretation (single (f + fun (x : BitString n) => x i)) ≤ complexity interpretation (single f) + 4

Adding a coordinate to f costs at most four gates more than f.

theorem Cslib.Circuits.Boolean.complexity_add_projs_le {n m : ℕ} (f : BooleanFunction n) (i : Fin m → Fin n) : (complexity interpretation fun (x : Fin n → Bool) (o : Fin m) => f x + x (i o)) ≤ complexity interpretation (single f) + 4 * m

Joint complexity of shifts. The m functions x ↦ f x + x_{i o} together cost at most four gates each more than f: compute f once beside the inputs, then one exclusive or per output.

theorem Cslib.Circuits.Boolean.circuitDist_add_proj {n : ℕ} (f : BooleanFunction n) (i j : Fin n) : circuitDist (f + fun (x : BitString n) => x i) (f + fun (x : BitString n) => x j) = circuitDist (fun (x : BitString n) => x i) fun (x : BitString n) => x j

Shifting two projections by the same f keeps their computational Hamming distance.

theorem Cslib.Circuits.Boolean.circuitDist_proj_le {n : ℕ} (i j : Fin n) : (circuitDist (fun (x : BitString n) => x i) fun (x : BitString n) => x j) ≤ 8

Two coordinate projections are at computational Hamming distance at most eight.

theorem Cslib.Circuits.Boolean.five_le_circuitDist_proj {n : ℕ} {i j : Fin n} (hij : i ≠ j) : 5 ≤ circuitDist (fun (x : BitString n) => x i) fun (x : BitString n) => x j

Two distinct coordinate projections are at computational Hamming distance at least five: their exclusive or is not a projection.