linearSmallBias
plain-language theorem explainer
The linearSmallBias definition supplies an explicit small-bias family candidate by assigning the linearFamily enumeration to the systems field of SmallBiasFamily. Complexity researchers examining deterministic constructions of small-bias XOR systems would reference this when testing linear-mask families for derandomization applications. The definition is a direct one-line wrapper that populates the structure with the mask-and-parity enumeration.
Claim. Define the linear small-bias family by setting its systems map to the function that, for each $n$, produces the list of all XOR systems obtained by ranging over masks below $(n+1)^2$ and pairing each mask with both parity choices.
background
SmallBiasFamily is a structure containing one field that maps each dimension $n$ to a list of XOR systems of that dimension. Its intended use is to host families whose size grows polynomially while approximating pairwise independence, with the $n.succ$ convention avoiding zero-edge cases. The module treats this as a placeholder for concrete small-bias constructions inside SAT complexity analysis.
proof idea
One-line wrapper that applies linearFamily to fill the systems field of the SmallBiasFamily structure.
why it matters
The definition supplies the concrete family instantiated by the downstream linearSmallBias_poly instance, which attaches the HasPolySize property via the linearFamily_poly_bound lemma. It therefore serves as the explicit linear-mask candidate inside the SAT.SmallBias development, leaving open the verification that the generated systems actually achieve small bias.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.