Operations Research

Learning to bid in first-price auctions

Display advertising has been moving from second-price to first-price auctions: several exchanges began rolling them out in 2017, and Google Ad Manager completed its move at the end of 2019 (Davies 2019). In a second-price auction bidding one's value is a dominant strategy; in a first-price auction the optimal bid depends on the distribution of the competing bids, which a bidder does not know and must learn from repeated play. Most of the learning literature on auctions takes the seller's side of the second-price auction (reserve prices, e.g. Cesa-Bianchi, Gentile, Mansour 2015); on the bidder's side of the first-price auction, the main prior approach is the cross-learning framework of Balseiro et al. 2019.

Han, Zhou and Weissman (arXiv:2003.09795) study the bidder's problem with the feedback that ad exchanges actually provide, where only the winning price is announced, and with no assumption on the distribution of the competing bids. Their two upper bounds are $\widetilde O(\sqrt T)$ regret: Theorem 1 for iid private values and Theorem 2, the subject of this mission, for values chosen by an oblivious adversary. A matching $\Omega(\sqrt T)$ lower bound holds even under full information (Theorem 9).

Setting

A single bidder plays $T$ rounds. In round $t$ she observes a private value $v_t\in[0,1]$, bids $b_t\in[0,1]$, and wins if $b_t\ge m_t$, where $m_t\in[0,1]$ is the highest other bid (HOB). Her payoff is (1)

$$r(v_t,b_t;m_t)=(v_t-b_t)\,\mathbb 1(b_t\ge m_t).$$

The HOBs are iid with an unknown cumulative distribution function $G(x)=\mathbb P(m_t\le x)$ on $[0,1]$; $G$ may be discrete, continuous or mixed. Feedback is censored: after round $t$ only $\max\{b_t,m_t\}$ is revealed, so $m_t$ is observed only when the bidder loses. The expected reward is $R(v,b)=(v-b)G(b)$, and the regret of a policy $\pi$ against the value sequence $v=(v_1,\dots,v_T)$ is (3)

$$R_T(\pi;v)=\sum_{t=1}^T\Big(\max_{b\in[0,1]}R(v_t,b)-R(v_t,b_t)\Big),$$

the shortfall against an oracle that knows $G$. A policy bids in round $t$ as a (possibly randomized) function of $v_1,\dots,v_t$ and of the feedback of rounds $1,\dots,t-1$. An oblivious adversary fixes the whole value sequence in advance, independently of the bids and the HOBs.

The policy analysed is ML-IS-UCB (Algorithm 4). It restricts bids to the grid $b^i=(i-1)/K$, $i\in[K]$, with $K=\lceil\sqrt T\rceil$; it splits time into $L=\lceil\log_2T\rceil$ levels after an initialization phase of $T_0=(L+1)\lceil\sqrt T\rceil$ zero bids; and at each level it computes a width $w^\ell_{i,t}$, an interval-splitting reward estimate $\hat r^\ell_{i,t}$ and a candidate set $\mathcal B^\ell_t$ by the displays (12)–(16).

Formalization targets

Goal: Theorem 2

There is an absolute constant $C>0$ such that for every $T\ge2$ some policy $\pi$ satisfies, for every value sequence $v\in[0,1]^T$ and every $G$ on $[0,1]$,

$$\mathbb E\big[R_T(\pi;v)\big]\le C\sqrt T\log^3T .$$

The constant is unspecified, so the goal survives any improvement of the constants below.

The explicit bound: Theorem 7

For every $\gamma\ge3$, the ML-IS-UCB policy satisfies

$$\mathbb E\big[R_T(\pi^{\mathrm{ML\text{-}IS\text{-}UCB}};v)\big]\le4+(L+4)\lceil\sqrt T\rceil+80\gamma^{3/2}\log(LKT)(1+\log T)\,L\sqrt T .$$

Milestones

In the order of the proof (Section 4.3 and Appendix C):

1. Lemma 7: with probability at least $1-4T^{-3}$, $|\hat r^\ell_{i,t}-r_{i,t}|\le w^\ell_{i,t}$ for all $i,\ell$ and $T_0<t\le T$, and $w^\ell_{i,t}$ is bounded by (18) in terms of the true interval probabilities $p_j=G(b^{j+1})-G(b^j)$.
2. Lemma 8: on that event the best grid bid is never eliminated, and a round assigned to level $\ell$ has regret at most $8\cdot2^{-\ell}$ against the grid.
3. Display (19): the grid regret is at most $T_0+8\sum_\ell2^{-\ell}|\Phi^\ell(T)\cap(T_0,T]|$.
4. Lemma 16: a deterministic counting bound for the sums $\sum_t\sum_{j\ge i(t)}v_j/n^\ell_{j,t}$.
5. Lemma 9: $2^{-\ell}|\Phi^\ell(T)\cap(T_0,T]|\le10\gamma^{3/2}\log(LKT)(1+\log T)\sqrt T$.
6. Theorem 7.

A supporting item, not a milestone, states the quantization step $\max_{b\in[0,1]}R(v,b)\le\max_iR(v,b^i)+1/K$ for the grid of Algorithm 4.

Significance

The result shows that adversarial values cost at most a logarithmic factor relative to iid values in repeated first-price auctions with censored feedback, and that no regularity of $G$ is needed. ML-IS-UCB is also an algorithmic template: its widths are computed before the data of the current level is used, which makes the estimates at each level independent of the bids that select them, and its interval-splitting estimator uses the variance of each interval rather than a uniform bound. Remark 3 notes that replacing the interval probabilities by $1$ gives only $\widetilde O(\sqrt{KT})$.

All results of the paper are proved in the preprint; none of them is machine-checked. A complete development formalizes a multi-level elimination algorithm with data-dependent level assignment, a Bernstein-type concentration argument for estimates indexed by random sets, and the counting lemma behind the logarithmic factors. Each of these is reusable for other elimination-based bandit algorithms.

Difficulty

The obvious route is a single UCB index per grid bid, (11) on p. 27, built from all past observations through the estimates $\hat p^t_j=\sum_{s\le t}\mathbb 1(b_s\le b^j)\mathbb 1(m_s\in(b^j,b^{j+1}])/\sum_{s\le t}\mathbb 1(b_s\le b^j)$. It fails because $\hat p^t_j$ is not a normalized binomial variable: each bid depends on the earlier HOBs, so conditioned on the bids the HOBs are no longer independent and $\hat p^t_j$ is not even unbiased. Self-normalized martingale bounds control each $\hat p^t_j$ separately but not the sum $\sum_{j\ge i}\hat p^t_j$ that the reward estimate needs. Algorithm 4 restores conditional independence through its level structure, and Lemma 7 has to make that precise: the sets $\Phi^\ell(t)$ are random, and the bound must hold uniformly over all $(i,\ell,t)$ with a variance term estimated from a held-out sample. Lemma 9 then needs the variance-sensitive width (18); a crude width loses a factor $\sqrt K$ (Remark 3).

Formalization scope

