Pseudorandom generators from pseudoentropy pairs

Realize the pair with a deterministic sampler and saved coins, enumerate the entropy grid, pad and amplify every candidate, then XOR their outputs. Finally extend the resulting family to every seed length. The density schedule must resolve the pair's gap; no entropy estimate or chosen successful candidate is supplied to the generator.

Main results

• Cslib.Crypto.Pseudoentropy.SamplablePair.HasGap.exists_pseudorandomGenerator: a samplable pseudoentropy pair with an efficiently resolved gap gives a uniform one-bit expanding PRG.

References

This formalizes T. Holenstein, Pseudorandom Generators from One-Way Functions, Section 5 and the final proof of Theorem 1. The matrix extractor used here gives polynomial seed length without claiming the paper's optimized seed-length exponent.

Adapted from Crypto/Computational/Pseudoentropy/Generator.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using typed machine certificates and the nonnegative game API.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.HasGap.exists_pseudorandomGenerator {pair : SamplablePair} {gap : ℕ → ℝ} (hpair : pair.HasGap gap) {densityBound : ℕ → ℕ} (hdensity : Turing.MultiTapeTM.ComputableTidilyInPolyTime densityBound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hgap : ∀ᶠ (n : ℕ) in Filter.atTop, 4 / ↑(Probability.dyadicSize (densityBound n)) ≤ gap n) : ∃ (generator : List Bool → List Bool), PseudorandomGenerator generator fun (n : ℕ) => n + 1

A samplable pseudoentropy pair with an efficiently resolved gap gives a uniform PRG expanding every seed length by one bit.