Boolean repetition codes

This is the first concrete finite linear code in the metacomplexity coding layer. Repeating every message bit copies > 0 times multiplies every Hamming distance by exactly copies, giving a minimum-distance lower bound of copies, unique decoding below half that distance, and a specialized finite packing inequality.

@[simp]

theorem Complexity.BooleanCode.repetitionEncode_apply {messageLength copies : ℕ} (message : BooleanHamming.Word messageLength) (coordinate : Fin (messageLength * copies)) : repetitionEncode messageLength copies message coordinate = message (finProdFinEquiv.symm coordinate).1

Repetition encoding at a canonical product coordinate reads the selected message bit.

theorem Complexity.BooleanCode.repetitionEncode_injective {messageLength copies : ℕ} (hcopies : 0 < copies) : Function.Injective (repetitionEncode messageLength copies)

Positive-copy repetition encoding is injective.

theorem Complexity.BooleanCode.distance_repetitionEncode {messageLength copies : ℕ} (left right : BooleanHamming.Word messageLength) : BooleanHamming.distance (repetitionEncode messageLength copies left) (repetitionEncode messageLength copies right) = BooleanHamming.distance left right * copies

Repetition multiplies absolute Hamming distance by the copy count.

theorem Complexity.BooleanCode.repetitionEncode_isLinear {messageLength copies : ℕ} : repetitionEncode messageLength copies (zeroWord messageLength) = zeroWord (messageLength * copies) ∧ ∀ (left right : BooleanHamming.Word messageLength), repetitionEncode messageLength copies (xorWords left right) = xorWords (repetitionEncode messageLength copies left) (repetitionEncode messageLength copies right)

The repetition encoder preserves zero and coordinatewise XOR.

def Complexity.BooleanCode.repetitionCode (messageLength copies : ℕ) (hcopies : 0 < copies) : BooleanCode messageLength (messageLength * copies)

Concrete positive-copy repetition code.

Equations

• Complexity.BooleanCode.repetitionCode messageLength copies hcopies = { encode := Complexity.BooleanCode.repetitionEncode messageLength copies, encode_injective := ⋯ }

theorem Complexity.BooleanCode.repetitionCode_isLinear {messageLength copies : ℕ} (hcopies : 0 < copies) : (repetitionCode messageLength copies hcopies).IsLinear

The concrete repetition code is linear over GF(2).

theorem Complexity.BooleanCode.repetitionCode_rate {messageLength copies : ℕ} (hmessageLength : 0 < messageLength) (hcopies : 0 < copies) : rate messageLength (messageLength * copies) = 1 / ↑copies

At positive message length and copy count, the repetition-code rate is exactly the reciprocal of the copy count.

theorem Complexity.BooleanCode.repetitionCode_hasMinimumDistance {messageLength copies : ℕ} (hcopies : 0 < copies) : (repetitionCode messageLength copies hcopies).HasMinimumDistance copies

A positive-copy repetition code has minimum distance at least copies.

theorem Complexity.BooleanCode.repetitionCode_decodeUnique?_eq_some_of_close {messageLength copies radius : ℕ} (hcopies : 0 < copies) (hradius : 2 * radius < copies) (received : BooleanHamming.Word (messageLength * copies)) (message : BooleanHamming.Word messageLength) (hclose : BooleanHamming.distance ((repetitionCode messageLength copies hcopies).encode message) received ≤ radius) : (repetitionCode messageLength copies hcopies).decodeUnique? received radius = some message

Repetition decoding recovers a message from every received word within a radius strictly below half the copy count.

theorem Complexity.BooleanCode.repetitionCode_packing_bound {messageLength copies radius : ℕ} (hcopies : 0 < copies) (hradius : 2 * radius < copies) : 2 ^ messageLength * BooleanHamming.volume (messageLength * copies) radius ≤ 2 ^ (messageLength * copies)

Specialized packing inequality for the concrete repetition code.