All missions

Motivation

A convex optimization problem can be handed to a semidefinite programming solver only after its constraints and objective have been written as linear matrix inequalities (LMIs): conditions of the form $\mathcal A(x,u) \succeq 0$, where $\mathcal A$ is affine in the decision variables $x$ and in auxiliary variables $u$, and $\succeq 0$ means positive semidefinite. A large share of modern engineering optimization is built this way, in robust control, structural design, and statistics and machine learning (nuclear-norm and spectral-norm regularization, eigenvalue optimization). Modeling tools such as CVX and YALMIP rest on a catalog of functions known to admit such a description.

Lecture 4 of A. Ben-Tal and A. Nemirovski, Lectures on Modern Convex Optimization (SIAM, 2001, doi:10.1137/1.9780898718829), builds that catalog for the semidefinite cone. Its central entry is a general rule: a convex function of a symmetric matrix that depends only on the eigenvalues, symmetrically, is expressible by LMIs whenever the underlying function of a vector is. This covers the largest eigenvalue, sums of the $k$ largest eigenvalues (Ky Fan, 1949), Schatten norms $\|X\|_p$ and powers of the determinant at once. The tool behind it is the theory of majorization (Hardy, Littlewood and Pólya, 1929; Rado, 1952) together with Birkhoff's theorem on double-stochastic matrices (1946).

Setting

For a symmetric $m\times m$ real matrix $X$, $\lambda(X) = (\lambda_1(X),\dots,\lambda_m(X))$ denotes its eigenvalues counted with multiplicity in nonascending order, $\lambda_1(X) \ge \cdots \ge \lambda_m(X)$. $S_k(X) = \lambda_1(X) + \cdots + \lambda_k(X)$ is the sum of the $k$ largest. For a vector $y \in \mathbb R^m$, $S_j(y)$ is the sum of its $j$ largest entries, and $X[x]$ is the convex hull of the $m!$ coordinate permutations of $x$. A function $g : \mathbb R^m \to \mathbb R\cup\{+\infty\}$ is symmetric if permuting the coordinates of its argument leaves its value unchanged. A matrix is double-stochastic if its entries are nonnegative and every row and column sums to $1$.

A function $g$ is semidefinite representable (SDr) if there is a map $\mathcal S(x,t,u)$, affine in $(x,t,u) \in \mathbb R^m\times\mathbb R\times\mathbb R^k$ with values in the symmetric $N\times N$ matrices, such that

$$t \ge g(x) \iff \exists u : \mathcal S(x,t,u) \succeq 0 \qquad \text{for all } x \in \mathbb R^m,\ t\in\mathbb R.$$

For a $k\times l$ matrix $X$ ($k \le l$), the singular values are $\sigma_i(X) = \lambda_i((XX^T)^{1/2})$, and $\Sigma_j(X) = \sigma_1(X)+\cdots+\sigma_j(X)$.

Formalization targets

Goal: Proposition 4.2.1 (p. 151)

Let $g$ be symmetric and SDr with representation $\mathcal S$. Then for every symmetric $m\times m$ matrix $X$ and real $t$,

$$t \ge g(\lambda(X)) \iff \exists\, x \in \mathbb R^m,\ u:\ \ \mathcal S(x,t,u)\succeq 0,\ \ x_1\ge\cdots\ge x_m,\ \ S_j(X)\le x_1+\cdots+x_j\ (j=1,\dots,m-1),\ \ \operatorname{Tr}X = x_1+\cdots+x_m. \tag{4.2.3}$$

Milestones, in attack order

1. (A), p. 148: $X \succeq X' \Rightarrow \lambda_i(X) \ge \lambda_i(X')$ for every $i$.
2. Example 18.c, p. 147: for $k \le m$, $S_k(X) \le t$ iff there are $s \in \mathbb R$ and $Z$ with $t - ks - \operatorname{Tr}Z \ge 0$, $Z \succeq 0$, $Z - X + sI_m \succeq 0$ (4.2.2).
3. Birkhoff's theorem, p. 281: the double-stochastic matrices are exactly the convex combinations of permutation matrices. This is referenced, already proved on the platform as FamousTheorems.birkhoff_von_neumann.
4. (C), p. 281: $f(Px) \le f(x)$ for a convex symmetric $f$, $x \in \operatorname{Dom} f$ and double-stochastic $P$.
5. Claim (majorization principle), p. 285: $X[x] = \{y : S_j(y) \le S_j(x),\ j = 1,\dots,m-1,\ \sum_i y_i = \sum_i x_i\}$.
6. (D), p. 282: for a real-valued convex symmetric $f$, $f(\lambda(A)) = \max_{V \text{ orthogonal}} f(\operatorname{Dg}(V^TAV))$.
7. Proposition 4.2.2, p. 154: for $g$ symmetric, monotone on $\mathbb R^k_+$ and SDr, $t \ge g(\sigma(X))$ iff $\exists x, u$ with $\mathcal S(x,t,u)\succeq 0$, $x_1 \ge \cdots \ge x_k$, $\Sigma_j(X) \le x_1+\cdots+x_j$ for $j = 1,\dots,k$ (4.2.4).

A further level

A strengthened variant of the goal states that (4.2.3) remains exact when the ordering constraint $x_1 \ge \cdots \ge x_m$ is removed.

Significance

The result itself. Proposition 4.2.1 reduces semidefinite representability of a spectral function on $\mathbf S^m$, a space of dimension $m(m+1)/2$, to semidefinite representability of a symmetric function on $\mathbb R^m$. The extra cost is $m$ scalar variables, $m-1$ ordering inequalities, $m-1$ Ky Fan constraints (each an LMI of size $m$ by 18.c) and one trace equation. The representation is explicit, so a modeling language can generate it mechanically. Proposition 4.2.2 does the same for functions of singular values, which covers the nuclear norm and the operator norm of rectangular matrices. Fact (D) is the variational description that makes $X \mapsto g(\lambda(X))$ convex (Davis, 1957; Lewis, 1996).

Formalizing it. All results here are classical and proved in the book, partly through exercises (4.14–4.16 for the goal). None of them is formalized on Prove2Me beyond Birkhoff's theorem, which Mathlib has as doublyStochastic_eq_convexHull_permMatrix. A related proved platform item, Matrix.IsHermitian.sorted_eigenvalues_le_add_of_re_dotProduct_le, is a Weyl-type inequality that implies (A) when its slack is zero. Mathlib has sorted eigenvalues of Hermitian matrices (eigenvalues₀) but no Ky Fan sums, no majorization theory and no notion of semidefinite representation. This mission produces them.

Difficulty

The forward direction of every representation is a choice of witness. The content is in the converse: from an arbitrary feasible point of the LMI system one must recover the inequality for the eigenvalues. For (4.2.3) this means showing that partial-sum domination plus equal totals places $\lambda(X)$ inside the convex hull of the permutations of the witness $x$. The obvious coordinatewise comparison fails, because $\lambda(X)$ is not dominated entrywise by $x$. The hard half of the majorization principle (Exercise 4.15) is this step, and it does not follow from convexity of $S_j$ alone. In Proposition 4.2.2 the witness only dominates the singular values in partial sums, with no equality of totals, so majorization alone does not suffice there.

Formalization scope

Vectors are Fin m → ℝ (0-based indices) and matrices Matrix (Fin m) (Fin m) ℝ. Symmetric means Matrix.IsHermitian and $\succeq 0$ means Matrix.PosSemidef, which includes symmetry. $\lambda(X)$ is Mathlib's antitone IsHermitian.eigenvalues₀; it is applied only to symmetric matrices. Functions with values in $\mathbb R\cup\{+\infty\}$ are EReal-valued and never $-\infty$, and only order comparisons with real numbers are made on them. A representation $\mathcal S$ is an explicit affine map with symmetric coefficient matrices. In Proposition 4.2.2 the function $g$, given on $\mathbb R^k_+$ only, is extended by $+\infty$ outside $\mathbb R^k_+$. The singular values are written as $\sqrt{\lambda_i(XX^T)}$, which equals $\lambda_i((XX^T)^{1/2})$. Typos on the page are corrected and listed in the items: $S_k(x)$ for $S_k(X)$ in 18.c, and $f$ and $j = 1,\dots,m$ in Proposition 4.2.2.

The claim "$f$ is SDr" admits a trivializing formalization: asserting that some LMI system projects onto the epigraph, with no control over its shape or size, says nothing beyond convexity. Every statement here instead pins the representation down as the book's explicit system (4.2.2), (4.2.3) or (4.2.4), quantified over every symmetric matrix and every real $t$.

Beyond the paper. One strengthened variant is posed: Proposition 4.2.1 with the constraint $x_1 \ge \cdots \ge x_m$ removed from (4.2.3) (finding F1). The evidence is that $x_1+\cdots+x_j$ never exceeds the sum of the $j$ largest entries of $x$, so the remaining constraints already express majorization. The variant is not a milestone, and the book's statement stays the goal.

A complete development needs:

• majorization on $\mathbb R^m$ (sums of largest entries, the permutation hull);
• Birkhoff's theorem, available in Mathlib;
• monotonicity of sorted eigenvalues in the Loewner order;
• spectral decomposition for constructing witnesses;
• singular values through $XX^T$.

Majorization, the Ky Fan representation and fact (A) are reusable well beyond this chapter, for instance in eigenvalue optimization and the analysis of interior-point methods. Contributions of these as standalone results are welcome.

Selected references

• A. Ben-Tal, A. Nemirovski, Lectures on Modern Convex Optimization: Analysis, Algorithms, and Engineering Applications, MPS/SIAM Series on Optimization, SIAM, 2001. doi:10.1137/1.9780898718829
• G. Birkhoff, Tres observaciones sobre el álgebra lineal, Univ. Nac. Tucumán Rev. Ser. A 5 (1946), 147–151.
• K. Fan, On a theorem of Weyl concerning eigenvalues of linear transformations I, Proc. Natl. Acad. Sci. USA 35 (1949), 652–655. doi:10.1073/pnas.35.11.652
• A. S. Lewis, Convex analysis on the Hermitian matrices, SIAM J. Optim. 6 (1996), 164–177. doi:10.1137/0806009
• A. W. Marshall, I. Olkin, B. C. Arnold, Inequalities: Theory of Majorization and Its Applications, 2nd ed., Springer, 2011. doi:10.1007/978-0-387-68276-1

