All missions

Motivation

Firms that serve several geographic markets must decide both how much to produce and where to sell it. A capacity limit couples those regional decisions: an extra unit sent to one region cannot also be sent to another. Different transport costs and demand curves make a collection of independent single-region Cournot models inadequate. Alsabah, Bernard, Capponi, Iyengar and Sethuraman study whether this coupled quantity game has a determinate outcome. Their 2020 author version proves a unique equilibrium allocation and characterizes it through firms' marginal profits. This mission concerns that result, Theorem 4.5 on p. 12 of that version.

Setting

There are firms $i=1,\ldots,N$ and regions $r=1,\ldots,R$. Firm $i$ sells quantity $q_r^i\ge0$ in region $r$. Its total output is $q_{tot}^i=\sum_r q_r^i$, constrained by capacity $\kappa^i$. The total sales in region $r$ are $q_r^{tot}=\sum_i q_r^i$. The inverse demand function $p_r(q)$ gives the price when total sales are $q$. Firm $i$ pays production cost $a^i$ per unit and transport cost $t_r^i$ per unit sent to region $r$. Its profit at allocation $Q=(q_r^i)$ is

$$\pi^i(Q)=\sum_r\bigl(p_r(q_r^{tot})-t_r^i\bigr)q_r^i-a^i q_{tot}^i.$$

A strategy for firm $i$ is any nonnegative regional allocation whose total is at most $\kappa^i$. A Nash equilibrium is a feasible profile at which no firm can gain by changing its entire regional allocation while the others hold theirs fixed. This is the feasible unilateral-deviation definition in the paper's Definition 3.1, p. 8.

The marginal profit in region $r$ is

$$g_r^i(Q)=p'_r(q_r^{tot})q_r^i+p_r(q_r^{tot})-t_r^i-a^i.$$

For a vector $\rho=(\rho^i)$ of marginal-profit levels, condition (2) says $g_r^i(Q)\le\rho^i$ and $q_r^i(g_r^i(Q)-\rho^i)=0$ for every firm and region. Proposition 4.2 gives a unique nonnegative allocation satisfying these conditions, denoted $\hat Q(\rho)$, when $\rho$ lies in the box $[0,\bar w]^N$, where $w_r=p_r(0)$ and $\bar w=\max_r w_r$. The reduced-form operator $\Phi$ assigns firm $i$ zero marginal profit if its output at $\rho^i=0$ is below capacity. Otherwise it assigns the marginal-profit level at which its output under $\hat Q$ equals $\kappa^i$. This is the two-case definition on p. 11; it depends on the other firms' marginal-profit levels through $\hat Q$.

Formalization targets

Fixed point of the reduced-form operator

Lemma 4.3 asserts that $\Phi$ has exactly one fixed point in the marginal-profit box:

$$\exists!\rho^*\in[0,\bar w]^N:\quad\Phi(\rho^*)=\rho^*.$$

Unique equilibrium allocation

Theorem 4.5 identifies every equilibrium of the original quantity game with the allocation at that fixed point:

$$Q\text{ is a Nash equilibrium}\quad\Longleftrightarrow\quad Q=\hat Q(\rho^*).$$

The goal includes existence of $\rho^*$ and the equivalence, so it asserts both existence and uniqueness of the equilibrium allocation. Its milestones follow the paper's supporting statements: existence of a pure equilibrium, marginal-profit conditions, existence and uniqueness of $\hat Q$, continuity and comparative statics, fixed points of $\Phi$, and the link from an equilibrium to a fixed point. The Algorithm 4.1 computation clause of Proposition 4.2 and the iteration-convergence clause of Lemma C.5 are identified as partial milestones; their full printed text is retained in the milestone provenance.

Significance

The result establishes that capacities, regional demand, and unequal shipping costs still lead to a single predicted sales allocation under the paper's regularity conditions. It also gives a common language for comparing the original game with a smaller game in marginal-profit vectors. Subsequent results in the paper analyze changes in costs, capacities, prices, and consumer surplus relative to this equilibrium Alsabah et al., §§5–6; those later comparative-statics claims are outside this mission.

The mathematical result is proved in the cited paper. The goal here is a machine-checked Lean development of its model, its fixed-point characterization, and the existence and uniqueness theorem. The current proposal contains definitions and theorem statements, with proofs open. The pure-Nash relation is a published reusable definition; the market model, complementarity allocation, and operator are new interfaces that could also support later formalizations of the paper's comparative-statics results.

Difficulty

An equilibrium of the quantity game satisfies the marginal-profit conditions, but those conditions alone describe candidate allocations and do not replace feasible unilateral deviations. Conversely, a fixed point of $\Phi$ does not become an equilibrium merely from the fixed-point equation: the capacity-constrained regional payoff problem still has to be connected to the allocation $\hat Q$. Uniqueness also requires control of how all firms' regional sales respond when one marginal-profit coordinate changes. Lemma C.4 records weak and strict changes, including boundary cases where a firm stops selling in a region. The existence lemma invokes a general pure-strategy equilibrium argument; the statement is kept even though that infrastructure is substantial in Lean.

Formalization scope

