Motivation

Video-game consoles, streaming services, ride-hailing apps and payment systems are sold in markets where the value of a product grows with the number of people who use it. In the classical analysis of such markets every consumer buys exactly one of the competing products (singlehoming). Under that assumption, a stronger network effect intensifies price competition in Hotelling models of incompatible products, so equilibrium prices fall (Farrell and Saloner, 1992; Shy, 2001); Katz and Shapiro (1985) find the same under Cournot competition. In practice many consumers own both a PlayStation and an Xbox, or subscribe to several streaming services (multihoming).

Foros, Kind and Stähler (Management Science, 2025; SNF Working Paper 16/21, 2021) let consumers choose endogenously whether to buy one good or both. Their Proposition 1 shows that the classical conclusion reverses once some consumers multihome: near the point without network effects, a stronger network effect raises each firm's demand, price and profit, even when the firms differ in size. This mission formalizes that proposition together with the computations on which the paper rests it.

Setting

Two firms $i\in\{0,1\}$ are located at the ends of a Hotelling line of unit length, along which a unit mass of consumers is uniformly distributed. A consumer at distance $d$ from firm $i$ pays a mismatch cost $td$, with $t>0$. Good $i$ has exclusive features worth $e_i$ and shared features worth $o$; buying good $i$ also yields a network benefit $\mu z_i$, where $\mu\ge0$ is the strength of the network effect and $z_i$ is the expected number of buyers of good $i$. Throughout, $\mu<t$ (Assumption 1 (i) of the paper), and $j$ denotes the rival of $i$.

When some consumers buy both goods and expectations are fulfilled ($z_i=x_i$), the paper derives the demand for good $i$ at prices $(p_i,p_j)$:

$$x_i^M(p_i,p_j)=\frac{\mu}{t+\mu}+t\,\frac{e_i-p_i}{t^2-\mu^2}-\mu\,\frac{e_j-p_j}{t^2-\mu^2}. \qquad (14)$$

Maximizing the profit $p_i x_i^M(p_i,p_j)$ (marginal costs are zero) gives the reaction function

$$p_i^M(p_j)=\frac{t\mu-\mu^2+te_i}{2t}+\mu\,\frac{p_j-e_j}{2t}, \qquad (15)$$

and solving the two reaction functions gives the candidate prices

$$p_i^M=\frac{t-\mu}{2t-\mu}(\mu+e_i)+\frac{\mu t}{4t^2-\mu^2}(e_i-e_j). \qquad (16)$$

At these prices the output of good $i$ is $x_i=x_i^M(p_i^M,p_j^M)$, the number of singlehomers of good $i$ (consumers who buy only $i$) is $s_i=1-x_j$, the number of multihomers is $m=1-s_0-s_1$, and firm $i$'s profit is $\pi_i=p_i^Mx_i$. All of these are functions of $\mu$ for fixed $t,e_0,e_1$. In Lean they are demandM, reactM, priceM, outM, singleM, multiM and profitM in the namespace Multihoming.Local, each taking its parameters in the order $(t,\mu,e_i,e_j)$.

Partial multihoming means that some consumers buy both goods and some buy only one of each: $m>0$, $s_0>0$, $s_1>0$. At $\mu=0$ this is exactly $e_0<2t$, $e_1<2t$ and $2t<e_0+e_1$.

Formalization targets

Goal: Proposition 1

Assume $t>0$ and $e_0<2t$, $e_1<2t$, $2t<e_0+e_1$. Then there is $\delta\in(0,t)$ such that, for each $i\in\{0,1\}$,

$$x_i,\ p_i^M,\ \pi_i \text{ are strictly increasing and } s_i \text{ is strictly decreasing in } \mu \text{ on } [0,\delta].$$

The goal fixes no constant and no size of the neighbourhood: it asserts the direction of every effect near $\mu=0$, for asymmetric firms.

Milestones

1. (15) The reaction function maximizes $p\,x_i^M(p,p_j)$ over all real $p$, for $0\le\mu<t$.
2. (16) The candidate prices solve the two reaction functions simultaneously.
3. (19)–(20) Closed forms of $s_i$, $m$ and $x_i$ at the candidate prices.
4. (22) $\dfrac{\partial m}{\partial\mu}\Big|_{\mu=0}=\dfrac{(2t-e_0)+(2t-e_1)}{4t^2}>0$ and $\dfrac{\partial s_i}{\partial\mu}\Big|_{\mu=0}=-\dfrac{2t-e_i}{4t^2}<0$.
5. Footnote 15 $\dfrac{d\pi_i}{d\mu}\Big|_{\mu=0}=\dfrac{(2t-e_j)e_i}{4t^2}>0$.

Significance

The result separates two regimes that the classical theory does not distinguish. Under singlehoming, network effects are a force for competition and lower prices; under partial multihoming, a small network effect makes prices strategic complements (each firm's reaction function slopes upward in the rival's price) and raises the prices, outputs and profits of both firms. This is the paper's explanation for why firms facing multihoming consumers may welcome network effects, and it is the starting point of the paper's later analysis of symmetric firms, of the thresholds on exclusive content, and of mergers.

The proposition is proved in the paper by a short computation: differentiating closed forms at $\mu=0$. To our knowledge none of it has been machine-checked. A formal proof would confirm the closed forms (16), (19), (20), the derivative signs (22) and footnote 15, and would upgrade the paper's derivative-at-a-point argument to monotonicity on an explicit interval. The formalization also records a printed slip: the second constant of (22) is printed as $2t^2$, while the value implied by (16) and (17) is $4t^2$. The sign, and so Proposition 1, is unaffected.

Difficulty

Each identity is a rational-function computation with up to quartic denominators, which is tedious but routine once the denominators are known to be nonzero. The substantive step is from a derivative at one point to monotonicity on an interval. The paper computes one-sided derivatives at $\mu=0$. To conclude strict monotonicity on $[0,\delta]$, one needs the derivatives to keep their sign on a neighbourhood, which requires continuity of the derivative of each of eight functions (four quantities for each of two firms) and a common $\delta$. The price claim has no printed derivative at all. A further subtlety is that the profit derivative at $0$ is positive only because $e_i>0$, which is not a hypothesis but follows from $e_i>2t-e_j>0$.

Formalization scope

