Finite Boolean codes

This module turns the finite Hamming geometry into an abstract coding layer. An injective code has exactly 2^messageLength codewords, minimum distance implies the exact sphere-packing bound, and exhaustive decoding is uniquely correct below half that distance. No runtime claim is bundled into these semantic results. The repetition submodule supplies the first concrete linear code with exact distance amplification.

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

Codewords are exactly encoded messages.

@[simp]

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

An injective Boolean code has exactly 2^messageLength codewords.

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

A message-level minimum-distance contract separates the finite codeword set by the same amount.

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

Coding-theoretic Hamming packing bound with exact finite parameters.

@[simp]

theorem Complexity.BooleanCode.mem_decodeCandidates_iff {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

Candidate-list membership is exactly proximity of the encoded message.

theorem Complexity.BooleanCode.mem_decodeCandidates_of_close {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

Every sufficiently close message occurs in exhaustive decoding.

theorem Complexity.BooleanCode.eq_of_mem_decodeCandidates {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

Below half the minimum distance, any two decoding candidates coincide.

theorem Complexity.BooleanCode.card_decodeCandidates_le_one {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

Exhaustive decoding contains at most one message below half the minimum distance.

theorem Complexity.BooleanCode.decodeCandidates_eq_singleton_of_close {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}

A nearby message is the entire exhaustive candidate set below half the minimum distance.

theorem Complexity.BooleanCode.decodeUnique?_eq_some_of_close {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

The exhaustive decoder recovers every message from fewer than half the minimum-distance errors.