Finite Boolean Hamming geometry

This module supplies the exact finite geometry used by coding-based metacomplexity and hardness magnification: a metric on Boolean words, exact binomial sphere and ball counts, and the Hamming packing bound. Absolute and rational relative distance are connected explicitly. BooleanCode then packages injective finite encodings, exact rate, minimum distance, and exhaustive unique decoding without asserting an efficient implementation. A finite Gilbert--Varshamov theorem supplies separated covering codes nonconstructively.

@[simp]

theorem Complexity.BooleanHamming.mem_disagreement {length : ℕ} (left right : Word length) (coordinate : Fin length) : coordinate ∈ disagreement left right ↔ left coordinate ≠ right coordinate

Membership in the disagreement support is pointwise inequality.

@[simp]

theorem Complexity.BooleanHamming.distance_refl {length : ℕ} (word : Word length) : distance word word = 0

Every word has distance zero from itself.

theorem Complexity.BooleanHamming.distance_comm {length : ℕ} (left right : Word length) : distance left right = distance right left

Boolean Hamming distance is symmetric.

@[simp]

theorem Complexity.BooleanHamming.distance_eq_zero_iff {length : ℕ} (left right : Word length) : distance left right = 0 ↔ left = right

Distance zero characterizes equality of words.

theorem Complexity.BooleanHamming.distance_triangle {length : ℕ} (first second third : Word length) : distance first third ≤ distance first second + distance second third

Boolean Hamming distance satisfies the triangle inequality.

theorem Complexity.BooleanHamming.distance_le_length {length : ℕ} (left right : Word length) : distance left right ≤ length

Hamming distance never exceeds the word length.

theorem Complexity.BooleanHamming.distance_eq_popCount_translate {length : ℕ} (left right : Word length) : distance left right = popCount (translate right left)

Distance from right is the Hamming weight after XOR translation.

@[simp]

theorem Complexity.BooleanHamming.translate_translate {length : ℕ} (center word : Word length) : translate center (translate center word) = word

XOR translation by a fixed center is an involution.

theorem Complexity.BooleanHamming.relativeDistance_eq_distance_div {length : ℕ} (left right : Word length) : BooleanListCode.relativeDistance left right = ↑(distance left right) / ↑length

The list-decoding relative distance is absolute Hamming distance divided by the coordinate count. This remains valid at length zero under rational division's total convention.

@[simp]

theorem Complexity.BooleanHamming.mem_sphere {length : ℕ} (center word : Word length) (radius : ℕ) : word ∈ sphere center radius ↔ distance word center = radius

Membership in a Hamming sphere.

@[simp]

theorem Complexity.BooleanHamming.mem_ball {length : ℕ} (center word : Word length) (radius : ℕ) : word ∈ ball center radius ↔ distance word center ≤ radius

Membership in a closed Hamming ball.

theorem Complexity.BooleanHamming.ball_mono {length : ℕ} (center : Word length) {first second : ℕ} (hradius : first ≤ second) : ball center first ⊆ ball center second

Increasing the radius enlarges a Hamming ball.

theorem Complexity.BooleanHamming.card_distance_filter_eq_popCount_filter {length : ℕ} (center : Word length) (predicate : ℕ → Prop) [DecidablePred predicate] : {word : Word length | predicate (distance word center)}.card = {word : Word length | predicate (popCount word)}.card

XOR translation makes every distance-profile count center-independent.

theorem Complexity.BooleanHamming.card_sphere {length : ℕ} (center : Word length) (radius : ℕ) : (sphere center radius).card = length.choose radius

A radius-r sphere in the Boolean cube has exactly length.choose r words, independently of its center.

theorem Complexity.BooleanHamming.card_ball {length : ℕ} (center : Word length) (radius : ℕ) : (ball center radius).card = volume length radius

A radius-r Boolean Hamming ball has its exact binomial volume.

theorem Complexity.BooleanHamming.volume_le_two_pow (length radius : ℕ) : volume length radius ≤ 2 ^ length

A Hamming ball contains at most all 2^length Boolean words.

theorem Complexity.BooleanHamming.volume_eq_two_pow_of_length_le_radius {length radius : ℕ} (hradius : length ≤ radius) : volume length radius = 2 ^ length

Once the radius reaches the word length, the ball is the entire cube.

theorem Complexity.BooleanHamming.disjoint_balls_of_two_mul_radius_lt_distance {length radius : ℕ} {left right : Word length} (hfar : 2 * radius < distance left right) : Disjoint (ball left radius) (ball right radius)

Balls of radius r around centers farther than 2r are disjoint.

theorem Complexity.BooleanHamming.pairwiseDisjoint_balls_of_isSeparated {length minimumDistance radius : ℕ} {code : Finset (Word length)} (hcode : IsSeparated code minimumDistance) (hradius : 2 * radius < minimumDistance) : (↑code).PairwiseDisjoint fun (center : Word length) => ball center radius

A separated finite code induces pairwise-disjoint decoding balls below half its minimum distance.

theorem Complexity.BooleanHamming.packing_bound {length minimumDistance radius : ℕ} {code : Finset (Word length)} (hcode : IsSeparated code minimumDistance) (hradius : 2 * radius < minimumDistance) : code.card * volume length radius ≤ 2 ^ length

Finite Boolean Hamming packing bound.