Finite Boolean Hamming geometry -- definitions

This module fixes absolute Hamming distance on n-bit words, finite spheres and balls, their binomial volume, and a minimum-distance predicate for finite codes. The rational relative-distance bridge remains compatible with the existing Boolean list-decoding API.

@[reducible, inline]

abbrev Complexity.BooleanHamming.Word (length : ℕ) : Type

A fixed-length Boolean word.

Equations

• Complexity.BooleanHamming.Word length = (Fin length → Bool)

def Complexity.BooleanHamming.disagreement {length : ℕ} (left right : Word length) : Finset (Fin length)

Coordinates on which two Boolean words disagree.

Equations

• Complexity.BooleanHamming.disagreement left right = {coordinate : Fin length | left coordinate ≠ right coordinate}

def Complexity.BooleanHamming.distance {length : ℕ} (left right : Word length) : ℕ

Absolute Hamming distance.

Equations

• Complexity.BooleanHamming.distance left right = (Complexity.BooleanHamming.disagreement left right).card

def Complexity.BooleanHamming.translate {length : ℕ} (center word : Word length) : Word length

Translate a Boolean word by coordinatewise XOR with a fixed center.

Equations

• Complexity.BooleanHamming.translate center word coordinate = (word coordinate ^^ center coordinate)

def Complexity.BooleanHamming.sphere {length : ℕ} (center : Word length) (radius : ℕ) : Finset (Word length)

Words at absolute distance exactly radius from center.

Equations

• Complexity.BooleanHamming.sphere center radius = {word : Complexity.BooleanHamming.Word length | Complexity.BooleanHamming.distance word center = radius}

def Complexity.BooleanHamming.ball {length : ℕ} (center : Word length) (radius : ℕ) : Finset (Word length)

Words at absolute distance at most radius from center.

Equations

• Complexity.BooleanHamming.ball center radius = {word : Complexity.BooleanHamming.Word length | Complexity.BooleanHamming.distance word center ≤ radius}

def Complexity.BooleanHamming.volume (length radius : ℕ) : ℕ

Binomial volume of a Boolean Hamming ball. Terms above length vanish.

Equations

• Complexity.BooleanHamming.volume length radius = ∑ weight ∈ Finset.range (radius + 1), length.choose weight

def Complexity.BooleanHamming.IsSeparated {length : ℕ} (code : Finset (Word length)) (minimumDistance : ℕ) : Prop

A finite code has pairwise distance at least minimumDistance.

Equations

• One or more equations did not get rendered due to their size.