Probability

Motivation

Model-based reinforcement learning algorithms for Markov decision processes estimate each transition distribution $P_{s,a}$ from the transitions they have observed out of the state–action pair $(s,a)$. Their regret analyses then need to know how far the empirical distribution $\hat p$ can be from the true one $p$. The standard tool is an $\ell_1$ bound on $\hat p-p$, as in UCRL2 (Jaksch, Ortner and Auer, 2010), which costs a factor of order $\sqrt S$ in the number of states $S$. What the analysis actually uses, however, is the deviation along one direction: the projection $(\hat p-p)^Th$ onto a bias (or value) vector $h$ whose entries differ by at most the MDP's diameter $D$.

S. Agrawal and R. Jia (arXiv:1705.07041v3, published in Mathematics of Operations Research, 2023, as Optimistic Posterior Sampling for Reinforcement Learning: Worst-Case Regret Bounds) prove a worst-case regret bound of order $\tilde O(D\sqrt{SAT})$ for an optimistic variant of posterior sampling. One ingredient of that analysis is their Proposition 5.2: a Bernstein-type bound on $(\hat p-p)^Th$ whose leading term is governed by a variance of $h$ under $p$, written in stick-breaking form. This mission formalizes that proposition and the steps of its proof.

Setting

Fix a number of states $S$ and order them $1,\dots,S$. A probability vector $p\in\Delta^S$ has $p_i\ge0$ and $\sum_ip_i=1$. A multinoulli trial with parameter $p$ is a random state $X$ with $\mathbb P(X=i)=p_i$. Draw $n$ independent trials $X_1,\dots,X_n$ and let

