Nisan--Wigderson overlap hardwiring -- proof internals #

theorem Complexity.NWDesign.map_challengeOverlap_internal {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

theorem Complexity.NWDesign.card_challengeOverlap_internal {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current previous : Fin outputLength) :

(design.challengeOverlap current previous).card = design.overlap current previous

theorem Complexity.NWDesign.seedWithChallenge_apply_coordinates_internal {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

theorem Complexity.NWDesign.seedWithChallenge_apply_of_not_mem_support_internal {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

theorem Complexity.NWDesign.challengedBlock_current_internal {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

theorem Complexity.NWDesign.challengedBlock_dependsOn_overlap_internal {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)

theorem Complexity.NWDesign.challengedValue_dependsOn_overlap_internal {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)

theorem Complexity.NWDesign.predecessorTable_restrict_internal {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)

theorem Complexity.NWDesign.card_predecessorAssignments_internal {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current previous : Fin outputLength) :

Fintype.card (↥(design.challengeOverlap current previous) → Bool) = 2 ^ design.overlap current previous

theorem Complexity.NWDesign.predecessorTableEntriesAt_eq_internal {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) :

design.predecessorTableEntriesAt current = ∑ previous < current, 2 ^ design.overlap current previous

theorem Complexity.NWDesign.overlapCostAt_eq_predecessorTableEntriesAt_add_internal {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) :

design.overlapCostAt current = design.predecessorTableEntriesAt current + (outputLength - (↑current + 1))

theorem Complexity.NWDesign.predecessorTableEntriesAt_le_overlapCostAt_internal {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (current : Fin outputLength) :

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

Documentation