The Hamming geometry of the Boolean cube

Points of the cube ι → Bool are compared by Mathlib's Hamming distance, the number of coordinates where they differ. The Boolean operations act on points coordinatewise, and their geometry is exact. For f g h : ι → Bool on a finite set ι:

• conjunction and disjunction sort a pair coordinatewise, so the distances from f ∧ g and f ∨ g to any h add up to those from f and g (Cslib.BitString.hammingDist_and_add_hammingDist_or);
• f ∧ g and f ∨ g lie on geodesics from f to g (Cslib.BitString.hammingDist_add_hammingDist_and, Cslib.BitString.hammingDist_add_hammingDist_or), and both are 1-Lipschitz in each argument;
• adding a fixed point, which is the coordinatewise exclusive or, and negation are isometries (Cslib.BitString.hammingDist_add_right, Cslib.BitString.hammingDist_not);
• the cube is a median algebra for the coordinatewise majority m(f,g,h) = (f ∧ g) ∨ (g ∧ h) ∨ (h ∧ f) (Cslib.BitString.median), the lattice median of the distributive lattice ι → Bool: it satisfies the majority law, symmetry and the associative law, and it distributes over itself. The median lies between any two of its arguments and minimizes the total distance to the three of them.

The truth tables of Boolean functions are points of the cube (ι → Bool) → Bool. The parities on two distinct sets S and T disagree exactly where the parity on the symmetric difference S ∆ T is true, which happens on half of the inputs, so they differ on exactly half of the inputs (Cslib.BitString.two_mul_hammingDist_parityOn). Two distinct coordinate projections x ↦ x i and x ↦ x j are the parities on {i} and {j}, so they differ on exactly half of the inputs (Cslib.BitString.two_mul_hammingDist_proj), and so do their shifts f + x_i and f + x_j by any common function f (Cslib.BitString.two_mul_hammingDist_add_proj), however complicated f is.

Main definitions

• Cslib.BitString.median: the coordinatewise majority of three points.

Main results

• Cslib.BitString.hammingDist_and_add_hammingDist_or: conjunction and disjunction sort.
• Cslib.BitString.hammingDist_add_hammingDist_and, Cslib.BitString.hammingDist_add_hammingDist_or: geodesics.
• Cslib.BitString.hammingDist_and_le, Cslib.BitString.hammingDist_or_le: Lipschitz gates.
• Cslib.BitString.hammingDist_add_right, Cslib.BitString.hammingDist_add_left, Cslib.BitString.hammingDist_not: isometries.
• Cslib.BitString.median_self_left, Cslib.BitString.median_swap_left, Cslib.BitString.median_swap_right, Cslib.BitString.median_assoc: the median algebra laws.
• Cslib.BitString.median_median_distrib: distributivity.
• Cslib.BitString.hammingDist_add_hammingDist_median, Cslib.BitString.hammingDist_median_le: betweenness and minimality of the median.
• Cslib.BitString.two_mul_hammingDist_parityOn: distinct parities are half the cube apart.
• Cslib.BitString.two_mul_hammingDist_proj, Cslib.BitString.hammingDist_proj_div, Cslib.BitString.two_mul_hammingDist_add_proj: projections and their shifts are half the cube apart.

References

• [F. J. MacWilliams, N. J. A. Sloane, The Theory of Error-Correcting Codes] [MWS77]

The median

def Cslib.BitString.median {ι : Type u_1} (f g h : ι → Bool) : ι → Bool

The median of three points: their coordinatewise majority (f ∧ g) ∨ (g ∧ h) ∨ (h ∧ f). This is the lattice median (f ⊓ g) ⊔ (g ⊓ h) ⊔ (h ⊓ f) of the distributive lattice ι → Bool.

theorem Cslib.BitString.median_apply_eq_majority {ι : Type u_1} (f g h : ι → Bool) (i : ι) : median f g h i = majority 3 ![f i, g i, h i]

The median is the majority of three bits at each coordinate.

@[simp]

theorem Cslib.BitString.median_self_left {ι : Type u_1} (f g : ι → Bool) : median f f g = f

The majority law: a point repeated twice is the median.

theorem Cslib.BitString.median_swap_left {ι : Type u_1} (f g h : ι → Bool) : median f g h = median g f h

The median is symmetric in its first two arguments.

theorem Cslib.BitString.median_swap_right {ι : Type u_1} (f g h : ι → Bool) : median f g h = median f h g

The median is symmetric in its last two arguments.

theorem Cslib.BitString.median_assoc {ι : Type u_1} (f g h k : ι → Bool) : median (median f k g) k h = median f k (median g k h)

The associative law of median algebras. Together with the majority law and symmetry it makes the cube a median algebra.

theorem Cslib.BitString.median_median_distrib {ι : Type u_1} (f g h k l : ι → Bool) : median (median f g h) k l = median (median f k l) (median g k l) (median h k l)

The median distributes over itself.

