linearFamily_poly_bound
plain-language theorem explainer
The lemma witnesses a polynomial upper bound on the length of the linear family of XOR systems, establishing that its size grows at most quadratically in the dimension n. Researchers in complexity theory working on explicit small-bias generators and derandomization would cite this to confirm the family satisfies the polynomial-size requirement for HasPolySize. The proof is a one-line wrapper that supplies constants c=2 and k=2 then invokes the prior length bound lemma.
Claim. There exist natural numbers $c$ and $k$ such that for every natural number $n$, the length of the linear family of XOR systems at dimension $n$ satisfies $|L_n| ≤ c · (n+1)^k$.
background
The linear family is the deterministic construction that enumerates all masks below (n+1)^2 and, for each mask, produces two XOR systems differing only in parity. This serves as an explicit candidate small-bias family inside the SAT complexity module, whose overall setting is a placeholder structure for such families of XOR systems. The upstream lemma linearFamily_length_bound already shows the length is at most 2 · (n+1)^2; the successor operation is the standard Peano successor.
proof idea
The term proof refines the existential quantifier to the concrete witnesses c=2 and k=2. It then introduces the variable n and applies the linearFamily_length_bound lemma directly to obtain the required inequality.
why it matters
This lemma supplies the polynomial-size witness required by the downstream HasPolySize instance linearSmallBias_poly for the linear small-bias family. It therefore places the explicit linear-mask construction inside the polynomial-size regime of small-bias generators. The result sits in the Complexity domain and supports later claims about polynomial-size explicit constructions without invoking any Recognition Science forcing-chain landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.