IndisputableMonolith.Complexity.SAT.SmallBias

   1import Mathlib
   2import IndisputableMonolith.Complexity.SAT.CNF
   3import IndisputableMonolith.Complexity.SAT.XOR
   4
   5namespace IndisputableMonolith
   6namespace Complexity
   7namespace SAT
   8
   9/-- Placeholder structure for an explicit small-bias family of XOR systems. -/
  10structure SmallBiasFamily where
  11  𝓗 : (n : Nat) → List (XORSystem n)
  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 :=
  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⟩
  80
  81end SAT
  82end Complexity
  83end IndisputableMonolith
  84