Finite Boolean Hamming geometry -- proof internals

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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