constraintOfMask
plain-language theorem explainer
constraintOfMask assembles an XOR constraint by taking the variable subset selected by a bitmask and pairing it with a supplied parity bit. Researchers constructing explicit small-bias XOR families for complexity bounds cite the construction when they need a canonical single-constraint parity hash. The definition is a direct record literal that delegates variable selection to maskVars and copies the parity flag.
Claim. For $n,m∈ℕ$ and $p∈{0,1}$, the map returns the XOR constraint whose variable list is exactly the set of $v<n$ such that the $v$-th bit of $m$ is set and whose required parity equals $p$.
background
XORConstraint is the structure whose fields are a list of variables and a boolean parity; its defining doc-comment states that it encodes an XOR constraint over $n$ variables whose parity on the listed subset equals the given boolean. maskVars returns the filtered list of variables $v$ in the range $[0..n)$ for which Nat.testBit mask v.val holds. The module supplies placeholder structure for an explicit small-bias family of such XOR systems.
proof idea
One-line definition that builds the XORConstraint record by setting its vars field to the output of maskVars n mask and its parity field to the supplied boolean argument.
why it matters
The definition supplies the atomic building block for single-constraint XOR systems inside the small-bias family. It is invoked directly by systemOfMask to produce a singleton list that forms a parity-hash system. Within the Recognition Science framework the construction supports deterministic enumeration of (mask, parity) pairs required for linear small-bias families and the subsequent polynomial-size bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.