linearSmallBias
The linearSmallBias definition supplies an explicit small-bias family candidate by assigning the linearFamily enumeration to the systems field of SmallBiasFamily. Complexity researchers examining deterministic constructions of small-bias XOR systems would reference this when testing linear-mask families for derandomization applications. The definition is a direct one-line wrapper that populates the structure with the mask-and-parity enumeration.
claimDefine the linear small-bias family by setting its systems map to the function that, for each $n$, produces the list of all XOR systems obtained by ranging over masks below $(n+1)^2$ and pairing each mask with both parity choices.
background
SmallBiasFamily is a structure containing one field that maps each dimension $n$ to a list of XOR systems of that dimension. Its intended use is to host families whose size grows polynomially while approximating pairwise independence, with the $n.succ$ convention avoiding zero-edge cases. The module treats this as a placeholder for concrete small-bias constructions inside SAT complexity analysis.
proof idea
One-line wrapper that applies linearFamily to fill the systems field of the SmallBiasFamily structure.
why it matters in Recognition Science
The definition supplies the concrete family instantiated by the downstream linearSmallBias_poly instance, which attaches the HasPolySize property via the linearFamily_poly_bound lemma. It therefore serves as the explicit linear-mask candidate inside the SAT.SmallBias development, leaving open the verification that the generated systems actually achieve small bias.
scope and limits
- Does not establish that the enumerated systems satisfy the small-bias property.
- Does not derive any bound on the bias parameter itself.
- Does not connect the construction to physical constants or forcing-chain steps.
- Does not treat the $n=0$ case directly.
formal statement (Lean)
45def linearSmallBias : SmallBiasFamily :=
proof body
Definition body.
46 { 𝓗 := linearFamily }
47
48/-- Each mask contributes exactly 2 systems. -/