15class HasPolySize (F : SmallBiasFamily) : Prop where 16 bound : ∃ c k : Nat, ∀ n, (F.𝓗 n).length ≤ c * n.succ^k 17 18/-! ## Explicit linear-mask family (Track A scaffold) 19 20We instantiate a concrete deterministic family by taking every square-many 21linear masks (viewed as bitmasks over the `n` variables) and pairing each mask 22with both parity choices. This yields `O(n^2)` XOR systems, giving us a 23polynomial-size handle for further combinatorial proofs. -/ 24 25open List 26 27/-- Set of variables selected by a bitmask `mask`. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.