$$\hat p_i=\frac{\#\{t: X_t=i\}}{n}$$

be the empirical probability vector, the average of the one-hot outcomes. For $p$ and a vector $h\in\mathbb R^S$ define the stick-breaking quantities

$$\gamma_i=\frac{p_i(p_{i+1}+\cdots+p_S)}{p_i+\cdots+p_S},\qquad H_{i+1}=\frac{1}{\sum_{j=i+1}^Sp_j}\sum_{j=i+1}^Sh_jp_j,\qquad c_i=h_i-H_{i+1}.$$

Thus $H_{i+1}$ is the mean of $h$ under $p$ conditioned on the states after $i$, and $c_i$ compares $h_i$ with it. The sum $\sum_{i<S}\gamma_ic_i^2$ equals the variance of $h(X)$ for $X\sim p$. In Lean these objects are gammaCoef p i, Hnext p h i, cCoef p h i, phat ω i, the law of one trial is cat p and the law of $n$ trials is trialsLaw n p, all in the namespace OptimisticPSRL.Concentration.

Formalization targets

Goal: Proposition 5.2 (p. 9)

Let $h\in\mathbb R^S$ satisfy $|h_i-h_{i'}|\le D$ for all $i,i'$, let $n\ge96$ and $\rho\in(0,1)$. Then, with probability at least $1-\rho$,

$$\big|(\hat p-p)^Th\big|\le2\sqrt{\log(n/\rho)\sum_{i<S}\frac{\gamma_ic_i^2}{n}}+3D\,\frac{\log(2/\rho)}{n}.$$

Milestones

1. Fact 1 (p. 17), a deterministic identity: for probability vectors $\tilde p,\bar p$ with stick-breaking ratios $\tilde y_i=\tilde p_i/(\tilde p_i+\cdots+\tilde p_S)$ and $\bar y_i$,

$$(\tilde p-\bar p)^Th=\sum_i(\tilde y_i-\bar y_i)(h_i-\tilde H_{i+1})(\bar p_i+\cdots+\bar p_S)=\sum_i(\tilde y_i-\bar y_i)(h_i-\bar H_{i+1})(\tilde p_i+\cdots+\tilde p_S).$$

2. The projection as a sum of martingale differences (proof, p. 21): with $Z_{t,i}=c_i\mathbb 1(X_t=i)-c_i\frac{p_i}{p_i+\cdots+p_S}\mathbb 1(X_t\ge i)$ and $Z_t=\sum_iZ_{t,i}$,

$$\frac1n\sum_{t=1}^nZ_t=(\hat p-p)^Th,$$

together with the two intermediate expressions of the page. 3. Uncorrelated coordinates (proof, p. 21): $\mathbb E[Z_{t,i}Z_{t,j}]=0$ for $i\ne j$. 4. The predictable variance (proof, p. 21): $\sum_{t=1}^n\mathbb E[Z_t^2]=\sum_ic_i^2\,n\,\gamma_i$. 5. Corollary B.1 (p. 26), Bernstein's inequality for bounded martingale differences with random predictable variance $V_n$: for $n\ge96$, $\delta\in(0,1)$, with probability greater than $1-\delta$,

$$|M_n|\le2\sqrt{V_n\ln(n/\delta)}+3K\ln(n/\delta).$$

Significance

The result. Proposition 5.2 is the concentration half of the optimism step of the paper (Lemma 5.3): combined with an anti-concentration bound for Dirichlet samples along the same direction (Proposition 5.1), it shows that some posterior sample is optimistic along $h$ with constant probability. Because the bound is stated along a single direction and is weighted by the variance of $h$ rather than by $D$ alone, it avoids the $\sqrt S$ loss that an $\ell_1$ bound would incur, which is part of how the paper's regret bound improves on UCRL2's $\tilde O(DS\sqrt{AT})$. The stick-breaking form of the variance is what lets the same quantity appear on both sides of the optimism argument, in the Dirichlet bound and in the empirical bound.

Formalizing it. The proposition and its proof steps are proved on paper; none of them has a machine-checked proof. The regret theorem of the paper (Theorem 1) is not posed: its constants are hidden in $O(\cdot)$ and its algorithm's parameters are given as $\Theta(\cdot)$. Proposition 5.2, by contrast, is fully explicit. Corollary B.1 is a reusable martingale inequality with explicit constants. The predictable-variance identity and Fact 1 are exact identities about stick-breaking coordinates that recur in analyses of Dirichlet and categorical models.

Difficulty

Two steps resist the obvious approach. First, the statement carries the variance in stick-breaking form, not as $\mathrm{Var}_p(h)$; linking the two needs the decomposition of Fact 1 and the identity for the predictable variance, which are exact algebraic identities whose bookkeeping of tails and empty tails is error-prone. Second, the paper's own route goes through Corollary B.1, a martingale Bernstein inequality with a random variance, which rests on a peeling argument over a grid of variance levels (Seldin et al., 2012); Mathlib has neither this inequality nor a Bernstein inequality with explicit constants for bounded variables.

A known subtlety: the paper's proof, through Corollary B.1, yields the second term $3D\log(n/\rho)/n$, while the statement prints the smaller $3D\log(2/\rho)/n$. The printed statement is still true for $n$ iid trials (the classical Bernstein inequality gives a bound below it), so the goal is posed as printed. The paper's own proof therefore does not establish the printed constant.

Formalization scope

• States are Fin S with its natural order, 0-based; the paper's range $i<S$ is every state but the last (belowLast S). Fact 1 holds for every ordering; the natural order covers this since states are labels.
• Probability vectors are p : Fin S → ℝ with IsProbVec p (nonnegative, summing to one). Zero entries are allowed. A ratio whose denominator is zero evaluates to $0$ (Lean's convention), which gives the values the identities need; no positivity of $p$ is assumed.
• One trial has law cat p $=\sum_ip_i\delta_i$; $n$ trials have the product law trialsLaw n p $=$ Measure.pi. The empirical vector phat ω is computed from the sample ω : Fin n → Fin S. "With probability $1-\rho$" is ENNReal.ofReal (1 - ρ) ≤ trialsLaw n p {good event}; Corollary B.1's "greater than $1-\delta$" is strict. $\log$ is Real.log.
• The proof displays (milestones 2–4) are stated in the iid reading of the proposition: the paper writes them for transitions of an MDP out of a fixed $(s,a)$, with an indicator $\mathbb 1(s_{t-1}=s,a_{t-1}=a)$ and a random count $\tau$; here the indicator is one and $\tau=n$, and the conditional expectations are expectations under one draw of law $p$. Milestone 2 assumes every drawn state has positive probability (true almost surely), which the page's intermediate sum over $i\le S-1$ needs.
• Corollary B.1 is posed for a general filtered probability space, with $Z_i$ $\mathcal F_i$-measurable, $|Z_i|\le K$ almost surely and $\mathbb E[Z_i\mid\mathcal F_{i-1}]=0$.

The goal cannot be satisfied by a degenerate reading: $\hat p$ is built from the sample, the measure is the $n$-fold product of the categorical law $p$, the event is the good event itself (not a complement bound), and the variance term is not identically zero (for $S=2$, $p=(\tfrac12,\tfrac12)$ it equals $(h_1-h_2)^2/4$).

Needed infrastructure: finite-sum manipulations over tails of Fin S; a Bernstein or Freedman inequality with explicit constants (for iid bounded variables for the goal, for martingale differences for Corollary B.1). Contributions of either inequality are reusable well beyond this mission and are welcome, as are alternative proofs of the goal that bypass Corollary B.1.

Selected references

• S. Agrawal and R. Jia, Posterior sampling for reinforcement learning: worst-case regret bounds, arXiv:1705.07041v3, 2020; published as Optimistic Posterior Sampling for Reinforcement Learning: Worst-Case Regret Bounds, Mathematics of Operations Research, 2023. https://arxiv.org/abs/1705.07041
• T. Jaksch, R. Ortner and P. Auer, Near-optimal regret bounds for reinforcement learning, Journal of Machine Learning Research 11, 2010. https://www.jmlr.org/papers/v11/jaksch10a.html
• Y. Seldin, F. Laviolette, N. Cesa-Bianchi, J. Shawe-Taylor and P. Auer, PAC-Bayesian inequalities for martingales, IEEE Transactions on Information Theory 58(12), 2012. https://doi.org/10.1109/TIT.2012.2211334

Motivation

Cutting plane methods minimize a convex function, or find a point in a convex set, using only a separation oracle: a routine that, given a query point, either certifies it is good or returns a halfspace containing the target. Lee, Sidford and Wong (arXiv:1508.04874, FOCS 2015) gave a cutting plane method for a convex set in $\mathbb R^n$ inside a box of radius $R$ that uses an expected $O(n\log(nR/\epsilon))$ oracle calls and $O(n^3\log^{O(1)}(nR/\epsilon))$ additional time, improving on the $O(n^{\omega+1}\log(nR/\epsilon))$ additional time of Vaidya's method from over 25 years earlier, and derived from it faster algorithms for submodular function minimization, matroid intersection and submodular flow.

The speed-up depends on not recomputing the leverage scores of the current constraint matrix from scratch at every step. The algorithm maintains approximations and refreshes a few of them per step. Section 7.2 of the paper isolates the bookkeeping question this raises as a two-player game, the stochastic chasing $\vec 0$ game, and shows that a simple greedy strategy keeps the accumulated error small. The game is self-contained and has nothing to do with convexity: it is a statement about a random walk in $\mathbb R^m$ that is partially reset at every step.

Setting

Fix a dimension $m\ge1$ and constants $c>0$, $R>0$. For $\vec v\in\mathbb R^m$, $\|\vec v\|_\infty=\max_i|v_i|$ and $\|\vec v\|_2=(\sum_iv_i^2)^{1/2}$.

A point starts at $\vec x^{(1)}=\vec 0$. Each round $k=1,2,\dots$ runs as follows (Algorithm 4).

1. A stochastic adversary chooses a probability distribution $\mathcal D^{(k)}$ on $\mathbb R^m$ with mean $\vec 0$ and $\|\vec\Delta\|_2\le c$ for every $\vec\Delta$ in its support.
2. The adversary chooses an observation $\vec y^{(k)}$ with $\|\vec y^{(k)}-\vec x^{(k)}\|_\infty\le R$.
3. The player chooses a coordinate $i^{(k)}$, knowing only $\vec y^{(k)}$: neither $\vec x^{(k)}$, nor $\mathcal D^{(k)}$, nor the step.
4. A step $\vec\Delta^{(k)}$ is drawn from $\mathcal D^{(k)}$ and the point moves to

$$x^{(k+1)}_{i^{(k)}}=0,\qquad x^{(k+1)}_j=x^{(k)}_j+\Delta^{(k)}_j\quad(j\ne i^{(k)}).$$

The adversary may use everything that has happened so far to make its choices. The player wants to keep $\vec x^{(k)}$ near $\vec 0$ in $\|\cdot\|_\infty$; the adversary wants to push it away. The largest-coordinate strategy is $i^{(k)}=\operatorname{argmax}_i|y^{(k)}_i|$: reset the coordinate that looks largest.

Formalization targets

Goal: Theorem 34

If the player uses the largest-coordinate strategy, then for every $p\in(0,1]$, with probability at least $1-p$,

$$\|\vec x^{(k)}\|_\infty\le2(c+R)\log\big(4mk^2/p\big)\qquad\text{for all }k\ge1.$$

The bound holds simultaneously for all rounds, against every adaptive adversary, and grows only logarithmically in $k$, in $m$ and in $1/p$.

Milestones

The milestones are the steps that the paper's proof of Theorem 34 (pp. 43–44) displays:

1. the exponential inequality $e^x\le1+x+\tfrac{x^2}{2}e^{|x|}$ and its consequence $e^{\alpha x+\alpha\delta}\le e^{\alpha x}+\alpha\delta e^{\alpha x}+\tfrac12\alpha^2\delta^2e^{\alpha x+|\alpha|c}$ for $|\delta|\le c$;
2. the one-step drift bound for the potential $\Phi(\vec x)=\sum_ie^{\alpha x_i}+\sum_ie^{-\alpha x_i}$:

$$\mathbb E_{\vec\Delta\sim\mathcal D}\,\Phi(\vec x+\vec\Delta)\le\Phi(\vec x)+\alpha^2e^{\alpha c}c^2\eta,\qquad\eta=\max\big(\max_ie^{\alpha x_i},\max_ie^{-\alpha x_i}\big);$$

3. the choice $\alpha=1/(2(c+R))$, for which $e^{2\alpha(c+R)}(\alpha(c+R))^2\le1$ and $\alpha^2e^{\alpha c}c^2\le e^{-\alpha(R+c)}$;
4. the union-bound arithmetic $1-\sum_{k\ge1}2m/\lambda_k=1-\sum_{k\ge1}p/(2k^2)\ge1-p$ for $\lambda_k=4mk^2/p$.

Significance

Within the paper, Theorem 34 is what lets the cutting plane method keep its leverage-score estimates within a bounded multiplicative error while refreshing only one estimate per step; this is one of the ingredients behind the $O(n^3\log^{O(1)}(nR/\epsilon))$ additional time. The game reappears whenever an algorithm tracks many slowly drifting quantities with noisy observations and can afford to recompute only a few of them exactly per step, which makes the statement useful beyond this paper.

None of the statements in this mission has a machine-checked proof. The theorem is published with a proof. The mission asks for a formal proof of the statement exactly as published, with the constant $4$ inside the logarithm. A formal proof of the milestones alone would already give a reusable exponential-potential toolkit for adaptive random processes in $\mathbb R^m$.

Difficulty

The point process is not a martingale: the player's resets depend on a noisy observation, the adversary is adaptive, and the reset can hit a coordinate that is up to $2R$ smaller in absolute value than the largest one. Per-coordinate tail bounds do not suffice, because the adversary may concentrate its moves on whichever coordinates the player is not resetting. A bound that holds for all $k$ at once, with only logarithmic dependence on $k$, has to control all coordinates jointly. Establishing such joint control, with the specific constant $4$ inside the logarithm, against the most adversarial interaction between the observation error $R$ and the step size $c$, is where the work lies.

Formalization scope

• Probability model. The randomness is a probability space $(\Omega,\mu)$ with a filtration $(\mathcal F_k)_{k\ge0}$. The adversary's adaptive choice of $\mathcal D^{(k)}$ is modelled by the conditional law of the step: each coordinate of the step has conditional mean $0$ given the past, the step is measurable with respect to the next $\sigma$-algebra, and $\sum_i\Delta_i^2\le c^2$ holds everywhere. The observation $\vec y^{(k)}$ is measurable with respect to the current $\sigma$-algebra, so it is fixed before the step is drawn, and $\|\vec y^{(k)}-\vec x^{(k)}\|_\infty\le R$ holds on the actual trajectory.
• Indexing. Coordinates are Fin m (0-based), with $m\ge1$. Lean round $k\in\mathbb N$ is the paper's round $k+1$, so the goal's bound reads $\log(4m(k+1)^2/p)$; at Lean round $0$ the point is $\vec 0$.
• Norms. $\|\cdot\|_\infty$ is Lean's sup norm on Fin m → ℝ. The step bound $\|\vec\Delta\|_2\le c$ is written as $\sum_i\Delta_i^2\le c^2$, never as a sup-norm bound. The paper's prose once writes $\|\vec\Delta\|_2^2\le c$; Algorithm 4 and the proof use $\|\vec\Delta\|_2\le c$, which is what is formalized.
• Tie rule. $\operatorname{argmax}_i|y_i|$ breaks ties by the least index; the paper's theorem is claimed for any tie rule.
• Constants. $c>0$, $R>0$ (Algorithm 4), $0<p\le1$, natural logarithm. The drift milestone adds $\alpha\ge0$.
• Not trivial by construction. The hypotheses are satisfiable by genuinely random adversaries (a fair-coin step of size $c$ is one), and the conclusion is a probability lower bound on an event, not a statement that holds vacuously; a formalization in which the observation could depend on the step, or in which the step bound were a sup-norm bound, would not be the paper's theorem.
• Out of scope. Running time, the leverage-score application (Section 7.1, Theorem 31) and the rest of the cutting plane method.
• Infrastructure. Conditional expectation with respect to a filtration, Markov's inequality and countable union bounds are in Mathlib. Supermartingale lemmas for nonnegative adapted processes, and the passage from a per-step drift inequality to a bound on the expected potential, are reusable well beyond this mission. Proofs of individual milestones are welcome independently of the goal.

Selected references

• Y. T. Lee, A. Sidford, S. C. Wong, A Faster Cutting Plane Method and its Implications for Combinatorial and Convex Optimization, FOCS 2015; arXiv:1508.04874v2, 2015. https://arxiv.org/abs/1508.04874
• P. M. Vaidya, A new algorithm for minimizing convex functions over convex sets, FOCS 1989; Mathematical Programming 73 (1996) 291–341. https://doi.org/10.1007/BF02592216

Motivation

Mobile retail stalls (self-driving or driver-operated vending vehicles that move to customers who order through a phone app) are studied by Cao and Qi in Stall Economy: The Value of Mobility in Retail on Wheels (Operations Research, 2022; the mission cites the authors' SSRN manuscript 3711896). A retailer partitions a city into service zones, one stall per zone, and must decide how densely to deploy stalls. That decision is made by continuous approximation: each zone is modelled as a small queueing system whose service time includes the stall's travel to the next customer. The mean and variance of that travel distance enter the Pollaczek–Khinchine waiting-time formula of an M/G/1 queue (the paper's equations (1a)–(2), p. 18), so closed forms for them are the input of the paper's whole deployment and pricing analysis (§4).

The paper considers two on-demand modes. In the door-to-door mode the stall drives to each customer's doorstep. In the within-radius mode each customer walks up to a distance $r$ toward the stall, and the stall only moves until the two are $r$ apart. This mission formalizes the travel-distance moments of both modes: Proposition 1 (door-to-door, p. 11) and Proposition 3 (within-radius, p. 18), whose proofs are in the paper's Appendix B (pp. 44–45 and 49–51).

Setting

All distances are Manhattan ($\ell_1$) distances (p. 9): $|A-B| = |a_1-b_1| + |a_2-b_2|$. A service zone is a square rotated by $45^\circ$, a diamond, of Euclidean edge length $R>0$; the paper sets $R = R(\rho) = 1/\sqrt\rho$ for a stall density $\rho$ (p. 11). In Manhattan coordinates centred at the zone's centre,

$$\mathcal Z_R = \{(x,y) : |x|+|y| \le R/\sqrt2\},$$

which has area $R^2$. Customers arrive uniformly on $\mathcal Z_R$.

Fix a walking radius $0\le r\le R/\sqrt2$. The inner diamond $\mathcal I_{R,r} = \{|x|+|y|\le R/\sqrt2-r\}$ lies $r$ inward from the boundary and has edge length $R-\sqrt2 r$. The paper's model for the stall's position when a new customer arrives (proof of Proposition 3, p. 49) is: the stall $A$ is uniform on $\mathcal I_{R,r}$, the customer $B$ is uniform on $\mathcal Z_R$, and the two are independent. The repositioning trip length is

$$L_r = \max\{|A-B| - r,\ 0\},$$

and $L_0' = |A-B|$ denotes the untruncated distance. In the door-to-door case $r=0$, both points are uniform on the zone and $L_0 = |A-B|$. The variance is $\operatorname{Var}(L_r) = \mathbb E[L_r^2]-\mathbb E[L_r]^2$.

The uniform law of the stall is the paper's Theorem 1 (the subject of the companion mission I), read in a continuum limit that the paper states informally (p. 17). This mission takes the uniform law as its model and does not depend on that limit.

Formalization targets

Goal: Proposition 3 (p. 18)

For all $R>0$ and $0\le r\le R/\sqrt2$,

$$\mathbb E[L_r] = \frac{7\sqrt2R^3-22R^2r+2\sqrt2Rr^2+12r^3}{15R^2},$$ $$\operatorname{Var}(L_r) = \frac{22R^6-22\sqrt2R^5r-140\sqrt2R^3r^3+400R^2r^4-48\sqrt2Rr^5-144r^6}{225R^4},$$

and both are non-decreasing in $R$ (on $\{R : r\le R/\sqrt2\}$) and non-increasing in $r$ (on $[0,R/\sqrt2]$).

Milestones, in the order of the proof

1. Proposition 1 (p. 11): $\mathbb E[L_0] = 7\sqrt2R/15$ and $\operatorname{Var}(L_0) = 22R^2/225$.
2. $\mathbb E[L_0'] = \tfrac{7\sqrt2R}{15}-\tfrac{7r}{15}+\tfrac{2\sqrt2r^2}{15R}+\tfrac{2r^3}{15R^2}$ (p. 49).
3. $\mathbb P(L_0'\le r) = 2r^2/R^2$ and $\mathbb E[L_0'\,\mathbf 1\{L_0'\le r\}] = \tfrac23r\cdot 2r^2/R^2$ (p. 50).
4. $\mathbb E[X^2] = (R^2-\sqrt2Rr+r^2)/6$ for the horizontal component $X$ of $|A-B|$ (p. 50).
5. $\mathbb E[(L_0')^2] = (8R^4-8\sqrt2R^3r+7R^2r^2+r^4)/(15R^2)$ (p. 51).
6. $\mathbb E[(L_0')^2\,\mathbf 1\{L_0'\le r\}] = \tfrac12r^2\cdot 2r^2/R^2$ (p. 51).
7. Proposition 3(I) and 8. Proposition 3(II) on their own.

A supporting theorem, $\mathbb E[XY] = (3R^4-3\sqrt2R^3r+2R^2r^2+r^4)/(30R^2)$ (p. 50), is posed as well.

Significance

The result. With Proposition 3 the service time of the within-radius mode has explicit first and second moments, so the M/G/1 waiting time, the stall's daily travel, and the profit density of §4 are explicit functions of $(\rho, r)$. Part (III) is the qualitative content the paper calls the first effect of avoiding the "last 100 meters": a longer customer walk shortens the stall's repositioning, and a larger zone lengthens it. Proposition 1 is the $r=0$ benchmark against which that saving is measured.

Formalizing it. The results are proved in the paper by direct integration; none is machine-checked. The proofs split the domain into several regions by the signs of coordinate differences and assert the values of the resulting polynomial integrals "by calculation". A formal proof checks every one of those integrals, the use of conditional expectations given the event $\{L_0'\le r\}$, and the derivative signs behind part (III), which the paper states without verification on the whole range. The intermediate moments are useful on their own for other models with uniform demand on diamonds under the Manhattan metric.

Difficulty

The obvious route rotates the diamond by $45^\circ$, where the $\ell_1$ distance becomes an $\ell_\infty$ distance and the zone a square, and then integrates. For $r=0$ this works cleanly. For $r>0$ the stall's square is smaller than the customer's, and $\max\{\cdot\}$ of two coordinate differences over two squares of different sizes splits into many polynomial pieces. The paper instead stays in the original coordinates and splits into six regions for $\mathbb E[XY]$. Either way, the truncation at $r$ is the delicate step: it requires that the whole $\ell_1$ ball of radius $r$ around the stall lies in the zone, which is exactly why the stall is confined to the inner diamond. Part (III) is not a consequence of (I) and (II) by inspection: the derivative in $R$ of the mean vanishes at the boundary $r = R/\sqrt2$, so the sign argument must be done on the closed range.

Formalization scope

Points are elements of ℝ × ℝ with Lebesgue measure. The definition StallEconomy.TripLength.Setting provides zone R, innerZone R r, the scale factor shrink R r = 1 − √2 r / R, the Manhattan distance l1, the trip length Lr r, the expectation E R r F, meanL R r and varL R r. The stall's uniform law is realised as $A = s\,U$ with $s = 1-\sqrt2r/R \in [0,1]$ and $U$ uniform on $\mathcal Z_R$, which is the uniform law on $\mathcal I_{R,r}$; it covers the endpoint $r=R/\sqrt2$, where the inner diamond is a single point, without dividing by $(R-\sqrt2r)^2$. Thus

$$\mathbb E[F(A,B)] = R^{-4}\int_{\mathcal Z_R}\int_{\mathcal Z_R} F(s\,u, b)\,db\,du.$$

Standing conventions and deviations from the page:

• every statement assumes $R>0$, and the within-radius statements $0\le r\le R/\sqrt2$, the paper's range;
• $R$ is the edge length itself, not $1/\sqrt\rho$;
• the conditional expectations given $\{L_0'\le r\}$ of pp. 50–51 are stated as truncated expectations $\mathbb E[\,\cdot\,\mathbf 1\{L_0'\le r\}]$, since the conditioning event has probability $0$ at $r=0$;
• the printed slips "$\mathbb P(L_0>r)$" (p. 50, $L_0'$ meant) and the conditioning event "$L_0'^2\le r$" (p. 51, $L_0'\le r$ meant) are corrected;
• "increasing/decreasing" in part (III) is weak monotonicity.

Formalizations that would trivialize the goal are ruled out: meanL and varL are integrals, not the closed forms; part (III) is stated about those integrals, not about the polynomials; and nothing is restricted to $r=0$ or to a fixed $R$.

A complete development needs iterated set integrals of piecewise polynomials over diamonds in ℝ × ℝ (Fubini on zone R, the change of variables $u\mapsto su$), and elementary calculus for part (III). Contributions of any of the moments, of a reusable lemma computing integrals of polynomials over diamonds, and of the monotonicity of the closed forms are all welcome. Proposition 2 of the paper, which is false as printed, is not claimed here.

Selected references

• J. Cao and W. Qi, Stall Economy: The Value of Mobility in Retail on Wheels, Operations Research, 2022 (articles in advance). https://doi.org/10.1287/opre.2022.2404 ; manuscript: SSRN 3711896, https://ssrn.com/abstract=3711896
• G. F. Newell, Dispatching policies for a transportation route, Transportation Science 5(1) 91–105, 1971 (origin of continuous approximation). https://doi.org/10.1287/trsc.5.1.91

Motivation

A permissioned blockchain is a shared ledger to which only approved participants may write. In supply chains it is proposed as a way to make product information (origin, quality, which supplier fulfilled an order) verifiable to buyers. Iyengar, Saleh, Sethuraman and Wang (SSRN 3602376; Management Science 2023, doi:10.1287/mnsc.2022.4532) ask who gains from such adoption and who pays for it.

Their first main result (Proposition 4.8, the subject of the companion mission I) identifies an adoption failure: when products differ strongly in how well they match consumers' tastes, full adoption raises total welfare, yet no manufacturer adopts, because price competition leaves manufacturers no profit with which to recover the adoption cost while the information gain accrues to consumers. Their second main result, Proposition 4.9, the goal of this mission, shows that a simple self-financing mechanism removes the failure: charge consumers a fee for access to the blockchain's information and pass the proceeds to the manufacturers.

Setting

There are $4m$ manufacturers, $m\ge 2$. Manufacturer $i$ has a horizontal type $q_i\in\{A,B\}$ and a vertical type $\xi_i\in\{h,l\}$; each of the four type classes has exactly $m$ members. Joining the blockchain costs manufacturer $i$ an amount $\chi_i>0$; $a_i\in\{0,1\}$ records the decision. A unit mass of consumers values a matching product at $H$ and a mismatched one at $L$, with $0\le L<H$, plus a vendor quality $h>l\ge 0$; the high-quality vendor has marginal cost $\gamma>0$. Each consumer $k$ also has an outside option $\phi_k$, drawn from a continuous distribution $G$ supported on $[0,\infty)$. The parameter of interest is the horizontal differentiation $\Delta=H-L$; $L$ is held fixed and $H=L+\Delta$.

Under full adoption, a consumer who has access to the blockchain's information finds a best product utility $\Delta+L+h-\gamma$; without access, only $\Delta/2+L+h-\gamma$. A system of transfers $(\kappa,\{\tau_i\}_{i\in M})$ charges each consumer who wants access a fee $\kappa$ and pays manufacturer $i$ an amount $\tau_i\ge 0$. A consumer pays ($b_k=1$) when

$$\max\{\Delta+L+h-\gamma,\phi_k\}-\kappa\ \ge\ \max\Big\{\tfrac{\Delta}{2}+L+h-\gamma,\phi_k\Big\},$$

and $\mu_\kappa$ denotes the mass of paying consumers. The system is self-financing if

$$\kappa\cdot\mu_\kappa=\sum_{i\in M}\tau_i. \tag{14}$$

Manufacturer $i$ earns $\Pi(a_i,a_{-i})-\chi_i a_i+\tau_i a_i$ (15), where the gross profit $\Pi$ is zero because of price competition. The system overcomes adoption failures if full adoption ($a_i=1$ for all $i$) is an equilibrium of this game.

The proof of Proposition 4.9 uses the fee $\kappa=\sum_i\chi_i/G(\phi)$ and the gain from access

$$h(\phi_k;\phi)=\max\{\Delta+L+h-\gamma,\phi_k\}-\frac{\sum_{i\in M}\chi_i}{G(\phi)}-\max\Big\{\frac{\Delta}{2}+L+h-\gamma,\phi_k\Big\}.$$

Formalization targets

Goal: Proposition 4.9 (p. 21)

$$\exists\,\Delta_0\ \forall\,\Delta>\Delta_0\ \exists\,\kappa,\{\tau_i\}:\quad \tau_i\ge 0,\quad \kappa\cdot\mu_\kappa=\sum_{i\in M}\tau_i,\quad a\equiv 1\ \text{is an equilibrium of (15)}.$$

The goal asserts the existence of a working scheme, as printed; it does not fix the scheme.

Milestones: Lemma B.1 (p. 38)

(a) For $\Delta>0$ and every $\phi$, $\phi_k\mapsto h(\phi_k;\phi)$ is continuous and weakly decreasing on $[0,\infty)$.

(b) For all sufficiently large $\Delta$ there is $\phi^*\ge 0$ with

$$h(\phi^*;\phi^*)=0,\qquad h(\phi_k;\phi^*)\ge 0\iff \phi_k\le\phi^*\quad(\phi_k\ge 0),$$

so that at the fee $\sum_i\chi_i/G(\phi^*)$ exactly the consumers with $\phi_k\le\phi^*$ pay.

Significance

Proposition 4.9 is the constructive half of the paper's message: an adoption failure driven by the split between who bears the cost and who reaps the benefit can be repaired without outside funding, by a fee on the side that benefits. The paper's scheme ($\tau_i=\chi_i$, $\kappa=\sum_i\chi_i/G(\phi^*)$) exactly reimburses adoption costs and is financed by a threshold set of consumers; Lemma B.1(b) is the fixed-point statement that makes this calibration consistent.

The result is proved in the paper (App. A.2, pp. 36–38, and App. B, pp. 38–41). It has no machine-checked proof. This mission produces one: a formal model of the access-fee mechanism in the reduced form the paper's proofs use, the threshold lemma, and the main proposition. The goal can be attacked through Lemma B.1(b) as in the paper, or by any other scheme meeting the definition.

Difficulty

The calibration is circular: the fee depends on the mass of paying consumers, and the mass of paying consumers depends on the fee. Lemma B.1(b) resolves this with a one-dimensional fixed point $h(\phi^*;\phi^*)=0$, and the delicate points are positivity of $G$ at the relevant arguments (so that the fee is finite), the three-piece shape of $h(\cdot;\phi)$, and choosing $\Delta$ large enough that the sign change happens inside the strictly decreasing piece. For the goal, the point to check is that the self-financing identity uses the actual mass of payers at the chosen fee: a fee too high drives the payers' mass, and with it the revenue, towards zero.

Formalization scope

• Reduced form. The paper's full model is a signal game with Bertrand pricing whose equilibrium concept is not defined precisely; its proofs work with the closed-form outcome of Proposition A.1. The formalization does the same: consumer utilities are those computed in the proof of 4.9 ($\Delta+L+h-\gamma$ with access, $\Delta/2+L+h-\gamma$ without), gross profit $\Pi$ is the constant $0$ in every profile (pp. 37–38, also for a deviating manufacturer), and "equilibrium" is a pure Nash equilibrium over unilateral switches of $a_i\in\{0,1\}$. Signal accuracy is $\alpha=1/2$, as in the paper's main text.
• Encoding. Manufacturers are Fin 2 × Bool × Fin m; adoption profiles are Bool-valued. $G$ is ProbabilityTheory.cdf μ for a measure μ on ℝ. $\Delta$ is an argument of every object, with $H=L+\Delta$.
• Standing assumptions (one predicate Model.Standing): $m\ge 2$, $0\le L$, $0\le l<h$, $\gamma>0$, $\chi_i>0$; $\mu$ a probability measure without atoms, $\mu((-\infty,0))=0$, and $\mu((a,b))>0$ for $0\le a<b$ (support $[0,\infty)$). No cost function $c_l$, no Assumption 1 and no finite mean are needed or assumed. Lemma B.1(a) additionally assumes $\Delta>0$, the model's $L<H$.
• Ties in the access decision go to paying, as in the proof's "$b_k=1$ iff $h\ge 0$".
• Ruled out. $\mu_\kappa$ is the $\mu$-measure of the paying consumers, not a free number in $[0,1]$; the equilibrium predicate and $\Pi$ are defined, not assumed; transfers are nonnegative; and no statement relies on Lean's value $0$ for a division by $G(\phi)=0$.
• Not formalized. The non-uniqueness clause of Lemma B.1(b) and Example B.1 (p. 40); the purchase-stage claims of the proof of 4.9 (market shares under transfers); Appendix C's symmetric-cost variant.
• Infrastructure. Only Mathlib's measure theory and ProbabilityTheory.cdf; no new library is needed. Lemmas on CDFs of atomless, fully supported laws on $[0,\infty)$ are reusable beyond this mission. Proofs of the milestones and of the goal are welcome; the goal may be proved by any route.

Selected references

• G. Iyengar, F. Saleh, J. Sethuraman, W. Wang, Economics of Permissioned Blockchain Adoption, SSRN 3602376, version of 2022-08-19. https://ssrn.com/abstract=3602376
• G. Iyengar, F. Saleh, J. Sethuraman, W. Wang, Economics of Permissioned Blockchain Adoption, Management Science, 2023. https://doi.org/10.1287/mnsc.2022.4532

Motivation

In many trades the buyer does not know how much the good is worth to it, and can find out before negotiating: a firm commissions due diligence before an acquisition, a hospital pilots a device before negotiating its price, a household inspects a house before making an offer. Such information has two effects. It makes the trade decision better informed, which enlarges the total surplus, and it is paid for by the buyer alone, while the surplus it creates is shared through bargaining.

L. Guo, Gathering Information before Negotiation (SSRN 3930651; Management Science, doi:10.1287/mnsc.2022.4360), studies how this interaction shapes the seller's payoff. Its headline is a reversal: a seller with more bargaining power, or with a more valuable outside option, can be worse off, and a seller with a higher production cost can be better off. The reason is that the buyer's information choice reacts to these parameters, and the reaction can outweigh their direct effect. This mission formalizes that reversal for the paper's worked example, the uniform prior with a linear information cost.

Setting

A seller and a buyer negotiate over one unit of a good. The seller's cost is $c\in(0,1)$. The buyer's value $u$ is unknown to both parties; the common prior is the uniform distribution $F(u)=u$ on $[0,1]$, with mean $\hat u=1/2$. The bargaining powers are $\theta_b\in(0,1)$ for the buyer and $\theta_s=1-\theta_b$ for the seller.

Before negotiating, the buyer chooses an informativeness $\alpha\in[\underline\alpha,\bar\alpha]$, with $0<\underline\alpha<\bar\alpha<1$. It then observes a truth-or-noise signal $w$: with probability $\alpha$ it equals $u$, and otherwise it is an independent draw from the prior. The buyer's posterior mean is $v=\alpha w+(1-\alpha)\hat u$. The information cost is linear,

$$k(\alpha)=\bar k\,\frac{\alpha-\underline\alpha}{\bar\alpha-\underline\alpha},\qquad \bar k>0 .$$

If $v>c$ the parties trade and split the net surplus $v-c$ in the proportions $\theta_s:\theta_b$; otherwise they do not trade. The total ex ante surplus is

$$A(\alpha,c)=\mathbb E\big[(v-c)^+\big]=\int_0^1\max\Big\{\alpha w+\frac{1-\alpha}{2}-c,\;0\Big\}\,dw ,$$

and the buyer chooses $\alpha$ to maximise

$$U_b(\alpha)=\theta_b\,A(\alpha,c)-k(\alpha).$$

The optimal set $\alpha^*$ is the set of maximisers of $U_b$ on $[\underline\alpha,\bar\alpha]$. The seller's equilibrium expected payoff is

$$U_s^*=\theta_s\,A(\alpha^*,c)\quad\text{(material cost)},\qquad V_s^*=c+\theta_s\,A(\alpha^*,c)\quad\text{(opportunity cost)}.$$

Write $\Delta(c)=A(\bar\alpha,c)-A(\underline\alpha,c)$ for the surplus gain of maximal information, and $\tilde\theta=\bar k/\Delta(c)$ when $\Delta(c)>\bar k$, $\tilde\theta=1$ otherwise. For fixed $\theta_b$, the cost thresholds $c_l\le 1/2\le c_h$ are the endpoints of the set of costs at which $\theta_b\Delta(c)>\bar k$.

Formalization targets

Goal: Proposition 2 (p. 14), uniform prior

For every selection of optimal information levels:

1. $\theta_s\mapsto U_s^*$ and $\theta_s\mapsto V_s^*$ are nondecreasing on $(0,1-\tilde\theta)$ and on $(1-\tilde\theta,1)$, and, if $\tilde\theta<1$, drop strictly at $\theta_s=1-\tilde\theta$;
2. $c\mapsto U_s^*$ is nonincreasing on $(0,c_l)$ and on $(c_l,1)$, and, if $c_l<c_h$, jumps up strictly at $c=c_l$;
3. $c\mapsto V_s^*$ is nondecreasing on $(0,c_h)$ and on $(c_h,1)$, and, if $c_l<c_h$, drops strictly at $c=c_h$.

A drop at $t_0$ means: for some $\varepsilon>0$, every value just to the right of $t_0$ is strictly below every value just to the left.

Milestones

$$A(\alpha,c)=\begin{cases}\max\{1/2-c,0\},&\alpha\le|1-2c|,\\ [(1+\alpha)/2-c]^2/(2\alpha),&\alpha\ge|1-2c|,\end{cases}$$

the uniform display of p. 13. The proof of Corollary 1 (p. 30) then contributes three steps: $A(\cdot,c)$ is constant and then increasing, and convex; the optimum is a corner, $\alpha^*\in\{\underline\alpha,\bar\alpha\}$; and $\Delta$ vanishes for extreme costs, rises and then falls in $c$, and peaks at $\Delta(1/2)=(\bar\alpha-\underline\alpha)/8$. Corollary 1 (p. 13) gives the two threshold rules: (i) $\alpha^*=\underline\alpha$ for $\theta_b\le\tilde\theta$ and $\alpha^*=\bar\alpha$ for $\theta_b>\tilde\theta$; (ii) $\alpha^*=\bar\alpha$ exactly for $c_l<c<c_h$.

Significance

The result. Without information acquisition, the seller's payoff is increasing in its bargaining power and in its outside option and decreasing in its material cost: these are the direct effects. Proposition 2 shows that each of them can be reversed by a discontinuous jump. The mechanism is that the buyer stops gathering information when its own share of the surplus becomes too small (high $\theta_s$) or the trade decision becomes clear-cut (extreme $c$). The result bears on when a seller should prefer to commit to a weaker bargaining position, and on why cost increases need not hurt a seller facing an uninformed buyer.

Formalizing it. The paper calls Proposition 2 an immediate consequence of Corollary 1. That corollary rests on a short appendix argument whose printed version contains slips: the peak of $\Delta$ is printed as $\theta_b(\bar\alpha-\underline\alpha)/8$, strictness is claimed on a closed interval at whose endpoints $\Delta=0$, and "$\alpha^*\in\{\underline\alpha,\bar\alpha\}$" fails at $c=1/2$ when the two corners tie. A machine-checked development settles exactly which form of each claim is true. The result has been proved informally in the paper; it has not been formalized before.

Difficulty

The obvious argument treats $\alpha^*$ as a function and differentiates $U_s^*$. That does not work here. At the thresholds $\alpha^*$ is not single-valued, and between them it is constant, so the whole content lies in the jumps. A jump statement must hold whichever optimal level is selected at each parameter, and it must compare values on both sides of a threshold whose location depends on $\Delta$. Showing that the thresholds are well placed requires the inverted-U shape of $\Delta$, which comes from an explicit but piecewise integral. The corner property needs convexity of $A$ across the kink at $\alpha=|1-2c|$, where the two branches of the closed form meet.

Formalization scope

All quantities are real numbers. $A$ is the interval integral over the uniform prior after the change of variables $v=\alpha w+(1-\alpha)\hat u$; no density is assumed. The bargaining stage is not modelled; the payoffs are the paper's reduced forms (6) and $\theta_sA(\alpha^*,c)$. Conventions: $c\in(0,1)$ (the paper's $c\in(\underline u,\bar u)$); $\theta_b,\theta_s\in(0,1)$ with $\theta_s=1-\theta_b$; $[\underline\alpha,\bar\alpha]$ non-degenerate; $\tilde\theta=1$ when $\Delta(c)\le\bar k$, which avoids $\bar k/0$ and keeps $\tilde\theta\in(0,1]$. Monotonicity is claimed on each side of the jump point, open at that point (and across the other cost threshold), and the jump whenever the threshold is interior. In (ii) and (iii), $c_l\le1/2\le c_h$ are assumed to satisfy "$c_l<c<c_h$ iff $\theta_b\Delta(c)>\bar k$" for all $c\in(0,1)$, which determines them; when the buyer never gathers information this forces $c_l=c_h=1/2$.

The paper states Corollary 1 and Proposition 2 for four focal priors (uniform, exponential, logistic, modified Pareto) but works out only the uniform one. This mission is pinned to the uniform prior and the linear cost.

A trivializing formalization is ruled out: $A$ is not defined by its closed form (that closed form is a milestone), $\alpha^*$ is the set of maximisers of $U_b$ and not a threshold rule, and the goal quantifies over every selection from that set, so neither Corollary 1 nor Proposition 2 holds by definition.

A complete development needs piecewise interval integrals of $\max\{\cdot,0\}$, convexity of a function with a $C^1$ junction, and the fact that a convex function on a segment attains its maximum at an endpoint. All of these are general facts, reusable beyond this mission. Proofs of the milestones in any order are welcome; Proposition 3 and the other priors are not posed here.

Selected references

• L. Guo, Gathering Information before Negotiation, SSRN 3930651, manuscript of 15 Feb 2022. https://ssrn.com/abstract=3930651
• L. Guo, Gathering Information before Negotiation, Management Science (journal version of the manuscript above; its theorem numbering is not used here). https://doi.org/10.1287/mnsc.2022.4360

Motivation

The Lightning Network is a payment layer built on top of Bitcoin: pairs of participants lock funds in a bilateral payment channel and then exchange payments off-chain, settling on the blockchain only occasionally. Keeping a channel open costs money, because it ties up capital and needs periodic rebalancing, and Guasoni, Huberman and Shikhelman (Lightning Network Economics: Channels, 2022, cited in the paper as [GHS22]) showed that this recurring cost depends on the channel's net flow and grows less than proportionally with it. Which network topology a population of payers and payees should use is therefore an economic question about subadditive costs on graphs.

Lightning Network Economics: Topology (SSRN 4439190; published version in Management Science, 2024, doi:10.1287/mnsc.2023.03872) answers this question in an axiomatic model. Its §3.2 introduces hermetization, which replaces the channels inside a group of nodes by channels to a new hub, and asks when this reduces cost. Theorem 3.8 gives a deterministic sufficient condition, a large average degree compared with the spread of channel sizes. Theorem 3.9, the subject of this mission, shows that the condition is typical: if channel sizes are random with thin, power-law-bounded cost tails, the network is hermetizable with high probability. The paper reads this as "cost reduction is the norm, not the exception", which is the economic argument for hubs in payment-channel networks.

Setting

Nodes form a finite set $V$. A Lightning Network (LN) is an anti-symmetric real matrix $\Lambda=(\lambda_{i,j})_{i,j\in V}$, $\lambda_{i,j}=-\lambda_{j,i}$, of net channel flows; $\lambda_{i,j}=0$ means there is no channel between $i$ and $j$. A channel cost is a function $c:\mathbb R\to\mathbb R_+$ with

• (MO) $c(x)>c(y)$ for $x>y\ge 0$; (SY) $c(-x)=c(x)$; (CI) $c(0)=0$;
• (SA) $c(x+y)<c(x)+c(y)$ for $x,y>0$;
• (SA+) for a strictly increasing $g_+:\mathbb R_+\to\mathbb R_+$, $c(kx)<\dfrac{k}{g_+(k)}c(x)$ for $k>1$, $x>0$.

The cost of the network is $c(G)=\tfrac12\sum_{i,j}c(\lambda_{i,j})$. For a node $i$, $d(i)$ is its number of channels, $s(i)$ the smallest and $S(i)$ the largest $|\lambda_{i,j}|$ over its channels.

The hermetization of a set of nodes $U$ deletes all channels inside $U$, adds a new node $v_0$, and joins each $i\in U$ to $v_0$ by a channel carrying $\sum_{j\in U}\lambda_{i,j}$, its net flow towards the rest of $U$. The set $U$ is hermetizable if this strictly lowers the cost, and the LN is hermetizable if some $U$ is.

In the random model a simple graph $E$ on $V$ fixes the channels, so $d(i)$ is the degree of $i$ in $E$ and is not random. On a probability space $(\Omega,\mathbb P)$, the flows $\lambda_{i,j}(\omega)$ are random variables, nonzero exactly on the channels of $E$, and $\Lambda(\omega)$ is an LN for every $\omega$.

Formalization targets

Goal: Theorem 3.9

Let $a>1$, $b>0$, $\varepsilon>0$. There is $k>0$, depending only on $(a,b,\varepsilon)$, such that for every finite $E$ with at least one channel, every $c,g_+$ satisfying (MO)–(SA+), and every random LN with, for all channels $ij\in E$,

$$\text{(i)}\ \ \mathbb P\big(c(\lambda_{i,j})>x\big)<b\,x^{-a}\ \ (x>0),\qquad \text{(ii)}\ \ \mathbb P\big(c(\lambda_{i,j})>\varepsilon\big)=1,$$

the LN is hermetizable with probability at least

$$1-k\sum_{i\in V}d(i)\,\big(g_+(d(i))\big)^{-a}.$$

The constant is not fixed: any $k$ uniform in the network and in $c,g_+$ is a proof of the goal.

Milestones

1. Lemma B.1. If every $i$ in a nonempty set $U$ has a channel in $U$ and $g_+(d_U(i))>2c(S_U(i))/c(s_U(i))$, with degrees and sizes in the subnetwork induced on $U$, then $U$ is hermetizable.
2. (8)–(10). $\mathbb P(\text{hermetizable})\ge 1-\sum_{i:\,d(i)\ge1}\mathbb P\big(g_+(d(i))\le 2c(S(i))/c(s(i))\big)$.
3. (11). Under (ii), $\mathbb P\big(g_+(d(i))\le 2c(S(i))/c(s(i))\big)\le\mathbb P\big(\tfrac{\varepsilon}{2}g_+(d(i))\le c(S(i))\big)$ for $d(i)\ge1$.
4. (12)–(13). Under (i), $\mathbb P\big(c(S(i))\ge x\big)\le d(i)\,b\,x^{-a}$ for every $x>0$.

The paper closes with "for some constant $k$, $\mathbb P\big(c(S(i))\ge\tfrac{\varepsilon}{2}g_+(d(i))\big)\le k\,d(i)\,(g_+(d(i)))^{-a}$, whence the claim."

Significance

The theorem turns the deterministic criterion of Lemma B.1 into a statement about typical networks. When degrees grow, $g_+(d)^{-a}$ decays, and the probability that no hub can reduce cost vanishes for any law with a power-bounded cost tail and a positive cost floor. This is the paper's evidence that hub-and-spoke structures are the economically stable outcome; the companion results of the paper (Theorem 3.1 on local restructuring, Theorem 3.10 on the star topology) are treated in sibling missions of this series.

The result is proved in the paper, in about half a page. It has no machine-checked proof. Formalizing it makes the quantifier structure explicit, in particular that $k$ does not depend on the network, settles the boundary cases the paper leaves implicit, and records corrected forms of two axioms that are unsatisfiable as printed. Lemma B.1 is shared with the mission on Theorem 3.8.

Difficulty

The probabilistic estimates are elementary; the obstacles are in the bookkeeping. Lemma B.1 compares two costs on different node sets (the hermetized network has one more node), and its degrees and channel sizes must be read in the subnetwork induced on $U$; with the degrees of the whole network the lemma is false. To apply it to a random network one must choose $U$: the set of all nodes fails when some node is isolated, because $s(i)$ is then undefined. The step from the strict tail $\mathbb P(c>x)$ of (i) to the weak tail $\mathbb P(c\ge x)$ used in (12)–(13) is a limit the paper does not write out. The inverse $g_+^{-1}$ that the paper uses need not exist, since $g_+$ is not assumed onto.

Formalization scope

Nodes are an arbitrary finite type V; the LN is Λ : V → V → ℝ, anti-symmetric; the channel graph is E : SimpleGraph V, with $\lambda_{i,j}(\omega)\ne0\iff ij\in E$ for every $\omega$, and $d(i)$ is E.degree i. The cost is the $\tfrac12\sum_{i,j}$ form. The hub $v_0$ of a hermetization is none : Option V. Probabilities are toReal of a probability measure, and events are not assumed measurable. Each $\lambda_{i,j}$ is assumed measurable in the goal. The conventions committed to:

• (SA) is used for all $x,y>0$: as printed ("for $x>y\ge0$") it demands $c(x)<c(x)$ at $y=0$. The corrected range is the one Appendix D verifies.
• (SA+) is used for $k>1$, $x>0$: as printed ($k\in\mathbb R_+$) it fails at $x=0$, and for $k\le1$ even for the paper's own example.
• Every condition $d>g_+^{-1}(y)$ is written $g_+(d)>y$.
• In Lemma B.1, $d$, $s$, $S$ are those of the subnetwork induced on $U$; $U$ is nonempty and each $i\in U$ has a channel in $U$. For a node without a channel, $s$ and $S$ take the junk value $0$, which no statement uses.
• The constants $a,b,\varepsilon$ are common to all channels. Neither independence nor identical distribution of the flows is assumed: the theorem's hypotheses are only (i) and (ii).
• The goal assumes at least one channel. With none, the printed bound is $1$ but the cost $0$ cannot be reduced.

The following formalizations are trivializing and are ruled out: a $k$ allowed to depend on $V$, $E$, $\mathbb P$, $\Lambda$, $c$ or $g_+$ (take $k$ large enough that the bound is $\le0$); a specific law, such as a Pareto law, or a specific cost such as $c(x)=\sqrt{|x|}$; replacing "the LN is hermetizable" by the event that every node satisfies Lemma B.1's inequality; an empty channel set; and the printed, unsatisfiable (SA) or (SA+), under which every statement is vacuous.

The development needs finite sums over Option V, a min/max over a node's channels, and union bounds for outer measures (Mathlib's measure_biUnion_finset_le). Contributions welcome: proofs of the milestones, a proof that the corrected axioms are satisfiable by $c(x)=\sqrt{|x|}$, $g_+(k)=k^{1/4}$, and a reusable statement of Lemma B.1 for the series.

Selected references

• P. Guasoni, G. Huberman, C. Shikhelman, Lightning Network Economics: Topology, SSRN working paper 4439190, version of February 3, 2023. https://ssrn.com/abstract=4439190 ; published in Management Science, 2024, https://doi.org/10.1287/mnsc.2023.03872
• P. Guasoni, G. Huberman, C. Shikhelman, Lightning Network Economics: Channels, 2022 (cited in the paper as [GHS22]; reference list, p. 16 of SSRN 4439190).
• J. Poon, T. Dryja, The Bitcoin Lightning Network: Scalable Off-Chain Instant Payments, 2016. https://lightning.network/lightning-network-paper.pdf