geoSmallBias_poly
plain-language theorem explainer
The declaration shows that the geometric small-bias family built from Morton octant masks has polynomial size. Researchers working on small-bias constructions for derandomization or SAT complexity in the Recognition Science setting would cite it to confirm the family meets the required growth bound. The proof is a one-line wrapper that supplies the explicit constants 4 and 2 together with the quadratic bound lemma for the underlying geometric family.
Claim. The geometric small-bias family satisfies the polynomial-size property: there exist constants $c=4$ and $k=2$ such that for every natural number $n$, the cardinality of the family at $n$ is at most $4(n+1)^2$.
background
The module defines the geometric XOR family as the extension of the linear mask family by Morton-curve-aligned octant parity constraints. The SmallBiasFamily record packages this family for isolation arguments, while the HasPolySize class encodes the requirement that family size grows at most polynomially via the bound predicate on $n.succ^k$ (using $n.succ$ to avoid the zero case). Upstream, geoFamily_poly_bound proves the concrete quadratic estimate $(geoFamily n).length ≤ 4 · n.succ² by splitting into linear and Morton-octant components, and geoSmallBias simply sets the family field to geoFamily.
proof idea
The proof is a one-line wrapper that directly constructs the HasPolySize witness by pairing the constants 4 and 2 with the function that applies geoFamily_poly_bound at each n.
why it matters
This instance places the geometric family inside the small-bias track of the SAT complexity development by verifying the size condition required for HasPolySize. It rests on the quadratic bound for geoFamily and the definition of geoSmallBias, supporting later use in isolation or derandomization steps within the Recognition Science framework. No downstream theorems are recorded, leaving open its concrete application to pairwise-independence approximations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.