twoSystems_length
plain-language theorem explainer
Each mask generates exactly two XOR systems, one for each parity choice. Researchers deriving cardinality bounds for small-bias families inside Recognition Science cite this when sizing linear SAT instances. The proof is immediate reflexivity on the explicit two-element list.
Claim. For natural numbers $n$ and $mask$, the list formed by the single-constraint XOR system with even parity and the one with odd parity has length exactly 2.
background
The module supplies a placeholder for an explicit small-bias family of XOR systems. XORSystem $n$ is the type of lists of XOR constraints on $n$ variables. The generator systemOfMask $n$ $mask$ $parity$ returns the singleton list holding the parity constraint selected by the mask.
proof idea
Term proof by reflexivity. The equality holds definitionally for the literal two-element list.
why it matters
Supplies the base counting step for linearFamily_length_eq, which establishes family size exactly $2(n+1)^2$. This supports the combinatorial construction of small-bias XOR families, consistent with discrete counting derived from phi-forcing chains and spectral emergence structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.