All missions

Motivation

A portfolio can look attractive on average and still perform poorly when the financial system is under stress. Capponi and Rubtsov's Systemic Risk Driven Portfolio Selection asks an investor to choose asset weights using the portfolio return expected in a specified system stress state, rather than using only an unconditional mean or variance. The question is concrete: when the system return is at a low quantile, which portfolio has the highest expected return among outcomes below its own conditional low quantile? This mission formalizes the paper's closed-form answer for the Gaussian case, Proposition 2 of the May 25, 2019 working paper.

The paper distinguishes a system fixed at its value-at-risk level from a system lying anywhere below that level. The former has an explicit optimizer under a technical condition; the latter leads to a different criterion and is outside this mission. The distinction matters because conditioning on one exact system return and conditioning on a tail event produce different laws and different portfolio problems. The working paper, pp. 5–14, develops both settings.

Setting

There are $n\ge2$ risky assets and no risk-free asset. Their random return vector has mean $\mu$ and covariance matrix $\Sigma$. A portfolio is a real weight vector $w$ satisfying $\mathbf1^\top w=1$; the paper imposes no nonnegative-weight or no-short-sale constraint. Its return $R_p$ has mean $\mu_p=w^\top\mu$ and standard deviation $\sigma_p=\sqrt{w^\top\Sigma w}$. The system return $R_m$ has mean $\mu_m$ and standard deviation $\sigma_m$, and $\sigma$ denotes the vector of covariances between each asset and the system. Thus the portfolio-system correlation is $\rho(w)=w^\top\sigma/(\sigma_m\sigma_p)$.

For a law $\nu$ on the real line, value at risk at level $q$ is its lower $q$-quantile, $\operatorname{VaR}_q(\nu)=\inf\{v:q\le\nu(({-}\infty,v])\}$. Let $q_m$ and $q_p$ be quantile levels strictly between zero and one half, as in the paper's stress convention. The conditional value at risk $\operatorname{CoVaR}_{q_p}(w)$ is the $q_p$-quantile of the conditional law of $R_p$ when $R_m=\operatorname{VaR}_{q_m}(R_m)$. The performance criterion is the co-expected return

$$\operatorname{CoER}^{=}(w) =\mathbb E\!\left[R_p\mid R_p\le\operatorname{CoVaR}_{q_p}(w),\ R_m=\operatorname{VaR}_{q_m}(R_m)\right].$$

Under Assumption 2, $(R_p,R_m)$ is bivariate Gaussian, with the means, standard deviations and correlation above. The proof of Proposition 2 uses the joint covariance of all asset returns and the system, $[\Sigma\ \sigma;\sigma^\top\ \sigma_m^2]$. The working paper, pp. 5–7 and 28, gives these definitions and parameters.

Formalization targets

The first targets identify the Gaussian quantile and lower-tail mean, then the conditional Gaussian law. They yield the paper's CoVaR display and the closed form for $\operatorname{CoER}^{=}(w)$ in Proposition 1:

$$\operatorname{CoER}^{=}(w) =w^\top\mu+\frac{\Phi^{-1}(q_m)}{\sigma_m}w^\top\sigma -\frac{\phi(\Phi^{-1}(q_p))}{q_p} \sqrt{w^\top\Sigma w-\frac{(w^\top\sigma)^2}{\sigma_m^2}}.$$

Here $\Phi$ and $\phi$ are the standard normal cumulative distribution and density. Define $\widehat\mu=\mu+\Phi^{-1}(q_m)\sigma/\sigma_m$, $\widehat\Sigma=\Sigma-\sigma\sigma^\top/\sigma_m^2$, and $\lambda=\phi(\Phi^{-1}(q_p))/q_p$. The paper's Appendix partitions $\widehat\mu$ and $\widehat\Sigma$ after asset $n-1$ to obtain $\Delta$ and $Q$. Proposition 2 gives a particular inverse-matrix expression $w^*$ and states that, provided $\lambda>\sqrt{\Delta^\top Q^{-1}\Delta}$, it maximizes $\operatorname{CoER}^{=}$ over all weights summing to one. The goal includes feasibility and uniqueness:

$$\mathbf1^\top w^*=1,\qquad \operatorname{CoER}^{=}(w)\le\operatorname{CoER}^{=}(w^*) \quad\text{for every }w\text{ with }\mathbf1^\top w=1,$$

with equality only for $w=w^*$. The exact $w^*$ is part of the Lean definitions and reproduces the formula printed in Proposition 2, including its last-asset partition and transpose on $Q^{-1}$. The draft theorem chain covers the paper's displayed results (A.1)–(A.4), Proposition 1 (2.4), and the optimization step (A.7)–(A.8); the mission's milestones mark the conditional law, CoVaR, CoER=, the vector formula, and the optimizer. The working paper, pp. 7, 9 and 27–29, states them.

Significance

The result gives an explicit portfolio choice for a stress-sensitive objective, subject only to the full-investment constraint. Its condition identifies the regime in which the finite optimizer exists; when the condition fails, the paper notes that portfolios with arbitrarily high objective values can be constructed. The conditional-return formula also separates ordinary expected return, exposure to the system, and variance left after accounting for that exposure. This permits a precise comparison with a mean-variance portfolio using the same covariance data. The working paper, pp. 7–10, gives the comparison and its numerical illustration.

The paper proves these claims analytically. Here the Lean declarations compile as statements with open proofs; this mission does not claim a machine-checked proof of Proposition 2. A completed formalization would connect the conditional-density meaning of CoER= to the Gaussian formulas and then verify the optimizer for the full class of feasible weights. The quantile, conditional Gaussian, and quadratic objective interfaces are reusable in other risk and stochastic optimization results.

Difficulty

The event $R_m=\operatorname{VaR}_{q_m}(R_m)$ has probability zero for a nondegenerate Gaussian. An ordinary ratio of event probabilities therefore does not define the conditional law at that exact point. The paper relies on the bivariate density to specify it. Even after its Gaussian form is known, the objective contains a square root of a covariance quadratic form, and the feasible set is an unbounded affine hyperplane because weights may be negative. A first-order stationary calculation alone does not establish a global, unique maximizer or exclude unbounded cases. The condition in Proposition 2 addresses that boundary.

Formalization scope

Vectors use Fin (m + 1) → ℝ with $m\ge1$; the final asset is Fin.last m. Matrices are finite real Mathlib matrices. The formal model builds $\mu_p$, $\sigma_p$ and $\rho(w)$ from asset and system parameters, and builds CoER= from the conditional law for every weight vector. It does not replace CoVaR or CoER= by their later closed forms. This prevents the Gaussian and portfolio milestones from becoming restatements of definitions.

The conditional law at an exact system value is the density ratio of the bivariate Gaussian, fixing the continuous version needed at a null event. VaR is a left quantile; $\Phi^{-1}$ is the same construction for the standard normal law. Gaussian variances use nonnegative reals, while portfolio quantities and matrix algebra use reals. Expectations are set integrals under the conditional law, divided by the actual conditional probability of the lower-tail event.

The standing assumptions include positive definiteness of the joint asset-system covariance $[\Sigma\ \sigma;\sigma^\top\ \sigma_m^2]$ and $\sigma_m>0$. Positive definiteness makes all conditional Gaussian variances positive and supplies the nonsingular matrices required by the printed inverse formula. In particular, the mission excludes degenerate covariance matrices for which Lean's total inverse or square root could silently return a default value. The formalization needs finite-matrix positive-definiteness and Schur-complement facts, Gaussian density and quantile facts, set-integral facts, and a constrained optimization theorem for the square-root quadratic objective. Contributions proving any of those faithful milestones or reusable supporting lemmas are within scope.

Selected references

• Agostino Capponi and Alexey Rubtsov, Systemic Risk Driven Portfolio Selection, SSRN working paper 3394471, version of May 25, 2019. SSRN.

Motivation

When a financial institution fails, its counterparties on over-the-counter derivatives are exempt from the automatic stay of bankruptcy: they may terminate their contracts at once, accelerate what is owed to them, and seize posted collateral. Whether this exemption stabilizes or destabilizes the system has been debated since the 1990s, and the failure of Lehman Brothers in 2008 sharpened the question. Termination turns contingent contract values into immediate payment obligations, which can push further institutions into default. But it also brings cash into the system and frees collateral, which can let other obligations be met.

