Finite Boolean list decoding -- proof internals

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

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

theorem Complexity.BooleanListCode.decodeAtIndexBits?_encodeDecoderIndex_internal {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)

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

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

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

theorem Complexity.BooleanListCode.exists_decoder_index_of_agreementProbability_ge_internal {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

theorem Complexity.BooleanListCode.exists_indexBits_of_agreementProbability_ge_internal {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

theorem Complexity.BooleanListCode.mem_candidates_of_agreementProbability_ge_internal {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

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

theorem Complexity.BooleanListCode.mem_candidates_of_half_add_margin_internal {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

theorem Complexity.BooleanListCode.exists_indexBits_of_half_add_margin_internal {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

theorem Complexity.BooleanListCode.mem_candidates_and_card_le_of_half_add_margin_internal {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