Leftover Hash Lemma Extraction Bound for Unpredictable Random-Oracle Sources, Public Seed

·

Statement: human-written, AI-formalized, AI-matched against the informal statement. Proof: AI draft, not yet independently reviewed, not yet formalized.

Leftover Hash LemmaRandom Oracle ModelRandomness Extraction

View PDF · LaTeX source · Formal statement – one conjecture, the public-seed one stated below, followed by a remark deriving what a direct application of the leftover hash lemma gives instead, and why that lands at the same square root in \(K\) but pays a set size under it where this conjecture pays a number of bits. Its secret-seed companion is a different claim, not a restatement; it had a statement note and a page of its own until both were removed on 28 August 2026, and it now survives only in the opening section of the proof note, which reproduces it verbatim because the counterexample there is about an expression derived from it. In text written before that day, “Conjecture 2” means the public-seed conjecture and “Conjecture 1” the secret-seed one.

Setting

Fix nonempty finite sets \(\mathcal{K}\) (seeds), \(\mathcal{D}\) (inputs), \(\mathcal{R}\) (outputs), and write \(K := |\mathcal{K}|\), \(D := |\mathcal{D}|\), \(R := |\mathcal{R}|\). Let \(\mathsf{Fun}(\mathcal{K}\times\mathcal{D},\mathcal{R})\) be the set of all functions \(\mathcal{K}\times\mathcal{D}\to\mathcal{R}\), let \(\mathrm{SD}(\cdot,\cdot)\) denote statistical distance, and \(U_\mathcal{R}\) the uniform distribution on \(\mathcal{R}\). The source \(S\), the predictor \(P\), and the distinguisher \(\mathsf{D}\) below are all computationally unbounded and receive the entire function table of \(H\) as an explicit input.

