Finite statistical tests for binary generators

This module formalizes the first finite step in Hirahara's 2018 Nisan--Wigderson reconstruction argument. A dense set of strings that are random for a time-bounded Kolmogorov threshold is a statistical test against any generator whose outputs all lie strictly below that threshold.

In particular, if the machine directly produces each generated output from its seed within the clock and the seed length is strictly below the randomness threshold, the test has zero acceptance probability on generated outputs. Its distinguishing advantage therefore equals its uniform density exactly.

Every finite test also has a canonical total Boolean oracle: fixed-length queries receive their membership bit and malformed lengths are rejected.

theorem Complexity.BitGenerator.isTimeBoundedRandomTest_iff_subset {outputLength tapes time threshold : ℕ} {test : Finset (Fin outputLength → Bool)} {machine : TM tapes} : IsTimeBoundedRandomTest test machine time threshold ↔ test ⊆ machine.timeBoundedRandomStrings outputLength time threshold

Being a time-bounded random-string test is exactly finite-set inclusion in the canonical set of strings at or above the chosen complexity threshold.

theorem Complexity.BitGenerator.timeBoundedRandomStrings_isRandomTest {tapes : ℕ} (machine : TM tapes) (outputLength time threshold : ℕ) : IsTimeBoundedRandomTest (machine.timeBoundedRandomStrings outputLength time threshold) machine time threshold

The full canonical set of threshold-random strings is a random-string test.

theorem Complexity.BitGenerator.timeBoundedRandomStrings_isDenseTest {tapes : ℕ} (machine : TM tapes) (outputLength time threshold : ℕ) : IsDenseTest (machine.timeBoundedRandomStrings outputLength time threshold) (1 - ↑(2 ^ threshold - 1) / 2 ^ outputLength)

The full random-string test has the quantitative uniform density supplied by strict finite incompressibility.

theorem Complexity.BitGenerator.hasLowTimeBoundedComplexity_of_seedDescriptions {seedLength outputLength tapes time threshold : ℕ} {generator : BitGenerator seedLength outputLength} {machine : TM tapes} (hseedLength : seedLength < threshold) (hproduces : ∀ (seed : Fin seedLength → Bool), machine.ProducesInTime (List.ofFn seed) (List.ofFn (generator seed)) time) : generator.HasLowTimeBoundedComplexity machine time threshold

If the machine produces every generated output directly from its seed and the seed is shorter than the threshold, every output has complexity below the threshold. This is the finite description step used for efficiently computable short-seed generators.

theorem Complexity.BitGenerator.output_not_mem_of_randomTest {seedLength outputLength tapes time threshold : ℕ} {generator : BitGenerator seedLength outputLength} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} (hlow : generator.HasLowTimeBoundedComplexity machine time threshold) (hrandom : IsTimeBoundedRandomTest test machine time threshold) (seed : Fin seedLength → Bool) : generator seed ∉ test

A low-complexity generator output cannot belong to a test containing only strings at or above the same complexity threshold.

theorem Complexity.BitGenerator.acceptedSeeds_eq_empty_of_randomTest {seedLength outputLength tapes time threshold : ℕ} {generator : BitGenerator seedLength outputLength} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} (hlow : generator.HasLowTimeBoundedComplexity machine time threshold) (hrandom : IsTimeBoundedRandomTest test machine time threshold) : generator.acceptedSeeds test = ∅

The test accepts no seed of a low-complexity generator.

theorem Complexity.BitGenerator.generatedAcceptanceProbability_eq_zero_of_randomTest {seedLength outputLength tapes time threshold : ℕ} {generator : BitGenerator seedLength outputLength} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} (hlow : generator.HasLowTimeBoundedComplexity machine time threshold) (hrandom : IsTimeBoundedRandomTest test machine time threshold) : generator.generatedAcceptanceProbability test = 0

A random-string test has exactly zero acceptance probability under any generator whose outputs are all below its complexity threshold.

theorem Complexity.BitGenerator.distinguishingAdvantage_eq_uniform_of_randomTest {seedLength outputLength tapes time threshold : ℕ} {generator : BitGenerator seedLength outputLength} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} (hlow : generator.HasLowTimeBoundedComplexity machine time threshold) (hrandom : IsTimeBoundedRandomTest test machine time threshold) : generator.distinguishingAdvantage test = uniformAcceptanceProbability test

For a random-string test against a low-complexity generator, the absolute distinguishing advantage is exactly the test's uniform acceptance probability.

theorem Complexity.BitGenerator.density_le_distinguishingAdvantage_of_randomTest {seedLength outputLength tapes time threshold : ℕ} {generator : BitGenerator seedLength outputLength} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} {density : ℚ} (hlow : generator.HasLowTimeBoundedComplexity machine time threshold) (hrandom : IsTimeBoundedRandomTest test machine time threshold) (hdense : IsDenseTest test density) : density ≤ generator.distinguishingAdvantage test

A density-dense random-string test distinguishes every low-complexity generator with advantage at least density.

theorem Complexity.BitGenerator.density_le_distinguishingAdvantage_of_seedDescriptions {seedLength outputLength tapes time threshold : ℕ} {generator : BitGenerator seedLength outputLength} {machine : TM tapes} {test : Finset (Fin outputLength → Bool)} {density : ℚ} (hseedLength : seedLength < threshold) (hproduces : ∀ (seed : Fin seedLength → Bool), machine.ProducesInTime (List.ofFn seed) (List.ofFn (generator seed)) time) (hrandom : IsTimeBoundedRandomTest test machine time threshold) (hdense : IsDenseTest test density) : density ≤ generator.distinguishingAdvantage test

Hirahara's finite statistical-test step: a dense random-string test has advantage at least its density against a generator whose short seeds directly describe its outputs within the chosen clock.

theorem Complexity.BitGenerator.incompressibilityBound_le_distinguishingAdvantage {seedLength outputLength tapes time threshold : ℕ} {generator : BitGenerator seedLength outputLength} {machine : TM tapes} (hlow : generator.HasLowTimeBoundedComplexity machine time threshold) : 1 - ↑(2 ^ threshold - 1) / 2 ^ outputLength ≤ generator.distinguishingAdvantage (machine.timeBoundedRandomStrings outputLength time threshold)

The canonical random-string test distinguishes every generator whose outputs are below the threshold by the full strict-incompressibility lower bound. No computability property of the test is asserted here.

theorem Complexity.BitGenerator.incompressibilityBound_le_distinguishingAdvantage_of_seedDescriptions {seedLength outputLength tapes time threshold : ℕ} {generator : BitGenerator seedLength outputLength} {machine : TM tapes} (hseedLength : seedLength < threshold) (hproduces : ∀ (seed : Fin seedLength → Bool), machine.ProducesInTime (List.ofFn seed) (List.ofFn (generator seed)) time) : 1 - ↑(2 ^ threshold - 1) / 2 ^ outputLength ≤ generator.distinguishingAdvantage (machine.timeBoundedRandomStrings outputLength time threshold)

A directly seed-described generator is distinguished by the canonical random-string test with the explicit strict-incompressibility advantage.