linearSmallBias_poly
plain-language theorem explainer
The instance certifies that the linear-mask small-bias family meets the polynomial-size requirement of HasPolySize. Researchers constructing explicit small-bias generators for derandomization or SAT approximation cite this when they need a concrete O(n^2) family of XOR systems. The proof is a one-line wrapper that directly supplies the bound witness from the linear-family length lemma.
Claim. Let $F$ be the linear-mask small-bias family with systems generated by linearFamily. Then $F$ satisfies the HasPolySize property: there exist constants $c,k$ such that for every $n$ the number of systems in $F(n)$ is at most $c(n+1)^k$.
background
SmallBiasFamily is a structure whose field H maps each n to a list of XOR systems; the module treats it as a placeholder for an explicit family that approximates pairwise independence. HasPolySize is the class whose sole field is the bound predicate requiring the list length to be polynomial in n, using n.succ to avoid the zero case. linearSmallBias is the concrete definition that sets H to linearFamily, the family obtained by taking every square-many linear masks paired with both parity choices.
proof idea
The instance is witnessed by the term linearFamily_poly_bound. That lemma supplies the existential witness with c=2 and k=2, which in turn reduces to the length bound on linearFamily.
why it matters
This declaration supplies the HasPolySize instance for the linear small-bias family, closing the Track A scaffold that lets downstream combinatorial arguments treat an explicit polynomial-size family of XOR systems as given. It sits inside the Complexity.SAT.SmallBias module whose module doc describes an explicit small-bias family of XOR systems, providing the polynomial handle needed before bias or correlation properties can be analyzed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.