Probability

Motivation

A Russian option is a perpetual American-type claim that pays, when the holder exercises at time $\tau$, the maximum of the asset price seen so far, discounted by $e^{-\alpha\tau}$. It was introduced by Shepp and Shiryaev for the Black–Scholes market (Shepp–Shiryaev 1993), where the underlying log-price is a Brownian motion with drift. Empirical work on asset returns (skewness, heavy tails, downward jumps) motivates replacing the Brownian motion by a Lévy process with negative jumps only. Avram, Kyprianou and Pistorius (2004) solve the Russian optimal stopping problem in that model in closed form, in terms of the scale functions of the process.

Timeline. 1993: Shepp and Shiryaev solve the Russian problem for geometric Brownian motion; Duffie and Harrison give its no-arbitrage price. Graversen and Peskir, and Kyprianou and Pistorius, treat further variants within the Black–Scholes market (the works the paper cites in §6). 2004: Avram, Kyprianou and Pistorius solve it for every spectrally negative Lévy process, covering both unbounded and bounded variation, using the exit problem of the reflected process $Y=\overline X-X$ (their Theorem 1, the subject of the first mission of this series).

Setting

Let $(\Omega,\mathcal F,\mathbf F=\{\mathcal F_t\}_{t\ge0},\mathbb P)$ be a filtered probability space with a right-continuous filtration, and $X=\{X_t,\ t\ge0\}$ a spectrally negative Lévy process for $\mathbf F$: $X_0=0$, càdlàg paths with no positive jumps, independent and stationary increments with $X_{s+t}-X_s$ independent of $\mathcal F_s$, and paths that are not monotone. The standing assumption of the paper is that $X$ has unbounded variation, or bounded variation and a Lévy measure absolutely continuous with respect to Lebesgue measure.

The Laplace exponent is $\psi(\theta)=\log\mathbb E[e^{\theta X_1}]$, and $\Phi(q)$ is the largest root of $\psi(\theta)=q$. For $q\ge0$ the $q$-scale function $W^{(q)}:\mathbb R\to[0,\infty)$ is the unique function that vanishes on $(-\infty,0]$, is continuous on $(0,\infty)$, and satisfies $\int_0^\infty e^{-\theta x}W^{(q)}(x)\,dx=(\psi(\theta)-q)^{-1}$ for $\theta>\Phi(q)$. Then $Z^{(q)}(x)=1+q\int_{-\infty}^xW^{(q)}(z)\,dz$. The tilted scale functions $W_v^{(p)}$ are those of the exponent $\psi_v(\theta)=\psi(\theta+v)-\psi(v)$.

Fix $r\ge0$ with $\psi(1)=r$ (the risk-neutral condition), and let $\mathbb P^1$ be the Esscher measure, $d\mathbb P^1/d\mathbb P|_{\mathcal F_t}=e^{X_t-rt}$. For $z\ge0$, under $\mathbb P^1_{-z}$ the process starts at $-z$ with running maximum $\overline X_t=\max\{0,\sup_{u\le t}X_u\}$, and the reflected process $Y=\overline X-X$ starts at $Y_0=z$. The passage time is $\tau_k=\inf\{t\ge0:Y_t\notin[0,k)\}$. Fix $\alpha>0$ and put $q=\alpha+r$.

The Russian optimal stopping problem (28) is

$$w^R(z)=\sup_\tau\ \mathbb E^1_{-z}\big[e^{-\alpha\tau+Y_\tau}\big],$$

the supremum over all $\mathbb P^1$-almost surely finite $\mathbf F$-stopping times. The option price is $V_r(M_0,S_0)=S_0\,w^R(\log(M_0/S_0))$.

Formalization targets

Goal: Theorem 2

With the optimal level (30) and the candidate value

$$\kappa^*=\inf\{x:\ Z^{(q)}(x)\le qW^{(q)}(x)\},\qquad u(z)=e^zZ^{(q)}(\kappa^*-z),$$

for every $z\ge0$,

$$w^R(z)=u(z)=\mathbb E^1_{-z}\big[e^{-\alpha\tau_{\kappa^*}+Y_{\tau_{\kappa^*}}}\big],$$

and $\tau_{\kappa^*}$ is a $\mathbb P^1$-a.s. finite $\mathbf F$-stopping time.

Milestones

