Nisan--Wigderson set systems and generators

This module exposes an exact finite interface for the set systems and generator used in the metacomplexity reconstruction. Blocks are injectively enumerated, their intersection costs are finite natural numbers, and the associated NW generator is definitionally a BitGenerator.

Combining the random-string statistical-test theorem with the finite hybrid lemma shows that every dense random test against a low-complexity NW generator has an oriented adjacent hybrid gap of at least its density divided by the output length. The public submodules also connect that gap to an exact next-bit predictor and realize the weak-design predecessor term as the entry count of canonical overlap-indexed hardwiring tables. A fixed-advice reconstruction then assembles those tables, outside seed coordinates, candidate bit, and later tail into exactly the query evaluated by that predictor. Finite fiber averaging fixes one such advice choice while preserving the predictor's full agreement rate.

@[simp]

theorem Complexity.NWDesign.card_support {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (output : Fin outputLength) : (design.support output).card = inputLength

Every block support has exactly the hard function's input length.

theorem Complexity.NWDesign.mem_support_iff {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (output : Fin outputLength) (coordinate : Fin seedLength) : coordinate ∈ design.support output ↔ ∃ (input : Fin inputLength), (design.coordinates output) input = coordinate

A seed coordinate lies in a block support exactly when it is named by the block's injective enumeration.

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

Design-block overlap is symmetric.

@[simp]

theorem Complexity.NWDesign.overlap_self {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (output : Fin outputLength) : design.overlap output output = inputLength

A block overlaps itself in exactly all inputLength coordinates.

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

No pair of blocks overlaps in more than inputLength coordinates.

theorem Complexity.NWDesign.HasOverlapBudget.mono {outputLength inputLength seedLength first second : ℕ} {design : NWDesign outputLength inputLength seedLength} (hbudget : design.HasOverlapBudget first) (hle : first ≤ second) : design.HasOverlapBudget second

Enlarging the overlap budget preserves the weak-design property.

@[simp]

theorem Complexity.NWDesign.restrictSeed_apply {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (output : Fin outputLength) (seed : Fin seedLength → Bool) (input : Fin inputLength) : design.restrictSeed output seed input = seed ((design.coordinates output) input)

Seed restriction is evaluation along the block's coordinate embedding.

@[simp]

theorem Complexity.NWDesign.generator_apply {outputLength inputLength seedLength : ℕ} (design : NWDesign outputLength inputLength seedLength) (hardFunction : (Fin inputLength → Bool) → Bool) (seed : Fin seedLength → Bool) (output : Fin outputLength) : design.generator hardFunction seed output = hardFunction (design.restrictSeed output seed)

Each NW output bit evaluates the hard function on the corresponding restricted seed.

theorem Complexity.NWDesign.exists_oriented_hybridGap_of_randomTest {outputLength inputLength seedLength tapes time threshold : ℕ} {design : NWDesign outputLength inputLength seedLength} {hardFunction : (Fin inputLength → Bool) → Bool} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} {density : ℚ} (houtputLength : 0 < outputLength) (hlow : (design.generator hardFunction).HasLowTimeBoundedComplexity machine time threshold) (hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold) (hdense : BitGenerator.IsDenseTest test density) : ∃ (complement : Bool), ∃ step < outputLength, density / ↑outputLength ≤ (design.generator hardFunction).hybridGap (BitGenerator.orientTest test complement) step

A dense random-string test against a low-complexity NW generator yields an oriented adjacent hybrid gap of at least density / outputLength.

theorem Complexity.NWDesign.exists_oriented_hybridGap_of_seedDescriptions {outputLength inputLength seedLength tapes time threshold : ℕ} {design : NWDesign outputLength inputLength seedLength} {hardFunction : (Fin inputLength → Bool) → Bool} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} {density : ℚ} (houtputLength : 0 < outputLength) (hseedLength : seedLength < threshold) (hproduces : ∀ (seed : Fin seedLength → Bool), machine.ProducesInTime (List.ofFn seed) (List.ofFn (design.generator hardFunction seed)) time) (hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold) (hdense : BitGenerator.IsDenseTest test density) : ∃ (complement : Bool), ∃ step < outputLength, density / ↑outputLength ≤ (design.generator hardFunction).hybridGap (BitGenerator.orientTest test complement) step

Hirahara's finite NW hybrid bridge with the low-complexity premise discharged by direct short-seed descriptions.

theorem Complexity.NWDesign.exists_predictionSuccess_ge_half_add_density_div {outputLength inputLength seedLength tapes time threshold : ℕ} {design : NWDesign outputLength inputLength seedLength} {hardFunction : (Fin inputLength → Bool) → Bool} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} {density : ℚ} (houtputLength : 0 < outputLength) (hlow : (design.generator hardFunction).HasLowTimeBoundedComplexity machine time threshold) (hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold) (hdense : BitGenerator.IsDenseTest test density) : ∃ (complement : Bool) (step : Fin outputLength), 1 / 2 + density / ↑outputLength ≤ NextBitPrediction.successProbability ((design.generator hardFunction).targetBit step) ((design.generator hardFunction).testAtCandidate (BitGenerator.orientTest test complement) step)

End-to-end finite probabilistic NW reconstruction step: a dense random test against a low-complexity generator yields a polarity and coordinate whose canonical next-bit predictor succeeds with probability at least 1/2 + density / outputLength.

theorem Complexity.NWDesign.exists_predictionSuccess_ge_half_add_density_div_of_seedDescriptions {outputLength inputLength seedLength tapes time threshold : ℕ} {design : NWDesign outputLength inputLength seedLength} {hardFunction : (Fin inputLength → Bool) → Bool} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} {density : ℚ} (houtputLength : 0 < outputLength) (hseedLength : seedLength < threshold) (hproduces : ∀ (seed : Fin seedLength → Bool), machine.ProducesInTime (List.ofFn seed) (List.ofFn (design.generator hardFunction seed)) time) (hrandom : BitGenerator.IsTimeBoundedRandomTest test machine time threshold) (hdense : BitGenerator.IsDenseTest test density) : ∃ (complement : Bool) (step : Fin outputLength), 1 / 2 + density / ↑outputLength ≤ NextBitPrediction.successProbability ((design.generator hardFunction).targetBit step) ((design.generator hardFunction).testAtCandidate (BitGenerator.orientTest test complement) step)

The same concrete next-bit prediction guarantee with low complexity discharged by direct production from seeds shorter than the threshold.