ε-Cell First-Fire Bound

This file develops the first-fire bound for a hidden value drawn from an arbitrary sampler oa : ProbComp R whose every outcome has probability at most ε. Where the uniform development (FirstFire.lean) charges a state-dependent 1 / (|R| - S.card) per genuine read and needs an exact telescope to fold the growing exclusion sets, the ε-development charges a single uniform ε per read, valid in every state. The first-fire telescope collapses to a plain union bound: an adaptive q-read strategy fires with probability at most q · ε.

The model

A hidden target w ← oa is drawn once and committed into the run's state; an adaptive q-read strategy σ : List Bool → R, mapping the boolean reply history (hit/miss) to the next read point, then probes that fixed w, firing as soon as some read equals w. Up to the first hit the read points are fixed by the all-miss history and independent of w, so averaging over the single hidden draw — without ever conditioning on the drawn value — bounds the firing probability by the union of q fixed singletons, each of mass at most ε. This models an eager run that commits a sampled key at draw time and exposes it only through later membership tests. Because the per-outcome bound ∀ r, Pr[= r | oa] ≤ ε holds unconditionally, the bound is valid in every state.

Main results

• hiddenReadMany / probEvent_hiddenReadMany_le : the single-target adaptive read game and its first-fire union bound Pr[fire] ≤ q · ε.
• hiddenReadList / probEvent_hiddenReadList_le : the per-attempt-fresh-target list game and its union bound.
• probEvent_bind_fire_le_of_gen : the deferred-sampling fire bound whose marginal is a hidden-target read, against an opaque continuation.
• drawList : the explicit i.i.d. front-tape form of the per-attempt draws.

Hidden-target adaptive first-fire bound

hiddenReadMany draws a single hidden target w ← oa once and lets an adaptive q-read strategy probe that fixed w repeatedly. This is the structure of an eager run that commits a sampled key into its state at draw time and then exposes it only through later membership tests: the key's value is hidden until the first hit, so up to the first hit the read points are fixed (determined by the all-miss reply history) and independent of w. Averaging over the single hidden draw — without ever conditioning on the drawn value — gives the union bound q · ε.

noncomputable def OracleComp.readMany {R : Type} [DecidableEq R] (w : R) : ℕ → (List Bool → R) → Bool

Adaptive q-read game against a FIXED hidden target w: the strategy σ maps the list of boolean replies (hit/miss) seen so far to the next read point, and the game fires (returns true) iff some read equals w. The target w is reused across all reads; it is drawn once, outside this program (see hiddenReadMany).

noncomputable def OracleComp.hiddenReadMany {R : Type} [DecidableEq R] (oa : ProbComp R) (q : ℕ) (σ : List Bool → R) : ProbComp Bool

The hidden-target game: draw the target w ← oa once, then run q adaptive reads against that fixed w.

theorem OracleComp.readMany_true_iff {R : Type} [DecidableEq R] (w : R) (q : ℕ) (σ : List Bool → R) : readMany w q σ = true ↔ ∃ j < q, w = σ (List.replicate j false)

Fixed read points before the first hit. A FIXED-target adaptive read game fires iff the hidden target w equals one of the q read points reached along the all-miss history σ (List.replicate j false). The point: those read points do not depend on w (until a hit, every reply is a miss, so the history is replicate j false), which is exactly what turns the averaged firing probability into a plain union bound.

theorem OracleComp.probEvent_hiddenReadMany_le {R : Type} [DecidableEq R] {oa : ProbComp R} {ε : ENNReal} (hε : ∀ (r : R), Pr[= r | oa] ≤ ε) (q : ℕ) (σ : List Bool → R) : (probEvent (hiddenReadMany oa q σ) fun (b : Bool) => b = true) ≤ ↑q * ε

Hidden-target adaptive first-fire bound. A FIXED target w ← oa drawn once and probed by q adaptive reads fires with probability at most q · ε, whenever every outcome of oa has mass at most ε. The averaging is over the single hidden draw; we never condition on w. Because the read points are fixed by the all-miss history (readMany_true_iff), the firing event is the union of the q fixed singletons {w = σ (replicate j false)}, each of mass at most ε.