Lean uses Fin N and Fin R for zero-based firm and region indices. An allocation has type Fin N → Fin R → ℝ, with the firm coordinate first, the transpose of the matrix orientation in the paper. Finite sums give firm and region totals. The inverse demands are $C^2$ on $\mathbb R$, strictly decreasing and concave on nonnegative quantities; deriv is therefore the ordinary derivative at the quantities used here. The paper phrases Assumption 1 for direct demand $d_r$ on $[0,w_r]$ and then uses regularity of its inverse $p_r$. The formal model makes that inverse-demand regularity an explicit assumption. It also states $w_r=p_r(0)\ge0$, as implicit in the interval $[0,w_r]$, positive capacities, and nonnegative production and transport costs. Those sign assumptions are needed for the box and the two branches of $\Phi$ to have the stated meaning. No positivity of prices at all quantities or finite choke quantity is assumed.

IsEquilibrium uses the published CarbonDoubleCount.Planner.IsPureNash relation, testing every feasible full strategy deviation. Qhat is chosen as the unique solution of condition (2), and Phi is computed from that allocation and the market capacities. On the stated box, the proposal's milestones establish that the selection and inverse branches denote the paper's objects. The intended theorem excludes encodings that choose an active set freely, pass $\Phi$ or $\rho^*$ as arbitrary parameters, or substitute first-order conditions or coordinatewise deviations for Nash equilibrium. The definition layer and results on continuity, monotonicity, and fixed points are reusable parts of the development. Contributions that prove these stated targets or provide supporting analysis of the firm's concave payoff problem are within scope.

Selected references

• H. Alsabah, B. Bernard, A. Capponi, G. Iyengar and J. Sethuraman, Multiregional Oligopoly with Capacity Constraints, SSRN 3280688, author version dated June 6, 2020; published in Management Science, 2021. SSRN author version.

Why the attacker's timing matters

A visible patroller gives an attacker information: the attacker can observe when a location is vacant and wait for a favorable moment. This changes the patrolling problem from choosing how often to visit each location to choosing a movement rule that remains effective against an adversary who chooses the attack time. The preprint The Uniformed Patroller Game studies this setting on a star network, where the patroller moves between a central base and the locations she protects. Its main result characterizes a robust attack delay and a robust patroller reflection rule for every attack duration, as well as exactly when those choices are unique. The source here is arXiv:1908.07366v2, by Alpern, Chleboun, and Katsikas; the later journal article has a different title and author list.

The star and the two strategy sets

The network $S_n$ has a centre $C$ and $n$ end nodes. Each end node is a location to defend; the centre is a base and is not an attack location. A Markov patroller strategy is a pair $(p,s)$. When at $C$, the patroller goes to each specified end node with probability $p$ and stays at $C$ with probability $r=1-np$. When at an end node, she returns to $C$ with probability $s$ and otherwise stays at that same end node. Thus $p>0$, $np\leq 1$, and $0<s\leq 1$. The strategy does not depend on which node the attacker selects.

The attacker chooses an end node $A$ and an integer delay $d\geq1$. After the patroller leaves $A$, the attacker counts consecutive periods of her absence. If she returns before $d$ periods pass, the count resets. Otherwise the attack begins in the $d$th period of absence. It lasts $m\geq2$ periods and is intercepted if the patroller visits $A$ during that interval. The paper requires $m\geq2$ because a one-period attack could always begin immediately after departure. This mission also takes $n\geq2$, ensuring another end node exists and the conditional attack event has positive probability under the admissible strategies.

Let $T_A$ be the first positive step at which the patroller, having just left $A$ for $C$, returns to $A$. The starting state $X_0=C$ is already the first period of absence. The interception probability is the paper's equation (17):

$$Q_{n,m}(p,s;A,d) =1-\frac{\Pr_C(T_A\geq d+m-1)}{\Pr_C(T_A\geq d)}.$$

The patroller maximizes $Q$ and the attacker minimizes it. A saddle point is a pair of strategies for which neither can improve by changing alone, with comparisons over all admissible $(p,s)$ and all end-node-and-delay pairs $(A,d)$. A strategy is called optimal if it occurs in a saddle point. The source analyzes pure strategies in these parametric sets; a pure saddle remains a saddle if independent randomization of these strategies is permitted.

Formalization targets

Main theorem

Theorem 1 asserts that some optimal patroller strategy has $s=1$ and pairs with an attack at any end node with $d=2$. It also asserts two exact uniqueness regimes:

$$\begin{aligned} &d=2\text{ is the only optimal delay}\quad\Longleftrightarrow\quad m\text{ is even},\\ &s=1\text{ is the only reflection probability of an optimal patroller strategy} \quad\Longleftrightarrow\quad m\geq3. \end{aligned}$$

The patroller's centre-to-end probability $p$ is selected optimally; it is not fixed in the main statement. The attack node is immaterial by symmetry, but it remains an explicit part of every attacker strategy. The theorem is posed over the full strategy sets, so its uniqueness assertions cannot be satisfied by restricting those sets to the displayed choices.

Cases and supporting targets

The milestone list follows the source's symmetry reduction, Lemmas 1–3, equations (3) and (15), and Propositions 1–2. For $m=2$, Proposition 1 identifies $\hat p=1-\sqrt{n(n-1)}/n$ and the value $V=(2n-1)-2\sqrt{n(n-1)}$. It also identifies optimal reflection probabilities below one. For odd $m$, Proposition 2 identifies the unique optimal patroller strategy $(1/n,1)$, permits every attacker delay, and gives

$$V=1-\left(\frac{n-1}{n}\right)^{(m-1)/2}.$$

