Nisan--Wigderson overlap hardwiring -- definitions

Fixing an NW output coordinate turns its block input into a challenge and leaves all seed coordinates outside that block fixed. A predecessor block can then vary only through the challenge coordinates lying in the two blocks' intersection. This module defines that challenge experiment and its canonical hardwiring table.

def Complexity.NWDesign.challengeOverlap {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current previous : Fin outputLength) : Finset (Fin inputLength)

Challenge coordinates of current whose seed positions also occur in previous.

Equations

• design.challengeOverlap current previous = {input : Fin inputLength | (design.coordinates current) input ∈ design.support previous}

def Complexity.NWDesign.seedWithChallenge {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) (outside : Fin seedLength → Bool) (challenge : Fin inputLength → Bool) : Fin seedLength → Bool

Replace the seed coordinates in one design block by a challenge, retaining an outside assignment on every other coordinate. The finite inverse of the block embedding makes this operation executable.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.NWDesign.challengedBlock {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current previous : Fin outputLength) (outside : Fin seedLength → Bool) : (Fin inputLength → Bool) → Fin inputLength → Bool

The input seen by a block when current carries the challenge and all coordinates outside current are fixed.

Equations

• design.challengedBlock current previous outside challenge = design.restrictSeed previous (design.seedWithChallenge current outside challenge)

def Complexity.NWDesign.predecessorTable {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current previous : Fin outputLength) (outside : Fin seedLength → Bool) (observe : (Fin inputLength → Bool) → Bool) : (↥(design.challengeOverlap current previous) → Bool) → Bool

The canonical advice table for an observed predecessor-block value. Its indices are assignments to precisely the overlap coordinates.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.NWDesign.predecessorTableEntriesAt {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) : ℕ

Total number of Boolean entries in all predecessor tables at one output coordinate.

Equations

• design.predecessorTableEntriesAt current = ∑ previous < current, Fintype.card (↥(design.challengeOverlap current previous) → Bool)