Combining the three pseudoentropy extractors

One collection of sampler seeds supplies the observations, hidden labels, and remaining seed randomness. Each extractor keeps its independent public matrix seed. The security argument replaces the remaining-seed component, then the labels, then the observations by uniform bits. The middle transition uses a strict PPT test; the other two are statistical transitions. The indexed theorem allows any valid choice from a polynomial-size family. The choice belongs only to the security argument; the efficient test handles all indices uniformly.

Main definitions

• ThreeSource.extract: sample once and hash observations, labels, and retained sampler seeds.
• ThreeSource.seedLength, ThreeSource.outputLength: exact input and output budgets.
• ThreeSource.Efficient: the shared uniformity contract for the extraction schedules.

Main results

• ThreeSource.isPPTOn_extract: the composed program has a strict PPT certificate.
• SamplablePair.HasGap.extract_indexed_three: uniform security for any valid candidate choice.
• SamplablePair.HasGap.extract_three: the single-candidate computational interface.

References

• Thomas Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, TCC 2006, Section 5, Lemma 5 and the final proof of Theorem 1. [Hol06]. We use the shared Boolean-matrix family and make the three component transitions explicit.

Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8. Statistical transitions quantify over all randomized Boolean tests of the complete output; only the middle transition restricts tests to strict PPT.

noncomputable def Cslib.Crypto.Pseudoentropy.ThreeSource.finish (bound observationBits : ℕ) (middle : List (List Bool) × List Bool × List Bool) : ProbComp (List Bool)

Finish the first two components by hashing observations and retaining the label hash.

theorem Cslib.Crypto.Pseudoentropy.ThreeSource.isPPTOn_finish {α : Type} {input : α ↪ List Bool} {bound observationBits : α → ℕ} {middle : α → List (List Bool) × List Bool × List Bool} (hbound : Turing.MultiTapeTM.ComputableTidilyInPolyTime bound input Turing.MultiTapeTM.encUnary) (hobservation : Turing.MultiTapeTM.ComputableTidilyInPolyTime observationBits input Turing.MultiTapeTM.encUnary) (hmiddle : Turing.MultiTapeTM.ComputableTidilyInPolyTime middle input (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) : Probability.IsPPTOn input Turing.MultiTapeTM.encBits fun (a : α) => finish (bound a) (observationBits a) (middle a)

The last observation hash composes with a certified intermediate result.

noncomputable def Cslib.Crypto.Pseudoentropy.ThreeSource.extract (count seedBits bound observationBits labelBits remainingBits : ℕ) (source : ProbComp ((List Bool × Bool) × List Bool)) : ProbComp (List Bool)

Sample once and hash all three components, retaining every independent matrix seed.

theorem Cslib.Crypto.Pseudoentropy.ThreeSource.isPPTOn_extract {α : Type} {input : α ↪ List Bool} {count seedBits bound observationBits labelBits remainingBits : α → ℕ} {source : α → ProbComp ((List Bool × Bool) × List Bool)} (hsource : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool) Turing.MultiTapeTM.encBits) source) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hseed : Turing.MultiTapeTM.ComputableTidilyInPolyTime seedBits input Turing.MultiTapeTM.encUnary) (hbound : Turing.MultiTapeTM.ComputableTidilyInPolyTime bound input Turing.MultiTapeTM.encUnary) (hobservation : Turing.MultiTapeTM.ComputableTidilyInPolyTime observationBits input Turing.MultiTapeTM.encUnary) (hlabel : Turing.MultiTapeTM.ComputableTidilyInPolyTime labelBits input Turing.MultiTapeTM.encUnary) (hremaining : Turing.MultiTapeTM.ComputableTidilyInPolyTime remainingBits input Turing.MultiTapeTM.encUnary) : Probability.IsPPTOn input Turing.MultiTapeTM.encBits fun (a : α) => extract (count a) (seedBits a) (bound a) (observationBits a) (labelBits a) (remainingBits a) (source a)

The complete three-component program is PPT from ordinary sampler and size certificates.