Motivation

In the present paper we introduce and study Bosonic Gaussian classical-quantum (c-q) channels; the embedding of the classical input into quantum is always possible and therefore the classical entanglement-assisted capacity C_{ea} under appropriate input constraint is well defined. We prove a general property of entropy increase for weak complementary channel, that implies the equality C_{ea}=C (where C is the unassisted capacity) for certain class of c-q Gaussian channel under appropriate energy-type constraint. On the other hand, we show by explicit example that the inequality C<C_{ea} is not unusual for constrained c-q Gaussian channel.

This mission is the statement-level formalization of Gaussian classical-quantum channels: gain of entanglement-assistance (arXiv:1211.4774v1). 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 §3, unnumbered criterion (14): Gaussian c-q iff isotropic K (§3, unnumbered criterion (14): Gaussian c-q iff isotropic K, PDF p. 5). 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:

• Abstract/main claim: strict entanglement-assistance gain in Example 2: A valid unrestricted unassisted-capacity identification or a valid operational separation for the channel (31). (source-ambiguity)
• §4.2, printed unassisted capacity (33): A valid unrestricted unassisted-capacity identification or a valid operational separation for the channel (31). (source-ambiguity)
• §4.2, claimed capacity-gain asymptotics: A valid unrestricted unassisted-capacity identification or a valid operational separation for the channel (31). (source-ambiguity)

Selected references

• Gaussian classical-quantum channels: gain of entanglement-assistance, arXiv:1211.4774v1, https://arxiv.org/abs/1211.4774v1

Improve the separation exponent between block sensitivity and sensitivity of total Boolean functions. This mission targets $\alpha\ge2.13$; higher is better.

For every $\varepsilon>0$ and every integer $S\ge2$, the goal asks for a total Boolean function $f$ with $s(f)\ge S$ and $bs(f)\ge s(f)^{2.13-\varepsilon}$. The shared definition SensitivityCampaign.AchievesExponent expresses this requirement. This is an open proof target.

Using a finite certificate. Choose a total Boolean function $f$, an input $x$, and integers $A,B>1$. Prove $s(f)\le A$, $B\le bs(f,x)$, and $A^{2.13}\le B$, then apply SensitivityCampaign.finite_certificate. The shared theorem handles normalization and passage to arbitrarily large sensitivity. Direct proofs of the asymptotic goal are equally welcome. Use exact certified bounds; numerical estimates alone do not establish the target.

Background: OpenAI problem 132 and the campaign proposal.

Comparing single-coordinate and block changes

Two natural ways to measure the local instability of a Boolean function can behave differently. One counts individual input bits whose flips change the answer. The other permits several bits to change together, provided the chosen groups are disjoint. Quantifying the largest possible gap is a question in the complexity of total Boolean functions, and the Block Sensitivity vs. Sensitivity campaign tracks concrete lower bounds on its separation exponent.

The task is to establish a specified asymptotic exponent using the campaign's shared definitions. A numerical score for an abstract recurrence is insufficient: the witnesses must be actual total Boolean functions, and the sensitivities must become arbitrarily large. This mission records one completed construction checkpoint and its exact mathematical scope. Earlier accepted results, the original OpenAI construction and the community's intermediate refinements provide the surrounding research history in the campaign references.

Boolean functions and sensitive blocks

A total Boolean function on $n$ coordinates is a map $f:\{0,1\}^n\to\{0,1\}$ defined at every binary input. At an input $x$, a coordinate is sensitive if flipping that bit changes the output. The sensitivity $s(f,x)$ counts these coordinates, and $s(f)$ is the maximum over all inputs.

A sensitive block at $x$ is a nonempty subset of coordinates whose simultaneous flip changes the output. The block sensitivity $bs(f,x)$ is the maximum size of a collection of pairwise disjoint sensitive blocks at that same input. The global value $bs(f)$ maximizes this quantity over all inputs. Blocks in one witness share an input and must be disjoint as coordinate sets; their sizes need not agree. These conventions are exactly those in the shared foundation mission.

Formalization target

For every real $\varepsilon>0$ and every integer $S\ge2$, establish the existence of a dimension $n$ and a total Boolean function $f$ such that

$$s(f)\ge S,\qquad bs(f)\ge s(f)^{2.1303-\varepsilon}.$$

The number $2.1303$ is an exact finite decimal. The witnesses may depend on both $\varepsilon$ and $S$. This is the campaign proposition $\operatorname{AchievesExponent}(2.1303)$, and the main theorem instantiates its template literally.

A supporting finite-family theorem asserts that, for every natural number $m$, there is a finite total Boolean function with

$$s(f_m)\le3418946681687790375032\cdot50063687^m,\qquad bs(f_m,0)\ge25260794820729601^m.$$

The associated exact logarithmic quotient is approximately $2.13031993959$. It is a lower bound supplied by this construction, rather than a determination of the optimal separation exponent. The fixed prefactor is independent of $m$, and the lower bound concerns explicit nonempty pairwise disjoint sensitive blocks at the all-zero input.

Consequences and verification status

Any fixed exponent strictly below $2.1303$ gives a literal power separation along functions of unbounded sensitivity. Taking increasing thresholds $S$ yields an infinite family whose sensitivities tend to infinity. The theorem does not assert a loss-free inequality at the displayed endpoint, an optimality result, or an improved universal upper bound.

The full construction, its actual Boolean functions and the exponent conversion have passed complete local Lean kernel checks with only the standard three axioms. The shared-labeling lemma is separately accepted and publicly Proved. The main theorem currently has a checked reduction on Prove2Me; the larger finite-family dependency still awaits server acceptance after combined submissions exceeded the300-second verification limit. This mission records the exact proved local statement while preserving that server-status distinction.

The reusable content includes the finite-family statement, the unchanged campaign finite-certificate interface, and the exact exponent conversion. Those interfaces permit later constructions to replace the finite witnesses without changing what the campaign's asymptotic goal means. Source attribution to the original OpenAI development, community contributors and Robin Kothari/Codex is retained in the published proof sources. The new contribution is credited to username yousofy with Codex.

Why the quantifiers matter

A high block-sensitivity value at one input does not by itself control maximum sensitivity over all inputs. Likewise, a finite example with a favorable ratio does not by itself state the required unbounded-sensitivity family. A valid contribution must account for both requirements. Checking only selected inputs, allowing overlapping blocks, or changing the shared complexity definitions would establish a different assertion.

A large part of the formal verification concerns this connection between finite construction data and actual Boolean functions. Exact integer comparisons also matter: rounded decimal scores and floating-point feasibility checks do not prove the target inequality. Independent source and numerical audits supplement the Lean kernel checks; the authoritative server status of each referenced theorem remains visible separately.

Formalization scope and reusable interfaces

The formalization uses Lean4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Finite input coordinates are represented by Fin n, and Boolean outputs by Bool. The shared SensitivitySeparation definitions count single-bit changes and nonempty pairwise disjoint sensitive blocks. The shared SensitivityCampaign definition quantifies over arbitrary positive real exponent loss and integer sensitivity thresholds.

The published goal has no hypothesis assuming the desired construction, separation, or labeling. In particular, zero-dimensional or bounded-sensitivity examples cannot satisfy the threshold quantifier. Standard real powers are used for the final comparison, while construction certificates are checked using exact natural-number arithmetic. The shared finite-certificate theorems and supporting finite-family statements are included as reference items. Corrections to exposition, independently checked proofs of the same goal, reusable supporting lemmas and genuinely stronger constructions are welcome.

Selected references

• Prove2Me community, Block Sensitivity vs. Sensitivity, collaborative campaign,2026. Campaign and shared definitions.
• OpenAI, Sensitivity separation construction, Lean mathematical development. Original construction.
• Robin Kothari and Codex, Separation exponent at least2.075, Prove2Me,2026. Accepted foundation and retained attribution.
• yousofy with Codex, Shared local-lemma labelings: exponent2.1303, Prove2Me,2026. Main statement and proof submissions.

Comparing single-coordinate and block changes

Two natural ways to measure the local instability of a Boolean function can behave differently. One counts individual input bits whose flips change the answer. The other permits several bits to change together, provided the chosen groups are disjoint. Quantifying the largest possible gap is a question in the complexity of total Boolean functions, and the Block Sensitivity vs. Sensitivity campaign tracks concrete lower bounds on its separation exponent.

The task is to establish a specified asymptotic exponent using the campaign's shared definitions. A numerical score for an abstract recurrence is insufficient: the witnesses must be actual total Boolean functions, and the sensitivities must become arbitrarily large. This mission records one completed construction checkpoint and its exact mathematical scope. Earlier accepted results, the original OpenAI construction and the community's intermediate refinements provide the surrounding research history in the campaign references.

Boolean functions and sensitive blocks

A total Boolean function on $n$ coordinates is a map $f:\{0,1\}^n\to\{0,1\}$ defined at every binary input. At an input $x$, a coordinate is sensitive if flipping that bit changes the output. The sensitivity $s(f,x)$ counts these coordinates, and $s(f)$ is the maximum over all inputs.

A sensitive block at $x$ is a nonempty subset of coordinates whose simultaneous flip changes the output. The block sensitivity $bs(f,x)$ is the maximum size of a collection of pairwise disjoint sensitive blocks at that same input. The global value $bs(f)$ maximizes this quantity over all inputs. Blocks in one witness share an input and must be disjoint as coordinate sets; their sizes need not agree. These conventions are exactly those in the shared foundation mission.

Formalization target

For every real $\varepsilon>0$ and every integer $S\ge2$, establish the existence of a dimension $n$ and a total Boolean function $f$ such that

