A signed MOD3 cube inside a binary affine solution set

Choose disjoint coordinate blocks, each containing more than twice as many coordinates as the system has equations. Every affine solution coset then contains an injective cube with one direction in each block. On that cube the full Hamming residue is a sum of independent zero/one parameters with nonzero coefficients in ZMod 3; each coefficient is therefore 1 or -1.

theorem Algebraic.BooleanCube.ModThree.residue_affineCube {ι : Type u_1} {J : Type u_3} [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)

Hamming residue on a disjoint cube is the affine sum of the single-direction residue changes, with each cube parameter interpreted as zero or one.

theorem Algebraic.BooleanCube.ModThree.exists_affineCube_of_disjoint_blocks {ι : Type u_1} {κ : Type u_2} {J : Type u_3} [Fintype ι] [Fintype κ] [Fintype J] (R : (ι → ZMod 2) →ₗ[ZMod 2] κ → ZMod 2) (a : ι → ZMod 2) (B : J → Finset ι) (disjoint : Pairwise fun (j k : J) => Disjoint (B j) (B k)) (large : ∀ (j : J), 2 * Fintype.card κ < (B j).card) : ∃ (v : J → ι → ZMod 2), DisjointDirections v ∧ Function.Injective (affineCube a v) ∧ (∀ (z : J → ZMod 2), R (affineCube a v z) = R a) ∧ (∀ (j : J), residue (a + v j) - residue a ≠ 0) ∧ ∀ (z : J → ZMod 2), residue (affineCube a v z) = residue a + ∑ j : J, bit (z j) * (residue (a + v j) - residue a)

Each sufficiently large disjoint coordinate block supplies one independent MOD3 direction inside the original affine solution coset.

theorem Algebraic.BooleanCube.ModThree.exists_signed_cube {n q : ℕ} (R : (Fin n → ZMod 2) →ₗ[ZMod 2] Fin q → ZMod 2) (a : Fin n → ZMod 2) : ∃ (L : (Fin (n / (2 * q + 1)) → ZMod 2) →ₗ[ZMod 2] Fin n → ZMod 2) (δ : Fin (n / (2 * q + 1)) → ZMod 3), Function.Injective ⇑L ∧ (∀ (z : Fin (n / (2 * q + 1)) → ZMod 2), R (L z) = 0) ∧ (∀ (j : Fin (n / (2 * q + 1))), δ j = 1 ∨ δ j = -1) ∧ ∀ (z : Fin (n / (2 * q + 1)) → ZMod 2), residue (a + L z) = residue a + ∑ j : Fin (n / (2 * q + 1)), bit (z j) * δ j

Any q binary linear equations on n coordinates retain a signed MOD3 cube of dimension n / (2*q+1) in every affine solution coset.