Finite Boolean codes -- definitions

An abstract Boolean code is an injective map from fixed-length messages to fixed-length codewords. Correctness, minimum distance, exhaustive decoding, and rate are represented independently of any efficiency claim.

structure Complexity.BooleanCode (messageLength blockLength : ℕ) : Type

An injective fixed-block-length Boolean encoding.

• encode : BooleanHamming.Word messageLength → BooleanHamming.Word blockLength

  Encode one message as a codeword.

• encode_injective : Function.Injective self.encode

  Distinct messages have distinct codewords.

def Complexity.BooleanCode.zeroWord (length : ℕ) : BooleanHamming.Word length

The all-zero Boolean word.

Equations

• Complexity.BooleanCode.zeroWord length x✝ = false

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

Coordinatewise addition over GF(2), represented by Boolean XOR.

Equations

• Complexity.BooleanCode.xorWords left right coordinate = (left coordinate ^^ right coordinate)

def Complexity.BooleanCode.rate (messageLength blockLength : ℕ) : ℚ

Exact rational information rate for the two code lengths. At block length zero this uses the total rational-division convention.

Equations

• Complexity.BooleanCode.rate messageLength blockLength = ↑messageLength / ↑blockLength

def Complexity.BooleanCode.IsLinear {messageLength blockLength : ℕ} (code : BooleanCode messageLength blockLength) : Prop

Linearity over GF(2), stated directly through zero and XOR so the coding layer does not need a second representation of Boolean words.

Equations

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

def Complexity.BooleanCode.codewords {messageLength blockLength : ℕ} (code : BooleanCode messageLength blockLength) : Finset (BooleanHamming.Word blockLength)

Finite image of all messages.

Equations

• code.codewords = Finset.image code.encode Finset.univ

def Complexity.BooleanCode.HasMinimumDistance {messageLength blockLength : ℕ} (code : BooleanCode messageLength blockLength) (minimumDistance : ℕ) : Prop

Every pair of distinct messages encodes at distance at least the stated minimum.

Equations

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

def Complexity.BooleanCode.decodeCandidates {messageLength blockLength : ℕ} (code : BooleanCode messageLength blockLength) (received : BooleanHamming.Word blockLength) (radius : ℕ) : Finset (BooleanHamming.Word messageLength)

Exhaustive list of messages whose codewords lie in a received-word ball.

Equations

• code.decodeCandidates received radius = {message : Complexity.BooleanHamming.Word messageLength | Complexity.BooleanHamming.distance (code.encode message) received ≤ radius}

noncomputable def Complexity.BooleanCode.decodeUnique? {messageLength blockLength : ℕ} (code : BooleanCode messageLength blockLength) (received : BooleanHamming.Word blockLength) (radius : ℕ) : Option (BooleanHamming.Word messageLength)

Exhaustive decoder returning the first nearby message, if one exists. Minimum-distance hypotheses make this result unique but do not make the search efficient.

Equations

• code.decodeUnique? received radius = (code.decodeCandidates received radius).toList.head?