linearFamily_length_bound
plain-language theorem explainer
The lemma establishes an upper bound of 2(n+1)^2 on the length of the linear family of XOR systems over n variables. Researchers building explicit small-bias generators for SAT would cite this polynomial size control. The proof is a one-line rewrite that invokes the exact length equality for the family.
Claim. For every natural number $n$, let $F_n$ be the list of XOR systems obtained by ranging over all masks below $(n+1)^2$ and both parity choices via systemOfMask. Then $|F_n| ≤ 2(n+1)^2$.
background
The linearFamily definition enumerates masks in the range 0 to (n+1)^2 and produces two XORSystem n instances per mask, one for each parity, using systemOfMask. This yields a deterministic candidate family inside the SmallBias module, whose module doc describes it as placeholder structure for an explicit small-bias family of XOR systems. The upstream lemma linearFamily_length_eq proves the length equals exactly 2(n.succ)^2 by induction on the range size, with base case zero and inductive step preserving the factor of two.
proof idea
The proof is a one-line wrapper that rewrites the target inequality using the exact length equality lemma linearFamily_length_eq.
why it matters
The bound is invoked directly by the downstream lemma linearFamily_poly_bound, which witnesses constants c=2 and k=2 such that the length is at most c n^k for all n. This supplies the polynomial-size witness required for the small-bias construction in the SAT complexity setting. The result therefore closes the size-control step inside the linearFamily definition before any bias analysis begins.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.