For general even $m$, the statement that an optimum has $np<1$ is recorded separately. It is needed to support the delay-uniqueness clause, while the paper illustrates this interior maximum numerically in Figure 2 rather than proving it as a numbered result.

What the result settles

The theorem reduces the strategic choices in this game: regardless of attack duration, delay two is an optimal response, and full reflection is compatible with an optimal patrol. The uniqueness clauses explain when alternatives are possible. With odd duration, the zero-holding random walk makes all delays equally good for the attacker. With duration two, a range of reflection probabilities below one remains optimal for the patroller. Those facts distinguish a recommendation that is optimal from one that is forced by the game.

The paper gives arguments for its numbered results, but this mission's Lean theorems are open statements awaiting machine-checked proofs. A completed development would provide a reusable finite-path model of conditional hitting probabilities and a formal game-theoretic treatment of the full delay set. The even-duration interior-maximizer milestone also calls for an analytic proof of a property that the preprint supports with plots. The finite-path and generic saddle-point definitions can be reused outside this particular star network.

Where the difficulty lies

The apparently direct comparison of attack delays fails because the patroller's state at attack start depends on surviving the entire waiting period without a return to $A$. The conditional distribution at that start time changes with $d$. Likewise, increasing reflection probability can change both the trajectory and the event on which the payoff is conditioned. A comparison of one-step transition probabilities alone does not establish a comparison of $Q$. Exact uniqueness is more delicate still: at $np=1$ the chain alternates between centre and end nodes, creating genuine ties between delays for odd durations. The even-duration argument needs an optimum away from this boundary.

Formalization scope

Lean represents the original star as Option (Fin n), with none denoting $C$ and some i denoting end node $i$. It builds finite-step taboo path probabilities and defines $Q$ by the ratio above, rather than by a closed-form solution or by the three-state reduction. The two-player saddle predicate is a separate generic definition; the paper-specific model supplies its strategy types and payoff. The definitions use real probabilities. The conditions $n\geq2$, $m\geq2$, $p>0$, $np\leq1$, $0<s\leq1$, and $d\geq1$ are explicit. They make the relevant conditioning event nonempty and ensure the natural-number indices $d-1$ and $d+m-2$ mean the intended periods.

Lemmas 1–2 count the attack start as $X_1$ and count interception by $T(X)\leq m$; the model instead uses $X_0=C$ at departure and $m-1$ later transitions from the attack-start state. Lemma 3's printed claim that odd $m$ makes delay two uniquely optimal conflicts with Proposition 2 at $np=1$. The milestone states a corrected strict claim under $np<1$, for all $m$, and records the discrepancy. Contributions to the model's finite-path identities, the three-state symmetry reduction, the numbered lemmas, the case propositions, and the even-duration interior maximum are all within scope.

Selected references

• S. Alpern, P. Chleboun, and S. Katsikas, The Uniformed Patroller Game, arXiv:1908.07366v2, 2020, §§1–2, especially Theorem 1, p. 10. arXiv
• S. Alpern, P. Chleboun, S. Katsikas, and K. Y. Lin, Adversarial Patrolling in a Uniform, Operations Research 70(1), 2022. This is the later journal version; the mission's page and result indices follow the preprint. DOI

Motivation

Many allocation problems in online advertising are decisions about order, not only about membership. A search engine that rewrites an incoming query into one of several ad-matching configurations, or a publisher that runs a sequence of ad allocations over a day, extracts revenue that depends on which configurations are used and on the order in which they are applied: advertisers' budgets are spent down along the way, so a configuration run early changes what a later one can earn. Classical submodular set functions cannot express this order dependence, and the guarantees developed for them do not apply directly.

Alaei, Makhdoumi and Malekian (arXiv:1009.4153v4; Management Science, 2021) introduce sequence functions, which assign a value to every finite sequence of actions, and identify a sequence analogue of monotonicity and submodularity under which a simple greedy rule is provably near-optimal. They apply the discrete version to query rewriting in sponsored search and a continuous version to online ad allocation with budgets.

Timeline:

• 1978: Nemhauser, Wolsey and Fisher prove that the greedy algorithm achieves a $1-1/e$ fraction of the optimum for maximizing a monotone submodular set function under a cardinality constraint (Math. Programming 14).
• 2010–2021: Alaei, Makhdoumi and Malekian state the discrete and continuous sequence-submodular framework and prove the $1-1/e^{\alpha}$ guarantee for $\alpha$-approximate greedy choices (arXiv first version 2010, journal version 2021).

Setting

Let $\mathcal S$ be a finite set of actions. A discrete sequence is a tuple $A=(s_1,\dots,s_k)$ with $k\ge0$ and every $s_i\in\mathcal S$; for $k=0$ it is the empty sequence $\emptyset$. Its length is $|A|=k$, and $\mathbb H^D(\mathcal S)$ denotes the set of all discrete sequences. The concatenation $A\perp B$ lists the elements of $A$ followed by those of $B$. For $H=(s_1,\dots,s_T)$ the refinement $H_{[1,i]}=(s_1,\dots,s_i)$ is its prefix of length $i$, with $H_{[1,0]}=\emptyset$.

A sequence $A$ is dominated by $B$, written $A\prec B$, if $A$ can be obtained from $B$ by removing some of its elements while keeping the order of the remaining ones. Thus $(a,c)\prec(a,b,c)$ but $(c,a)\not\prec(a,b,c)$.

A discrete sequence function is any $u:\mathbb H^D(\mathcal S)\to\mathbb R$. The marginal value of appending $B$ after $A$ is