noncomputable def OracleComp.readManyList {R : Type} [DecidableEq R] (ws : List R) (q : ℕ) (σ : List Bool → R) : Bool

The multi-key fixed-target game: a list ws of hidden keys, each probed by the same q adaptive reads; fires iff some read hits some key. Used to model the eager ghost run, whose ghost cache accumulates one sampled key per rejected signing attempt.

theorem OracleComp.readManyList_true_iff {R : Type} [DecidableEq R] (ws : List R) (q : ℕ) (σ : List Bool → R) : readManyList ws q σ = true ↔ ∃ w ∈ ws, readMany w q σ = true

The list game fires iff some individual key's game fires.

theorem OracleComp.probEvent_bind_const_or_pure (q : Bool) (mb : ProbComp Bool) : (probEvent (do let b ← mb pure (q || b)) fun (c : Bool) => c = true) ≤ (probEvent (pure q) fun (c : Bool) => c = true) + probEvent mb fun (c : Bool) => c = true

Appending a fixed OR-flag q to a Boolean draw raises the firing probability by at most the mass of q (i.e. 1 when q = true, 0 otherwise) over the residual draw.

noncomputable def OracleComp.hiddenReadList {R : Type} [DecidableEq R] (oa : ProbComp R) (q : ℕ) (σ : List Bool → R) : ℕ → ProbComp Bool

The probabilistic multi-key game: draw n hidden targets independently from oa, one per rejected signing attempt, and probe each by the same q adaptive reads; fire iff some read hits some target. This is the accumulating-ghost-cache form of hiddenReadMany.

theorem OracleComp.probEvent_hiddenReadList_le {R : Type} [DecidableEq R] {oa : ProbComp R} {ε : ENNReal} (hε : ∀ (r : R), Pr[= r | oa] ≤ ε) (q : ℕ) (σ : List Bool → R) (n : ℕ) : (probEvent (hiddenReadList oa q σ n) fun (b : Bool) => b = true) ≤ ↑n * (↑q * ε)

Multi-key hidden-target first-fire bound. Drawing n independent hidden targets from oa (each outcome of mass at most ε) and probing each by q adaptive reads fires with probability at most n · q · ε. Proved by induction on n: the head key's contribution is the single-target bound probEvent_hiddenReadMany_le (≤ q · ε), the tail's is the inductive hypothesis (≤ n · q · ε), combined by the OR-append step probEvent_bind_const_or_pure. This is the form that bounds the eager ghost run's bad probability once the run is factored so that each rejected signing attempt's key draw is read off as an independent hiddenReadMany target.

Averaging the key count and the run-factorization bridge

The multi-key bound probEvent_hiddenReadList_le is stated for a fixed number of keys n. In the intended application the key count is itself random (one ghost key is drawn per rejected signing attempt), so the closing step averages the bound over a key-count distribution kn : ProbComp ℕ, yielding E[n] · q · ε. The final bridge probEvent_le_of_eq_bind_hiddenReadList packages the union-bound side of the direct route: once a run's bad marginal is exhibited as a kn >>= hiddenReadList oa q σ game (the deferred-sampling factorization), the bound is immediate.

