linearFamily_length_bound
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove that the generated family satisfies the small-bias property.
- Does not supply an explicit bias parameter or its dependence on n.
- Does not address the time complexity of enumerating or evaluating the family.
- Does not link the construction to any forcing-chain step or Recognition constant.
Lean usage
refine ⟨2, 2, ?_⟩; intro n; exact linearFamily_length_bound nformal statement (Lean)
67lemma linearFamily_length_bound (n : Nat) :
68 (linearFamily n).length ≤ 2 * (n.succ ^ 2) := by
proof body
Term-mode proof.
69 rw [linearFamily_length_eq]
70
71/-- Polynomial bound witness for the linear family. -/