• Model. Rounds are Fin T; Lean round $t$ is paper time $t+1$. The HOB law is a probability measure μG on ℝ with μG [0,1]ᶜ = 0, and $G(x)$ is (μG (Set.Iic x)).toReal; atoms are allowed. The maximum in (3) is a supremum over $[0,1]$.
• Policies. A policy has internal randomness $u\sim\mu_U$ and, for each $u$, a bidding rule whose round-$t$ bid receives only the values of rounds $\le t$ and the feedback $\max\{b_s,m_s\}$ of rounds $<t$, enforced by the argument types; bids lie in $[0,1]$ and are jointly measurable. The expectation is a Bochner integral over $u$ and $m\sim G^{\otimes T}$, and Theorems 2 and 7 also assert integrability, so the integral cannot be a junk value.
• Algorithm 4. Grid indices are 0-based ($b^{i+1}=i/K$, $b^{K+1}=1$); inside the algorithm times are the paper's $1,\dots,T$. Every quantity $n,w,\hat p,\hat r,\mathcal B$ is defined by its formula for every $(i,\ell,t)$. The estimators (14) and $\hat p^0$ are computed from the feedback, not from $m$, and the algorithm recomputes its own past decisions, so it is a censored-feedback rule. "An arbitrary $i$" is a selection rule depending on the time and the level only. If no level breaks (impossible for $\gamma\ge3$, $T\ge2$) the round goes to level $L$ with bid $0$.
• Hypotheses added to the printed statements, each disclosed in its item: $T\ge2$ in Theorem 2 (the printed bound is $0$ at $T=1$); Lemmas 8, 9 and (19) are stated pathwise under the inequalities of Lemma 7 that their proofs use; Lemma 16 assumes that the set contains $\lceil\sqrt T\rceil$ initialization rounds with bid $0$, which its proof uses; the quantization display is adapted from the grid of Lemma 4 to that of Algorithm 4.
• Ruled out. A policy that reads $m_t$, $G$ or future values, a constant $C$ chosen after $T$, $v$ or $G$, a policy chosen after $v$ or $G$, and an expectation of a non-integrable function would each make the goal trivial; the statements exclude all four.
• Needed and welcome. Bernstein and multiplicative Chernoff bounds for binomial variables (Lemmas 14, 15 of the paper are cited from the literature), measurability of the run of the algorithm, and the harmonic-sum bound $\sum_{k=a}^T1/k\le1+\log T$. Contributions toward any milestone, or alternative proofs of the goal, are welcome.

Selected references

• Y. Han, Z. Zhou, T. Weissman, Optimal No-regret Learning in Repeated First-price Auctions, Operations Research, 2025; preprint arXiv:2003.09795v7, 2024. https://arxiv.org/abs/2003.09795
• N. Cesa-Bianchi, C. Gentile, Y. Mansour, Regret Minimization for Reserve Prices in Second-Price Auctions, IEEE Transactions on Information Theory 61(1), 2015. https://doi.org/10.1109/TIT.2014.2365772
• P. Auer, Using Confidence Bounds for Exploitation-Exploration Trade-offs, Journal of Machine Learning Research 3, 2002. https://www.jmlr.org/papers/v3/auer02a.html
• S. Balseiro, N. Golrezaei, M. Mahdian, V. Mirrokni, J. Schneider, Contextual Bandits with Cross-Learning, NeurIPS 2019. https://arxiv.org/abs/1809.09582
• J. Davies, What to know about Google's implementation of first-price ad auctions, Digiday, 2019. https://digiday.com/media/buyers-welcome-auction-standardization-as-google-finally-goes-all-in-on-first-price/

Motivation

A bidder in repeated first-price auctions faces a learning problem with two kinds of side information. Their private value is a context that changes every round, and the outcome of one bid reveals something about other bids (graph feedback across actions) and about other values (cross learning across contexts). Han, Zhou and Weissman (arXiv:2003.09795v7) abstract this structure into partially ordered contextual bandits and show that, when contexts are iid, an arm-elimination policy has regret $\widetilde O(\sqrt{\alpha\beta T})$ (Theorem 5), with no polynomial dependence on the number of contexts or actions.

Theorem 6 of the same paper asks whether this survives when contexts are chosen by an adversary. It does not: with adversarial contexts every policy suffers regret polynomial in $\min\{\alpha M, K\}$. This separation is what forces the paper to look beyond the partially ordered structure for its $\widetilde O(\sqrt T)$ adversarial-value result (Theorem 2). The lower bound is also of independent interest for contextual bandits with cross learning (Balseiro et al., NeurIPS 2019) and with feedback graphs (Alon et al., COLT 2015).

Setting

A stochastic contextual bandit with graph feedback and cross learning (Definition 2, p. 14) has a horizon $T$, $M$ contexts $\mathcal C$, $K$ actions $\mathcal A$, a joint reward law $P$ on $[0,1]^{\mathcal C\times\mathcal A}$ with means $R_{c,a}$, and a directed graph $G=(\mathcal A,E)$ without self-loops. In round $t$ the learner sees a context $c_t$, picks $a_t$, nature draws a fresh reward vector $r_t\sim P$, and the learner observes $r_{t,c,a}$ for every context $c$ and every $a\in I_t=\{a_t\}\cup\{a:(a_t,a)\in E\}$. The regret (5) is

$$R_T(\pi)=\sum_{t=1}^T\Big(\max_{a\in\mathcal A}R_{c_t,a}-R_{c_t,a_t}\Big).$$

The independence number $\alpha$ of $G$ is the size of a largest set of actions with no edge between any two of them; for a partial order, $\beta$ is the size of a largest set of pairwise incomparable elements.

The instance is a partially ordered contextual bandit (Definition 3, pp. 16–17) if $G$ is a DAG equal to its own transitive closure, so that $a_1\preceq_G a_2$ iff $a_1=a_2$ or $(a_1,a_2)\in E$ is a partial order, and there is a partial order $\preceq_{\mathcal C}$ on contexts with $c_1\preceq_{\mathcal C}c_2\Rightarrow a^\star(c_1)\preceq_G a^\star(c_2)$ for optimal actions $a^\star(c)\in\arg\max_a R_{c,a}$.

A policy $\pi$ chooses $a_t$ from its internal randomness, the contexts $c_1,\dots,c_t$ and the earlier observations. The context sequence is oblivious: fixed in advance, possibly depending on $\pi$ but not on its random draws.

Formalization targets

Goal: Theorem 6 in the regime of its proof

For integers $\alpha\ge1$, $M\ge1$, with $K=(\alpha+1)M$, $K^3\le T$ and $M\mid T$: there is a feedback graph $G$ on $K$ actions with independence number $\alpha$ such that for every policy $\pi$ there are a reward law $P$ (making $(G,P)$ partially ordered with the total order on contexts, $\beta=1$) and contexts $(c_t)$ with

$$\mathbb E[R_T(\pi)]\ \ge\ \frac{\sqrt{KT}}{32e^3}.$$

Because $\alpha M\le K$, this is at least $\frac1{32e^3}\min\{\sqrt{\alpha MT},\sqrt{KT},T^{2/3}\}$, the printed form of Theorem 6, in this regime.

Milestones

