geoSmallBias
plain-language theorem explainer
The geoSmallBias definition supplies the geometric XOR family as a concrete small-bias family candidate built from linear masks plus Morton octant constraints. Researchers studying geometric SAT hardness or small-bias approximations in XOR systems would cite this construction when establishing polynomial-size families. The definition is a direct one-line wrapper that populates the sole field of the SmallBiasFamily structure with the output of geoFamily.
Claim. Let $H_{geo}(n)$ be the list of XOR systems formed by concatenating the linear family with the Morton octant family at width $n$. Then geoSmallBias is the small-bias family whose component $H$ equals $H_{geo}$.
background
The module defines the geometric XOR family $H_{geo}(n)$ that augments the linear mask family with Morton-curve-aligned octant parity constraints; each octant contributes exactly two systems. The SmallBiasFamily structure is a placeholder whose sole field $H$ maps each natural number $n$ to a list of XOR systems of width $n$, with the intended property that the family size remains polynomial and approximates pairwise independence. This sits inside the SAT complexity development that imports the CNF, XOR, and SmallBias modules.
proof idea
The definition is a one-line wrapper that applies geoFamily to populate the $H$ field of the SmallBiasFamily structure.
why it matters
This definition supplies the concrete family that the downstream instance geoSmallBias_poly uses to establish polynomial size via the bound geoFamily_poly_bound. It fills the geometric candidate slot in the SAT isolation arguments, extending the linear family with octant masks to achieve the required small-bias approximation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.