noncomputable def Cslib.Crypto.Pseudoentropy.ThreeSource.withoutSeeds (count seedBits bound observationBits labelBits remainingBits : ℕ) (source : ProbComp (List Bool × Bool)) : ProbComp (List Bool)

The first hybrid replaces the remaining-seed component by independent uniform bits.

noncomputable def Cslib.Crypto.Pseudoentropy.ThreeSource.withoutLabels (count seedBits bound observationBits labelBits remainingBits : ℕ) (source : ProbComp (List Bool)) : ProbComp (List Bool)

The second hybrid also replaces the label component by independent uniform bits.

def Cslib.Crypto.Pseudoentropy.ThreeSource.outputLength (count seedBits bound observationBits labelBits remainingBits : ℕ) : ℕ

The output length counts every digest and every retained matrix seed.

theorem Cslib.Crypto.Pseudoentropy.ThreeSource.length_extract (count seedBits bound observationBits labelBits remainingBits : ℕ) (source : ProbComp ((List Bool × Bool) × List Bool)) (hbound : ∀ sample ∈ source.eval.support, sample.1.1.length ≤ bound) {output : List Bool} (houtput : output ∈ (extract count seedBits bound observationBits labelBits remainingBits source).eval.support) : output.length = outputLength count seedBits bound observationBits labelBits remainingBits

Every supported output has the advertised length when sampled observations fit the bound. The statement also covers zero-sized components and malformed retained seeds.

def Cslib.Crypto.Pseudoentropy.ThreeSource.seedLength (count seedBits bound observationBits labelBits remainingBits : ℕ) : ℕ

Original sampler coins followed by the three matrix seeds in execution order.

theorem Cslib.Crypto.Pseudoentropy.ThreeSource.isPolyTime_seedLength {α : Type} {input : α ↪ List Bool} {count seedBits bound observationBits labelBits remainingBits : α → ℕ} (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hseed : Turing.MultiTapeTM.ComputableTidilyInPolyTime seedBits input Turing.MultiTapeTM.encUnary) (hbound : Turing.MultiTapeTM.ComputableTidilyInPolyTime bound input Turing.MultiTapeTM.encUnary) (hobservation : Turing.MultiTapeTM.ComputableTidilyInPolyTime observationBits input Turing.MultiTapeTM.encUnary) (hlabel : Turing.MultiTapeTM.ComputableTidilyInPolyTime labelBits input Turing.MultiTapeTM.encUnary) (hremaining : Turing.MultiTapeTM.ComputableTidilyInPolyTime remainingBits input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => seedLength (count a) (seedBits a) (bound a) (observationBits a) (labelBits a) (remainingBits a)) input Turing.MultiTapeTM.encUnary

The exact seed ledger can be computed in unary from efficient dimensions.

theorem Cslib.Crypto.Pseudoentropy.ThreeSource.isPolyTime_outputLength {α : Type} {input : α ↪ List Bool} {count seedBits bound observationBits labelBits remainingBits : α → ℕ} (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hseed : Turing.MultiTapeTM.ComputableTidilyInPolyTime seedBits input Turing.MultiTapeTM.encUnary) (hbound : Turing.MultiTapeTM.ComputableTidilyInPolyTime bound input Turing.MultiTapeTM.encUnary) (hobservation : Turing.MultiTapeTM.ComputableTidilyInPolyTime observationBits input Turing.MultiTapeTM.encUnary) (hlabel : Turing.MultiTapeTM.ComputableTidilyInPolyTime labelBits input Turing.MultiTapeTM.encUnary) (hremaining : Turing.MultiTapeTM.ComputableTidilyInPolyTime remainingBits input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => outputLength (count a) (seedBits a) (bound a) (observationBits a) (labelBits a) (remainingBits a)) input Turing.MultiTapeTM.encUnary

The exact output ledger can be computed in unary from efficient dimensions.