• Representation. All parameters are real numbers. The overlapping features $o$ cancel from every object and are not a parameter. The model's demand is (14) with fulfilled expectations, taken as given: its derivation from the consumer's choice problem (10)–(13), the single-homing regime and the full pricing game (regime switching, deviations) are not formalized. The prices are those of (16), the profit is $p_i^M x_i$ as in (5) with zero marginal costs, and milestones (15)–(16) tie the prices to profit maximization.
• Standing assumptions. $t>0$; $0\le\mu<t$ (the model's $\mu\ge0$ and Assumption 1 (i)). Assumption 1 (ii)–(iii), which concern market coverage and positive shares in the full game, are not used and not assumed. Milestones 4–5 need only $t>0$: their functions are smooth near $\mu=0$, and the derivatives are two-sided.
• Pinned hypotheses. "Assume partial multihoming" is the three inequalities $e_0<2t$, $e_1<2t$, $2t<e_0+e_1$. The paper's text names only one condition $2t-e_i>0$; both firms' conditions are needed. "In the neighborhood of $\mu=0$" is strict monotonicity on $[0,\delta]$ with $0<\delta<t$.
• Trivializations ruled out. The goal is about (14) evaluated at (16), not about the closed form (20); $\delta>0$ excludes a vacuous interval; the statement is monotonicity on an interval, not a derivative sign at one point; and every denominator is positive on the domain, so no claim holds through Lean's convention $x/0=0$.
• Not posed. Proposition 4 of the paper, the characterization of the Nash equilibria, is not posed by this series because it is false as printed (a profitable deviation exists at some parameters the proposition covers). Expression (21), which mixes partial derivatives at fixed and at equilibrium prices, is not posed either.
• Infrastructure. Only Mathlib's real analysis is needed (HasDerivAt, StrictMonoOn). Lemmas turning a positive continuous derivative on an interval into strict monotonicity are reusable. Proofs of the milestones and of the goal are welcome, as are proofs that derive the goal from the milestones.

Selected references

• Ø. Foros, H. J. Kind and F. Stähler, Endogenous multihoming and network effects: PlayStation, Xbox, or both?, Management Science, 2025. https://doi.org/10.1287/mnsc.2022.00613 (read from SNF Working Paper No. 16/21, NHH Bergen, December 2021).
• J. Farrell and G. Saloner, Converters, compatibility, and the control of interfaces, Journal of Industrial Economics 40(1), 1992. https://doi.org/10.2307/2950625
• O. Shy, The Economics of Network Industries, Cambridge University Press, 2001. https://doi.org/10.1017/CBO9780511754401
• M. L. Katz and C. Shapiro, Network externalities, competition, and compatibility, American Economic Review 75(3), 1985. https://www.jstor.org/stable/1814809
• B.-C. Kim and D. Serfes, A duopoly model with consumers' multiple-purchase behavior, International Journal of Industrial Organization 24(6), 2006. https://doi.org/10.1016/j.ijindorg.2005.10.008
• S. P. Anderson, Ø. Foros and H. J. Kind, Product functionality, competition, and multipurchasing, International Economic Review 58(1), 2017. https://doi.org/10.1111/iere.12212

Motivation

Online platforms run controlled experiments in which subjects (users, sessions, sellers) arrive one at a time and must be assigned to control or treatment on arrival, before later subjects are seen. A good design makes the two groups look alike in their observed covariates, because covariate imbalance inflates the variance of treatment-effect estimates. Classical offline remedies such as matched-pair designs need all covariates in advance, and the simplest online design, complete randomization, ignores covariates altogether.

Zhao and Zhou (arXiv:2201.12936, Management Science 2025) measure imbalance by the cost of the best one-to-one matching between the treated and the control subjects, which links sequential experimental design to online matching. They propose the pigeonhole design: partition the covariate space into cells and, inside each cell, assign each arrival to the group that is currently short there. This mission formalizes their main upper bound for one continuous covariate.

Setting

A horizon $T$, assumed even, of subjects arrives sequentially. Subject $t$ carries a covariate $x_t\in[0,1]$, and the whole sequence $x=(x_1,\dots,x_T)$ is fixed in advance by an adversary who does not see the randomization (an oblivious adversary). Each subject is assigned, at arrival and irrevocably, to the control group $A$ or the treated group $B$, and in the end $|A|=|B|=T/2$.

The discrepancy of a split is the cost of a minimum-weight perfect matching between the two groups (display (1) of the paper):

$$d_{A,B}=\min_{e:A\to B\ \text{bijective}}\ \sum_{a\in A}|x_a-x_{e(a)}| .$$

The completely randomized design chooses $A$ uniformly among the $\binom{T}{T/2}$ subsets of size $T/2$; its expected discrepancy is written $\mathrm{ALG}^{\mathsf C}(x)$.

A pigeonhole design takes a partition of $[0,1]$ into cells. When subject $t$ arrives: (1) if one group already holds $T/2$ subjects, $t$ joins the other; (2) otherwise, if the cell of $x_t$ currently holds fewer control than treated subjects, $t$ joins control, if fewer treated, $t$ joins treatment, and on a tie a fair coin decides. Its expected discrepancy is the average of $d_{A,B}$ over the coins.

The uniform pigeonholes with parameter $\eta\in(0,1)$ are the $T^{\eta}$ cells $[0,T^{-\eta}),[T^{-\eta},2T^{-\eta}),\dots,[1-T^{-\eta},1]$.

Formalization targets

Goal: Lemma 3

For every fixed $\eta\in(0,1)$ there are $C>0$ and $T_0$ such that, for every even $T\ge T_0$ and every $x\in[0,1]^T$, the pigeonhole design with uniform pigeonholes satisfies

$$\mathbb E\bigl[d_{A,B}\bigr]\ \le\ C\Bigl(T^{\frac12-\frac\eta2}+T^{\frac\eta2}(\log T)^{\frac12}\Bigr).$$

The constant may depend on $\eta$ but on nothing else. Corollary 1, the case $\eta=1/2$ giving $O(T^{1/4}(\log T)^{1/2})$, is included as a separate statement.

Milestones

In attack order:

1. Hoeffding's inequality for a binomial with deviation $\sqrt{n\log n}$ (Lemma EC.1).
2. The value of $\mathrm{ALG}^{\mathsf C}$ on the two-point instance $(0,\dots,0,1,\dots,1)$ (Lemma EC.4, with corrected constant).
3. Permutation invariance of the completely randomized design (Lemma EC.5).
4. $\mathrm{ALG}^{\mathsf C}$ is $\Theta(T^{1/2})$ in the worst case (Lemma 2).
5. Every run of a pigeonhole design is balanced (remark after Definition 3).
6. A median-crossing swap does not decrease the single-cell design's expected discrepancy (Lemma EC.7, corrected).
7. The single-cell design has expected discrepancy $O(T^{1/2})$ (Proposition EC.1).
8. At the stopping time $\tau$, each cell has at most one unmatched subject and $|H^0_\tau-H^1_\tau|=T-\tau$.
9. The subjects matched inside cells contribute $O(T^{1/2-\eta/2})$ (Component 1).
10. The unmatched subjects and the last $T-\tau$ subjects contribute $O(T^{\eta/2}(\log T)^{1/2})$ (Component 2).

Significance

Lemma 3 shows that a simple, time-invariant, covariate-aware online rule beats complete randomization by a polynomial factor: with $\eta=1/2$ the expected discrepancy is $O(T^{1/4}(\log T)^{1/2})$, against $\Theta(T^{1/2})$ for complete randomization (Lemma 2). A companion result of the paper (Lemma 4) shows that no pigeonhole design does better than $\Omega(T^{1/4})$, so the bound is tight up to the logarithm. The same two-component argument underlies the paper's multi-dimensional result.

The paper proves these statements in an e-companion; none is machine-checked. A formalization adds the following. It fixes the exact model behind each expectation, namely an average over coin vectors with the balancing rule included. It repairs the places where the printed argument does not close as written. The printed constant of Lemma EC.4 is wrong, and the stated value here is the corrected one. Lemma EC.7 is false as printed in its strict form and trivial in its weak form, and the stated version is the one the proof actually establishes. The printed proof of Lemma 2 passes through a lemma (EC.6) that is false. Component 2 relies on a conditional binomial law that does not hold literally. A complete development would certify Lemma 3 independently of these slips.

Difficulty

The natural first idea is to bound each cell separately and add the results. This handles subjects that are paired inside their own cell, but it leaves out the balancing rule. Once one group is full, every later subject is forced into the other group regardless of its covariate. These forced subjects can be far from everything they are matched to. The number of forced subjects, $T-\tau$, equals the imbalance among the cells' leftover subjects, which is random and read at a random time. Bounding its expectation requires a concentration argument that is uniform over time.

A second difficulty is the per-cell bound itself. Inside one cell the design pairs consecutive arrivals with random orientation, but the number of pairs in a cell is random and depends on the stopping time. A bound of the form $c\,\ell\sqrt n$ for a cell of length $\ell$ holding $n$ subjects must therefore survive a coin-dependent truncation. Finally, the discrepancy is a minimum over matchings, so every upper bound must exhibit a matching, and every comparison between instances (Lemma EC.7) is an exchange argument over all coin outcomes.

Formalization scope

All statements live in the namespace PigeonholeDesign.Upper, and the conventions are fixed as follows:

• Time and assignments. Subjects are indexed by Fin T, from $0$, so the paper's subject $t$ is index $t-1$, and its odd index $i$ is an even 0-based position. An assignment is Fin T → Bool, with true meaning treated.
• Discrepancy. The minimum over bijections between the two groups of the summed distances, which equals the assignment problem (1). When the groups differ in size this infimum is Lean's junk value $0$. The balance milestone shows that the designs never produce such a split.
• Randomness. The pigeonhole design is run on a coin vector in $\{0,1\}^T$, and coin $t$ is read only when subject $t$ meets a tie. Every expectation is the average over all $2^T$ coin vectors (respectively over all $\binom{T}{T/2}$ control sets), never one run or the best run.
• Partition. The printed partition has $T^{\eta}$ cells, which is not an integer in general. It is pinned as $K=\lceil T^{\eta}\rceil$ equal cells of length $1/K\le T^{-\eta}$, with the last cell closed. This coincides with the printed one when $T^\eta$ is an integer.
• Asymptotics. "$O(f(T))$" means that there exist $C>0$ and $T_0$, chosen before $T$ and $x$, depending only on $\eta$ (an absolute $C$ where the page says "absolute constant"). "$\Theta$" means both bounds. The logarithm is natural.
• Corrected statements. Lemma EC.4 uses $1/\sqrt{2\pi}$ in place of the printed $1/\sqrt\pi$. Lemma EC.7 is the non-strict inequality for the specific swap of positions $i+1$ and $j+1$. Component 2 states only its conclusion. Lemma EC.6 is not posed.

Several formalizations would make the statements easy for the wrong reason, and the statements rule them out. The junk value $0$ of an unbalanced split never applies, because the designs are balanced. A bound on a single run, or on the best run, in place of the average over all coin vectors is not the claim. Constants may not depend on $T$ or $x$. The partition is fixed, and the statements do not range over arbitrary partitions.

A complete development needs:

• finite combinatorics of the design run;
• one-dimensional matching (on the line the sorted matching is optimal);
• binomial and hypergeometric tail and mean-absolute-deviation estimates;
• a central-binomial asymptotic for Lemma EC.4.

The design definitions and the balance lemma are reusable by the paper's lower-bound and multi-dimensional missions. Contributions of any milestone, of alternative proofs that bypass the faulty printed steps, and of sharper constants are welcome.

Selected references

• J. Zhao and Z. Zhou, Pigeonhole Design: Balancing Sequential Experiments from an Online Matching Perspective, arXiv:2201.12936v6 (2024); Management Science (2025). https://arxiv.org/abs/2201.12936
• W. Hoeffding, Probability inequalities for sums of bounded random variables, Journal of the American Statistical Association 58 (1963) 13–30. https://doi.org/10.1080/01621459.1963.10500830
• C. R. Blyth, Expected absolute error of the usual estimator of the binomial parameter, The American Statistician 34 (1980) 155–157. https://doi.org/10.1080/00031305.1980.10483022
• D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific (1997), Chapter 7.8 (assignment problem).

Motivation

Short selling is never free. To sell a share short, an investor borrows it from a holder and pays that holder a lending fee, and the size of these fees has been documented empirically for decades (D'Avolio 2002; Duffie, Gârleanu and Pedersen 2002). Most equilibrium models of asset pricing either forbid short sales or take the fee as exogenous. Evgeniou, Hugonnier and Prieto build a continuous-time general-equilibrium economy where the fee is determined jointly with prices: investors disagree about expected dividend growth, the pessimist wants to short, the optimist owns the shares, and the cost of shorting clears the securities lending market. The paper uses the model to explain how a positive shorting cost can coexist with apparent mispricing, as in the 3Com/Palm spin-off.

In the special case of a single risky asset (the market portfolio), the equilibrium reduces to a pair of algebraic equations for the shorting cost and the lending yield at each state, and the paper solves them in closed form (Proposition 3). This mission formalizes that closed form and its comparative statics in the belief gap.

Setting

At a fixed state of the economy, three numbers describe the environment:

• $\sigma>0$, the volatility of aggregate consumption, which in the one-asset case is also the volatility of the risky asset;
• $\delta=\sigma\Delta=\mu^{(o)}-\mu^{(p)}\ge 0$, the unscaled difference in beliefs: the gap between the expected dividend growth rates perceived by the optimist $o$ and the pessimist $p$ ($\Delta$ is the same gap per unit of volatility);
• $s\in(0,1)$, the consumption share of the optimist.

Short selling is active only when the optimist holds a large enough share of consumption, namely on the shorting region $s>s^*$, where

$$s^*=\min\Big\{1,\frac{\sigma}{\Delta}\Big\}=\min\Big\{1,\frac{\sigma^2}{\delta}\Big\}.$$

Two unknowns are determined in equilibrium: the shorting cost $\Phi$, the flow rate a short seller pays per unit of position, and the lending yield $\Gamma$, the flow rate a lender receives per unit of shares held. The paper shows (p. 27) that with one risky asset they satisfy

$$\Phi=\mathbb 1_{\{s>s^*\}}\frac{(\delta+\Gamma)s-\sigma^2}{1+s},\qquad \Gamma=\mathbb 1_{\{s>s^*\}}\frac{(1-s)(s\delta-\Gamma-\sigma^2)\big((\delta+\Gamma)s-\sigma^2\big)}{\sigma^2(1+s)^2}. \tag{29–30}$$

The proof of Proposition 3 works with the per-volatility yield $\gamma=\Gamma/\sigma$ and the quadratic

$$g(\gamma)=(1-s)(s\Delta-\gamma-\sigma)\big((\gamma+\Delta)s-\sigma\big)-\gamma\sigma(1+s)^2 .$$

In Lean these objects are costOne σ δ s, yieldOne σ δ s, IsOneAssetSystem σ δ s Φ Γ and gQuad σ Δ s γ, all in the namespace CostlyShort.OneAsset.

Formalization targets

Goal: Proposition 3

For $\sigma>0$ and $s\in(0,1)$: for every $\delta\ge 0$ and every $\Gamma\ge 0$, the pair $(\Phi,\Gamma)$ solves (29)–(30) if and only if

$$\Phi=\mathbb 1_{\{s>s^*\}}\frac{s(1-s)\delta-2\sigma^2+\sqrt{s^2(1-s)^2\delta^2+4\sigma^4 s}}{2(1-s)}, \tag{31}$$ $$\Gamma=\mathbb 1_{\{s>s^*\}}\frac{-s\big((1-s)^2\delta+4\sigma^2\big)+(1+s)\sqrt{s^2(1-s)^2\delta^2+4\sigma^4 s}}{2s(1-s)}, \tag{32}$$

and both (31) and (32), as functions of $\delta$, are non-decreasing and convex on $[0,\infty)$ and strictly increasing for $\delta>\sigma^2/s$.

Milestones

1. On the shorting region, (30) is equivalent to $g(\gamma)=0$ (proof of Proposition 3, p. 50).
2. $g(0)=(1-s)(s\Delta-\sigma)^2>0$, $g'(0)<0$, $g''\equiv-2s(1-s)<0$ and $g(\gamma)\to-\infty$ (p. 50).
3. For $s>s^*$, $g$ has a unique strictly positive root (p. 50).
4. The closed form (32) is strictly positive and solves (30) on the region (p. 50).
5. Substituting (32) into (29) gives (31) (p. 50).
6. The market-clearing identity (33) with the utilization (34): $\Gamma=\Phi\Upsilon/(1+\Upsilon)$, $\Upsilon=\frac{1-s}{\sigma^2}\Phi$ (p. 28).
7. $\Phi$ is non-decreasing and convex in $\delta$ on $[0,\infty)$, strictly increasing on the region (Proposition 3, p. 28).

A companion statement, not a milestone, formalizes the limits on p. 29: as $s\uparrow 1$, $\Phi\to(1-s^*)\delta/2$ and $\Gamma\to 0$.

Significance

Proposition 3 is the only fully explicit equilibrium of the paper. It gives the level of the shorting cost and of the lending yield as functions of disagreement and of the wealth distribution, and its monotonicity in $\delta$ is the model's prediction that short interest and lending fees rise with the dispersion of beliefs, which the paper checks against analysts' forecast dispersion (Table 1). Convexity says the effect accelerates with disagreement. The two-asset case of §4.2 has no closed form and is solved numerically; the one-asset formulas are its benchmark.

The result is proved in the paper, but the proof of the comparative statics is omitted ("We omit the details", p. 50), and the selection of the positive root is asserted ("it is clear"). A formal development supplies the omitted differentiation argument, including convexity across the kink at the boundary $\delta=\sigma^2/s$ of the shorting region, and checks the paper's algebra. No part of this paper has a machine-checked proof.

Difficulty

The algebra of milestones 1, 4 and 5 is mechanical but involves a square root and several divisions, whose signs must be tracked throughout. The substantive step is the comparative statics. Monotonicity and convexity of $\Phi$ in $\delta$ need the derivative of a square-root expression on the open region, and then a separate argument at the kink: both functions vanish identically for $\delta\le\sigma^2/s$, so convexity on $[0,\infty)$ requires the one-sided derivative at $\sigma^2/s$ to be non-negative, which is a computation rather than a consequence of convexity on each piece. For $\Gamma$ the paper's route is indirect: $\Gamma=h(\Phi)$ with $h(x)=cx^2/(1+cx)$, and composition of a non-decreasing convex $h$ with a non-decreasing convex $\Phi$. Differentiating (32) directly is possible but heavier.

Formalization scope

Everything is pointwise in real numbers. The continuous-time economy of §2 (Brownian dividends, portfolio choice, the derivation of (29)–(30) from the equilibrium conditions (16), (20), (21)) is the paper's motivation and is not formalized; Proposition 3 is stated relative to (29)–(30), which is exactly where the paper's proof begins. Conventions committed to:

• standing assumptions $\sigma>0$ and $0<s<1$ in every theorem; the endpoints $s\in\{0,1\}$ are absorbing states where (31)–(32) divide by zero, and are excluded;
• the indicator $\mathbb 1_{\{s>s^*\}}$ is encoded as $\sigma^2<s\delta$, equivalent for $\sigma>0$, $\delta\ge 0$, $s\in(0,1)$; it is never written as $s>\min\{1,\sigma/\Delta\}$, where Lean's $\sigma/0=0$ would make every state a shorting state when $\Delta=0$;
• in the goal's equivalence the lending yield is restricted to $\Gamma\ge 0$. This is a disclosed pin: on the shorting region the quadratic also has a negative root, which solves (29)–(30) as well; the paper's proof selects "the unique strictly positive solution", and a lending yield is a non-negative flow rate;
• "increasing" is stated as non-decreasing on $[0,\infty)$ plus strictly increasing on $(\sigma^2/s,\infty)$, because both functions are zero below the region;
• the paper prints $g''=-s(1-s)$; the correct second derivative $-2s(1-s)$ is stated (milestone 2);
• only the outer equality of (34) is used; its middle expression involves the pessimist's portfolio and needs the economy.

A trivializing formalization is ruled out: stating only that (31)–(32) satisfy (29)–(30), or convexity only on the open shorting region, would be strictly weaker than the paper and is not the goal.

Needed infrastructure is Mathlib's real analysis: Real.sqrt, deriv, MonotoneOn, ConvexOn, and convexity of compositions. Proofs of any milestone are welcome independently. Facts about convexity of a function that vanishes up to a point and is convex beyond it are reusable outside this mission.

Selected references

• T. Evgeniou, J. Hugonnier and R. Prieto, Asset Pricing with Costly Short Sales, Swiss Finance Institute Research Paper N°22-21, version of September 22, 2022 (the source of this mission; §3.3, §4.1, App. A). Published as J. Hugonnier and R. Prieto, Management Science, 2024. https://doi.org/10.1287/mnsc.2023.01887
• G. D'Avolio, The market for borrowing stock, Journal of Financial Economics 66 (2002) 271–306. https://doi.org/10.1016/S0304-405X(02)00206-4
• D. Duffie, N. Gârleanu and L. H. Pedersen, Securities lending, shorting, and pricing, Journal of Financial Economics 66 (2002) 307–339. https://doi.org/10.1016/S0304-405X(02)00226-X
• J. Detemple and S. Murthy, Equilibrium asset prices and no-arbitrage with portfolio constraints, Review of Financial Studies 10 (1997) 1133–1174. https://doi.org/10.1093/rfs/10.4.1133

Complete Life Assurances, Lump Sums and Insurance–Annuity Identities

Motivation

A life assurance pays a contingent lump sum under a policy-defined event, rather than a sequence of survivor-contingent instalments. A benefit paid at the end of the policy year of death has a different value from one paid immediately on death. A pure endowment pays instead when the insured survives to maturity, while an endowment assurance combines cover for death before maturity with a maturity payment to survivors. For these products, the event partition, contractual recipient and payment instant must be explicit before an expected present value is calculated.

Promislow (2015, Chapter 5, sections 5.1–5.8) derives a general annual insurance–annuity relationship from benefit vectors. Dickson, Hardy and Waters (2020, Chapter 4) develops the corresponding conventional life insurance factors. The mission makes the death, survival and maturity events visible as actual random cashflows, then derives the classical identities without taking the desired identities as assumptions.

Setting

Let the lifetime-state variable $K$ take values $0,\ldots,h$. For $j<h$, state $K=j$ represents death during the policy year whose start is anniversary $j$ and whose end is anniversary $j+1$. State $K=h$ represents survival at the model's right-censoring anniversary. Nonnegative probabilities $p_j$ satisfy $\sum_{j=0}^{h}p_j=1$. The anniversary survival probability is $S(j)=\sum_{k=j}^{h}p_k$, for $0\le j\le h$. The annual discount factor $v$ satisfies $0<v\le1$, and all values are expressed at policy commencement, time zero.

For an amount schedule $b_j$ in money per death claim, the random present value of a death benefit payable at the end of the death year is

$$Z(K)=\sum_{j=0}^{h-1}v^{j+1}b_j\mathbf{1}_{\{K=j\}}.$$

A temporary assurance of duration $n$ includes deaths in policy years $0,\ldots,n-1$. A deferred term assurance adds a waiting period $a$ and covers deaths in years $a,\ldots,a+n-1$. A pure endowment is triggered by $K\ge n$ and pays at time $n$. The term and maturity components are disjoint for $0\le n\le h$. The specific settlement recipient can be identified contractually; if recipient survival or eligibility changes the payment event, that condition requires an additional model variable.

Formalization targets

Realised insurance values

The foundational result is a reconciliation between the expectation of the realised random present value $Z$ and a separate valuation made from the probability of death in each covered policy year. For a unit sum assured, both routes must produce an actuarial value from exactly the same state law. The analogous pure-endowment reconciliation averages realised survivor payments and independently discounts the survival tail.

Maturity-event partition and annuity identity

The next result establishes the endowment decomposition from disjoint actual payment events, including the zero-term boundary and a terminal survivor who must not receive a fictitious death claim. The year-end-of-death benefit and the maturity benefit are valued separately. Their combination is then reconciled with a survival-contingent annuity paid in advance at anniversaries $0,\ldots,n-1$.

Writing $d=1-v$ for the annual effective discount rate, the central finite relationship for unit death and maturity benefits is

$$A_n^{1}+v^nS(n)+d\ddot a_n=1, \qquad \ddot a_n=\sum_{j=0}^{n-1}v^jS(j).$$

Here $A_n^{1}$ includes deaths before maturity and settlement at the following policy-year end. The maturity mass $v^nS(n)$ captures those alive at $n$. The formula is derived by telescoping discounted survival decrements. When the horizon is right-censored, a whole-horizon death-only assurance omits terminal survivors and requires a residual term. A familiar whole-life identity without that term needs certain death by the terminal horizon or an expressly defined terminal benefit.

Variable benefits and moments

The source also defines arithmetic increasing and decreasing insured amounts, geometric escalation and minimum-benefit floors. It constructs the second moment of the actual claim present value by squaring its realised value and compares it to a separate squared-benefit death-mass sum. Distinct death years are mutually exclusive, so mixed claim terms vanish. A variance is meaningful only with a normalised, nonnegative probability law. Additional families cover insurance-term extensions, the split of a deferred term, exact commutation recursions and benefit or discount ordering.

The principal capstone starts with a single finite lifetime law and one annual discount basis. It simultaneously derives the death-claim expectation, the pure-endowment expectation, the disjoint endowment decomposition, the finite insurance–annuity conservation identity and the independent second-moment formula. The conservation equation is the substantive conclusion rather than a restated hypothesis. Each item remains an open theorem statement until a valid Prove2Me proof is separately accepted.

Continuous and fractional-time valuation

The additional model uses an actual real future lifetime T with a specified probability measure μ supported on nonnegative times. It does not infer a continuous death-time distribution from annual mortality probabilities. At nonnegative maturity n, death in 0≤T<n triggers an immediately paid claim. Death at T=n instead belongs to the pure-endowment event T≥n, even if the probability law has an atom there.

At constant force of interest δ, put U=min(T,n). A continuously paid unit annuity has realised present value Y=(1−exp(−δU))/δ when δ≠0, and Y=U when δ=0. An immediate death benefit or maturity benefit pays exp(−δU) under exactly one of the two events. Therefore its pathwise conservation law is

$$\exp(-\delta U)+\delta Y=1.$$

Taking expectations under the same μ produces the distinct continuous insurance–annuity identity

$$\overline A_n^1+\exp(-\delta n)\Pr(T\ge n)+\delta\overline a_n=1.$$

Fractional-time results specify m>0 annual instalment periods, each ending at (r+1)/m. A death in [r/m,(r+1)/m) is payable at the following subperiod end, without ambiguity at exact grid instants. At nonnegative force, immediate payment is at least as valuable as m-thly payment, which is at least as valuable as year-end payment. Supporting results cover cashflow moments, settlement lag, escalation and UDD-versus-constant-force survival. The annual–continuous bridge equates year-end claim values under matched policy-year death masses.

Significance

This event-level basis, grounded in the insurance benefit conventions of Dickson, Hardy and Waters (2020, Chapter 4), supports analyses of death-in-service benefits, death-in-deferment cover, pension-scheme lump sums, term life protection and survival maturity benefits. It also makes transparent why the expected value of a lump-sum death claim can be represented using an annuity schedule only after the schedules and discounting are related mathematically. The annuity correspondence reflects an exact payment-mass identity, and a denominator used for recurring premiums needs strict positivity before division.

These reusable cashflow models can support future dependent-beneficiary and pension-scheme guarantees, but true survivor entitlement requires an additional joint-life state.

Difficulty

Careful classification at anniversaries is essential. In the annual model, a death allocated to the policy year following maturity cannot generate both the pre-maturity death benefit and the maturity benefit. Terminal censoring distinguishes survival observed at the end of a finite table from guaranteed eventual death. The conservation identity should remain valid at zero interest and zero term; when no covered deaths occur, its insurance component must vanish. Later death-year payments also make valuation sensitive to the chosen discount factor.

Death-claim second moments require exclusive event indicators, not independence. The capstones derive values from cashflows rather than commutation-table definitions. These constraints exclude vacuous premises and cosmetic equalities.

Formalization scope

The private formal development contains two distinct models: a finite annual right-censored K-model with discount factor v and an actual real-lifetime T-model with exponential discounting at force δ. The annual root remains the main theorem, while the continuous insurance–annuity result is a separate supporting capstone. Targeted Mathlib imports encode a probability measure, real claim instants, fractional settlement and cashflow moments.

The classical actuarial identities are already established in the literature. The Draft contains 119 open theorem statements, including seven explicitly formulated reusable root-support lemmas, with no accepted mission proofs. Pinned-revision private Lean checks have verified 85 distinct theorem statements, including the complete 12-conjunct finite annual root, distribution-level insurance–annuity conservation and the annual–continuous settlement bridge. These are private compiler diagnostics, not accepted proofs of published mission targets.

Annual discount d=1−v differs from continuous force δ. The fractional branch models UDD and finite constant-force survival and bridges half-year survival to the payment grid. General-duration inequalities, death-time density valuation, select tables, dependent-survivor eligibility and infinite-horizon convergence remain open. A time-dependent recipient multiplier does not establish joint-life entitlement.

Selected references

• David C. M. Dickson, Mary R. Hardy and Howard R. Waters (2020), Actuarial Mathematics for Life Contingent Risks, third edition, Chapter 4, Cambridge University Press. https://doi.org/10.1017/9781108784184
• S. David Promislow (2015), Fundamentals of Actuarial Mathematics, third edition, Chapters 5 and 7, and Chapter 8, section 8.8, Wiley, ISBN 9781118782460. https://www.wiley.com/en-us/Fundamentals+of+Actuarial+Mathematics%2C+3rd+Edition-p-9781118782521

Motivation

Flatly Foliated Relativity (FFR) is a theory of gravity introduced by Bray, Hamm, Hirsch, Wheeler and Zhang (arXiv:1911.00967, 2019) that sits between special and general relativity. It keeps the Einstein–Hilbert action of general relativity (GR) but restricts it to spacetimes that are foliated by flat Euclidean spaces (Assumption 1 of the paper): "matter curves spacetime, but not space". The authors motivate this by the observed spatial flatness of the local universe. Since gravitational waves are excluded, FFR is proposed as an approximation of GR whose metric equations are much more tractable. It still contains the big bang (FLRW spacetimes with $k = 0$), accelerated expansion and the exterior Schwarzschild spacetime.

One headline feature of the theory is how a positive cosmological constant $\Lambda > 0$ (Assumption 2) shapes it. For $\Lambda>0$ the paper shows that the FFR metric equations are elliptic on every slice, that the mean curvature of the foliation gives a geometric arrow of time, and that there is exactly one vacuum solution among solutions that are spherically symmetric at infinity. For $\Lambda=0$ uniqueness fails, and for $\Lambda<0$ existence fails. This mission formalizes Sections 3.2–5 of the paper, which contain these statements.

Setting

All FFR equations live on a single flat slice $\mathbb R^3_t$, with no time derivatives, so the formalization works on $\mathbb R^3$ with coordinates $x_1,x_2,x_3$. The spacetime metric is

$$g = (-\eta^2+|\omega|^2)\,dt^2-(\omega\otimes dt+dt\otimes\omega)+\delta_{\mathbb R^3},$$

where $\eta>0$ is the lapse and $\omega$ is a one-form on $\mathbb R^3$, identified with a vector field through the flat metric. Matter enters through the energy density $\mu$ and the momentum density $J$. Writing $\omega_{i,j}=\partial_j\omega_i$, $\nabla\cdot\omega=\omega_{i,i}$ and $\Delta$ for the flat Laplacian (summation over repeated indices), the FFR equations (34)–(35) are

$$2\Lambda+16\pi\mu=\frac1{\eta^2}\Big[(\nabla\cdot\omega)^2-\tfrac14\|\omega_{i,j}+\omega_{j,i}\|^2\Big],$$ $$16\pi J_i=\frac1\eta\big(\Delta\omega_i-\partial_i(\nabla\cdot\omega)\big)+\frac2{\eta^2}(\nabla\cdot\omega)\eta_i-\frac1{\eta^2}(\omega_{i,j}+\omega_{j,i})\eta_j .$$

Substituting $\omega=df+\zeta$ with $\nabla\cdot\zeta=0$ gives the elliptic form (39)–(41), with unknowns $(f,\zeta,\eta)$. Here $Q_{ij}=f_{ij}+\tfrac12(\zeta_{i,j}+\zeta_{j,i})$:

$$(\Delta f)^2-\|Q\|^2=(16\pi\mu+2\Lambda)\eta^2,$$ $$\Delta\zeta_i=16\pi J_i\eta-\tfrac2\eta(\Delta f\,\delta_{ij}-Q_{ij})\eta_j,$$ $$(\Delta f\,\delta_{ij}-Q_{ij})\eta_{ij}=8\pi\nabla\cdot(J\eta^2),$$

together with the requirement $\nabla\cdot\zeta\to0$ at infinity. Vacuum means $\mu=0$ and $J=0$. When $\Lambda>0$, the paper fixes the time orientation by the arrow-of-time convention $K=(\nabla\cdot\omega)/\eta=\Delta f/\eta>0$ (Convention 1). A pair $(\omega,\eta)$ is spherically symmetric at infinity if it is spherically symmetric on $\{r\ge r_0\}$ for some $r_0>0$. Two vacuum solutions count as the same if they differ by an overall positive constant factor, which corresponds to rescaling $t$.

Formalization targets

Goal: Corollary 2

For $\Lambda>0$, the pair $\omega=\sqrt{\Lambda/3}\,r\,\partial_r$, $\eta=1$ is a smooth vacuum solution that is spherically symmetric at infinity. Every smooth vacuum solution with $\eta>0$ and $(\nabla\cdot\omega)/\eta>0$ that is spherically symmetric at infinity has the form

$$\eta\equiv c,\qquad \omega=c\sqrt{\Lambda/3}\;x\qquad(c>0).$$

Milestones

Theorem 2 (equivalence with the elliptic form), Theorem 3 (arrow of time), Theorem 4 (ellipticity inequality), Lemma 1 (symmetrization), identity (82)–(83), Theorem 5 (uniqueness for the elliptic form under approximate spherical symmetry), Lemma 2 ($\Lambda=0$: many vacua) and Lemma 3 ($\Lambda<0$: no vacuum).

Significance

Corollary 2 is the fourth claim of the paper's main result (Theorem 1). It is the precise sense in which FFR with $\Lambda>0$ is rigid, in contrast to GR, which has many vacuum solutions that are spherically symmetric at infinity (gravitational waves). Together with Lemmas 2 and 3, it singles out the sign of $\Lambda$ as the parameter that controls existence and uniqueness. The intermediate results are of independent use. Theorem 2 lets the elliptic system replace the original one, Theorem 4 is the ellipticity statement behind the existence question posed in the paper (Question 1), and Lemma 1 is a symmetrization inequality for the $2$-Hessian operator $\sigma_2(\nabla^2 f)$.

These are paper proofs. No machine-checked version of any of them is known to the proposer. The mission asks for a complete formal proof of the goal and the milestones in Lean 4 with Mathlib.

Difficulty

The algebra is elementary. The difficulty is analytic. The uniqueness arguments rest on maximum principles for the elliptic equations (41) and (45) on all of $\mathbb R^3$ under conditions at infinity, on Liouville-type arguments for harmonic functions, and on a Newtonian-potential representation (convolution with the Green's function of $\Delta$) used to show $\zeta\to0$. Lemma 1 needs averaging over rotations (spherical symmetrization), Jensen's inequality and a characterization of its equality case. Theorem 5 then needs a divergence-theorem argument on large balls that is controlled only by the approximate symmetry hypothesis. Mathlib provides the divergence theorem on boxes and some harmonic-function theory, but no ready-made maximum principle for second-order elliptic operators with variable coefficients on $\mathbb R^n$.

Formalization scope

• Space is EuclideanSpace ℝ (Fin 3). One-forms $\omega,\zeta,J$ are vector fields $\mathbb R^3\to\mathbb R^3$, and the paper's $\omega$ is written w in Lean. Partial derivatives are fderiv applied to the standard basis vectors. Because fderiv returns $0$ at non-differentiable points, every statement assumes smoothness (ContDiff ℝ ∞) of all fields, as the paper does.
• "Spherically symmetric" means invariance (for scalars) or equivariance (for one-forms) under all linear isometries of $\mathbb R^3$. Because $SO(3)$ acts transitively on spheres, this is equivalent to rotational symmetry.
• The spherical symmetrization $\bar f(x)$ is the average of $f$ over the sphere of radius $|x|$, taken with respect to the surface measure volume.toSphere. "Approximately spherically symmetric at $\infty$" is read as: $f-\bar f$ is bounded and $r^2\,\|\nabla^2(f-\bar f)\|\,\|\nabla(f-\bar f)\|\to0$ uniformly as $r\to\infty$, using operator norms.
• The arrow-of-time convention $\Delta f/\eta>0$ (respectively $(\nabla\cdot\omega)/\eta>0$) is an explicit hypothesis wherever the paper invokes it. Without it, $f\mapsto-f$ (time reversal) produces a second solution.
• Existence parts are stated with explicit witnesses. A formalization that drops smoothness, $\eta>0$ or the convention would be trivial or false, and is not acceptable.
• Contributions such as maximum principles, Liouville theorems and spherical averaging in $\mathbb R^n$ are reusable well beyond this mission and are welcome as separate lemmas.

Selected references

• H. L. Bray, B. Hamm, S. Hirsch, J. Wheeler, Y. Zhang, Flatly Foliated Relativity, arXiv:1911.00967v2, 2019. https://arxiv.org/abs/1911.00967
• L. Caffarelli, L. Nirenberg, J. Spruck, The Dirichlet problem for nonlinear second order elliptic equations, III: Functions of the eigenvalues of the Hessian, Acta Mathematica 155 (1985), 261–301 (cited in the paper for the existence theory of the $J=0$ case).
• J. Corvino, R. M. Schoen, On the asymptotics for the vacuum Einstein constraint equations, Journal of Differential Geometry 73(2) (2006), 185–217 (cited in the paper for the comparison with GR).

Motivation

Mass–energy equivalence is the relationship between mass and energy in a system's rest frame: the two differ only by the constant factor $c^2$, the square of the speed of light,

$$E = mc^2 .$$

It was proposed as a general principle by Albert Einstein in 1905 ("Does the inertia of a body depend upon its energy-content?") as a consequence of special relativity, and it underlies nuclear and particle physics: the mass defect of a nucleus measures its binding energy, and the energy released in fission or annihilation is accounted for by the change in rest mass.

Timeline. Electromagnetic-mass relations of the form $m \propto E_{em}/c^2$ were considered in the late 1800s and by Poincaré (1900) and Hasenöhrl (1904). Einstein (1905) derived the relativistic kinetic energy $E_k = mc^2(\gamma-1)$ and stated that a body emitting energy $L$ as radiation loses mass $L/c^2$. Planck, Stark, Lewis–Tolman and Lorentz (1907–1914) rewrote the relation in its modern forms, and von Laue (1911) gave a proof from the stress–energy tensor. This mission follows the Wikipedia article Mass–energy equivalence.

Setting

Velocities and momenta are vectors in $\mathbb R^3$ with Euclidean norm $|\cdot|$. Fix a speed of light $c>0$. A body of rest mass $m\ge0$ moving with velocity $\mathbf v$, $|\mathbf v|<c$, has

• Lorentz factor $\gamma = 1/\sqrt{1-|\mathbf v|^2/c^2}$,
• relativistic energy $E_{\mathrm{rel}} = \gamma mc^2$ and relativistic momentum $\mathbf p = \gamma m\mathbf v$,
• rest energy $E_0 = mc^2$, kinetic energy $E_k = E_{\mathrm{rel}} - mc^2$, and relativistic mass $m_{\mathrm{rel}} = E_{\mathrm{rel}}/c^2$.

For a finite system of free particles $i\in s$ the invariant mass is $M = c^{-2}\sqrt{(\sum_i E_i)^2 - c^2|\sum_i\mathbf p_i|^2}$, the total energy over $c^2$ in the centre-of-momentum frame (zero total momentum). A Lorentz boost with speed $|u|<c$ along the first axis sends $(E,\mathbf p)$ to $E' = \gamma_u(E-up_1)$, $\mathbf p' = (\gamma_u(p_1 - uE/c^2), p_2, p_3)$.

Formalization targets

Goal: energy–momentum relation

$$E_{\mathrm{rel}}^2 - |\mathbf p|^2c^2 = m_0^2c^4 \qquad (c>0,\ m_0\ge 0,\ |\mathbf v|<c).$$

It contains $E=mc^2$ as the case $\mathbf p = 0$.

Milestones

1. $E = mc^2$ in the rest frame ($\mathbf v = 0 \Rightarrow \mathbf p = 0,\ E = mc^2$).
2. $E_{\mathrm{rel}} = \sqrt{(m_0c^2)^2 + (pc)^2}$.
3. Massless particles: $E^2-(pc)^2 = 0$, $E,p\ge0 \Rightarrow E = pc$.
4. Relativistic mass: $m_0 \le m_{\mathrm{rel}} = m_0 + E_k/c^2$, with equality iff $\mathbf v = 0$ (for $m_0>0$).
5. Power series $E = m_0c^2\sum_n \binom{2n}{n}4^{-n}(v/c)^{2n} = m_0c^2[1+\tfrac12(v/c)^2+\tfrac38(v/c)^4+\tfrac5{16}(v/c)^6+\cdots]$.
6. Correspondence principle: $E_k = \tfrac12 m_0v^2 + O(v^4)$ as $\mathbf v\to0$.
7. Third-order approximation: $E = m_0c^2 + \tfrac12 m_0v^2(1+\tfrac{3v^2}{4c^2}) + O(v^6)$.
8. Parker Solar Probe: $\tfrac{3v^2}{4c^2}\approx 3.9\times10^{-8}$ for $v = 68\,600$ m/s.
9. $c^2 = 89\,875\,517\,873\,681\,764$ J/kg.
10. Boost invariance of $E^2 - c^2|\mathbf p|^2$: rest mass is the same in all inertial frames.
11. Zero total momentum $\Rightarrow M = \sum_i E_i/c^2$.
12. Non-additivity: $\sum_i m_i \le M$, with equality iff all constituents share one velocity.

Significance

The energy–momentum relation is the kinematic identity behind relativistic energy bookkeeping: rest energy, kinetic energy, invariant-mass reconstruction and the frame independence of rest mass all follow from it. The low-speed expansion makes precise in what sense Newtonian mechanics is the $v\ll c$ limit of relativity. The composite-system statements formalize why, in relativity, mass is neither additive nor separately conserved while energy and momentum are conserved.

All results are classical and established in the physics literature. The mission produces machine-checked versions of these kinematic facts in a reusable $\mathbb R^3$-vector setting with an explicit speed of light.

Difficulty

Most single-particle statements are algebraic once the square roots are controlled; the work lies in handling the square-root and division conventions of a total formal language. The power-series milestone requires the binomial series of $(1-x)^{-1/2}$, and the asymptotic milestones require Taylor-type bounds near $\mathbf v = 0$. The non-additivity milestone is a reverse triangle inequality for future-pointing timelike four-vectors, including its equality case, which does not reduce to a one-line computation.

Formalization scope

Lean uses EuclideanSpace ℝ (Fin 3) for $\mathbb R^3$, with explicit $c$ (no natural units). All definitions are total functions: $\sqrt{x}=0$ for $x<0$ and $x/0 = 0$, so every theorem assumes $c>0$ and $|\mathbf v|<c$; rest masses are assumed non-negative. Massless particles cannot be described by velocity-based quantities ($\gamma$ is undefined at $|\mathbf v| = c$), so milestone 3 is phrased directly in terms of an energy–momentum pair. Only boosts along the first axis are formalized. Systems are finite and free (no interaction potential). Historical derivations (Einstein 1905, Rohrlich 1990) and the nuclear-physics applications are not formalized.

Selected references

• A. Einstein, Ist die Trägheit eines Körpers von seinem Energieinhalt abhängig?, Annalen der Physik 18 (1905) 639–641. https://doi.org/10.1002/andp.19053231314
• A. Einstein, Zur Elektrodynamik bewegter Körper, Annalen der Physik 17 (1905) 891–921. https://doi.org/10.1002/andp.19053221004
• Wikipedia, Mass–energy equivalence. https://en.wikipedia.org/wiki/Mass%E2%80%93energy_equivalence

Motivation

Robust control repeatedly meets linear matrix inequalities that must hold for every value of an unknown, norm-bounded matrix. A typical instance is

$$C + EFG + G^\top F^\top E^\top < 0 \quad\text{for all } F \text{ with } F^\top F \leqslant \bar F,$$

where $F$ collects model uncertainty or noise. Such a condition quantifies over infinitely many matrices and cannot be checked directly. Petersen's lemma (Petersen and Hollot, Automatica 1986; Petersen, Systems & Control Letters 1987) replaces it by a single inequality in one scalar multiplier $\lambda>0$. The lemma is a standard tool in the design of quadratically stabilizing controllers for uncertain systems, and it was recently used for controller design from noisy data (Bisoffi, De Persis and Tesi, arXiv:2109.12175).

H. J. van Waarde, M. K. Camlibel, J. Eising and H. L. Trentelman (arXiv:2203.12959v3, 2023; SIAM J. Control Optim.) develop a theory of quadratic matrix inequalities (QMIs) and prove matrix versions of the S-lemma. In §4.5.3 they show that both the strict and the non-strict Petersen lemma follow from their matrix S-lemmas (Theorems 4.10 and 4.7) by a suitable choice of the two quadratic forms. This mission formalizes that derivation.

Timeline. Petersen and Hollot (1986) and Petersen (1987) state the lemma for stabilization of uncertain linear systems. Bisoffi, De Persis and Tesi (arXiv 2021) use strict and non-strict versions for data-driven stabilization. van Waarde, Camlibel, Eising and Trentelman (2023, Proposition 4.16) recover both versions from matrix S-lemmas.

Setting

All matrices are real. For a symmetric matrix $A$, $A \geqslant 0$ ($A>0$) means positive semidefinite (definite), and $A \leqslant B$ means $B-A\geqslant0$; the notation includes symmetry. $A^\dagger$ is the Moore–Penrose pseudo-inverse and $\bar F^{1/2}$ the positive semidefinite square root of $\bar F\geqslant0$.

Quadratic matrix inequalities. A symmetric $\Pi \in \mathbb S^{q+r}$ is partitioned into blocks $\Pi_{11}$ ($q\times q$), $\Pi_{12}$, $\Pi_{21}$, $\Pi_{22}$ ($r\times r$). Its solution sets are

$$\mathcal Z_r(\Pi)=\Big\{Z\in\mathbb R^{r\times q}: \begin{bmatrix}I_q\\ Z\end{bmatrix}^\top \Pi \begin{bmatrix}I_q\\ Z\end{bmatrix}\geqslant 0\Big\},$$

and $\mathcal Z_r^+(\Pi)$ is defined in the same way with $>0$. The generalized Schur complement is $\Pi\,|\,\Pi_{22}=\Pi_{11}-\Pi_{12}\Pi_{22}^\dagger\Pi_{21}$, and the class $\boldsymbol\Pi_{q,r}$ consists of the $\Pi$ with $\Pi_{22}\leqslant0$, $\Pi\,|\,\Pi_{22}\geqslant0$ and $\ker\Pi_{22}\subseteq\ker\Pi_{12}$.

Petersen's data. Fix $C\in\mathbb R^{n\times n}$ symmetric, $E\in\mathbb R^{n\times p}$, $\bar F\in\mathbb R^{q\times q}$ with $\bar F\geqslant0$, and $G\in\mathbb R^{q\times n}$. The uncertainty set is $\mathcal F=\{F\in\mathbb R^{p\times q}: F^\top F\leqslant\bar F\}$. Display (4.17) defines

$$M=\begin{bmatrix}-C&-E\\-E^\top&0\end{bmatrix},\qquad N=\begin{bmatrix}G^\top\bar FG&0\\0&-I\end{bmatrix}.$$

In this proposition the letters $q,r$ of the QMI section become $n,p$, so $\mathcal Z_p(N)\subseteq\mathbb R^{p\times n}$.

Formalization targets

Goal: Proposition 4.16 (Petersen's lemma)

(a) The robust strict inequality holds if and only if a single multiplier exists:

$$\big(\forall F\in\mathcal F:\ C+EFG+G^\top F^\top E^\top<0\big)\iff \exists\,\lambda>0:\ C+\lambda EE^\top+\lambda^{-1}G^\top\bar FG<0.$$

(b) If $E\neq0$, $\bar F>0$ and $G\neq0$, the same equivalence holds with $\leqslant 0$ in place of $<0$ on both sides.

Milestones

1. Lemma A.1 (p. 26): $A^\top A\leqslant B^\top B$ if and only if $A=SB$ for some contraction $S$ ($S^\top S\leqslant I$); the strict version under full column rank of $B$; and $S=AB^\dagger$ is such a factor.
2. Set identity (p. 17): $\{FG: F\in\mathcal F\}=\{S\bar F^{1/2}G: S^\top S\leqslant I\}=\{H: H^\top H\leqslant G^\top\bar FG\}$.
3. Reformulation (4.17) (p. 17): the strict robust inequality is $\mathcal Z_p(N)\subseteq\mathcal Z_p^+(M)$, the non-strict one is $\mathcal Z_p(N)\subseteq\mathcal Z_p(M)$, and $N\in\boldsymbol\Pi_{n,p}$ with $N_{22}<0$.
4. Theorem 4.10 (strict matrix S-lemma, p. 13): for $N\in\boldsymbol\Pi_{q,r}$ with $N_{22}<0$, $\mathcal Z_r(N)\subseteq\mathcal Z_r^+(M)$ iff $M-\alpha N>0$ for some $\alpha\geqslant0$.
5. Theorem 4.7 (matrix S-lemma, p. 12): for $N\in\boldsymbol\Pi_{q,r}$ with a positive eigenvalue, $\mathcal Z_r(N)\subseteq\mathcal Z_r(M)$ iff $M-\alpha N\geqslant0$ for some $\alpha\geqslant0$.
6. Schur-complement step (p. 17): for $\alpha>0$, $M-\alpha N>0$ iff $-C-\alpha G^\top\bar FG-\alpha^{-1}EE^\top>0$, together with the non-strict analogue.
7. Slater condition (p. 17): $\bar F>0$ and $G\neq0$ imply that $N$ has a positive eigenvalue.

Significance

The result itself. Petersen's lemma converts a semi-infinite family of matrix inequalities into one inequality that is jointly an LMI after a Schur complement. In controller synthesis this makes robust quadratic stabilization against norm-bounded uncertainty a convex feasibility problem. The derivation in this paper places the lemma inside a general theory: Petersen's lemma becomes the special case of the matrix S-lemmas for the pair $(M,N)$ of (4.17), and the hypotheses $E\neq0$, $\bar F>0$, $G\neq0$ of the non-strict version become exactly the Slater condition of Theorem 4.7.

Formalizing it. All results here are proved in the paper. None of them, and no matrix S-lemma, has a machine-checked proof on this platform. The mission produces formal statements and proofs of Petersen's lemma in both forms, of the contraction factorization Lemma A.1, and of the strict and non-strict matrix S-lemmas, which are reused by the data-driven stabilization results of the same paper (Theorems 5.1 and 5.3).

Difficulty

The "if" directions are routine: a multiplier certificate yields the robust inequality by completing a square. The difficulty is the converse, which needs a lossless S-lemma for matrix-valued quadratic forms. The scalar S-lemma rests on the convexity of the joint range of two quadratic forms (Dines' theorem). It does not apply directly to matrix inequalities, and the reduction of Section 4.2 from the matrix case to the vector case is the main obstacle. A second, smaller obstacle is the non-strict case: an equivalence with $\leqslant 0$ is false without a Slater-type condition, and the formal statement has to carry $E\neq0$, $\bar F>0$ and $G\neq0$ exactly where the paper does. Petersen's lemma does not follow from a pointwise choice of $F$. The quantifier over $\mathcal F$ must first become a QMI in $H=FG$, which is what Lemma A.1 provides.

Formalization scope

Matrices are Mathlib Matrix over ℝ. In the goal the sizes are Fin n, Fin p, Fin q. In the S-lemmas the two block index types are arbitrary finite types, and a partitioned matrix is a matrix over the sum type. $X<0$ is (−X).PosDef and $X\leqslant0$ is (−X).PosSemidef; both include symmetry, as the paper's notation does. $F^\top F\leqslant\bar F$ is (F̄ − FᵀF).PosSemidef. The multiplier $\lambda$ is required positive, so $\lambda^{-1}$ is the true inverse. The pseudo-inverse is the unique matrix satisfying the four Penrose conditions, selected by Hilbert's ε, and the square root is Mathlib's CFC.sqrt under the scoped matrix order. "At least one positive eigenvalue" refers to the eigenvalues of the symmetric matrix $N$. "Full column rank" is B.rank = q.

Two choices differ from a literal transcription, and both are disclosed in the items. The strict "Moreover" of Lemma A.1 carries no rank hypothesis, because $A^\top A<B^\top B$ already forces full column rank. The Schur step includes its non-strict analogue, which the paper uses implicitly ("the proof of statement (b) is analogous").

A trivializing formalization is excluded. The quantifier in the goal ranges over every $F\in\mathbb R^{p\times q}$ with $F^\top F\leqslant\bar F$, not over a fixed $F$ or over $H$. Part (b)'s extra hypotheses are not added to part (a), and the sanity instance $n=p=q=1$, $C=-3$, $E=G=\bar F=1$ satisfies every hypothesis and both multiplier conditions at $\lambda=1$.

A complete development needs: Loewner-order calculus and Schur complements for block matrices; Moore–Penrose pseudo-inverse identities; positive semidefinite square roots; the scalar S-lemma (Dines' theorem); and the reduction from matrix to vector QMIs. The S-lemmas and Lemma A.1 are reusable well beyond this mission. Proofs of any milestone, and of the auxiliary results of §4.1–4.2 (Lemmas 4.1–4.5, Theorem 4.6) as supporting theorems, are welcome.

Selected references

• H. J. van Waarde, M. K. Camlibel, J. Eising and H. L. Trentelman, Quadratic matrix inequalities with applications to data-based control, SIAM J. Control Optim., 2023; preprint arXiv:2203.12959v3. https://arxiv.org/abs/2203.12959v3
• I. R. Petersen, A stabilization algorithm for a class of uncertain linear systems, Systems & Control Letters 8 (1987) 351–357 (reference [35] of the paper).
• I. R. Petersen and C. V. Hollot, A Riccati equation approach to the stabilization of uncertain linear systems, Automatica 22 (1986) 397–411 (reference [36] of the paper).
• A. Bisoffi, C. De Persis and P. Tesi, Data-driven control via Petersen's lemma, preprint, 2021. https://arxiv.org/abs/2109.12175
• H. J. van Waarde, M. K. Camlibel and M. Mesbahi, From noisy data to feedback controllers: nonconservative design via a matrix S-lemma, IEEE Trans. Automat. Control 67 (2022) 162–175 (reference [54] of the paper).

Motivation

Quadratic matrix inequalities (QMIs) describe sets of matrices rather than sets of vectors. They appear whenever an unknown matrix is constrained by a quadratic bound: in robust control, where an uncertain block of a system is only known to lie in a norm ball or a sector, and in data-driven control, where the system matrices $(A, B)$ of a linear system $x(t+1) = Ax(t) + Bu(t) + w(t)$ are unknown and the measured data, corrupted by noise satisfying a quadratic bound, only pin them down to a set defined by a QMI.

H. J. van Waarde, M. K. Camlibel, J. Eising and H. L. Trentelman (arXiv:2203.12959, SIAM J. Control Optim. 2023) develop a systematic theory of such sets, culminating in matrix versions of the S-lemma and of Finsler's lemma and in data-based stabilization tests. Before any of that can be used, one has to know when the set of matrices satisfying a QMI is nonempty, convex, bounded, has interior points, or contains strict and boundary solutions. Section 3.1 of the paper answers these questions in terms of the blocks of the matrix defining the QMI. This mission formalizes that section, Theorem 3.2, together with the Schur complement identities (3.2)–(3.4) on which it rests.

Setting

All matrices are real. Fix integers $q, r \ge 0$. For a matrix $A$, the Moore–Penrose pseudo-inverse $A^\dagger$ is the unique matrix $X$ with

$$AXA = A,\quad XAX = X,\quad (AX)^\top = AX,\quad (XA)^\top = XA.$$

$\mathbb S^n$ is the set of symmetric $n\times n$ matrices; for $A \in \mathbb S^n$, $A \ge 0$ and $A > 0$ mean positive semidefinite and positive definite, $A \le 0$, $A < 0$ the negative versions, and $A \ge B$ means $A - B \ge 0$ (the Loewner order).

A matrix $\Pi \in \mathbb S^{q+r}$ is always partitioned as

$$\Pi = \begin{bmatrix}\Pi_{11} & \Pi_{12}\\ \Pi_{21} & \Pi_{22}\end{bmatrix},\qquad \Pi_{11}\in\mathbb R^{q\times q},\ \Pi_{22}\in\mathbb R^{r\times r},\ \Pi_{21} = \Pi_{12}^\top .$$

For $Z \in \mathbb R^{r\times q}$ the QMI is

$$\begin{bmatrix} I_q\\ Z\end{bmatrix}^\top \Pi \begin{bmatrix} I_q\\ Z\end{bmatrix} \ge 0,$$

with solution set $\mathcal Z_r(\Pi)$. Replacing $\ge 0$ by $> 0$ or $= 0$ gives the sets $\mathcal Z_r^+(\Pi)$ of strict solutions and $\mathcal Z_r^0(\Pi)$ of solutions of the quadratic matrix equation. The generalized Schur complement is

$$\Pi\,|\,\Pi_{22} := \Pi_{11} - \Pi_{12}\Pi_{22}^\dagger\Pi_{21},$$

and the class $\boldsymbol\Pi_{q,r}$ (equation (3.5) of the paper) consists of the $\Pi \in \mathbb S^{q+r}$ with

$$\Pi_{22} \le 0,\qquad \Pi\,|\,\Pi_{22} \ge 0,\qquad \ker\Pi_{22} \subseteq \ker\Pi_{12}.$$

In Lean these are pinv, qmiForm, ZSet, ZPlus, ZZero, schur and InPi in the namespace QuadMatIneq.Basic.

Formalization targets

Goal: Theorem 3.2

For $\Pi \in \boldsymbol\Pi_{q,r}$:

• (a) $\mathcal Z_r(\Pi)$ is nonempty and convex;
• (b) for $q \ge 1$, $\mathcal Z_r(\Pi)$ is bounded if and only if $\Pi_{22} < 0$;
• (c) $\mathcal Z_r(\Pi)$ has nonempty interior if and only if $\Pi_{22} = 0$ or $\Pi\,|\,\Pi_{22} > 0$;
• (d) $\mathcal Z_r^+(\Pi) \ne \varnothing$ if and only if $\Pi\,|\,\Pi_{22} > 0$;
• (e) $\mathcal Z_r^0(\Pi) \ne \varnothing$ if and only if $\operatorname{rank}\Pi_{22} \ge \operatorname{rank}(\Pi\,|\,\Pi_{22})$.

Milestones

For $\Pi \in \mathbb S^{q+r}$ with $\Pi_{22} \le 0$ and $\ker\Pi_{22}\subseteq\ker\Pi_{12}$:

• (3.2): $\ker\Pi_{22}\subseteq\ker\Pi_{12} \iff \Pi_{12}\Pi_{22}\Pi_{22}^\dagger = \Pi_{12}$, and

$$\Pi = \begin{bmatrix} I_q & \Pi_{12}\Pi_{22}^\dagger\\ 0 & I_r\end{bmatrix}\begin{bmatrix}\Pi\,|\,\Pi_{22} & 0\\ 0 & \Pi_{22}\end{bmatrix}\begin{bmatrix} I_q & 0\\ \Pi_{22}^\dagger\Pi_{21} & I_r\end{bmatrix};$$

• (3.3): $\begin{bmatrix} I_q\\ Z\end{bmatrix}^\top \Pi \begin{bmatrix} I_q\\ Z\end{bmatrix} = \Pi\,|\,\Pi_{22} + (Z + \Pi_{22}^\dagger\Pi_{21})^\top\Pi_{22}(Z + \Pi_{22}^\dagger\Pi_{21})$;
• (3.4): $\Pi\,|\,\Pi_{22}$ is the value at $Z = -\Pi_{22}^\dagger\Pi_{21}$ and dominates the value at every $Z$ in the Loewner order;
• the claim after (3.4): $\mathcal Z_r(\Pi) \ne\varnothing$ if and only if $\Pi\,|\,\Pi_{22}\ge 0$;
• Theorem 3.2(b), (c), (e) as separate items.

Significance

Theorem 3.2 turns geometric questions about a set of matrices into finite checks on the blocks of $\Pi$: semidefiniteness, definiteness, vanishing and a rank comparison. In the data-driven setting of the paper, $\mathcal Z_r(\Pi)$ (after transposition) is the set of noise samples, and hence of systems, consistent with the data; part (b) decides when that set is compact, part (c) when it has interior, and (a) guarantees convexity, which is what allows linear matrix inequalities to be used over it. The identities (3.2)–(3.4) are used throughout the rest of the paper, in the matrix S-lemma, the matrix Finsler lemma and the parametrization of solution sets.

The result and its proof appear in the paper; this mission produces machine-checked versions. Mathlib has the Schur complement for invertible blocks and positive semidefiniteness, but no Moore–Penrose pseudo-inverse for matrices and nothing on QMI solution sets. To the knowledge of this mission no formalization of these statements exists.

Difficulty

The obvious argument is the classical Schur complement, which requires $\Pi_{22}$ to be invertible. Here $\Pi_{22}$ is only negative semidefinite, and the singular case is exactly where the interesting behaviour lives: the solution set is unbounded precisely when $\Pi_{22}$ has a kernel, and $\Pi_{22} = 0$ gives the whole space. Working with the pseudo-inverse requires the range and kernel identities of $\Pi_{22}^\dagger$ for a symmetric matrix and the kernel inclusion $\ker\Pi_{22}\subseteq\ker\Pi_{12}$ at every step. Part (c) needs a topological argument about the interior in $\mathbb R^{r\times q}$, and part (e) needs a factorization of one positive semidefinite matrix through another of possibly different size, which is a rank argument rather than an identity.

Formalization scope

• Matrices are indexed by arbitrary finite types: $\iota$ with $|\iota| = q$ and $\kappa$ with $|\kappa| = r$, so $\Pi$ is a matrix over $\iota \oplus \kappa$ and its blocks are Mathlib's toBlocks₁₁, …, toBlocks₂₂. Nothing assumes $q, r \ge 1$ except part (b).
• $A^\dagger$ is defined by Classical.epsilon over the four Penrose conditions. Since a solution exists and is unique, this is the pseudo-inverse and not a default value; the total inverse A⁻¹, which is $0$ on singular matrices, is not used anywhere.
• $\ge 0$ and $> 0$ are Mathlib's PosSemidef and PosDef, which include symmetry, matching the paper's convention that definiteness is only asserted for symmetric matrices. $\Pi\in\mathbb S^{q+r}$ is IsHermitian.
• Kernel inclusions are written $\forall v,\ \Pi_{22}v = 0 \Rightarrow \Pi_{12}v = 0$.
• "Bounded" means entrywise bounded, which is equivalent to boundedness in any norm on $\mathbb R^{r\times q}$. The interior is taken in $\mathbb R^{r\times q}$ with its Euclidean topology, not relative to an affine hull.
• Part (b) carries the hypothesis $q \ge 1$. For $q = 0$ the space $\mathbb R^{r\times 0}$ is a single point, so the solution set is bounded for every $\Pi$, including those with singular $\Pi_{22}$, and (b) as printed fails. The other parts are stated without it and hold for $q = 0$ and for $r = 0$.
• The trivializing formalizations are excluded: the pseudo-inverse is not a junk inverse, the class $\boldsymbol\Pi_{q,r}$ is inhabited (e.g. $\Pi = \operatorname{diag}(1, -1)$ and $\Pi = \operatorname{diag}(1, 0)$ for $q = r = 1$), and the identities (3.2)–(3.4) are stated with the paper's exact block layouts.

Infrastructure needed and reusable beyond this mission: the existence and uniqueness of the matrix pseudo-inverse with its basic identities ($(A^\dagger)^\top = (A^\top)^\dagger$, $AA^\dagger$ is the orthogonal projector onto the range), and the generalized Schur complement identities. Contributions of these as separate lemmas are welcome.

Selected references

• H. J. van Waarde, M. K. Camlibel, J. Eising, H. L. Trentelman, Quadratic matrix inequalities with applications to data-based control, SIAM J. Control Optim., 2023; preprint arXiv:2203.12959v3. https://arxiv.org/abs/2203.12959
• D. S. Bernstein, Matrix Mathematics: Theory, Facts, and Formulas, 2nd ed., Princeton University Press, 2009 (reference [4] of the paper, for eigenvalue and pseudo-inverse facts). https://doi.org/10.1515/9781400833344
• F. Zhang (ed.), The Schur Complement and Its Applications, Springer, 2005. https://doi.org/10.1007/b105056