The computational Hamming metric

Boolean functions on n inputs form a group under the exclusive or, which is the addition of Mathlib's Boolean ring Bool, taken pointwise: (f + g) x = f x ^^ g x. The computational Hamming distance Cslib.Circuits.Boolean.circuitDist f g is 0 when f = g, and otherwise the De Morgan circuit complexity of f + g plus four, the cost of an exclusive or (Cslib.Circuits.Boolean.circuitDist_def). It is the difference distance of Complexity.Computability.Circuit.Metric for the De Morgan interpretation with c = 4, by definition (Cslib.Circuits.Boolean.circuitDist_eq_diffDist), since f - g = f + g and -f = f.

It is a translation-invariant metric: f + h = (f + g) + (g + h) gives the triangle inequality from C(f ⊕ h) ≤ C(f ⊕ g) + C(g ⊕ h) + 4. Circuit complexity is 1-Lipschitz for it, |C(f) - C(g)| ≤ circuitDist f g (Cslib.Circuits.Boolean.dist_complexity_single_le_circuitDist), which is the correction bound |C(f) - C(g)| ≤ C(f ⊕ g) + 4 of Cslib.Circuits.Boolean.dist_complexity_single_le_complexity_xor [Juk12]. Unlike the normalized Hamming distance, it does not separate functions that differ on many inputs but in a simple way: two functions whose exclusive or is a projection are at distance four.

The same quantity is a norm, 0 at 0 and C(f) + 4 otherwise (Cslib.Circuits.Boolean.circuitNorm), and induces the metric (Cslib.Circuits.Boolean.dist_circuitNormedAddCommGroup). The normed group is a definition, not an instance, since BooleanFunction n is a function type. Apart from the zero function and the offset, the minimum circuit size problem asks for membership in balls about zero: C(f) ≤ s exactly when f lies in the closed ball of radius s + 4 about 0 (Cslib.Circuits.Boolean.complexity_single_le_iff_mem_closedBall).

Main definitions

• Cslib.Circuits.Boolean.circuitDist: the computational Hamming distance.
• Cslib.Circuits.Boolean.circuitNorm: the corresponding norm.
• Cslib.Circuits.Boolean.circuitNormedAddCommGroup: the induced normed group, as a definition.

Main results

• Cslib.Circuits.Boolean.circuitDist_eq_zero_iff, Cslib.Circuits.Boolean.circuitDist_comm, Cslib.Circuits.Boolean.circuitDist_triangle: a metric.
• Cslib.Circuits.Boolean.circuitDist_add_right, Cslib.Circuits.Boolean.circuitDist_add_left: translation invariance.
• Cslib.Circuits.Boolean.dist_complexity_single_le_circuitDist: complexity is 1-Lipschitz.
• Cslib.Circuits.Boolean.complexity_single_le_iff_circuitDist_le, Cslib.Circuits.Boolean.complexity_single_le_iff_mem_closedBall: complexity bounds as balls.

References

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

The group operations as circuits

theorem Cslib.Circuits.Boolean.complexity_single_add_le : complexity interpretation (single fun (y : Fin 2 → Bool) => y 0 + y 1) ≤ 4

Adding two inputs, an exclusive or, costs four De Morgan gates.

theorem Cslib.Circuits.Boolean.complexity_single_neg {n : ℕ} (f : BooleanFunction n) : complexity interpretation (single (-f)) = complexity interpretation (single f)

Negation is the identity on Boolean functions, so it leaves complexity unchanged.

The computational Hamming distance

noncomputable def Cslib.Circuits.Boolean.circuitDist {n : ℕ} (f g : BooleanFunction n) : ℕ

The computational Hamming distance: 0 if f = g, and otherwise the complexity of f + g, the inputs where f and g differ, plus four.

theorem Cslib.Circuits.Boolean.circuitDist_eq_diffDist {n : ℕ} (f g : BooleanFunction n) : circuitDist f g = diffDist interpretation 4 f g

