twoSystems_length

formal source

  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
  71/-- Polynomial bound witness for the linear family. -/
  72lemma linearFamily_poly_bound :
  73    ∃ c k : Nat, ∀ n, (linearFamily n).length ≤ c * n.succ ^ k := by
  74  refine ⟨2, 2, ?_⟩
  75  intro n
  76  exact linearFamily_length_bound n
  77
  78instance linearSmallBias_poly : HasPolySize linearSmallBias :=
  79  ⟨linearFamily_poly_bound⟩