theorem Cslib.Crypto.Pseudoentropy.ThreeSource.seedLength_lt_outputLength_iff (count seedBits bound observationBits labelBits remainingBits : ℕ) : seedLength count seedBits bound observationBits labelBits remainingBits < outputLength count seedBits bound observationBits labelBits remainingBits ↔ count * seedBits < observationBits + labelBits + remainingBits

Retained matrix seeds cancel in the expansion budget: only the digest bits must exceed the original sampler coins. ThreeSource.Seeded realizes this exact input length.

theorem Cslib.Crypto.Pseudoentropy.ThreeSource.eval_ideal_remaining (count seedBits bound observationBits labelBits remainingBits : ℕ) (source : ProbComp (List Bool × Bool)) : (do let third ← extractMatrixLabelsIdeal source count (count * seedBits) remainingBits let middle ← extractWordLabels count labelBits third.1 let front ← finish bound observationBits middle pure (front ++ (third.2.1 ++ third.2.2))).eval = (withoutSeeds count seedBits bound observationBits labelBits remainingBits source).eval

Moving the independent ideal seed component to the end gives the first hybrid exactly.

theorem Cslib.Crypto.Pseudoentropy.ThreeSource.eval_ideal_labels (count bound observationBits labelBits : ℕ) (source : ProbComp (List Bool)) : (extractWordLabelsIdeal source count labelBits >>= finish bound observationBits).eval = (do let samples ← OracleComp.replicate count source let first ← extractWordObservations bound observationBits samples let middle ← BitString.sampleList (labelBits * count + labelBits) pure (first ++ middle)).eval

Once the label hash is ideal, its seed and digest can follow the observation extraction.

theorem Cslib.Crypto.Pseudoentropy.ThreeSource.replace_remaining {pair : SamplablePair} (saved : pair.SeedRealization) (bound inverseSlack observationBits labelBits remainingBits : ℕ → ℕ) (hbudget : ∀ᶠ (n : ℕ) in Filter.atTop, remainingBits n = 0 ∨ ↑(remainingBits n) + 2 * ↑(ExtractionSchedule.slack n (saved.length n) (inverseSlack n)) ≤ ↑(ExtractionSchedule.count n (saved.length n) (inverseSlack n)) * (↑(saved.length n) - Probability.PMF.entropy (PMF.map Prod.fst (pair.joint n)) - Probability.PMF.conditionalEntropy (pair.joint n))) : have count := fun (n : ℕ) => ExtractionSchedule.count n (saved.length n) (inverseSlack n); Game.Indistinguishable (fun (test : ℕ → List Bool → Game) (n : ℕ) => (extract (count n) (saved.length n) (bound n) (observationBits n) (labelBits n) (remainingBits n) (saved.sampleWithSeed n)).eval.bind (test n)) (fun (test : ℕ → List Bool → Game) (n : ℕ) => (withoutSeeds (count n) (saved.length n) (bound n) (observationBits n) (labelBits n) (remainingBits n) (pair.sample n)).eval.bind (test n)) fun (x : ℕ → List Bool → Game) => True

Statistical extraction replaces the third component while retaining the data needed by the first two components. No efficiency assumption is needed for this postprocessing.

theorem Cslib.Crypto.Pseudoentropy.ThreeSource.replace_observations {pair : SamplablePair} (saved : pair.SeedRealization) (bound inverseSlack observationBits labelBits remainingBits : ℕ → ℕ) (hbound : ∀ (n : ℕ), ∀ observation ∈ (PMF.map Prod.fst (pair.joint n)).support, ((pair.encode n) observation).length ≤ bound n) (hbudget : ∀ᶠ (n : ℕ) in Filter.atTop, observationBits n = 0 ∨ ↑(observationBits n) + 2 * ↑(ExtractionSchedule.slack n (saved.length n) (inverseSlack n)) ≤ ↑(ExtractionSchedule.count n (saved.length n) (inverseSlack n)) * Probability.PMF.entropy (PMF.map Prod.fst (pair.joint n))) : have count := fun (n : ℕ) => ExtractionSchedule.count n (saved.length n) (inverseSlack n); Game.Indistinguishable (fun (test : ℕ → List Bool → Game) (n : ℕ) => (withoutLabels (count n) (saved.length n) (bound n) (observationBits n) (labelBits n) (remainingBits n) (Prod.fst <$> pair.sample n)).eval.bind (test n)) (fun (test : ℕ → List Bool → Game) (n : ℕ) => (BitString.uniformList (outputLength (count n) (saved.length n) (bound n) (observationBits n) (labelBits n) (remainingBits n))).bind (test n)) fun (x : ℕ → List Bool → Game) => True