Along the proof (pp. 22–24): the construction is a partially ordered contextual bandit with $\beta=1$ and independence number $\alpha$; properties 1–4 of the mean rewards; property 5, the KL divergence of the observed rewards; the regret decomposition (7); the testing lemma (Lemma 13, p. 36)

$$\frac1n\sum_{i=1}^nQ_i(\Psi\ne i)\ \ge\ \frac1{2n}\sum_{i=2}^n e^{-D_{\mathrm{KL}}(Q_1\|Q_i)};$$

the self-referential inequality (8)

$$R_T\ \ge\ \frac{\sqrt{KT}}{16e^3}\exp\Big(-\frac{16KR_T}{3T}\Big),\qquad R_T=\max_u\mathbb E_u[R_T(\pi)];$$

and the final step $R_T\ge\sqrt{KT}/(32e^3)$.

Significance

The theorem separates stochastic from adversarial contexts. Under iid contexts, Theorem 5 gives $\widetilde O(\sqrt{\alpha\beta T})$; with adversarial contexts, even when $\beta=1$, regret must grow like $\sqrt{\alpha MT}$, matching the upper bound of Theorem 4 up to logarithms. For first-price auctions with adversarial values (Remark 2), the bound shows that the partially ordered structure alone cannot give $\widetilde O(\sqrt T)$; the paper's $\widetilde O(\sqrt T)$ algorithm must use the extra correlation of auction rewards.

The paper proves the theorem in full. As far as we know, none of it has been formalized; in particular, no machine-checked version of a Bayesian multi-hypothesis lower bound for bandits with graph feedback and cross learning exists. A formal proof will produce reusable pieces: Lemma 13 is a general testing inequality; the KL chain rule for adaptively collected bandit observations, with feedback revealed on a graph, is needed for any information-theoretic bandit lower bound; and the interaction model is shared with the paper's upper bounds.

Difficulty

The standard minimax argument for $K$-armed bandits compares two instances that differ in one arm, and the regret follows directly from a testing error. Here that argument fails: feedback graphs and cross learning mean that pulling one arm can reveal everything, and a policy may pay to explore. The proof instead plays a uniform prior over $(\alpha+1)^M$ instances and obtains an inequality in which the maximal regret $R_T$ appears on both sides, (8). If the regret is small, the policy has not explored enough to tell the instances apart, which in turn forces large regret. Making this rigorous requires the chain rule of KL divergence over the adaptively chosen observations, the specific ordering of contexts (decreasing over blocks, so early observations say nothing about late optimal actions), and the regime $K^3\le T$ to close the self-referential bound.

Formalization scope

• Contexts are Fin M, rounds Fin T (paper index = Lean index + 1). The goal uses actions Fin K; the construction uses Fin M × Fin (α + 1), with $j=0$ the action $(i,0)$.
• A reward law is a measure on Fin M → A → ℝ. Definition 2 requires a probability measure carried by $[0,1]^{M\times K}$ and a graph without self-loops. Means are integrals, and $\max_a$ is a supremum over the finite action set.
• Definition 3's "DAG equal to its transitive closure" is encoded as "no self-loops and transitive". The printed $\arg\max$ is read as a selection of maximisers.
• Independence numbers are exact: a set of the given size exists, and none is larger.
• Policies are randomized and non-anticipating. The action is a measurable function of the internal randomness (an arbitrary probability space), the contexts so far and the past observations, and the argument types enforce non-anticipation. An observation is the reward vector with unrevealed coordinates set to $0$; the learner knows its own action, so this carries exactly the revealed rewards. Deterministic-only policies would give a weaker theorem, and they are not the class used.
• Expected regret integrates over the internal randomness and iid reward vectors, with the context sequence fixed.
• KL divergence is Mathlib's $[0,\infty]$-valued klDiv. In Lemma 13, $e^{-\infty}$ is read as $0$, so an infinite divergence cannot be truncated to $0$ and inflate the right side.
• The reduction from general $(M,K,T)$ by "dummy contexts and actions" (p. 21) is not formalized. It needs $\min\{K,(\alpha+1)M,T^{1/3}\}\ge\alpha+1$, and the printed theorem is false at $K=1$. The hypotheses $M\mid T$ and $\alpha\ge1$ replace the paper's "without loss of generality".
• Property 5 assumes $u_c\neq0$, because for $u_c=0$ the two laws coincide. (7) is stated for each $u$, which implies the printed form for the maximum.

Needed infrastructure: Bernoulli product measures and their KL divergence, the KL chain rule for the law of an adaptive interaction, and a Bretagnolle–Huber-type inequality. Contributions of these general lemmas, and of the measurability facts for the interaction, are welcome.

Selected references

• Y. Han, Z. Zhou, T. Weissman, Optimal No-regret Learning in Repeated First-price Auctions, Operations Research, 2025; preprint arXiv:2003.09795v7. https://arxiv.org/abs/2003.09795
• Z. Gao, Y. Han, Z. Ren, Z. Zhou, Batched Multi-armed Bandits Problem, NeurIPS 2019 (source of Lemma 13). https://arxiv.org/abs/1904.01763
• S. Balseiro, N. Golrezaei, M. Mahdian, V. Mirrokni, J. Schneider, Contextual Bandits with Cross-learning, NeurIPS 2019. https://arxiv.org/abs/1809.09582
• N. Alon, N. Cesa-Bianchi, O. Dekel, T. Koren, Online Learning with Feedback Graphs: Beyond Bandits, COLT 2015. https://arxiv.org/abs/1502.07617
• A. B. Tsybakov, Introduction to Nonparametric Estimation, Springer, 2009. https://doi.org/10.1007/b13794

Why hubs appear in payment-channel networks

The Lightning Network (LN) is a layer-two payment system for Bitcoin. Two parties open a payment channel by locking funds on the blockchain and can then pay each other off-chain; payments between parties without a common channel are routed along paths of channels. Locking funds is costly, and the amount a channel needs grows with the net flow it has to carry. Guasoni, Huberman and Shikhelman (SSRN 4439190, version of February 3, 2023; published in Management Science, 2024) ask which network topologies support a given pattern of payments at least cost, using only qualitative properties of the channel cost derived in their earlier work on channel sizing (Guasoni, Huberman and Shikhelman, Lightning Network Economics: Channels, 2022, cited in the paper as [GHS22]).

One of the paper's central findings is that adding a new hub node, and routing the traffic of a group of nodes through it, reduces cost in a broad class of networks. This explains, from cost considerations alone, why hub-and-spoke structures emerge in deployed payment-channel networks. This mission formalizes the deterministic sufficient condition for that phenomenon (Theorem 3.8) and the chain of lemmas in Appendix B.1 that proves it.

Setting

Fix a finite set $V$ of nodes. A Lightning Network is an anti-symmetric real matrix $\Lambda=(\lambda_{i,j})_{i,j\in V}$: $\lambda_{u,v}$ is the net flow from $u$ to $v$ in the channel between them, $\lambda_{u,v}=-\lambda_{v,u}$, and $\lambda_{u,v}=0$ means there is no channel.