$$u(B\mid A)=u(A\perp B)-u(A).$$

The function $u$ is sequence-non-decreasing if $u(A)\le u(B)$ whenever $A\prec B$, and $u(\emptyset)=0$ (display (10)). It is sequence-submodular if

$$u(C\mid A)\ \ge\ u(C\mid B)\qquad\text{for all }A,B,C\text{ with }A\prec B$$

(display (11)): appending the same sequence $C$ gains less after a longer history. Assumption 2 requires both properties.

The optimization problem (12) is, for a length budget $T\in\mathbb N$,

$$\max_{H\in\mathbb H^D(\mathcal S)}u(H)\quad\text{subject to}\quad|H|\le T.$$

For $\alpha\in[0,1]$, a sequence $H=(s_1,\dots,s_T)$ is $\alpha$-greedy if at every step its choice is within a factor $\alpha$ of the best single-action marginal value (display (13)):

$$u\big(s_i\mid H_{[1,i-1]}\big)\ \ge\ \alpha\max_{s\in\mathcal S}u\big(s\mid H_{[1,i-1]}\big)\qquad(i=1,\dots,T).$$

Formalization targets

Goal: Theorem 3 (p. 17)

Under Assumption 2, for every $\alpha\in[0,1]$, every $\alpha$-greedy $H$ of length $T$ and every sequence $O$ with $|O|\le T$,

$$u(H)\ \ge\ \Big(1-\frac1{e^{\alpha}}\Big)u(O).$$

Applied to the optimum $O$ of (12), this is the paper's display (14), $u(H)/u(O)\ge1-1/e^{\alpha}$.

Milestones

1. Lemma 10 (p. 26): if $u$ is sequence-submodular, then for every $A$ and every nonempty $B$ there is $s\in\mathcal S$ with

$$u(s\mid A)\ \ge\ \frac1{|B|}\,u(B\mid A).$$

2. Eq. (38) (p. 26): for an $\alpha$-greedy $H$ of length $k$, every $O$ with $|O|\le k$ and every $i$,

$$u\big(s_i\mid H_{[1,i-1]}\big)\ \ge\ \frac{\alpha}{k}\Big(u(O)-u\big(H_{[1,i-1]}\big)\Big).$$

3. Eq. (41) (p. 27): under the same hypotheses,

$$u(H)\ \ge\ \Big(1-\Big(1-\frac{\alpha}{k}\Big)^k\Big)u(O).$$

Significance

For sets, the $1-1/e$ bound of Nemhauser, Wolsey and Fisher is the reference guarantee for greedy selection. Theorem 3 transfers it to sequences: any objective that can be shown sequence-non-decreasing and sequence-submodular inherits a $1-e^{-\alpha}$ guarantee for a greedy rule, with no further analysis. The paper uses this for query rewriting (Theorem 4) and, through the continuous analogue, for budgeted online ad allocation (Theorem 2). The parameter $\alpha$ covers the common situation in which the best next action can only be found approximately, for instance by solving a subproblem with an approximation algorithm.

Theorem 3 is proved in the paper. As far as a search of the Prove2Me catalog shows, no sequence-function model and no sequence-submodular greedy bound has been formalized there; set-function greedy bounds exist on the platform only as separate, set-based statements. This mission produces a machine-checked version of the discrete model and of the guarantee, which later missions on sequence or string submodularity can import.

Difficulty

The set-function argument compares the greedy set with the optimum by adding the optimum's elements one at a time to the current greedy set and using that the union is at least as valuable as the optimum. For sequences the comparison object is $H_{[1,i-1]}\perp O$, and two features of the order break the direct transcription. First, sequence-submodularity only compares marginal values after a dominated history, so each comparison has to be arranged so that the shorter history is a subsequence of the longer one, in the right order. Second, the averaging over the elements of $O$ produces a factor $1/|O|$, while the recursion needs the uniform factor $1/k$; the replacement relies on feasibility $|O|\le k$ together with nonnegativity of $u(O\mid H_{[1,i-1]})$, which comes from monotonicity. A formal proof also has to handle the indices of the refinement and the edge cases $|O|=0$, $k=0$ and $\alpha=0$ that the printed argument passes over.

Formalization scope

All declarations live in the namespace SeqSubmod.Discrete.

• Sequences are Lean lists List S over a type S with [Fintype S]; concatenation is ++, the empty sequence is [], and $|A|$ is A.length.
• Domination $\prec$ is List.Sublist (A <+ B), the subsequence order. It is neither the prefix order nor the subset order of the underlying sets.
• marginal u B A := u (A ++ B) - u A is $u(B\mid A)$, with the arguments in the paper's order.
• Sequence-non-decreasing keeps the normalization $u(\emptyset)=0$, so $u\ge0$; sequence-submodularity has the paper's direction.
• The $\alpha$-greedy condition uses Lean's 0-based indexing: H[i] is the paper's $s_{i+1}$ and H.take i is $H_{[1,i]}$. The maximum over $\mathcal S$ is Finset.univ.sup', which needs [Nonempty S]. This is added and harmless: with no actions the only sequence is empty.
• The optimum of (12) is not defined: the goal quantifies over every $O$ with $|O|\le|H|$. This is equivalent to the statement about the optimum, which exists because there are finitely many feasible sequences.
• The ratio (14) is stated in multiplied form, $(1-e^{-\alpha})\,u(O)\le u(H)$, because the ratio is $0/0$ when $u(O)=0$.
• Lemma 10 adds $B\neq\emptyset$, since $1/|B|$ is undefined at $|B|=0$.