$$s(f)\ge S,\qquad bs(f)\ge s(f)^{2.1301-\varepsilon}.$$

The number $2.1301$ is an exact finite decimal. The witnesses may depend on both $\varepsilon$ and $S$. This is the campaign proposition $\operatorname{AchievesExponent}(2.1301)$, and the main theorem instantiates its template literally.

A supporting finite-family theorem asserts that, for every natural number $m$, there is a finite total Boolean function with

$$s(f_m)\le32057676379612508934192581\cdot7922^m,\qquad bs(f_m,0)\ge201838849^m.$$

The natural number $m$ indexes distinct finite construction instances; it is not a dimension bound. The fixed prefactor does not depend on $m$. The associated exact logarithmic quotient is a lower bound supplied by this construction, rather than a determination of the optimal separation exponent.

Consequences and verification status

Any fixed exponent strictly below $2.1301$ gives a literal power separation along functions of unbounded sensitivity. Taking increasing thresholds $S$ yields an infinite family whose sensitivities tend to infinity. The theorem does not assert a loss-free inequality at the displayed endpoint, an optimality result, or an improved universal upper bound.

The main theorem and its reusable finite-family input have accepted proofs and public Proved status. The exact growth-rate lower bound log(201838849)/log(7922), approximately2.13012479519, is also separately accepted. These facts are recorded with source hashes and acceptance receipts in the accompanying proof package.

The reusable content includes the finite-family statement, the unchanged campaign finite-certificate interface, and the exact exponent conversion. Those interfaces permit later constructions to replace the finite witnesses without changing what the campaign's asymptotic goal means. Source attribution to the original OpenAI development, community contributors and Robin Kothari/Codex is retained in the published proof sources. The new contribution is credited to username yousofy with Codex.

Why the quantifiers matter

A high block-sensitivity value at one input does not by itself control maximum sensitivity over all inputs. Likewise, a finite example with a favorable ratio does not by itself state the required unbounded-sensitivity family. A valid contribution must account for both requirements. Checking only selected inputs, allowing overlapping blocks, or changing the shared complexity definitions would establish a different assertion.

A large part of the formal verification concerns this connection between finite construction data and actual Boolean functions. Exact integer comparisons also matter: rounded decimal scores and floating-point feasibility checks do not prove the target inequality. Independent source and numerical audits supplement the Lean kernel checks; the authoritative server status of each referenced theorem remains visible separately.

Formalization scope and reusable interfaces

The formalization uses Lean4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Finite input coordinates are represented by Fin n, and Boolean outputs by Bool. The shared SensitivitySeparation definitions count single-bit changes and nonempty pairwise disjoint sensitive blocks. The shared SensitivityCampaign definition quantifies over arbitrary positive real exponent loss and integer sensitivity thresholds.

The published goal has no hypothesis assuming the desired construction, separation, or labeling. In particular, zero-dimensional or bounded-sensitivity examples cannot satisfy the threshold quantifier. Standard real powers are used for the final comparison, while construction certificates are checked using exact natural-number arithmetic. The shared finite-certificate theorems and supporting finite-family statements are included as reference items. Corrections to exposition, independently checked proofs of the same goal, reusable supporting lemmas and genuinely stronger constructions are welcome.

Selected references

• Prove2Me community, Block Sensitivity vs. Sensitivity, collaborative campaign,2026. Campaign and shared definitions.
• OpenAI, Sensitivity separation construction, Lean mathematical development. Original construction.
• Robin Kothari and Codex, Separation exponent at least2.075, Prove2Me,2026. Accepted foundation and retained attribution.
• yousofy with Codex, Coupled target and guard profiles: exponent2.1301, Prove2Me,2026. Main statement and proof submissions.

Motivation

A rule that assigns an output bit to every input string can respond differently to changing one bit and changing a group of bits. Sensitivity counts individual changes that affect an output. Block sensitivity permits disjoint groups of coordinates to change separately. Understanding the largest possible difference between these measures is a question about the dependence of Boolean functions on their inputs.

Hao Huang's 2019 theorem established a polynomial relation between sensitivity and polynomial degree, resolving the Sensitivity Conjecture. Determining the sharp quantitative relation between sensitivity and block sensitivity remained a separate problem. OpenAI's 2026 result disproved a universal quadratic bound for total Boolean functions. Subsequent accepted results include the 2.075 theorem by Robin Kothari and Codex and the accepted 2.085 certificate developed for yousofy with Codex. This mission records a stronger quantitative target, 2.119.

Setting

A total Boolean function is a map

$$f:\{0,1\}^n\longrightarrow\{0,1\}$$

that assigns an output to every length-$n$ bit string. For an input $x$ and a coordinate set $B$, let $x^B$ denote the string obtained by reversing exactly the bits in $B$.

A coordinate $i$ is sensitive at $x$ if $f(x^{\{i\}})\ne f(x)$. Write $s(f,x)$ for the number of such coordinates, and define

$$s(f)=\max_x s(f,x).$$

A sensitive block at $x$ is a nonempty coordinate set $B$ with $f(x^B)\ne f(x)$. Let $bs(f,x)$ be the largest size of a family of pairwise disjoint sensitive blocks at the same input, and set

$$bs(f)=\max_x bs(f,x).$$

Each member of a block family is flipped separately from the original input. The definitions use finite coordinate sets and finite families of blocks.

Formalization target

The main theorem is

$$\operatorname{AchievesExponent}(2.119),\qquad 2.119=\frac{2119}{1000}.$$

Explicitly, for every real $\varepsilon>0$ and every natural number $S\ge2$, there must exist a natural number $n$ and a total Boolean function $f:\{0,1\}^n\to\{0,1\}$ such that

$$s(f)\ge S,\qquad bs(f)\ge s(f)^{2.119-\varepsilon}.$$

The formal statement is SensitivityCampaign.AchievesExponent (2.119 : ℝ). Both $n$ and $f$ may depend on $\varepsilon$ and $S$. The decimal denotes the exact rational number displayed above. The claim includes arbitrarily small positive exponent loss and arbitrarily large sensitivity; neither quantifier is optional.

In particular, the statement gives a fixed exponent 2.118 for functions of unbounded sensitivity, strictly above 2.1. The target is a specific checkpoint in the broader problem of determining the optimal separation exponent. It does not assert that the displayed endpoint is attained without exponent loss.

Significance and verification status

The target extends these earlier quantitative bounds and crosses the campaign's 2.10 checkpoint. It requires the separation to persist beyond every sensitivity threshold, so a favorable comparison confined to bounded sensitivity would not establish the result. It also leaves the exact optimal exponent unresolved.

The new contribution is a certified finite construction and formal proof within the existing nine-predicate framework. The proof retains the generic development and attribution from Kothari and Codex's accepted 2.075 contribution, including its credit to abhishekdpseok's accepted 2.0635 proof and the earlier OpenAI and community work. The new certificate and its assembly were developed for username yousofy with Codex.

The complete self-contained source has passed standalone compilation in Lean 4.33.1, with only the standard axioms propext, Classical.choice, and Quot.sound. Its numerical certificates and source correspondence have also undergone independent checks. Prove2Me accepted the complete proof on 20 October 2026, submission bb3251a4-f00f-4b06-962a-97be2de5db1b. The public theorem and proof record records its verification status. Further work can examine the proof, improve its reusable interfaces, or establish stronger bounds.

Difficulty

The sensitivity bound must hold at every input. A calculation only at an input supporting many sensitive blocks does not control this maximum. Likewise, a collection of output-changing coordinate sets provides the required block bound only when every set is nonempty and the sets are pairwise disjoint.

The asymptotic requirement creates a separate difficulty. Increasing the dimension alone does not force sensitivity to increase, because added coordinates may be ignored. A complete argument must provide witnesses above every prescribed sensitivity threshold. Finally, the exact rational exponent needs rigorous comparisons: an approximate numerical score alone does not prove the stated inequality.

Formalization scope

The shared Lean representation is f : (Fin n → Bool) → Bool, using the definitions in SensitivityCampaign and OAI.Paper320. Sensitivity is the finite supremum over all inputs. Block sensitivity takes the finite supremum over all block families at each input, assigning zero to any family that fails the disjointness, nonemptiness, or output-change conditions. The empty family is allowed.

The target imposes no normalization on $f$ or a distinguished input, and it includes no promise restricting the function's domain. Dimensions zero and constant functions are permitted by the underlying types, but cannot satisfy $s(f)\ge S\ge2$. Natural-number complexity measures are cast to real numbers before real exponentiation. Every positive $\varepsilon$ is included, even when $2.119-\varepsilon$ is nonpositive.

The complete source imports Mathlib and the unchanged campaign definition. Existing reusable infrastructure includes the complexity measures, coordinate reindexing results, and the finite-certificate interface. Independent verification, clearer reusable statements, and stronger certified bounds are welcome, while preserving totality, global sensitivity, and the unbounded-sensitivity requirement.

Selected references

• Hao Huang, Induced subgraphs of hypercubes and a proof of the Sensitivity Conjecture, Annals of Mathematics 190(3), 949–955, 2019. DOI.
• OpenAI, A superquadratic separation between sensitivity and block sensitivity, OpenAI Math Release preprint, September 2026. Manuscript; formalization scope.
• Robin Kothari and Codex, Separation exponent at least 2.075, Prove2Me accepted proof, 2026. Theorem and proof record.
• abhishekdpseok, Separation exponent at least 2.0635, Prove2Me accepted proof, 2026. Theorem and proof record.
• yousofy with Codex, Separation exponent at least 2.085, Prove2Me accepted proof, 2026. Theorem and proof record.
• yousofy with Codex, Separation exponent at least 2.119 from a periodic profile invariant, Prove2Me accepted proof, 2026. Theorem and verification record.

Motivation