A channel cost is a function $c:\mathbb R\to\mathbb R_+$ that is strictly increasing on $[0,\infty)$ (MO), even (SY), zero at zero (CI), and strictly subadditive, $c(x+y)<c(x)+c(y)$ for $x,y>0$ (SA). It satisfies (SA+) with a nonnegative, strictly increasing $g_+$ on $[0,\infty)$ if $c(kx)<\tfrac{k}{g_+(k)}\,c(x)$ for all $k>1$, $x>0$: when the flow of a channel grows $k$-fold, its cost grows by at most $k/g_+(k)$. The cost of the network is $c(G)=\tfrac12\sum_{i,j}c(\lambda_{i,j})$.

For a node $v$ and a set $U$ of nodes, $d_U(v)$ is the number of channels of $v$ into $U$, $s_U(v)$ the smallest and $S_U(v)$ the largest absolute flow of these channels, $\delta(U)=\min_{v\in U}d_U(v)$ the minimum degree, and $\mathrm{disc}(U)=\max_v c(S_U(v))/c(s_U(v))$ the discrepancy, the maximum over nodes of $U$ with a channel in $U$. For $U=V$ these are $d(v)$, $s(v)$, $S(v)$, $\delta(G)$, $\mathrm{disc}(G)$, and $\bar d(G)=\sum_v d(v)/|V|$ is the average degree.

The hermetization of $U$ deletes all channels among nodes of $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 $U$; every node keeps its net flow. $U$ is hermetizable if hermetization strictly reduces the cost, and the network is hermetizable if some $U$ is.

Formalization targets

Goal: Theorem 3.8 (existence part)

Under (MO)–(SA+), every network with at least one channel and

$$\bar d(G)\;>\;2\,g_+^{-1}\big(2\,\mathrm{disc}(G)\big)$$

is hermetizable. The cost function and $g_+$ are arbitrary subject to the axioms.

Milestones

1. Lemma B.1. A nonempty $U$ is hermetizable if $d_U(i)>g_+^{-1}\big(2c(S_U(i))/c(s_U(i))\big)$ for every $i\in U$.
2. Lemma B.2. A nonempty $U$ is hermetizable if $\delta(U)\ge g_+^{-1}\big(2\,\mathrm{disc}(U)\big)$.
3. Lemma B.4. A finite graph of average degree at least $2d$, $d>0$, has a nonempty induced subgraph $G'$ with $\delta(G')>d$.
4. Lemma B.3 (the peeling procedure). Repeatedly deleting every vertex with at most $t$ neighbours among the remaining vertices returns the largest vertex set inducing minimum degree $>t$; it is empty exactly when no such set exists.

Significance

Theorem 3.8 turns a qualitative property of channel costs into a checkable topological criterion: if a network is dense relative to how unequal its channel flows are, a cost-reducing hub exists. The paper uses it to argue that such restructuring is profitable for an intermediary who charges part of the savings, and its probabilistic companion (Theorem 3.9) shows that random networks whose channel costs have light tails are hermetizable with high probability. The degree-to-subgraph Lemma B.4 is a standard tool of extremal graph theory (Diestel, Graph Theory, Prop. 1.2.2), and Lemma B.3 is the classical $k$-core peeling.

Mathematically the result is proved in the paper. None of it is formalized: Lean's Mathlib has minimum degree and induced subgraphs but neither Lemma B.4 nor the correctness of $k$-core peeling, and there is no formal model of payment-channel networks or of hermetization. The mission produces that model, machine-checked versions of the Appendix B.1 lemmas, and a statement of Theorem 3.8 under axioms that are actually satisfiable (see below).

Difficulty

The cost comparison in Lemma B.1 is node by node: the channels of a node inside $U$ are replaced by one channel to the hub carrying their sum. The obvious bound on the hub channel's cost uses only monotonicity and subadditivity, and that is too weak: a single channel carrying the sum of $d$ flows can cost almost as much as the $d$ channels it replaces, while the deleted channels are each shared by two nodes. The quantitative axiom (SA+) is what makes the comparison strict, and the discrepancy controls how unequal the replaced flows may be.

Passing from the average degree of the whole network to a subnetwork in which every node has high degree is the second step, and it must keep track of the fact that the discrepancy of an induced subnetwork can be smaller but never larger than that of the network. Lemma B.4 needs an argument that the deletion process cannot exhaust the graph; a counting argument that treats every deleted vertex alike loses exactly the margin needed.

Formalization scope

Nodes form an arbitrary finite type V; the network is Λ : V → V → ℝ with anti-symmetry IsLN. The hub is the extra element none of Option V. The cost is the $\tfrac12\sum_{i,j}$ form. In Lemmas B.1 and B.2 all degree data are those of the subnetwork induced on $U$; in Theorem 3.8 those of the whole network. $s(v)$ has the junk value $0$ for a node without channels, so every statement assumes the relevant nodes have a channel, and the discrepancy is a maximum over nodes having a channel.

Two axioms are corrected from the printed page and the correction is part of the statement. (SA) is printed for $x>y\ge0$, which at $y=0$ reads $c(x)<c(x)$; it is stated for all $x,y>0$, the form the paper's Appendix D verifies. (SA+) is printed for all $k\in\mathbb R_+$, which fails at $x=0$ and, for the paper's own example cost, at every $k\le1$; it is stated for $k>1$, $x>0$. Under the printed axioms every theorem would hold vacuously.

$g_+$ is strictly increasing but not assumed onto, so $g_+^{-1}$ is replaced throughout by the equivalent $g_+$-form: $d>g_+^{-1}(y)$ becomes $g_+(d)>y$, as in the paper's own proof of Lemma B.1. Theorem 3.8 therefore assumes $g_+(\bar d(G)/2)>2\,\mathrm{disc}(G)$ and, explicitly, that the network has a channel (implied by the printed hypothesis). Lemma B.4 adds $d>0$ and reads "average degree $2d$" as "at least $2d$", as its proof does. The polynomial-time clause of Theorem 3.8 and the $O(V+E)$ bound of Lemma B.3 are complexity claims and are not formalized; Lemma B.3 is posed as correctness of the procedure in its proof, which finds minimum degree $>t$ (the printed statement says $\ge t$).

Formalizations that would trivialize the mission are excluded: a specific cost such as $c(x)=2(B|x|/r)^{1/2}$ or a specific $g_+$; hermetizability defined by the per-node inequality instead of the cost comparison; Theorem 3.8 with the empty set allowed to witness hermetizability (the strict cost decrease rules it out); Lemma B.4 without nonemptiness; and Lemma B.3 as "there exists an algorithm".

The definitions (network, cost axioms, degree data, hermetization, peeling) are reusable by the companion missions on this paper. Proofs of any milestone are welcome, Lemma B.4 and Lemma B.3 being independent of the network model.

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 (theorem numbers here follow the SSRN version).
• P. Guasoni, G. Huberman, C. Shikhelman, Lightning Network Economics: Channels, 2022 (cited in the paper as [GHS22]; no stable link is given there).
• R. Diestel, Graph Theory, 5th ed., Springer, 2017, Proposition 1.2.2. https://doi.org/10.1007/978-3-662-53622-3
• J. Poon, T. Dryja, The Bitcoin Lightning Network: Scalable Off-Chain Instant Payments, 2015. https://lightning.network/lightning-network-paper.pdf

