A finite-tree tail bound for adaptive rank-decreasing processes

A state may store the entire previous history. At each state, a finite kernel chooses an outcome and the state updates deterministically. Rank never increases, and while positive it strictly decreases with probability at least p. The probability of positive rank after t rounds is bounded using a killed exponential potential. This yields a coarse exponential tail; it does not establish the paper's sharper leading constant 2n.

structure LeanPool.SingleCopyStabilizer.AdaptiveProcess.RankedProcess (S : Type u_1) (Ω : Type u_2) [Fintype Ω] : Type (max u_1 u_2)

A finite outcome kernel together with a monotone natural-valued rank. There is no Markov restriction: S can contain the complete history.

• weight : S → Ω → ℝ

  Conditional probability of an outcome at the current state.

• next : S → Ω → S

  State reached after observing the chosen outcome.

• rank : S → ℕ

  Natural-valued obstruction whose disappearance marks success.

• weight_nonneg (s : S) (o : Ω) : 0 ≤ self.weight s o
• weight_sum (s : S) : ∑ o : Ω, self.weight s o = 1
• rank_mono (s : S) (o : Ω) : self.rank (self.next s o) ≤ self.rank s

def LeanPool.SingleCopyStabilizer.AdaptiveProcess.potential (r : ℕ) : ℝ

The exponential potential is killed on reaching rank zero.

Equations

• LeanPool.SingleCopyStabilizer.AdaptiveProcess.potential r = if r = 0 then 0 else 2 ^ r

@[simp]

theorem LeanPool.SingleCopyStabilizer.AdaptiveProcess.potential_zero : potential 0 = 0

theorem LeanPool.SingleCopyStabilizer.AdaptiveProcess.potential_nonneg (r : ℕ) : 0 ≤ potential r

theorem LeanPool.SingleCopyStabilizer.AdaptiveProcess.potential_le_pow (r : ℕ) : potential r ≤ 2 ^ r

theorem LeanPool.SingleCopyStabilizer.AdaptiveProcess.potential_mono {a b : ℕ} (h : a ≤ b) : potential a ≤ potential b

theorem LeanPool.SingleCopyStabilizer.AdaptiveProcess.potential_le_half_of_lt {a b : ℕ} (h : a < b) : potential a ≤ potential b / 2

Strict rank progress at least halves the killed exponential potential.

def LeanPool.SingleCopyStabilizer.AdaptiveProcess.RankedProcess.progressMass {S : Type u_1} {Ω : Type u_2} [Fintype Ω] (P : RankedProcess S Ω) (s : S) : ℝ

Total probability assigned to strict progress at the current state.

Equations

• P.progressMass s = ∑ o : Ω, if P.rank (P.next s o) < P.rank s then P.weight s o else 0

def LeanPool.SingleCopyStabilizer.AdaptiveProcess.RankedProcess.failureProbability {S : Type u_1} {Ω : Type u_2} [Fintype Ω] (P : RankedProcess S Ω) : ℕ → S → ℝ

Probability of positive rank after the given number of rounds, defined by the finite probability tree. Each recursive layer is one fresh kernel draw.

Equations

• P.failureProbability 0 x✝ = if P.rank x✝ = 0 then 0 else 1
• P.failureProbability t.succ x✝ = ∑ o : Ω, P.weight x✝ o * P.failureProbability t (P.next x✝ o)

theorem LeanPool.SingleCopyStabilizer.AdaptiveProcess.RankedProcess.failure_probability_nonneg {S : Type u_1} {Ω : Type u_2} [Fintype Ω] (P : RankedProcess S Ω) (t : ℕ) (s : S) : 0 ≤ P.failureProbability t s

theorem LeanPool.SingleCopyStabilizer.AdaptiveProcess.RankedProcess.failure_probability_le_one {S : Type u_1} {Ω : Type u_2} [Fintype Ω] (P : RankedProcess S Ω) (t : ℕ) (s : S) : P.failureProbability t s ≤ 1

theorem LeanPool.SingleCopyStabilizer.AdaptiveProcess.RankedProcess.failure_probability_of_rank_zero {S : Type u_1} {Ω : Type u_2} [Fintype Ω] (P : RankedProcess S Ω) (t : ℕ) (s : S) (hs : P.rank s = 0) : P.failureProbability t s = 0

Rank zero is absorbing, so positive rank after t rounds is equivalent to not having reached rank zero earlier.

theorem LeanPool.SingleCopyStabilizer.AdaptiveProcess.RankedProcess.potential_drift {S : Type u_1} {Ω : Type u_2} [Fintype Ω] (P : RankedProcess S Ω) (p : ℝ) (hprogress : ∀ (s : S), 0 < P.rank s → p ≤ P.progressMass s) (s : S) : ∑ o : Ω, P.weight s o * potential (P.rank (P.next s o)) ≤ (1 - p / 2) * potential (P.rank s)

A per-node strict-progress mass bound gives a one-step contraction of the killed potential, including at the terminal states.

theorem LeanPool.SingleCopyStabilizer.AdaptiveProcess.RankedProcess.failure_probability_le_potential {S : Type u_1} {Ω : Type u_2} [Fintype Ω] (P : RankedProcess S Ω) (p : ℝ) (hp : p ≤ 2) (hprogress : ∀ (s : S), 0 < P.rank s → p ≤ P.progressMass s) (t : ℕ) (s : S) : P.failureProbability t s ≤ (1 - p / 2) ^ t * potential (P.rank s)

Finite adaptive-tree tail bound. The success assumption is checked at every reachable or unreachable state of the supplied process, so it applies uniformly to states encoding arbitrary previous histories.

theorem LeanPool.SingleCopyStabilizer.AdaptiveProcess.RankedProcess.failure_probability_le {S : Type u_1} {Ω : Type u_2} [Fintype Ω] (P : RankedProcess S Ω) (p : ℝ) (hp : p ≤ 2) (hprogress : ∀ (s : S), 0 < P.rank s → p ≤ P.progressMass s) (t n : ℕ) (s : S) (hrank : P.rank s ≤ n) : P.failureProbability t s ≤ 2 ^ n * (1 - p / 2) ^ t

A simpler tail bound using only an upper bound on the initial rank.

theorem LeanPool.SingleCopyStabilizer.AdaptiveProcess.RankedProcess.failure_probability_le_seven_eighths {S : Type u_1} {Ω : Type u_2} [Fintype Ω] (P : RankedProcess S Ω) (hprogress : ∀ (s : S), 0 < P.rank s → 1 / 4 ≤ P.progressMass s) (t n : ℕ) (s : S) (hrank : P.rank s ≤ n) : P.failureProbability t s ≤ 2 ^ n * (7 / 8) ^ t

If each nonterminal state progresses with probability at least one quarter, failure after t rounds is at most 2^n (7/8)^t.

theorem LeanPool.SingleCopyStabilizer.AdaptiveProcess.RankedProcess.failure_probability_eight_rounds_per_bit {S : Type u_1} {Ω : Type u_2} [Fintype Ω] (P : RankedProcess S Ω) (hprogress : ∀ (s : S), 0 < P.rank s → 1 / 4 ≤ P.progressMass s) (n k : ℕ) (s : S) (hrank : P.rank s ≤ n) : P.failureProbability (8 * (n + k)) s ≤ (1 / 2) ^ k

A concrete confidence budget: 8(n+k) rounds give failure probability at most 2^(-k) under the quarter-progress hypothesis. This is deliberately coarser than the paper's sharp geometric-sum estimate.