A rule that assigns an output bit to every input string can react very differently to changing one bit and changing several bits together. Quantifying that difference is a basic question about Boolean functions in theoretical computer science. Sensitivity measures how many individual bit changes can affect one output; block sensitivity allows disjoint groups of bits to change separately. The question here is how far apart these two measures can grow.

Hao Huang's 2019 theorem established a polynomial relation between sensitivity and polynomial degree, resolving the Sensitivity Conjecture. The sharper question about the exponent remained. OpenAI's 2026 superquadratic separation ruled out a universal quadratic bound. The subsequent accepted exponent-2.075 contribution by Robin Kothari and Codex provides the established comparison point for this mission. The target is the stronger quantitative bound 2.085.

Setting

A total Boolean function is a map

$$f:\{0,1\}^n\longrightarrow\{0,1\}$$

that assigns an output to every length-$n$ bit string. For an input $x$ and a set $B$ of coordinate positions, write $x^B$ for the string obtained by reversing exactly the bits in $B$.

A coordinate $i$ is sensitive at $x$ when $f(x^{\{i\}})\ne f(x)$. Write $s(f,x)$ for the number of such coordinates and define

$$s(f)=\max_x s(f,x).$$

A sensitive block at $x$ is a nonempty coordinate set $B$ with $f(x^B)\ne f(x)$. Define $bs(f,x)$ as the largest size of a family of pairwise disjoint sensitive blocks at that same input, and set

$$bs(f)=\max_x bs(f,x).$$

Each block is flipped separately from the original input. All functions and coordinate sets in these definitions are finite.

Formalization target

The main theorem is the campaign statement

$$\operatorname{AchievesExponent}(2.085),\qquad 2.085=\frac{417}{200}.$$

Its full meaning is

$$\forall\varepsilon>0\;\forall S\in\mathbb N,\ S\ge2\;\Longrightarrow\; \exists n\in\mathbb N\;\exists f:\{0,1\}^n\to\{0,1\},$$ $$s(f)\ge S\quad\text{and}\quad bs(f)\ge s(f)^{2.085-\varepsilon}.$$

The exact formal target and its proof status are recorded here. Both the dimension and the function may depend on $\varepsilon$ and $S$. The decimal denotes an exact rational number. The statement permits arbitrarily small positive exponent loss and explicitly requires arbitrarily large sensitivity. For example, choosing $\varepsilon=0.001$ gives exponent 2.084 at every requested sensitivity threshold. This is a concrete checkpoint within the broader problem of determining the optimal separation exponent.

Significance and current status

The target raises the established exponent bound from 2.075 to 2.085, with the quantifiers stated above. In particular, it supplies a fixed exponent strictly above 2.075 for a family whose sensitivities are unbounded. This distinction matters: a favorable comparison for one finite Boolean function, without an appropriate asymptotic conclusion, would not establish the target.

The new contribution is an eight-layer numerical certificate within the existing nine-predicate framework. Its foundation comes from Kothari and Codex's accepted 2.075 proof, which retains credit to abhishekdpseok's accepted 2.0635 development and the earlier OpenAI and community proofs.

The complete self-contained proof has compiled successfully in Lean 4.33.1. The certificate and its assembly have also passed independent checks. Prove2Me has accepted the complete proof, submission c6096517-61e7-4f51-bc68-c1521d61eb65, on 20 October 2026. The target record is the reference for subsequent verification status. The separate proof explanation supplies the construction details and exact arithmetic.

Difficulty

The sensitivity estimate must hold at every input. Checking only the input that supports many sensitive blocks leaves that requirement unresolved. Likewise, a collection of output-changing sets is insufficient unless its members are nonempty and pairwise disjoint.

The asymptotic quantifiers impose a further requirement: witnesses must exist beyond every sensitivity threshold. Merely increasing the dimension does not establish this, since a function can ignore added coordinates. Finally, the exact rational exponent requires rigorous arithmetic bounds; a numerical logarithm estimate alone does not prove the formal statement.

Formalization scope

The shared Lean representation uses f : (Fin n → Bool) → Bool and the definitions in SensitivityCampaign and OAI.Paper320. Sensitivity is the finite supremum over all inputs. Block sensitivity takes the finite supremum over all block families at each input, assigning zero to a family that fails the disjointness, nonemptiness, or output-change conditions. The empty family is allowed.

The target imposes no normalization on $f$ or on a distinguished input. Dimensions zero and constant functions are permitted by the underlying types, but cannot satisfy the required sensitivity threshold $S\ge2$. Real exponentiation is applied after casting the natural-number complexity measures to real numbers.

The development uses Mathlib and the unchanged campaign definitions. Reusable infrastructure includes the complexity-measure definitions and the finite-certificate interface. Independent verification, clearer reusable statements, and stronger rigorously certified bounds are welcome contributions. Any stronger target should preserve totality, global sensitivity, and the unbounded-sensitivity requirement.

Selected references

• Hao Huang, Induced subgraphs of hypercubes and a proof of the Sensitivity Conjecture, Annals of Mathematics 190(3), 949–955, 2019. DOI.
• OpenAI, A superquadratic separation between sensitivity and block sensitivity, OpenAI Math Release preprint, September 2026. Manuscript; formalization scope.
• Robin Kothari and Codex, Separation exponent at least 2.075, Prove2Me accepted proof, 2026, submission 819ad4c6-aa25-48ca-82e9-c8df39c182c0. Theorem and proof record.
• abhishekdpseok, Separation exponent at least 2.0635, Prove2Me accepted proof, 2026, submission f80a3f37-72fa-4d56-a094-3e4d351764f3. Theorem and proof record.

Motivation

Building on the ideas in L E Labuschagne, Composition Operators on Non-commutative $L^p$-spaces, \textit{Expo. Math} \textbf{17}(1999), 429--468, we indicate how the concept of a composition operator may be extended to the context of Haagerup $L^p$-spaces.