Lending to sellers on a marketplace

Online marketplaces such as Amazon, Alibaba and JD.com host millions of third-party sellers, many of them small firms without the working capital to pay their suppliers upfront. Two sources of credit compete for them. In trade credit the supplier ships the goods and is paid at the end of the season, bearing the risk that the seller cannot repay. In platform financing the marketplace itself lends the purchase cost to the seller at an interest rate $r$ of its choosing, the supplier is paid immediately, and the platform bears the default risk. Platform lending programmes (the Amazon Lending Program, launched in 2011; the financial affiliates of Alibaba and JD.com) put the marketplace in the lender's seat. Supply-chain finance research, from Buzacott and Zhang (2004) to Kouvelis and Zhao (2012), studies who should finance a capital-constrained firm; the platform adds a lender that also earns a commission on the borrower's sales, and the question becomes when lending benefits the platform, its sellers and their suppliers.

Huang, Lai, Wang and Xiao study this question in a stylized supply chain with a random market-clearing price and a limited-liability seller. They obtain closed-form equilibria for both schemes and compare the three parties' profits. This mission concerns the platform's side of that comparison: for which loan rates the platform itself earns more by lending than by leaving credit to the supplier.

The version formalized here is the authors' manuscript posted on SSRN (abstract 4014045), titled Lending to Third-party Sellers with Platform Loan. The paper was published in Management Science in 2024 under the title Platform Financing vs. Trade Credit for Lending to Third-Party Sellers. All page and label references are to the SSRN manuscript.

The model

A supplier produces at unit cost $c>0$. A seller with no capital orders $q\ge0$ units and sells all of them at the market-clearing price $p=\tilde a-q$, where the market size $\tilde a$ is uniform on $[a-\delta,a+\delta]$ with $0<\delta<a$. The platform keeps the share $\varphi\in[0,1)$ of the revenue and passes $(1-\varphi)pq$ to the seller. The supplier's and the platform's capital cost is the risk-free rate $r_f\ge0$, and $(1-\varphi)a>c(1+r_f)$. The seller has limited liability: if her revenue does not cover what she owes, she hands over all of it.

• Trade credit. The supplier sets a deferred wholesale price $w$; the seller orders $q$; at the end the seller pays $\min\{(1-\varphi)pq,\,wq\}$. The seller earns $\mathbb E[((1-\varphi)(\tilde a-q)q-wq)^+]$, the supplier $\mathbb E[\min\{(1-\varphi)(\tilde a-q)q,wq\}]-cq(1+r_f)$, and the platform $\Pi^T_p=\mathbb E[\varphi(\tilde a-q)q]$.
• Platform financing at rate $r$. The supplier sets an upfront price $w$; the seller orders $q$ with a loan $wq$ from the platform and repays $\min\{(1-\varphi)pq,\,wq(1+r)\}$. The seller earns $\mathbb E[((1-\varphi)(\tilde a-q)q-wq(1+r))^+]$, the supplier $(w-c)q(1+r_f)$, and the platform

$$\Pi^P_p=\mathbb E\big[\varphi(\tilde a-q)q+\min\{(1-\varphi)(\tilde a-q)q,\;wq(1+r)\}-wq(1+r_f)\big].$$

Each scheme is a two-stage Stackelberg game solved by backward induction: a profile is a price $w$ and an order rule $w\mapsto q(w)$, and a subgame-perfect equilibrium has the seller best-responding at every price and the supplier choosing the price that maximizes his profit given that rule. $\Pi^T_p$ and $\Pi^P_p(r)$ denote the platform's profits along the equilibrium paths.

Formalization targets

Goal: Proposition 7 (p. 19)

Let

$$\delta_2=\frac{(1-\varphi)a-c(1+r_f)}{(2+\sqrt6)(1-\varphi)},\qquad r_1=\frac{(1-\varphi)(a-(\sqrt6+2)\delta)}{c}-1,\qquad \bar c=\frac{a(1-\varphi)^2}{1+r_f},$$ $$r_6=\frac{\sqrt{8a^2(2-\varphi)(1-\varphi)^3+\varphi^2(2a(1-\varphi)+c(1+r_f))^2}-2a(1-\varphi)\varphi-c(4+r_f\varphi-\varphi)}{2c(2-\varphi)},\qquad r_5=\min\{r_1,r_6\}.$$

For $\delta\le\delta_2$:

$$c\le\bar c\;\Longrightarrow\; r_6\ge r_f\ \text{ and }\ \Pi^P_p(r)>\Pi^T_p\ \text{ for all } r_f<r<r_5,$$ $$c>\bar c\;\Longrightarrow\; r_6<r_f\ \text{ and }\ \Pi^P_p(r)>\Pi^T_p\ \text{ for all } r>-1,\ r_6<r<r_f .$$

Milestones

1. Lemma 1 (p. 10): the seller's unique best response to an owed amount $W<(1-\varphi)(a+\delta)$.
2. Proposition 1 (p. 11): existence and closed form $(w^T,q^T)$ of the trade-credit equilibrium.
3. (9) (p. 41): $\Pi^T_p=\varphi(a(1-\varphi)-c(1+r_f))(3a(1-\varphi)+c(1+r_f))/(16(1-\varphi)^2)$ for $\delta\le\delta_1$.
4. Lemma 2 (p. 13): Lemma 1 with $W=w(1+r)$.
5. Proposition 2 (p. 13): existence and closed form $(w^P,q^P)$ of the platform-financing equilibrium at rate $r$.
6. (10) (p. 41): the closed form of $\Pi^P_p(r)$ for $\delta\le\delta_r$.

Significance

Proposition 7 identifies two distinct reasons a platform lends. When production is cheap ($c\le\bar c$) the platform gains by charging slightly more than its capital cost, earning interest while sales barely fall. When production is expensive ($c>\bar c$) it gains by subsidizing the loan below $r_f$: the lower rate raises the seller's order enough that the larger commission outweighs the interest forgone. Combined with the paper's Proposition 6, which shows that rates below $r_f$ can make both seller and supplier better off at low uncertainty, the second case is a regime in which platform financing benefits all three parties. The paper's §5 uses the same comparison to derive the platform's optimal rate.

The result is proved in the manuscript; it has not been machine-checked. A formalization adds three things. It certifies the closed-form equilibria of both games under limited liability, including uniqueness up to the paper's tie-breaking conventions. It verifies the radical algebra behind $r_6$ and the sign of $\Pi^P_p-\Pi^T_p$ on each side of $r_f$. And it records the model precisely enough for the companion missions of this paper (seller and supplier comparisons; the endogenous rate) to be checked against the same objects.

Difficulty

