HasPolySize
plain-language theorem explainer
A family of XOR systems has polynomial size if the number of systems for each variable count n is bounded by a polynomial in n. Researchers constructing explicit small-bias spaces for derandomization cite this property to control family cardinality. The definition encodes the bound directly via an existential statement over constants c and k applied to list lengths.
Claim. Let $F$ be a family of XOR systems. Then $F$ has polynomial size if there exist natural numbers $c,k$ such that for every natural number $n$, the length of the list of systems for $n$ variables satisfies $|F(n)|$ ≤ $c · (n+1)^k$.
background
SmallBiasFamily is a structure that maps each natural number n to a list of XOR systems on n variables. The module supplies placeholder structures for explicit small-bias families of XOR systems in the SAT complexity setting. The bound employs the successor operation on n to treat the zero case uniformly and keep the growth O(n^k).
proof idea
This is a class definition with no proof body. It states the polynomial-size property directly as an existential quantifier over constants c and k, with the length comparison applied to the family map at each n.
why it matters
The property is instantiated for the linear small-bias family and the geometric small-bias family through the downstream instances linearSmallBias_poly and geoSmallBias_poly. It supplies the polynomial-size handle for the explicit linear-mask family described in the module comment, enabling further combinatorial arguments. In the Recognition framework this scaffolds the complexity layer that may interface with the forcing chain via explicit constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.