A trivializing formalization is ruled out: a prefix or subset order, a reversed (11), a dropped $u(\emptyset)=0$, or an existentially quantified $O$ would each change the theorem, and none is used.

A complete development needs telescoping sums of marginal values along a list, an averaging argument over a finite sum, the recursion (40), and the inequality $(1-\alpha/k)^k\le e^{-\alpha}$, which Mathlib provides. The definitions file is reusable by any later work on sequence functions, including the continuous model of the paper's §3, which is not part of this mission. Proofs of the milestones, alternative proofs of the goal, and tightness examples are all welcome contributions.

Selected references

• S. Alaei, A. Makhdoumi, A. Malekian, Maximizing Sequence-Submodular Functions and Its Application to Online Advertising, Management Science, 2021; preprint arXiv:1009.4153v4 (2019). https://arxiv.org/abs/1009.4153
• G. L. Nemhauser, L. A. Wolsey, M. L. Fisher, An analysis of approximations for maximizing submodular set functions — I, Mathematical Programming 14, 265–294, 1978. https://doi.org/10.1007/BF01588971

Motivation

A defined benefit pension promises payments whose form depends on a member's employment and retirement status at death, and on the existence and later survival of a qualifying dependent. The same member can generate very different death benefits while employed, after leaving with preserved rights, or after retirement. A scheme may specify a salary-related lump sum before exit, a revalued preserved-rights benefit in deferment, a spouse's continuing pension after death, and instalments under a fixed pension guarantee. Coordination rules determine which payments coincide.

This mission formalises a finite-horizon actuarial contract in which the payable cash amounts and their dates follow explicit benefit switches, rather than being inferred from names such as “spouse's pension” or “death benefit”. The pension and multiple-state foundations are described by Dickson, Hardy and Waters (2020), Chapters 8–11, https://doi.org/10.1017/9781108784184. The contractual rules here are independently defined examples.

Scheme rules and governing documents determine legal entitlement and tax treatment. No salary multiple, spouse percentage, contribution refund or guarantee is universal.

Setting

Time is measured in integer anniversary ticks, numbered from valuation time zero. Let $h$ be a finite mortality horizon, $e$ the employment exit tick and $r$ the pension commencement tick. The coherent contract satisfies $e\leq r\leq h$. A member death-year index $i<h$ means death occurs during $(i,i+1]$ and a death-related lump sum is paid at tick $i+1$. The terminal index $i=h$ denotes no death within the observable horizon. A dependent's corresponding death index is $j$, with the same convention. A same-tick death is treated as non-qualifying; within-year ordering needs a finer model.

The joint mortality law has masses $p_{ij}\geq0$ summing to one. At member death $i$, $q_i\in[0,1]$ is the probability of a qualifying spouse, conditionally independent of the hypothetical dependent death index $j$ given $i$. A spouse qualifies only when $j>i$, then receives payments while $t\leq j$. Eligibility is fixed at death; later mortality is checked at each due date.

An active death has $i<e$, a deferred death has $e\leq i<r$, and a retired death has $r\leq i<h$. Define benefit amounts $L_{\text{A}}(i+1)$, $L_{\text{D}}(i+1)$ and $L_{\text{R}}(i+1)$ at settlement for these disjoint regimes. The active benefit can include an optional salary multiple, an accrued-service amount and a contractual refund. The deferred death lump uses preserved annual pension multiplied by revaluation and an explicit pension-to-capital factor measured in years; any contribution refund is a separate cash amount. The retired benefit is a distinct lump-sum rider if the scheme provides one. No component is automatically cumulative with another merely because both appear in the model.

Let $b_t$ be the original member pension payable at anniversary $t\geq r$, conditional on the member surviving that date. Let $s_{\text{A}}(i+1)$, $s_{\text{D}}(i+1)$ and $s_{\text{R}}(i+1)$ be survivor pensions fixed from the death regime, with survivor indexation multiplier $u_t$. The amounts can reflect salary or service to death, preserved rights, or a fraction of a retirement pension. The main survivor contract pays for $t>i+1$; a separate immediate alternative allows $t=i+1$. Amounts are per instalment, with consistent monthly units when required.

A retirement guarantee of $g$ ticks covers pension due dates $r,r+1,\ldots,r+g-1$. After a retired member dies, remaining guaranteed member instalments continue to the contractual recipient. Under the parallel rule the surviving spouse also receives its separately payable pension. Under the replacement rule the survivor pension is suppressed while the guarantee remains payable, then resumes when eligible after its expiry. A separate commutation switch can replace all unpaid estate-guaranteed instalments with one lump sum at death settlement, priced using consistent forward discount factors. No guarantee or payment alternative is universal.

Formalization targets

Mutually exclusive death states

Existing joint-life mathematics provides basic survivor occupancy identities. This mission extends them to the three death regimes. For $i<h$ and $e\leq r$:

$$I_{\text{A}}(i)+I_{\text{D}}(i)+I_{\text{R}}(i)=1.$$

The indicators are pairwise disjoint, preventing multiple death-regime claims.

Death and subsequent pension cashflows

