Boolean repetition codes -- proof internals

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

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

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

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