Finite statistical tests for binary generators -- definitions

This layer fixes exact finite conventions for the first step of the Nisan--Wigderson reconstruction used in metacomplexity. A generator maps a uniform fixed-length Boolean seed to a fixed-length Boolean output. A test's acceptance probability is measured both under uniform output bits and under the generator, and its distinguishing advantage is the absolute difference.

The complexity predicates remain relative to an arbitrary deterministic machine and primitive clock. Universality and efficient computability of a particular generator are separate hypotheses.

@[reducible, inline]

abbrev Complexity.BitGenerator (seedLength outputLength : ℕ) : Type

A deterministic binary generator from seedLength bits to outputLength bits. No expansion or computability condition is built into the type.

Equations

• Complexity.BitGenerator seedLength outputLength = ((Fin seedLength → Bool) → Fin outputLength → Bool)

def Complexity.BitGenerator.acceptedSeeds {seedLength outputLength : ℕ} (generator : BitGenerator seedLength outputLength) (test : Finset (Fin outputLength → Bool)) : Finset (Fin seedLength → Bool)

The seeds whose generated outputs are accepted by a finite test.

Equations

• generator.acceptedSeeds test = {seed : Fin seedLength → Bool | generator seed ∈ test}

def Complexity.BitGenerator.generatedAcceptanceProbability {seedLength outputLength : ℕ} (generator : BitGenerator seedLength outputLength) (test : Finset (Fin outputLength → Bool)) : ℚ

Acceptance probability of a test under a uniform generator seed.

Equations

• generator.generatedAcceptanceProbability test = Complexity.eventProb (generator.acceptedSeeds test)

def Complexity.BitGenerator.uniformAcceptanceProbability {outputLength : ℕ} (test : Finset (Fin outputLength → Bool)) : ℚ

Acceptance probability of a test under uniform output bits.

Equations

• Complexity.BitGenerator.uniformAcceptanceProbability test = Complexity.eventProb test

def Complexity.BitGenerator.distinguishingAdvantage {seedLength outputLength : ℕ} (generator : BitGenerator seedLength outputLength) (test : Finset (Fin outputLength → Bool)) : ℚ

Absolute distinguishing advantage of a test between uniform output bits and the output of a generator on a uniform seed.

Equations

• generator.distinguishingAdvantage test = |Complexity.BitGenerator.uniformAcceptanceProbability test - generator.generatedAcceptanceProbability test|

def Complexity.BitGenerator.IsDenseTest {outputLength : ℕ} (test : Finset (Fin outputLength → Bool)) (density : ℚ) : Prop

A test is density-dense when it accepts at least that much uniform output mass.

Equations

• Complexity.BitGenerator.IsDenseTest test density = (density ≤ Complexity.BitGenerator.uniformAcceptanceProbability test)

def Complexity.BitGenerator.HasLowTimeBoundedComplexity {seedLength outputLength tapes : ℕ} (generator : BitGenerator seedLength outputLength) (machine : TM tapes) (time threshold : ℕ) : Prop

Every generated output has time-bounded complexity strictly below the specified threshold.

Equations

• generator.HasLowTimeBoundedComplexity machine time threshold = ∀ (seed : Fin seedLength → Bool), machine.timeBoundedKolmogorovComplexity (List.ofFn (generator seed)) time < ↑threshold

def Complexity.BitGenerator.IsTimeBoundedRandomTest {outputLength tapes : ℕ} (test : Finset (Fin outputLength → Bool)) (machine : TM tapes) (time threshold : ℕ) : Prop

Every output accepted by the test is random at the specified threshold and clock. Equivalently, the test is a subset of the corresponding finite set of time-bounded random strings.

Equations

• Complexity.BitGenerator.IsTimeBoundedRandomTest test machine time threshold = ∀ output ∈ test, ↑threshold ≤ machine.timeBoundedKolmogorovComplexity (List.ofFn output) time