systemOfMask
plain-language theorem explainer
systemOfMask constructs a singleton XOR system from a mask and parity bit over n variables. Complexity researchers building explicit small-bias families cite this when forming deterministic linear enumerations of XOR systems. The definition is a one-line wrapper that applies constraintOfMask and returns the result as a list.
Claim. For natural numbers $n$ and $mask$ together with boolean $parity$, the value systemOfMask$(n, mask, parity)$ is the list containing the single XOR constraint whose variables are selected by maskVars $n$ $mask$ and whose parity equals the supplied boolean.
background
XORSystem $n$ is an abbreviation for the type of lists of XOR constraints on $n$ variables. constraintOfMask $n$ $mask$ $parity$ builds one constraint by setting its variable set to maskVars $n$ $mask$ and its parity flag to the given boolean. The module supplies placeholder structures for an explicit small-bias family of XOR systems.
proof idea
The definition is a one-line wrapper that applies constraintOfMask to the three arguments and places the result inside a singleton list literal.
why it matters
linearFamily depends directly on systemOfMask to enumerate both parities for each mask below $(n+1)^2$, producing the deterministic family of size $2(n+1)^2$. This supplies the linear-mask small-bias candidate inside the Complexity.SAT.SmallBias module and feeds the length lemmas that bound the family size.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.