Ghamami, Glasserman and Young (Management Science, 2022) build a clearing model in which payments, collateral seizure, returned collateral and contract termination interact over successive rounds. They compare two policies. Under full termination the default of a node accelerates every derivative contract it is party to, in both directions. Under selective termination (creditor "cherry-picking") only the obligations of the defaulted node become due. Their headline comparison is that, under a bound on aggregate derivatives leverage, full termination leaves no larger system-wide payment shortfall than selective termination.

Setting

A finite set $\mathcal N$ of $N$ nodes. For nodes $i, j$: $\bar p_{ij} \ge 0$ is the payment due from $i$ to $j$, with total $\bar p_i = \sum_k \bar p_{ik}$; $c_i \ge 0$ is the cash of $i$; $m_{ij} \ge 0$ is the collateral posted by $i$ for its obligations to $j$; $v_{ij} \ge 0$ is the value to $j$ of its derivatives with $i$, owed by $i$ on termination, with $v_i = \sum_j v_{ij}$. Diagonals vanish and obligations are netted ($\bar p_{ij}\bar p_{ji} = v_{ij} v_{ji} = 0$). Collateral has constant value $1$.

Round 1. Given payments $p^{(1)}$, node $i$ has assets $A^{(1)}_i = c_i + \sum_k p^{(1)}_{ki}$ and defaults if $A^{(1)}_i < \bar p_i$; $D^{(1)}$ is the default set. A creditor $j$ of a defaulted $i$ first seizes $\Delta_{ij} = m_{ij} \wedge \bar p_{ij}$, and the rest of $i$'s assets is shared pro rata over the residual claims $[\bar p_{ij} - m_{ij}]^+$. Clearing payments are the nonnegative solutions of these fixed-point equations. Excess collateral is returned after Round 1: a defaulted node gets back what was not seized, a surviving node gets back what it had posted to defaulted nodes.

Proposition 2.1 also treats a Round 2 without derivative termination: remaining obligations are $\bar p_{ij}-p^{(1)}_{ij}$, paid from returned collateral and incoming payments. Its total-payment identity (15) is included.

Rounds $m = 2, \dots, N$ under full termination. A default in round $m-1$ creates the obligation $v_{ij}$ between the defaulted node and each counterparty that has survived; unpaid obligations carry over; two survivors owe each other nothing. A node's assets in round $m$ are its cash $c^{(m)}_i$, its returned collateral $r^{(m)}_i$ and the payments it receives; it defaults in round $m$ if they fall short of its round-$m$ obligations, and payments again solve a pro rata fixed-point equation. $D^f = \bigcup_l D^{(l)}$ is the full-termination default set.

Selective termination shares Round 1, and in Round 2 only defaulted nodes owe: $\bar q^{(2)}_{ij} = v_{ij} + \bar p_{ij} - p^{(1)}_{ij}$ for $i \in D^{(1)}$, else $0$. No node defaults after Round 1, and payments $q^{(2)}$ solve the Round-2 equation.

The payment shortfalls are

$$L^f = \sum_{i \in D^f} (v_i + \bar p_i - p_i), \qquad L^s = \sum_{i \in D^{(1)}} (v_i + \bar p_i - q_i),$$

with $p_i$ the total paid by $i$ over all rounds and $q_i$ its total over the two selective rounds. The net worth at the end of Round 1 is $e_i = c_i + r_i + \sum_k p^{(1)}_{ki} - \bar p_i$.

Formalization targets

Goal: Proposition 5.2 (i)

With constant collateral price, common first-round payments, and both models taken at their largest, or both at their smallest, second-round clearing payments ((37) or (38)), the aggregate derivatives leverage condition

$$\sum_{i \in D^f - D^{(1)}} v_i \;\le\; \sum_{i \in D^f - D^{(1)}} e_i \tag{40}$$

implies

$$L^f \le L^s .$$

Milestones

1. Existence and total-payment identity of the two-round freed-collateral model (Proposition 2.1), and existence of clearing payments in every round of full termination (Proposition 4.1).
2. No collateral is seized after Round 1: $\Delta^{(m)} = 0$ for $m \ge 2$.
3. Round-2 comparison of parameters: $\bar p^{(2)} \ge \bar q^{(2)}$ and $a^{(2)} \ge \hat a^{(2)}$; existence of extremal round-2 solutions in both models.
4. Lemma 5.1: $p^{(2)}_{ij} \ge q^{(2)}_{ij}$ at the largest, or at the smallest, solutions.
5. Freed-collateral Round 2 node totals; a node in $D^f - D^{(1)}$ pays at least $e_i$ after Round 1; the shortfall identity (67)–(68).

Significance

The result. Proposition 5.2 is the paper's formal answer to the policy question raised by the safe-harbor debate: it identifies a balance-sheet condition, derivatives liabilities bounded by equity in aggregate, under which the stay exemption does not worsen the total amount of unpaid obligations, even though full termination always produces at least as many defaults (Proposition 5.1). The paper's Example 5.1 shows that without such a condition the comparison can go either way and by arbitrary amounts.

Formalizing it. The paper gives proofs; none is machine-checked. A formalization fixes the accounting of a multi-round collateralized clearing model precisely. This matters here: read literally, the cash recursion of §4 drops unsold returned collateral, and with it Proposition 5.2 (i) fails on a four-node network. The mission states the repaired accounting under which the paper's argument goes through. It also produces reusable statements about extremal fixed points of Eisenberg–Noe-type clearing maps with collateral and their monotone comparison.

Difficulty

The two models are compared at fixed points of different maps, and fixed points need not be unique; a pointwise comparison of arbitrary solutions is false in general. The comparison has to be made at extremal fixed points, through monotone comparative statics in the parameters (obligations and pro rata proportions), and both the largest and the smallest cases are needed. Second, full termination runs up to $N$ rounds with new defaults in each; the shortfall bound requires tracking each node's cash, returned collateral and payments across rounds, and showing that a node defaulting after Round 1 has paid out at least its Round-1 net worth. The tempting shortcut, assuming that full termination creates no new defaults ($D^f = D^{(1)}$), turns the goal into Corollary 5.1, a different and weaker statement.

Formalization scope

All values are real numbers; nodes form a Fintype with decidable equality. One definitions file CollatNet.Termination.Model holds the network, its standing assumptions, Round 1, the §2.3 freed-collateral Round 2, a round state (cash, returned collateral, obligations, survivors), the full-termination round map, the selective Round 2, default sets, shortfalls and net worth. Conventions:

• The collateral price is $1$ throughout (case (i)); prices do not appear.
• Sums over $k \ne i$ are written over all $k$; zero diagonals make them equal.
• A pro rata proportion with zero denominator is $0$, as on the page.
• Clearing payments are nonnegative, i.e. lie in the box $[0, \bar p]$ of the paper's fixed-point argument; otherwise negative circular "payments" would solve the equations.
• Defaults are strict: assets $<$ obligations.
• The number of rounds is $R = \max(2, N)$; payment sequences are indexed by rounds $\ell \in \mathbb N$ and only $\ell = 1, \dots, R$ are used.
• Repaired cash recursion (disclosed): $c^{(m+1)}_i = c^{(m)}_i + r^{(m)}_i + \sum_k p^{(m)}_{ki} - \sum_k (p^{(m)}_{ik} - \Delta^{(m)}_{ik})$. Unsold returned collateral is carried as cash, and seized collateral is not paid out of cash.
• "Largest/smallest second-round payments" are IsGreatest/IsLeast in the componentwise order on each model's round-2 clearing set; later full-termination rounds may be any clearing payments.
• Selective termination is modelled through Round 2 only, as in the appendix's formula (64).

Case (ii) of Proposition 5.2 (illiquid collateral, no excess collateral) is not posed: it is false as printed, because returned collateral is sold below its Round-1 value.

The goal must keep (40) as its hypothesis. Replacing (40) by $D^f = D^{(1)}$, or dropping the later full-termination rounds (which forces $D^f = D^{(1)}$ by construction), would state Corollary 5.1 instead.