The comparison itself is algebra once (9) and (10) are known, and an obvious approach would start from those formulas. The difficulty is that they are statements about equilibria of games, not definitions. Each requires maximizing an expectation of a positive part (the seller) or of a minimum (the supplier, the platform) over an interval in which default can or cannot occur. The seller's objective is piecewise polynomial in $q$ with a kink where default first becomes possible, and global optimality, not just stationarity, must be shown. The supplier's problem then compares two local optima whose ordering changes at $\delta_1$ (trade credit) or $\delta_r$ (platform financing). On top of this the goal requires the threshold facts $r_6\ge r_f\iff c\le\bar c$ and the positivity of a quadratic in $r$ on the stated intervals, as well as checking that every rate in the intervals keeps the platform-financing equilibrium in its no-default branch ($r<r_1$).

Formalization scope

The expectation over $\tilde a$ is the normalized interval integral $(2\delta)^{-1}\int_{a-\delta}^{a+\delta}$; all integrands are continuous. Payoffs are stated with the literal revenue $(1-\varphi)(\tilde a-q)q$, and $\Pi^T_p$ is the expectation $\mathbb E[\varphi(\tilde a-q)q]$, not the page's closed form $\varphi(a-q)q$ (the two agree). A profile is a price together with the seller's whole order rule. Equilibria carry two tie-breaks, both the paper's own conventions: an indifferent seller with no profitable order orders zero (proofs of Propositions 1–2), and the supplier's equilibrium price is the least optimal one, which places $\delta=\delta_1$ and $\delta=\delta_r$ in the low-price branch as the propositions do. The goal quantifies over a trade-credit equilibrium and over a family of platform-financing equilibria, one for each rate satisfying conditions (ii)–(iii) of the Appendix ($r>-1$, $c(1+r)<(a+\delta)(1-\varphi)$).

Standing assumptions and pins: $0<\delta<a$ reads the page's assumption that the price is always positive; $\varphi<1$ is forced by $(1-\varphi)a>c(1+r_f)$; $c>0$ and $r_f\ge0$ read "production cost" and "risk-free rate". Lemmas 1–2 add $W<(1-\varphi)(a+\delta)$, outside which every order earns zero. Corrected slips: the $\delta>\delta_1$ branch of Proposition 1 on p. 11 omits a factor $\delta$ under the root, and the formalization uses the proof's form (p. 31). The proof of Proposition 7 writes $\delta<\delta_2$ where the statement has $\delta\le\delta_2$; the statement's form is used.

The page says only "there exist two thresholds $r_5$ and $r_6$", which an empty interval satisfies trivially. The goal therefore names the proof's thresholds and includes $r_6\ge r_f$ and $r_6<r_f$ in the two cases. Stating the goal about the closed forms (9)–(10) instead of equilibrium profits would also trivialize it; these appear only as milestones.

A complete development needs: optimization of piecewise-polynomial expectations on an interval (reusable for any newsvendor-type problem with a uniform demand), the backward-induction equilibria of both games, and real-radical inequalities. Proofs of any milestone, and of the sanity facts $\Pi^T_p=\varphi(a-q)q$, are welcome.

Selected references

• R. Huang, G. Lai, X. Wang, W. Xiao, Lending to Third-party Sellers with Platform Loan, SSRN working paper 4014045 (manuscript formalized here). https://ssrn.com/abstract=4014045
• R. Huang, G. Lai, X. Wang, W. Xiao, Platform Financing vs. Trade Credit for Lending to Third-Party Sellers, Management Science, 2024. https://doi.org/10.1287/mnsc.2022.00201
• J. A. Buzacott, R. Q. Zhang, Inventory Management with Asset-Based Financing, Management Science 50(9), 2004. https://doi.org/10.1287/mnsc.1040.0244
• P. Kouvelis, W. Zhao, Financing the Newsvendor: Supplier vs. Bank, and the Structure of Optimal Trade Credit Contracts, Operations Research 60(3), 566–580, 2012. https://doi.org/10.1287/opre.1110.1030

Motivation

In a first-price auction the highest bidder wins and pays her own bid. Display advertising moved to first-price auctions around 2019, and a bidder who participates in millions of them faces a learning problem: at each round $t$ she sees a private value $v_t\in[0,1]$ for the item, bids $b_t\in[0,1]$, and wins when $b_t$ is at least the highest other bid (HOB) $m_t$, earning $(v_t-b_t)\mathbb 1(b_t\ge m_t)$. Since the HOB is unknown, she must learn how much to shade her bid.

Han, Zhou and Weissman (arXiv:2003.09795v7, Operations Research, 2025) show that when the HOBs are iid draws from an unknown distribution, a bidder can achieve regret $\widetilde O(\sqrt T)$ against the oracle that knows the distribution, whether the values are iid or chosen by an oblivious adversary, and with only censored feedback. Their §2.2 justifies the iid assumption by the size of the bidder population, and notes that learning "could become impossible even when the iid assumption is only slightly violated". Section 5.2 makes this precise. This mission formalizes that impossibility result, Theorem 8.

Setting

Fix a horizon $T$. Values $v=(v_1,\dots,v_T)\in[0,1]^T$ form an oblivious sequence, fixed in advance. Fix two probability laws $P,Q$ on $[0,1]$ and a threshold $v^\star$. The HOBs are independent across rounds with

$$m_t\sim P\ \text{ if } v_t<v^\star,\qquad m_t\sim Q\ \text{ if } v_t\ge v^\star .$$

Feedback is full information: $m_t$ is revealed at the end of round $t$. The laws $P,Q$ are known to the bidder; only $v^\star$ is not.

The payoff of bid $b$ against HOB $m$ at value $v$ is $r(v,b;m)=(v-b)\mathbb 1(b\ge m)$ (ties are won). For a law $\mu$ of the HOB with CDF $G$, the expected reward is $R(v,b)=(v-b)G(b)$, and the oracle reward is $\max_{b\in[0,1]}R(v,b)$.

A policy $\pi$ draws internal randomness $u$ once and bids $b_t=\pi_t(u;v_1,\dots,v_t;m_1,\dots,m_{t-1})\in[0,1]$. Its expected regret is

$$\mathbb E[R_T(\pi;v^\star,v)]=\sum_{t=1}^T\Big(\max_{b\in[0,1]}\mathbb E_{m\sim L_t}\big[(v_t-b)\mathbb 1(b\ge m)\big]-\mathbb E\big[(v_t-b_t)\mathbb 1(b_t\ge m_t)\big]\Big),$$

with $L_t=P$ if $v_t<v^\star$ and $L_t=Q$ otherwise: the oracle knows $v^\star$ and bids optimally at every round.

Formalization targets

Goal: Theorem 8 (p. 34)

There are an absolute constant $c>0$ and laws $P,Q$ on $[0,1]$ such that for every $T$ and every policy $\pi$ there are a threshold $v^\star\in[0,1]$ and values $v\in[0,1]^T$ with

$$\mathbb E[R_T(\pi;v^\star,v)]\ \ge\ c\,T .$$

The constant is existential, which is the paper's $\Omega(T)$; the value $1/16$ obtained in the paper's argument is not hard-coded.

Milestones (p. 34)

