linearFamily_length_eq
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish any small-bias property of the generated systems.
- Does not apply to families using more than two systems per mask.
- Does not address satisfiability or bias parameters of the systems.
- Does not extend beyond finite natural numbers n.
Lean usage
rw [linearFamily_length_eq n]formal statement (Lean)
55lemma linearFamily_length_eq (n : Nat) :
56 (linearFamily n).length = 2 * (n.succ ^ 2) := by
proof body
Term-mode proof.
57 unfold linearFamily
58 induction (n.succ ^ 2) with
59 | zero => simp
60 | succ k ih =>
61 simp only [List.range_succ, List.flatMap_append, List.flatMap_singleton, List.length_append]
62 rw [ih]
63 simp only [twoSystems_length]
64 omega
65
66/-- Linear family length bound O((n+1)²). -/