The computational Hamming distance is the difference distance with c = 4.

theorem Cslib.Circuits.Boolean.circuitDist_def {n : ℕ} (f g : BooleanFunction n) : circuitDist f g = if f = g then 0 else complexity interpretation (single (f + g)) + 4

@[simp]

theorem Cslib.Circuits.Boolean.circuitDist_self {n : ℕ} (f : BooleanFunction n) : circuitDist f f = 0

theorem Cslib.Circuits.Boolean.circuitDist_of_ne {n : ℕ} {f g : BooleanFunction n} (h : f ≠ g) : circuitDist f g = complexity interpretation (single fun (x : Fin n → Bool) => f x ^^ g x) + 4

Distinct functions are at distance the complexity of their exclusive or plus four.

theorem Cslib.Circuits.Boolean.circuitDist_eq_zero_iff {n : ℕ} {f g : BooleanFunction n} : circuitDist f g = 0 ↔ f = g

theorem Cslib.Circuits.Boolean.circuitDist_comm {n : ℕ} (f g : BooleanFunction n) : circuitDist f g = circuitDist g f

theorem Cslib.Circuits.Boolean.circuitDist_triangle {n : ℕ} (f g h : BooleanFunction n) : circuitDist f h ≤ circuitDist f g + circuitDist g h

The triangle inequality, from the cost of an exclusive or.

@[simp]

theorem Cslib.Circuits.Boolean.circuitDist_add_right {n : ℕ} (f g a : BooleanFunction n) : circuitDist (f + a) (g + a) = circuitDist f g

@[simp]

theorem Cslib.Circuits.Boolean.circuitDist_add_left {n : ℕ} (a f g : BooleanFunction n) : circuitDist (a + f) (a + g) = circuitDist f g

theorem Cslib.Circuits.Boolean.dist_complexity_single_le_circuitDist {n : ℕ} (f g : BooleanFunction n) : (complexity interpretation (single f)).dist (complexity interpretation (single g)) ≤ circuitDist f g

Circuit complexity is 1-Lipschitz for the computational Hamming distance.

The norm

noncomputable def Cslib.Circuits.Boolean.circuitNorm (n : ℕ) : AddGroupNorm (BooleanFunction n)

The computational Hamming norm: 0 at 0, and otherwise the complexity plus four.

theorem Cslib.Circuits.Boolean.circuitNorm_apply {n : ℕ} (f : BooleanFunction n) : (circuitNorm n) f = ↑(circuitDist f 0)

@[reducible, inline]

noncomputable abbrev Cslib.Circuits.Boolean.circuitNormedAddCommGroup (n : ℕ) : NormedAddCommGroup (BooleanFunction n)

The normed group of Boolean functions with the computational Hamming norm. This is a definition, not an instance, since BooleanFunction n is a function type.

theorem Cslib.Circuits.Boolean.dist_circuitNormedAddCommGroup {n : ℕ} (f g : BooleanFunction n) : dist f g = ↑(circuitDist f g)

The normed group induces the computational Hamming distance.

Complexity bounds as balls

theorem Cslib.Circuits.Boolean.complexity_single_le_iff_circuitDist_le {n : ℕ} {f : BooleanFunction n} (hf : f ≠ 0) (s : ℕ) : complexity interpretation (single f) ≤ s ↔ circuitDist f 0 ≤ s + 4

For f ≠ 0, the minimum circuit size problem is membership in a ball about 0.

theorem Cslib.Circuits.Boolean.complexity_single_le_iff_mem_closedBall {n : ℕ} {f : BooleanFunction n} (hf : f ≠ 0) (s : ℕ) : complexity interpretation (single f) ≤ s ↔ f ∈ Metric.closedBall 0 (↑s + 4)

For f ≠ 0, the minimum circuit size problem is membership in the closed ball of radius s + 4 about 0 for the computational Hamming norm.