Conjunction and disjunction

theorem Cslib.BitString.hammingDist_and_add_hammingDist_or {ι : Type u_1} [Fintype ι] (f g h : ι → Bool) : hammingDist (fun (i : ι) => f i && g i) h + hammingDist (fun (i : ι) => f i || g i) h = hammingDist f h + hammingDist g h

Conjunction and disjunction sort a pair, so their distances to any h add up to those of the pair.

theorem Cslib.BitString.hammingDist_add_hammingDist_and {ι : Type u_1} [Fintype ι] (f g : ι → Bool) : (hammingDist f fun (i : ι) => f i && g i) + hammingDist (fun (i : ι) => f i && g i) g = hammingDist f g

The conjunction lies on a geodesic from f to g.

theorem Cslib.BitString.hammingDist_add_hammingDist_or {ι : Type u_1} [Fintype ι] (f g : ι → Bool) : (hammingDist f fun (i : ι) => f i || g i) + hammingDist (fun (i : ι) => f i || g i) g = hammingDist f g

The disjunction lies on a geodesic from f to g.

theorem Cslib.BitString.hammingDist_and_le {ι : Type u_1} [Fintype ι] (f f' g g' : ι → Bool) : (hammingDist (fun (i : ι) => f i && g i) fun (i : ι) => f' i && g' i) ≤ hammingDist f f' + hammingDist g g'

Conjunction is 1-Lipschitz in each argument.

theorem Cslib.BitString.hammingDist_or_le {ι : Type u_1} [Fintype ι] (f f' g g' : ι → Bool) : (hammingDist (fun (i : ι) => f i || g i) fun (i : ι) => f' i || g' i) ≤ hammingDist f f' + hammingDist g g'

Disjunction is 1-Lipschitz in each argument.

Isometries

@[simp]

theorem Cslib.BitString.hammingDist_add_right {ι : Type u_1} [Fintype ι] (f g a : ι → Bool) : hammingDist (f + a) (g + a) = hammingDist f g

Adding a fixed point, coordinatewise the exclusive or, is an isometry.

@[simp]

theorem Cslib.BitString.hammingDist_add_left {ι : Type u_1} [Fintype ι] (a f g : ι → Bool) : hammingDist (a + f) (a + g) = hammingDist f g

Adding a fixed point on the left is an isometry.

@[simp]

theorem Cslib.BitString.hammingDist_not {ι : Type u_1} [Fintype ι] (f g : ι → Bool) : (hammingDist (fun (i : ι) => !f i) fun (i : ι) => !g i) = hammingDist f g

Negation is an isometry.

Distances to the median

theorem Cslib.BitString.hammingDist_add_hammingDist_median {ι : Type u_1} [Fintype ι] (f g h : ι → Bool) : hammingDist f (median f g h) + hammingDist (median f g h) g = hammingDist f g

The median lies between any two of its arguments.

theorem Cslib.BitString.hammingDist_median_le {ι : Type u_1} [Fintype ι] (f g h k : ι → Bool) : hammingDist (median f g h) f + hammingDist (median f g h) g + hammingDist (median f g h) h ≤ hammingDist k f + hammingDist k g + hammingDist k h

The median minimizes the total distance to its three arguments.

Parities and coordinate projections

theorem Cslib.BitString.two_mul_hammingDist_parityOn {ι : Type u_1} [Fintype ι] [DecidableEq ι] {S T : Finset ι} (h : S ≠ T) : 2 * hammingDist (parityOn S) (parityOn T) = 2 ^ Fintype.card ι

Distinct parities differ on exactly half of the inputs: they disagree where the parity on the symmetric difference is true.

theorem Cslib.BitString.two_mul_hammingDist_proj {ι : Type u_1} [Fintype ι] [DecidableEq ι] {i j : ι} (hij : i ≠ j) : (2 * hammingDist (fun (x : ι → Bool) => x i) fun (x : ι → Bool) => x j) = 2 ^ Fintype.card ι

Two distinct coordinate projections differ on exactly half of the inputs: they are the parities on {i} and {j}.

theorem Cslib.BitString.hammingDist_proj_div {ι : Type u_1} [Fintype ι] [DecidableEq ι] {𝕜 : Type u_2} [Semifield 𝕜] [CharZero 𝕜] {i j : ι} (hij : i ≠ j) : ↑(hammingDist (fun (x : ι → Bool) => x i) fun (x : ι → Bool) => x j) / 2 ^ Fintype.card ι = 1 / 2

The relative Hamming distance between two distinct coordinate projections is one half.

theorem Cslib.BitString.two_mul_hammingDist_add_proj {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) {i j : ι} (hij : i ≠ j) : 2 * hammingDist (f + fun (x : ι → Bool) => x i) (f + fun (x : ι → Bool) => x j) = 2 ^ Fintype.card ι

Shifts of distinct projections by a common function differ on half of the inputs, however complicated the common function f is.