This mission is the statement-level formalization of Composition Operators on Haagerup $L^p$-spaces (arXiv:math/0603612v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Normal states are epsilon-delta absolutely continuous (Lemma 3.2, 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.

Deferred results

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

• Lemma 3.3: State-preserving classical L-infinity star-algebra realization of an arbitrary abelian von Neumann algebra, including characteristic projections and genuine measure atomlessness. (hard)
• Remark 3.8: Actual modular continuous core, canonical trace and dual density; closed ordinary density products and symmetric Haagerup sandwiches, with finite and infinity exponents. (hard)
• Theorem 4.2: Haagerup Lp spaces and characteristic sandwiches; C(M) generated by the finite-projection span; arbitrary orthogonal strong-net sums and a normal Jordan extension. (hard)
• Lemma 4.3: Modular group constructed from an fns weight, core representation on L2(R,H), restriction to L2(R,eH), and restricted affiliated density. (hard)
• Remark 4.4: Extension by zero along L2(R,eH) into L2(R,H) for affiliated operators and its exact Haagerup Lp image. (hard)
• Lemma 4.5: Nonunital normal Jordan star maps, the normal composed weight, and its canonical support constructed from null projections. (hard)
• Step (I): canonical support reduction: Canonical support of the composed weight, normal Jordan restriction, central corner Haagerup compression, and faithful restricted composed weight. (hard)
• Proposition 4.6: Two weights in a canonically identified continuous core, closed density powers/products, bounded symmetric changes of weights, and their interpolation scale. (hard)
• Theorem 4.8: Actual Haagerup Lp bimodule actions, strong multiplication Lr times Lp into Lq, and bounded complex-linear module maps. (hard)
• Theorem 4.8: left-module counterpart: Actual Haagerup Lp left modules, right multiplication by Lr elements, and the bilinear trace dual pairing. (hard)
• Lemma 4.9: Haagerup quasi-Lp spaces at all positive finite exponents, strong product and trace-defined quasi-norm, with the bounded algebra at r=infinity. (hard)
• Lemma 4.10: Haagerup trace duality adjoint, closed e*h^(1/p), left support of affiliated operators, and a densely defined closed-product map into L1. (hard)
• Lemma 4.11: Measurable affiliated algebras of two continuous cores, canonical Jordan transport, shift generators and possibly nonmeasurable densities, and onto Lp isometries. (hard)
• Step (III): Jordan decomposition and WJ: Constructed two-summand Jordan decomposition, canonical support corners with overlapping supports, independent Lq product norm, and onto sandwich isometry WJ. (hard)
• Proposition 4.12: Actual Haagerup Lp and dense symmetric embedding of m_phi, closed density powers and products, and positive-map weight domination. (hard)
• Lemma 4.13: Nonunital normal Jordan map, generated von Neumann algebra B acting on J(1)H, and restriction of the target weight to B. (hard)
• Remark 4.14: Weight modular action, generated invariant B, constructed weight-preserving normal conditional expectation, and isometric Haagerup inclusion with sandwich compatibility. (hard)
• Lemma 4.15: Modular-invariant nonunital (anti)homomorphic range, support-corner Haagerup spaces, symmetric composition operators and bounded change of weights. (hard)
• Lemma 4.16: Modular group of an arbitrary fns weight, its actual dual density in the continuous core, and spectral commutation with arbitrary bounded d. (hard)
• Lemma 4.17: Canonically identified cores for two weights, their actual dual densities, strong spectral commutation, and the Pedersen-Takesaki commuting-weight condition. (hard)
• Theorem 4.19: All five canonical construction steps for Haagerup composition operators, two-copy weight changes and their scale, nonfaithful commuting weights and Jordan decomposition. (hard)

Selected references

• Composition Operators on Haagerup $L^p$-spaces, arXiv:math/0603612v2, https://arxiv.org/abs/math/0603612v2

Motivation

We explore complementarity between output and environment of a quantum channel (or, more generally, CP map), making an observation that the output purity characteristics for complementary CP maps coincide. Hence, validity of the mutiplicativity/additivity conjecture for a class of CP maps implies its validity for complementary maps. The class of CP maps complementary to entanglement-breaking ones is described and is shown to contain diagonal CP maps as a proper subclass, resulting in new class of CP maps (channels) for which the multiplicativity/additivity holds. Covariant and Gaussian channels are discussed briefly in this context.

This mission is the statement-level formalization of On complementary channels and the additivity problem (arXiv:quant-ph/0509101v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

24 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: complementary transfer of multiplicativity, additivity and superadditivity (Theorem 1: complementary transfer of multiplicativity, additivity and superadditivity, 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

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

• Two-mode attenuation Bogoljubov dilation and its marginals: Complete self-adjoint quadratic two-mode Fock generator, its actual unitary evolution, and both all-trace-class marginal identities. (hard)
• Two-mode amplification Bogoljubov dilation and its marginals: Complete self-adjoint quadratic two-mode Fock generator, its actual unitary evolution, and both all-trace-class marginal identities. (hard)
• Convex mixtures and constrained Holevo-capacity claim: Specified mixture construction, common output identifications/flags, and the constrained-Holevo product-constraint convention for the four listed classes. (source-ambiguity)
• Literal true-complement identification of Gaussian environmental marginal: Purity of the Gaussian environment, or retention of its omitted purifying subsystem in the true complement. (source-ambiguity)

Selected references

• On complementary channels and the additivity problem, arXiv:quant-ph/0509101v3, https://arxiv.org/abs/quant-ph/0509101v3

Motivation

We study the Braunstein-Kimble setup for teleportation of quantum state of a single mode of optical field. We assume that the sender and receiver share a two-mode Gaussian state and we identify optimum local Gaussian operations that maximize the teleportation fidelity. We consider fidelity of teleportation of pure Gaussian states and we also introduce fidelity of the teleportation transformation. We show on an explicit example that in some cases the optimum local operation is not a simple unitary symplectic transformation but some more general completely positive map.

This mission is the statement-level formalization of Improving fidelity of continuous-variable teleportation via local operations (arXiv:quant-ph/0202102v3). 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 Dissipative Gaussian preprocessing strictly beats every Bob symplectic unitary (Abstract; §IV, Fig.1, pp.6–7, 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

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

• §III, paragraph after Eq.(42): A proved unrestricted diagonal-optimality theorem for arbitrary diagonal A,B,C,D. (source-ambiguity)
• §III, claim after Eq.(47): A specified complete analytic diagonal root-search algorithm covering exceptional denominators and filtering squared roots. (source-ambiguity)
• Appendix A, Eqs.(A1)–(A6), continuation p.8: A well-defined renormalized bosonic process score on the accepted full separable state domain, with a fixed momentum-transpose convention, swap trace pairing, and agreement with regular Wigner slices. (hard)

Selected references

• Improving fidelity of continuous-variable teleportation via local operations, arXiv:quant-ph/0202102v3, https://arxiv.org/abs/quant-ph/0202102v3

Motivation

Time-series momentum is the empirical regularity that an asset's recent excess return predicts its future excess return. It has been documented across equity indices, currencies, commodities and bonds (Moskowitz, Ooi & Pedersen 2012), and momentum portfolios are among the most widely traded systematic strategies. Most of that literature builds portfolios from a single signal: the average return over a look-back window. Li and Liu (Operations Research 2022) ask what a long-horizon investor who rebalances should do when expected returns really are driven by such a moving average. Their answer has a structural feature that a Markovian model such as Merton's (Merton 1971) cannot produce. The optimal weight depends on the whole recent price path, not only on the current momentum.

Setting

A risky asset has price $S_t$ and log price $s_t=\ln S_t$, with

$$\frac{dS_t}{S_t} = [\alpha m_t + (1-\alpha)\mu + r]\,dt + \sigma\,dB_t,\qquad m_t = \frac1\tau\int_{t-\tau}^{t}\Big(\frac{dS_u}{S_u} - r\,du\Big),$$

where $B$ is a Brownian motion. Momentum $m_t$ is the equally weighted moving average of excess returns over a look-back window of length $\tau>0$. The parameter $0<\alpha<1$ measures how strongly momentum enters the expected return, $\mu$ is the unconditional risk premium, $r$ is the constant short rate and $\sigma>0$ is the volatility. Because the drift depends on $s_t - s_{t-\tau}$, the price is not Markov: the state at time $t$ is the whole path on $[t-\tau,t]$.

An investor with constant relative risk aversion $\gamma>0$ maximizes expected utility of terminal wealth at a horizon $T$ by trading the asset and a riskless bond. The mission works in the paper's short-horizon regime $0\le T\le\tau$, with the investor standing at time $0$, so the realized path $s$ on $[-\tau,0]$ is known.

The paper's analysis (Appendix A.2) produces the following objects:

• the market price of risk at time $0$, $\theta_0 = [(1-\alpha)\mu - \alpha(r-\sigma^2/2) + \frac\alpha\tau(s_0-s_{-\tau})]/\sigma$;
• functions $A_1, A_2$ on $[0,T]$ that solve a Riccati equation and a linear equation, the system (A.9), with $A_1(T)=A_2(T)=0$ and forcing term $s_{u-\tau}$;
• the optimal weight $\phi^*_0 = \theta_0/(\gamma\sigma) + A_{1,0}s_0 + A_{2,0}$ of (A.11);
• explicit functions $C_0$, $\hat\omega$, the weight $\omega$ on $[-\tau,0]$ and a constant $C_1$, all of (A.14).

The Lean development names them theta0, SolvesA9, phiStar, C0, omegaHat, omega and C1 in the namespace DynMomentum.ShortHorizon.

Formalization targets

Goal: Proposition 3.3

For every solution $(A_1,A_2)$ of (A.9),

$$\phi^*_0 = \underbrace{\frac{\alpha}{\gamma\sigma^2}\int_{-\tau}^{0}\frac1\tau\Big(\frac{dS_v}{S_v}-r\,dv\Big) + \frac{(1-\alpha)\mu}{\gamma\sigma^2}}_{\phi^M_0} + \underbrace{\frac{(1-\gamma)\alpha}{\gamma\sigma^2}\int_{-\tau}^{0}\omega_v\Big(\frac{dS_v}{S_v}-r\,dv\Big) + C_1}_{\phi^H_0}. \tag{3.8}$$

Moreover, $\omega$ is positive on $(-\tau,0]$ when $T>0$, strictly increasing on $[-\tau,T-\tau]$, and constant on $[T-\tau,0]$. The first summand $\phi^M$ is the myopic mean-variance weight; the second, $\phi^H$, is the hedging demand.

Milestones

1. (A.9) solves (A.8). The ansatz $f(x,t)=\exp\{A_{1,t}x^2/2+A_{2,t}x+A_{3,t}\}$ solves the Feynman–Kac PDE (A.8) whenever $(A_1,A_2,A_3)$ solve (A.9).
2. (A.13), $A_1$. The closed form $A_{1,t}=\alpha(\gamma-1)(1-e^{2\alpha(T-t)/(\sqrt\gamma\tau)})/(\gamma\sigma^2\tau D(T,t))$ solves the Riccati equation with $A_{1,T}=0$.
3. (A.13), $A_2$. For any solution $A_1$, the variation-of-constants integral for $A_2$ solves the linear equation with $A_{2,T}=0$.
4. (A.14). $\hat\omega_u>0$ for $u\in[-\tau,-\tau+T]$.
5. Proposition 3.3, last sentence. The positivity and shape of $\omega$, stated on its own.

Significance

The result. Proposition 3.3 shows that a momentum investor who rebalances should not trade on momentum alone. The hedging demand weights past returns unequally, with more weight on recent ones, so two price paths with identical momentum lead to different optimal positions. This is the paper's explanation of why path dependence is intrinsic to optimal momentum trading. It underlies the paper's later comparisons with momentum-only strategies, the horizon extension of Proposition 6.3, and the closed-form expansions of Online Appendix III.

Formalizing it. The proof's analytic half, from (A.9) to (3.8), is summarized in the paper by the phrase "after some manipulations". Writing that step out yields a checked identity between an ODE-defined weight and an explicit integral formula. Doing so has already caught an error. The constant $C_1$ printed in (A.14) is wrong: it differs from the true value by a path-independent amount, and it becomes correct after deleting both occurrences of $-\sigma^2/2$ (a numerical solution of (A.9) agrees with the corrected formula to $10^{-10}$). The proposition is proved in the paper. As far as is known, no part of it has been machine-checked.

Difficulty

Each milestone is a direct calculus statement; the goal is not. The obvious approach is to substitute the closed forms (A.13) into (A.11) and simplify. That leaves $A_{2,0}$ as a double integral of the past path $s$ against two nested exponential kernels written in the ODE's own parameterization, while (3.8) is a single integral of returns $dS/S$ against the weight $\omega$ of (A.14), which is written in a different parameterization. The paper gives no derivation of the match. The path is only continuous, so no step may differentiate $s$. Separately, the Riccati closed form divides by a quantity that vanishes for small $\gamma<1$, so every step has to track where that denominator is positive.

Formalization scope

• What is formalized. Everything from (A.9) to (3.8). The stochastic layer is not formalized: Lemmas 3.1–3.2 (martingale method), the measure change, the Feynman–Kac representation and the volatility matching (A.10)–(A.12) need stochastic integration, Itô's formula and martingale representation, which Mathlib does not have at this revision. Equation (A.11) is therefore taken as the definition of the optimal weight: $\phi^*_0 := \theta_0/(\gamma\sigma) + A_{1,0}s_0 + A_{2,0}$.
• Time. The statement is at $t=0$ with horizon $0\le T\le\tau$ and the path on $[-\tau,0]$, as in Appendix A.2. The model is time-homogeneous, so a general $t$ is a shift.
• ODEs. "Solves (A.9)" means a derivative within $[0,T]$ at every point of $[0,T]$, plus the terminal conditions. At $T=0$ the derivative clause is vacuous; that is the paper's zero-horizon case.
• Admissibility. The hypothesis $D(T,0)=(\sqrt\gamma-1)e^{2\alpha T/(\sqrt\gamma\tau)}+(\sqrt\gamma+1)>0$ is added. It holds automatically for $\gamma\ge1$. Without it, the Riccati solution blows up for small $\gamma<1$ and the goal would be vacuous.
• Pathwise returns. The return integral $\int_{-\tau}^0 w_v(dS_v/S_v - r\,dv)$, for a deterministic absolutely continuous weight $w$ with derivative $w'$, is read as $w_0s_0 - w_{-\tau}s_{-\tau} - \int_{-\tau}^0 w'_vs_v\,dv + (\sigma^2/2-r)\int_{-\tau}^0 w_v\,dv$. This is its value by Itô's formula and the product rule. With $w\equiv1/\tau$ it gives back $m_0$ of (2.3).
• Corrections. $C_1$ is the corrected constant described above. The positivity of $\omega$ is stated on $(-\tau,0]$ under $T>0$, because $\omega_{-\tau}=0$ and $\omega\equiv0$ when $T=0$.
• What a correct formalization rules out. The goal is not obtained by definition. $\phi^*$ is (A.11), never $\phi^M+\phi^H$. The functions $\omega$, $\hat\omega$, $C_0$ and $C_1$ are the explicit formulas of (A.14), never derived from the ODE solution. The goal quantifies over every solution of (A.9), not over the closed forms.
• Infrastructure. The development uses Mathlib's HasDerivWithinAt, interval integrals, Real.exp and Real.sqrt. Two lemmas are reusable well beyond this mission: the closed form of a constant-coefficient scalar Riccati equation, and variation of constants for a scalar linear ODE with merely continuous forcing. Contributions of those lemmas, of uniqueness for (A.9), and of the integration-by-parts step are welcome.

Selected references

• K. Li and J. Liu, Optimal Dynamic Momentum Strategies, Operations Research, 2022. https://doi.org/10.1287/opre.2021.2254
• R. C. Merton, Optimum consumption and portfolio rules in a continuous-time model, Journal of Economic Theory 3(4), 1971. https://doi.org/10.1016/0022-0531(71)90038-X
• T. J. Moskowitz, Y. H. Ooi and L. H. Pedersen, Time series momentum, Journal of Financial Economics 104(2), 2012. https://doi.org/10.1016/j.jfineco.2011.11.003

Motivation

A firm can sell a product outright or charge customers each time they use it. Selling collects one payment and transfers the asset to the customer. Pay-per-use service (PPU) keeps control of the asset, earns revenue from each use, and incurs a delivery or operating cost each time. These arrangements coexist for equipment, vehicles, and other products whose useful life contains many potential uses. A firm choosing between them needs to know how production cost and delivery cost affect the profit it can earn in competition. Ladas, Kavadias, and Loch study that question in a two-stage game and derive a threshold for which business model earns more in an asymmetric duopoly equilibrium.

The threshold is a result about competitive earnings, not just customer preference. A service provider can attract customers who need few uses, while a seller can attract customers who expect to use the product often. Each firm's price changes the boundary between those groups. The mission focuses on the paper's base model and its Proposition 3: the comparison of the seller's and service provider's equilibrium profits. The paper proves the result in its 2021 SSRN manuscript; this mission asks for a machine-checked account of that known result.

Setting

There are two firms. One sells a product for a single price $p_s$ and pays a production cost $c>0$ for each unit sold. The other charges a price $p_u$ per use. Under the paper's strong pooling assumption, one asset supplies its full capacity of $q_m>0$ uses, so the provider allocates production cost over those uses. Its effective cost per use is $c_u=c/q_m+\delta$, where $\delta\ge0$ is delivery cost per use. The willingness to pay for one use is $a>0$. The base model assumes that all customers have this same value but differ in desired lifetime usage $q$, uniformly distributed over $[0,q_m]$ with density $1/q_m$. Sections 2.1–2.3 set out these assumptions.

The customer utilities are $U_s(q;p_s)=qa-p_s$ from buying and $U_u(q;p_u)=q(a-p_u)$ from service. A customer belongs to the seller's segment if buying gives nonnegative utility and at least as much utility as service. A customer belongs to the provider's segment if service gives nonnegative utility and at least as much utility as buying. These conditions define the market segments at every price pair, including prices far from equilibrium. The paper writes both comparisons weakly, so a customer at a tie belongs to both segments. In the relevant equilibria, such ties have zero measure.

The seller's profit is its margin $p_s-c$ times the mass of its segment. The provider's profit is the average over its segment of usage $q$ times margin $p_u-c_u$. Both averages use the uniform density $1/q_m$. Firms first select business models and then set prices simultaneously. This mission fixes the asymmetric subgame with one seller and one service provider. A price equilibrium is a pair at which neither firm can increase its profit by changing its own price; the provider's price is constrained by $p_u\le a$. The comparison is made where the provider is admissible, $c_u\le a$, as the paper specifies before Proposition 3 and when discussing infeasibility in Section 3.2. The model and game timing appear on manuscript pages 7–9.

Formalization targets

Equilibrium profit comparison

Write $\Pi_s(p_s,p_u)$ and $\Pi_u(p_s,p_u)$ for the integral-defined profits at an equilibrium. Proposition 3 gives a production-cost-dependent delivery threshold:

$$\bar\delta(c)= \begin{cases} \dfrac{c}{2q_m}, & c\le\dfrac{aq_m}{3},\\ a-\dfrac{c}{q_m}-2a\left(\dfrac{aq_m-c}{aq_m+c}\right)^2, & c>\dfrac{aq_m}{3}. \end{cases}$$

The goal asserts that an equilibrium exists and that every price equilibrium has the stated comparison:

$$\Pi_s(p_s,p_u)\le\Pi_u(p_s,p_u) \quad\Longleftrightarrow\quad \delta\le\bar\delta(c).$$

For delivery cost above the threshold, the seller's equilibrium profit is strictly larger. The milestone list follows the paper's Appendix A.2.1 profit and equilibrium table and Appendix A.2.4's two threshold regimes. Proposition 3, manuscript page 14 states the comparison.

Significance

The result separates two drivers of the business-model choice. Production cost creates a possible pooling advantage for the provider, because many uses can share one asset's cost. Delivery cost erodes that advantage on every use. The threshold states exactly when the provider's equilibrium earnings exceed the seller's, under the base model's assumptions. It also provides a benchmark for the paper's later analyses of usage uncertainty, heterogeneous valuation, and queueing inefficiencies. Those extensions change the model and are outside this mission. Sections 3–6 develop the base result and its extensions.

The result is already proved in the cited manuscript. The formalization would make explicit the price game, its whole strategy spaces, and the passage from the model's utility-defined market segments to equilibrium profits. It would also establish that the comparison is valid at every equilibrium in the admissible region, including boundary parameter values. No machine-checked proof of this model or Proposition 3 is being reused here; the platform search found related duopoly models with different customers, prices, and cost conventions. The definitions of the segments and profit integrals can be reused for later formalizations of this paper's variants.

Difficulty

The paper computes an indifferent customer's usage and then obtains price candidates from an interior first-order condition and a constrained KKT calculation. Those calculations alone do not establish a global equilibrium: a deviation can put all customers on one side of the indifferent point, leave a firm with no customers, or use a nonpositive price. The profit formulas derived for an interior split do not describe those cases. A formal equilibrium statement must compare each firm with every permitted price, rather than treating the stationary equations as a definition of equilibrium.

The boundary $c=aq_m,\delta=0$ also matters. At that point the seller can have several equilibrium prices with the same zero profits, so uniqueness of prices is too strong. The goal concerns profits at every equilibrium. Appendix A.2.4 switches the algebraic profit comparison according to the provider's price regime, while Proposition 3 switches its threshold formula at $c=aq_m/3$; the two switches have to describe the same profit ordering over the whole admissible region.

Formalization scope

Lean represents $a,q_m,c,\delta,p_s,p_u$, and customer usage $q$ as real numbers. The parameter predicate records $a>0$, $q_m>0$, $c>0$, $\delta\ge0$, and $c/q_m+\delta\le a$. The last condition is the paper's service admissibility condition; it implies $c\le aq_m$. Customer mass is real Lebesgue measure restricted to the utility-defined segment and divided by $q_m$; service profit integrates $q$ over its segment and divides by the same $q_m$. These segments are bounded and measurable, so their measures and integrals have the intended finite values. The threshold and table formulas only use divisions whose denominators are positive under admissibility.

The paper's weak market inequalities are retained, including their treatment of ties. Seller deviations range over all real prices because no duopoly seller-price bound is imposed in the source. Provider deviations range over all prices at most $a$, matching its stated constraint. The equilibrium predicate requires global profit comparisons. The goal asserts existence before saying what holds at every equilibrium, so an empty equilibrium set cannot satisfy it. Profits in the goal are calculated from customer segments and integrals at an equilibrium; they are not defined by the table. The paper's Appendix A.2.1 table provides a separate milestone proving those values, and the global best-response and equilibrium-profit statements are identified as stronger than the printed calculations.

This mission needs Mathlib's real measure, set integral, and real algebra libraries, plus the paper-specific definitions of utility, market segments, profits, equilibrium, the two pricing regimes, and $\bar\delta(c)$. Contributions that establish the closed-form integrals, global best responses, equilibrium table, all-equilibrium profit identity, and regime comparisons are within scope. The earlier monopoly benchmark, the full business-model choice game, and the later heterogeneous, uncertain-usage, and queueing models are separate targets.

Selected references

• K. Ladas, S. Kavadias, and C. Loch, Product Selling vs. Pay-Per-Use Service: A Strategic Analysis of Competing Business Models, authors' SSRN manuscript, 2021, SSRN 3356458; published in Management Science, doi:10.1287/mnsc.2021.4125. This mission cites manuscript pages 7–9, 13–14, 36–37, and 42.

Motivation

Product recalls are frequent and costly. A firm that launches an innovation without thorough quality assurance testing gains time on the market but risks a recall, which brings direct costs (repairs, refunds, legal settlements) and lasting damage to the product's reputation. Testing removes the risk but delays the launch, and while a firm tests, a rival can take the market with its own innovation. Kim, Koenigsberg and Ofek (SSRN 3492105, November 2019; published in Management Science, 2022, doi:10.1287/mnsc.2022.4303) model this trade-off as a two-period game and ask when competing firms test and when they rush to market. Their answer for two identical firms, Proposition 2, is the goal of this mission: depending on the failure probability of an untested product, neither firm tests, both test, or exactly one tests.

Setting

Two firms each hold an innovation. The mature product has quality $V>0$ and the innovation quality $V+B$, with $B>0$. Production costs nothing. There are two periods, $t=1,2$.

Before $t=1$, each firm chooses its testing decision $QA\in\{0,1\}$ simultaneously. A firm that tests ($QA=1$) sells its mature product at $t=1$ and a fail-proof innovation at $t=2$. A firm that does not test ($QA=0$) launches its innovation at $t=1$. The untested innovation fails during that period with probability $\theta\in(0,1)$, independently across firms. On failure the firm pays a recall cost $\Delta=\rho+\delta\,\pi_1$, where $\rho>0$ is a fixed cost, $\delta\in(0,1]$ a penalty per unit of first-period revenue and $\pi_1$ the firm's first-period profit, and at $t=2$ it sells a recalled innovation of quality $(V+B)(1-\gamma)$, with reputation damage $\gamma\in(0,1)$.

In each period a new unit mass of consumers arrives, with tastes $\phi$ uniform on $[0,1]$. A consumer of taste $\phi$ gets utility $\phi\,q-p$ from a product of quality $q$ at price $p$ and buys the product of greatest utility if that utility is nonnegative. Given the two products on offer, the firms set prices; the pricing subgame is the one-period price game, and its equilibrium profit for quality $q$ against $q'$ is written $\pi(q,q')$. The testing game is the simultaneous $2\times2$ game in which a firm choosing $a$ against a rival choosing $b$ earns the expected two-period payoff $\Pi^{a,b}$, and an equilibrium is a pure Nash equilibrium of it.

Formalization targets

Goal: Proposition 2

With the cutoffs of the paper's appendix,

$$\tilde\theta^{st}=\frac{4B(V+B)^2(3+\gamma)^2}{(V+B)\big(4B(V+B)(3+\gamma)^2\delta-(3V+4B)^2(1-\gamma)\gamma\big)+(3V+4B)^2(3+\gamma)^2\rho},$$

and $\tilde\theta^{nt}=[\underline{\tilde\theta}^{nt},\overline{\tilde\theta}^{nt}]$, the interval between the two roots of the quadratic in $\theta$ given by (A.3):

$$\text{no firm tests}\iff\theta\in\tilde\theta^{nt},\qquad \text{both test}\iff\theta\ge\tilde\theta^{st},\qquad \text{exactly one tests}\iff\theta\le\tilde\theta^{st}\ \text{and}\ \theta\notin\tilde\theta^{nt},$$

and the two symmetric equilibria never coexist.

Milestones

1. Lemma 1 (three bullets): the equilibrium prices and profits of the pricing subgame, namely mature product against innovation, innovation against recalled innovation, and Bertrand pricing at equal qualities.
2. The four payoffs $\Pi^{1,1}=0$, $\Pi^{0,1}$, $\Pi^{1,0}$, $\Pi^{0,0}$ in closed form (proof of Proposition 2).
3. (A.3) and (A.4): the best-response conditions $\Pi^{0,0}\ge\Pi^{1,0}\iff\theta\in\tilde\theta^{nt}$ and $\Pi^{1,1}\ge\Pi^{0,1}\iff\theta\ge\tilde\theta^{st}$.
4. (A.5) and the $\tilde\rho^{nt}$ bound: the recall-cost thresholds under which each cutoff lies in $(0,1)$.
5. Corollary 3: a dual-firm-test equilibrium requires $\rho\ge\tilde\rho^{st}$, and $\tilde\rho^{st}>\tilde\rho^{nt}$.

Significance

Proposition 2 is the paper's main result for competition. It shows that competition changes the testing decision in two directions. A rival's early launch makes simultaneous rushing less costly, because identical products earn nothing in the first period and the revenue-based recall penalty then vanishes. Firms also try to differentiate their timing, which produces the asymmetric equilibrium in which one firm tests and the other does not. Comparing the result with the monopoly benchmark (Proposition 1) gives the paper's managerial conclusions: duopolists may skip a test that a monopolist would run (Corollary 2), and both firms test only when the fixed recall cost is large (Corollary 3).

The proofs in the paper are algebraic and partly omitted ("tedious algebra … available from the authors"). A formal development checks every case of the price equilibria, including the global deviations that the first-order conditions do not cover, and the exact boundaries of each equilibrium region. It also settles the boundary behaviour the paper leaves implicit: the regions are disjoint only off their boundaries. No machine-checked proof of any result of this paper is known.

Difficulty

Most of the work is in Lemma 1. The first-order conditions of the price game give the stated prices, but an equilibrium must also survive non-local deviations: the low-quality firm may undercut to take the whole market, and the high-quality firm may price below the region where both firms sell. Demand is piecewise in the prices, with kinks where one firm's market vanishes and a tie-splitting rule at equal qualities, so each best response is a maximization over several branches. The uniqueness half of the Bertrand bullet needs an undercutting argument. The cutoff characterizations then require sign control of a quadratic in $\theta$ whose discriminant can be negative, and of a denominator in $\tilde\theta^{st}$ that is negative for small $\rho$.

Formalization scope

All quantities are real numbers. The parameters are a structure with fields $V,B,\rho,\delta,\gamma,\theta$, and a predicate bundles the standing assumptions $V>0$, $B>0$, $\rho>0$, $0<\delta\le1$, $0<\gamma<1$, $0<\theta<1$. The page writes neither $V>0$ nor $B>0$; both are implicit and are made explicit here.

Demand is the Lebesgue measure of the set of tastes in $[0,1]$ that buy the product, with indifferent consumers counted with weight $\tfrac12$. A price equilibrium allows deviations to every nonnegative price. The period profit $\pi(q,q')$ is revenue at the prices computed in the proof of Lemma 1, $2q(q-q')/(4q-q')$ for the higher quality, $q(q'-q)/(4q'-q)$ for the lower and $0$ for equal qualities. It is computed from demand, so Lemma 1's profit formulas are theorems. The untested firm's objective $(1-\theta\delta)\,p\,d-\theta\rho$ of (A.1) is a positive affine transform of revenue and has the same best responses, so the price game is posed on revenue.

Lemma 1 identifies the unique price equilibrium for each of the two differentiated quality pairs as well as for equal qualities. The payoff $\Pi^{a,b}$ is built from the recall events, each failing independently with probability $\theta$, and from the period profits. Testing decisions are Booleans (true = test). Equilibria of the testing game are pure Nash equilibria with weak best responses, using the published agt_games predicate AGT.IsPureNash.

The cutoffs are written exactly as on p. 37. Every statement that uses $\tilde\theta^{st}$ requires its denominator to be positive, and every statement that uses $\tilde\theta^{nt}$ requires the discriminant to be nonnegative; when these fail, the corresponding region is empty. The paper calls its regions "mutually exclusive", but at the boundaries a symmetric and an asymmetric equilibrium coexist, so the goal asserts exclusivity only between the two symmetric equilibria.

Trivializing formalizations are ruled out. Defining the payoffs by the four closed forms of the paper's proof, or the period profits by Lemma 1's formulas, would make the milestones definitional and the goal pure algebra. Here both are built from consumer choice.

Not in scope: the monopoly benchmark (Proposition 1, Corollary 1), Corollary 2 (proved only in a limit), the comparative statics of Corollary 4, the conditions $B<\tilde B^{nt}$ and $\tilde\gamma^{nt}$ of (A.3), and the extensions of §5. Contributions are welcome on any milestone. Lemma 1's analysis of the vertical-differentiation price game with uniform tastes is reusable for other quality-competition models.

Selected references

• B. Kim, O. Koenigsberg, E. Ofek, I Don’t “Recall”: The Decision to Delay Innovation Launch to Avoid Costly Product Failure, SSRN working paper 3492105, November 2019. https://ssrn.com/abstract=3492105 — published in Management Science, 2022. https://doi.org/10.1287/mnsc.2022.4303
• A. Shaked, J. Sutton, Relaxing Price Competition Through Product Differentiation, Review of Economic Studies 49(1), 1982. https://doi.org/10.2307/2297136
• J. Tirole, The Theory of Industrial Organization, MIT Press, 1988.

Motivation

The Pratt–Arrow risk premium is the basic local measure of risk aversion under expected utility (EU): a decision-maker with a twice differentiable utility $U$ facing a small zero-mean risk $\tilde\varepsilon$ at wealth $w_0$ pays approximately

$$\pi \simeq \frac{\sigma^2}{2}\left(-\frac{U''(w_0)}{U'(w_0)}\right),$$

variance times the index of absolute risk aversion (Pratt 1964; Arrow 1965). It is used throughout portfolio theory, insurance pricing and decision analysis, wherever a risk attitude has to be summarised by one number.

Much of decision theory since the 1980s replaces EU by rank-dependent utility (RDU, Quiggin 1982), which distorts cumulative probabilities by a probability weighting function $h$. Its special case with linear utility is Yaari's dual theory (DT, Yaari 1987). Under these models risk aversion comes from two sources, the curvature of $U$ and the curvature of $h$, and the variance alone no longer measures how much a small risk costs. Eeckhoudt and Laeven (arXiv:1612.03347v2, published in Operations Research, 2022) identify the missing measure: the second dual moment, or maxiance, the expected best of two independent draws of the risk. They show that under DT the local risk premium is proportional to the maxiance, and that under RDU it is the sum of a variance term and a maxiance term.

Setting

A finite lottery lists outcomes $x_1 \le \dots \le x_n$ in increasing order with unconditional probability masses $\pi_1, \dots, \pi_n$. Write $F_i = \pi_1 + \dots + \pi_i$ and $F_0 = 0$. The masses need not sum to one: the risks below are attached to one branch of a lottery and carry only that branch's mass. An RDU decision-maker with utility $U$ and weighting function $h$ evaluates a lottery by (4.1):

$$\int U(x)\,\mathrm dh(F(x)) = \sum_{i=1}^n U(x_i)\bigl(h(F_i) - h(F_{i-1})\bigr).$$

DT is the case $U(x) = x$ (3.1). The paper assumes that $U$ is twice continuously differentiable with $U' > 0$, and that $h : [0,1] \to [0,1]$ is twice continuously differentiable with $h(0) = 0$, $h(1) = 1$, $h' > 0$.

For a risk with cumulative distribution $F$ and mean $m = \int x\,\mathrm dF(x)$, the unconditional variance and maxiance are

$$m_2 = \int (x - m)^2\,\mathrm dF(x), \qquad \bar m_2 = \int (x - m)\,\mathrm d(F(x))^2,$$

and $\Pr$ denotes the total unconditional mass. For a probability distribution, $\bar m_2 = \mathbb E[\max(\tilde\varepsilon^{(1)}, \tilde\varepsilon^{(2)})] - \mathbb E[\tilde\varepsilon]$ (2.1).

Fix $0 < p_0 < 1$, $0 < \varepsilon_1 < \min\{p_0, 1 - p_0\}$, $\varepsilon_2 > 0$ and initial wealth $w_0$. Lottery $C$ pays $w_0 - \varepsilon_2$ with probability $p_0$ and $w_0 + \varepsilon_2$ with probability $1 - p_0$. Lottery $D$ takes mass $\varepsilon_1$ from each branch of $C$ and puts the released mass $2\varepsilon_1$ on a middle outcome $w_0 + y$ with $-\varepsilon_2 < y < \varepsilon_2$. The RDU risk premium is $\lambda = 0 - y$ for the $y$ that makes the decision-maker indifferent between $C$ and $D$, that is, the solution of (4.2). The spread from $D$ with $y = 0$ to $C$ attaches to the middle branch the risk $\tilde\varepsilon_{12}$, which takes the values $\pm\varepsilon_2$ each with unconditional probability $\varepsilon_1$. The DT construction with lotteries $A$, $B$, outcomes $\pm1$, premium $\rho$ and risk $\tilde\varepsilon_1$ ($\pm1$ with probability $\varepsilon_1$ each) is the same with $\varepsilon_2 = 1$ and $U(x) = x$.

Formalization targets

Goal: the RDU risk premium, (4.3)

As $(\varepsilon_1, \varepsilon_2) \to (0^+, 0^+)$ jointly, with $m_2$, $\bar m_2$, $\Pr$ the moments of $\tilde\varepsilon_{12}$,

$$\lambda = \frac{m_2}{2\Pr}\left(-\frac{U''(w_0)}{U'(w_0)}\right) + \frac{\bar m_2}{2\Pr}\left(-\frac{h''(p_0)}{h'(p_0)}\right) + o\!\left(\frac{m_2}{\Pr} + \frac{\bar m_2}{\Pr}\right).$$

Milestones

1. The moments of $\tilde\varepsilon_1$: $\bar m_2 = 2\varepsilon_1^2$, $\Pr = 2\varepsilon_1$ (§3, p. 6).
2. The moments of $\tilde\varepsilon_{12}$: $m_2 = 2\varepsilon_1\varepsilon_2^2$, $\bar m_2 = 2\varepsilon_1^2\varepsilon_2$, $\Pr = 2\varepsilon_1$ (footnote 21).
3. DT indifference between $A$ and $B$ is equation (3.2).
4. The explicit DT premium (3.3): $\rho = \dfrac{(h(p_0) - h(p_0 - \varepsilon_1)) - (h(p_0 + \varepsilon_1) - h(p_0))}{h(p_0 + \varepsilon_1) - h(p_0 - \varepsilon_1)}$.
5. The DT approximation (3.4): $\rho = \dfrac{\bar m_2}{2\Pr}\left(-\dfrac{h''(p_0)}{h'(p_0)}\right) + o\!\left(\dfrac{\bar m_2}{\Pr}\right)$ as $\varepsilon_1 \to 0^+$.
6. RDU indifference between $C$ and $D$ is equation (4.2), and it has exactly one solution $\lambda$ with $-\varepsilon_2 < \lambda < \varepsilon_2$.

Significance

The result. Formula (4.3) shows that, for a small zero-mean risk, an RDU decision-maker's premium splits additively into an EU part (variance times utility risk aversion $-U''/U'$) and a DT part (maxiance times probability-weighting risk aversion $-h''/h'$). Variance and maxiance appear on an equal footing, so the maxiance is the natural second risk measure for non-EU preferences, as the variance is for EU. The DT index $-h''(p_0)/h'(p_0)$ plays the role of the Arrow–Pratt coefficient in the probability plane. The paper builds its global comparative risk aversion result (Proposition 5.1), its examples with Prelec's weighting function and its portfolio application on this local index.

Formalizing it. The result is proved in the paper by Taylor expansion, with "$\simeq$" left informal. This mission fixes the precise asymptotic meaning: a little-o remainder in the joint limit. It also makes definite the claims the paper takes for granted: that the premium exists and is unique, and that the moments of $\tilde\varepsilon_1$ and $\tilde\varepsilon_{12}$ take the stated values. No part of this development, nor any rank-dependent utility evaluation, is formalized on the platform or, as far as is known, elsewhere.

Difficulty

The obvious argument expands both sides of (4.2) and keeps "the second-order terms". This needs care on two counts. First, the premium is defined only implicitly, so its size has to be controlled before $U(w_0 - \lambda)$ is expanded: the $\lambda^2$ term is negligible only once $\lambda = O(\varepsilon_2^2 + \varepsilon_1\varepsilon_2)$ is known. Second, the two leading terms have different orders, $\varepsilon_2^2$ and $\varepsilon_1\varepsilon_2$, and the remainder must be uniformly small relative to their sum in a two-parameter limit. The tempting reading "small variance and small maxiance" (p. 4) with $\varepsilon_1$ fixed is false: at fixed $\varepsilon_1$ the dual term carries a relative error of order $\varepsilon_1$ that does not vanish as $\varepsilon_2 \to 0$. The DT step (3.4) needs the explicit solution (3.3) and the strict positivity of $h(p_0 + \varepsilon_1) - h(p_0 - \varepsilon_1)$.

Formalization scope

All quantities are real. A lottery is a pair of vectors indexed by $\mathrm{Fin}\,n$; the evaluation (4.1) is the finite rank-dependent sum, with cumulative masses computed from the vector. The sum equals the Stieltjes integral only for outcomes in increasing order, so the premium predicates keep the page's ranges $-1 < x < 1$ and $-\varepsilon_2 < y < \varepsilon_2$, which order $B$ and $D$. Initial wealth $w_0$ is added to every outcome.

Committed conventions:

• $U$ is $C^2$ on $\mathbb R$ with $U' > 0$ everywhere (footnote 1). $h$ is $C^2$ on $[0,1]$, maps $[0,1]$ into itself, satisfies $h(0) = 0$, $h(1) = 1$, and has positive one-sided derivative within $[0,1]$ (p. 5, footnote 12). These are the page's hypotheses, kept although local differentiability at $w_0$ and $p_0$ would suffice.
• $U''(w_0)$, $h'(p_0)$, $h''(p_0)$ are ordinary iterated derivatives; $p_0$ is interior.
• Pinned reading of "$\simeq$". (4.3) is a little-o statement along the filter of $(0,0)$ restricted to $(0,\infty)^2$, relative to $m_2/\Pr + \bar m_2/\Pr$; (3.4) is the one-variable analogue as $\varepsilon_1 \to 0^+$, relative to $\bar m_2/\Pr$.
• The premium is any function of $(\varepsilon_1, \varepsilon_2)$ satisfying the indifference on the feasible region; milestone 6 shows it exists and is unique.
• The moments $m_2$, $\bar m_2$, $\Pr$ in the goal are computed from $\tilde\varepsilon_{12}$ by the definitions, not written as $2\varepsilon_1\varepsilon_2^2$, $2\varepsilon_1^2\varepsilon_2$, $2\varepsilon_1$. $\Pr = 2\varepsilon_1 > 0$ on the filter, so no division by zero enters.

A formalization that defined the premium by its Taylor polynomial, replaced $\lambda$ by the leading terms, or took the limit in $\varepsilon_2$ alone would be trivial or false; the goal quantifies over every solution of the indifference and uses the joint limit.

Not formalized: the equivalence of (2.1) with the Stieltjes form, Proposition 5.1 (global comparative risk aversion), the examples of §6, the portfolio application of §7 and the non-binary generalisation of Appendix A.

Needed infrastructure: finite rank-dependent sums, Taylor expansion of $C^2$ functions with little-o remainders (Mathlib's taylor_mean_remainder family and Asymptotics), and the intermediate value theorem. Contributions welcome: proofs of the milestones, and a general Stieltjes-integral version of (4.1) for finitely supported distributions that would let later missions treat non-binary risks.

Selected references

• L. R. Eeckhoudt, R. J. A. Laeven, Dual Moments and Risk Attitudes, arXiv:1612.03347v2, 2018 (the version formalized here; later published in Operations Research, 2022). https://arxiv.org/abs/1612.03347v2
• J. W. Pratt, Risk Aversion in the Small and in the Large, Econometrica 32, 1964. https://doi.org/10.2307/1913738
• J. Quiggin, A Theory of Anticipated Utility, Journal of Economic Behavior & Organization 3, 1982. https://doi.org/10.1016/0167-2681(82)90008-7
• M. E. Yaari, The Dual Theory of Choice under Risk, Econometrica 55, 1987. https://doi.org/10.2307/1911158
• K. J. Arrow, Aspects of the Theory of Risk-Bearing, Yrjö Jahnssonin Säätiö, Helsinki, 1965.