class
definition
HasPolySize
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Complexity.SAT.SmallBias on GitHub at line 15.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
12
13/-- Intended property: the family size is polynomial and approximates pairwise-independence.
14 Note: We use n.succ to avoid n=0 edge cases; this is still O(n^k). -/
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`. -/
28def maskVars (n mask : Nat) : List (Var n) :=
29 (List.finRange n).filter fun v => Nat.testBit mask v.val
30
31/-- XOR constraint induced by a mask/parity pair. -/
32def constraintOfMask (n mask : Nat) (parity : Bool) : XORConstraint n :=
33 { vars := maskVars n mask, parity := parity }
34
35/-- Single-constraint XOR system (parity hash). -/
36def systemOfMask (n mask : Nat) (parity : Bool) : XORSystem n :=
37 [constraintOfMask n mask parity]
38
39/-- Deterministic family: enumerate `(mask, parity)` pairs for mask < (n+1)^2. -/
40def linearFamily : (n : Nat) → List (XORSystem n) := fun n =>
41 (List.range ((n.succ) ^ 2)).flatMap fun mask =>
42 [systemOfMask n mask false, systemOfMask n mask true]
43
44/-- The linear-mask small-bias candidate. -/
45def linearSmallBias : SmallBiasFamily :=