Hamming residue on binary affine parametrizations

The residue records the full Hamming weight modulo three, rather than one Boolean residue predicate. Coordinates are elements of ZMod 2, with their usual zero/one interpretation. An affine parametrization has coordinates a i + L i u.

def Algebraic.BooleanCube.ModThree.bit (x : ZMod 2) : ZMod 3

A binary coordinate, interpreted as a zero/one element of ZMod 3.

Equations

• Algebraic.BooleanCube.ModThree.bit x = if x = 0 then 0 else 1

def Algebraic.BooleanCube.ModThree.residue {ι : Type u_1} [Fintype ι] (x : ι → ZMod 2) : ZMod 3

The full Hamming-weight residue modulo three.

Equations

• Algebraic.BooleanCube.ModThree.residue x = ∑ i : ι, Algebraic.BooleanCube.ModThree.bit (x i)

def Algebraic.BooleanCube.ModThree.sign (x : ZMod 2) : ZMod 3

The sign character of a binary coordinate, with values in ZMod 3.

Equations

• Algebraic.BooleanCube.ModThree.sign x = if x = 0 then 1 else -1