All missions

Motivation

Before the thermodynamic limit, macroscopic averages need not commute for a quantum system. As a consequence, aspects of macroscopic fluctuations or of constrained equilibrium require a careful analysis, when dealing with several observables. We propose an implementation of ideas that go back to John von Neumann's writing about the macroscopic measurement. We apply our scheme to the relation between macroscopic autonomy and an H-theorem, and to the problem of equivalence of ensembles. In particular, we show how the latter is related to the asymptotic equipartition theorem. The main point of departure is an expression of a law of large numbers for a sequence of states that start to concentrate, as the size of the system gets larger, on the macroscopic values for the different macroscopic observables. Deviations from that law are governed by the entropy.

This mission is the statement-level formalization of Quantum Macrostates, Equivalence of Ensembles and an H-Theorem (arXiv:math-ph/0601027v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

16 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 3.1: equivalence of the three quantum ensembles (Theorem 3.1: equivalence of the three quantum ensembles, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

3 results of the paper are not stated yet, because the library lacks an interface they need:

• §2.1.4: printed spin microcanonical projection construction: A source-corrected directional spin shell and its physical domain. (source-ambiguity)
• §3 opening: equality iff a concentrating canonical maximizer exists: An admissibility/attainment domain for equality of canonical entropy suprema. (source-ambiguity)
• §4.3: printed product-shell Kac microcanonical macrostate: A source-corrected spin factor and domain for the Kac product-shell macrostate. (source-ambiguity)

Selected references

• Quantum Macrostates, Equivalence of Ensembles and an H-Theorem, arXiv:math-ph/0601027v2, https://arxiv.org/abs/math-ph/0601027v2

Motivation

A connected algebraic group in characteristic 0 is uniquely determined by its Lie algebra. In this paper an algorithm is given for constructing an algebraic group in characteristic 0, given its Lie algebra. Using this an algorithm is presented for finding a maximal reductive subgroup and the unipotent radical of an algebraic group.

This mission is the statement-level formalization of Constructing algebraic groups from their Lie algebras (arXiv:math/0612557v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Chevalley: connected algebraic subgroups generate by uniformly bounded products (Theorem 1 (Chevalley), PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

5 results of the paper are not stated yet, because the library lacks an interface they need:

• Unnumbered main result: reconstruct the connected group from its algebraic Lie algebra: Effective presentation of arbitrary characteristic-zero F, splitting extension access and complete rational eigenvalue relations (source-ambiguity)
• Algorithm 3: terminating closed-product construction of the generated algebraic group: Executable base-field polynomial product-closure, geometric equality testing, and terminating Algorithm 3 loop (hard)
• Algorithm 7: semisimple hull defining polynomials: Effective presentation of arbitrary characteristic-zero F, splitting extension access and complete rational eigenvalue relations (source-ambiguity)
• Unnumbered main application: compute maximal reductive subgroup and unipotent radical: Effective presentation of arbitrary characteristic-zero F, splitting extension access and complete rational eigenvalue relations; transport/recompute a Levi factor compatible with the newly computed toral complement (source-ambiguity)
• Unnumbered algorithmic consequence of Lemma 11: compute bases of d′ and n: Executable Jordan decomposition, finite Fitting bracket iteration, and finite basis extraction relative to the cited Cartan primitive (hard)

Selected references

• Constructing algebraic groups from their Lie algebras, arXiv:math/0612557v1, https://arxiv.org/abs/math/0612557v1

Motivation

We present an algorithm for the explicit numerical calculation of SU(N) and SL(N,C) Clebsch-Gordan coefficients, based on the Gelfand-Tsetlin pattern calculus. Our algorithm is well-suited for numerical implementation; we include a computer code in an appendix. Our exposition presumes only familiarity with the representation theory of SU(2).

This mission is the statement-level formalization of A numerical algorithm for the explicit calculation of SU(N) and SL(N,C) Clebsch-Gordan coefficients (arXiv:1009.0437v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

7 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is GT Littlewood–Richardson acceptance and multiplicities (§VIII, Eq.(31), Appendix B, PDF p. 9). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

2 results of the paper are not stated yet, because the library lacks an interface they need:

• §XII steps 1–3, §I p.1 announcement: Operational exact real-algebraic three-stage GT CG table-construction program, with deterministic rank-ordered product columns and RREF/Gram–Schmidt highest rows, returning all labels, multiplicities and coefficients. (hard)
• §XII polynomial running-time assertion: Specified operation-cost and precision model, uniformity in N and allowed polynomial-constant dependencies. (source-ambiguity)

Selected references

• A numerical algorithm for the explicit calculation of SU(N) and SL(N,C) Clebsch-Gordan coefficients, arXiv:1009.0437v2, https://arxiv.org/abs/1009.0437v2

Motivation

We describe a new method for approximating an arbitrary $n$ qubit unitary with precision $\varepsilon$ using a Clifford and T circuit with $O(4^{n}n(\log(1/\varepsilon)+n))$ gates. The method is based on rounding off a unitary to a unitary over the ring $\mathbb{Z}[i,1/\sqrt{2}]$ and employing exact synthesis. We also show that any $n$ qubit unitary over the ring $\mathbb{Z}[i,1/\sqrt{2}]$ with entries of the form $(a+b\sqrt{2}+ic+id\sqrt{2})/2^{k}$ can be exactly synthesized using $O(4^{n}nk)$ Clifford and T gates using two ancillary qubits. This new exact synthesis algorithm is an improvement over the best known exact synthesis method by B. Giles and P. Selinger requiring $O(3^{2^{n}}nk)$ elementary gates.

This mission is the statement-level formalization of Synthesis of unitaries with Clifford+T circuits (arXiv:1306.3200v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Approximate Clifford+T synthesis with two ancillas (Theorem 1, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Selected references

• Synthesis of unitaries with Clifford+T circuits, arXiv:1306.3200v1, https://arxiv.org/abs/1306.3200v1

Motivation

In this note we collect several characterizations of unitary representations $(\pi, \mathcal{H})$ of a finite dimensional Lie group $G$ which are trace class, i.e., for each compactly supported smooth function $f$ on $G$, the operator $\pi(f)$ is trace class. In particular we derive the new result that, for some $m \in \mathbb{N}$, all operators $\pi(f)$, $f \in C^m_c(G)$, are trace class. As a consequence the corresponding distribution character $\theta_\pi$ is of finite order. We further show $\pi$ is trace class if and only if every operator $A$, which is smoothing in the sense that $A\mathcal{H}\subseteq \mathcal{H}^\infty$, is trace class and that this in turn is equivalent to the Fr'echet space $\mathcal{H}^\infty$ being nuclear, which in turn is equivalent to the realizability of the Gaussian measure of $\mathcal{H}$ on the space $\mathcal{H}^{-\infty}$ of distribution vectors. Finally we show that, even for infinite dimensional Fr'echet-Lie groups, $A$ and $A^*$ are smoothing if and only if $A$ is a Schwartz operator, i.e., all products of $A$ with operators from the derived representation are bounded.

This mission is the statement-level formalization of On the characterization of trace class representations and Schwartz operators (arXiv:1512.02451v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 1.1: integrated operators preserve smooth vectors (Lemma 1.1, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

20 results of the paper are not stated yet, because the library lacks an interface they need:

• Theorem 1.3: Finite-order test topology and canonical Nelson resolvent (hard)
• Unnumbered main consequence: Distribution character on the finite-order test-function topology (hard)
• Theorem 1.4 (Nelson–Stinespring): L1 integrated action and canonical compact Nelson resolvent (hard)
• Unnumbered smoothing factorization, equation (5): Bounded integrated action and the smoothing complex submodule (hard)
• Proposition 1.6: Trace-class representation predicate tied to the actual bounded integrated action (hard)
• Proposition 1.7: Hilbert-Schmidt topology and restricted left action (hard)
• Corollary 1.8: Hilbert-Schmidt joint orbits and the arbitrary-representation Schwartz form (hard)
• Lemma 1.9: Actual derived action, derivative topology and continuous anti-dual (hard)
• Proposition 1.10: Complex trace sandwich pairing on the HS smooth-vector Frechet space (hard)
• Proposition 1.11: Locally convex nuclearity and real distribution dual Gaussian realization (hard)
• Proposition 2.2: Nonnormable locally convex Lie representation and derived sandwich (hard)
• Unnumbered quantitative estimate (7) for derivative sandwiches: Maximal generator weights, unbounded square roots and canonical bounded extensions (hard)
• Remark 2.3(a,b): Locally convex joint C1 calculus and operator-norm orbit derivatives (hard)
• Theorem 2.4: Nonnormable Frechet-Lie smoothness and bounded-form Schwartzness (hard)
• Remark 2.5: Form-defined bounded sandwich and squared maximal-generator domain (hard)
• Theorem 2.6: Merely metrizable locally convex Lie algebra and operator-norm joint smoothness (hard)
• Proposition 2.7: Arbitrary Frechet-Lie Schwartz predicate with actual positive square root (hard)
• Proposition 3.1: Constructed polarized Heisenberg Schrodinger representation and derivative algebra (hard)
• Unnumbered comparison: Coordinate transport and equality of the HS and KKW Schwartz topologies (hard)
• Unnumbered general consequence: General trace-class representation and arbitrary derived Schwartz sandwiches (hard)

Selected references

• On the characterization of trace class representations and Schwartz operators, arXiv:1512.02451v1, https://arxiv.org/abs/1512.02451v1

Motivation

In this paper we consider the $\chi$-function (the Holevo capacity of constrained channel) and the convex closure of the output entropy for arbitrary infinite dimensional channel. It is shown that the $\chi$-function of an arbitrary channel is a concave lower semicontinuous function on the whole state space, having continuous restriction to any set of continuity of the output entropy. The explicit representation for the convex closure of the output entropy is obtained and its properties are explored. It is shown that the convex closure of the output entropy coincides with the convex hull of the output entropy on the convex set of states with finite output entropy. Similarly to the case of the $\chi$-function, it is proved that the convex closure of the output entropy has continuous restriction to any set of continuity of output entropy. Some applications of these results to the theory of entanglement are discussed. The obtained properties of the convex closure of the output entropy make it possible to generalize to the infinite dimensional case the convex duality approach to the additivity problem.

This mission is the statement-level formalization of On entropic quantities related to the classical capacity of infinite dimensional quantum channels (arXiv:quant-ph/0411091v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

27 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §6, unnumbered Theorem: convex-duality additivity equivalence and consequences (§6, unnumbered Theorem: convex-duality additivity equivalence and consequences, PDF p. 19). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

1 results of the paper are not stated yet, because the library lacks an interface they need:

• Section 7, unnumbered energy-continuity assertion: The Hamiltonian domain intended by the unqualified Section 7 mean-energy-continuity sentence. (source-ambiguity)

Selected references

• On entropic quantities related to the classical capacity of infinite dimensional quantum channels, arXiv:quant-ph/0411091v1, https://arxiv.org/abs/quant-ph/0411091v1

Motivation

We show that for a fixed amount of entanglement, two-mode squeezed states are those that maximize Einstein-Podolsky-Rosen-like correlations. We use this fact to determine the entanglement of formation for all symmetric Gaussian states corresponding to two modes. This is the first instance in which this measure has been determined for genuine continuous variable systems.

This mission is the statement-level formalization of Entanglement of formation for symmetric Gaussian states (arXiv:quant-ph/0304042v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Symmetric Gaussian entanglement of formation (Proposition 2: entanglement of formation of symmetric two-mode Gaussian states, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Selected references

• Entanglement of formation for symmetric Gaussian states, arXiv:quant-ph/0304042v1, https://arxiv.org/abs/quant-ph/0304042v1

Motivation

Previous work on the classical information capacities of bosonic channels has established the capacity of the single-user pure-loss channel, bounded the capacity of the single-user thermal-noise channel, and bounded the capacity region of the multiple-access channel. The latter is a multi-user scenario in which several transmitters seek to simultaneously and independently communicate to a single receiver. We study the capacity region of the bosonic broadcast channel, in which a single transmitter seeks to simultaneously and independently communicate to two different receivers. It is known that the tightest available lower bound on the capacity of the single-user thermal-noise channel is that channel's capacity if, as conjectured, the minimum von Neumann entropy at the output of a bosonic channel with additive thermal noise occurs for coherent-state inputs. Evidence in support of this minimum output entropy conjecture has been accumulated, but a rigorous proof has not been obtained. In this paper, we propose a new minimum output entropy conjecture that, if proved to be correct, will establish that the capacity region of the bosonic broadcast channel equals the inner bound achieved using a coherent-state encoding and optimum detection. We provide some evidence that supports this new conjecture, but again a full proof is not available.

This mission is the statement-level formalization of Classical capacity of bosonic broadcast communication and a new minimum output entropy conjecture (arXiv:0706.3416v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Conditional coherent-state capacity region (Section IV, Eqs. (1), (16)-(17); PDF pp.1,3-5, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

1 results of the paper are not stated yet, because the library lacks an interface they need:

• Section V / Figure 4, PDF pp.6-7: The exact MAC photon-budget/power-allocation constraint defining the envelope compared with the coherent bosonic broadcast region. (source-ambiguity)

Selected references

• Classical capacity of bosonic broadcast communication and a new minimum output entropy conjecture, arXiv:0706.3416v1, https://arxiv.org/abs/0706.3416v1

Motivation

We introduce a new form for the bosonic channel minimal output entropy conjecture, namely that among states with equal input entropy, the thermal states are the ones that have slightest increase in entropy when sent through a infinitesimal thermalizing channel. We then detail a strategy to prove the conjecture through variational techniques. This would lead to the calculation of the classical capacity of a communication channel subject to thermal noise. Our strategy detects input thermal ensembles as possible solutions for the optimal encoding of the channel, lending support to the conjecture. However, it does not seem to be able to exclude the possibility that other input ensembles can attain the channel capacity.

This mission is the statement-level formalization of The bosonic minimum output entropy conjecture and Lagrangian minimization (arXiv:0906.2758v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Thermal and displaced thermal stationary witnesses and local output-entropy minima (Unnumbered main result: thermal stationarity and local output-entropy minima, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

11 results of the paper are not stated yet, because the library lacks an interface they need:

• Section I: finite conjecture: A proved unrestricted global vacuum-output entropy bound, rather than its conjecture. (hard)
• Section I: infinitesimal fixed-entropy conjecture: A proved global fixed-entropy instantaneous-rate inequality. (hard)
• Section VIII: claimed equivalence: A reverse implication from the finite pure-input minimum to the positive-entropy rate conjecture. (source-ambiguity)
• Section II, Eq.(5): entropy trace expansion: A source-specified trace differentiability domain and controlled second-order entropy remainder. (source-ambiguity)
• Section IV, Eqs.(6)–(8): all-cutoff stationarity: An exact N-to-N+1 cutoff dynamics, its rectangular dual, and order-of-time convention. (source-ambiguity)
• Section IV: energy-minimum attainment in a connected minimum manifold: A source-supported attainment condition on every connected minimum component. (source-ambiguity)
• Section V, Eqs.(9)–(13): double-stationary classification: Consistent complete primal/dual stationarity equations and common unbounded domains for all candidate solutions. (source-ambiguity)
• Section VI, Eq.(14): full thermal perturbation expansion: Norm/domain and remainder bound for the complete infinite-dimensional Eq.(14). (source-ambiguity)
• Section VII: attributed stationarity sufficiency: A valid second-order or convexity sufficiency hypothesis for Eq.(16). (source-ambiguity)
• Appendix 1: cutoff-independent stationary solutions and their limit: Consistent cutoff CCR, truncated Gibbs normalization, and a stationary-limit theorem. (source-ambiguity)
• Appendix 2: unqualified boundary asymptotic coefficient: A pinned, correct general boundary leakage coefficient and its trace domain. (source-ambiguity)

Selected references

• The bosonic minimum output entropy conjecture and Lagrangian minimization, arXiv:0906.2758v3, https://arxiv.org/abs/0906.2758v3

Why loan trading can change bank capital

Banks that can sell loans after origination may face different incentives to screen them before lending. A buyer that has invested in screening can inspect a seller's loan and buy it when its quality is high. That opportunity can make screening more valuable and reduce the equity a buyer needs to commit. At the same time, a seller may prefer to avoid the screening cost and rely on a later sale. Song and Thakor study when these two choices coexist in an interbank market, even though banks begin with the same opportunities and information (Song and Thakor, SSRN 3667175). The resulting question concerns the capital structure of banks and whether a trading market opens a region of heterogeneous behavior between two homogeneous regimes.

The paper's Proposition 2 is a result about this transition as the chance of a boom changes. It also compares the width of the heterogeneous region across market efficiencies. The mission formalizes that result from the authors' specified model and their preprint's assumptions. The preprint describes the paper as forthcoming in Management Science; the DOI record identifies the associated journal work.

The model and its quantities

A good loan pays $X>I$ at its final date. A medium loan pays $X$ in a boom and zero in a recession. Both require an initial investment $I$. The probability of a boom is $\theta\in[0,\bar\theta]$, with $\bar\theta<I/X$, so a medium loan is not creditworthy on its own. Before a bank screens, each type has probability one half. Screening costs $c$ and reveals the type. A bank can finance the loan with deposits and equity; supplying one unit of equity costs insiders $\psi$ per unit. Default also loses the bank its charter value $Y(\theta)$. The paper restricts $X,I,c,\delta,\psi,\bar\theta$, and $Y$ by Assumptions 1–4 and fixes the matching technology by Assumption 5 (preprint, pp. 7–12); $Y$ is increasing and concave.

Without loan trading, the minimum screening equity is $E^{\mathrm{hom}}(\theta)$, the profit from screening is $\pi_s^{\mathrm{hom}}(\theta)$, and the profit without screening is $\pi_{ns}^{\mathrm{hom}}(\theta)$. Their difference, $\Delta\pi^{\mathrm{hom}}(\theta)$, is the screening advantage. The paper writes each quantity as an explicit real-valued function of $\theta$ in equations (8)–(11). A cutoff $\theta^*$ separates the choices when the loan market is closed (Proposition 1, p. 15).

With trading, some banks can be buyers that screen, while others are sellers that do not. If buyers have mass $N_b$ and sellers mass $N_s$, market tightness is $n=N_b/N_s$. A seller meets a buyer with probability $\alpha(n)=\lambda n/(1+n)$; a buyer meets a seller with probability $\lambda/(1+n)$. Here $\lambda\in[0,1]$ measures matching efficiency. The buyer's bargaining weight is $1/(1+n)$, and the price for a verified good loan is $p(n)=X-(X-I)/(1+n)$. Trading reduces the buyer's required equity to $E^{\mathrm{het}}(\theta,n)=E^{\mathrm{hom}}(\theta)-\lambda(X-p(n))/(1+n)$ (Assumption 5, equation (13), and Lemma 1; the matching function follows Kiyotaki and Wright (1993)).

Formalization targets

The main target is Proposition 2, p. 21. Under the paper's assumptions and its endpoint conditions, there are cutoffs $0<\theta_L<\theta_H<\bar\theta$. Every bank screens below $\theta_L$; none screens above $\theta_H$; between them, buyers and sellers coexist. In the interior the buyer/seller ratio is determined by

$$\lambda(X-I)\left[\frac{1-\theta}{2}\frac{n-1}{n+1}-\frac{\psi}{(n+1)^2}\right] =\Delta\pi^{\mathrm{hom}}(\theta).$$

The two cutoffs solve the paper's equations (A4) and (A7). The mission also targets uniqueness of the equilibrium in every regime, expansion of the heterogeneous region when a larger feasible $\lambda$ is used, and falling $n$ and $p(n)$ as $\theta$ rises within that region. The milestone list covers the matching identities of Assumption 5, the Nash price (13), Lemma 1's equity threshold, the monotonicity of $E^{\mathrm{hom}}$ (footnote 19), the sign form of the cost condition (A1), the strict concavity of $\Delta\pi^{\mathrm{hom}}$, the closed-market cutoff of Proposition 1, the two trading cutoffs (A4) and (A7), the interior indifference equation (A9)/(15), and the monotonicity in $n$ of the left side of (15) (Appendix A, pp. 34–37).

What the result establishes

The result identifies a region in which banks that started alike choose different capital structures and screening decisions. A loan-trading market changes the relative payoffs of screening and not screening, and the boom probability determines which choice can survive a unilateral switch. The cutoffs show precisely where the market moves from all-screening to mixed behavior and then to no-screening. The market-efficiency comparison says when the mixed region widens. These distinctions matter for the paper's subsequent welfare comparison and its discussion of capital requirements (Song and Thakor, §§3–4).

The result is proved in the source paper. The remaining work is a machine-checked proof of the model-specific statements and their consequences, including the bargaining maximum, incentive threshold, cutoff existence and uniqueness, and comparative statics. The definitions are reusable for further formal work on the paper's welfare and capital-requirement results; this mission does not assert that those extensions have been formalized.

Main mathematical difficulty

The equilibrium claim joins several regimes in one statement. The homogeneous corners are governed by whether a single bank would gain by changing its behavior, whereas the interior is governed by equality of buyer and seller profits. A root of the displayed equation alone does not establish an equilibrium: the cutoff and no-switch conditions must also hold, and the root must be unique. Moreover, the source's claimed global negative derivative for $\Delta\pi^{\mathrm{hom}}$ is not implied by its assumptions. The cutoff argument must therefore use a valid shape condition without importing that false assertion. The charter-value function $Y$ is concave but otherwise general, so reasoning cannot rely on a particular polynomial example.

Formalization scope

Lean represents all expectations by the closed-form real expressions in equations (7)–(15); there is no probability space. The parameter structure fixes $X,I,c,\delta,\psi,\lambda,\bar\theta$, and $Y$. All five numbered assumptions remain explicit, including Assumption 4. The formalization reads screening cost and equity cost as positive, reads the paper's smooth $Y$ as differentiable on $[0,\bar\theta]$, and requires $\lambda>0$ for an open market. The bargaining price is optimized over $[I,X]$. The buyer meeting probability uses its continuous value $\lambda$ at $n=0$. Proposition 1 uses a reduced closed-market outcome that records screening and equity; at its profit tie, footnote 21 selects no screening. The open-market equilibrium variable is the buyer share $s\in[0,1]$, with $n=s/(1-s)$ only in the interior; the all-buyer corner uses the sole-seller limit instead. Price and buyer equity are constructed from the paper's equations, and are never arbitrary choices. The cutoffs are required to satisfy $0<\theta_L<\theta_H<\bar\theta$, so all three regimes are nonempty; a version in which the equilibrium is any root of (15), or in which price or buyer equity are free variables, would be a different and weaker statement and is excluded. The hypotheses are jointly satisfiable, but only for small market efficiency (numerical searches find $\lambda\lesssim0.015$); an explicit rational instance is checked in Lean.

The preprint prints a plus sign in (A6) where its preceding deviation inequality requires a minus sign; the Lean condition uses the latter. The paper also claims that the absolute sensitivity of $n$ to $\theta$ falls with $\lambda$, but that claim is false under its hypotheses, so the mission does not include either sensitivity clause of Proposition 2. The paper's unsupported global first-derivative bound for $\Delta\pi^{\mathrm{hom}}$ is excluded. The milestone from the proof of Proposition 5 states its displayed second-derivative identity wherever $Y''$ exists, and states strict concavity throughout the interval. Any further result should keep these corrections explicit. Contributions to the bargaining, real-analysis, and equilibrium lemmas are welcome; proofs of the milestone statements can then support the capstone theorem.

Selected references

• N. Kiyotaki and R. Wright, A search-theoretic approach to monetary economics, American Economic Review 83(1), 63–77, 1993. JSTOR
• F. Song and A. V. Thakor, Market Freeze and Bank Capital Structure Heterogeneity, SSRN preprint 3667175, version dated 2022-02-21; forthcoming in Management Science in the source artifact. SSRN; DOI.

Motivation

Rooftop solar changes both a household's electricity bill and the utility's cost of serving its customers. A tariff that encourages an aggregate amount of solar generation can still leave one customer tier paying more than before. Regulators therefore face a joint design question: can they induce a chosen adoption pattern while meeting the solar supplier's and utility's profit requirements and protecting every customer tier? Singh and Scheller-Wolf formulate this question for a solar company that sells generation through a power purchase agreement, a regulated utility, and households grouped into tiers. Their SSRN paper studies several tariff families; Proposition 5 identifies a tiered tariff that can implement the selected outcome and, when the customers' aggregate financial gain is nonnegative, avoid cross-subsidization.

The selected outcome is assumed to have been chosen for social welfare reasons. The result concerns the next task: implementing it through the tariff while customers decide whether to adopt and the solar company chooses its price. That distinction matters because a tariff that appears to allocate enough money to all parties may change the solar company's preferred price, and therefore change which households adopt.

Setting

There are finitely many customer tiers $i$. Tier $i$ contains $h_i$ households. Each household has annual electricity demand $d_i$, potential solar generation $g_i$, and excess generation $e_i$. If it adopts solar, it draws $d'_i=d_i-(g_i-e_i)$ from the grid and sells $e_i$ back. The target adopting set $A$ identifies the tiers whose households install solar. Let $E^0=\sum_i h_i d_i$ be baseline utility demand, $\Delta_E^A=\sum_{i\in A}h_i g_i$ the target rooftop generation, and $E^A=E^0-\Delta_E^A$ net utility demand. The paper restricts attention to outcomes with at least one adopting tier and $\Delta_E^A\le E^0$ (§3, pp. 10–11).

The regulator sets a tariff $T(d',e,s)$, a customer's utility bill based on grid draw $d'$, electricity sold to the grid $e$, and adoption indicator $s$. For tier $i$, the two relevant bills are $T(d_i,0,0)$ and $T(d'_i,e_i,1)$. A solar company chooses a single price $p_s$ per unit generated by adopting households and pays unit cost $c_s(y)$ when its sales volume is $y$. Each customer adopts when its adopter bill plus $p_sg_i$ is no larger than its nonadopter bill. With ties favoring adoption, this is $p_s\le t(i)$, where $t(i)=[T(d_i,0,0)-T(d'_i,e_i,1)]/g_i$. Thus the solar company's price determines both its sales volume and its unit cost (§§3–4, pp. 10–13).

The regulator's P2 objective is the largest increase in a tier household's cash outflow relative to the baseline rate $p_{r0}$. A nonpositive objective means no tier is financially worse off, which the paper calls cross-subsidization free. P2 also requires a specified solar-company profit $\Delta_S$ and utility profit change $\Delta_U$. Write $\Delta_{WF}$ for the financial welfare improvement of the whole system and $\Delta_C=\Delta_{WF}-\Delta_S-\Delta_U$ for customers' aggregate financial gain (§4, pp. 12–15).

Formalization targets

Proposition 5(a): inducing the target outcome

Tariffs of type $T_3$ charge nonadopters $p_rd_i$ and adopters $p_rd'_i-p_re_i+f_i$, where $p_r$ is a common rate and $f_i$ a tier-specific adopter charge. The paper constructs one such tariff, $T^*$, from the target outcome. At its prescribed price $t(m)$, the target tiers adopt, the solar company earns $\Delta_S$ and earns strictly less at every other price, and the utility receives its specified profit change $\Delta_U$:

$$A(t(m))=A,\qquad \Pi_S(t(m))=\Delta_S>\Pi_S(p)\quad(p\ne t(m)),\qquad \Delta\Pi_U=\Delta_U.$$

This is the feasibility claim of Proposition 5(a), p. 18.

Proposition 5(b): equity and optimality

When the aggregate customer gain is nonnegative, $T^*$ has a nonpositive P2 objective:

$$\Delta_C\ge0\quad\Longrightarrow\quad\max_i\Delta\mathrm{outflow}_i(T^*,t(m))\le0.$$

If a tier with the smallest demand does not adopt, Proposition 5(b) further says $T^*$ minimizes this objective among feasible $T_3$ tariffs. Both clauses belong to the combined goal theorem. The milestone list also includes the customer threshold, the welfare identity, the $T_3$ threshold formula, Proposition 5(a), Lemma 1, the retail-rate identity for $T^*$, and the cross-subsidization clause (p. 18 and proof on p. S.3).

Significance

Proposition 5 gives a tariff implementation for any admissible target adoption set without relying on control of the solar company's price. Its equity guarantee has a clear limit: it requires nonnegative aggregate customer gain. Within the paper's $T_3$ family, the additional lowest-demand condition gives an exact minimax result for customers' bill changes (Proposition 5, p. 18). This distinguishes the existence of an implementing tariff from its distributional performance.

The mathematical result is already proved in the paper; this mission asks for a machine-checked development of its model, construction, and claims. The reusable pieces include finite-tier induced-adoption sets, price-dependent sales volume, and the accounting identities between company profits and customer outflows. The statements in this proposal are proof targets and do not claim an existing Lean proof.

Difficulty

Setting each customer's adoption threshold to produce $A$ is insufficient by itself. The solar company chooses $p_s$ to maximize profit, and a change in price can change both the adopting set and the unit cost $c_s(y)$. The prescribed price must beat every alternative real price strictly. The utility's required profit change constrains the same tier fees used to set thresholds. Finally, a nonnegative total customer gain does not by itself imply that every tier benefits; P2 asks about the largest individual tier increase. These coupled requirements are visible in the paper's P2 formulation and in the proof of Proposition 5 (pp. 13–14, 18, S.3).

Formalization scope

Lean represents tiers by a finite type and outcomes by finite sets of tiers. All demands, prices, bills, costs, volumes, and profit changes are real. The tier type is unordered: the paper relabels tiers during $T^*$'s construction. A tariff is represented by its two bills per tier, the evaluations P2 uses. For $T_3$, fees are indexed by tier, consistent with the paper's statement that the utility can infer a solar customer's tier from grid draw (p. 17). Adoption ties go to adoption, and the solar company's price ranges over all real numbers. P2 feasibility includes the induced adopter set, the firm's unique best response, and the utility constraint.

The standing assumptions state $h_i,d_i,g_i>0$, $0\le e_i\le g_i$, nonincreasing $c_s$, and $\Delta_S>0$. Positivity of $h_i,d_i,g_i$ is implicit in the paper and makes the displayed volume and price divisions valid. The target set is nonempty and satisfies $\Delta_E^A\le E^0$. The utility's total generation cost is outside the household sum in its accounting constraint; this is the reading consistent with the paper's welfare identity. The printed indexing slips in (17) and (19) are avoided by expressing the induced equilibrium directly. Customer aggregate gain is computed from $\Delta_{WF}-\Delta_S-\Delta_U$, rather than defined from the desired conclusion. The optimality quantifier covers feasible $T_3$ tariffs, the family studied in §4.3. Contributions may develop the equilibrium argument, the accounting lemmas, the $T^*$ rate identity, or the complete optimality proof.

Selected references

• Singh, S. P., and A. Scheller-Wolf, That’s Not Fair: Tariff Structures for Electric Utilities with Rooftop Solar, SSRN version, 2022. SSRN 2926676. Source for all statement and appendix page references in this mission.
• Singh, S. P., and A. Scheller-Wolf, That’s Not Fair: Tariff Structures for Electric Utilities with Rooftop Solar, Manufacturing & Service Operations Management 24(3), 2022. DOI:10.1287/msom.2020.0930. Published bibliographic record; the mission cites the SSRN version's numbering and pages.

Motivation

A standard-essential patent is a patent that an implementer must use to make a product compliant with a technical standard. Its owner may demand a royalty from firms using the standard. Whether a patent is truly essential can be disputed, yet licensing offers and investment decisions are made before a court resolves that dispute. Standard-setting organizations can commission essentiality checks that certify patents before licensing. Better checks identify more patents that are not essential, but they also change what an implementer believes about a patent that passes the check. Schuett and Wipusanawan study how those two effects interact with litigation and research investment in their TILEC discussion paper, §§2–5.

A common policy intuition is that a more accurate check should save litigation costs by excluding weak patent claims. The paper identifies a countervailing effect in a model where an innovator chooses research effort before it knows whether its patent will be essential. The question here is local: when a small increase in check accuracy leaves each state's licensing regime unchanged, how does equilibrium welfare change if the patent owner faces no effective cap on royalties? The paper's Proposition 1 answers this question, building on its licensing, investment, and welfare formulas Schuett and Wipusanawan, pp. 16–25.

Setting

An upstream firm chooses research effort $x\in[0,1]$ at cost $c(x)$. Research succeeds with probability $x$. Following success, the standard uses the firm's technology, its patent is essential, and the commercial value is one of finitely many values $v_i$ with probabilities $p_i^H$. Following failure, the standard uses a status-quo technology, the patent is not essential, and value $v_i$ occurs with probability $p_i^0$. The separate distribution $p^L$ for the unsuccessful upstream technology enters the paper's assumption that the status quo has higher expected value than that technology. The model requires $\sum_i p_i^H v_i>\sum_i p_i^0 v_i>\sum_i p_i^L v_i$ Assumption 1, p. 10.

An essentiality check certifies an essential patent correctly. It also certifies a non-essential patent in error with probability $1-\beta$, where $\beta\in[0,1]$ is accuracy. After observing certification and value, the upstream firm offers a royalty fraction $\alpha_i$ bounded by $\bar\alpha\in(0,1]$. The downstream firm can accept or litigate. Litigation costs each firm $l_i$; the court determines essentiality correctly. A non-certified patent earns the upstream firm no licensing revenue in this model. The paper assumes $l_i<\bar\alpha v_i$ Assumption 2, p. 12.

A certified patent can produce a hybrid licensing outcome, in which the unsuccessful firm sometimes offers a low royalty and the downstream firm sometimes litigates a high offer, or a pooling outcome, in which both types offer the maximum royalty. Write $H$ and $P$ for the sets of states with those outcomes. The implementer's belief that a certified patent is essential, $\lambda_i^c$, depends on expected effort $\hat x$, accuracy $\beta$, and the value distributions. In equilibrium, $\hat x=x^*$. The paper derives a private investment wedge from the difference between expected licensing revenues after success and failure, and a social wedge from expected value less both parties' litigation costs equations (1)–(7), pp. 16–22.

Formalization targets

The main target is Proposition 1. With an ineffective royalty cap, $\bar\alpha=1$, fix $\beta_0<1$ where no positive-probability state lies exactly at the hybrid–pooling boundary. Along a continuous path of nearby equilibrium efforts $x^*(\beta)$, the right derivative of welfare $w$ satisfies

$$\frac{d}{d\beta}w\bigl(\beta,x^*(\beta)\bigr)\bigg|_{\beta_0+}\le 0.$$

The inequality is weak because the paper concludes $\partial w^*/\partial\beta\le0$ Proposition 1 and its proof, pp. 24–25. The target concerns a marginal increase that preserves the licensing regimes; it makes no claim about a large change that moves states between $H$ and $P$.

The milestone statements cover the regime condition (4), the private revenue wedge (5), the welfare identity (6), Lemma 2's positive response of research effort to accuracy, and Lemma 3's comparison of private and social investment incentives. Their order exposes the quantities the goal uses without replacing Proposition 1 with a narrower fixed-regime statement.

Significance

Within this model, the result says that improved screening can lower welfare when unconstrained licensing already induces too much research investment. It identifies a limit on an intervention aimed at reducing disputes over essentiality: even a check that detects more non-essential patents may change the incentives of firms whose patents pass. This is a statement about the model's local equilibrium, not a claim that every real-world checking program lowers welfare. The paper separately examines changes large enough to alter licensing regimes and the case of an effective royalty cap Schuett and Wipusanawan, §§5–6.

The economic theorem is proved in the cited paper. This mission asks for a machine-checked account of its finite-state model and the local welfare claim; the displayed Lean statements are open proof targets. The shared definitions of certification beliefs, licensing outcomes, revenue, and welfare are useful for checking later variants of the model, including alternative certification errors or royalty caps. No machine-checked proof of this paper's proposition is claimed here.

Difficulty

The local comparison crosses three choices. Accuracy changes the chance that a failed innovator is certified. Certification changes the downstream firm's belief when it sees a high royalty. The resulting licensing outcome affects the innovator's incentive to invest, and effort feeds back into the belief. Simply holding effort fixed misses the welfare effect in Proposition 1. Treating the hybrid and pooling sets as fixed for all accuracy levels is also too broad: the paper restricts the result to a neighborhood where the regime condition does not meet equality. At a boundary, the relevant formulas can switch and the local derivative need not have the same form pp. 20, 24–25.

Formalization scope

The Lean model uses real values and probabilities on a finite state type Fin n. Each of $p^H$, $p^L$, and $p^0$ is a nonnegative probability vector. Assumptions 1 and 2, $0<\bar\alpha\le1$, and the paper's increasing convex research cost with $c'(0)=0$ and $c'(x)\to\infty$ as $x\uparrow1$ are explicit standing conditions. The cost is represented by a real function twice continuously differentiable on $(-\infty,1)$, which covers the effort domain below one. Equilibrium effort is interior and satisfies the private first-order condition with the implementer's belief equal to effort.

Three premises used in the paper's argument are made explicit. Litigation costs satisfy $l_i>0$. The second derivative at the equilibrium effort satisfies $c''(x^*)>0$, as required by the displayed denominator in Lemma 2; convexity alone gives only nonnegativity. A right-continuous equilibrium-effort path supplies nearby equilibria for the local comparison. The derivative is one-sided because the target concerns an increase from $\beta_0$, including $\beta_0=0$. Strictness of the regime condition is demanded only for states with positive probability under $p^H$ or $p^0$; an absent state cannot affect welfare or investment.

The belief formula is the paper's ratio when its denominator is positive. Its value at a zero-probability state is immaterial to the weighted outcome; the regime milestone also gives a cross-multiplied condition there. Uncertified patents give the upstream firm zero revenue, and the downstream firm retains value without litigation. Welfare is assembled from the two firms' payoffs in every certification and licensing outcome, then related to equation (6). Defining welfare directly by (6), fixing $H$ in the goal, or assuming the derivative of $x^*$ would remove the main work of the proposition. Contributions to the finite-state payoff model, the regime and welfare identities, and the local derivative and wedge comparison are all within scope.

Selected references

• F. Schuett and C. Wipusanawan, Essentiality Checks for Standard Essential Patents, TILEC Discussion Paper DP 2023-21, December 2023, SSRN 4688864. The pinned discussion-paper version is the citation basis for every page and equation in this mission.
• F. Schuett and C. Wipusanawan, Essentiality Checks for Standard Essential Patents, Management Science, 2024, DOI 10.1287/mnsc.2023.04292. The mission does not use the journal pagination.

Motivation

Bundle methods minimize a convex objective while using local supporting affine functions to represent a component that may be nonsmooth. Their iterations can spend time improving the model without moving the current proximal center, so a bound on useful center changes alone does not bound the total work. Liang and Monteiro study a common generic proximal bundle (GPB) framework for several model update rules and give one explicit iteration bound that covers every rule admitted by its bundle update blackbox. The result is a proved theorem in their paper, rather than an open complexity conjecture.

The framework matters when a convex objective combines a component supplied through subgradients with another component whose proximal subproblems can be handled directly. One-cut, two-cut, and multiple-cut bundle updates fit the same abstract requirements in the paper. A common statement makes their guarantees comparable without identifying a specific update formula as canonical.

Setting

The problem is to minimize hybrid convex composite objective $\phi=f+h$ over $\mathbb R^n$. The effective domain $D=\operatorname{dom}h$ is nonempty and contained in the domain of $f$. The function $h$ is lower semicontinuous and $\mu$-convex, for $\mu\ge0$: its convexity inequality gains the quadratic term $\mu\alpha(1-\alpha)\|x-y\|^2/2$. For each $x\in D$, a chosen subgradient $f'(x)$ defines a supporting affine cut

$$\ell_f(u;x)=f(x)+\langle f'(x),u-x\rangle.$$

The hybrid oracle condition allows both a constant and a distance-dependent part:

$$\|f'(x)-f'(y)\|\le 2M_f+L_f\|x-y\|\qquad(x,y\in D),$$

where $M_f,L_f\ge0$. For tolerance $\bar\varepsilon>0$, the pair $(\bar M_f,\bar L_f)$ minimizes $M^2+\bar\varepsilon L$ among all nonnegative pairs satisfying the same condition. An optimal point $x_0^*$ nearest the initial point $x_0\in D$ exists under the paper's assumptions, and $d_0=\|x_0-x_0^*\|$.

A GPB run is an infinite sequence of points $x_j$, best-so-far points $y_j$, centers $x_j^c$, and convex bundle models $\Gamma_j$. At a serious update, the next center is the current point and the next model lies between $\ell_f(\cdot;x_j)+h$ and $\phi$. At a null update, the center stays fixed and a bundle update blackbox selects the next model. Its output must dominate a mixture of a fresh cut and an auxiliary model $\bar\Gamma_j$ that agrees with the previous model at $x_j$ and has $x_j$ as its proximal minimizer. Every new $x_j$ minimizes its model plus the squared distance to its center divided by $2\lambda$. The best-so-far point $y_j$ minimizes the observed objective values. The gap $t_j$ compares $\phi(y_j)$ with the proximal model value; a step is serious when $t_j\le\bar\varepsilon/2$.

Formalization targets

The goal is Proposition 4.9, an explicit total iteration bound for every run admitted by GPB when $\tau$ is set by equation (38). Put $\lambda_\mu=\lambda/(1+\lambda\mu)$ and

$$\bar t=\bar M_f^2+4(\bar L_f+2) \bigl(\max\{1,2\lambda\bar L_f\}d_0+\lambda\bar M_f\bigr)^2.$$

There is an index $j$ with $\phi(y_j)-\phi^*\le\bar\varepsilon$ and

$$j\le\left( \left\lceil\left(1+\frac{8\lambda_\mu(M_f^2+\bar\varepsilon L_f)}{\bar\varepsilon}\right) \max\left\{\log\frac{4\bar t}{\bar\varepsilon},0\right\}\right\rceil+1\right) \left(\operatorname{serBound}(\mu,\lambda,\bar\varepsilon,d_0^2)+1\right).$$

Here $\operatorname{serBound}$ is the minimum of the two serious-iteration expressions in (61), with the paper's limiting convention at $\mu=0$. The milestones follow the two quantities in this product: Corollary B.2 and Lemma 4.2 yield the serious-iteration estimate; Proposition 4.3 packages it. Equation (7), Lemmas 4.6, A.3, and 4.7 bound the behavior within each cycle; Proposition 4.8 bounds the cycle length. The goal combines the two bounds without selecting one concrete bundle update.

Significance

The theorem gives a finite tolerance certificate with a numerical bound on all iterations, including those that only improve the bundle model. The bound depends on the oracle parameters, curvature, initial distance to the solution set, tolerance, and proximal stepsize. It therefore states what an implementation gains by satisfying the BU conditions even when its internal model construction differs from another implementation. The broader paper also analyzes particular update schemes and an adaptive method, but the target here is the common GPB result Liang and Monteiro, §3–4.

The mathematical result is already proved in the source. This mission asks for machine-checked definitions and proofs of its explicit bound and the selected supporting statements. No machine-checked proof is supplied by these open theorem items. The definitions of the hybrid oracle, proximal model, and abstract GPB run can be reused to formalize the paper's concrete update schemes later.

Difficulty

Counting serious steps does not count intervening null steps. A null step can leave the center fixed while the model changes, and the BU condition permits many such models. The main obstacle is to obtain a uniform bound for a complete cycle from conditions that are local to one model update. The separate analytic obstacle is the hybrid descent estimate (7): the oracle bound contains both a constant term and a term proportional to distance, and the needed quadratic coefficient is $L_f/2$, not the easier $L_f$. The source's auxiliary proximal displacement estimate also depends on lower semicontinuity so that its minimizers exist.

Formalization scope

The Lean space is EuclideanSpace ℝ (Fin n), with its usual norm and real inner product. The function domain $D$ stands for $\operatorname{dom}h$; $f$, $h$, and each bundle model are real-valued on $D$, with an extended value $+\infty$ off $D$ when lower semicontinuity is stated. All model inequalities and proximal minimizations are over $D$. This represents the paper's extended-valued functions without ambiguous arithmetic at $+\infty$. The selected subgradient inequality is also required only on $D$. The source's lower semicontinuity of $f$ and of the BU auxiliary model is omitted, which strengthens the resulting claims; lower semicontinuity of $h$ and of each generated model remains. The abstract serious-iterate sequences explicitly keep their auxiliary points in $D$.

Index zero is initialization and counts as serious because $t_0=0$; subsequent indices are natural numbers. The GPB run predicate retains the existential auxiliary model in every null update, so it covers every admissible variant. The goal concludes existence of a successful bounded index. It assumes $M_f^2+\bar\varepsilon L_f>0$ so equation (38) defines $\tau\in(0,1)$. For $\mu=0$, the serious-step formula uses the limiting value rather than real division by zero. The printed cycle and total bounds omit an integer rounding and can be too small; the formal targets use a ceiling and a nonnegative logarithm. Lemma 4.2(c), Lemma A.3, and Lemma 4.7 carry the additional qualifications needed by their printed proofs, disclosed beside their statements.

The development needs Mathlib's finite-dimensional Euclidean spaces, convexity, lower semicontinuity, and real logarithm, plus real-sequence and finite-index estimates. Contributions proving the milestones, the goal, or reusable facts about the GPB model are within scope. A proof for one fixed update formula alone does not establish the goal over the BU blackbox.

Selected references

• J. Liang and R. D. C. Monteiro, A Unified Analysis of a Class of Proximal Bundle Methods for Solving Hybrid Convex Composite Optimization Problems, Mathematics of Operations Research, 2024; source used here: arXiv:2110.01084v3, 2023, §§2–4 and Appendices A–B.

Motivation

Large language models answer reasoning questions better when they are allowed to write out a chain of thought (CoT) before the final answer, but every generated token costs time and money. A large body of recent work therefore asks models to "think less": prompts such as "be concise" or "use at most 10 words", and training methods that shorten the reasoning trace. These methods trade accuracy for length, and the natural question is how good such a trade can possibly be.

Lee, Che and Peng (2025) study this question empirically on MATH-500, GSM8K and MMLU-Pro Math with 31 prompts and several frontier models. Their key observation is that, question by question, correctness is almost a threshold function of the response length: a model solves a question if and only if its chain of thought is at least as long as a question-specific token complexity. Under this hypothesis they derive the best possible accuracy–length tradeoff over all prompts, and show that existing prompting strategies are far from it (Table 4 of the paper). This mission formalizes that derivation: Theorem 1 of the paper and the steps of its proof in Appendix D.

Setting

Fix one language model and a dataset of $n \ge 1$ questions $i = 1, \dots, n$. A prompt $P$ determines, for each question $i$, a chain of thought of token length $t_i(P) \in \mathbb N$ and a correctness indicator $a_i(P) \in \{0, 1\}$. The accuracy and the average token length of a prompt are

$$\mathrm{Acc}(P) = \frac1n \sum_{i=1}^n a_i(P), \qquad \bar t(P) = \frac1n \sum_{i=1}^n t_i(P).$$

The two optimal tradeoff curves are the optimal accuracy at average budget $T$ and the minimal average length for accuracy $\alpha$:

$$\alpha^*(T) = \max_P \{\mathrm{Acc}(P) : \bar t(P) \le T\}, \qquad T^*(\alpha) = \min_P \{\bar t(P) : \mathrm{Acc}(P) \ge \alpha\}.$$

Assumption 1 (token complexity hypothesis). There are numbers $\tau_i \in \mathbb N \cup \{\infty\}$, the token complexities, such that for every prompt $P$ and question $i$,

$$a_i(P) = \mathbf 1\{t_i(P) \ge \tau_i\}.$$

The value $\tau_i = \infty$ marks a question the model never solves. The paper also assumes the prompts are rich: every vector of token counts $(t_i) \in \mathbb N^n$ is produced by some prompt. The answer is expressed through the empirical quantities

$$F_n(t) = \frac1n \sum_{i} \mathbf 1\{\tau_i \le t\}, \qquad E_n(t) = \frac1n \sum_{i} \tau_i \mathbf 1\{\tau_i \le t\}, \qquad A^* = \frac1n \sum_i \mathbf 1\{\tau_i < \infty\},$$

where $A^*$ is the largest accuracy any prompt can reach.

Formalization targets

Goal: Theorem 1 (corrected), p. 7

Assume Assumption 1, rich prompts, and pairwise distinct finite token complexities. Let $t_T$ be the largest finite $\tau_j$ with $E_n(\tau_j) \le T$ and $q_\alpha$ the smallest finite $\tau_j$ with $F_n(\tau_j) \ge \alpha$. Then for every $T \ge 0$ and every $0 < \alpha \le A^*$,

$$\alpha^*(T) = \frac1n \sum_{i=1}^n \mathbf 1\{\tau_i \le t_T\}, \qquad T^*(\alpha) = \frac1n \sum_{i=1}^n \tau_i\, \mathbf 1\{\tau_i \le q_\alpha\},$$

with both optima attained. As printed, the theorem defines $t_T \equiv \inf\{t \in \mathbb R : E_n(t) = t\}$, which does not depend on $T$, and $q_\alpha = \sup\{t : F_n(t) \le \alpha\}$, which overshoots the quantile; both readings give wrong values on one- and two-question examples. The goal uses the thresholds that the proof and the text describe ("the highest value of τ that the LLM puts into the knapsack", "the α-quantile of the empirical distribution").

Milestones (Appendix D, p. 14)

1. Eq. (8): under Assumption 1, $\mathrm{Acc}(P) = \frac1n\sum_i \mathbf 1\{\tau_i \le t_i(P)\}$ (the page prints the inequality reversed).
2. Eqs. (9)–(10): with rich prompts, $\alpha^*(T)$ and $T^*(\alpha)$ are the optima of the same problems over token-count vectors $t \in \mathbb N^n$.
3. Eqs. (11)–(12): these equal the optima of a 0-1 knapsack with unit rewards and costs $\tau_i$,

$$\max_{x \in \{0,1\}^n} \frac1n \sum_i x_i \quad \text{s.t.} \quad \frac1n \sum_i \tau_i x_i \le T.$$

4. The greedy claim: for $T \ge 0$ the knapsack optimum is $m/n$, where $m$ is the largest number with $\tau_{(1)} + \dots + \tau_{(m)} \le nT$ for the sorted finite token complexities $\tau_{(1)} \le \tau_{(2)} \le \cdots$.
5. The $T^*$ analogue: for $0 \le \alpha \le A^*$ the minimal cost is $\frac1n(\tau_{(1)} + \dots + \tau_{(\lceil n\alpha\rceil)})$.

Milestones 4 and 5 allow ties among the token complexities; the goal's closed form does not.

Significance

Theorem 1 turns an optimization over all conceivable prompting strategies, an infinite and unstructured set, into a formula in the empirical distribution of $n$ numbers. Its consequence, Corollary 1, is that $T^*(A^*)$, the average token complexity of the solvable questions, is a lower bound on the average length of any lossless compression of the chain of thought; the paper's Table 4 uses it to show that current concise prompts leave a 3–11× reduction unrealized. The same characterization explains why adaptive strategies, which spend more tokens on harder questions, are necessary to approach the frontier.

The result has a pen-and-paper proof of a few lines in Appendix D; the prior-art search found no machine-checked version. Formalizing it adds a correct statement: the printed definitions of $t_T$ and $q_\alpha$ are wrong, eq. (8) has a reversed inequality, and the closed form silently needs distinct token complexities. The mission records the correct versions with the counterexamples to the printed ones, and separates the tie-robust greedy form (milestones 4–5) from the CDF form (the goal).

Difficulty

The individual steps are elementary, but the obvious argument skips three points. First, passing from prompts to token vectors uses richness in both directions: an optimal prompt must be matched by a token vector and conversely, and the optima must be shown attained, not merely bounded. Second, the reduction to $t_i \in \{0, \tau_i\}$ must handle questions with $\tau_i = \infty$, which can never be selected. Third, the greedy claim is a statement about every feasible selection, not only the sorted ones, and translating the greedy count into the threshold forms $\mathbf 1\{\tau_i \le t_T\}$ and $\mathbf 1\{\tau_i \le q_\alpha\}$ is exactly where ties break the formula, so distinctness must be used at that step and nowhere else.

Formalization scope

• Model. One LLM, superscript $\pi$ dropped. Questions are Fin n; prompts are an arbitrary type; a Benchmark gives token lengths len : Prompt → Fin n → ℕ and correctness correct : Prompt → Fin n → Bool. Each (prompt, question) pair yields one deterministic chain of thought.
• Token complexities are ℕ∞-valued; $\tau_i = \infty$ is ⊤. Assumption 1 is correct P i = true ↔ τ i ≤ len P i ("above" read as $\ge$, as the displayed formula on p. 5 shows). Every count or sum over $\tau$ filters on $\tau_i \ne \infty$ before converting to a natural number.
• Averages are real numbers with division by $n$; the goal assumes $n \ge 1$.
• Optima are IsGreatest/IsLeast predicates over the set of values achieved by prompts, never sSup/sInf, so empty or unbounded feasible sets cannot produce a junk value.
• Added hypotheses, all disclosed: $n \ge 1$; $T \ge 0$; $0 < \alpha \le A^*$ for the $T^*$ part ($\alpha \ge 0$ in milestone 5); pairwise distinct finite token complexities in the goal only.
• Trivializing formalizations ruled out. The goal quantifies over prompts and links them to $\tau$ only through Assumption 1 and richness; neither $\alpha^*$ nor $T^*$ is defined as its closed form, and the goal is not stated over token vectors or knapsack variables. Richness is satisfiable: the canonical benchmark with prompts $\mathbb N^n$ satisfies both hypotheses for every $\tau$.
• Not formalized: Corollary 1 (a consequence the proof of Theorem 1 does not use), the threshold-classifier estimators of §3, and the empirical results.

The definitions (benchmark, empirical CDF over an ℕ∞-valued family, sorted prefix sums) are self-contained. A proof of the greedy milestones gives a reusable fact about unit-reward knapsacks. Proofs of any milestone and of the goal are welcome, as is a formalization of Corollary 1 on top of the goal.

Selected references

• A. Lee, E. Che, T. Peng, How Well do LLMs Compress Their Own Chain-of-Thought? A Token Complexity Approach, arXiv preprint, 2025. https://arxiv.org/abs/2503.01141 (version v2 is the one formalized).
• J. Wei et al., Chain-of-Thought Prompting Elicits Reasoning in Large Language Models, NeurIPS, 2022. https://arxiv.org/abs/2201.11903

Motivation

An entrepreneur deciding whether to continue a project may value continued control even when liquidation would generate more cash. The project has a known liquidation value, but its final cash flow is uncertain. An accounting signal changes what the entrepreneur expects from continuation and can therefore change the decision. A regulator who cares about total cash flow can choose how much the signal reveals. Jiang and Yang ask which accounting rule best corrects the entrepreneur's excessive willingness to continue and show that the answer has a precise threshold form (Jiang and Yang 2023, §§2–3). The mission formalizes their main threshold characterization for the regulator's reduced problem.

The question belongs to information design: a decision maker chooses a signal before the state is known, anticipating how another party will act after observing it. The result gives a concrete instance in which the optimal signal is neither arbitrary disclosure nor full disclosure. It also identifies a parameter range in which the regulator can obtain the same liquidation decisions as if the entrepreneur had no private benefit.

Setting

At date 1 a project can be liquidated for $M>0$ or continued to produce a random date 2 cash flow $\theta$. The prior law $P$ of $\theta$ has a density and full interval support $[\underline\theta,\overline\theta]$, where $0\le\underline\theta<M<\overline\theta$. The entrepreneur receives an additional private benefit $B\in[0,M]$ from continuation. The regulator counts the project's cash flow, not that private benefit. These assumptions and the common prior are from §2 of Jiang and Yang.

An accounting rule reveals information about $\theta$. The signal induces a posterior probability distribution $\mu$ and hence a posterior mean $\mathbb E_\mu[\theta]$. Under decision rule (4), the entrepreneur continues exactly when $\mathbb E_\mu[\theta]+B>M$; on equality they terminate, following the paper's tie rule. The regulator's payoff after that posterior is

$$V(\mu)=\begin{cases}\mathbb E_\mu[\theta],&\mathbb E_\mu[\theta]>M-B,\\M,&\mathbb E_\mu[\theta]\le M-B.\end{cases}$$

The formal representation of a rule is a distribution $\tau$ over posteriors. It is Bayes plausible when its average posterior equals the prior $P$; the regulator's value is $\int V(\mu)\,d\tau(\mu)$. This posterior representation is the one used in the paper's Appendix A.1 and is consistent with the general Bayesian persuasion framework of Kamenica and Gentzkow 2011. For an event $S$ of positive prior probability, $\mathbb E_P[f(\theta)\mid S]$ denotes $\int_S f(\theta)\,dP(\theta)/P(S)$.

A threshold rule at $t$ sends a high signal precisely on $\{\theta>t\}$. It sends the low signal when $\theta\le t$. The strict boundary agrees with Proposition 2; because the prior has a density, the single boundary state has probability zero.

Formalization targets

Optimal threshold and first-best regime

For $0<B\le M$ and $\underline\theta<M-B$, the goal is the corrected endpoint form of Proposition 2. There is a threshold $\hat\theta\in(M-B,M]$ whose reveal policy attains at least the value of every Bayes-plausible accounting rule. Its two cases are

$$\hat\theta=M\quad\text{if }B\le\mathbb E_P[M-\theta\mid\theta\le M],$$ $$\hat\theta\in(M-B,M),\qquad \mathbb E_P[\theta\mid\theta\le\hat\theta]=M-B\quad\text{otherwise}.$$

The interior solution is unique. The entrepreneur follows the signal: continuation after the high signal and termination after the low signal. The first case gives the first-best liquidation decision, which continues precisely for $\theta>M$.

Appendix milestones

The milestone list follows the source's Appendix A.1: reduction from Bayes-plausible posterior rules to a binary signal probability $m(\theta)$; the relation between the two binary mean constraints (A.1) and (A.2) in each prior-mean regime; the threshold shape associated with the appendix's multiplier; the first-best case; existence, uniqueness, and optimality of the interior threshold; and the closing implication that joins the low-prior-mean case to the first-best case. Together these statements connect the general accounting-rule problem (5) to the threshold formula (6).

Significance

The theorem specifies when disclosure can neutralize the private continuation benefit and when a more conservative threshold is required. In the latter case the low signal must put the entrepreneur exactly at the continuation indifference point. The threshold characterization also underlies the paper's claims about full disclosure and how the optimal rule changes with $B$ and $M$ (Jiang and Yang 2023, Corollaries 1–2). Those corollaries are consequences of the present target, not assumptions of it.

The paper proves Proposition 2 mathematically; the Lean goal and milestone statements here remain open for machine-checked proofs. A complete development would provide a reusable posterior-to-binary reduction for a payoff with two linear segments, plus formal results about conditional means under full interval support. The referenced Bayes-plausibility definition is already published on Prove2Me. Proposition 1 of the paper concerns financing contracts and is outside this reduced regulator problem; its proof is in an online appendix not held with the cited PDF.

Difficulty

The regulator ranges over every Bayes-plausible distribution over posteriors, while the proposed optimum uses only two signals. Checking that a given threshold is best among threshold rules leaves this larger comparison unresolved. The regulator's payoff also switches formula at the entrepreneur's indifference mean, so a direct global smoothness argument does not apply. Finally, the conditional mean below a moving threshold must reach $M-B$ at one and only one interior point under the prior's support conditions. The binary reduction and these boundary properties are substantial parts of the formalization.

Formalization scope

Lean uses real cash flows and a probability measure $P$ on $\mathbb R$ with $P\ll\mathrm{volume}$, mass one on $[\underline\theta,\overline\theta]$, and positive mass on every open subinterval. A published definition supplies Bayes-plausible measures $\tau$ on the Giry space of posterior measures and the two-cell reveal policy. The strict high cell is $\{\theta>\hat\theta\}$; equality goes to the low cell and termination. Conditional means are ratios of restricted integrals to event probabilities, and every event used by the theorem has positive prior mass. Bounded support makes the relevant posterior means finite almost everywhere under a Bayes-plausible rule.

Two endpoint guards repair the source's literal Proposition 2. At $B=0$, its asserted interval $(M-B,M]$ is empty. At $\underline\theta=M-B$, the interior equation need not have a solution: with $\theta$ uniform on $[0,2]$ and $M=B=1$, its left side is positive for every positive threshold. The goal therefore assumes $B>0$ and $\underline\theta<M-B$. The paper's assumption (1), involving investor reservation value, is absent from the reduced problem (5), and Appendix A.1 treats a prior-mean case that assumption would exclude; it is not imposed here.

The comparison in the goal covers all Bayes-plausible accounting rules. The payoff uses the entrepreneur's posterior-mean response, including the tie rule. A development that compares only threshold rules or fixes the entrepreneur's action to the signal would not establish this target. Contributions to the binary reduction, conditional-mean continuity and uniqueness, and optimality of the two threshold cases are directly reusable.

Selected references

• X. Jiang and M. Yang, Optimal Accounting Rules, Private Benefits of Control, and Efficient Liquidation, Management Science, Articles in Advance, 2023, pp. 1–13. DOI: 10.1287/mnsc.2019.03087.
• E. Kamenica and M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011, pp. 2590–2615. DOI: 10.1257/aer.101.6.2590.

Motivation

In a linear bandit problem, a learner chooses a vector and observes a noisy scalar response that carries information about an unknown parameter. Regret analyses often need to control the sum of the learner's uncertainty in the directions it chooses. The familiar elliptical potential lemma does this when uncertainty is represented by the inverse of a deterministic, successively updated Gram matrix. Bayesian learning presents a different object: the posterior covariance of the unknown parameter given the observations. It changes with the realized data and can increase on an individual sample path. Hamidi and Bayati's technical note establishes a potential bound for this posterior object under general prior and noise distributions and uses it to analyze linear Thompson sampling.

The deterministic lemma and the posterior result answer related but distinct questions. In the deterministic setting, the update is fixed by the chosen vectors. Here, actions may depend on earlier observations and the next posterior covariance is itself random. The mission concerns the latter claim, including the observation model that gives the covariance its meaning.

Setting

Let $(\Omega,\mathcal F,\mathbb P)$ be a probability space with an increasing filtration $(\mathcal F_t)_{t\ge1}$. An unknown parameter $\Theta^\star\in\mathbb R^d$ obeys $\|\Theta^\star\|_2\le1$ almost surely. At time $t$, the learner chooses an $\mathcal F_t$-measurable action $A_t\in\mathbb R^d$ with $\|A_t\|_2\le1$ almost surely. An observation $Y_t$, measurable at time $t+1$, has conditional mean $\langle\Theta^\star,A_t\rangle$ and conditional variance at most $\sigma^2$ when both $\mathcal F_t$ and $\Theta^\star$ are known. No Gaussian law or independent noise model is part of these assumptions.

Write $\Gamma_t=\operatorname{Var}(\Theta^\star\mid\mathcal F_t)$ for the posterior covariance matrix. The quantity $A_t^\top\Gamma_t A_t$ is the remaining parameter uncertainty in the chosen direction. The matrix function used to measure accumulated uncertainty is

$$f(\Sigma,x)=\log\det(I+x\Sigma),\qquad \Sigma\succeq0,\quad x>0.$$

The matrix order $B\succeq A$ means that $B-A$ is positive semidefinite. Conditional expectations of matrices are taken entrywise. The filtration can contain information beyond the actions and observations; it need not be generated by them.

Formalization targets

The first target is the source's stochastic variance reduction inequality. For every $t\ge1$, almost surely,

$$\mathbb E[\Gamma_{t+1}\mid\mathcal F_t]\preceq\Gamma_t-\frac{\Gamma_t^\top A_tA_t^\top\Gamma_t}{\sigma^2+A_t^\top\Gamma_t A_t}.$$

The matrix potential targets are the concavity of $f(\cdot,x)$ on the positive semidefinite cone and equation (2.2): if $\Sigma'=\Sigma-\Sigma VV^\top\Sigma/(1+V^\top\Sigma V)$, then

$$\log(1+V^\top\Sigma V)+f(\Sigma',x)\le f(\Sigma,x+V^\top V).$$

Two scalar and covariance bounds from the proof complete the milestone list: $x\le2\log(1+x)$ on $[0,1]$, and $A_t^\top\Gamma_t A_t\le1$ almost surely. The main target, a conditional formulation of Theorem 2.1, is

$$\mathbb E\!\left[\sum_{t=1}^{T}A_t^\top\Gamma_t A_t\,\middle|\,\mathcal F_1\right]\le 2\max(\sigma^2,1)\log\det(I+T\Gamma_1)\quad\text{almost surely}.$$

The source prints an unconditional expectation on the left although $\Gamma_1$ can be random. Conditioning on $\mathcal F_1$ supplies a coherent general statement; it becomes the printed display when the initial information is trivial. The goal retains the explicit factor $2\max(\sigma^2,1)$ and the horizon $T$ inside the log determinant.

Significance

The result controls a cumulative, adaptively selected posterior quadratic form using only the initial posterior covariance, the horizon and the conditional noise bound. It permits a regret analysis of linear Thompson sampling without replacing the prior by a Gaussian model. In the source, this bound feeds the Bayesian regret theorem for that algorithm; that later theorem is outside this mission's scope. Its proof would also require formalizing the sampling policy and its action-selection law.

The formal development fixes a reusable interface for finite-dimensional posterior covariance under a filtration: a parameter, adapted actions, conditional moments of observations, and an entrywise matrix covariance. It also states the matrix potential claims separately from the probability model, so those claims can serve other analyses of covariance updates. The statements compile locally as open Lean theorems; this mission does not claim machine-checked proofs of them. The deterministic elliptical potential statement already available elsewhere uses a Gram-matrix update and does not establish this posterior result.

Difficulty

Posterior covariance is not pathwise decreasing. The paper's Section 2 example has an observation after which $\Gamma_2>\Gamma_1$. A bound that assumes $\Gamma_{t+1}\preceq\Gamma_t$ for every outcome therefore fails at the first stochastic step. The issue matters especially when actions are adapted: later actions can point toward directions whose posterior variance became large after earlier data. Conditional covariance reduction is a matrix inequality, while the target is a scalar sum of quadratic forms; its potential must remain valid across those different objects.

Formalization scope

Lean uses vectors Fin d → ℝ and the Euclidean dot product, so the unit-ball assumptions mean $v^\top v\le1$. The posterior covariance is the conditional expectation of centered coordinate products. The expectation of a covariance matrix is defined entrywise; matrix order is positive semidefiniteness of the difference. The conditioning sigma-algebra for $Y_t$ is $\mathcal F_t\vee\sigma(\Theta^\star)$, not merely $\mathcal F_t$. Every observation is explicitly square-integrable, so Lean's totalized conditional variance cannot silently return zero for a non-square-integrable input. The source's bound on the parameter already supplies its integrability.

Rounds start at $1$; the finite sum uses $1\le t\le T$. At $T=0$ it is empty and both sides of the goal are zero. No positivity assumption on $\sigma$ is imposed, since the statements use $\sigma^2$ and the zero-denominator covariance correction has zero numerator. The log determinant is used on positive semidefinite covariance matrices with nonnegative scalar argument, where its determinant is positive. The paper's square-root factorization of $\Sigma'$ is represented by its equal direct matrix formula. A deterministic Gram matrix in place of $\Gamma_t$, an independent-observation construction in place of the conditional-moment model, or a supremum-norm ball would change the theorem. The separate matrix and probability lemmas, conditional expectation infrastructure, and finite-dimensional matrix order are the principal reusable components.

Selected references

• Nima Hamidi and Mohsen Bayati, The Elliptical Potential Lemma for General Distributions with an Application to Linear Thompson Sampling, technical note, Operations Research, 2023; formalization source: arXiv:2102.07987v3, 2022, §2 and Appendix A.

Motivation

Capacitated vehicle routing asks how to serve clients from a depot with vehicles that can carry only a limited load. In the unsplittable version, one vehicle must deliver each client's entire demand. This makes the choice of routes interact with bin packing: a short tour can fail because its total demand exceeds the vehicle's capacity. Approximation algorithms are therefore useful when exact optimization is impractical, and their guarantees must account for both travel distance and capacity. Friggstad et al., arXiv:2111.08138v1, pp. 1–2.

The paper distinguishes unit-demand, splittable-demand and unsplittable-demand CVRP. Earlier tour-partitioning methods gave constant-factor guarantees, while the paper's first main result is a combinatorial algorithm with ratio $\alpha+1.75$, where $\alpha$ is an approximation ratio for metric traveling salesman tours. Taking $\alpha=1.5$ gives the paper's stated $3.25$ ratio. The paper also gives a separate linear-programming-based improvement, which is outside this mission. These are results already proved mathematically; the mission concerns their precise Lean statements and a machine-checked proof of the combinatorial result. Friggstad et al., arXiv:2111.08138v1, pp. 2–3.

Setting

An instance consists of a finite set $V$ of clients, a separate depot $r$, a symmetric nonnegative metric cost $c(u,v)$, and a demand $d_v\in(0,1]$ for each client. A vehicle has capacity $1$. A route starts and ends at $r$, visits a sequence of clients, and carries at most one unit of total demand. A feasible solution is a collection of routes in which every client appears exactly once. Its cost is the sum of its routes' travel costs, and $\mathrm{opt}$ is the least such cost. The normalization to unit capacity and the positivity of every demand are standing assumptions of §2. Friggstad et al., arXiv:2111.08138v1, p. 4, Definitions 3–4.

For a threshold $\delta\in[0,1/2]$, a client is small when $d_v\le\delta$ and big when $d_v>\delta$. The radial sums are

$$\mathcal D=\sum_{v\in V}2d_vc(r,v),\qquad \mathcal D_{\rm small}=\sum_{v\text{ small}}2d_vc(r,v),\qquad \mathcal D_{\rm big}=\sum_{v\text{ big}}2d_vc(r,v),\qquad \mathcal D'_{\rm big}=\sum_{v\text{ big}}2c(r,v).$$

The last sum is the cost of giving each big client its own depot route. Lemma 6 says $\mathcal D\le\mathrm{opt}$. Friggstad et al., arXiv:2111.08138v1, pp. 4–5.

Algorithm 1 fixes $\delta=1/3$. It obtains one traveling-salesman tour $A_s$ through the small clients and another $A_a$ through all clients. A consecutive split partitions the visiting order of a tour into capacity-feasible routes; $\operatorname{Split}(A)$ is the minimum cost of such a partition. The algorithm also finds a minimum-cost matching with loops on the big clients, whose one- or two-client routes cost $\operatorname{Match}(V_{\rm big})$. It returns the cheaper of a matching plus a split of $A_s$, and a split of $A_a$. Friggstad et al., arXiv:2111.08138v1, pp. 7–8, Algorithm 1.

Formalization targets

The first targets are the paper's intermediate bounds: Lemma 6's radial lower bound; the TSP lower bound used in §3.1; Claims 8–9 on the probabilities of the tank events; Lemma 7's $\delta$-tank cost guarantee; Lemmas 10–11 on the matching; and the two branch estimates (4)–(5). These are the mission's milestones in the order in which their results are needed. Friggstad et al., arXiv:2111.08138v1, pp. 4–8.

The goal is Theorem 1. Let $\operatorname{TSP}(S)$ be the minimum depot tour length through exactly the client set $S$, and suppose

$$c(A_s)\le\alpha\operatorname{TSP}(V_{\rm small}),\qquad c(A_a)\le\alpha\operatorname{TSP}(V),\qquad \alpha\ge1.$$

For the specific cost

$$C_{\rm alg}:=\min\{\operatorname{Match}(V_{\rm big})+\operatorname{Split}(A_s), \operatorname{Split}(A_a)\},$$

the goal says that a feasible solution attains $C_{\rm alg}$ and, for every feasible solution $\mathcal T$,

$$C_{\rm alg}\le(\alpha+1.75)c(\mathcal T).$$

Quantifying over every feasible solution expresses the ratio against $\mathrm{opt}$ without relying on a default value of a real infimum. Friggstad et al., arXiv:2111.08138v1, p. 2, Theorem 1; pp. 7–8, Algorithm 1.

Significance

The theorem supplies a cost guarantee for a concrete routing algorithm with a fixed threshold and two prescribed branches. It applies to unequal, indivisible client demands, while a unit-demand model cannot express the main capacity issue. The $3.25$ instance obtained from a $1.5$-approximate TSP routine is a directly interpretable guarantee. The stronger LP-based theorem in §4 is a separate result and is not needed to establish this one. Friggstad et al., arXiv:2111.08138v1, pp. 2, 7–9.

A completed formalization would connect the paper's demand-aware CVRP model to a reusable published metric-route module, add definitions for optimal consecutive tour splitting and loop-allowed matching, and certify the stated branch and radial inequalities. Related platform results cover unit-demand VRP and TSP bounds, but their capacity and demand conventions differ. This mission introduces the unsplittable-demand statements rather than treating those unit-demand results as interchangeable.

Difficulty

The direct shortcut from a TSP tour to CVRP routes does not control capacity: a segment cheap in distance may carry too much demand. The big clients are especially restrictive at $\delta=1/3$, since no feasible route can contain three of them. The tank lemma has to relate a partition of a fixed visiting order to the four radial terms with the exact coefficients shown above. The final ratio depends on comparing the two algorithm branches, including both matching bounds; an arbitrary feasible solution with a small cost would not establish a guarantee for Algorithm 1. Friggstad et al., arXiv:2111.08138v1, pp. 5–8.

Formalization scope

Lean represents the nodes by Fin (n+1), with depot $0$ and all other nodes as clients. A route is a nonempty list of clients, and a solution is a list of routes whose concatenation contains each required client once. The metric and route-cost functions come from the published SupplyChainTheory_vrp definition module; its unit-demand feasibility predicate is not used. The number of clients may be zero. Costs and demands are real, capacity is exactly $1$, and every client demand lies in $(0,1]$. The value at the depot is unused.

Each optimum in the statement is a real infimum over a finite, nonempty, nonnegative cost set for a valid instance. Singleton routes make the split and matching candidate sets nonempty; an ordering exists for every finite client set. The TSP inputs list exactly their intended client sets, and their $\alpha$ guarantees refer to the corresponding TSP optima. The explicit $\alpha\ge1$ condition records what the paper means by an approximation ratio. Lemma 7 is stated for any client subset because Algorithm 1 applies it both to the small-client tour and the all-client tour. Display (5) is an upper bound: the printed equality replaces the tour cost by upper bounds. The running-time assertions are outside this cost formalization. Friggstad et al., arXiv:2111.08138v1, pp. 5–8.

The goal bounds the cost of the specified algorithm, including attainment by a feasible solution. Merely asserting that some feasible solution has cost at most $(\alpha+1.75)\mathrm{opt}$ would be trivial, since an optimal solution already does. Contributions to the finite-tour, consecutive-split, radial, matching and tank-event lemmas are useful beyond the final ratio.

Selected references

• Z. Friggstad, R. Mousavi, M. Rahgoshay, and M. R. Salavatipour, Improved Approximations for CVRP with Unsplittable Demands, arXiv:2111.08138v1, 2021; published in Mathematics of Operations Research, 2025. arXiv

Motivation

Firms that disclose a product carbon footprint can lower it in two ways: by cutting the emissions they control (better materials, cleaner processes), which costs money up front, or by buying carbon offsets from a third party at a constant price per tonne. Offsets have become cheap and widely available, and the business press has repeatedly argued that cheaper offsets let firms substitute away from costly abatement (The Wall Street Journal 2008, Forbes 2020 and The Washington Post 2020, as cited by Gao and Souza, p. 14). Whether that substitution actually happens matters for climate policy: if a lower offset price always raises a firm's own emissions, cheap offsets undercut real abatement.

Gao and Souza, Carbon Offsetting with Eco-Conscious Consumers (Management Science, 2022, doi:10.1287/mnsc.2021.4293), study this question in a model where demand responds to the disclosed footprint. Their Proposition 1 shows that the conventional intuition can fail in both directions of preference correlation: a cheaper offset can make the firm cut its controllable emissions. This mission formalizes that proposition together with the lemmas of its proof.

Setting

A firm sells to $m>0$ consumers. It chooses a controllable emission level $e\in[0,\bar e]$ per unit, which determines a unit cost $c(e)$ and a fixed cost $f(e)$, with $c'<0$, $c''>0$, $f'<0$, $f''>0$ on $[0,\bar e]$ and $f(\bar e)=0$. Each unit also carries uncontrollable emissions $e_o\ge0$. At the offset price $g>0$ the firm offsets $t\in[0,e+e_o]$ units, and discloses the footprint $\mathcal E=e+e_o-t$.

A consumer with valuation $V\ge0$ and environmental disutility $\Xi$ gets utility $u=V-\Xi\mathcal E-p$ at the price $p$, and buys if and only if $u\ge0$. A share $\alpha\in[0,1]$ of consumers is eco-conscious ($\Xi=\xi>0$); the rest are eco-unconscious ($\Xi=0$). A share $\beta_c$ of eco-conscious and $\beta_u$ of eco-unconscious consumers have the high valuation $v_h$; the others have $v_l$, with $0\le v_l$, $c(\bar e)<v_l<v_h$. The demand is the sum of the four segment masses whose utility is nonnegative, and the firm's profit is

$$\pi(p,e,t\mid g)=(p-c(e)-gt)\,d(p,e,t)-f(e).$$

A best response to $g$ is a feasible $(p,e,t)$ maximizing $\pi(\cdot\mid g)$.

Two special cases carry the analysis: Case N ($\beta_u=1$, negative correlation between caring about function and caring about the environment) and Case P ($\beta_c=1$, positive correlation). For $x\ge0$, the segment-optimal emission $e_{x,a}$ is the maximizer over $[0,\bar e]$ of $-(c(e)+xe)\,a\,m-f(e)$: the abatement level a firm chooses when it serves a segment of size $a$ and pays $x$ per unit of footprint. The proof compares the profit of covering the whole market at $v_l$ with that of serving only high-value consumers at $v_h$; their difference $h(g)$ has a least zero $X$, the offset price at which the firm switches.

Formalization targets

Goal: Proposition 1

In Case N, with $\alpha>0$, $\beta_c<B_2=\big(\frac{v_l-c(\bar e)}{v_h-c(\bar e)}-1+\alpha\big)/\alpha$, a sign change of $h$ at its least zero $X<\xi$, and condition (1) of the proof at $X$, there are offset prices

$$0<g_1<g_2\quad\text{with}\quad t^*(g_i)>0,\quad e^*(g_1)\le e^*(g_2),\quad d_u^*(g_1)=d_u^*(g_2),\quad d_c^*(g_1)>d_c^*(g_2),$$

for every pair of best responses (which exist), with strict emissions inequality when $e_{X,1}<\bar e$ and $e_{X,a}>0$. In Case P the analogue holds with $v_h-v_l<\xi e_o$, $\beta_u<\tilde B_2$, $d_c^*(g_1)=d_c^*(g_2)$ and $d_u^*(g_1)>d_u^*(g_2)$.

Milestones

1. $e_{x,a}$ exists, is unique and solves the first-order condition when it is interior (Online Supplement p. 1).
2. Lemma VI1: $e_{x,a}$ is weakly decreasing in $x$ and in $a$, plus its strict version for $a<1$.
3. In each case, the reduction of the firm's problem to two candidate profiles when offsets are bought.
4. $h(0)>0\iff\beta_c<B_2$, and existence of $X$ (Case N); $\beta_u<\tilde B_2\Rightarrow h(0)>0$ and existence of $X$ (Case P).
5. The switch of best responses across $X$, in each case.
6. Condition (1) is an upper set in $\beta_c$ (Case N) and in $\beta_u$ (Case P): the thresholds $B_1$, $\tilde B_1$.

Significance

Proposition 1 identifies a mechanism by which cheaper offsets complement, rather than substitute for, controllable abatement. In Case N a lower offset price lets the firm lower its footprint enough to attract low-value eco-conscious consumers; in Case P it lets the firm price down to the low-value eco-unconscious consumers while keeping eco-conscious buyers. In both cases the served volume grows, and because abatement is a fixed cost, the larger volume makes deeper abatement worthwhile (economies of scale). The paper builds its NGO-pricing results (Propositions 2 and 4) on this subgame analysis.

The result is proved in the paper by a case analysis and derivative arguments; it has no machine-checked proof. Formalizing it produces a complete, checked treatment of a discontinuous best response in a pricing model with threshold demand, and it makes several steps of the published proof precise: where the paper asserts $\partial h/\partial g|_{g=X}<0$ and "$X<G$" without proof, the formal statements carry them as disclosed hypotheses, and the formalization of "$\beta_c\in(B_1,B_2)$ for some $B_1,B_2$" pins both thresholds down.

Difficulty

The best response is not a continuous function of $g$: demand is a step function of price and footprint, so the firm's problem splits into six regimes (Online Supplement I1), and the optimal price jumps between $v_l$, $v_h$ and the footprint-adjusted prices. Comparative statics by differentiating first-order conditions, the method of the paper's lemmas, applies only within a regime. The obvious argument, "$e^*$ is decreasing in $g$ by Lemma VI1", is wrong across the switch at $X$: there the served segment shrinks, and Lemma VI1's monotonicity in the segment size works against its monotonicity in the price. Showing that the jump in segment size dominates requires controlling the best response on both sides of $X$, including uniqueness of the best response and the behaviour of $e_{x,a}$ at the ends of $[0,\bar e]$ where the first-order condition fails.

Formalization scope

All quantities are real. The model is one definition file, EcoOffset.Subgame.Model, with a structure Params of primitives and a predicate Params.Standing bundling the standing assumptions of §3: $m,\bar e,\xi>0$, $e_o\ge0$, $\alpha,\beta_c,\beta_u\in[0,1]$, $0\le v_l$, $c(\bar e)<v_l<v_h$, $c,f$ of class $C^2$ on $\mathbb R$ with the sign conditions on $c',c'',f',f''$ on the closed interval $[0,\bar e]$, and $f(\bar e)=0$. Prices range over all of $\mathbb R$; consumers buy at zero utility. A best response is a predicate, never a chosen function, and the goal quantifies over every best response at $g_1$ and $g_2$ and asserts that one exists. $e_{x,a}$ is defined as the maximizer, not through the paper's root of the first-order condition (which does not exist at $x=0$). The switching price $X$ is a variable pinned by $h(X)=0$ and $h>0$ on $[0,X)$.

Added hypotheses relative to the page, all disclosed in the statements: $X<\xi$ (the proof's unproved "$X<G$"; numerical Case N instances violate it); a sign change of $h$ at $X$ (the proof's unproved $\partial h/\partial g|_{g=X}<0$); $\alpha>0$ in Case N and $\alpha<1$ in Case P (divisions in $B_2$, $\tilde B_2$); $e_o>0$ for the existence of $X$ in Case N; explicit interiority conditions in place of "if $\bar e$ is large enough".

Stating the goal about the two named profiles (for example $e_{g_1,1}\le e_{g_2,a}$) would reduce it to Lemma VI1 plus algebra and is ruled out: the goal is about best responses of the full profit maximization. The paper's "for some $B_1,B_2\ge0$" is likewise not used, since $B_1=B_2$ would make it vacuous.

A complete development needs: existence, uniqueness and continuity in $x$ of the maximizer of a strictly concave function on an interval (Berge's maximum theorem in one dimension); monotone comparative statics for $e_{x,a}$; the case analysis of the step-function demand; and intermediate-value arguments for $X$. The first two are reusable for any one-dimensional parametric optimization. Proofs of individual milestones, and of the goal from the milestones, are welcome.

Selected references

• F. Gao and G. C. Souza, Carbon Offsetting with Eco-Conscious Consumers, Management Science, 2022. https://doi.org/10.1287/mnsc.2021.4293
• F. Gao and G. C. Souza, Carbon Offsetting with Eco-Conscious Consumers, preprint with Online Supplement (the version formalized here; all page numbers refer to it), SSRN 3440652. https://ssrn.com/abstract=3440652