The Boolean cube

An input on a finite coordinate set V is a map V → Bool. For A : Finset V we write flipSet x A for the input x^A of Section 1 of bs_lambda.txt, obtained by flipping every coordinate of A.

Hamming distance is taken from Mathlib (hammingDist).

Adapted for Lean Pool from Timeroot/BS_Lam at commit 7bd39a8d41ee7910d3296d0477ad18f8fff9d870; ported to Lean Pool with proof and dependency cleanup.

theorem Finset.symmDiff_singleton_singleton {α : Type u_1} [DecidableEq α] {p q : α} (hpq : p ≠ q) : symmDiff {p} {q} = {p, q}

The symmetric difference of two distinct singletons is the corresponding pair. This is a general Finset fact, stated here because Mathlib does not have it.

@[reducible, inline]

abbrev BSLambda.Input (V : Type u_1) : Type u_1

An input to a Boolean function on the coordinate set V.

Equations

• BSLambda.Input V = (V → Bool)

def BSLambda.zeroInput (V : Type u_1) : Input V

The all-zero input, written 0^V in bs_lambda.txt.

Equations

• BSLambda.zeroInput V x✝ = false

@[simp]

theorem BSLambda.zeroInput_apply {V : Type u_1} (v : V) : zeroInput V v = false

def BSLambda.flipSet {V : Type u_1} [DecidableEq V] (x : Input V) (A : Finset V) : Input V

flipSet x A is the input written x^A in the source document: it flips every coordinate lying in A and leaves all other coordinates unchanged.

Equations

• BSLambda.flipSet x A v = if v ∈ A then !x v else x v

@[simp]

theorem BSLambda.flipSet_apply_of_mem {V : Type u_1} [DecidableEq V] {x : Input V} {A : Finset V} {v : V} (hv : v ∈ A) : flipSet x A v = !x v

@[simp]

theorem BSLambda.flipSet_apply_of_notMem {V : Type u_1} [DecidableEq V] {x : Input V} {A : Finset V} {v : V} (hv : v ∉ A) : flipSet x A v = x v

@[simp]

theorem BSLambda.flipSet_apply_eq_self_iff {V : Type u_1} [DecidableEq V] {x : Input V} {A : Finset V} {v : V} : flipSet x A v = x v ↔ v ∉ A

A coordinate survives flipSet exactly when it lies outside the flipped set.

theorem BSLambda.flipSet_apply_ne_self_iff {V : Type u_1} [DecidableEq V] {x : Input V} {A : Finset V} {v : V} : flipSet x A v ≠ x v ↔ v ∈ A

A coordinate is changed by flipSet exactly when it lies in the flipped set.

theorem BSLambda.ne_flipSet_apply {V : Type u_1} [DecidableEq V] {x : Input V} {A : Finset V} {v : V} (hv : v ∈ A) : x v ≠ flipSet x A v

An input differs from its flip at every flipped coordinate.

@[simp]

theorem BSLambda.flipSet_empty {V : Type u_1} [DecidableEq V] (x : Input V) : flipSet x ∅ = x

theorem BSLambda.flipSet_flipSet_symmDiff {V : Type u_1} [DecidableEq V] (x : Input V) (A B : Finset V) : flipSet (flipSet x A) B = flipSet x (symmDiff A B)

Flipping A and then B flips exactly the coordinates of the symmetric difference.

@[simp]

theorem BSLambda.flipSet_flipSet {V : Type u_1} [DecidableEq V] (x : Input V) (A : Finset V) : flipSet (flipSet x A) A = x

theorem BSLambda.flipSet_singleton_flipSet_singleton {V : Type u_1} [DecidableEq V] (x : Input V) {p q : V} (hpq : p ≠ q) : flipSet (flipSet x {p}) {q} = flipSet x {p, q}

Flipping two distinct coordinates one after the other is the same as flipping the pair at once.

theorem BSLambda.flipSet_pair_flipSet_singleton {V : Type u_1} [DecidableEq V] (x : Input V) {p q : V} (hpq : p ≠ q) : flipSet (flipSet x {p, q}) {q} = flipSet x {p}

Undoing one half of a pair flip leaves the single flip at the other coordinate: this is the "other midpoint" identity behind every two-midpoint argument.

theorem BSLambda.flipSet_left_injective {V : Type u_1} [DecidableEq V] (A : Finset V) : Function.Injective fun (x : Input V) => flipSet x A

Flipping a fixed set of coordinates is injective in the input.

@[simp]

theorem BSLambda.flipSet_left_inj {V : Type u_1} [DecidableEq V] {x y : Input V} {A : Finset V} : flipSet x A = flipSet y A ↔ x = y

theorem BSLambda.flipSet_singleton_injective {V : Type u_1} [DecidableEq V] (x : Input V) : Function.Injective fun (v : V) => flipSet x {v}

Distinct coordinates give distinct single-coordinate flips of a fixed input.

theorem BSLambda.flipSet_singleton_self {V : Type u_1} [DecidableEq V] (x : Input V) (v : V) : flipSet x {v} v = !x v

The flipped coordinate of a single-coordinate flip.

@[simp]

theorem BSLambda.flipSet_zeroInput_apply {V : Type u_1} [DecidableEq V] (A : Finset V) (v : V) : flipSet (zeroInput V) A v = decide (v ∈ A)

Flipping a set of coordinates of the all-zero input yields its indicator function.

@[simp]

theorem BSLambda.hammingDist_flipSet {V : Type u_1} [Fintype V] [DecidableEq V] (x : Input V) (A : Finset V) : hammingDist x (flipSet x A) = A.card

The Hamming distance from x to x^A is exactly A.card.

theorem BSLambda.hammingDist_flipSet_flipSet {V : Type u_1} [Fintype V] [DecidableEq V] (x : Input V) (A B : Finset V) : hammingDist (flipSet x A) (flipSet x B) = (symmDiff A B).card

Two flips of the same input differ exactly on the symmetric difference of the flipped sets.

theorem BSLambda.flipSet_filter_ne {V : Type u_1} [Fintype V] [DecidableEq V] (x y : Input V) : flipSet x {v : V | x v ≠ y v} = y

Every input is a flip of every other, at the set of coordinates where they differ.

theorem BSLambda.exists_eq_flipSet_singleton_of_hammingDist_eq_one {V : Type u_1} [Fintype V] [DecidableEq V] {x y : Input V} (h : hammingDist x y = 1) : ∃ (v : V), y = flipSet x {v}

Two inputs at Hamming distance 1 differ in exactly one coordinate.

theorem BSLambda.hammingDist_flipSet_singleton {V : Type u_1} [Fintype V] [DecidableEq V] (x : Input V) (v : V) : hammingDist x (flipSet x {v}) = 1