Finite Boolean list decoding -- definitions

A Boolean list code maps fixed-length messages to Boolean functions on an arbitrary finite coordinate type. Its decoder returns a fixed-size indexed candidate list. Relative distance and agreement are exact rational uniform probabilities, matching the truth-table view used in metacomplexity.

structure Complexity.BooleanListCode (messageLength listSize : ℕ) (coordinate : Type u) : Type u

A fixed-length binary code together with a decoder producing listSize candidate messages.

• encode : (Fin messageLength → Bool) → coordinate → Bool

  Encode a message as a Boolean function on the codeword coordinates.

• decode : (coordinate → Bool) → Fin listSize → Fin messageLength → Bool

  Decode any received word into a fixed-size indexed candidate list.

def Complexity.BooleanListCode.agreementProbability {coordinate : Type u} [Fintype coordinate] (left right : coordinate → Bool) : ℚ

Exact fraction of coordinates on which two Boolean words agree.

Equations

• Complexity.BooleanListCode.agreementProbability left right = Complexity.uniformProbability {input : coordinate | left input = right input}

def Complexity.BooleanListCode.relativeDistance {coordinate : Type u} [Fintype coordinate] (left right : coordinate → Bool) : ℚ

Exact relative Hamming distance between two Boolean words.

Equations

• Complexity.BooleanListCode.relativeDistance left right = Complexity.uniformProbability {input : coordinate | left input ≠ right input}

def Complexity.BooleanListCode.IsListDecodableAt {messageLength listSize : ℕ} {coordinate : Type u} [Fintype coordinate] (code : BooleanListCode messageLength listSize coordinate) (radius : ℚ) : Prop

List-decoding guarantee at a relative Hamming radius.

Equations

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

def Complexity.BooleanListCode.candidates {messageLength listSize : ℕ} {coordinate : Type u} (code : BooleanListCode messageLength listSize coordinate) (received : coordinate → Bool) : Finset (Fin messageLength → Bool)

Distinct messages appearing among the decoder's indexed candidates.

Equations

• code.candidates received = Finset.image (code.decode received) Finset.univ

def Complexity.BooleanListCode.decoderIndexBitWidth (listSize : ℕ) : ℕ

Number of bits sufficient to select one of listSize indexed decoder outputs.

Equations

• Complexity.BooleanListCode.decoderIndexBitWidth listSize = Fin.bitWidth listSize

def Complexity.BooleanListCode.encodeDecoderIndex {listSize : ℕ} (index : Fin listSize) : List Bool

Fixed-width binary encoding of an indexed decoder output.

Equations

• Complexity.BooleanListCode.encodeDecoderIndex index = index.toBits

def Complexity.BooleanListCode.decodeDecoderIndex? (listSize : ℕ) (bits : List Bool) : Option (Fin listSize)

Decode a fixed-width decoder index, rejecting malformed lengths and values outside Fin listSize.

Equations

• Complexity.BooleanListCode.decodeDecoderIndex? listSize bits = Fin.fromBits? listSize bits

def Complexity.BooleanListCode.decodeAtIndexBits? {messageLength listSize : ℕ} {coordinate : Type u} (code : BooleanListCode messageLength listSize coordinate) (received : coordinate → Bool) (bits : List Bool) : Option (Fin messageLength → Bool)

Decode a source message using a fixed-width encoded list index.

Equations

• code.decodeAtIndexBits? received bits = match Complexity.BooleanListCode.decodeDecoderIndex? listSize bits with | some index => some (code.decode received index) | none => none