Residue-changing directions under binary linear constraints

Fewer than half as many binary equations as coordinates cannot fix the full Hamming residue modulo three on any solution coset. This is the geometric step used on each coordinate block in the restricted-circuit MOD3 argument.

theorem Algebraic.BooleanCube.ModThree.exists_kernel_residue_ne {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (R : (ι → ZMod 2) →ₗ[ZMod 2] κ → ZMod 2) (a : ι → ZMod 2) (large : 2 * Fintype.card κ < Fintype.card ι) : ∃ (u : ι → ZMod 2), R u = 0 ∧ residue (a + u) ≠ residue a

A system with more than twice as many coordinates as equations admits a homogeneous direction that changes the full Hamming residue at any base point.