Finite Boolean list decoding

Exact truth-table agreement above 1/2 + ε places the original message in the candidate set of any code list-decodable up to radius 1/2 - ε. The candidate set contains at most the advertised indexed list size. A canonical fixed-width codec stores the selecting index in exactly clog₂(listSize) bits and turns the existential decoder occurrence into an actual bit string. The family layer separates semantic inverse-accuracy decoding, concrete polynomial parameter bounds, and single-machine encoder/full-decoder uniformity.

@[simp]

theorem Complexity.BooleanListCode.length_encodeDecoderIndex {listSize : ℕ} (index : Fin listSize) : (encodeDecoderIndex index).length = decoderIndexBitWidth listSize

Encoding a decoder index uses exactly the ceiling-logarithmic number of bits needed for the advertised list size.

theorem Complexity.BooleanListCode.decodeDecoderIndex?_encodeDecoderIndex {listSize : ℕ} (index : Fin listSize) : decodeDecoderIndex? listSize (encodeDecoderIndex index) = some index

Fixed-width decoder-index encoding round-trips exactly.

theorem Complexity.BooleanListCode.decodeAtIndexBits?_encodeDecoderIndex {messageLength listSize : ℕ} {coordinate : Type u} (code : BooleanListCode messageLength listSize coordinate) (received : coordinate → Bool) (index : Fin listSize) : code.decodeAtIndexBits? received (encodeDecoderIndex index) = some (code.decode received index)

Selecting a list decoder output through its encoded index agrees with selecting it directly.

theorem Complexity.BooleanListCode.relativeDistance_eq_one_sub_agreementProbability {coordinate : Type u} [Fintype coordinate] [DecidableEq coordinate] [Nonempty coordinate] (left right : coordinate → Bool) : relativeDistance left right = 1 - agreementProbability left right

Relative Boolean Hamming distance is one minus exact agreement probability.

theorem Complexity.BooleanListCode.agreementProbability_add_relativeDistance {coordinate : Type u} [Fintype coordinate] [DecidableEq coordinate] [Nonempty coordinate] (left right : coordinate → Bool) : agreementProbability left right + relativeDistance left right = 1

Exact agreement and relative Hamming distance partition the coordinate space.

theorem Complexity.BooleanListCode.relativeDistance_le_of_agreementProbability_ge {coordinate : Type u} [Fintype coordinate] [DecidableEq coordinate] [Nonempty coordinate] {left right : coordinate → Bool} {radius : ℚ} (hagreement : 1 - radius ≤ agreementProbability left right) : relativeDistance left right ≤ radius

Agreement at least 1 - radius implies relative distance at most radius.

theorem Complexity.BooleanListCode.exists_decoder_index_of_agreementProbability_ge {messageLength listSize : ℕ} {coordinate : Type u} [Fintype coordinate] [DecidableEq coordinate] [Nonempty coordinate] {code : BooleanListCode messageLength listSize coordinate} {radius : ℚ} (hcode : code.IsListDecodableAt radius) (message : Fin messageLength → Bool) (received : coordinate → Bool) (hagreement : 1 - radius ≤ agreementProbability (code.encode message) received) : ∃ (index : Fin listSize), code.decode received index = message

A list-decoding guarantee and sufficient agreement produce an indexed decoder occurrence of the original message.

theorem Complexity.BooleanListCode.exists_indexBits_of_agreementProbability_ge {messageLength listSize : ℕ} {coordinate : Type u} [Fintype coordinate] [DecidableEq coordinate] [Nonempty coordinate] {code : BooleanListCode messageLength listSize coordinate} {radius : ℚ} (hcode : code.IsListDecodableAt radius) (message : Fin messageLength → Bool) (received : coordinate → Bool) (hagreement : 1 - radius ≤ agreementProbability (code.encode message) received) : ∃ (bits : List Bool), bits.length = decoderIndexBitWidth listSize ∧ code.decodeAtIndexBits? received bits = some message

A list-decoding guarantee and sufficient agreement produce an actual fixed-width bit string selecting the original message.

theorem Complexity.BooleanListCode.mem_candidates_of_agreementProbability_ge {messageLength listSize : ℕ} {coordinate : Type u} [Fintype coordinate] [DecidableEq coordinate] [Nonempty coordinate] {code : BooleanListCode messageLength listSize coordinate} {radius : ℚ} (hcode : code.IsListDecodableAt radius) (message : Fin messageLength → Bool) (received : coordinate → Bool) (hagreement : 1 - radius ≤ agreementProbability (code.encode message) received) : message ∈ code.candidates received

Sufficient agreement places the original message in the decoder candidate set.

theorem Complexity.BooleanListCode.card_candidates_le {messageLength listSize : ℕ} {coordinate : Type u} (code : BooleanListCode messageLength listSize coordinate) (received : coordinate → Bool) : (code.candidates received).card ≤ listSize

Deduplicating the indexed decoder output leaves at most listSize messages.

theorem Complexity.BooleanListCode.mem_candidates_of_half_add_margin {messageLength listSize : ℕ} {coordinate : Type u} [Fintype coordinate] [DecidableEq coordinate] [Nonempty coordinate] {code : BooleanListCode messageLength listSize coordinate} {margin : ℚ} (hcode : code.IsListDecodableAt (1 / 2 - margin)) (message : Fin messageLength → Bool) (received : coordinate → Bool) (hagreement : 1 / 2 + margin ≤ agreementProbability (code.encode message) received) : message ∈ code.candidates received

For a code list-decodable to radius 1/2 - ε, agreement 1/2 + ε puts the message in the decoder candidate set.

theorem Complexity.BooleanListCode.exists_indexBits_of_half_add_margin {messageLength listSize : ℕ} {coordinate : Type u} [Fintype coordinate] [DecidableEq coordinate] [Nonempty coordinate] {code : BooleanListCode messageLength listSize coordinate} {margin : ℚ} (hcode : code.IsListDecodableAt (1 / 2 - margin)) (message : Fin messageLength → Bool) (received : coordinate → Bool) (hagreement : 1 / 2 + margin ≤ agreementProbability (code.encode message) received) : ∃ (bits : List Bool), bits.length = decoderIndexBitWidth listSize ∧ code.decodeAtIndexBits? received bits = some message

At agreement 1/2 + ε, the original message is selected by an actual ceiling-logarithmic decoder-index string.

theorem Complexity.BooleanListCode.mem_candidates_and_card_le_of_half_add_margin {messageLength listSize : ℕ} {coordinate : Type u} [Fintype coordinate] [DecidableEq coordinate] [Nonempty coordinate] {code : BooleanListCode messageLength listSize coordinate} {margin : ℚ} (hcode : code.IsListDecodableAt (1 / 2 - margin)) (message : Fin messageLength → Bool) (received : coordinate → Bool) (hagreement : 1 / 2 + margin ≤ agreementProbability (code.encode message) received) : message ∈ code.candidates received ∧ (code.candidates received).card ≤ listSize

Hirahara's abstract list-decoding bridge: a 1/2 + ε approximator identifies a candidate set containing the original message and having at most the advertised list size.