Finite Boolean codes -- proof internals

theorem Complexity.BooleanCode.mem_codewords_iff_internal {messageLength blockLength : ℕ} (code : BooleanCode messageLength blockLength) (word : BooleanHamming.Word blockLength) : word ∈ code.codewords ↔ ∃ (message : BooleanHamming.Word messageLength), code.encode message = word

theorem Complexity.BooleanCode.card_codewords_internal {messageLength blockLength : ℕ} (code : BooleanCode messageLength blockLength) : code.codewords.card = 2 ^ messageLength

theorem Complexity.BooleanCode.isSeparated_codewords_internal {messageLength blockLength : ℕ} {code : BooleanCode messageLength blockLength} {minimumDistance : ℕ} (hdistance : code.HasMinimumDistance minimumDistance) : BooleanHamming.IsSeparated code.codewords minimumDistance

theorem Complexity.BooleanCode.packing_bound_internal {messageLength blockLength minimumDistance radius : ℕ} {code : BooleanCode messageLength blockLength} (hdistance : code.HasMinimumDistance minimumDistance) (hradius : 2 * radius < minimumDistance) : 2 ^ messageLength * BooleanHamming.volume blockLength radius ≤ 2 ^ blockLength

theorem Complexity.BooleanCode.mem_decodeCandidates_iff_internal {messageLength blockLength : ℕ} (code : BooleanCode messageLength blockLength) (received : BooleanHamming.Word blockLength) (radius : ℕ) (message : BooleanHamming.Word messageLength) : message ∈ code.decodeCandidates received radius ↔ BooleanHamming.distance (code.encode message) received ≤ radius

theorem Complexity.BooleanCode.mem_decodeCandidates_of_close_internal {messageLength blockLength : ℕ} (code : BooleanCode messageLength blockLength) (received : BooleanHamming.Word blockLength) (radius : ℕ) (message : BooleanHamming.Word messageLength) (hclose : BooleanHamming.distance (code.encode message) received ≤ radius) : message ∈ code.decodeCandidates received radius

theorem Complexity.BooleanCode.eq_of_mem_decodeCandidates_internal {messageLength blockLength : ℕ} {code : BooleanCode messageLength blockLength} {minimumDistance radius : ℕ} (hdistance : code.HasMinimumDistance minimumDistance) (hradius : 2 * radius < minimumDistance) (received : BooleanHamming.Word blockLength) {left right : BooleanHamming.Word messageLength} (hleft : left ∈ code.decodeCandidates received radius) (hright : right ∈ code.decodeCandidates received radius) : left = right

theorem Complexity.BooleanCode.card_decodeCandidates_le_one_internal {messageLength blockLength : ℕ} {code : BooleanCode messageLength blockLength} {minimumDistance radius : ℕ} (hdistance : code.HasMinimumDistance minimumDistance) (hradius : 2 * radius < minimumDistance) (received : BooleanHamming.Word blockLength) : (code.decodeCandidates received radius).card ≤ 1

theorem Complexity.BooleanCode.decodeCandidates_eq_singleton_of_close_internal {messageLength blockLength : ℕ} {code : BooleanCode messageLength blockLength} {minimumDistance radius : ℕ} (hdistance : code.HasMinimumDistance minimumDistance) (hradius : 2 * radius < minimumDistance) (received : BooleanHamming.Word blockLength) (message : BooleanHamming.Word messageLength) (hclose : BooleanHamming.distance (code.encode message) received ≤ radius) : code.decodeCandidates received radius = {message}

theorem Complexity.BooleanCode.decodeUnique?_eq_some_of_close_internal {messageLength blockLength : ℕ} {code : BooleanCode messageLength blockLength} {minimumDistance radius : ℕ} (hdistance : code.HasMinimumDistance minimumDistance) (hradius : 2 * radius < minimumDistance) (received : BooleanHamming.Word blockLength) (message : BooleanHamming.Word messageLength) (hclose : BooleanHamming.distance (code.encode message) received ≤ radius) : code.decodeUnique? received radius = some message