After the other two components are uniform, observation extraction completes the statistical comparison with a single uniform word of the advertised total length.

structure Cslib.Crypto.Pseudoentropy.ThreeSource.Efficient (candidates bound inverseSlack densityBound : ℕ → ℕ) (observationBits labelBits remainingBits numerator : ℕ → ℕ → ℕ) : Prop

Plain polynomial-time computation of the schedules used by three-source extraction. This contract covers every candidate; it imposes no computability requirement on the index chosen in the security proof. Entropy and observation-size assumptions remain separate.

• candidates_isPolyTime : Turing.MultiTapeTM.ComputableInPolyTime candidates Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary
• bound_isPolyTime : Turing.MultiTapeTM.ComputableInPolyTime bound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary
• observation_isPolyTime : Turing.MultiTapeTM.ComputableInPolyTime (fun (input : ℕ × ℕ) => observationBits input.1 input.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encUnary
• label_isPolyTime : Turing.MultiTapeTM.ComputableInPolyTime (fun (input : ℕ × ℕ) => labelBits input.1 input.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encUnary
• remaining_isPolyTime : Turing.MultiTapeTM.ComputableInPolyTime (fun (input : ℕ × ℕ) => remainingBits input.1 input.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encUnary
• slack_isPolyTime : Turing.MultiTapeTM.ComputableInPolyTime inverseSlack Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary
• numerator_isPolyTime : Turing.MultiTapeTM.ComputableInPolyTime (fun (input : ℕ × ℕ) => numerator input.1 input.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encUnary
• density_isPolyTime : Turing.MultiTapeTM.ComputableInPolyTime densityBound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary

theorem Cslib.Crypto.Pseudoentropy.ThreeSource.efficient_iff_tidy {candidates bound inverseSlack densityBound : ℕ → ℕ} {observationBits labelBits remainingBits numerator : ℕ → ℕ → ℕ} : Efficient candidates bound inverseSlack densityBound observationBits labelBits remainingBits numerator ↔ Turing.MultiTapeTM.ComputableTidilyInPolyTime candidates Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary ∧ Turing.MultiTapeTM.ComputableTidilyInPolyTime bound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary ∧ Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (input : ℕ × ℕ) => observationBits input.1 input.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encUnary ∧ Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (input : ℕ × ℕ) => labelBits input.1 input.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encUnary ∧ Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (input : ℕ × ℕ) => remainingBits input.1 input.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encUnary ∧ Turing.MultiTapeTM.ComputableTidilyInPolyTime inverseSlack Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary ∧ Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (input : ℕ × ℕ) => numerator input.1 input.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encUnary ∧ Turing.MultiTapeTM.ComputableTidilyInPolyTime densityBound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary

Recover the tidy presentation for proofs without changing the security contract.

theorem Cslib.Crypto.Pseudoentropy.ThreeSource.replace_indexed_labels {pair : SamplablePair} {gap : ℕ → ℝ} (hpair : pair.HasGap gap) (saved : pair.SeedRealization) (choose : ℕ → ℕ) {candidates bound inverseSlack densityBound : ℕ → ℕ} {observationBits labelBits remainingBits numerator : ℕ → ℕ → ℕ} (efficient : Efficient candidates bound inverseSlack densityBound observationBits labelBits remainingBits numerator) (hchoose : ∀ᶠ (n : ℕ) in Filter.atTop, choose n < candidates n) (hvalid : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < numerator n (choose n) ∧ numerator n (choose n) ≤ Probability.dyadicSize (densityBound n) ∧ ↑(numerator n (choose n)) / ↑(Probability.dyadicSize (densityBound n)) ≤ Probability.PMF.conditionalEntropy (pair.joint n) + gap n) (hbudget : ∀ᶠ (n : ℕ) in Filter.atTop, ↑(labelBits n (choose n)) + 2 * ↑(ExtractionSchedule.slack n (saved.length n) (inverseSlack n)) ≤ ↑(ExtractionSchedule.count n (saved.length n) (inverseSlack n)) * (↑(numerator n (choose n)) / ↑(Probability.dyadicSize (densityBound n)))) (adversary : ℕ → ℕ → List Bool → ProbComp Bool) (hadversary : Probability.IsPPTOn (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool fun (input : (ℕ × ℕ) × List Bool) => adversary input.1.1 input.1.2 input.2) : have count := fun (n : ℕ) => ExtractionSchedule.count n (saved.length n) (inverseSlack n); Negligible fun (n : ℕ) => Game.advantage (withoutSeeds (count n) (saved.length n) (bound n) (observationBits n (choose n)) (labelBits n (choose n)) (remainingBits n (choose n)) (pair.sample n) >>= adversary n (choose n)).eval (withoutLabels (count n) (saved.length n) (bound n) (observationBits n (choose n)) (labelBits n (choose n)) (remainingBits n (choose n)) (Prod.fst <$> pair.sample n) >>= adversary n (choose n)).eval

Indexed label extraction remains secure when the test computes the observation hash and supplies the independent third component. Only the proof uses the chosen valid index.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.HasGap.extract_indexed_three {pair : SamplablePair} {gap : ℕ → ℝ} (hpair : pair.HasGap gap) (saved : pair.SeedRealization) (choose : ℕ → ℕ) {candidates bound inverseSlack densityBound : ℕ → ℕ} {observationBits labelBits remainingBits numerator : ℕ → ℕ → ℕ} (efficient : ThreeSource.Efficient candidates bound inverseSlack densityBound observationBits labelBits remainingBits numerator) (hfits : ∀ (n : ℕ), ∀ observation ∈ (PMF.map Prod.fst (pair.joint n)).support, ((pair.encode n) observation).length ≤ bound n) (hchoose : ∀ᶠ (n : ℕ) in Filter.atTop, choose n < candidates n) (hvalid : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < numerator n (choose n) ∧ numerator n (choose n) ≤ Probability.dyadicSize (densityBound n) ∧ ↑(numerator n (choose n)) / ↑(Probability.dyadicSize (densityBound n)) ≤ Probability.PMF.conditionalEntropy (pair.joint n) + gap n) (hfirst : ∀ᶠ (n : ℕ) in Filter.atTop, observationBits n (choose n) = 0 ∨ ↑(observationBits n (choose n)) + 2 * ↑(ExtractionSchedule.slack n (saved.length n) (inverseSlack n)) ≤ ↑(ExtractionSchedule.count n (saved.length n) (inverseSlack n)) * Probability.PMF.entropy (PMF.map Prod.fst (pair.joint n))) (hmiddle : ∀ᶠ (n : ℕ) in Filter.atTop, ↑(labelBits n (choose n)) + 2 * ↑(ExtractionSchedule.slack n (saved.length n) (inverseSlack n)) ≤ ↑(ExtractionSchedule.count n (saved.length n) (inverseSlack n)) * (↑(numerator n (choose n)) / ↑(Probability.dyadicSize (densityBound n)))) (hlast : ∀ᶠ (n : ℕ) in Filter.atTop, remainingBits n (choose n) = 0 ∨ ↑(remainingBits n (choose n)) + 2 * ↑(ExtractionSchedule.slack n (saved.length n) (inverseSlack n)) ≤ ↑(ExtractionSchedule.count n (saved.length n) (inverseSlack n)) * (↑(saved.length n) - Probability.PMF.entropy (PMF.map Prod.fst (pair.joint n)) - Probability.PMF.conditionalEntropy (pair.joint n))) (test : ℕ → ℕ → List Bool → ProbComp Bool) (htest : Probability.IsPPTOn (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool fun (input : (ℕ × ℕ) × List Bool) => test input.1.1 input.1.2 input.2) : have count := fun (n : ℕ) => ExtractionSchedule.count n (saved.length n) (inverseSlack n); Negligible fun (n : ℕ) => Game.advantage (ThreeSource.extract (count n) (saved.length n) (bound n) (observationBits n (choose n)) (labelBits n (choose n)) (remainingBits n (choose n)) (saved.sampleWithSeed n) >>= test n (choose n)).eval (BitString.sampleList (ThreeSource.outputLength (count n) (saved.length n) (bound n) (observationBits n (choose n)) (labelBits n (choose n)) (remainingBits n (choose n))) >>= test n (choose n)).eval

A valid candidate in an efficient polynomial-size family passes the complete three-source game argument. The candidate may vary arbitrarily with the parameter; one efficient indexed test handles the entire family. All three entropy budgets are needed only at the chosen candidate.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.HasGap.extract_three {pair : SamplablePair} {gap : ℕ → ℝ} (hpair : pair.HasGap gap) (saved : pair.SeedRealization) {bound inverseSlack observationBits labelBits remainingBits numerator densityBound : ℕ → ℕ} (efficient : ThreeSource.Efficient (fun (x : ℕ) => 1) bound inverseSlack densityBound (fun (n x : ℕ) => observationBits n) (fun (n x : ℕ) => labelBits n) (fun (n x : ℕ) => remainingBits n) fun (n x : ℕ) => numerator n) (hfits : ∀ (n : ℕ), ∀ observation ∈ (PMF.map Prod.fst (pair.joint n)).support, ((pair.encode n) observation).length ≤ bound n) (hvalid : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < numerator n ∧ numerator n ≤ Probability.dyadicSize (densityBound n) ∧ ↑(numerator n) / ↑(Probability.dyadicSize (densityBound n)) ≤ Probability.PMF.conditionalEntropy (pair.joint n) + gap n) (hfirst : ∀ᶠ (n : ℕ) in Filter.atTop, observationBits n = 0 ∨ ↑(observationBits n) + 2 * ↑(ExtractionSchedule.slack n (saved.length n) (inverseSlack n)) ≤ ↑(ExtractionSchedule.count n (saved.length n) (inverseSlack n)) * Probability.PMF.entropy (PMF.map Prod.fst (pair.joint n))) (hmiddle : ∀ᶠ (n : ℕ) in Filter.atTop, ↑(labelBits n) + 2 * ↑(ExtractionSchedule.slack n (saved.length n) (inverseSlack n)) ≤ ↑(ExtractionSchedule.count n (saved.length n) (inverseSlack n)) * (↑(numerator n) / ↑(Probability.dyadicSize (densityBound n)))) (hlast : ∀ᶠ (n : ℕ) in Filter.atTop, remainingBits n = 0 ∨ ↑(remainingBits n) + 2 * ↑(ExtractionSchedule.slack n (saved.length n) (inverseSlack n)) ≤ ↑(ExtractionSchedule.count n (saved.length n) (inverseSlack n)) * (↑(saved.length n) - Probability.PMF.entropy (PMF.map Prod.fst (pair.joint n)) - Probability.PMF.conditionalEntropy (pair.joint n))) : have count := fun (n : ℕ) => ExtractionSchedule.count n (saved.length n) (inverseSlack n); ComputationallyIndistinguishable (fun (n : ℕ) => (ThreeSource.extract (count n) (saved.length n) (bound n) (observationBits n) (labelBits n) (remainingBits n) (saved.sampleWithSeed n)).eval) fun (n : ℕ) => BitString.uniformList (ThreeSource.outputLength (count n) (saved.length n) (bound n) (observationBits n) (labelBits n) (remainingBits n))

The three-source construction is computationally uniform under its three entropy budgets. The schedules must be computed by uniform polynomial-time algorithms. ThreeSource.Seeded implements this ensemble deterministically with an exact seed budget, and EntropyGrid supplies budgets for which some candidate is valid.