The paper's argument consists of a hard family indexed by signs $u\in\{\pm1\}^T$, with thresholds $f(u)=\frac12+\frac14\sum_t u_t/2^t$ and values $v_1=\frac12$, $v_{t+1}=v_t+u_t/2^{t+2}$, and four displayed claims:

1. the lexicographic order $f(\dots,u_{t-1},1,\dots)>f(\dots,u_{t-1},-1,\dots)$;
2. the sign identity $\operatorname{sign}(v_t-v^\star)=-\operatorname{sign}(u_t)$ for $v^\star=f(u)$;
3. the oracle reward $v_t-m_t$ with $m_t=\frac18\mathbb 1(v_t\ge v^\star)$ under $P=\delta_0$, $Q=\delta_{1/8}$, and $v_t\in[\frac14,\frac34]$;
4. the posterior-reward bound $\mathbb E_{m\sim\mathrm{Unif}\{0,1/8\}}[(v-b)\mathbb 1(b\ge m)]\le v-\frac18$ for $v\ge\frac14$;

and the Bayesian bound: averaged over uniform $u$, every policy has expected regret at least $T/16$.

Significance

The result. The upper bounds of the paper rely on the HOBs being iid and independent of the bidder's value. Theorem 8 shows that this cannot be relaxed to a mild form of dependence: one threshold, two known laws and full-information feedback already force linear regret against the per-round oracle. The paper concludes that a weaker benchmark is needed once HOBs may depend on values, and leaves that benchmark open.

Formalizing it. The theorem is proved in the paper, on one page; it is not known to be machine-checked. A formal proof pins down the quantifier order (the constant and the laws chosen before the policy, the threshold and values after it), the policy class (randomized, full information) and the treatment of ties, and it provides a reusable model of non-anticipating randomized bidding policies with full-information feedback.

Difficulty

The obvious attempt is to fix a threshold and values and argue that the bidder cannot know on which side of $v^\star$ each $v_t$ falls. For any fixed instance this fails: a policy can be tuned to that instance and bid optimally, with zero regret. The lower bound must therefore pass through an average over a family of instances. The family has to make the side of the threshold at round $t$ independent of everything the bidder has seen up to round $t$, including the past HOBs, which in full information reveal the past sides exactly. The dyadic construction does this. The formal difficulty is the bookkeeping: expressing the expected regret of an arbitrary randomized policy as an integral over its internal randomness and the HOBs, and exchanging the average over $u$ with that integral so that the conditional uniformity of $m_t$ can be used.

Formalization scope

• Time. Rounds are Fin T; Lean round $t$ is the paper's round $t+1$.
• Laws and CDF. HOB laws are Measure ℝ, with probability and support in $[0,1]$ required of the existential witnesses $P,Q$. The CDF is $G(x)=\mu((-\infty,x])$. Atoms are allowed, as in the paper; the construction uses point masses.
• Oracle. $\max_{b\in[0,1]}R(v,b)$ is the supremum over the subtype $[0,1]$; no arg max $b^\star_P(v)$ is chosen. The paper's two-term regret $\mathbb 1(v_t<v^\star)\mathbb E_P[\cdot]+\mathbb 1(v_t\ge v^\star)\mathbb E_Q[\cdot]$ is written with the law $L_t$.
• Policies. A structure with a probability space of internal randomness and, for each round, a jointly measurable bid map of the randomness, $v_1,\dots,v_t$ and $m_1,\dots,m_{t-1}$, with values in $[0,1]$. The types prevent reading $m_t$ or $v^\star$. Deterministic policies are the case of a one-point randomness space.
• Expectation. The bidder's expected payoff at round $t$ is a Bochner integral over the product of the policy's randomness law and the product law of $(m_1,\dots,m_T)$. A local check confirms that this integrand is measurable and bounded, so the integral is never Lean's junk value $0$, which would trivialize the lower bound.
• Knowledge of $(P,Q)$. The laws are fixed before $T$ and $\pi$; a policy chosen afterwards may depend on them. This encodes "revealed to the bidder" and is stronger than choosing $(P,Q)$ after $\pi$.
• Ties. $\mathbb 1(b\ge m)$ throughout; the oracle bids $b=m_t=1/8$ and wins.

A formalization in which the threshold or the values are chosen before the policy, the bid reads $m_t$, the expected payoff is not integrable, or the oracle bids a fixed price, is a different and easier statement; all four are excluded by the definitions above.

Contributions welcome: proofs of the four displayed claims (elementary real analysis on dyadic sums and on point masses), the Bayesian bound (the measure-theoretic core), and the step from the Bayesian bound to the goal. The policy and regret definitions are reusable for other full-information lower bounds in this series.

Selected references

• Y. Han, Z. Zhou, T. Weissman, Optimal No-regret Learning in Repeated First-price Auctions, Operations Research, 2025; read as arXiv:2003.09795v7, §5.2, pp. 33–34. https://arxiv.org/abs/2003.09795

Motivation

The Lightning Network is a payment layer built on top of Bitcoin. Two parties lock funds in a payment channel and then exchange payments off the blockchain, settling on-chain only when the channel closes. Payments between parties without a direct channel are routed along paths of channels. Locked funds are idle capital, and the amount a channel needs grows with the flow it carries, so the topology of the network (which channels exist and what each carries) determines what it costs to support a given pattern of payments.

Guasoni, Huberman and Shikhelman (SSRN 4439190) study this cost under a general channel cost function, building on their earlier analysis of the cost of a single bilateral channel ([GHS22]). Their §3.3 asks how much the globally cheapest network can cost, and how far a simple design is from it. A natural design is the star: every participant opens one channel to a common hub. Corollary 3.11 of the paper shows that a star is in general not cost-minimizing; Corollary 3.12, the goal of this mission, shows that it is never worse than the optimum by more than a factor of two. For symmetric channels (zero net flows) the factor-two bound was known from Sali and Zohar ([SZ20]); the present result covers arbitrary net flows and any cost function satisfying four axioms.

Setting

Let $V$ be a finite set of nodes. A payment flow is a vector $\mathcal F=(f_i)_{i\in V}$ of reals with

$$\sum_{i\in V} f_i = 0,$$

since every payment is sent by one node and received by another.

A Lightning Network (LN) on $V$ is an anti-symmetric real matrix $\Lambda=(\lambda_{i,j})_{i,j\in V}$: $\lambda_{u,v}$ is the net flow from $u$ to $v$ in the channel between them, $\lambda_{u,v}=-\lambda_{v,u}$, and $\lambda_{u,v}=0$ means that there is no channel. The LN supports $\mathcal F$ if $\sum_{j\in V}\lambda_{i,j}=f_i$ for every node $i$.

A channel cost function is a map $c:\mathbb R\to\mathbb R_+$ with

• (MO) $c(x)>c(y)$ whenever $x>y\ge0$;
• (SY) $c(-x)=c(x)$;
• (CI) $c(0)=0$;
• (SA) $c(x+y)<c(x)+c(y)$ for all $x,y>0$.

The cost of an LN $G=(\lambda_{i,j})$ is $c(G)=\tfrac12\sum_{i,j\in V}c(\lambda_{i,j})$, the sum of its channel costs. The minimal cost of supporting $\mathcal F$ is