The second family constructs the realised present value $Z(i,j)$ for a full benefit contract from the paid lump sum and the dated instalments. Write $v_t$ for the discount factor to time zero and $C_t(i,j;\eta)$ for the sum of original member pension, qualifying survivor instalment and remaining guaranteed payment under replacement switch $\eta$. Then

$$Z(i,j;\eta)=v_{i+1}L(i)+\sum_{t=0}^{n-1}v_t C_t(i,j;\eta).$$

The death lump is zero for the censored member state. The instalment horizon obeys $n\leq h+1$ in the root: right-censored members and spouses remain alive at every priced tick. Extension beyond $h$ needs a new mortality model.

Main capstone: event valuation and overlap

The principal target establishes an equality between mortality-event valuation and the payment-date component EPVs, together with a second equality accounting for guarantee coordination. With $V_{\text{event}}$ for expectation over the actual member and dependent death cells, $V_{\text{dated}}$ for the separately priced death, member, spouse and guarantee payment streams, and $O$ for the qualifying retiree-survivor pension suppressed during the guarantee:

$$V_{\text{event}}(\eta)=V_{\text{dated}}(\eta), \qquad V_{\text{event}}(\text{parallel}) =V_{\text{event}}(\text{replacement})+O.$$

The overlap is separately priced using $q_i$, survivor mortality, death regime and payment eligibility. It is not introduced as a residual defined by subtracting two values.

Significance

The event-based formulation follows member status and the amount payable at death. The payment-date formulation uses explicit mortality conditions at each cashflow date, as in the valuation models of Dickson, Hardy and Waters (2020), Chapter 11, https://doi.org/10.1017/9781108784184. Agreement provides an auditable reconciliation between those independently constructed views. Where the spouse receives income while guaranteed member payments continue to an estate, valuing the two promises separately is appropriate. Where a contract suppresses that survivor pension, the overlap term quantifies the adjustment required to prevent charging for both.

Supporting targets cover exit, retirement and guarantee endpoints, and frozen survivor entitlement. Further results mix dependent-age mortality scenarios and value child pensions with an explicit cessation age.

Difficulty

A death benefit calculated from salary or preserved rights at a member's death differs from a pension instalment conditional on living at a subsequent payment date. Moving from a double sum over member and dependent death times to a sum over payment dates must respect that distinction. In particular, multiplying an unconditional probability of marriage at every later instalment would introduce a new eligibility test absent from the contract. The overlap between an estate guarantee and a spouse pension creates a second risk of overvaluation when the intended rule replaces one stream with the other.

Boundary cases are sensitive to strict and weak inequalities. A guarantee ending at $r+g$ has no payment at that endpoint under the due-in-advance anniversary convention adopted here. Same-grid member and dependent death is not automatically resolved by a continuous-time assumption. The project therefore has to distinguish mathematical cashflow identities, genuine survival-law properties and scheme-specific premises throughout its theorem graph.

Formalization scope

Lean 4 represents joint death-year cell masses and real-valued finite sums with targeted Mathlib imports. It supports arbitrary dependent-life mortality associations and user-supplied discount factors, salary schedules, preserved rights, revaluation multipliers and survivor indexation. Salary multiples, contribution refunds, deferred benefit valuations and retirement lump sums are switches or amounts supplied by a contract. The retirement guarantee has zero, parallel and replacement regimes. Payment streams may be represented on a finer integer grid to accommodate monthly schedules, but no mathematical identity in the annual kernel asserts exact continuous-payment equivalence.

The principal theorem assumes a normalised joint mortality law, $e\leq r\leq h$, $n\leq h+1$ and $0\leq q_i\leq1$. The event-to-payment equality follows from explicit realised payments, not a vacuous equality hypothesis, independence assumption or constant-rate restriction. It relies on genuine death-year and survivor eligibility indicators, rather than stipulating valuation equality in the hypotheses. Continuous-time integration and stochastic marital-history transitions remain future extensions. Finite spouse age-difference mixtures and age-limited child payments are included as separate supporting results. Statutory GMP/excess floors and pension tax rules are outside the contractual core until a scheme type and applicable legal basis are separately verified.

Selected references

• David C. M. Dickson, Mary R. Hardy and Howard R. Waters, Actuarial Mathematics for Life Contingent Risks, third edition, Cambridge University Press, 2020, Chapters 8 (multiple state models), 9 (multiple decrements), 10 (joint-life benefits) and 11 (pension mathematics). https://doi.org/10.1017/9781108784184
• S. David Promislow, Fundamentals of Actuarial Mathematics, third edition, John Wiley & Sons, 2015: §13.3.1 (DB pension plans), §§10.6–10.8 (two-life contracts), §§11.2–11.3 (multiple-decrement valuation) and §§19.1–19.2 (multi-state pension cashflows). https://books.google.com/books?id=gZ3mBQAAQBAJ

Motivation