1. Remark 4: $W^{(u)}(x)=e^{vx}W_v^{(u-\psi(v))}(x)$.
2. Lemma 1: $Z^{(q)}(x)/W^{(q)}(x)\to q/\Phi(q)$ as $x\to\infty$ (for $q\ge0$, with the paper's convention for $0/\Phi(0)$).
3. Remark 3: $W_v(0+)=0$ if and only if $X$ has unbounded variation.
4. Corollary 1, (29): the value of stopping at $\tau_k$,

$$\mathbb E^1_{-z}\big(e^{-\alpha\tau_k+Y_{\tau_k}}\big)=e^z\Big(Z^{(q)}(k-z)+\frac{Z^{(q)}(k)-qW^{(q)}(k)}{W^{(q)\prime}(k)-W^{(q)}(k)}W^{(q)}(k-z)\Big).$$

5. Lemma 2 (i): for $q>r$, $f=Z^{(q)}-qW^{(q)}$ decreases on $[0,\infty)$ to $-\infty$.
6. Lemma 2 (ii): $\kappa^*=0$ if $W^{(q)}(0+)\ge q^{-1}$; otherwise $\kappa^*>0$ is the unique root of $f$.
7. The stopped process $e^{-\alpha(t\wedge\tau_{\kappa^*})}u(Y_{t\wedge\tau_{\kappa^*}})$ is a $\mathbb P^1$-martingale.
8. $\mathbb E^1_{-z}[e^{-\alpha t+Y_t}Z^{(q)}(\kappa^*-Y_t)]\le e^zZ^{(q)}(\kappa^*-z)$.
9. $e^{-\alpha t}u(Y_t)$ is a $\mathbb P^1$-supermartingale.

Significance

The result. Theorem 2 gives the price of the perpetual Russian option and its optimal exercise rule for every exponential spectrally negative Lévy market. The rule is to exercise when the ratio of the running maximum to the current price first reaches $e^{\kappa^*}$. The level is explicit through scale functions, and it separates the regimes: for bounded variation with $W^{(q)}(0+)\ge q^{-1}$, immediate exercise is optimal. The theorem is the model case of a general method: an optimal stopping problem for a functional of $(X,\overline X)$ is reduced, by a change of measure, to one for the reflected process, and solved by verification. The same method underlies the Canadized Russian option (third mission of the series).

Formalizing it. The result is proved in the paper; it has no machine-checked proof. This mission produces a Lean statement of the full verification theorem, including admissibility of $\tau_{\kappa^*}$. It also states the analytic facts about scale functions that the proof relies on (Lemmas 1, 2 and Remarks 3, 4), which apply to any problem phrased in scale functions.

Difficulty

The obvious route is the classical verification: show that $e^{-\alpha t}u(Y_t)$ is a supermartingale, apply optional stopping, and check equality at $\tau_{\kappa^*}$. The first step fails as a direct Itô computation. In the unbounded-variation case $u$ is only $C^1$ at $\kappa^*$, and in the bounded-variation case only continuous there. The generator of $Y$ is nonlocal, so smoothness away from $\kappa^*$ does not control the jump part of the process across the boundary. The equality case needs the exact value of stopping at $\tau_k$ (Corollary 1). That value requires the overshoot of $Y$ over $k$, which is caused by a downward jump of $X$, and the exit problem of the reflected process. Finally, $\mathbb P^1$ is not equivalent to $\mathbb P$ on $\mathcal F_\infty$, so passing from $\mathbb P$-facts to $\mathbb P^1$-facts is valid only on each $\mathcal F_t$.

Formalization scope

Conventions committed to in Lean:

• Time is $[0,\infty)$ (ℝ≥0) and values are real. Random times take values in $[0,\infty]$ (WithTop ℝ≥0), and the payoff is set to $0$ on $\{\tau=\infty\}$, a $\mathbb P^1$-null event for admissible $\tau$.
• The spectrally negative Lévy process is a structure: measurable marginals, $X_0=0$, independent increments, stationary increments, càdlàg paths, no positive jumps, not almost surely monotone. Paths start at $0$, are càdlàg, and have no positive jumps for every $\omega$, not merely almost surely. Adaptedness, independence of increments from the past, and right-continuity of $\mathbf F$ are added for the filtered version.
• "The usual conditions" are read as right-continuity only; completeness is not imposed. $\mathbb P^1$ is typically singular to $\mathbb P$ on $\mathcal F_\infty$, so a complete $\mathcal F_0$ would contradict (3).
• "Unbounded variation" means "not almost surely of bounded variation on compacts". Condition (AC) is stated through jumps: no jump lands in a Lebesgue-null set, almost surely. The standing assumption is "bounded variation implies (AC)".
• $\psi$ is Mathlib's cumulant generating function; "$\psi(v)<\infty$" is integrability of $e^{vX_1}$.
• $W^{(q)}$ is a definite description (choice among functions with the properties of Definition 2) for $q\ge0$, and the series (5) for $q<0$. $Z^{(q)}$ integrates over $(-\infty,x]$.
• $\mathbb P^1$ is data (a probability measure $\mathbb Q$) with $\mathbb Q|_{\mathcal F_t}=e^{X_t-rt}\cdot\mathbb P|_{\mathcal F_t}$ for all $t$. $\mathbb P^1_{-z}$ is encoded by the reflected process with prior maximum $0$ and starting point $-z$.
• The value function is a supremum in $[0,\infty]$ of lower Lebesgue integrals. Expectation identities (Corollary 1, the display on p. 230) are stated in $[0,\infty]$ and thereby assert finiteness.
• $W^{(q)}(0+)$ is Function.rightLim, and $\kappa^*$ is the real infimum (30); its nonemptiness is Lemma 2, not a hypothesis. $\tau_0=0$ extends the paper's $\tau_k$, $k>0$.
• Readings of informal words: "decreases monotonically" is strict decrease on $[0,\infty)$; "the unique root" is on $[0,\infty)$; Lemma 1 is formalized for $q\ge0$, with $0/\Phi(0)$ read as $\lim_{\theta\downarrow0}\theta/\Phi(\theta)$ as the paper stipulates; Remarks 3 and 4 for real $q$, $u$ only. The p. 230 martingale, bound and supermartingale claims are stated under the standing assumption, covering all three cases of the proof.

A trivializing formalization is ruled out: the supremum ranges over every $\mathbb P^1$-a.s. finite stopping time of the given filtration (not only passage times, not a smaller filtration), and it is taken in $[0,\infty]$, where no junk value of an unbounded real supremum can occur.

Infrastructure a complete development needs: Lévy processes on path space, their Laplace exponents and Esscher transforms, scale functions (existence, uniqueness, smoothness under the standing assumption), the reflected process and the exit identity of Theorem 1, optional stopping for continuous-time supermartingales, and Itô/change-of-variables formulas for semimartingales with jumps. The scale-function and Esscher layers are reusable for the other missions of this series and for any fluctuation-theory problem. Contributions to any of these layers, or to the milestones separately, are welcome.

Selected references

• F. Avram, A. E. Kyprianou, M. R. Pistorius, Exit problems for spectrally negative Lévy processes and applications to (Canadized) Russian options, Ann. Appl. Probab. 14(1), 215–238, 2004. https://doi.org/10.1214/aoap/1075828052
• L. Shepp, A. N. Shiryaev, The Russian option: reduced regret, Ann. Appl. Probab. 3(3), 631–640, 1993. https://doi.org/10.1214/aoap/1177005715
• J. Bertoin, Lévy Processes, Cambridge Tracts in Mathematics 121, Cambridge University Press, 1996. ISBN 0-521-56243-0
• A. E. Kyprianou, Fluctuations of Lévy Processes with Applications, 2nd ed., Springer, 2014. https://doi.org/10.1007/978-3-642-37632-0

Motivation

Stochastic approximation is the family of recursive algorithms that locate a zero of a vector field $h$ from noisy evaluations of it. Temporal-difference learning, Q-learning, actor–critic methods and stochastic gradient descent are all instances. In practice these algorithms are often run with a constant or bounded, non-vanishing stepsize: the iterate keeps adapting to new data and never freezes, at the price of never converging exactly. The natural question for such a scheme is quantitative: how far from the target does the iterate stay in the long run, and how does that distance scale with the stepsize?

Borkar and Meyn (SIAM J. Control Optim. 38(2), 2000) answer both halves of the question under one set of hypotheses. First, stability of a "fluid" ODE obtained by scaling $h$ at infinity implies that the iterates have bounded second moments, with no a priori boundedness or projection assumption. Second, if the ODE $\dot x = h(x)$ has a globally exponentially stable equilibrium $x^*$, the asymptotic mean-square error is of the order of the largest stepsize. The first result replaced the usual stochastic-Lyapunov-function verification in reinforcement-learning applications (Section 3 of the paper). This mission formalizes the bounded-stepsize branch of the paper. A companion mission (… I: Stability and Almost-Sure Convergence under Tapering Stepsizes) covers the vanishing-stepsize branch.

Setting

Fix $d \ge 1$ and a Lipschitz vector field $h : \mathbb{R}^d \to \mathbb{R}^d$. The stochastic approximation recursion (1.1) is

$$X(n+1) = X(n) + a(n)\big[h(X(n)) + M(n+1)\big], \qquad n \ge 0,$$

with a deterministic step sequence $\{a(n)\}$ and a noise sequence $\{M(n)\}$ on a probability space $(\Omega, \mathcal F, \mathsf P)$. The associated ODE (1.2) is $\dot x = h(x)$.

• The scaled fields are $h_r(x) = r^{-1} h(rx)$. Assumption (A1) asks that $h$ be Lipschitz, that $h_r(x) \to h_\infty(x)$ for every $x$ as $r \to \infty$, and that the origin be an asymptotically stable equilibrium of the fluid ODE $\dot x = h_\infty(x)$.
• Let $\mathcal F_n = \sigma(X(0), \dots, X(n))$. Assumption (A2) asks that $\{M(n)\}$ be a martingale difference sequence, $\mathsf E[M(n+1) \mid \mathcal F_n] = 0$, with conditional second moments $\mathsf E[\|M(n+1)\|^2 \mid \mathcal F_n] \le C_0(1 + \|X(n)\|^2)$ for a constant $C_0$.
• Assumption (BS), bounded stepsizes: $0 < \underline\alpha \le a(n) \le \bar\alpha < 1$ for all $n$, with $\underline\alpha < \bar\alpha$.
• The error (2.2) is $e(n) = \|X(n) - x^*\|$.

An equilibrium $x^*$ of (1.2) is globally asymptotically stable if it is Lyapunov stable and attracts every solution. It is globally exponentially asymptotically stable if there are $b$ and $\delta > 0$ with $\|x(t) - x^*\| \le b\,e^{-\delta t}\|x(0) - x^*\|$ for every solution.

The proofs compare the iterates with ODE solutions on a time grid: $t(n) = \sum_{i<n} a(i)$, blocks $T(j) = t(m(j))$ of length about $T$, the interpolated path $\psi$ of the iterates, its rescaled version $\phi_j = \psi/r(j)$ with $r(j) = \max(1, \|X(m(j))\|)$, and the ODE solutions $\hat\psi$, $\hat\phi_j$ restarted at each block.

Formalization targets

Goal: Theorem 2.3(ii)

Under (A1), (A2) and (BS), if $x^*$ is a globally asymptotically and globally exponentially asymptotically stable equilibrium of (1.2), there are $\alpha^* > 0$ and $b_2 < \infty$ such that for all $0 < \bar\alpha \le \alpha^*$ and every initial condition $X(0)$,

$$\limsup_{n \to \infty} \mathsf E\big[e(n)^2\big] \le b_2\, \bar\alpha .$$

The constant $b_2$ is uniform in the stepsizes and in $X(0)$. No rate constant is fixed: only the linear dependence on $\bar\alpha$ is asserted.

Milestones

1. Lemma 4.7. For fixed $T > 0$ there is $C_2$, independent of the stepsizes, with $\mathsf E[\|\phi_j(t) - \hat\phi_j(t)\|^2 \mid \mathcal F_{m(j)}] \le C_2\bar\alpha$ and $\mathsf E[\|\phi_j(t)\|^2 \mid \mathcal F_{m(j)}] \le C_2$ on every block.
2. Theorem 2.1(ii). There are $\alpha^* > 0$ and $C_1$ with $\limsup_n \mathsf E\|X(n)\|^2 \le C_1$ whenever $\bar\alpha < \alpha^*$.
3. Lemma 4.8. For $\bar\alpha \le \alpha^*$, $\sup_{t \ge 0} \mathsf E\|\hat\psi(t) - \psi(t)\|^2 \le C_3 \bar\alpha$.

Significance

The result. Theorem 2.1(ii) says that a stability property of a deterministic ODE at infinity controls a stochastic recursion in mean square, uniformly over initial conditions. Theorem 2.3(ii) turns this into an error bound: with a non-vanishing stepsize the iterate does not converge, but its mean-square distance from $x^*$ is eventually $O(\bar\alpha)$. This is the quantitative justification for constant-stepsize stochastic approximation in reinforcement learning and adaptive control, and it is the starting point of the trade-off between bias (small stepsize) and speed (large stepsize) discussed in Section 2.2 of the paper.

Formalizing it. The results are proved in the paper, partly by sketch: Lemma 4.8's proof refers to "familiar arguments using the Bellman–Gronwall lemma", and the paper writes several bounds as $O(\bar\alpha)$. A formal proof makes every constant and its dependence explicit, which the paper's quantifier order leaves partly implicit (see the scope section). No machine-checked proof of these results, or of any stochastic-approximation stability theorem in this generality, is known to exist.

Difficulty

The natural first argument, that the iterates track the ODE and the ODE converges, needs the iterates to be bounded. Bounded iterates are exactly what is being proved, so the argument is circular. The paper breaks the circularity by rescaling: on each block the iterate is divided by $r(j)$, so that on large scales it tracks the fluid ODE, whose stability contracts the norm by a fixed factor per block. Making this work in mean square requires conditional second-moment estimates that are uniform in the stepsize and the scale (Lemma 4.7). A second difficulty is that the stepsize does not vanish: the tracking error per block does not go to zero, and the goal's content is precisely that it is of order $\bar\alpha$ with a constant that does not depend on $\bar\alpha$.

Formalization scope

• The state space is EuclideanSpace ℝ (Fin d). ODE solutions are forward solutions: continuous on $[0,\infty)$ with right derivatives. Stability notions are the standard ones, with exponential stability in the form the proof of Theorem 2.3(ii) uses.
• The filtration is the natural filtration of the iterates. (A2) includes integrability of $M(n+1)$ and $\|M(n+1)\|^2$ so that the conditional expectations are meaningful. Each theorem quantifies over every probability space, every measurable process satisfying (1.1) and (A2), and every deterministic $X(0)$.
• Second moments, suprema and $\limsup$ are computed in $[0,\infty]$, so a bound is a genuine finiteness claim.
• Constant placement. $\alpha^*$, $C_1$ and $b_2$ depend only on $h$, $h_\infty$, $C_0$ (and $x^*$). $C_2$ depends in addition on $T$, and $C_3$ on $T$ and $X(0)$. None depends on the stepsizes. Theorem 2.3's page text puts $b_2$ after $\alpha$. Read literally, that would allow $b_2 = C_1/\bar\alpha$ and make the goal a restatement of Theorem 2.1(ii). The formal goal fixes $b_2$ before the stepsizes and the initial condition, as the proof ($16C_3\bar\alpha$) gives. $\alpha^*$ is existential in Theorem 2.3(ii) and Lemma 4.8 rather than tied to Theorem 2.1(ii)'s witness.
• The proof objects $\hat\psi$, $\hat\phi_j$ are characterized by predicates (initial value, continuity, ODE on the block). Lemmas 4.7 and 4.8 hold for every function satisfying them.
• Not included: Theorem 2.3(i) (its proof chooses a radius depending on $\bar\alpha$), Theorem 2.4 and the Markov-chain results of Section 4.3, and the asynchronous extension (Theorem 2.5). The deterministic ODE lemmas 4.1–4.4 belong to the companion mission.

Useful infrastructure, reusable beyond this mission: Bellman–Gronwall inequalities in discrete time (Lemma 4.3 of the paper), stability of scaled ODEs, and conditional second-moment estimates for martingale-difference-driven recursions. Contributions of any of these as separate lemmas are welcome.

Selected references

• V. S. Borkar and S. P. Meyn, The O.D.E. Method for Convergence of Stochastic Approximation and Reinforcement Learning, SIAM J. Control Optim. 38(2):447–469, 2000. https://doi.org/10.1137/S0363012997331639
• M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Math. 1709, Springer, 1999. https://doi.org/10.1007/BFb0096509
• H. J. Kushner and G. G. Yin, Stochastic Approximation and Recursive Algorithms and Applications, 2nd ed., Springer, 2003. https://doi.org/10.1007/b97441

Dividends, ruin and bail-out loans

An insurance company's surplus in the Cramér–Lundberg model grows linearly with premiums and falls by claims arriving as a compound Poisson process. When premium income exceeds the expected claims, the surplus drifts to infinity. De Finetti (1957) proposed that the surplus above a barrier should instead be paid to shareholders as dividends, and the resulting optimal dividend problem — maximize the expected discounted dividends — is a central problem of risk theory. A barrier policy, however, drives the surplus below zero with probability one. Harrison and Taylor (1978) and Løkka and Zervos studied, for Brownian motion, a variant with bail-out loans: ruin is forbidden, and the shareholders must inject capital whenever the surplus would become negative, at a cost $\varphi>1$ per unit.

Avram, Palmowski and Pistorius (Ann. Appl. Probab. 17 (2007)) solved the bail-out problem when the surplus is a general spectrally negative Lévy process, which includes the Cramér–Lundberg model, Brownian motion with drift and their sums. They showed that the optimal policy is a double barrier policy for every initial capital. This mission formalizes that result, Theorem 3 of the paper.

Timeline:

• 1957 — de Finetti introduces dividend barriers.
• 1978 — Harrison and Taylor: optimal control of a Brownian storage system with two reflecting barriers.
• 1995 — Jeanblanc and Shiryaev: optimal dividends for Brownian motion with drift.
• 2004 — Avram, Kyprianou and Pistorius: exit problems for spectrally negative Lévy processes reflected at their infimum and supremum, in terms of scale functions.
• 2007 — Avram, Palmowski and Pistorius: Theorems 1 and 3 of the present paper; Pistorius' pathwise construction of the doubly reflected process is used.

Setting

A spectrally negative Lévy process $X=\{X_t\}_{t\ge0}$ on a filtered probability space $(\Omega,\mathcal F,\mathbb F,P)$ starts at $X_0=0$, has càdlàg paths, is $\mathbb F$-adapted, and has stationary increments with $X_t-X_s$ independent of $\mathcal F_s$. Its jumps are all negative, and $E[e^{\theta X_t}]=e^{t\psi(\theta)}$ for $\theta\ge0$, where the Laplace exponent is

$$\psi(\theta)=c\theta+\tfrac{\sigma^2}{2}\theta^2+\int_{(-\infty,0)}(e^{\theta y}-1-\theta y\mathbf 1_{\{|y|<1\}})\,\nu(dy).$$

With initial capital $x\ge0$ the surplus is $x+X$. The standing assumptions are: $X$ does not have monotone paths; $E[X_1]>-\infty$ (so $\psi'(0+)=E[X_1]$ is finite); $\sigma>0$, or $\int_{(-1,0)}|y|\nu(dy)=\infty$, or $\nu$ has a density (condition (3.3)).

A policy $\bar\pi=(L,R)$ consists of nondecreasing adapted processes with $L_0=R_0=0$: cumulative dividends $L$ (left-continuous) and cumulative injected capital $R$ (right-continuous). The controlled surplus is $V_t=x+X_t-L_t+R_t$. The policy is admissible if $V_t\ge0$ for $t>0$ and $\int_0^\infty e^{-qt}dR_t<\infty$ almost surely. Its value and the value function are

$$\bar v_{\bar\pi}(x)=E\Bigl[\int_0^\infty e^{-qt}dL_t-\varphi\int_0^\infty e^{-qt}dR_t\Bigr],\qquad \bar v_*(x)=\sup_{\bar\pi\ \text{admissible}}\bar v_{\bar\pi}(x),$$

with discount rate $q>0$ and cost $\varphi>1$. The double-barrier strategy $\bar\pi_{0,a}$ pays out $(x-a)^+$ at once and then the minimal dividends and injections that keep $V$ in $[0,a]$: $dL$ is carried by $\{V=a\}$ and $dR$ by $\{V=0\}$.

The $q$-scale function $W=W^{(q)}$ vanishes on $(-\infty,0)$, is continuous and nondecreasing on $[0,\infty)$, and satisfies $\int_0^\infty e^{-\theta y}W(y)dy=1/(\psi(\theta)-q)$ for $\theta>\Phi(q)$, the largest root of $\psi=q$. Set $\overline W(y)=\int_0^yW$, $Z=1+q\overline W$, $\overline Z(y)=\int_0^yZ$. The candidate value of $\bar\pi_{0,a}$ is

$$\bar v_a(x)=\varphi\bigl(\overline Z(x)+\psi'(0+)/q\bigr)+Z(x)\frac{1-\varphi Z(a)}{qW(a)}\quad(0\le x\le a),\qquad \bar v_a(x)=x-a+\bar v_a(a)\quad(x>a),$$

and the barrier level is $d^*=\inf\{a>0:[\varphi Z(a)-1]W'(a)-\varphi qW(a)^2\le0\}$, with $\inf\emptyset=\infty$.

Formalization targets

Goal: Theorem 3

$$d^*<\infty,\qquad \bar v_*(x)=\bar v_{d^*}(x)\ \ (x\ge0),\qquad \bar\pi_{0,d^*}\ \text{exists, is admissible and attains }\bar v_*(x).$$

Milestones

• Lemma 1: $\overline W(y)/\overline W(a)\le W(y)/W(a)$ for $0\le y\le a$.
• Proposition 2, (3.17): the expected discounted undershoot $E_x[e^{-qT_0^-}X_{T_0^-}]$ in closed form.
• Theorem 1: the expected discounted dividends and injections of $\bar\pi_{0,a}$, $a>0$, in closed form; hence $\bar v_{\bar\pi_{0,a}}=\bar v_a$.
• Lemma 2(ii): $d^*=0$ if and only if $\sigma=0$ and $\nu(-\infty,0)\le q/(\varphi-1)$.
• Proposition 3(ii): $d^*<\infty$ and $\bar v_a\le\bar v_{d^*}$ for all levels $a$.
• Lemma 3(ii)–(iv): $1\le\bar v_{d^*}'\le\varphi$ with boundary slopes; $a\mapsto\bar v_a(x)$ nonincreasing for $a>d^*$; $\bar v_{d^*}$ concave.
• Lemma 5: $(\Gamma\bar v_{d^*}-q\bar v_{d^*})\le0$ on $(0,\infty)$, with equality on $(0,d^*)$.
• Proposition 4(ii): any $C^2$ solution of the variational inequality (5.9) dominates $\bar v_*$.

Significance

Theorem 3 answers the bail-out problem completely: for every initial capital and every spectrally negative Lévy surplus, the optimal policy is a double barrier with an explicit level and an explicit value in terms of scale functions. In the classical problem without injections (Theorem 2 of the same paper) the analogous conclusion needs an extra generator condition, and Azcue and Muler exhibited Cramér–Lundberg models where barrier policies are not optimal. The result is the basis of later work on dividends with capital injection, transaction costs and Parisian ruin.

The result has a published proof. What this mission adds is a machine-checked version. As far as is known, no part of the theory used — Lévy processes, scale functions, doubly reflected processes, the generator of a Lévy process, singular stochastic control — has been formalized in Lean's Mathlib.

Difficulty

The value function is a supremum over all adapted singular controls. Its upper bound requires a verification argument: Itô's formula for $e^{-qt}w(V_t)$ with a semimartingale $V$ that has jumps, a controlled bounded-variation part and a possibly nonzero continuous martingale part, followed by localization and limits. A function that satisfies the variational inequality only in the viscosity sense is not enough, so the candidate $\bar v_{d^*}$ must be shown to be regular enough and to satisfy $\Gamma\bar v_{d^*}-q\bar v_{d^*}\le0$ everywhere on $(0,\infty)$. Above the barrier this inequality does not follow from a martingale property: the paper derives it from concavity and a comparison with higher barriers, through the resolvent of the doubly reflected process. The lower bound requires the existence and value of the doubly reflected process, and computing that value needs fluctuation identities (two-sided exit, overshoot) that are themselves theorems about scale functions.

Formalization scope

Time is indexed by $\mathbb R_{\ge0}$. The process is a structure carrying the triplet $(c,\sigma,\nu)$, the paths, adaptedness, independence of future increments from $\mathcal F_s$, stationarity, the Laplace-exponent identity, and the usual conditions on the filtration. $P_x$ is the law of $x+X$. Policy values are computed as $E[\int e^{-qt}dL]-\varphi E[\int e^{-qt}dR]$ in the extended reals from two $[0,\infty]$-valued expectations, and the value function is a supremum in the extended reals; a policy with both expectations infinite gets $-\infty$. Stieltjes integrals include the jump at time $0$. The scale function is a hypothesis IsScaleFunction (it is unique), and $d^*$ lives in $[0,\infty]$, so an empty defining set gives $\infty$. The double-barrier strategy is characterized by the two-sided Skorokhod conditions plus mutual singularity of $dL$ and $dR$, which pins the level-$0$ policy of bounded-variation processes. These conditions hold almost surely, and they are stated on the post-decision surplus $V_{t+}=x+X_t-L_{t+}+R_t$: $dL$ is carried by $\{V_{t+}=a\}$ and $dR$ by $\{V_{t+}=0\}$. This is the paper's "minimal amount" (p. 4) and matches its construction on pp. 10–11. The closure-of-support wording of (4.2) on its own would also admit non-minimal lump dividends. Admissibility, $V_t\ge0$ for $t>0$ together with (2.3), is likewise required almost surely.

Printed slips corrected (milestone texts are verbatim):

• Theorem 3 and Proposition 3(ii) print "$\psi'(0+)<\infty$", which always holds; the intended $\psi'(0+)>-\infty$ is used.
• (3.3) prints $\int_{-1}^0x\,\nu(dx)=\infty$ for $\int_{(-1,0)}|x|\,\nu(dx)=\infty$.
• (3.4) prints $e^{-\theta x}$ in a $dy$-integral.
• p. 20 prints the extension $\bar v_{d^*}(x)+\varphi x$ for $\bar v_{d^*}(0)+\varphi x$.
• Lemma 3(iv) is printed for every $a>0$ but proved and used only for $a=d^*$, and is stated for $a=d^*$.
• Proposition 3(ii) at $a=0$ is stated only for bounded variation, where $\bar v_0$ is defined.

The goal cannot be satisfied trivially. It asserts equality of the value function with $\bar v_{d^*}$, not only an inequality. Existence of the optimal policy is part of the conclusion. Generator statements carry integrability of the jump integrand, so a non-integrable integrand cannot make them true with the junk value $0$.

A complete development needs Lévy processes and their Laplace exponents, scale functions, first-passage and two-sided exit identities, reflected and doubly reflected processes, Itô's formula for semimartingales with jumps, and a verification theorem for singular control. All of these are reusable well beyond this mission. Contributions of any of these foundations are welcome, as are proofs of the analytic milestones (Lemma 3, Proposition 3(ii)) from the scale-function properties.

Selected references

• F. Avram, Z. Palmowski, M. R. Pistorius, On the optimal dividend problem for a spectrally negative Lévy process, Ann. Appl. Probab. 17 (2007) 156–180. https://arxiv.org/abs/math/0702893
• F. Avram, A. E. Kyprianou, M. R. Pistorius, Exit problems for spectrally negative Lévy processes and applications to (Canadized) Russian options, Ann. Appl. Probab. 14 (2004) 215–238. https://doi.org/10.1214/aoap/1075828052
• M. R. Pistorius, On doubly reflected completely asymmetric Lévy processes, Stochastic Process. Appl. 107 (2003) 131–143. https://doi.org/10.1016/S0304-4149(03)00065-9
• J. M. Harrison, A. J. Taylor, Optimal control of a Brownian storage system, Stochastic Process. Appl. 6 (1978) 179–194. https://doi.org/10.1016/0304-4149(78)90059-5
• A. E. Kyprianou, Introductory Lectures on Fluctuations of Lévy Processes with Applications, Springer, 2006. https://doi.org/10.1007/978-3-540-31343-4

Motivation

Small and medium-sized suppliers that sell to large retailers typically ship first and are paid weeks or months later. Until the invoice is paid, the supplier's cash is trapped in accounts receivable, while production has to be financed up front. Factoring (selling or pledging the receivable to a financial intermediary for immediate cash) and reverse factoring (a buyer-initiated program in which the retailer approves the invoice and the supplier is paid early by the retailer's bank) are the standard remedies, and reverse factoring programs of large buyers are often coupled with an extension of payment terms. Which of these instruments a supplier should use, and how the answer depends on the credit ratings of the two firms, is the question addressed by Kouvelis and Xu, "A Supply Chain Theory of Factoring and Reverse Factoring", Management Science 67(10):6071–6088, 2021 (doi:10.1287/mnsc.2020.3788). The paper embeds each financing scheme in the pull wholesale-price game of Cachon (2004) and compares the resulting equilibria.

Setting

A retailer (the Stackelberg leader) offers a wholesale price $w$ to a capital-constrained supplier (the follower), who then chooses a production quantity $q \ge 0$ and carries the inventory; the retail price $p$ is fixed, and $0 < c < p$ is the unit production cost. Demand $D \ge 0$ has density $f$, complementary distribution function $\bar F$, finite mean, $f > 0$ on $[0, \mathbb Z]$ ($\mathbb Z \le +\infty$), and a strictly increasing failure rate $z = f/\bar F$ (strict IFR). Expected sales are $S(q) = \int_0^q \bar F(\xi)\,d\xi$, and $k(q) = S(q)/\bar F(q)$.

Each firm $j \in \{s, r\}$ has a credit rating $C_j \in (C_{\min}, C_{\max})$. The default probability $\rho_j = \rho(C_j) \in [0,1]$ is strictly decreasing in the rating, and the interest-rate premium $\eta_j = \eta(C_j) > 0$ is decreasing. Production takes a lead time $t_1$, payment follows after a term $t_2$, and the supplier faces a Poisson liquidity shock of rate $\lambda_s$ during production (the retailer, rate $\lambda_r$). Under a scheme $i \in \{\mathcal F, \mathcal N, \mathcal R\}$ (recourse, non-recourse, reverse factoring, the last with a payment extension $\tau \ge 0$), the supplier's expected profit is

$$\pi_i(q; w) = (1-\rho_s)\big(\Lambda_i e^{-\lambda_s t_1} w S(q) - c q e^{\eta_s t_1}\big),$$

with coefficients $\Lambda_{\mathcal F} = (1-\rho_r) + (1-\rho_s) - e^{\eta_s t_2}$, $\Lambda_{\mathcal N} = e^{-\eta_r t_2}(1-\rho_r)$, $\Lambda_{\mathcal R} = e^{-\eta_r(t_2+\tau)}$, and effective unit cost $c_i = c\,e^{(\eta_s+\lambda_s)t_1}/\Lambda_i$. The retailer's profit is $e^{-\lambda_s t_1}(1-\rho_r)(p-w)S(q)$ under factoring and carries the extra factor $2 - e^{-\lambda_r \tau}$ under reverse factoring.

Formalization targets

Goal: Proposition 5

For a given $\tau \ge 0$, let $\mathbb C_3$ be the unique supplier rating with $\Lambda_{\mathcal F} = \Lambda_{\mathcal R}$, $\mathbb C_1$ the one with $\Lambda_{\mathcal F} = \Lambda_{\mathcal N}$, and $\mathbb C_{\mathcal F}, \mathbb C_{\mathcal N}, \mathbb C_{\mathcal R}$ the feasibility thresholds ($c_i = p$). With all three schemes available,

$$e^{-\eta_r\tau} < 1-\rho_r:\quad \mathcal F \text{ adopted} \iff C_s > \mathbb C_{\mathcal F}\vee\mathbb C_1,\qquad \mathcal N \text{ adopted} \iff \mathbb C_{\mathcal N} < C_s \le \mathbb C_1;$$ $$1-\rho_r \le e^{-\eta_r\tau}:\quad \mathcal F \text{ adopted} \iff C_s > \mathbb C_{\mathcal F}\vee\mathbb C_3,\qquad \mathcal R \text{ adopted} \iff \mathbb C_{\mathcal R} < C_s \le \mathbb C_3.$$

Milestones

1. Proposition 2 (p. 6078): recourse factoring is feasible iff $C_s > \mathbb C_{\mathcal F}$, and then the unique equilibrium solves $p\bar F(q) = c_{\mathcal F}[1+z(q)k(q)]$, $w = c_{\mathcal F}/\bar F(q)$.
2. Proposition 3 (p. 6079): the same for non-recourse factoring with $c_{\mathcal N}$.
3. §5.2 (p. 6082, Proposition EC.2): the same for reverse factoring with $c_{\mathcal R}(\tau)$.
4. §4.4 (p. 6080, Lemma EC.2): between feasible schemes, the supplier's equilibrium profits are ordered as the $\Lambda_i$.
5. Proposition 4 (p. 6080): the choice between $\mathcal F$ and $\mathcal N$ alone.

A follow-on item states Corollary 1(i) (p. 6081): when the retailer's rating is at least the supplier's, non-recourse factoring strictly dominates recourse factoring whenever the latter is feasible.

Significance

Proposition 5 is the paper's main prediction: non-recourse factoring is the choice of medium-rated suppliers, recourse factoring of highly rated ones, and reverse factoring with a fixed payment extension is chosen only by low-to-medium-rated suppliers and only if the retailer's rating is not too high relative to the extension. The paper uses it to explain the documented reluctance of suppliers to join reverse-factoring programs that come with extended payment terms (Wuttke, Rosenzweig and Heese 2019; Corsten 2010, a teaching case), and it is the starting point of the paper's Proposition 6 on the retailer's optimal payment extension, which is the subject of the second mission of this series.

The results are proved in the paper's Online Appendix B. To the best of available knowledge none of them, and no model of supply chain finance, has a machine-checked proof. A formal development would also supply a reusable treatment of the pull wholesale-price game under a strictly IFR demand with an arbitrary effective unit cost, of which Propositions 2, 3 and EC.2 are three instances.

Difficulty

The case analysis of Proposition 5 is short once the milestones are available; the substance lies in them. Proposition 2 requires solving a bilevel problem: the follower's best response has to be identified for every wholesale price, including prices at which the supplier produces nothing, and the leader's objective has to be shown to have a single maximizer. The natural route through the first-order condition needs the IFR property to exclude multiple stationary points, and it has to cope with a support end $\mathbb Z$ that may be finite (where $\bar F$ vanishes and $k$, $z$ lose meaning) or infinite. Lemma EC.2 requires the equilibrium supplier profit as an explicit function of the effective cost and a monotonicity argument for it; comparing the $\Lambda_i$ directly, without the equilibrium, does not prove it. The proofs themselves are not in the main text.

Formalization scope

Demand is a probability measure μ on ℝ with a density f, the support end Z : EReal, and the complementary distribution function Fbar μ x = μ((x, ∞)). The model data, the coefficients coef, the effective costs cF, cN, cR, the two profit functions, best responses, equilibria, feasibility and adoption are definitions; all theorems are for arbitrary data satisfying Params.Valid and DemandModel. Readings fixed by the formalization:

• "Feasible": some wholesale price $w \ge 0$ with a supplier best response gives the retailer strictly positive profit. It is not defined as $c_i < p$, which is what Propositions 2 and 3 prove.
• "Adopted" / "should be adopted": the scheme is feasible and its equilibrium supplier profit is best among the feasible available schemes, with ties resolved $\mathcal R \succ \mathcal N \succ \mathcal F$, the order forced by the paper's boundaries ($C_s = \mathbb C_1$, $C_s = \mathbb C_3$, $C_r = \mathbb C_2$). Profits are compared, not the $\Lambda_i$.
• "The unique value of $C_s$ that satisfies …": a point of $(C_{\min}, C_{\max})$ satisfying the equation and the only such point. The equation $c_{\mathcal F} = p$ is cross-multiplied, $c\,e^{(\eta_s+\lambda_s)t_1} = p\Lambda_{\mathcal F}$, since $\Lambda_{\mathcal F}$ may be $\le 0$.
• "$C_r > \mathbb C_2$" is read through the paper's equivalence $\tau > -\eta_r^{-1}\ln(1-\rho_r)$, i.e. $e^{-\eta_r\tau} < 1-\rho_r$: the stated assumptions give no single crossing in $C_r$.
• "The unique equilibrium can be derived from …": the equilibrium exists and is unique, and it is exactly the solution of the system with $q \in (0, \mathbb Z)$; this part is stated under feasibility.
• "Increasing/decreasing" is weak unless stated (p. 6075); $\rho$ is strictly decreasing, $\eta$ weakly.
• Continuity of $f$ is read on $[0,\mathbb Z]$, and $\mathbb Z$ as the upper end of the support.
• Additions: wholesale prices are nonnegative; the retailer's reverse-factoring profit is the last line of the p. 6082 display (the middle line has a stray factor $w$).
• Corollary 1(i): "higher credit rating" is read as $C_r \ge C_s$, "dominates" as a strictly larger equilibrium supplier profit whenever recourse is feasible.

A formalization in which feasibility or adoption is defined by the inequalities being proved ($c_i < p$, largest $\Lambda_i$) makes the propositions trivial and is ruled out by the definitions above. The profit functions (7), (10) and the p. 6082 display are taken as the model; the derivation from bank and factor pricing (Eqs. (1), (5), (6), Lemma 1) is not formalized, and the unstated assumptions of Table EC.2 are not included. Contributions of reusable lemmas on $S$, $k$ and $z$ under strict IFR are welcome.

Selected references

• P. Kouvelis and F. Xu, A Supply Chain Theory of Factoring and Reverse Factoring, Management Science 67(10):6071–6088, 2021. https://doi.org/10.1287/mnsc.2020.3788
• G. P. Cachon, The Allocation of Inventory Risk in a Supply Chain: Push, Pull, and Advance-Purchase Discount Contracts, Management Science 50(2):222–238, 2004. https://doi.org/10.1287/mnsc.1030.0189
• D. A. Wuttke, E. Rosenzweig, H. S. Heese, An Empirical Analysis of Supply Chain Finance Adoption, Journal of Operations Management 65(3):242–261, 2019.
• P. Kouvelis and W. Zhao, Who Should Finance the Supply Chain? Impact of Credit Ratings on Supply Chain Decisions, Manufacturing & Service Operations Management 20(1):19–35, 2018.

Motivation

The Collatz map sends an even positive integer $n$ to $n/2$ and an odd one to $3n+1$. The Collatz conjecture asserts that every orbit of this map eventually reaches $1$. It remains an open problem.

Because the conjecture is open, a large part of the literature proves weaker statements that hold for almost all starting values. These results bound how small an orbit gets, not whether it reaches $1$. They are the strongest unconditional evidence for the conjecture. Terence Tao's 2022 theorem is the strongest result of this type: outside a set of logarithmic density zero, every orbit drops below any prescribed function that tends to infinity, however slowly (Tao 2022).

Timeline

Attributions follow the survey in Tao 2022, Section 1. Here $\mathrm{Col}_{\min}(N)$ is the least value in the orbit of $N$.

• 1976 to 1979, Terras and Everett. $\mathrm{Col}_{\min}(N) < N$ for almost all $N$, in natural density.
• 1979, Allouche. $\mathrm{Col}_{\min}(N) < N^{\theta}$ for almost all $N$, for every $\theta > 0.869$.
• 1994, Korec. The same bound for every $\theta > \log 3/\log 4 \approx 0.7924$.
• 2019 preprint, 2022 publication, Tao. The power $N^{\theta}$ is replaced by any $f(N) \to \infty$, in logarithmic density instead of natural density (Forum of Mathematics, Pi 10, e12).
• 2026, ProofAtlas. A complete machine-checked proof of Tao's theorem in Lean 4 is published (formalization record).

Setting

Let $\mathrm{collatzStep} : \mathbb{N} \to \mathbb{N}$ be

$$\mathrm{collatzStep}(n) = \begin{cases} n/2 & n \text{ even},\\ 3n+1 & n \text{ odd}. \end{cases}$$

Write $\mathrm{collatzStep}^{[k]}$ for the $k$-fold iterate, with $\mathrm{collatzStep}^{[0]}(n) = n$. The orbit of $n$ is the set of values $\mathrm{collatzStep}^{[k]}(n)$ for $k \ge 0$. It includes $n$ itself.

The Syracuse map acts on odd integers. It sends an odd $n$ to the odd part of $3n+1$, which is $\mathrm{syracuseStep}(n) = (3n+1)/2^{\nu_2(3n+1)}$. The Syracuse orbit minimum $\mathrm{syracuseOrbitMin}(n)$ is the least value $\mathrm{syracuseStep}^{[k]}(n)$ over $k \ge 0$.

For a set $A$ of positive integers and a real cutoff $x \ge 2$, the logarithmic mass of $A$ up to $x$ is

$$\mathrm{weightedLogMassReal}(x) = \frac{1}{\log x} \sum_{\substack{1 \le n \le x \\ n \in A}} \frac{1}{n}.$$

A set of positive integers has logarithmic density $d$ when this quantity tends to $d$ as $x \to \infty$. Since $\sum_{n \le x} 1/n = \log x + O(1)$, all positive integers together have logarithmic density $1$, and the odd positive integers have logarithmic density $1/2$.

A function $f : \mathbb{N} \to \mathbb{R}$ tends to infinity on positive inputs when for every real $M$ there is an $N$ such that $f(n) > M$ for all $n \ge N$ with $n > 0$.

Formalization targets

Goal: Tao's Theorem 1.3

For every $f$ that tends to infinity on positive inputs,

$$\lim_{x \to \infty} \frac{1}{\log x} \sum_{\substack{1 \le n \le x \\ \exists k,\ \mathrm{collatzStep}^{[k]}(n) < f(n)}} \frac{1}{n} = 1.$$

This is the Lean theorem collatz_almost_bounded_logarithmic. It fixes no rate and no constant, so later improvements do not invalidate it.

Syracuse form: Tao's Theorem 1.6

For every $f$ that tends to infinity on odd positive inputs, the odd $n$ whose Syracuse orbit contains a value below $f(n)$ have logarithmic density $1/2$, which is all of the odd integers. This is syracuse_almost_bounded_logarithmic.

Quantitative form: Tao's Theorem 3.1

There are constants $C, c > 0$ such that for all real $M \ge 2$ and $x \ge 2$,

$$\frac{1}{\log x} \sum_{\substack{1 \le n \le x,\ n \text{ odd} \\ \mathrm{syracuseOrbitMin}(n) > M}} \frac{1}{n} \le \frac{C}{(\log M)^{c}}.$$

This is syracuse_uniform_logarithmic_tail_bound. The three targets are listed from weakest to strongest. In Tao's paper, the goal and Theorem 1.6 both follow from Theorem 3.1.

Significance

The result. Theorem 1.3 improves the earlier almost-all bounds on Collatz orbit minima from a power of $N$ to any function that tends to infinity. For example, $\mathrm{Col}_{\min}(N) < \log\log\log\log N$ for almost all $N$. The theorem does not settle the conjecture. A single divergent orbit or nontrivial cycle is not excluded, because its predecessors form a set with bounded orbit minima.

The formalization. The theorem is proved, and a complete formalization already exists. The ProofAtlas record Tao's Almost-Bounded Collatz Orbits proves the statement taoAlmostBoundedColMin_checked with the same step map and an orbit that includes its starting value. That package has 397 first-party Lean files and about 124,000 source lines. ProofAtlas records a passing build with no sorry and the axiom profile propext, Classical.choice, Quot.sound. The source is released under the Apache-2.0 licence at commit d53c8de00056fb05999e44589f2399d7efa026e4, with copyright held by Advameg, Inc. It was built with Lean v4.30.0-rc2.

The remaining work for this mission is therefore a port, not new mathematics. The existing Lean development must be moved to Lean v4.33.1 and Mathlib 0df444a, and then connected to the goal statement above.

Difficulty

The mathematical difficulty is already resolved in the existing proof. The classical first-descent argument shows that a typical orbit drops below its starting value. Repeating that argument fails, because after one descent the new value is no longer distributed like a random integer of its size, and the error compounds at each repetition. That is why earlier results stop at a power bound $N^{\theta}$.

The difficulty of this mission is engineering. The port moves a development of about 124,000 lines forward across three minor Lean releases and the corresponding Mathlib changes. Lemma renames, deprecations, and changes in tactic behaviour must be repaired file by file without changing any statement.

Formalization scope

• Step map. collatzStep n = if Even n then n / 2 else 3 * n + 1, so $\mathrm{collatzStep}(0) = 0$. This is the same definition as in the ProofAtlas source.
• Orbit. The witness $k$ ranges over all natural numbers, including $k = 0$.
• Density. The goal uses weightedLogMassReal: a real cutoff $x$, the natural indices $0 \le n \le \lfloor x \rfloor$, weights $1/n$, and normalization by $\log x$. The ProofAtlas statement instead uses integer cutoffs and normalization by the harmonic sum $\sum_{n \le N} 1/n$. A short bridge between the two normalizations is part of the required work.
• Threshold. The hypothesis on $f$ constrains only positive inputs. The value $f(0)$ is irrelevant.
• Non-triviality. The case $k = 0$ alone covers only inputs with $n < f(n)$. For slowly growing $f$ this set is finite, so the goal is not satisfied by the starting value.

The goal is already reduced, through accepted proofs, to the single open statement syracuse_uniform_logarithmic_tail_bound. Two routes therefore close the mission. The first is to port the ProofAtlas development and prove the goal directly through the density bridge. The second is to prove Theorem 3.1 in its stated form. Contributions welcome include ported modules as reusable solutions, the density bridge, and a proof of Theorem 3.1. Every ported file must keep the Apache-2.0 notice and attribution to the ProofAtlas source.

Selected references

• Terence Tao, Almost all orbits of the Collatz map attain almost bounded values, Forum of Mathematics, Pi 10 (2022), e12. https://doi.org/10.1017/fmp.2022.8 and https://arxiv.org/abs/1909.03562
• ProofAtlas, Tao's Almost-Bounded Collatz Orbits, Lean 4 formalization, source commit d53c8de00056fb05999e44589f2399d7efa026e4, Apache-2.0, 2026. https://proofatlas.ai/formalizations/tao-almost-bounded-orbits/
• Jeffrey C. Lagarias (editor), The Ultimate Challenge: The 3x+1 Problem, American Mathematical Society, 2010. https://bookstore.ams.org/MBK/78