$$c_{\min}(\mathcal F)=\inf\{c(G) : G \text{ an LN on } V \text{ supporting } \mathcal F\}.$$

For a hub $h\in V$, the star $\Lambda^h$ is the LN in which each node $i\neq h$ has a single channel, to $h$, carrying its flow: $\lambda^h_{i,h}=f_i$, $\lambda^h_{h,i}=-f_i$, and all other entries are $0$.

In Lean these are IsLN, Supports, IsChannelCost, cost, cmin and star in the namespace LNTopology.StarBound.

Formalization targets

Goal: Corollary 3.12

For every channel cost function $c$, every flow $\mathcal F$ with $\sum_i f_i=0$, and every hub $h\in V$,

$$c(\Lambda^h)\;\le\;2\,c_{\min}(\mathcal F).$$

Theorem 3.10

For nonempty $V$,

$$\sum_{i\in V}c(f_i)-\max_{i\in V}c(f_i)\;\ge\;c_{\min}(\mathcal F)\;\ge\;\max\Big(\sum_{f_i>0}c(f_i),\ \sum_{f_i<0}c(f_i)\Big).$$

Milestones

1. For every matrix supporting $\mathcal F$ and every node $i$: $\sum_j c(\lambda_{i,j})\ge c(f_i)$ (proof of Theorem 3.10, p. 14).
2. The star at any hub $h$ is an LN supporting $\mathcal F$ and costs $\sum_i c(f_i)-c(f_h)$ (proof of Theorem 3.10, pp. 13–14).
3. Every LN supporting $\mathcal F$ costs at least $\sum_{f_i>0}c(f_i)$ and at least $\sum_{f_i<0}c(f_i)$ ((14)–(15), p. 14).
4. Theorem 3.10 (p. 8). A supporting item, not a milestone: the chain (16): $\sum_i c(f_i)-\max_i c(f_i)\le\sum_i c(f_i)=\sum_{f_i>0}c(f_i)+\sum_{f_i<0}c(f_i)\le 2M$, with $M$ the maximum of the two sums (p. 14).

Significance

The result. Computing a cost-minimizing network for a general concave-type channel cost is a combinatorial optimization problem with no known closed form; Theorem 3.10 brackets its value by two explicit sums, and Corollary 3.12 turns that bracket into a guarantee for a design that needs no optimization at all. A hub-and-spoke network, the structure that large Lightning Network routing nodes tend to create in practice, thus pays at most twice the optimal locked-capital cost, whatever the flow pattern and whatever the cost function within the axioms. The lower bound of Theorem 3.10 is also a certificate: any supporting network whose cost is within a given factor of $\max(\sum_{f_i>0}c(f_i),\sum_{f_i<0}c(f_i))$ is within that factor of optimal.

Formalizing it. The paper's argument is short, but it assumes that a cost-minimizing network exists and uses its bipartite structure (Theorem 3.1). For a cost function that is not continuous, the minimum need not be attained. The formal development replaces the minimizer by an infimum and proves the lower bound for every supporting network, which removes that gap. It also fixes the hub choice in the proof of the upper bound (see the Formalization scope). To our knowledge, no part of this paper has a machine-checked proof.

Difficulty

The upper bound and the inequality (16) are bookkeeping. The substantive step is the lower bound: every supporting network costs at least the total cost of the payers' flows. The obvious argument applies subadditivity at each payer to the channels incident to it, but those channels carry flows of both signs, and channels between two payers are incident to both of them, so summing over payers can count the same channel twice. Working only with a cost-minimizing network avoids the double count by structure, but a minimizer may not exist. The lower bound must therefore be proved for an arbitrary anti-symmetric supporting matrix, using only (MO), (SY), (CI) and (SA).

Formalization scope

• Nodes. An arbitrary finite type V with decidable equality, instead of $\{1,\dots,n\}$. V nonempty where a maximum over nodes appears (Theorem 3.10, (16)).
• Sign convention. "Supports" is the row-sum identity of §2.1, $\sum_j\lambda_{i,j}=f_i$, under which a net payer has $f_i>0$. The numerical example of §2 and the proofs in Appendix C use the opposite sign. Every statement of this mission is invariant under $\mathcal F\mapsto-\mathcal F$.
• Cost. The paper's $\tfrac12\sum_{i,j}c(\lambda_{i,j})$ form, equal to $\sum_{i>j}$, so no order on V is needed.
• Axiom (SA), corrected. The printed form "$c(x+y)<c(x)+c(y)$ for $x>y\ge0$" is unsatisfiable at $y=0$, which would make every theorem vacuously true. It is stated for all $x,y>0$, the form Appendix D verifies. A local check confirms that $c(x)=\sqrt{|x|}$ satisfies the corrected axioms. The stronger axiom (SA+) is not used in this mission.
• Minimal cost. $c_{\min}$ is an infimum (sInf) over LNs on the same node set V, not a minimum, because $c$ is not assumed continuous. Every statement involving it assumes $\sum_i f_i=0$; without that hypothesis no network supports $\mathcal F$ and $c_{\min}$ is Lean's junk value $0$.
• Star. The star uses $\lambda_{i,h}=f_i$. The paper writes $\lambda_{0,i}=f_i$, which has the opposite sign under the row-sum convention; by (SY) the cost is identical.
• Hub. Corollary 3.12 is stated for every hub $h$, matching the paper's sentence that "the star topology is at most twice as costly as the minimum". The paper's proof takes a hub with $f_0=\max_i f_i$ and then uses $c(f_0)=\max_i c(f_i)$, which fails when the most negative flow has larger magnitude. The milestone on the star is therefore stated with the cost $\sum_i c(f_i)-c(f_h)$ for every hub.
• Lower bound for every network. The inequalities (14)–(15) are derived in the paper for a cost-minimizing network. They are stated here for every supporting LN, which is a generalization and is what the infimum requires.

Trivializing formalizations are ruled out: the cost function is arbitrary subject to the axioms (not $\sqrt{|x|}$ or a power), flows are arbitrary (not the symmetric case of [SZ20]), $c_{\min}$ ranges over all LNs on V (not over stars, trees or bipartite networks), the bound holds for every hub (not one chosen hub), and $\sum_i f_i=0$ is kept so that $c_{\min}$ is never a junk value.

The development needs only finite sums and sInf on $\mathbb R$ from Mathlib. A reusable by-product is the many-term subadditivity $c(\sum_j x_j)\le\sum_j c(x_j)$ for a symmetric, monotone, subadditive $c$ with $c(0)=0$, which applies to any concave-type cost on signed quantities. Contributions are welcome on each milestone independently, in particular on the lower bound (14)–(15).

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; theorem numbers here follow the SSRN version).
• P. Guasoni, G. Huberman, C. Shikhelman, Lightning Network Economics: Channels [GHS22], working paper, 2022 (cited as [GHS22] in the SSRN version; no link given there).
• O. Sali, A. Zohar, Optimizing Off-Chain Payment Networks in Cryptocurrencies [SZ20], arXiv:2007.09410, 2020. https://arxiv.org/abs/2007.09410