Nisan--Wigderson overlap hardwiring

When one NW block is replaced by a challenge, each predecessor block depends on only the challenge coordinates in their intersection. Its observed Boolean value is therefore recoverable from a canonical table with exactly 2^|S_i ∩ S_j| entries. Summing these entry counts gives precisely the predecessor term in the design's overlap cost.

theorem Complexity.NWDesign.map_challengeOverlap {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current previous : Fin outputLength) : Finset.map (design.coordinates current) (design.challengeOverlap current previous) = design.support current ∩ design.support previous

Mapping overlap coordinates through the current block embedding produces exactly the intersection of the two block supports.

@[simp]

theorem Complexity.NWDesign.card_challengeOverlap {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current previous : Fin outputLength) : (design.challengeOverlap current previous).card = design.overlap current previous

Challenge overlap has exactly the design's recorded intersection size.

@[simp]

theorem Complexity.NWDesign.seedWithChallenge_apply_coordinates {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) (outside : Fin seedLength → Bool) (challenge : Fin inputLength → Bool) (input : Fin inputLength) : design.seedWithChallenge current outside challenge ((design.coordinates current) input) = challenge input

Inserting a challenge makes the current block read exactly that challenge.

theorem Complexity.NWDesign.seedWithChallenge_apply_of_not_mem_support {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) (outside : Fin seedLength → Bool) (challenge : Fin inputLength → Bool) (coordinate : Fin seedLength) (hcoordinate : coordinate ∉ design.support current) : design.seedWithChallenge current outside challenge coordinate = outside coordinate

Challenge insertion leaves every coordinate outside the current support unchanged.

@[simp]

theorem Complexity.NWDesign.challengedBlock_current {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) (outside : Fin seedLength → Bool) (challenge : Fin inputLength → Bool) : design.challengedBlock current current outside challenge = challenge

The challenged current block is definitionally faithful to the challenge.

theorem Complexity.NWDesign.challengedBlock_dependsOn_overlap {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current previous : Fin outputLength) (outside : Fin seedLength → Bool) : DependsOn (design.challengedBlock current previous outside) ↑(design.challengeOverlap current previous)

A predecessor block depends on the challenge only through the two blocks' intersection coordinates.

theorem Complexity.NWDesign.challengedValue_dependsOn_overlap {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current previous : Fin outputLength) (outside : Fin seedLength → Bool) (observe : (Fin inputLength → Bool) → Bool) : DependsOn (fun (challenge : Fin inputLength → Bool) => observe (design.challengedBlock current previous outside challenge)) ↑(design.challengeOverlap current previous)

Any Boolean observation of a predecessor block has the same overlap-only dependency.

@[simp]

theorem Complexity.NWDesign.predecessorTable_restrict {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current previous : Fin outputLength) (outside : Fin seedLength → Bool) (observe : (Fin inputLength → Bool) → Bool) (challenge : Fin inputLength → Bool) : design.predecessorTable current previous outside observe (BooleanDependency.restrict (design.challengeOverlap current previous) challenge) = observe (design.challengedBlock current previous outside challenge)

Looking up the actual overlap restriction in the canonical predecessor table recovers the observed predecessor value.

theorem Complexity.NWDesign.card_predecessorAssignments {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current previous : Fin outputLength) : Fintype.card (↥(design.challengeOverlap current previous) → Bool) = 2 ^ design.overlap current previous

The assignment space indexing one predecessor table has exactly one entry for every Boolean assignment to the intersection.

theorem Complexity.NWDesign.predecessorTableEntriesAt_eq {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) : design.predecessorTableEntriesAt current = ∑ previous < current, 2 ^ design.overlap current previous

Total predecessor-table entries equal the sum of the standard exponential intersection costs.

theorem Complexity.NWDesign.overlapCostAt_eq_predecessorTableEntriesAt_add {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) : design.overlapCostAt current = design.predecessorTableEntriesAt current + (outputLength - (↑current + 1))

The exact design overlap cost is the predecessor-table cost plus one unit for every later output coordinate.

theorem Complexity.NWDesign.predecessorTableEntriesAt_le_overlapCostAt {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) : design.predecessorTableEntriesAt current ≤ design.overlapCostAt current

Predecessor tables fit within the exact overlap cost.

theorem Complexity.NWDesign.predecessorTableEntriesAt_le_of_hasOverlapBudget {outputLength inputLength seedLength budget : ℕ} {design : NWDesign outputLength inputLength seedLength} (hbudget : design.HasOverlapBudget budget) (current : Fin outputLength) : design.predecessorTableEntriesAt current ≤ budget

A weak-design overlap budget bounds all predecessor hardwiring tables.