Neighbors and cliques in the Boolean input cube

Neighbors are single-bit flips. Distinct neighbors of a vertex are distance two apart, so every clique has at most two vertices.

def Algebraic.BooleanCube.graph {ι : Type u_1} [Fintype ι] : SimpleGraph (ι → Bool)

The graph whose edges change exactly one Boolean coordinate.

Equations

• Algebraic.BooleanCube.graph = { Adj := fun (left right : ι → Bool) => hammingDist left right = 1, symm := ⋯, loopless := ⋯ }

def Algebraic.BooleanCube.flip {ι : Type u_1} [DecidableEq ι] (vertex : ι → Bool) (i : ι) : ι → Bool

Flip one coordinate of a Boolean vertex.

Equations

• Algebraic.BooleanCube.flip vertex i = Function.update vertex i !vertex i

theorem Algebraic.BooleanCube.hammingDist_flip {ι : Type u_1} [Fintype ι] [DecidableEq ι] (vertex : ι → Bool) (i : ι) : hammingDist vertex (flip vertex i) = 1

A single flip changes exactly one coordinate.

theorem Algebraic.BooleanCube.flip_ne {ι : Type u_1} [Fintype ι] [DecidableEq ι] (vertex : ι → Bool) (i : ι) : flip vertex i ≠ vertex

A flipped vertex is different from the original vertex.

theorem Algebraic.BooleanCube.adjacent_iff_flip {ι : Type u_1} [Fintype ι] [DecidableEq ι] (left right : ι → Bool) : graph.Adj left right ↔ ∃ (i : ι), right = flip left i

Every neighbor is obtained by flipping a unique differing coordinate.

theorem Algebraic.BooleanCube.hammingDist_flip_flip {ι : Type u_1} [Fintype ι] [DecidableEq ι] (vertex : ι → Bool) {i j : ι} (different : i ≠ j) : hammingDist (flip vertex i) (flip vertex j) = 2

Flipping two different coordinates gives neighbors at mutual distance two.

theorem Algebraic.BooleanCube.not_adjacent_of_common_neighbor {ι : Type u_1} [Fintype ι] [DecidableEq ι] {base left right : ι → Bool} (hl : graph.Adj base left) (hr : graph.Adj base right) (different : left ≠ right) : ¬graph.Adj left right

Distinct neighbors of a Boolean vertex are never adjacent to each other.

theorem Algebraic.BooleanCube.card_le_two_of_pairwise_adjacent {ι : Type u_1} [Fintype ι] [DecidableEq ι] (vertices : Finset (ι → Bool)) (clique : ∀ a ∈ vertices, ∀ b ∈ vertices, a ≠ b → graph.Adj a b) : vertices.card ≤ 2

Every clique in the Boolean cube has at most two vertices.