linearFamily_length_eq
plain-language theorem explainer
The lemma establishes that the linear family of XOR systems on n variables has cardinality exactly 2(n+1)^2. Researchers constructing explicit small-bias spaces or polynomial-size SAT instances would cite this exact count. The argument proceeds by induction on the square of the successor of n, reducing via the auxiliary fact that each mask contributes precisely two systems.
Claim. Let $L(n)$ be the list of XOR systems on $n$ variables formed by ranging over all masks $0$ to $(n+1)^2-1$ and, for each mask, adjoining the two systems with even and odd parity. Then $|L(n)|=2(n+1)^2$.
background
The module supplies a placeholder structure for an explicit small-bias family of XOR systems. The linearFamily definition enumerates (mask, parity) pairs for mask < (n+1)^2 by flat-mapping List.range ((n.succ)^2) and producing, for each mask, the pair of systems given by systemOfMask n mask false and systemOfMask n mask true. The twoSystems_length lemma records that each such pair has length exactly 2. Upstream arithmetic supplies the successor operation appearing in the exponent.
proof idea
The proof unfolds linearFamily and inducts on (n.succ)^2. The zero base case closes by simplification. The successor step simplifies the flatMap-append structure, applies the induction hypothesis, rewrites with twoSystems_length, and finishes by omega arithmetic.
why it matters
The equality is invoked directly by linearFamily_length_bound to obtain the O((n+1)^2) bound and by geoFamily_poly_bound to control the size of the geometric family. It supplies the precise cardinality required for the small-bias construction in the Complexity.SAT module, enabling downstream polynomial bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.