Splitting one hybrid coordinate into a next-bit experiment -- definitions

The background retains a generator seed and a uniform output tail whose distinguished candidate coordinate is normalized to false. Replacing that coordinate by an explicit Boolean candidate recovers the full hybrid random space bijectively, without choosing an indexing of the remaining coordinates.

@[reducible, inline]

abbrev Complexity.BitGenerator.CandidateBackground (seedLength outputLength : ℕ) (step : Fin outputLength) : Type

All randomness in a hybrid experiment except the distinguished candidate bit. The output tail is normalized to false at that coordinate.

Equations

• Complexity.BitGenerator.CandidateBackground seedLength outputLength step = ((Fin seedLength → Bool) × { tail : Fin outputLength → Bool // tail step = false })

instance Complexity.BitGenerator.candidateBackgroundNonempty (seedLength outputLength : ℕ) (step : Fin outputLength) : Nonempty (CandidateBackground seedLength outputLength step)

The all-false seed and tail witness that every candidate-background space is nonempty.

def Complexity.BitGenerator.assembleCandidate {seedLength outputLength : ℕ} {step : Fin outputLength} (background : CandidateBackground seedLength outputLength step) (candidate : Bool) : Fin (seedLength + outputLength) → Bool

Reinsert a candidate bit and concatenate the generator seed with the completed random output tail.

Equations

• Complexity.BitGenerator.assembleCandidate background candidate = Complexity.blockAppend seedLength outputLength background.1 (Function.update (↑background.2) step candidate)

def Complexity.BitGenerator.targetBit {seedLength outputLength : ℕ} (generator : BitGenerator seedLength outputLength) (step : Fin outputLength) (background : CandidateBackground seedLength outputLength step) : Bool

The generator bit to be predicted from the background state.

Equations

• generator.targetBit step background = generator background.1 step

def Complexity.BitGenerator.testAtCandidate {seedLength outputLength : ℕ} (generator : BitGenerator seedLength outputLength) (test : Finset (Fin outputLength → Bool)) (step : Fin outputLength) (background : CandidateBackground seedLength outputLength step) (candidate : Bool) : Bool

Test result when the distinguished bit in the step-th hybrid is filled with candidate.

Equations

• generator.testAtCandidate test step background candidate = decide (generator.hybridOutput (↑step) (Complexity.BitGenerator.assembleCandidate background candidate) ∈ test)