Nisan--Wigderson set systems and generators -- definitions

An NWDesign m ell d is an ordered family of m injectively enumerated ell-coordinate subsets of a d-bit seed. Injective enumerations avoid cardinality casts when restricting a seed and retain the coordinate order used by the hard Boolean function.

The exact weak-design resource is recorded as a natural-number overlap cost. At output coordinate i, it is the sum of 2^|S_i ∩ S_j| over predecessors j < i, plus one unit for every later output coordinate. A separate predicate bounds this cost uniformly, allowing later analytic estimates to choose their own integer upper bound.

structure Complexity.NWDesign (outputLength inputLength seedLength : ℕ) : Type

An ordered family of injectively enumerated coordinate subsets for the Nisan--Wigderson generator.

• coordinates : Fin outputLength → Fin inputLength ↪ Fin seedLength

  The inputLength distinct seed coordinates used by each output bit.

def Complexity.NWDesign.support {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (output : Fin outputLength) : Finset (Fin seedLength)

The underlying coordinate set of one design block.

Equations

• design.support output = Finset.map (design.coordinates output) Finset.univ

def Complexity.NWDesign.overlap {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (first second : Fin outputLength) : ℕ

Cardinality of the intersection of two design blocks.

Equations

• design.overlap first second = (design.support first ∩ design.support second).card

def Complexity.NWDesign.overlapCostAt {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (output : Fin outputLength) : ℕ

Exact predecessor-overlap resource at one output coordinate, including one unit for each later output coordinate as in Hirahara's weak-design bound.

Equations

• design.overlapCostAt output = ∑ previous < output, 2 ^ design.overlap output previous + (outputLength - (↑output + 1))

def Complexity.NWDesign.HasOverlapBudget {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (budget : ℕ) : Prop

Every coordinate's exact overlap cost is at most budget.

Equations

• design.HasOverlapBudget budget = ∀ (output : Fin outputLength), design.overlapCostAt output ≤ budget

def Complexity.NWDesign.restrictSeed {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (output : Fin outputLength) (seed : Fin seedLength → Bool) : Fin inputLength → Bool

Restrict a seed to the ordered coordinates of one design block.

Equations

• design.restrictSeed output seed input = seed ((design.coordinates output) input)

def Complexity.NWDesign.generator {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) : BitGenerator seedLength outputLength

The Nisan--Wigderson generator associated to a design and a Boolean function on one design block.

Equations

• design.generator hardFunction seed output = hardFunction (design.restrictSeed output seed)