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.

View PDF · Download LaTeX source – states both the public-seed and secret-seed variants (Conjectures 2 and 1 respectively); only the public-seed case is tracked as its own statement on this site

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.

Definition (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

Conjecture (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) . \]

View PDF · Download LaTeX source

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 (Conjecture 1 of the same source document) 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

Proposition (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

Theorem (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).

Corollary (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/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.

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.

What remains is 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.

Independent human review of the informal proof (currently “reviewed by: nobody yet”).
Independent human match check of lean/Statement.lean against the Statement tab. MATCH.md is an AI match check; the quantifier order on c, and the bit convention in extGame (which the sanity lemmas deliberately do not pin down), are the two places to look first.
Finish the formal proof. lean/Proof.lean has the statistical-distance foundation, Fact 2.1 in full, and the bridge from the game to the analytic quantity, all sorry-free; lean/LEDGER.md lists the eight remaining obligations. Mathlib v4.33.0 has been checked and carries no McDiarmid and no bounded-differences inequality, so that step has to be proved from scratch in the finite case.
Decide whether Z should stay an arbitrary type or be pinned to a finite alphabet, and say so in the Statement tab either way.