Needed infrastructure: Knaster–Tarski on boxes in $\mathbb R^{\mathcal N \times \mathcal N}$ (Mathlib's OrderHom.lfp/gfp), a monotone comparison of extremal fixed points, and finite-sum bookkeeping over rounds. The extremal-fixed-point comparison and the node-total property of pro rata clearing are reusable for other clearing models. Proofs of any milestone are welcome; the shortfall identity and the dominance of round-2 parameters are the most self-contained.

Selected references

• S. Ghamami, P. Glasserman, H. P. Young, Collateralized networks, Management Science 68(3):2202–2225, 2022. https://doi.org/10.1287/mnsc.2020.3938 (accepted manuscript: LSE Research Online 107496, https://eprints.lse.ac.uk/107496/)
• L. Eisenberg, T. H. Noe, Systemic risk in financial systems, Management Science 47(2):236–249, 2001. https://doi.org/10.1287/mnsc.47.2.236.9835
• P. Milgrom, J. Roberts, Comparing equilibria, American Economic Review 84(3):441–459, 1994. https://www.jstor.org/stable/2118061
• A. Tarski, A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics 5(2):285–309, 1955. https://doi.org/10.2140/pjm.1955.5.285

Motivation

A financial network can contain firms or other agents that owe money to one another. Each agent's capacity to pay depends on what it receives from the others, so a payment decision at one agent can change the resources available elsewhere in the network. A clearing payment matrix describes a set of payments consistent with those interdependent resources and with the rules by which each agent divides its available estate among claimants. Whether that matrix is unique matters when the network is used to assign final payments and equity: several clearing matrices can imply different payments even for the same liabilities and endowments. Csóka and Herings study this question for general monotonic division rules, including rules that prioritize some claimants over others. Their working paper gives an explicit example with positive endowments and two clearing matrices, then identifies conditions on the network's liability cycles that guarantee uniqueness. Csóka and Herings, 2021.

Setting

A financial network is $N=(I,z,L,d)$, where $I$ is a finite set of agents, $z_i\ge0$ is agent $i$'s endowment, and $L_{ij}\ge0$ is the liability owed by $i$ to $j$. There are no self-liabilities: $L_{ii}=0$. The total liability of $i$ is $\bar L_i=\sum_jL_{ij}$. A division rule $d^i$ assigns payments $d^i_j(E)$ to each claimant $j$ when agent $i$ has an estate $E\ge0$. Payments are nonnegative, do not exceed individual claims, and sum to $\min\{E,\bar L_i\}$. Every rule is coordinatewise nondecreasing as the estate grows. The model permits $z_i=0$ and permits an agent to have no creditors. Csóka and Herings, 2021, §2.

A payment matrix $P$ has nonnegative entries and zero diagonal. Its entry $P_{ij}$ is the payment from $i$ to $j$. Agent $i$ has asset value $a_i(P)=z_i+\sum_jP_{ji}$ and equity $e_i(P)=a_i(P)-\sum_jP_{ij}$. A row $P_i$ is feasible when it equals $d^i(E)$ for some $E\ge0$. Definition 2.2 calls $P$ clearing when every row is feasible, every agent has nonnegative equity, and every agent paying strictly less than its liability row $L_i$ has zero equity. Here $P_i<L_i$ means coordinatewise $P_{ij}\le L_{ij}$ with at least one strict inequality; $L_i$ is a row, while $\bar L_i$ is a number. Theorem 3.1 establishes that this economic definition is equivalent to the payment equations $P_{ij}=d^i_j(a_i(P))$. Csóka and Herings, 2021, pp. 7–9.

Positive liabilities $L_{ij}>0$ define a directed graph. Let $O(i)$ be the strongly connected component containing $i$. An agent is cyclical when $O(i)$ has at least two members; $C$ is the set of such agents. A component has no successors when no positive liability leads from one of its members to an agent outside it. For a positive claim $L_{ij}>0$, the threshold $\underline a_{ij}$ marks the estate at which $i$ begins paying $j$. A rule is strictly monotonic if each positive-claim payment rises strictly whenever the estate rises within $[0,\bar L_i]$. It is positive monotonic if the same holds once the estate reaches $\underline a_{ij}$. Csóka and Herings, 2021, Definition 2.1 and §4.

Formalization targets

The intermediate targets establish that monotonic division rules are continuous, characterize clearing through the payment equations, show that the clearing matrices form a complete lattice, and show that every clearing matrix gives the same equity vector. The later milestones track what happens when a row differs between the least and greatest clearing matrices and isolate agreement on cyclical rows. These are the statements used by the paper on its route to Theorem 4.5. Csóka and Herings, 2021, §§2–4.

The goal is existence and uniqueness under the paper's three conditions:

$$\begin{gathered} O(i)\text{ cyclical and successor-free}\ \Longrightarrow\ \sum_{j\in O(i)}z_j>0,\\ i\in C,\ z_i>0\ \Longrightarrow\ d^i\text{ positive monotonic},\\ i\in C,\ z_i=0\ \Longrightarrow\ d^i\text{ strictly monotonic},\\ \exists!\,P\ \text{such that }P\text{ is a clearing payment matrix of }N. \end{gathered}$$

The first condition is over components, so stating it for every agent's component makes no difference. No extra monotonicity condition is placed on non-cyclical agents beyond the network's standing assumptions. Csóka and Herings, 2021, Theorem 4.5.

Significance

The theorem gives a network-level criterion for a unique payment outcome under general division rules. It is stronger than merely selecting a least or greatest clearing matrix: those extremal matrices exist even when payments are multiple. The paper uses its criterion to relate earlier uniqueness results for more specialized network and division-rule models, and later studies how uniqueness relates to continuity of a bankruptcy rule. Those later statements are outside this mission. Csóka and Herings, 2021, §§5–7.

The result is proved in the cited paper. This mission asks for a machine-checked Lean development of that known theorem and its listed intermediate results. The prior-art search for this proposal found only special-case clearing models and no published formalization of these exact statements with arbitrary monotonic division rules and zero endowments. The network, division-rule, and clearing definitions would also support formal work on the paper's later bankruptcy-rule results.

Difficulty

Monotonicity of the payment system gives a least and a greatest clearing matrix, but does not force them to coincide. The paper's priority-rule example has all endowments positive and still has distinct clearing matrices. An argument that only invokes a monotone fixed-point theorem therefore cannot settle uniqueness. The difficult distinction is between payment differences that can persist around liability cycles and those that cannot: positive and strict monotonicity are needed at different agents, and the endowment condition concerns only successor-free cycles. Csóka and Herings, 2021, Example 4.1 and Theorem 4.5.

Formalization scope

Agents are an arbitrary finite type, including the empty type. Matrices are functions $I\to I\to\mathbb R$ with entrywise order. Endowments and liabilities are nonnegative, and all division-rule conditions apply on $E\ge0$; a rule's value at negative $E$ is irrelevant. The clearing predicate is Definition 2.2's three conditions. The payment equations are a theorem, not its definition. This distinction prevents uniqueness from being built into the model. The conclusion quantifies over all payment matrices and asserts both existence and uniqueness.

The threshold $\underline a_{ij}$ is represented by the supremum of the nonnegative estates with $d^i_j(E)=0$ and is used only for positive claims, where the standing assumptions make that supremum meaningful. Reachability uses positive-liability walks; between distinct agents these have the same endpoints as the paper's paths of distinct agents. A component includes its named agent, and successor-free means that no positive-liability edge leaves it. The least and greatest clearing matrices in intermediate statements are characterized by order properties, not chosen objects.

A complete development needs finite-sum and real-order facts, continuity of monotone division rules under their sum constraint, complete-lattice fixed-point infrastructure, and finite directed-graph reasoning for strongly connected components. The general network and clearing definitions are reusable. Contributions toward any of the listed milestones, including supporting results about these definitions, are within scope.

Selected references

• Péter Csóka and P. Jean-Jacques Herings, Uniqueness of Clearing Payment Matrices in Financial Networks, GSBE Research Memorandum RM/21/014, Maastricht University, 2021. DOI: 10.26481/umagsb.2021014.
• Péter Csóka and P. Jean-Jacques Herings, Uniqueness of Clearing Payment Matrices in Financial Networks, Mathematics of Operations Research, 2024 (journal version; this mission cites the working paper's numbering). DOI: 10.1287/moor.2023.1354.

Motivation

A client who needs to buy a security may hire a dealer to execute the purchase. The client can observe market prices and trading volume but cannot observe the dealer's trades or the market conditions known to the dealer before trading. A contract based on the closing price or another benchmark can therefore change the dealer's incentives. Baldauf, Frei, and Mollner study when a familiar benchmark, the volume weighted average price (VWAP), implements the outcome the client would choose if the client could control the trades directly (Baldauf, Frei, and Mollner, 2022, §§3–5 of the August 8, 2020 working paper). The question matters wherever a benchmark price determines the payment for an order that an intermediary also influences through its execution.

Setting

A client asks a dealer to acquire one share over a finite number $T\ge1$ of periods. A trading schedule is a vector $x=(x_t)_{t=1}^T$ with $x_t\ge0$ and $\sum_t x_t=1$. Before trading, the dealer sees a vector of positive market conditions $\eta=(\eta_t)_{t=1}^T$; the client does not. Neither party observes the price shocks $\varepsilon=(\varepsilon_t)_{t=1}^T$ in advance. In the specialized model, the dealer chooses a static policy $x(\eta)$, so the whole schedule depends only on $\eta$ and cannot react to prices realized during trading. These information and policy restrictions are stated in §§3.1 and 4.1 of the working paper.

Period $t$ has price $p_t=h(x_t/\eta_t)+\varepsilon_t$ and total market volume $v_t=v(x_t,\eta_t)$. The paper assumes that $h$ is strictly increasing, $y\mapsto yh(y)$ is strictly convex, $v$ is positive on the relevant domain, and $v(x,\eta)=xV(x/\eta)$ for $x>0$, where $V$ is strictly decreasing. Every shock has the same conditional mean: $\mathbb E[\varepsilon_t\mid\eta]=\mu$ almost surely. The paper imposes no independence or identical distribution requirement on the components of $\eta$ or $\varepsilon$. The dealer's utility $u$ is strictly increasing and concave.

A contract $\tau(p,v)$ specifies the client's payment using only the observed price and volume vectors. The dealer's monetary payoff is $\tau(p,v)-p\cdot x$, and the dealer's expected utility must be at least $u(0)$, the utility from rejecting the contract. Incentive compatibility means that the recommended policy maximizes the dealer's expected utility among static policies. The client chooses a contract and a recommended policy to minimize $\mathbb E[\tau(p,v)]$ subject to those two constraints. This is the paper's second best problem; an optimal contract is part of a solution. The VWAP contract pays the realized volume weighted average price, $\tau^{\mathrm{VWAP}}(p,v)=\sum_t p_tv_t/\sum_s v_s$ (working paper, pp. 10–12, 21–22).

Formalization targets

First best and supporting results

The paper identifies the first best policy, the schedule the client would choose with direct control of trading:

$$x_t^{\mathrm{FB}}(\eta)=\frac{\eta_t}{\sum_s\eta_s}.$$

Its expected trading cost is $\mu+\mathbb E[h(1/\sum_t\eta_t)]$, and its share of each period's total market volume is $x_t^{\mathrm{FB}}(\eta)$. The mission includes Lemmas 10 and 11 on conditional means (their static case 1), both parts of Lemma 12's weighted inequality, the Jensen step of the proof of Lemma 3, the three sentences of Lemma 3 (the first best policy and its uniqueness, its expected cost, and its volume shares) as separate statements, and the sufficiency part of Lemma 4. It also records the full insurance and strict incentive claims stated in the proof of Proposition 5. These are the results the paper uses to reach its main assertion (working paper, pp. 21–23, 44–47, 50–53).

Optimality of VWAP

Proposition 5 says that the VWAP contract itself solves the client's second best problem:

$$\tau^{\mathrm{VWAP}}\in\operatorname*{arg\,min}_{\tau:\,\exists x\;(\tau,x)\text{ satisfies (IR) and (IC)}}\mathbb E[\tau(p,v(x(\eta),\eta))].$$

The comparison covers every measurable contract on prices and volumes and every admissible static policy. The goal does not select an impact function, a volume law, or a utility curve beyond the paper's assumptions (working paper, Proposition 5, p. 22).

Significance

Proposition 5 gives a condition under which a common benchmark contract reaches the same expected payment as direct control of the dealer's trading. The result links the first best schedule, the realized VWAP, and the dealer's incentives without specifying a distribution for market conditions or independent price shocks. Under the contract, the first best schedule leaves the dealer with zero realized monetary surplus, while other static schedules yield strictly lower expected utility in the paper's model (working paper, pp. 22–23 and proof on p. 53).

The published paper proves these statements. They do not yet have machine checked Lean proofs. A complete development would supply reusable definitions for static execution policies, price and volume outcomes, contracting constraints, and conditional cost comparisons, together with proofs of the paper's auxiliary inequalities.

Difficulty

A direct comparison of expected VWAP payments across schedules does not establish incentive compatibility: the dealer cares about expected utility of payment minus trading cost, and both terms change when the dealer changes the schedule. The relevant volume weights depend on the same schedule that changes price impact. The key difficulty is the strict equality case in Lemma 12's weighted inequality, including periods in which the dealer trades zero shares. Conditional means must also be carried through schedule dependent but $\eta$ measurable weights, while the final client comparison ranges over all feasible measurable contracts. Dropping that broad comparison would state a substantially weaker result (working paper, Lemmas 10–12 and proof of Proposition 5).

Formalization scope

Time is indexed by Fin T, with paper period $t$ represented by Lean index $t-1$. The probability space is arbitrary, its measure is a probability measure, and $T>0$. Market conditions are positive at every outcome. Shocks are integrable and have conditional mean $\mu$ given the sigma algebra generated by $\eta$. The model assumes measurability of $\eta$, $\varepsilon$, $h$, and $v$; it also assumes integrability of $h(1/\sum_t\eta_t)$ so the stated first best cost is finite. These measurability and integrability clauses make explicit conditions used by the paper's expectations but not separately listed there.

Policies are measurable maps from $\eta$ to schedules on the positive market condition domain; Lemmas 10 and 11 (case 1) are stated, as in the paper's appendix, in a general framework with only their own hypotheses: Lemma 10 for measurable functions of $\eta$ summing to one almost surely (with $\varepsilon_t x_t(\eta)$ integrable), Lemma 11 for measurable nonnegative functions of $\eta$ that need not sum to one and any positive measurable volume function $v$. Contracts are measurable functions of the price and volume vectors; their values off positive volume vectors are irrelevant. Feasible contract policy pairs require finite expected payment, cost, and dealer utility. Incentive compatibility compares against static deviations with integrable utility; under VWAP the omitted deviations cannot improve the dealer's expected utility, while this convention makes the competing contract class at least as demanding for optimality. First best is expressed by almost sure comparison of conditional expected costs. The properties of $h$ and $V$ are imposed on the nonnegative and positive arguments actually used by schedules. Positivity of volumes makes the VWAP denominator nonzero on realized outcomes. These conventions exclude empty schedules, division by zero at realized conditions, and Lean's default zero integral for nonintegrable payoffs.

The mission needs Mathlib's measurable functions, conditional expectations, Bochner integrals, finite sums, convexity, and almost everywhere relations. Its model definitions and the deterministic statements (Lemma 12, the Jensen step and the volume-share identity of Lemma 3, stated for arbitrary $h$, $v$, $V$ and every number of periods) are meant to be reusable. Contributions may prove the conditional mean lemmas, the deterministic inequality and equality case, the first best characterization, the sufficiency criterion, or the proposition. The goal must retain all measurable contracts and feasible static policies; restricting competitors to benchmark contracts or asserting only incentive compatibility would trivialize the intended optimality claim.

Selected references

• M. Baldauf, C. Frei, and J. Mollner, Principal Trading Arrangements: When Are Common Contracts Optimal?, working paper dated August 8, 2020; published in Management Science (2022). DOI: 10.1287/mnsc.2021.4022. This mission cites the working paper's printed pages, not the journal pagination.

Motivation

Influenza vaccine is made in fertilized chicken eggs, and how many doses an egg yields is not known until production is under way. By the time the season begins, the realized supply can fall short of, or exceed, what a planner would want. Two inefficiencies then compound. On the supply side, a manufacturer paid a wholesale price per dose sold carries all the yield risk and plans too little. On the demand side, vaccination protects others as well as the vaccinated person, so self-interested individuals vaccinate too little when supply is ample. When supply is scarce, high-risk individuals compete with low-risk ones under random rationing, and from society's point of view too many low-cost individuals seek the vaccine. Earlier work coordinated one side at a time: Chick, Mamani and Simchi-Levi (Operations Research 56(6), 2008) designed cost-sharing contracts between a government and a manufacturer, and Mamani, Adida and Dey (IIE Transactions on Healthcare Systems Engineering 2, 2012) studied subsidies that coordinate the vaccine market.

Arifoğlu and Tang (2022) design one program for both sides at once: a vaccination incentive $r(Q_r)$ for individuals and a transfer payment $T(Q_r)$ for the manufacturer, both contingent on the realized supply $Q_r$. A lump-sum tax $t$ completes it. The mission formalizes the paper's headline: this modified program attains the social optimum, balances the planner's budget in expectation, and lets the planner divide the optimal welfare between individuals and manufacturer at will.

Setting

The manufacturer plans an input quantity $Q \ge 0$. The realized supply is $Q_r = YQ$, where the yield $Y \ge 0$ is random with law $F$ and finite mean, the wholesale price is $w > 0$, the cost per planned unit is $c > 0$, and $w\,\mathbb E[Y] > c$.

A unit mass of individuals have infection costs $x$ uniform on $[0, \bar x]$, so $G(x) = x/\bar x$ and $\bar G(x) = 1 - G(x)$. A healthy individual enjoys $V_H$, and vaccination costs $w + p$. If a fraction $h$ is vaccinated, an unvaccinated individual is infected with probability $u(h)$ and a vaccinated one with probability $v(h) \le u(h)$. The zero-risk fraction $h_{zr}$ is the least $h$ at which the population risk $(1-h)u(h) + hv(h)$ vanishes (or $1$), and Assumption 1 of the paper imposes monotonicity, convexity and concavity conditions on $u$ and $v$ below $h_{zr}$.

When only individuals with cost above a threshold $\hat x$ seek vaccination, the vaccinated fraction is $h(\hat x, Q_r) = \min\{\bar G(\hat x), Q_r\}$, the fill rate under random rationing is $\phi = \min\{1, Q_r/\bar G(\hat x)\}$, and the ex-post welfare $W(\hat x, Q_r)$ is $V_H$ minus vaccination costs $ph$ minus the expected infection losses. The planner's threshold $x^{(c)}(Q_r)$ maximizes $W(\cdot, Q_r)$; its demand is

$$h^{(c)}(Q_r) = \bar G(x^{(c)}(Q_r)) = \min\{\bar G(x^c_1), Q_r\},$$

where $x^c_1$ is determined by the sign of the marginal social benefit $B = dW/d\hat x$. The planner's ex-ante problem is $\max_Q W^{(c)}(Q) = \mathbb E_Y[W(x^{(c)}(YQ), YQ)] - cQ$, with maximizer $Q^{(c)}$.

Without a program, individuals use the equilibrium threshold $x^{(d)}(Q_r)$: the least cost at which the marginal individual strictly gains from seeking vaccination, $x(u(h) - v(h)) > w + p$, given the fraction $h$ that threshold induces. With an incentive $r$, the right side becomes $w + p - r(Q_r)$, giving $x^{(I)}(Q_r)$. The program is

$$r(Q_r) = w + p - \bar x(1-h^{(c)})(u(h^{(c)}) - v(h^{(c)})),\qquad T(Q_r) = K - (w+p)h^{(c)} - \tfrac{\bar x}{2}\bigl[(1-h^{(c)})^2(u(h^{(c)})-v(h^{(c)})) + v(h^{(c)})\bigr],$$

with a free constant $K$. The planner's net payment is $S^{(I)} = T + r\,h^{(c)}$, and the constant $K_{bn} = \tfrac{\bar x}{2}\mathbb E_Y[(1-(h^{(c)})^2)u(h^{(c)}) + (h^{(c)})^2 v(h^{(c)})]$ is evaluated at $Q^{(c)}$.

Formalization targets

Goal: Proposition 7

With $t = K - K_{bn}$:

$$t = \mathbb E_Y\bigl[S^{(I)}(YQ^{(c)})\bigr],\qquad \text{utility of individuals} = V_H - K,\qquad \pi^{(I)}(Q^{(c)}) = K + W^{(c)} - V_H.$$

In addition, the manufacturer's profit-maximizing quantities are socially optimal, $K > \underline K$ makes the manufacturer better off than without a program, and $K < \bar K$ makes the individuals better off. Here $\underline K = V_H + \pi^{(d)} - W^{(c)}$ and $\bar K = V_H + \pi^{(d)} - W^{(d)}$ are computed at any equilibrium production $Q^{(d)}$ of the chain without a program.

Milestones

1. Lemma A.1(ii) (corrected): $B$ is strictly decreasing above $x_{zr}$, positive below $x^c_1$ and negative above it.
2. Proposition 1 (corrected): $x^{(c)}(Q_r)$ maximizes $W(\cdot, Q_r)$ for $Q_r > 0$, uniquely for $Q_r \ne h_{zr}$.
3. Proposition 5: $x^{(I)}(Q_r) = x^{(c)}(Q_r)$ for every $Q_r \ge 0$, and the maximizers of $\pi^{(I)}$ are those of $W^{(c)}$.
4. Proposition 6: participation and budget neutrality of the unmodified program.
5. Proposition 2: $Q^{(c)}$ exists, is positive and satisfies the first-order condition (10).

Significance

Proposition 7 says a planner can implement the first-best vaccination outcome under random yield with no expected subsidy. Any division of the first-best welfare is also achievable, which is what makes the program implementable: it can be tuned so that both the manufacturer and the population prefer it to the status quo. Propositions 5 and 6 isolate the two halves. The incentive $r$ aligns individual thresholds with the social optimum supply by supply, and the transfer $T$ makes the manufacturer's profit equal to social welfare up to a constant.

The results are proved in the paper and its Online Supplement; none is formalized anywhere. The mission adds three things. First, a machine-checked model of a supply chain with a consumer externality and an equilibrium threshold, which no existing formal library has. Second, corrected statements where the printed ones fail: Lemma A.1(ii) needs strict convexity, and Proposition 1's uniqueness fails at $Q_r = 0$ and at $Q_r = h_{zr}$. Third, an explicit equilibrium concept, the least-strict-gain threshold used in the proofs, under which the coordination claim holds.

Difficulty

The algebra of Proposition 7 is short once coordination is known: pointwise, $w h^{(c)} + T = W(x^{(c)}, Q_r) + K - V_H$, and the individuals' utility collapses to $V_H - K$. The difficulty is in coordination itself, Proposition 5(i). The marginal individual's gain $x(u(h(x)) - v(h(x))) - (w + p - r)$ must vanish exactly at $x^{(c)}(Q_r)$ and be positive above it. Above $x^{(c)}$ that rests on Assumption 1(iv) holding strictly. Below $x^{(c)}$, where the induced fraction is capped by supply rather than by demand, a separate argument is needed. Under the fixed-point reading of equilibrium, every individual is indifferent at $h = h_{zr}$ and coordination fails, so the threshold rule must be used exactly. Proposition 1 needs a piecewise analysis of $W(\cdot, Q_r)$ across the point where demand meets supply, with derivatives taken one-sided at $h = 0$ and through the kink at $h_{zr}$. Proposition 2 needs differentiation under the integral with a moving upper limit.

Formalization scope

The model is a structure of data ($\bar x$, $w$, $p$, $c$, $V_H$, $u$, $v$ and the law $\mu$ of $Y$, a measure on $\mathbb R$) plus a predicate Standing bundling every standing condition:

• the positivity of $\bar x$, $w$, $p$, $c$; $\mu$ a probability measure on $[0,\infty)$ with integrable identity, and $w\,\mathbb E[Y] > c$;
• $0 \le v \le u \le 1$ on $[0,1]$, both continuous, with $u = v = 0$ on $[h_{zr}, 1]$ when $v(1) = 0$;
• differentiability within $[0,1]$ on $[0, h_{zr})$, and Assumption 1(i)–(v).

The formalization commits to these conventions:

• derivatives are derivWithin on $[0,1]$, and Assumption 1(ii) is imposed on $[0, h_{zr})$;
• Assumption 1(iv) is strict;
• $W$ is the closed form of (4);
• expectations are Bochner integrals against $\mu$ of functions of $yQ$;
• $x^c_1$ is a variable satisfying a limit-free form of (8);
• $h^{(c)}$ and $x^{(c)}$ are defined by (7), not as a selection from an argmax;
• the equilibrium threshold is the infimum of the strict-gain set with $\bar x$ inserted, the paper's "the threshold is equal to $\bar x$" clause.

Two corrections carry added hypotheses: strict convexity in Assumption 1(iii) for Lemma A.1(ii) and the uniqueness part of Proposition 1, and a density of $F$ for the first-order condition (10).

Trivializing formalizations are ruled out. The thresholds $x^{(I)}$, $x^{(d)}$ and $h^{(c)}$ are computed from the primitives, never passed in as parameters. The manufacturer's choice under the program is concluded, not assumed. The infimum defining $h_{zr}$ is over a nonempty set, and $\bar x$ is inserted into the threshold set, so no junk value of $\inf\emptyset$ or of a division by zero enters a statement.

A complete development needs one-sided derivatives of convex functions, piecewise monotonicity arguments, and dominated differentiation under the integral sign. The threshold-equilibrium layer is reusable for other vaccination and rationing models. Proofs of any milestone are welcome, as are formalizations of the decentralized results the mission omits: Proposition 3 (decentralized demand) and Proposition 4 ($Q^{(d)} < Q^{(c)}$).

Selected references

• K. Arifoğlu and C. S. Tang, A Two-Sided Incentive Program for Coordinating the Influenza Vaccine Supply Chain, Manufacturing & Service Operations Management 24(1), 2022 (cited from the revised manuscript of 17 June 2020 and its Online Supplement). https://doi.org/10.1287/msom.2020.0938
• S. E. Chick, H. Mamani and D. Simchi-Levi, Supply Chain Coordination and Influenza Vaccination, Operations Research 56(6):1493–1506, 2008 (as listed in the paper's references; no link printed there).
• S. E. Chick, S. Hasija and J. Nasiry, Information Elicitation and Influenza Vaccine Production, Operations Research 65(1):75–96, 2017. https://doi.org/10.1287/opre.2016.1552
• H. Mamani, E. Adida and D. Dey, Vaccine Market Coordination Using Subsidy, IIE Transactions on Healthcare Systems Engineering 2:78–96, 2012 (as listed in the paper's references; no link printed there).

Motivation

How many ways can a closed orientable surface of genus $g$ be "coloured" by a finite group $G$? Precisely: how many group homomorphisms $\pi_1(\Sigma_g)\to G$ are there? The answer is the partition function of two-dimensional Dijkgraaf–Witten theory with gauge group $G$. That theory is the simplest topological quantum field theory (TQFT) in the sense of Atiyah and Segal, and the standard test case for gauge theory with a finite gauge group (Dijkgraaf–Witten 1990, Freed–Quinn 1993). The count has a closed form in terms of the dimensions of the irreducible representations of $G$ alone. It is known as Mednykh's formula.

Timeline. Frobenius (1896) counted pairs with a prescribed commutator, $\#\{(a,b):[a,b]=z\}$, in terms of characters, which is the genus-one case. Frobenius and Schur (1906) treated the non-orientable analogue. Mednykh (1978) proved the formula for every genus using character theory and the standard presentation of $\pi_1(\Sigma_g)$. It was rediscovered in physics as the partition function of 2D and 3D finite-gauge-group TQFTs (Freed–Quinn 1993), and reproved with matrix integrals (Mulase–Yu 2005) and with lattice TQFTs (Snyder 2007). The last paper fixes the form of the statement used here.

Setting

Let $G$ be a finite group. A surface tuple of genus $g$ in $G$ is a family $x=((x_1,y_1),\dots,(x_g,y_g))\in(G\times G)^g$. Its commutator product is

$$\mathrm{commProd}(x)=[x_1,y_1]\,[x_2,y_2]\cdots[x_g,y_g],\qquad [x,y]=xyx^{-1}y^{-1},$$

multiplied left to right. For $z\in G$ let $N_g(z)=\#\{x\in(G\times G)^g:\mathrm{commProd}(x)=z\}$ (commCount G g z). The surface group $\Gamma_g$ (SurfaceGroup g) is the presented group

$$\Gamma_g=\langle a_1,b_1,\dots,a_g,b_g\mid [a_1,b_1]\cdots[a_g,b_g]\rangle,$$

the standard presentation of the fundamental group of the closed orientable surface $\Sigma_g$ of genus $g$, whose Euler characteristic is $\chi(\Sigma_g)=2-2g$.

A complete irreducible family (IrrepFamily G ι) is a finite family $(V_i)_{i\in\iota}$ of finite-dimensional complex representations of $G$ that are irreducible, pairwise non-isomorphic, and such that every irreducible finite-dimensional complex representation is isomorphic to some $V_i$. Write $d_i=\dim_{\mathbb C}V_i$ and $\chi_i(g)=\operatorname{tr}V_i(g)$ for the character.

Formalization targets

Goal: Mednykh's formula

For every finite group $G$, every complete irreducible family and every $g\ge 0$,

$$\sum_{i\in\iota} d_i^{\,2-2g}\;=\;|G|^{\,1-2g}\;\#\operatorname{Hom}(\Gamma_g,G),$$

which is Mulase–Yu, Thm. 1.1 and Snyder, eq. (1) with $\chi(S)=2-2g$. Equivalently, $\#\operatorname{Hom}(\Gamma_g,G)=|G|\sum_i(|G|/d_i)^{2g-2}$. Exponents are integers: at $g=0$ the formula reads $\sum_i d_i^2=|G|$.

Milestones

The milestones follow the algebraic proof of the counting formula recorded in Mulase–Yu 2002, §4, which goes back to Frobenius and Mednykh. Write $(x\star y)(w)=\sum_{\sigma\in G}x(w\sigma^{-1})\,y(\sigma)$ for the convolution of functions on $G$.

• M0. A complete irreducible family exists, with finite index type.
• M1. $\#\operatorname{Hom}(\Gamma_g,G)=N_g(1)$.
• M2. $\sum_i d_i\,\chi_i(z)=|G|$ if $z=1$ and $0$ otherwise.
• M3. For irreducible $V$ of dimension $d$: \sum_{a\in G}\chi_V(axa^{-1}y)=rac{|G|}{d}\chi_V(x)\chi_V(y).
• M4 (Mulase–Yu eq. (4.2)). For irreducible $V,W$: $\chi_V\star\chi_W$ equals rac{|G|}{d_V}\chi_V if $V\cong W$ and $0$ otherwise.
• M5 (Frobenius). $N_1(z)=|G|\sum_i\chi_i(z)/d_i$.
• M6. $N_{g_1+g_2}=N_{g_1}\star N_{g_2}$.
• M7 (Mulase–Yu Thm. 4.1). $N_g(z)=|G|^{2g-1}\sum_i\chi_i(z)\,d_i^{\,1-2g}$ for all $g\ge0$, $z\in G$. Mulase–Yu state it for $g\ge1$; the case $g=0$ is M2.

Significance

The result. The formula says that the number of $G$-coloured genus-$g$ surfaces is a function of the multiset of irreducible dimensions alone. Two groups with the same character degrees (for example $D_4$ and $Q_8$, both with degrees $1,1,1,1,2$) have equally many homomorphisms from every surface group, even though the groups are not isomorphic. In TQFT language the left side is the evaluation $\varepsilon(h^{g})$ of the Frobenius algebra $Z(\mathbb C[G])$, where $h$ is its handle element. The right side is the gauge-theoretic state sum. The identity is the two-dimensional instance of the agreement between the Atiyah–Segal gluing description and the path-integral description of a TQFT. It also gives the volume of the moduli space of flat $G$-bundles on $\Sigma_g$, and it underlies counts of covering spaces of surfaces.

Formalizing it. The theorem is classical and fully proved; to our knowledge it has no machine-checked proof. Mathlib has characters of finite-dimensional representations, their orthonormality (FDRep.char_orthonormal) and Maschke's theorem. It lacks the completeness of irreducible characters, the column orthogonality relation (M2), and any statement linking class sums to characters (M3). These are reusable well beyond this mission. The mission also produces the first formal link between a surface-group presentation and representation theory.

Difficulty

The available orthogonality is the row relation between two irreducible characters. Every step here needs the column relation M2, $\sum_i d_i\chi_i(z)=|G|\delta_{z,1}$. That relation is equivalent to the decomposition of the regular representation $\mathbb C[G]\cong\bigoplus_i V_i^{\oplus d_i}$, and in particular to the finiteness and completeness of the irreducible family. Mathlib has no such decomposition. The convolution identity M4 must also be established in its non-isomorphic case, which the row relation alone does not give in convolution form. The passage from $\operatorname{Hom}(\Gamma_g,G)$ to tuples (M1) depends on the universal property of PresentedGroup and on using one ordering of the commutator product throughout. A proof that bypasses characters by brute counting is not available for general $G$.

Formalization scope

All representations are over $\mathbb C$: FDRep ℂ G with G : Type a Group with [Fintype G]. Characters are FDRep.character and $d_i$ is Module.finrank ℂ (V i). Counts are Nat.card. Powers with exponents depending on $g$ are integer powers (zpow) in $\mathbb C$, so $g=0$ is included and no natural-number truncation occurs. $\Gamma_g$ is PresentedGroup on generators Fin g × Bool, with $a_j=(j,\mathrm{false})$, $b_j=(j,\mathrm{true})$ and the single relator (List.ofFn fun j => ⁅a_j, b_j⁆).prod. This is the standard presentation and stands in for $\pi_1(\Sigma_g)$, since Mathlib has no fundamental groups of closed surfaces. The goal quantifies over every complete irreducible family. M0 shows that such families exist, so the goal is not vacuous. Because the family must be complete and pairwise non-isomorphic, it cannot be chosen to make the sums trivial.

Out of scope: the non-orientable formula of Frobenius–Schur (it needs Frobenius–Schur indicators), positive characteristic, and the bordism-category formulation of TQFTs. Reusable contributions are especially welcome: the decomposition of the regular representation, column orthogonality, and the class-sum Schur lemma.

Selected references

• N. Snyder, Mednykh's formula via lattice topological quantum field theories, arXiv:math/0703073 (2007). https://arxiv.org/abs/math/0703073
• A. D. Mednykh, Determination of the number of nonequivalent coverings over a compact Riemann surface, Dokl. Akad. Nauk SSSR 239 (1978) 269–271; English transl. Soviet Math. Dokl. 19 (1978) 318–320.
• R. Dijkgraaf, E. Witten, Topological gauge theories and group cohomology, Commun. Math. Phys. 129 (1990) 393–429. https://doi.org/10.1007/BF02096988
• D. S. Freed, F. Quinn, Chern–Simons theory with finite gauge group, Commun. Math. Phys. 156 (1993) 435–472. https://arxiv.org/abs/hep-th/9111004
• M. Mulase, J. T. Yu, A generating function of the number of homomorphisms from a surface group into a finite group, arXiv:math/0209008 (2002), §4 (algebraic proof). https://arxiv.org/abs/math/0209008
• M. Mulase, J. T. Yu, Non-commutative matrix integrals and representation varieties of surface groups in a finite group, Ann. Inst. Fourier 55 (2005) 1001–1036. https://arxiv.org/abs/math/0211127
• J. Kock, Frobenius Algebras and 2D Topological Quantum Field Theories, LMS Student Texts 59, Cambridge Univ. Press (2003). https://doi.org/10.1017/CBO9780511615443

Why search changes the bundling decision

A seller deciding whether to offer two products separately or as one bundle also changes what customers need to learn before buying. A customer can know what a familiar product is worth to her while remaining uncertain about a new one. She may pay to inspect the new product, buy it without inspection, or leave. The seller's price can move customers between those choices. Wu, Jin and Chen study this interaction in a tractable two-product market and identify the exact search-cost threshold at which the preferred selling scheme changes (Wu, Jin and Chen, 2022, §§3–5). The question matters for pricing a new product alongside an established one when customers can buy from a description but can also spend effort learning whether the new product suits them.

Market and customer choices

A monopolist faces a unit mass of risk-neutral customers and has zero marginal production cost. Each customer values products 1 and 2 at independent uniform valuations $V_1,V_2\sim U[0,1]$. Product 1 is mature: its valuation $v_1$ is already known to that customer. Product 2 is new: before search, the customer knows only that its valuation is uniform on $[0,1]$, with mean $1/2$. Searching product 2 reveals $v_2$ and costs $c\ge0$. Search is non-obligatory: a customer can buy a new product without inspecting it. The model and the information available at each decision are specified in §3 of the working paper.

Under separate selling, the seller posts nonnegative prices $p_1$ and $p_2$, and each product is purchased independently. The mature product sells when $v_1\ge p_1$; its revenue is $R_M(p_1)=p_1\Pr(V_1\ge p_1)$. For the new product, buying without search gives expected payoff $\mathbb E[V_2]-p_2$, searching gives $\mathbb E[(V_2-p_2)^+]-c$, and leaving gives zero. If a customer searches, she buys only when the observed $v_2\ge p_2$. Write $D_N(c,p_2)$ for the resulting purchase probability, $R_N(c,p_2)=p_2D_N(c,p_2)$, and $R_S(c,p_1,p_2)=R_M(p_1)+R_N(c,p_2)$ for total separate-selling revenue (§4).

Under pure bundling, the seller posts one nonnegative price $p_B$ for both products. A customer who knows $v_1$ compares leaving, buying immediately with expected payoff $v_1+1/2-p_B$, and searching product 2 with expected payoff $\mathbb E[(v_1+V_2-p_B)^+]-c$. After search she buys the bundle only when $v_1+v_2\ge p_B$. Let $D_B(c,p_B)$ be the probability of purchase after these choices, integrating over both independent uniform valuations, and let $R_B(c,p_B)=p_BD_B(c,p_B)$ (eqs. (1)–(2), pp. 11–13).

The customer follows the paper's footnote-10 tie rule: when an immediate purchase and search have equal best payoff, she buys without search; otherwise she searches if its expected payoff is nonnegative and a valuation in the support can meet the price. If search and leaving tie at zero payoff beyond the support, she leaves. The rule matters at exact optimal prices. It also ensures a customer is counted once when the two demand segments printed in §5.2 overlap at $c=0$.

Formalization targets

The mission first identifies the optimal new-product and bundle revenues, including prices at which they are attained. The new-product maximum has three search-cost regimes: $c\le1/32$, $1/32<c\le1/8$, and $c>1/8$. The bundle maximum likewise has three regimes, with boundaries $2-3\sqrt7/4$ and $1/32$. These are the cases of Propositions 1 and 2, pp. 9–13, and form the central milestones. The mature product's optimal revenue is $1/4$, attained at price $1/2$.

The goal is the paper's Theorem 1, p. 15. Write $R_S^*(c)$ for the maximum of $R_S(c,p_1,p_2)$ over $p_1,p_2\ge0$, and $R_B^*(c)$ for the maximum of $R_B(c,p_B)$ over $p_B\ge0$. The theorem asserts that these maxima exist and

$$R_S^*(c)\le R_B^*(c)\quad\Longleftrightarrow\quad 0\le c\le\frac{25}{512}.$$

At $c=25/512$, both revenues equal $9/16$. The formal goal therefore also records the strict form, $R_S^*(c)<R_B^*(c)$ exactly when $c<25/512$, under the standing assumption $c\ge0$. It asserts no unique optimal price: the new product can have two optimal prices at $c=1/32$.

What the result establishes

The threshold gives an exact decision rule in this model: below it, bundling earns more; at it, the schemes tie; above it, separate selling earns more. It is a comparison of optimized revenues, after the seller chooses the best admissible price for each scheme, rather than a comparison at fixed prices. It also makes precise how the familiar product's known value changes the demand generated by searching for the new one (Theorem 1 and its discussion, pp. 15–16).

The paper gives the analytical results, but this mission targets machine-checked proofs of their formal statements. The development contributes a reusable payoff-based rule for non-obligatory search and a concrete uniform-valuation revenue model. It leaves the interval-integral demand definition in place so that deriving the piecewise optimal revenues remains genuine mathematical work. No proof of these results is included in the SSRN copy held for this mission; the supporting milestones are the results stated in its main text.

Where the mathematics is difficult

Search and purchase choices change discontinuously when a price crosses a payoff threshold. For a single new product the same choice is made by every customer, but under bundling the mature valuation $v_1$ sorts customers into buyers without search, searchers who may buy after observing $v_2$, and nonbuyers. The bundle demand must integrate across these groups. Its maximizing price changes regime as $c$ moves through $2-3\sqrt7/4$ and $1/32$ (§5.2 and Figure 1, pp. 12–13). A fixed-price comparison cannot establish Theorem 1, because the best price itself depends on search cost and on the selling scheme.

Formalization scope

Lean uses real prices and costs, with $c\ge0$ and every price restricted to be nonnegative. Uniform expectations are interval integrals over $[0,1]$, and uniform tail probabilities are volumes intersected with that interval. Demand and revenue are built from the customer choice rule; optimal values are expressed as greatest elements of the image of the admissible price set. In particular, the goal does not substitute the closed formulas from Propositions 1 and 2 for those maxima. Such a substitution would reduce the intended economic comparison to arithmetic and leave the search model untested.

The formal choice rule implements footnote 10's immediate-purchase tie preference and selects leaving when zero-cost search could never result in a purchase. Bundle demand counts each customer once, including at $c=0$, where the two weak-inequality demand segments in the printed text overlap. The mature and new valuations remain independent uniform variables; search reveals the new value only, and every search incurs cost $c$. The real-valued interval integrals represent finite, bounded payoffs or bounded purchase probabilities, so their values are genuine expectations and probabilities rather than defaults for nonintegrable functions. No separate assumption of a unique maximizer is used. Contributions that establish the integral identities, measurable choice regions, piecewise demand formulas, and global optimality statements are within scope.

Selected references

• C. Wu, C. Jin, and Y.-J. Chen, Managing Customer Search via Product Bundling, SSRN working paper 3692871, version of 17 January 2022, §§3–5, pp. 7–16. SSRN.

Motivation

When a new durable product is launched, demand typically follows a diffusion curve. A few innovators buy on their own, and later buyers, the imitators, are drawn in by word of mouth from earlier adopters. Bass's diffusion model (Bass 1969) is the standard description of this process and is used throughout marketing and operations to forecast the sales of new products.

In a closed-loop supply chain the producer also collects products returned at the end of their use, remanufactures them and resells them, often at a higher unit margin than new items. Returns arrive only after units have been sold and used, so early in the life cycle there are few of them. Nadar, Kaya and Güler (MSOM 2021) ask whether a producer can gain by deliberately rejecting part of the demand early on. Rejection slows diffusion, but backlogged customers return later, when accumulated returns allow them to be served with higher-margin remanufactured units. Their Theorem 1 gives conditions under which this partial fulfillment is optimal, and conditions under which it is not.

This mission formalizes the second kind of condition, a sufficient condition for immediate fulfillment (meeting all demand in every period) to be optimal, together with the model it is stated in and the diffusion comparisons it rests on.

Setting

A producer sells over periods $t=1,\dots,T$. A sales plan chooses new-item sales $n_t$ and remanufactured-item sales $r_t$, with total sales $s_t=n_t+r_t$ and cumulative sales $S_1=0$, $S_t=\sum_{i<t}s_i$.

Diffusion. Only satisfied customers spread word of mouth. With market size $m$, coefficient of innovation $p$ and coefficient of imitation $q$, the diffusion demand in period $t$ is

$$d_t=\Bigl(p+\frac{qS_t}{m}\Bigr)(m-D_t),\qquad D_1=0,\quad D_t=\sum_{i<t}d_i .\tag{1}$$

When all demand is met, $S_t=D_t$ and (1) is the original Bass process $\widetilde d_t=(p+q\widetilde D_t/m)(m-\widetilde D_t)$.

Segments and backlogs. A fraction $\gamma_1=1-\gamma_2$ of arriving customers wants only new items. The remaining fraction $\gamma_2$ buys remanufactured items when available and new ones otherwise. A fraction $\alpha$ of unmet demand is backlogged one period and the rest is lost. The backlogs $b_{1t},b_{2t}$ of the two segments follow the two-case recursion (4) of the paper.

Returns. A fraction $\beta_i$ of the units sold in period $t$ comes back in period $t+i$. The return volume available for remanufacturing is $e_1=0$, $e_{t+1}=e_t-r_t+\sum_{i=1}^{t}\beta_is_{t+1-i}$ (6).

The producer's problem. Maximize $\sum_{t=1}^{T}[(p_n-c_n)n_t+(p_r-c_r)r_t]$ subject to

• $0\le s_t\le d_t+b_{1t}+b_{2t}$ (2);
• $0\le r_t\le\gamma_2d_t+b_{2t}$ (3);
• $0\le r_t\le e_t$ (5).

The standing assumptions are $p+q\le1$, $\sum_i\beta_i\le1$, $p_n>c_n$, $p_r>c_r$ and $p_r-c_r>p_n-c_n$.

Immediate fulfillment. The immediate-fulfillment plan meets all demand and serves remanufactured-item demand from returns as far as possible. Its return volume is $\widetilde e_t$, and it sells

$$\widetilde r_t=\min\{\widetilde e_t,\gamma_2\widetilde d_t\},\qquad \widetilde n_t=\widetilde d_t-\widetilde r_t .$$

Formalization targets

Goal: Theorem 1(a), first clause

If $\widetilde e_t\le\gamma_2\widetilde d_t$ for $t=1,\dots,T$, then $(\widetilde n,\widetilde r)$ is feasible, and every feasible plan $(n,r)$ satisfies

$$\sum_{t=1}^{T}\bigl[(p_n-c_n)n_t+(p_r-c_r)r_t\bigr]\le\sum_{t=1}^{T}\bigl[(p_n-c_n)\widetilde n_t+(p_r-c_r)\widetilde r_t\bigr].$$

The condition says that, under immediate fulfillment, returns never exceed remanufactured-item demand, so there is never a surplus of returns that delayed customers could absorb.

Milestones

1. §4.1, p. 7. The immediate-fulfillment plan is feasible, and run through (1)–(6) it gives $s_t=d_t=\widetilde d_t$, $S_t=D_t=\widetilde D_t$, zero backlogs and $\widetilde r_t=\min\{e_t,\gamma_2d_t\}$.
2. §4.1, p. 7. For a feasible class-(b) plan whose first rejection is before $T$, cumulative sales satisfy $S_t\le D_t$ through period $T+1$.
3. Lemma 2, p. 7. If a feasible plan first rejects demand in period $t_p<T$, then $D_t=\widetilde D_t$ for $t\le t_p+1$ and $D_t<\widetilde D_t$ afterwards, up to $T+1$; moreover, $D_T^-\ge D_T^+$.

Significance

The result separates the two forces in the paper. Lemma 2 says that rejection always costs diffusion, so its only possible benefit is a better use of returns. The goal shows that this benefit disappears when returns are scarce in every period. Theorem 1(b) and Corollary 1 then show that partial fulfillment can win when returns become abundant before the horizon ends. Together these results give a threshold structure that producers in fast-clockspeed industries, such as smartphones in the paper's numerical study, can check from the immediate-fulfillment trajectory alone.

The results are proved in the paper, with every proof in an online appendix. This mission produces machine-checked statements and, eventually, proofs of the fully posed part of Theorem 1 and of the diffusion comparisons beneath it. No part of this model has been formalized before. The discrete Bass process and the sales-dependent diffusion recursion are reusable for other diffusion-based sales-planning models.

Difficulty

The obvious argument compares profits period by period, and it fails. A feasible plan that rejects demand in some period can sell more than $\widetilde d_t$ in later periods, because backlogged customers return and because $D_T^+$ can be positive. Profit is therefore not dominated termwise. The comparison has to be made over cumulative quantities. One must control cumulative sales against the Bass trajectory along the whole horizon, through the nonlinear recursion (1). One must also control total remanufactured sales through the return recursion (6), whose lags $\beta_i$ couple every pair of periods. The backlog recursion (4) branches on the plan, which rules out a closed form.

Formalization scope

• Lean representation.
  • Parameters are a structure Params with real m p q alpha gamma2 pn cn pr cr, a horizon T : ℕ and beta : ℕ → ℝ. The standing assumptions are a predicate Standing.
  • A plan is a pair n r : ℕ → ℝ, read only on periods $1,\dots,T$.
  • $D$, $b$, $e$ and the immediate plan are defined by explicit recursions on the offset $k=t-1$. The original Bass process is its own definition module.
• Committed conventions.
  • $\gamma_1=1-\gamma_2$.
  • The second case of (4) is used as the "otherwise" branch. The two readings agree on plans satisfying (2)–(3).
  • The sign conditions $m>0$, $p>0$, $q>0$, $\alpha,\gamma_2\in[0,1]$ and $\beta_i\ge0$ are implicit in the paper and stated explicitly.
  • $n_t\ge0$ is not imposed, because the paper does not impose it.
  • Lemma 2's "otherwise" is read as $t_p+1<t\le T+1$.
  • $D_T^\pm$ sum over $t=1,\dots,T$.
• Ruled out.
  • The immediate-fulfillment plan and its profit are computed from the data, not taken as parameters.
  • The feasible set contains (5) and the backlog terms of (2)–(3).
  • Diffusion is driven by sales, not demand, and returns are computed from sales.
  • The goal asserts feasibility of the immediate plan, not only a profit inequality.
• Not formalized.
  • The second clause of Theorem 1(a), parts (b)–(c) and Proposition 1 depend on thresholds stated only in the paper's online appendix.
  • Lemma 1 concerns a case excluded by the standing assumptions.
  • Corollaries 1–5 concern model variants.
• Infrastructure needed. Finite sums over Finset.Icc/Finset.Ico, induction along the recursions, and monotonicity of $x\mapsto x+(p+qx/m)(m-x)$ on $[0,m]$. Contributions of auxiliary lemmas, such as nonnegativity of the Bass trajectory and $\widetilde D_t<m$, are welcome.

Selected references

• E. Nadar, B. E. Kaya, K. Güler, New-Product Diffusion in Closed-Loop Supply Chains, Manufacturing & Service Operations Management, Articles in Advance 2020 (issue 2021). https://doi.org/10.1287/msom.2019.0864
• F. M. Bass, A New Product Growth for Model Consumer Durables, Management Science 15(5), 1969. https://doi.org/10.1287/mnsc.15.5.215