def
definition
linearFamily
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Complexity.SAT.SmallBias on GitHub at line 40.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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)²). -/
67lemma linearFamily_length_bound (n : Nat) :
68 (linearFamily n).length ≤ 2 * (n.succ ^ 2) := by
69 rw [linearFamily_length_eq]
70