Ok, so your first paragraph holds for how addition is defined in this context:
It can essentially be thought of as vector addition. It should also be noted: we are working in ##\mathbb Z_{2}## (well, this is how we formed the basis of the addition anyway, but these are binary block codes)...
What do you mean by "the 1-bit additions carry"? I'm assuming they don't in this context because for any code x,y x+y = 0. So any instance of 1+1 = 0. Sorry, if I'm misunderstanding. I naively assumed the conventions of the field would more uniform like some other math courses I've taken...
I've been thinking about this since I posted and I think what you pointed out is what's bothering me. With the cases idea, it's easier to make use of the digits in the words themselves to more directly make the point.
For example:
A case where ##x = y##. If ##x = y##, then ##x + y = 0##, and...
I'm trying to prove the following:
##wt(x+y) \leq wt(x) + wt(y)##, where "wt(x)" is referring to the weight of a specific code word.
Proof:
For two code words ##x, y \in F^{n}_2##, we have the inequalities ##0 \leq wt(x)## and ##0 \leq wt(y)##. Adding these together, we have ##0 \leq wt(x) +...