Wald's identity without martingales: cap the steps and bound the stopped walk pathwise

To show E τ < ∞ for the first positive time τ of an iid walk with E ξ > 0 (only a first moment), avoid optional stopping. Replace ξ by min(ξ, c) with c large enough that E min(ξ, c) > 0 (dominated convergence by |ξ|, eventually equal pointwise). Capping only lowers the walk, so P(τ > k) ≤ P(τ' > k). Pathwise, T_n = ∑_{k<n} 1[S'_1..S'_k ≤ 0]·ξ'_k ≤ c, by induction with the invariant (on {S'_1..S'_n ≤ 0}, T_n = S'_n ≤ 0). Each term factorizes, E[1_{A_k} ξ'_k] = P(A_k) E ξ'_0, because A_k depends only on the first k steps. So E min(ξ,c) · ∑_{k<n} P(τ' > k) ≤ c, and the partial sums are bounded. In Lean the factorization is cleanest as a lemma ∫ Φ(trunc k X)·Ψ(shift k X) = ∫ Φ(trunc k X) · ∫ Ψ(X), proved from indep_iSup_of_disjoint on the past and future σ-algebras.