linearFamily_poly_bound
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.
claimThere 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 in Recognition Science
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.
scope and limits
- Does not establish the small-bias property of the family.
- Does not optimize the constants c and k beyond the supplied witnesses.
- Applies only to the specific linear-mask enumeration, not to arbitrary families.
- Does not address asymptotic tightness or lower bounds on size.
Lean usage
instance linearSmallBias_poly : HasPolySize linearSmallBias := ⟨linearFamily_poly_bound⟩formal statement (Lean)
72lemma linearFamily_poly_bound :
73 ∃ c k : Nat, ∀ n, (linearFamily n).length ≤ c * n.succ ^ k := by
proof body
Term-mode proof.
74 refine ⟨2, 2, ?_⟩
75 intro n
76 exact linearFamily_length_bound n
77