Provedattentioninnovationexternal-review-3

Exact deadline completion: expected-work recurrence

For all $\htmlData{mx=1}{p, \mathit{trial}, \mathit{dense} \in \htmlData{mx=0}{\mathbb{R}}}$ and $\htmlData{mx=3}{W : \htmlData{mx=0}{\mathbb{N}} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ , if $\htmlData{mx=0}{p} \mathrel{\htmlData{mx=1}{\neq}} 0$ , $\htmlData{mx=1}{\htmlData{mx=0}{W}(0)} \mathrel{\htmlData{mx=3}{=}} \htmlData{mx=2}{\mathit{dense}}$ and $\htmlData{mx=13}{\forall L,\ \htmlData{mx=3}{\htmlData{mx=0}{W}(\htmlData{mx=2}{\htmlData{mx=1}{L} + 1})} \mathrel{\htmlData{mx=12}{=}} \htmlData{mx=11}{\htmlData{mx=4}{\mathit{trial}} + \htmlData{mx=10}{(\htmlData{mx=6}{1 - \htmlData{mx=5}{p}}) \cdot \htmlData{mx=9}{\htmlData{mx=7}{W}(\htmlData{mx=8}{L})}}}}$ , then

\htmlData{mx=20}{\forall L,\ \htmlData{mx=2}{\htmlData{mx=0}{W}(\htmlData{mx=1}{L})} \mathrel{\htmlData{mx=19}{=}} \htmlData{mx=18}{\htmlData{mx=11}{\frac{\htmlData{mx=9}{\htmlData{mx=3}{\mathit{trial}} \cdot (\htmlData{mx=8}{1 - \htmlData{mx=7}{(\htmlData{mx=5}{1 - \htmlData{mx=4}{p}})^{\htmlData{mx=6}{L}}}})}}{\htmlData{mx=10}{p}}} + \htmlData{mx=17}{\htmlData{mx=12}{\mathit{dense}} \cdot \htmlData{mx=16}{(\htmlData{mx=14}{1 - \htmlData{mx=13}{p}})^{\htmlData{mx=15}{L}}}}}}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
x ∈ TVariables: p, trial, dense range over real numbers: the statement must hold for every choice. ((p trial dense : ℝ))
NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
⟹Implies: If ℕ, then ℝ. (Between types, A → B is the type of functions from A to B.) (ℕ → ℝ)
≠Not equal: p and 0 are different. (p ≠ 0)
f(x)Function application: W applied to 0. Lean writes f x; papers write f(x). (W 0)
=Equality: W(0) and dense are the same. (W 0 = dense)
∀For all: The statement after the comma holds for every L. (∀ L, W (L + 1) = trial + (1 - p) * W L)
+Addition: L plus 1. (L + 1)
a/bDivision: trial · (1 − (1 − p)^L) divided by p. In Lean, dividing by 0 gives 0. (trial * (1 - (1 - p) ^ L) / p)
aᵇPower: 1 − p raised to the power L. ((1 - p) ^ L)
·Multiplication: 1 − p times W(L). ((1 - p) * W L)
-Subtraction: 1 minus p. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (1 - p)

theorem innov-deadline-expected-work (p trial dense : ℝ) (W : ℕ → ℝ) (hp : p ≠ 0) (h0 : W 0 = dense) (hstep : ∀ L, W (L + 1) = trial + (1 - p) * W L) :
    ∀ L, W L = trial * (1 - (1 - p) ^ L) / p + dense * (1 - p) ^ L

Solves the trial-plus-dense-work recurrence under assumed base and step. No runtime or model speed measurement.

How it was proved

Proved: 6 October 2026
By: Ajax, with the agent “Baguette math & proofs (Claude Code, 2026-10-03)”
Checked by: Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms: Classical.choice, Quot.sound, propext
Proof: 15 lines of Lean

Exact deadline completion: expected-work recurrence

How it was proved

More proved statements