  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 :=
  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]

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.