theorem OracleComp.probEvent_bind_hiddenReadList_le {R : Type} [DecidableEq R] {oa : ProbComp R} {ε : ENNReal} (hε : ∀ (r : R), Pr[= r | oa] ≤ ε) (q : ℕ) (σ : List Bool → R) (kn : ProbComp ℕ) : (probEvent (do let n ← kn hiddenReadList oa q σ n) fun (b : Bool) => b = true) ≤ (∑' (n : ℕ), Pr[= n | kn] * ↑n) * (↑q * ε)

Averaged multi-key hidden-target bound. When the number of independently drawn hidden keys is itself sampled from kn : ProbComp ℕ, the firing probability of the multi-key game is at most E[n] · q · ε, where E[n] = ∑' n, Pr[= n | kn] · n is the expected key count. This is the averaging step (C3) of the direct route: it folds the fixed-n bound probEvent_hiddenReadList_le against the key-count distribution. Combined with an expected-count bound E[n] ≤ qS / (1 - p) it gives the target qS · q · ε / (1 - p).

theorem OracleComp.probEvent_le_of_eq_bind_hiddenReadList {R : Type} [DecidableEq R] {β : Type} {run : ProbComp β} {bad : β → Prop} {oa : ProbComp R} {ε : ENNReal} (hε : ∀ (r : R), Pr[= r | oa] ≤ ε) (q : ℕ) (σ : List Bool → R) (kn : ProbComp ℕ) (hfac : probEvent run bad ≤ probEvent (do let n ← kn hiddenReadList oa q σ n) fun (b : Bool) => b = true) : probEvent run bad ≤ (∑' (n : ℕ), Pr[= n | kn] * ↑n) * (↑q * ε)

Direct-route union-bound bridge. If an arbitrary run run : ProbComp β with a bad event bad : β → Prop has its bad marginal exhibited as the averaged multi-key hidden-target game kn >>= hiddenReadList oa q σ — i.e. the deferred-sampling factorization that pulls the run's hidden key draws into an independent front block, reading each off as a hiddenReadMany target probed by the q subsequent adaptive reads — then the run's bad probability is bounded by the expected-count union bound E[n] · q · ε.

This is the reusable closing lemma of the direct route: the entire remaining content is supplied as the hypothesis hfac, the distributional equality between the run's bad indicator and the abstract game. Establishing hfac is the deferred-sampling commutation (factoring the run's per-key draws to the front so the pre-first-hit reads become the deterministic strategy σ); the union-bound side it feeds into is fully discharged here via probEvent_bind_hiddenReadList_le.

Single output-irrelevant draw deferral

The lemmas above take the read strategy σ (and, in hiddenReadList, the key count) as already extracted data. The genuine new content of the sound route is the deferral primitive: lifting a single hidden draw out of an arbitrary run when that draw is used only output-irrelevantly — i.e. it influences neither the run's visible output nor the read points, only the boolean "fire" flag computed by membership tests against an adaptive read sequence.

The key observation (cf. ghostHybridImpl_proj_trans: the ghost cache is a per-step deterministic projection of the single ghost-blind run, and the read answer is independent of the ghost value) is that such a draw can be deferred past its continuation. Concretely, a run oa >>= k whose continuation k w is built from a w-free generator gen (producing both the visible output and the read strategy) with w entering only through readMany w q σ, has its fire-marginal equal to that of the deferred game gen >>= fun p => oa >>= fun w => …. Each generated branch is then a hiddenReadMany game on a fixed strategy p.2, charged q · ε by probEvent_hiddenReadMany_le. This converts "front-load the draw across the opaque continuation" into a local bind-commutation, the tractable route.

theorem OracleComp.probEvent_bind_fire_eq_defer {R : Type} [DecidableEq R] {α : Type} (oa : ProbComp R) (q : ℕ) (gen : ProbComp (α × (List Bool → R))) (k : R → ProbComp (α × Bool)) (hk : ∀ (w : R), k w = do let p ← gen pure (p.1, readMany w q p.2)) : (probEvent (oa >>= k) fun (z : α × Bool) => z.2 = true) = probEvent (do let p ← gen let w ← oa pure (p.1, readMany w q p.2)) fun (z : α × Bool) => z.2 = true

Bind-commutation for an output-irrelevant draw. When the continuation k w is gen >>= fun p => pure (p.1, readMany w q p.2) — a w-free generator gen producing both the visible output p.1 and the read strategy p.2, with the hidden draw w entering only through the fixed read game readMany w q p.2 — the fire-marginal of the run oa >>= k is unchanged by deferring the draw of w to after gen. This is the local deferral step that replaces the abstract "front-load across the fold" with a PMF.bind-commutation, proved here directly at the probEvent level via ENNReal.tsum_comm.

theorem OracleComp.probEvent_bind_fire_le_of_gen {R : Type} [DecidableEq R] {α : Type} {oa : ProbComp R} {ε : ENNReal} (hε : ∀ (r : R), Pr[= r | oa] ≤ ε) (q : ℕ) (gen : ProbComp (α × (List Bool → R))) (k : R → ProbComp (α × Bool)) (hk : ∀ (w : R), k w = do let p ← gen pure (p.1, readMany w q p.2)) : (probEvent (oa >>= k) fun (z : α × Bool) => z.2 = true) ≤ ↑q * ε

Single output-irrelevant draw first-fire bound (structural form). A run oa >>= k that draws one hidden value w ← oa (each outcome of mass at most ε) and feeds it to a continuation k w = gen >>= fun p => pure (p.1, readMany w q p.2) — a w-free generator gen producing the visible output and the read strategy, with w entering only through the fixed read game — fires with probability at most q · ε.

This is the reusable single-draw deferral primitive of the sound route. It formalizes "output-irrelevant draw ⇒ the read points are a fixed strategy independent of w" by demanding the continuation factor through a w-free gen; the proof defers the draw past gen (probEvent_bind_fire_eq_defer) so each generated branch becomes a hiddenReadMany game on a fixed strategy p.2, charged q · ε by probEvent_hiddenReadMany_le. Stage B lifts the n-interleaved draws by induction with gen carrying the remaining draws; Stage C instantiates gen/k for the ghost-blind run via the projection ghostHybridImpl_proj_trans.

theorem OracleComp.probEvent_bind_fire_le_of_marginal_eq_readMany {R : Type} [DecidableEq R] {α : Type} {oa : ProbComp R} {ε : ENNReal} (hε : ∀ (r : R), Pr[= r | oa] ≤ ε) (q : ℕ) (σ : List Bool → R) (k : R → ProbComp (α × Bool)) (hmarg : ∀ (w : R), (probEvent (k w) fun (z : α × Bool) => z.2 = true) = probEvent (pure (readMany w q σ)) fun (b : Bool) => b = true) : (probEvent (oa >>= k) fun (z : α × Bool) => z.2 = true) ≤ ↑q * ε

Single output-irrelevant draw first-fire bound (marginal form). The convenience special case of probEvent_bind_fire_le_of_gen for a run oa >>= k whose continuation's fire-marginal is, for every hidden value w, exactly that of the fixed read game readMany w q σ against a single strategy σ independent of w. Whenever every outcome of oa has mass at most ε, the run fires with probability at most q · ε.

Use this form when the deferred read strategy is a fixed σ (the simplest output-irrelevant case); use the structural probEvent_bind_fire_le_of_gen when the strategy is itself produced by w-free randomness.

Iterated draws: the explicit front-block key list

Stage A defers a single output-irrelevant draw. drawList lifts this to n interleaved draws by collecting them into an explicit front block: draw a list of n independent keys up front, against which a run's hidden draws can be exhibited and then charged by the abstract hiddenReadList union bound.

noncomputable def OracleComp.drawList {R : Type} (oa : ProbComp R) : ℕ → ProbComp (List R)

Draw a list of n independent keys from oa (the front block of the deferred-sampling factorization). The keys are the hidden targets; the list length is the key count n.

@[simp]

theorem OracleComp.probFailure_drawList {R : Type} (oa : ProbComp R) (n : ℕ) : Pr[⊥ | drawList oa n] = 0

The front-block draw never fails: it only ever draws from oa (which is failure-free) and returns, so drawList oa n has zero failure mass.

theorem OracleComp.tsum_probOutput_drawList_eq_one {R : Type} (oa : ProbComp R) (n : ℕ) : ∑' (ws : List R), Pr[= ws | drawList oa n] = 1

Total output mass of the front-block draw is 1 (it never fails).