Boolean repetition codes -- definitions

The repetition encoder writes each of messageLength bits into copies coordinates, using the library's canonical Fin (messageLength * copies) block equivalence. It is defined even at zero copies; the code construction later requires positivity for injectivity.

def Complexity.BooleanCode.repetitionEncode (messageLength copies : ℕ) (message : BooleanHamming.Word messageLength) : BooleanHamming.Word (messageLength * copies)

Repeat every input bit in a block of copies output coordinates.

Equations

• Complexity.BooleanCode.repetitionEncode messageLength copies message = (Complexity.blocksEquiv messageLength copies).symm fun (input : Fin messageLength) (x : Fin copies) => message input