Residue and injectivity of disjoint affine cubes

At each coordinate all sums collapse to at most one direction. Summing those coordinate identities makes the full Hamming residue affine over ZMod 3 in the zero/one interpretations of the cube parameters.

theorem Algebraic.BooleanCube.ModThree.Internal.cubeLinearMap_coordinate {ι : Type u_1} {J : Type u_2} [Fintype J] (v : J → ι → ZMod 2) (disjoint : DisjointDirections v) (z : J → ZMod 2) (j : J) (i : ι) (nonzero : v j i ≠ 0) : (cubeLinearMap v) z i = z j * v j i

A coordinate touched by a direction reads only that cube parameter.

theorem Algebraic.BooleanCube.ModThree.Internal.affineCube_injective {ι : Type u_1} {J : Type u_2} [Fintype J] (a : ι → ZMod 2) (v : J → ι → ZMod 2) (disjoint : DisjointDirections v) (nonzero : ∀ (j : J), v j ≠ 0) : Function.Injective (affineCube a v)

Disjoint nonzero directions give an injective affine cube.

theorem Algebraic.BooleanCube.ModThree.Internal.residue_affineCube {ι : Type u_1} {J : Type u_2} [Fintype ι] [Fintype J] (a : ι → ZMod 2) (v : J → ι → ZMod 2) (disjoint : DisjointDirections v) (z : J → ZMod 2) : residue (affineCube a v z) = residue a + ∑ j : J, bit (z j) * (residue (a + v j) - residue a)

Full Hamming residue restricts to a signed affine sum on a disjoint cube.