We develop a theory of exact transmission of finite-dimensional $C^*$-algebras through quantum channels. These algebras describe hybrid classical-quantum information, allowing the dimension of the quantum system to depend on the classical message. Allowing arbitrary encodings and decodings yields a transmission set of algebra types, ordered by embedding, that unifies zero-error information theory with operator-algebraic error correction. We ask if this set admits a dominating algebra into which every transmittable algebra embeds. Our central finding is that domination can fail even in small dimensions. In its absence, several incomparable maximal algebras can describe different optimal uses of the same channel, forcing the user to select one depending on the operational task and the type of information to be preserved. We introduce hybrid capacities that reconstruct the only possible dominating algebra type and present a complete finite characterization of domination using minimal forbidden algebra types. We identify dominating algebras for channels whose operator systems are graph-isomorphic to $*$-algebras, including highly divisible channels, and for channels with zero one-shot zero-error quantum capacity. Under tensor products, we prove that joint coding can produce new algebra types, giving an algebraic analogue of superadditivity from Shannon theory. Domination can fail for the joint use of two channels, even when both channels separately admit dominating algebras. Finally, we construct a channel whose $n$-fold tensor powers have doubly exponentially many maximal algebra types, attaining the largest possible growth scaling for finite-dimensional channels. Consequently, new transmittable algebra types appear at arbitrarily large block-lengths for this channel, so its full transmission structure cannot be generated from any finite collection of bounded-block-length codes. △ Less