Game \(\mathsf{Pred}^{S}_{P}\) Game \(\mathsf{Ext\text{-}pub}^{S}_{\mathsf{D}}\) (public seed)
\(H \stackrel{\$}{\leftarrow} \mathsf{Fun}(\mathcal{K}\times\mathcal{D},\mathcal{R})\)
\((x,z) \stackrel{\$}{\leftarrow} S(H)\)
\(x' \stackrel{\$}{\leftarrow} P(H,z)\)
return \((x = x')\)		 \(H \stackrel{\$}{\leftarrow} \mathsf{Fun}(\mathcal{K}\times\mathcal{D},\mathcal{R})\)
\((x,z) \stackrel{\$}{\leftarrow} S(H)\);   \(\mathit{sd} \stackrel{\$}{\leftarrow} \mathcal{K}\)
\(y_0 \leftarrow H(\mathit{sd},x)\);   \(y_1 \stackrel{\$}{\leftarrow} \mathcal{R}\)
\(b \stackrel{\$}{\leftarrow} \{0,1\}\)
\(b' \stackrel{\$}{\leftarrow} \mathsf{D}(H, \mathit{sd}, y_b, z)\)
return \((b = b')\)

Prediction game (left) and the public-seed extraction game (right); the distinguisher receives the seed \(\mathit{sd}\) explicitly, unlike in the secret-seed variant defined alongside it in the same source document.

NoteDefinition (Advantages and Unpredictability)

Set \(\mathbf{Adv}^{\mathrm{pred}}_{\mathcal{K},\mathcal{D},\mathcal{R},S}(P) := \Pr[\mathsf{Pred}^{S}_{P} \Rightarrow 1]\) and \[ \mathbf{Adv}^{\mathrm{ext\text{-}pub}}_{\mathcal{K},\mathcal{D},\mathcal{R}}(S,\mathsf{D}) := 2\Pr[\mathsf{Ext\text{-}pub}^{S}_{\mathsf{D}} \Rightarrow 1] - 1 . \] A source \(S\) is \(\epsilon\)-unpredictable if \(\mathbf{Adv}^{\mathrm{pred}}_{\mathcal{K},\mathcal{D},\mathcal{R},S}(P) \le \epsilon\) for every unbounded predictor \(P\).

The Conjecture

ImportantConjecture (Public seed)

There is a universal constant \(c > 0\), independent of \(\mathcal{K}\), \(\mathcal{D}\), \(\mathcal{R}\) and \(\epsilon\), such that for all nonempty finite \(\mathcal{K}, \mathcal{D}, \mathcal{R}\), all \(\epsilon \in (0,1]\), every \(\epsilon\)-unpredictable source \(S\), and every unbounded distinguisher \(\mathsf{D}\), \[ \mathbf{Adv}^{\mathrm{ext\text{-}pub}}_{\mathcal{K},\mathcal{D},\mathcal{R}}(S,\mathsf{D}) \;\le\; \delta_{\mathrm{pub}}(\epsilon, K, D, R) \;:=\; c \cdot \Bigl( \sqrt{\epsilon R} + \sqrt{\frac{\log_2 D}{K}} \,\Bigr) . \]

Sources

See Relation to the extractor literature on the problem hub for how these bear on the conjecture, and the Discussion tab for the short version.

View PDF · LaTeX source · Formal proof

AI: Claude Opus 5 (Anthropic) · Prompted by: Pooya Farshim · Reviewed by: nobody yet · 14 August 2026.

Scope. This note resolves the conjecture above, with \(c = 2\) (in fact \(c=\tfrac85\) suffices, and the smallest constant obtainable by this route is \(\approx 1.5615\)). Along the way, it also shows that the most natural guess for a public-seed bound – literally transposing the secret-seed expression (reproduced verbatim in the proof note’s opening section) from \(\mathbf{Adv}^{\mathrm{ext}}\) to \(\mathbf{Adv}^{\mathrm{ext\text{-}pub}}\) – is false, which is what motivates the corrected bound below and is a useful negative result in its own right.

The naive transposition is false in this model

NoteProposition (Counterexample to the naive transposition)

For every \(c > 0\) there are nonempty finite \(\mathcal{K}, \mathcal{D}, \mathcal{R}\), a value \(\epsilon \in (0,1]\), an \(\epsilon\)-unpredictable source \(S\), and a distinguisher \(\mathsf{D}\) with \[ \mathbf{Adv}^{\mathrm{ext\text{-}pub}}_{\mathcal{K},\mathcal{D},\mathcal{R}}(S,\mathsf{D}) \;\ge\; \tfrac14 \;>\; c\,\sqrt{\frac{\epsilon R + \log_2 D}{K}} \;. \] The witness has \(z = \bot\) and \(X\) uniform on all of \(\mathcal{D}\) – the largest entropy a source over \(\mathcal{D}\) can have – with \(R = D\); \(\mathsf{D}\) simply checks whether its challenge lies in the image of the row \(H(\mathit{sd},\cdot)\), which it can compute in full since it holds both \(H\) and \(\mathit{sd}\). Since the right-hand side can be pushed below \(\tfrac14\) by taking \(K\) large with everything else fixed, no universal constant \(c\) can make the transposed bound hold uniformly in \(K\).

Once the seed is public, the map \(x \mapsto H(\mathit{sd},x)\) is known to \(\mathsf{D}\) in full, so the only randomness left is that of \(X\) itself – the seed can no longer contribute entropy, and any correct bound must contain a term in \(\epsilon R\) that does not decay in \(K\).

The corrected bound

ImportantTheorem (Corrected public-seed bound)

For all nonempty finite \(\mathcal{K}, \mathcal{D}, \mathcal{R}\), all \(\epsilon \in (0,1]\), every \(\epsilon\)-unpredictable source \(S\), and every unbounded distinguisher \(\mathsf{D}\), \[ \mathbf{Adv}^{\mathrm{ext\text{-}pub}}_{\mathcal{K},\mathcal{D},\mathcal{R}}(S,\mathsf{D}) \;\le\; \frac{1}{\sqrt{2}}\sqrt{\epsilon R} \;+\; \frac{6}{5}\sqrt{\frac{1 + \ln D}{K}} \;\le\; 2\sqrt{\epsilon R + \frac{\log_2 D}{K}} \; , \] and also, in a form sharper for large \(D\) or \(\epsilon\) near its minimum \(1/D\), \[ \mathbf{Adv}^{\mathrm{ext\text{-}pub}}_{\mathcal{K},\mathcal{D},\mathcal{R}}(S,\mathsf{D}) \;\le\; \frac{1}{\sqrt{2}}\sqrt{\epsilon R} \;+\; \sqrt{\frac{\ln(2eD\epsilon)}{2K}} \;+\; \frac{9}{10\sqrt{K}} \; . \]

Publishing the seed costs exactly one factor of \(K\), and costs it in one summand only: the \(\sqrt{\epsilon R}\) term (entropy deficiency) does not improve as the seed space grows, while the second term (adversarial selection over which support to attack) keeps its \(1/K\) in full. Proving this is a four-step argument – flatten the source to a fixed-size support, compute the mean statistical distance for one fixed support, control the deviation uniformly over all supports of all sizes via a bounded-differences (McDiarmid) concentration bound, and average – carried out in full in the linked PDF (Sections 3-4 there).

NoteCorollary (the conjecture holds)

For all nonempty finite \(\mathcal{K}, \mathcal{D}, \mathcal{R}\) with \(D \ge 2\), all \(\epsilon \in (0,1]\), every \(\epsilon\)-unpredictable source \(S\), and every unbounded distinguisher \(\mathsf{D}\), the conjectured bound \(\delta_{\mathrm{pub}}\) holds with \(c = \tfrac85\); the smallest constant obtainable by this route is \(\tfrac65\sqrt{1+\ln 2} \approx 1.5615\), attained at \(D = 2\). For \(D = 1\) it holds with \(c = \tfrac{1}{\sqrt2} + \tfrac65 < 1.91\). So \(c = 2\) suffices throughout the range in which an \(\epsilon\)-unpredictable source exists – the conjecture is proven.

Formal artifact.

Lean sources, highlighted · lean/Statement.lean · lean/MATCH.md

AI: Claude Opus 5 (Anthropic) · Reviewed by: nobody yet · 16 August 2026.

The statement is formalized; the proof is not. lhl_public_seed is the conjecture with a sorry for its proof, and that sorry is the only one in the file.

Nothing in it is opaque. Where c/0001 through c/0003 hide the object under study behind an opaque constant (which compiles, but pins nothing down), every quantifier here is written out: the finite sets, the uniform function table, both games, the two advantages, and the epsilon-unpredictability hypothesis. The constant c is bound outermost, ahead of the types and of epsilon, which is what makes it a universal constant and is the whole content of the conjecture.

Six lemmas are proved with no sorry, and #print axioms reports only propext, Classical.choice and Quot.sound for each: that the prediction advantage lies in [0,1], that the extraction advantage lies in [-1,1], and that when the output set is a singleton the extraction advantage is exactly 0. That last one is the real check on the definitions: it says the two challenge branches are interchangeable exactly when they carry no information, which fails for several plausible ways of getting the game wrong.

MATCH.md maps every quantifier, game line and constant of the Statement tab onto its Lean name, and records the judgement calls, including the one place the informal statement is silent (the alphabet the auxiliary information z is drawn from, left an arbitrary type here rather than assumed finite).

Partial progress on the proof

lean/Proof.lean · lean/LEDGER.md

proof_formal stays open, and will until lhl_public_seed itself compiles with no sorry. What exists is the bottom of the argument, proved rather than assumed: Proof.lean has zero sorrys of its own.

An audit of Mathlib v4.33.0 came first, because it decides the shape of the work. Two of the seven “standard facts” the proof PDF borrows from outside itself are not in fact available: there is no McDiarmid and no bounded-differences inequality at all (Azuma exists, but only in the measure-theoretic martingale setting), and there is no statistical distance on a PMF. Both have to be built.

Proved so far:

  • Statistical distance on a finite type, as half the l1 distance, with its basic properties and the one-sided identity the next step turns on.
  • Fact 2.1 in full: the best advantage any unbounded, randomized distinguisher achieves between two distributions is exactly their statistical distance. Bound and attainment, via the maximum-a-posteriori test, packaged as IsGreatest because the informal proof states it with a maximum.
  • The bridge, Lemma 3.1’s first half: the extraction game is a distinguishing game between the two laws the distinguisher’s view has under the two challenge bits, so the best extraction advantage equals that view distance. This is what lets every later step work with an analytic quantity instead of a game, and nothing above it could be formalized first.
  • The predictor bound, Lemma 3.1’s other half: no unbounded predictor beats the expected largest mass.

LEDGER.md lists the eight remaining obligations in dependency order and is blunt about which is the hard one: the finite bounded-differences inequality, which Mathlib does not help with and which is a project in itself.

Built against Mathlib v4.33.0 (db584cd6d46c92f209a44c0f1c829460d327499d) on leanprover/lean4:v4.33.0.

Why this is worth asking, and what in it is new. The bound’s shape is classical: in extractor parameters it is Theorem 6.17 of Vadhan’s Pseudorandomness, at parameters Radhakrishnan and Ta-Shma proved optimal. What is new is the hypothesis — \(\epsilon\)-unpredictability is an average over \(H\), so the source may have no entropy at all on an \(\epsilon\)-fraction of oracles, and the side information \(z\) may be \(H\) itself, which is exactly what puts it out of reach of the average-min-entropy leftover hash lemma. What makes it worth asking is the price of the seed. Read the game as key derivation: an unsalted random oracle needs no salt, but only because it assumes the source cannot look at \(H\) — drop that and it fails outright. A 2-universal family survives a source that can look, but needs \(\log_2 D - \log_2 R\) bits of salt, which is Stinson’s 1994 limitation. The conjecture says \(\log_2\log_2 D + 2\log_2(1/\delta) + O(1)\) bits buy the second’s robustness at essentially the first’s price — 77 bits against 1920 for a Diffie–Hellman element in a 2048-bit group at \(\delta = 2^{-32}\) — and buy it against an unbounded distinguisher, where bounding the adversary’s queries instead would ask for 113 bits at a budget of \(2^{80}\). The rest of this tab is that argument in detail; the statement note now carries the same paragraph.

This is the one resolved statement on the site, and the shape of the resolution is worth keeping in view: the naive guess — transposing the secret-seed expression directly into the public-seed game — is false, and the proof both refutes it and establishes a corrected bound with an explicit near-optimal constant. So the value here is not only the theorem but the counterexample that rules out the obvious statement.

Relation to known results

Recorded 28 August 2026, and it recalibrates the page. In extractor parameters this theorem is classical. Put \(n := \log_2 D\), \(k := \log_2(1/\epsilon)\), \(m := \log_2 R\), \(d := \log_2 K\) and balance each summand against a target error \(\delta\): the \(\sqrt{\epsilon R}\) term gives \(m = k - 2\log(1/\delta)\) and the \(\sqrt{\log_2 D / K}\) term gives \(d = \log n + 2\log(1/\delta)\). That is Theorem 6.17 of Vadhan’s Pseudorandomness — a random function is, with high probability, a strong extractor with optimal entropy loss — and Radhakrishnan and Ta-Shma proved those parameters optimal. The match is exact, not approximate: the second bound above carries \(\ln(2eD\epsilon) \approx (n-k)\ln 2\) and so delivers \(d = \log(n-k) + 2\log(1/\delta) + O(1)\), the sharp form, while the \(b_t := \tfrac1t\ln\binom{D}{t}\) the proof introduces to get there is the textbook count of flat \(k\)-sources.

Two things survive that reading, and they are why the page is not simply a rediscovery.

  • The leftover hash lemma genuinely cannot give this. It needs \(\{H(k,\cdot)\}_{k \in \mathcal{K}}\) to be 2-universal, and universal families need \(K \ge D/R\) whenever \(R < D\); the regime here is \(K \approx \log_2 D\), where no universal family exists. Conditioning on \(H\) and using an almost-universal LHL does not repair it, and the way it fails is worth stating exactly. On the \(\sqrt{\epsilon R}\) term the two routes give the same estimate — a universal family yields \(\tfrac12\sqrt{\epsilon R}\), and Lemma 3.2 above yields \(\tfrac12\sqrt{R/t}\), the \(1/\sqrt2\) in the theorem being only the floor step \(\lfloor 1/\epsilon_{H,z}\rfloor \ge 1/(2\epsilon_{H,z})\). The whole difference sits in the selection term, and the obstruction there is structural. Put \(W := \min\{R, \lfloor D\epsilon\rfloor\}\). Fix one seed \(k_1\), let \(\mathcal{S}\) be the \(R/W\) commonest symbols in the row \(H(k_1,\cdot)\) — they carry at least \(D/W \ge \lfloor 1/\epsilon\rfloor\) inputs — and let the source be uniform on a \(\lfloor 1/\epsilon\rfloor\)-subset of them. Cauchy–Schwarz twice (\(c_{k_1} \ge W/R\) on that support, and \(c_k \ge 1/R\) always) gives \(R\bar c - 1 \ge (W-1)/K\) for every table, so the LHL returns at least \(\tfrac12\sqrt{(W-1)/K}\). The rate in \(K\) is the same square root the theorem gives; what differs is what sits under it — the lemma pays \(\sqrt{W}\), a set size, where the theorem pays \(\sqrt{\log_2 D}\), a number of bits. Two side conditions gate the comparison: the floor bounds \(R\bar c - 1 = R\,\mathrm{CP} + \gamma\), so it concerns the second summand only when \((W-1)/K > R/t\), and the conjectured bound certifies \(\delta\) at all only when \(c\sqrt{\epsilon R} < \delta\). Where both hold — \(D = 2^{256}\), \(R = 2^{64}\), min-entropy \(160\), \(\delta = 2^{-32}\) — the comparison is \(\log_2 K = 74\) against at least \(126\), a gap of 52 bits; at min-entropy \(254\) it shows no loss at all, and at \(\epsilon = 1/D\) the bound is trivial, there being nothing to select. The cause is the Cauchy–Schwarz step \(\|v\|_1 \le \sqrt{KR}\|v\|_2\), tight only for a deviation spread over all \(KR\) cells. It does not follow that the true advantage against that source is \(O(1/K)\): the \(K-1\) unpinned rows contribute \(\Theta(\sqrt{R/t})\) and dominate. The floor says what the technique can certify, not how weak the source is. Cryptographically the gap is a salt-length gap, and one of kind rather than degree: with the derived key no longer than the source’s entropy gap, the conjectured salt is \(\log_2 n + 2\log_2(1/\delta) + 2\) bits and the collision route’s is \(m + 2\log_2(1/\delta) - 2\) — the first growing with the logarithm of the secret’s length, the second with the length of the key being derived. Deriving a 256-bit key rather than a 128-bit one from the same secret costs no extra salt under the conjecture and 128 further bits under the route; for a Diffie–Hellman element in a 2048-bit group at \(\delta = 2^{-32}\) it is a 77-bit salt against 190, and at 77 bits the route certifies \(2^{24.5}\), which is vacuous. This does not make the random oracle a worse extractor than universal hashing: a universal family avoids the second summand only by needing \(K \ge D/R\) seeds, and given that same salt the random oracle’s second summand falls to \(2^{-954.5}\) and the two tie — while at the salt the problem is posed at, 77 bits against at least 1920, universal hashing does not exist. Its immunity to support selection and its exponential seed are one property seen twice: universality constrains every pair separately, which is what makes choosing pairs last useless and what costs \(D/R\) seeds. All of this — the leftover-hash step, the calibration, the limitation, the two side conditions, the key-derivation reading and the comparison with universal hashing — is written out with proofs in a companion note: What the Leftover Hash Lemma Gives (LaTeX source). It resolves nothing; its prior-art section records that the bound is not new — it is the leftover hash lemma’s known seed-length limitation, stated as such by Barak et al. and attributed to Stinson — and its closing section says plainly what it does not claim: that the lemma attains that floor. It now also lists Barak et al.’s own results — the seed-length and entropy-loss limitations, their generalised LHL, expand-then-extract, and the unsalted random-oracle heuristic — because the two axes are independent and it matters which one is at issue here: their entropy-loss improvement leaves the seed-length limitation exactly where it was, and their own attempt on the seed length, expand-then-extract, fails in general (a DDH-based generator with a perfectly universal hash is distinguishable with probability near 1 given the short seed), holding only for logarithmically many extracted bits or in minicrypt. Reading the paper again to list them caught a misquote in the note: their generalised bound is \(\sqrt{\varepsilon 2^{-L}}\), not \(\varepsilon 2^{-L/2}\). It is organised around that comparison: the setting, then every bound with no proof, then the comparison, then what is not claimed — with the proofs and everything peripheral to the seed-length question in appendices. The proof above avoids this by working in \(L_1\) throughout, which is the same route the classical existence proofs take. See the problem hub for the arithmetic.
  • The hypothesis is weaker than the classical one. \(\epsilon\)-unpredictability bounds \(\mathbb{E}_{(H,Z)}[\max_x \Pr[X=x \mid H,Z]]\), an average over \(H\), so the source may have zero entropy on an \(\epsilon\)-fraction of oracles. Classical statements quantify per source and conclude with high probability over the extractor, which cannot be applied; the average-min-entropy leftover hash lemma of Dodis, Ostrovsky, Reyzin and Smith does not help, since there the side information must be independent of the hash key and here \(z\) may be \(H\) itself. The note’s closing remark isolates this correctly — the selection term is a high-probability-over-\(H\) statement, the deficiency term inherently is not — without saying that this is the part with no precedent.

What is not novel, contrary to how the setting reads, is that the source sees the entire function table. The probabilistic-method union bound runs over flat sources before the source is fixed, so it already covers supports chosen with \(H\) in hand.

One consequence for the proof note itself: Remark 5.3 offers matching lower bounds for both summands as sketches (“For the second we only sketch”). Radhakrishnan and Ta-Shma proved both — \(d \ge \log(n-k) + 2\log(1/\epsilon) - O(1)\), and \(d + k - m \ge 2\log(1/\epsilon) - O(1)\), which specialises to \(k - m \ge 2\log(1/\epsilon) - O(1)\) for strong extractors since \((\mathit{sd}, \mathrm{Ext}(x,\mathit{sd}))\) is then an ordinary extractor with output \(m+d\). The sketch can be replaced by a citation. See the problem hub for the full comparison, including the secret-seed cell.

Bounding the queries

Recorded 29 August 2026. The game hands every party the whole table. Bound the oracle queries instead — the source makes \(q_S\), the distinguisher \(q_D\), the predictor still unbounded so the hypothesis is unchanged — and both routes move, but not symmetrically. The companion note states these among its bounds and proves them.

  • What governs the collision route is row breadth, not query count. Write \(r_S\) for the expected number of distinct seeds at which the source queries anything, and \(s_S\) for the expected number at which it queries its own output; both are at most \(\min(q_S,K)\), and both equal \(1\) for the source that forces the floor above, which spends \(D\) queries reading one row. Then \(\mathbf{Adv} \le \tfrac12\sqrt{\epsilon R + 2R\,r_S/K}\). The proof is that an untouched row stays fresh: conditioning on the whole table normally destroys that, but the row-versus-rest factorisation survives it. The dependence is exact up to a factor of two — a source pinning \(j\) rows at one input forces \(R\bar c - 1 \ge (R-1)j/K\) for every table — so a source may spend \(D\) queries inside one row and stay capped, while \(K\) queries placed one per row exhaust the bound.
  • That closes the window the note left open. Theorem 1 there is a floor with no matching ceiling; the one sketched exceeded it by about \(2^{21}\). For \(D = 2^{256}\), \(R = 2^{64}\), min-entropy \(160\) and \(K = 2^{74}\) the floor is \((W-1)/K \approx 2^{-10}\) and the new ceiling is \(\epsilon R + 2R/K \approx 2^{-9}\): a factor of two.
  • \(q_D\) cannot appear in that route at all. It passes through a statistical distance, which is the supremum of the advantage over all distinguishers, so no bound obtained that way can improve as \(q_D\) falls. Pricing \(q_D\) means leaving the lemma. Doing so — identical-until-bad on the single cell \((\mathit{sd},x)\) — gives \(\mathbf{Adv} \le s_S/K + q_D\epsilon\), and the two are incomparable: the bad-cell route is the smaller exactly when \(q_D \le \tfrac12\sqrt{R/\epsilon}\).
  • At a realistic query budget, bounding the queries buys no salt. Reading Theorem 3 as a salt requirement, \(\log_2 K \ge n + \log_2(1/\delta) + 1\) when both parties make \(2^n\) queries — feasible only while \(n \le \mu - \log_2(1/\delta) - 1\). For the three settings of the salt table that is \(113\), \(145\) and \(145\) bits at \(n = 80\), against the conjecture’s \(77\), \(141\) and \(139\). The conjectured salt is flat in the query budget and holds against an unbounded adversary; this one grows a bit per doubling, and they cross at \(n = 44\), \(76\), \(74\). The bad-cell route pays \(\log_2 q\) where the conjecture pays \(\log_2\log_2 D\), and only halves the \(\delta\) term in exchange. That certified column is also generous: \(s_S \le 2^n\) is unreachable at these min-entropies, since each pinned row costs \(\log_2 R\) bits of it, capping the attack at \(14\), \(6\) and \(1\) rows and forcing only \(36\), \(67\) and \(64\) bits. A source can query \((k,x)\) at its own output for many \(k\) and ignore the answers — no entropy lost, no advantage gained, yet \(s_S\) inflates to the budget and Theorem 3 charges for it.
  • That threshold is not a close call. It is \(2^{111}\) in the instance above, and \(2^{127}\) for a \(128\)-bit key derived from a source of min-entropy \(128\). Below it — which is every query budget anyone would deploy — the leftover hash lemma is simply the wrong instrument for this game: against \(q_D = 2^{80}\) the bad-cell route returns \(2^{-74}\) where the collision route returns \(2^{-5.5}\). So the conjecture’s content is specifically about the unbounded distinguisher, and its second summand is the price of that unboundedness.

The predictor has a budget too, and it is not free. Write \(\epsilon_q\) for the source’s unpredictability against predictors making at most \(q\) oracle queries, so \(\epsilon_0 \le \epsilon_1 \le \cdots \le \epsilon_\infty\), the last being the full-table notion used above. Bounding the predictor weakens the hypothesis, so the question is how weak it may be made. The two routes answer differently, and one witness settles both — a source that sums \(m\) reserved cells of row 1 modulo \(R\), for which \(\epsilon_q\) jumps from \(1/R\) to \(1\) exactly at \(q = m\), and whose output is a deterministic function of the table.

  • The bad-cell route needs the predictor to be as rich as the distinguisher, and no richer. Its reduction is query-preserving: the predictor built there runs the distinguisher and forwards each of its queries, drawing \(\mathit{sd}\) and \(y\) itself, so it makes exactly \(q_D\) queries. Hence \(\mathbf{Adv} \le s_S/K + q_D\epsilon\) whenever \(q_P \ge q_D\). That is tight to within one query: at \(q_P \le q_D - 2\) the witness makes the same bound false.
  • The collision route needs an unbounded predictor, and no finite budget will do. It bounds a statistical distance, so its distinguisher is unbounded by construction, and the predictor must match. On the witness with \(m = q_P + 1\) the source looks perfectly unpredictable — \(\epsilon_{q_P} = 1/R\) — while \(\mathrm{CP} = 1\) and an unbounded distinguisher wins with advantage \(1 - 1/R\); stated with \(\epsilon_{q_P}\) the bound would read \(\tfrac12\sqrt{2}\) at \(K \ge 2R\), and be false for every \(R \ge 4\).

So every bound before this section is stated against a predictor holding the whole table not as a stylistic preference for the strongest hypothesis, but because the technique forces it. The predictor must be granted at least what the distinguisher is granted, and granting it exactly that is enough. One consequence is worth stating on its own: for a deterministic source \(\epsilon_{q_S} = 1\), since a predictor with \(q_S\) queries just reruns it — so such a source can only be extracted from securely against distinguishers strictly poorer than the source itself, whatever the seed length, and whatever entropy is being extracted must sit in the source’s coins rather than in the oracle it reads.

What is not proved is the bound one would most like, \(s_S/K + \tfrac12\sqrt{\epsilon R}\), which would match the true advantage against the witness in both summands. It needs the freshness lemma refined from “row \(k\) untouched” to “the cell \((k,X)\) untouched”, and that refinement does not follow from the argument given.

What remains

Verification rather than mathematics. The proof is AI-written and has not been reviewed by a human, and the Lean formalization stops at the statement: lean/Statement.lean still carries the single real sorry, and lean/LEDGER.md lists what a full formalization would have to discharge, item 6 (bounded differences, which Mathlib does not have) being the largest.