def
definition
systemOfMask
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 36.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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 :=
46 { 𝓗 := linearFamily }
47
48/-- Each mask contributes exactly 2 systems. -/
49lemma twoSystems_length (n mask : Nat) :
50 ([systemOfMask n mask false, systemOfMask n mask true] : List (XORSystem n)).length = 2 := rfl
51
52/-- Linear family length bound: exactly 2 * (n+1)².
53 Proof sketch: flatMap over range(k) where each element contributes list of length 2
54 gives total length k * 2 = 2 * (n+1)². -/
55lemma linearFamily_length_eq (n : Nat) :
56 (linearFamily n).length = 2 * (n.succ ^ 2) := by
57 unfold linearFamily
58 induction (n.succ ^ 2) with
59 | zero => simp
60 | succ k ih =>
61 simp only [List.range_succ, List.flatMap_append, List.flatMap_singleton, List.length_append]
62 rw [ih]
63 simp only [twoSystems_length]
64 omega
65
66/-- Linear family length bound O((n+1)²). -/