This mission is the statement-level formalization of Transmitting algebras through quantum channels (arXiv:2609.40054v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

49 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Main nonexistence result; Example 4.2 and (4.3) (Main nonexistence result; Example 4.2 and (4.3), PDF p. 30). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 4.20 and Definition 2.13, p.17: Canonical peripheral spectral projection P_Phi; support H0perp=im P_Phi(I); restricted channel and its adjoint image Xstar(Phi) with ordinary multiplication. (hard)

Selected references

• Transmitting algebras through quantum channels, arXiv:2609.40054v1, https://arxiv.org/abs/2609.40054v1

Motivation

Firms that already buy a service from an incumbent supplier regularly re-source the contract: they invite new suppliers, the entrants, to compete in a descending open-bid auction. Entrants may be cheaper but are unproven: before the contract can be awarded to an entrant, the buyer must pay for qualification screening (visits to the supplier's facility, purchasing and testing sample products), and an entrant passes only with some probability. Industry practice splits into screening every entrant before the auction (pre-qualification) and screening only the winner after it (post-qualification). Zhang, Chen and Katok, “Now or Later?” When to deploy qualification screening in open-bid auction for re-sourcing, Operations Research 69(6), 2021, compare the two formats in equilibrium.

In the post-qualification format (POST), the incumbent needs no screening, so he faces a genuine dynamic decision: as the clock price falls and entrants drop out, when should he quit? His drop-out price determines the buyer's procurement cost in POST, and Theorem 2 of the paper characterizes it completely. This mission formalizes that theorem.

Setting

Costs lie in an interval $[\underline R,\overline R]$. The incumbent's cost is $x_0\in[\underline R,\overline R]$. There are $N\ge2$ entrants with i.i.d. costs of density $f_e$ and c.d.f. $F_e$, supported on $[\underline R,\overline R]$. Screening one entrant costs the buyer $K>0$, and an entrant passes with probability $\beta\in(0,1)$. In POST, the clock descends from $\overline R$; when the incumbent drops out at price $b$, the price jumps down by the decrement $\Delta:=K/\beta$, and the incumbent ends up with the contract at price $b$ only if all remaining entrants fail screening. The paper assumes $\Delta<\overline R-\underline R$ and Assumption 1: $F_e/f_e$ is nondecreasing and convex.

Before the incumbent quits, an entrant with cost $x_j$ stays until the price reaches his effective cost $x_j+\Delta$. With $m$ entrants left at price $p$, the highest remaining entrant cost therefore has c.d.f. $G^m_e(z;p-\Delta)=[F_e(z)/F_e(p-\Delta)]^m$ and density $g^m_e$. Writing $\ell(x_0)=\max\{\underline R+\Delta,x_0\}$, the incumbent's value $V^m_0(x_0,p)$ solves the Bellman system (8)–(10):

$$\Pi^m_0(b;x_0,p)=\int_b^p V^{m-1}_0(x_0,z)\,g^m_e(z-\Delta;p-\Delta)\,dz+G^m_e(b-\Delta;p-\Delta)(1-\beta)^m(b-x_0),$$ $$V^m_0(x_0,p)=\max_{b\in[\ell(x_0),p]}\Pi^m_0(b;x_0,p),\qquad V^0_0(x_0,p)=p-x_0 .$$

Here $b$ is the planned drop-out price. The integral covers the event that an entrant drops out first, at price $z$; the second term covers the event that the incumbent quits at $b$ and all $m$ entrants then fail screening.

Theorem 2 introduces four objects. $m^\star(x_0)$ is the floor of the minimum over $b$ of $(1-\beta)F_e(b-\Delta)/(\beta(b-x_0)f_e(b-\Delta))$. The compete threshold $b^\star_m(x_0)$ is the first price at which $H(b)=F_e(b-\Delta)/f_e(b-\Delta)$ falls below $L^m(b;x_0)=m\beta(b-x_0)/(1-\beta)$. The switching price $p^\star_m(x_0)$ is the least price above $b^\star_m(x_0)$ at which quitting is worth as much as competing down to $b^\star_m(x_0)$. The candidate drop-out rule is $s^\star_m(x_0;p)$.

Formalization targets

Goal: Theorem 2

For all $x_0\in[\underline R,\overline R]$, $1\le m\le N$ and $p\ge\ell(x_0)$:

$$s^\star_m(x_0;p)=\begin{cases}b^\star_m(x_0)\wedge p,& m>m^\star(x_0),\ p\le p^\star_m(x_0),\\ p,&\text{otherwise}\end{cases}\quad\text{maximizes } b\mapsto\Pi^m_0(b;x_0,p)\text{ on }[\ell(x_0),p],$$

and $V^m_0(x_0,p)=\Pi^m_0(s^\star_m(x_0;p);x_0,p)$. The goal also asserts that $m^\star,b^\star_m,p^\star_m$ are well defined and satisfy $p^\star_m>b^\star_m\ge x_0$. It asserts the monotonicity of part (i): $m^\star$ and $b^\star_m$ are nondecreasing in $x_0$, $b^\star_m$ is nonincreasing in $m$, and $p^\star_m$ is nonincreasing in $x_0$ and nondecreasing in $m$. Finally, $s^\star_m(x_0;p)$ is nondecreasing in $x_0$ and $p$ and nonincreasing in $m$.

Milestones

The proof in the e-companion (pp. ec5–ec11) provides the milestones, in attack order:

1. the drop-now value $(1-\beta)^m(p-x_0)\le V^m_0(x_0,p)$;
2. the derivative formula (EC.7) with its bound $\zeta^m$;
3. the factorization (EC.8)–(EC.9) of $\zeta^m$ through $H-L^m$;
4. well-definedness of $b^\star_m$ and $p^\star_m$;
5. Lemma EC.1 (a)–(d);
6. Claim EC.1, the sign pattern of $\zeta^m$;
7. Lemma EC.2, the induction behind the monotonicity of $p^\star_m$;
8. the fold-only case $m\le m^\star(x_0)$.

Significance

The theorem turns an infinite-horizon-looking stopping problem into a compete-or-fold rule. Either the incumbent stays in until the price falls to the threshold $b^\star_m(x_0)$, or he drops out immediately. The choice depends only on how many entrants remain and on whether the price is above the curve $p^\star_m(x_0)$. With Lemma 2 and Theorem 1 (the entrants' strategies), this completes the equilibrium of POST. The paper's comparison of POST and pre-qualification, and its closed form for the buyer's expected cost, both rest on this equilibrium.

The result is proved in the paper; it has not been machine-checked. A formal proof would check a long argument with an intricate induction: Lemma EC.2 interleaves the strict monotonicity of $\Pi^{m'}_0$ with the monotonicity of $p^\star_{m'}$ in $m'$ and $x_0$. It would also check the treatment of the boundary case $x_0=\underline R+\Delta$, where the proof appeals to the convexity in Assumption 1.

Difficulty

The obvious argument differentiates $\Pi^m_0$ in $b$ and reads off the sign. That fails because the derivative involves $V^{m-1}_0(x_0,b)$, which is itself the value of an optimization. Its sign is controlled by the explicit function $\zeta^m$ only after an induction on $m$ shows that $V^{m-1}_0$ has the form $(1-\beta)^{m-1}(b-x_0)$ wherever it matters. The induction must carry the ordering of $b^\star$, $b^{\star\star}$ and $p^\star$ across different $m$ and $x_0$ (Claim EC.1) at the same time. Another difficulty is that $\Pi^m_0$ must be evaluated beyond the current price: $p^\star_m(x_0)$ is defined at the reference price $\overline R+\Delta$ and may exceed $p$.

Formalization scope

All prices and costs are real numbers, and $m$ is a natural number with $1\le m\le N$. The standing assumptions (including Assumption 1) are hypotheses of every statement. One hypothesis is added to the page: $f_e$ is positive and continuous on $[\underline R,\overline R]$. The page's own formulas divide by $f_e(b-\Delta)$ and differentiate (9) in $b$. $\Delta$ is defined as $K/\beta$, not taken as a parameter, and $F_e$ is the integral of $f_e$.

The max in (8) is a real supremum over the compact feasible interval; that it is attained is part of the goal. The integral in (9) is a signed interval integral, so $\Pi^m_0(b;x_0,p)$ is given by (9) for $b>p$ as well. The minimum defining $m^\star$ is read as an infimum over $(\max\{x_0,\underline R+\Delta\},\overline R+\Delta]$, because the ratio has a zero denominator at $b=x_0$. The page's $(b^\star_m,\infty]$ is taken over the reals. "Optimal drop-out price" means a maximizer in (8): at $p=p^\star_m(x_0)$ two maximizers exist, so uniqueness would be false. The derivative (EC.7) is stated away from the kink $b=\overline R+\Delta$. Milestones use the open price domain $p>\ell(x_0)$ the proof uses.

The game-theoretic layer is not modelled. The hypothesis "entrants follow Lemma 2 and Theorem 1" is how the page derives (8)–(10), and the statement is about (8)–(10). A formalization that states only the sign pattern of $\zeta^m$ or the inductive hypothesis $\mathbb H^m$ would be trivializing; the goal states optimality of $s^\star_m$ in (8) for every $m$, $x_0$, $p$, together with part (i).

A development needs differentiation under a parametrized integral (the fundamental theorem of calculus for $\int_b^p$), continuity of $V^m_0$ in $p$, and real-analysis facts about convex functions crossing a line. These are reusable for other auction and optimal-stopping models. Proofs of any milestone are welcome, as are proofs of the fold-only case independently of the compete case.

Selected references

• W. Zhang, Q. (George) Chen, E. Katok, “Now or Later?” When to deploy qualification screening in open-bid auction for re-sourcing, Operations Research 69(6):1715–1733, 2021. https://doi.org/10.1287/opre.2021.2111 (accepted manuscript: LBS Research Online eprint 1542, https://lbsresearch.london.edu/id/eprint/1542/)