All missions

Motivation

A state on a tripartite quantum system $A \otimes B \otimes C$ forms a Markov chain if it can be reconstructed from its marginal on $A \otimes B$ by a quantum operation from $B$ to $B \otimes C$. We show that the quantum conditional mutual information $I(A: C | B)$ of an arbitrary state is an upper bound on its distance to the closest reconstructed state. It thus quantifies how well the Markov chain property is approximated.

This mission is the statement-level formalization of Quantum conditional mutual information and approximate Markov chains (arXiv:1410.0664v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

39 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Relative entropy from dominated approximants (Lemma 2.1, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Lemma 3.1: A nonempty purification domain in the fixed ancillary space (source-ambiguity)
• Lemma 4.1: A nonempty purification domain in the fixed ancillary space (source-ambiguity)
• Lemma B.11: A nonempty purification domain in the fixed ancillary space (source-ambiguity)
• Theorem 5.1: Arbitrary trace-class root fidelity and lower-semicontinuous extended CMI in a shared state model (hard)
• Remark 5.2: Arbitrary trace-class root fidelity and lower-semicontinuous extended CMI in a shared state model (hard)
• Eq.6: Arbitrary trace-class root fidelity and lower-semicontinuous extended CMI in a shared state model (hard)

Selected references

• Quantum conditional mutual information and approximate Markov chains, arXiv:1410.0664v3, https://arxiv.org/abs/1410.0664v3

Motivation

Between 2017 and 2019 thousands of start-ups sold utility tokens in initial coin offerings (ICOs): digital vouchers that grant access to a product that does not yet exist, sold before launch and often enforced by a smart contract. The financial literature mostly treats ICOs as a way to raise capital. Shakhnov and Zaccaria (SSRN 3613261; published in Management Science, 2023, doi:10.1287/mnsc.2023.4917) ask a different question: what does a token sale do to a monopolist's pricing power when the product has network effects?

Their answer turns on commitment. A token can restrict who may use an early version of the product, so the seller can sell to high-valuation users first and serve the rest later at a lower price, without the incentive to renege that would otherwise destroy such a scheme. The paper characterises when this two-price strategy beats an ordinary one-price sale. The prediction is that token sales are more attractive for products with strong network effects and for more able entrepreneurs, and the paper's empirical section tests it on ICO data. This mission formalizes the theory: the comparison of the two strategies in Sections 5–6 and Appendix A.

Setting

A monopolist sells a digital product to a unit mass of consumers. Consumer types $\theta$ are uniform on $[0,\Theta]$ with $\Theta>1$; $\Theta$ measures how much more an engaged ("active") user values the product than a basic user, and the paper reads it as entrepreneurial ability. If a share $a\in[0,1]$ of consumers is active, a basic user gets utility $v=a\,x$ (display (1)), where $x>0$ is the network intensity, and an active user of type $\theta$ gets $\theta v$.

The paper writes every price as a threshold: choosing $\bar\theta\in[1,\Theta]$ means exactly the types $\theta\ge\bar\theta$ become active, so

$$a=\frac{\Theta-\bar\theta}{\Theta},\qquad v=a\,x,\qquad p=\bar\theta v .$$

$\bar\theta=1$ is the non-discriminatory price $p=v$ at which everyone buys.

• Traditional sales ($T$). One price $p^T_1=\bar\theta v$. Demand is $1$ at $\bar\theta=1$ and $(\Theta-\bar\theta)/\Theta$ for $\bar\theta>1$ (display (3)); the profit is $X_T(\bar\theta)=p^T_1Q(p^T_1)$.
• ICO ($I$). At cost $f>0$, tokens are sold at $p^I_0=\bar\theta v$ (demand (8), the same two-piece formula), and only token holders may become active. The remaining consumers are served later at $p^I_1\in[v,\Theta v]$, with demand $1-Q(p^I_0)$ if $p^I_1=v$ and $0$ otherwise (display (9)). The profit is $X_I(\bar\theta,p^I_1)=p^I_0Q(p^I_0)+p^I_1Q(p^I_1)-f$ (problem (10)).

The optimal payoffs are $X^*_T=\sup_{\bar\theta\in[1,\Theta]}X_T$ and $X^*_I=\sup X_I$ over the pairs $(\bar\theta,p^I_1)$. Strategy $S^*=i$ is an equilibrium when $X^*_i\ge X^*_{-i}$. The closed forms are

$$\theta^*=\max\Bigl[1,\frac{2\Theta+1-\sqrt{\Theta^2+\Theta+1}}{3}\Bigr]\ \ (11),\qquad \tilde\Theta=\frac{\sqrt5+3}{2}\approx2.62,$$ $$F(\Theta)=(\theta^*-1)\Bigl[\Bigl(\frac{\Theta-\theta^*}{\Theta}\Bigr)^2-\frac1\Theta\Bigr],\qquad \bar x=\frac{f}{F(\Theta)} .$$

The main analysis restricts to $\Theta\in(1,3]$.

Formalization targets

Goal: Section 6, (15)–(16), with Appendix A

For $f>0$:

$$1<\Theta\le\tilde\Theta,\ x>0\ \Longrightarrow\ X^*_I<X^*_T\qquad(15)$$ $$\tilde\Theta<\Theta\le3\ \Longrightarrow\ \bar x>0\ \text{ and }\ \bigl(X^*_T\le X^*_I\iff x\ge\bar x\bigr)\ \ \forall x>0\qquad(16)$$

and $\Theta\mapsto\bar x(\Theta,f)$ is strictly decreasing on $(\tilde\Theta,3]$.

Milestones

In attack order:

1. the discriminatory profit (7) decreases in $\bar\theta$ (p. 18);
2. Proposition 1: $X^*_T=\frac{\Theta-1}{\Theta}x$, attained only at $\bar\theta=1$ (p. 17);
3. the late ICO price $p^I_1=v$ is optimal (p. 21);
4. the reduced ICO problem, whose attained maximum over $\bar\theta\in[1,\Theta]$ equals the original optimum (pp. 21–22);
5. Proposition 2: $\theta^*$ is the unique optimal ICO threshold and $X^*_I$ is (12) (pp. 20–21);
6. Lemma 1: $\theta^*=1$ exactly for $\Theta\le\tilde\Theta$ (p. 22);
7. Proposition 3: for $\Theta\in(\tilde\Theta,3]$ the ICO discriminates and traditional sales do not (p. 22);
8. ICO revenues are strictly larger, $X^*_I-X^*_T=F(\Theta)x-f$ with $F>0$ (p. 23);
9. the derivative formula and bounds of Appendix A (p. 35);
10. $F$ has positive derivative and is strictly increasing for $\Theta>\tilde\Theta$ (p. 35).

Significance

The result says when a token sale pays. A token adds no technology to the product. It only lets the seller commit to a two-price schedule, and that commitment pays exactly when the network is valuable enough to cover the cost $f$. Because the threshold $\bar x$ falls with $\Theta$, more able entrepreneurs need weaker network effects to gain from an ICO. This is the comparative static the paper takes to the data. It also shows that network effects can make price discrimination unprofitable for a single-price monopolist (Proposition 1). A commitment device can make it profitable again (Proposition 3).

The paper's arguments are short calculus on closed forms, but several of its claims are stated on closed intervals where they fail at an endpoint. Its Appendix A also assumes the sign of $\bar x$ to prove its monotonicity. A machine-checked version settles the exact ranges and gives the positivity of $F$ an independent proof. No part of the model has been formalized before.

Difficulty

Each step is elementary, and the difficulty lies in the case structure. The traditional-sales profit has a jump at $\bar\theta=1$: (6) is not the limit of (7), so the optimum cannot be read off a derivative. For the ICO the two pieces do join continuously, but the strategy space has two prices, and the late price must be shown optimal at $v$. The ICO optimum $\theta^*$ is the root of a cubic's derivative, which involves a square root. Comparing the two optimal payoffs needs the sign of $F(\Theta)$, and a direct expansion of $F$ in terms of $\sqrt{\Theta^2+\Theta+1}$ does not settle it. Finally, the monotonicity of $\bar x$ is a statement about $F$ on the whole range $\Theta>\tilde\Theta$, which the paper argues via a derivative whose printed formula contains a slip.

Formalization scope

Everything lives in the namespace UtilityTokens.ICOChoice, with one definitions module UtilityTokens.ICOChoice.Setting. All quantities are real-valued functions of $(\Theta,x,f)$ and of the strategy $(\bar\theta,p^I_1)$:

• The demands (3), (8), (9) are piecewise definitions, with the case $\bar\theta=1$ (respectively $p^I_1=v$) split off exactly as on the page.
• $X^*_T$ and $X^*_I$ are suprema (sSup) of the profits over the strategy sets. They are not their closed forms, and Propositions 1–2 prove the suprema are attained maxima.
• $\theta^*$ is the closed form (11), not "the maximizer".
• The ICO strategy set keeps $p^I_1\in[v,\Theta v]$ free; fixing $p^I_1=v$ in the definition would make milestone 3 empty.
• Every statement about $X^*_T$, $X^*_I$ keeps $\Theta>1$, and every statement about $\bar x$ keeps $\Theta>\tilde\Theta$, because sSup and division return junk values outside those ranges.

Deviations from the page:

• The paper prints the ranges as $[1,\tilde\Theta]$ and $[\tilde\Theta,3]$. The formalization uses $(1,\tilde\Theta]$ and $(\tilde\Theta,3]$, because $\Theta=1$ violates the standing assumption and at $\Theta=\tilde\Theta$ the denominator of $\bar x$ vanishes. Proposition 3 is stated on $(\tilde\Theta,3]$ for the same reason.
• (15) is stated strictly, $X^*_I<X^*_T$. This needs $f>0$, which is kept as a hypothesis, as is $x>0$.
• Appendix A's bullets differentiate the interior root $(2\Theta+1-\sqrt{\Theta^2+\Theta+1})/3$, called $\theta^*$ there; they are stated for that root.

Not formalized: consumer types as a probability distribution, the participation constraints and the fixed point from which (3), (8), (9) are derived (taken as primitives), the renegotiation argument of p. 20, the welfare computation of pp. 24–26, Appendix B ($\Theta>3$) and the empirical Section 3. The infrastructure needed is only Mathlib's real analysis (Real.sqrt, HasDerivAt, monotonicity on intervals); nothing outside Mathlib is required. Proofs of any milestone are welcome, as are lemmas splitting the goal into its three conjuncts.

Selected references

• K. Shakhnov and L. Zaccaria, Utility Tokens, Network Effects, and Pricing Power, SSRN working paper 3613261 (PDF of 2023-04-23). https://ssrn.com/abstract=3613261
• K. Shakhnov and L. Zaccaria, Utility Tokens, Network Effects, and Pricing Power, Management Science, 2023. https://doi.org/10.1287/mnsc.2023.4917

Why network information has a cost

Choosing a small group of people to start an intervention can have a much larger effect when their contacts pass it on. In many applications the contacts themselves are expensive to learn: a survey worker can ask about a person's neighbors, or a crawler can request one adjacency-list entry, but neither necessarily has a complete network. Eckles, Esfandiari, Mossel and Rahimian study influence maximization with this information cost included. Their paper asks whether a near-greedy spread guarantee can be obtained while limiting the number of edge queries made to the network. An edge query reveals one indexed neighbor of one vertex. The bound matters when the graph is large and acquiring its edges is a material part of the work, rather than a free preprocessing step.

Graph, spread, and sketches

The independent cascade model starts with a finite undirected simple graph $G=(V,E)$ and a common probability $p\in[0,1]$. Each edge is independently active with probability $p$. Given a seed set $S\subseteq V$, a vertex adopts when an active-edge path joins it to a seed; a seed adopts by a path of length zero. Write $\phi(v,S)$ for the probability that $v$ adopts. The influence function is the expected number of adopters,

$$\Gamma(S)=\sum_{v\in V}\phi(v,S),\qquad \mathrm{OPT}=\max_{S\subseteq V,\ |S|=k}\Gamma(S).$$

The problem is to choose exactly $k$ seeds. Here $n=|V|$ and $1\le k\le n$. These definitions follow Section 2, Definitions 1–2, of the source paper.

The paper's PROBE procedure samples an initial vertex set $V_\rho$ and produces $T$ partial graphs. It explores outward through neighbor queries, retaining each candidate edge with probability $p$. Exploration from a vertex stops once its revealed component reaches a threshold $\tau$. A query is charged even when its answer points to a vertex already explored and the answer is discarded. From these partial graphs, the paper defines an influence estimate $\Gamma^{(T)}_{\rho,\tau}$. Its SEED procedure applies randomized greedy selection to that estimate. Algorithm 4 fixes the parameters, runs PROBE, then runs SEED. The estimator and procedures are specified in Sections 3.1–3.4 of the paper.

Formalization targets

The goal is the explicit Algorithm 4 form of Theorem 7. For $0<\epsilon'\le1$ and $n\ge(30/\epsilon')^2$, let $\Lambda^*$ be the output seed set and $q$ the number of PROBE edge queries. With $\epsilon=\epsilon'/7$ and $\delta=2\log n$, the targets are

$$\mathbb E[\Gamma(\Lambda^*)]\ge(1-1/e)\mathrm{OPT}-\epsilon'n, \qquad \mathbb E[q]\le Q^{n,k}_{\epsilon,\delta}+6T^{n,k}_{\epsilon,\delta}.$$

The first inequality is Theorem 7's spread claim; the second is the explicit query inequality (30) in its Appendix B.12 proof. The theorem also states asymptotic query and run-time classes. This mission states the explicit query bound and does not give a machine-level running-time semantics. Theorem 7 and Appendix B.12 identify both formulas.

The milestones record the approximation-transfer lemma, the two concentration claims for initial sampling and probing, the coverage structure of the truncated sketch, the randomized-greedy guarantee, Theorem 5's high-probability query bound, and the worst-case query bound used to pass to expectation. The statement of each is tied to its source page.

What the result supplies

The spread inequality makes the cost of incomplete graph information explicit: the output's expected spread is within an additive $\epsilon'n$ of the standard $1-1/e$ factor times the complete-information optimum. The query inequality specifies the expected amount of network information Algorithm 4 requests, using the paper's constants $Q$ and $T$. This puts a concrete price on obtaining a seed set without reading the whole graph. The paper gives the corresponding asymptotic discussion and simulations; neither simulations nor a running-time model is part of the target here.

Formalizing this result requires reusable definitions of finite set-function maxima and submodularity, a finite independent-cascade spread model, and an exact account of a random graph-exploration algorithm. The model separates the graph's random active edges from the algorithm's random probes and from SEED's random candidate sets. The resulting definitions can support later statements about graph sampling, coverage functions, and influence maximization. The target is a known paper claim that has been stated in Lean with open proofs; the proposal does not assert that these proof obligations have already been discharged by a machine checker.

Where the difficulty lies

One cannot simply apply a greedy approximation theorem to $\Gamma$: Algorithm 4 chooses seeds using a random, truncated sketch, while its guarantee concerns the original cascade spread. The random initial set, the repeated probe copies, and the threshold each change the objective being optimized. The required probability bounds must hold across all size-$k$ seed sets, not only a fixed one. Query accounting also has to charge revealed neighbors that do not enter the sketch. Those are the reasons the proposition is stronger than a routine monotone-submodular maximization statement; the distinct claims appear in Lemmas 1–3, Theorem 5, and Appendix B.12 of the paper.

Formalization scope

Lean uses $V=\operatorname{Fin}(n)$, a finite undirected SimpleGraph, real-valued probabilities and objectives, and natural logarithms. Cascade probabilities are finite weighted sums over retained edge sets. PROBE randomness is represented by finite permutations and Bernoulli coins; probabilities and expectations are finite weighted sums. A single PROBE realization returns both its sketch edges and its count of step-10 queries. The untruncated sketch uses threshold $n+1$. SEED draws a uniform subset of the remaining vertices at each round and chooses a maximum marginal gain, with least-index tie breaking. These choices make the algorithm in the theorem a defined object, so its expected query count cannot be made zero by treating the entire graph as free input.

Three boundary conventions make Algorithm 4 total. When $\rho>1$, its initial sample size is $\min(\lceil n\rho\rceil,n)$. PROBE's inner loop ends when the selected neighbor indices are exhausted. SEED uses the ceiling of its nonintegral subset size, capped at the number of unselected vertices. The proof targets for Lemmas 2–3 and Theorem 5 explicitly use $n\ge5$ and $\delta\ge2\log n$; Lemma 1 includes $\alpha\ge0$. Lemma 3 also states the inherited initial-sample size and sampling-rate conditions. These refinements are identified in the item descriptions and audit notes. The formulas for $\rho$, $T$, $\tau$, $E$, $C$, and $Q$ retain the constants of equations (5)–(7) of the paper.

The foundational definitions, exact theorem statements, and proofs of the listed milestones are within scope. Results about directed graphs, other diffusion models, and empirical network simulations are separate from this target.

Selected references

• D. Eckles, H. Esfandiari, E. Mossel, and M. A. Rahimian, Seeding with Costly Network Information, Operations Research, 2022; arXiv:1905.04325v5.

Motivation

Many consequential outcomes (a faculty position, a high-paying job) are the end of a long pipeline of earlier stages: neighbourhood, elementary school, high school, college, graduate school. Inequities that compound along such a pipeline are hard to correct by intervening only at its last stage, and a planner with a limited budget would like to decide where along the pipeline to invest. Arunachaleswaran, Kannan, Roth and Ziani (arXiv:2002.06592) introduce the pipeline intervention problem, a stylized optimization model of this question, and study it under a social-welfare objective and two fairness-motivated maximin objectives. The problem is non-convex: the welfare is a product of the decision matrices, so standard convex-optimization guarantees do not apply. Their positive result for social welfare is an additive fully polynomial-time approximation scheme (FPTAS) for networks of constant width, based on a dynamic program over a discretization of the budget and of the probability simplex. This mission formalizes that result.

Setting

A layered graph has $k$ layers $L_1,\dots,L_k$, each with $w$ nodes (the width). Between consecutive layers $L_t$ and $L_{t+1}$ every node is connected to every node. Write $\mathcal D=\{x\in[0,1]^w:\sum_i x(i)=1\}$ for the simplex of probability distributions on $[w]$ and $\mathcal M$ for the set of left stochastic $w\times w$ matrices: nonnegative entries, every column summing to $1$. An instance consists of

1. initial transition matrices $M^0_1,\dots,M^0_{k-1}\in\mathcal M$, where $M^0_t(v,u)$ is the probability of moving from $u\in L_t$ to $v\in L_{t+1}$ (distributions are multiplied on the right);
2. an initial distribution $D_1\in\mathcal D$ of the population over $L_1$;
3. rewards $R(v)\ge 0$ on the final layer $L_k$;
4. for each $t$ a set $E^t_{mal}$ of malleable entries; the other entries cannot be changed.

Changing $M^0_t$ into $M_t$ costs $c(M_t,M^0_t)=\sum_{i,j}|M_t(i,j)-M^0_t(i,j)|$. With budget $B$, the feasible set $\mathcal F(B,M^0)$ consists of the tuples $(M_1,\dots,M_{k-1})$ with each $M_t\in\mathcal M$, $M_t$ equal to $M^0_t$ on non-malleable entries, and $\sum_t c(M_t,M^0_t)\le B$. The social welfare of a tuple is $W(M)=R^\top M_{k-1}\cdots M_1D_1$, and $OPT$ is its maximum over $\mathcal F(B,M^0)$.

Algorithm 1 fixes $\varepsilon>0$, the budget grid $\mathcal B(\varepsilon)=\{n\varepsilon:n\in\mathbb N\}$, $B^\varepsilon=\max\{x\in\mathcal B(\varepsilon):x\le B\}$, and a finite $\varepsilon$-net $\mathcal D(\varepsilon)\subseteq\mathcal D$ in $\ell_1$ (every $D\in\mathcal D$ is within $\ell_1$ distance $\varepsilon$ of some element). Working backwards from the last layer, for each layer $t$, grid budget $B_{\ge t}\le B$ and net distribution $D_t$ (or $D_1$ itself at $t=1$), it solves Program (7): maximize $R^\top M(B_{\ge t+1},D_{t+1})M_tD_t$ over $M_t\in\mathcal M$ agreeing with $M^0_t$ off $E^t_{mal}$ with $c(M_t,M^0_t)\le B_{\ge t}-B_{\ge t+1}$, for every smaller grid budget $B_{\ge t+1}$ and every $D_{t+1}\in\mathcal D(\varepsilon)$, and stores the best product $M(B_{\ge t},D_t)=M(B_{\ge t+1},D_{t+1})M_t$. It returns $M(B^\varepsilon,D_1)$.

Formalization targets

Goal: Theorem 1 (p. 10)

For every instance, every $B\ge 0$, every $\varepsilon>0$ and every $\varepsilon$-net $\mathcal D(\varepsilon)$: Algorithm 1 has a run; every run returns a tuple $M\in\mathcal F(B,M^0)$ with

$$W(M)\ \ge\ OPT-3(k-1)\,\varepsilon\,\|R\|_\infty ;$$

and the algorithm solves at most $(k-1)(\lfloor B/\varepsilon\rfloor+1)^2|\mathcal D(\varepsilon)|^2$ instances of Program (7).

Milestones

1. Lemma 1 (p. 11): $\|MD-MD'\|_1\le\|D-D'\|_1$ for $M\in\mathcal M$, $D,D'\in\mathcal D$.
2. Corollary 2 (p. 12): $R^\top MD\ge R^\top MD'-\|R\|_\infty\varepsilon$ when $\|D-D'\|_1\le\varepsilon$.
3. The budget-saving matrix of the proof of Claim 1 (App. A.1, p. 25): from any admissible $M^*_t$ one obtains $M^\varepsilon_t$ with $c(M^\varepsilon_t,M^0_t)=\max(0,c(M^*_t,M^0_t)-\varepsilon)$ losing at most $\|R\|_\infty\varepsilon$ of reward.
4. Claim 1 (p. 8, social-welfare part): some solution with budgets in $\mathcal B(\varepsilon)$ has welfare $\ge OPT-(k-1)\varepsilon\|R\|_\infty$.
5. The induction invariant of the proof of Theorem 1 (p. 12): $R^\top M(B_{\ge t},D_t)D_t\ge OPT^\varepsilon-2(k-t)\varepsilon\|R\|_\infty$.
6. Claim 2 (p. 8, corrected size): an $\ell_1$ $\varepsilon$-net of $\mathcal D$ with at most $(\lceil 2w/\varepsilon\rceil+1)^{w-1}$ points.

Significance

Theorem 1 shows that, for networks of constant width, the welfare-maximizing intervention can be approximated to within an additive $\delta\|R\|_\infty$ in time polynomial in $k$, $B$ and $1/\delta$, even though the problem is non-convex in the matrices. The same dynamic program, run over population-wise distributions, gives the paper's FPTAS for the ex-post maximin objective (Theorem 2), and through a no-regret reduction for the ex-ante maximin objective (Lemma 2). The paper also shows that the width restriction cannot be removed: approximating the maximin objective is NP-hard for polynomial width.

The result is proved in the paper; to our knowledge none of it has been machine-checked. The formalization makes the algorithm itself a mathematical object (a run relation with arbitrary tie-breaking) and checks the guarantee for every run and every net. It also pins down two statements the paper gets slightly wrong: the running-time count of Theorem 1, whose proof omits one budget loop, and the net size of Claim 2, which fails for large $\varepsilon$; both are stated here in corrected form. Lemma 1, Corollary 2 and the simplex net are reusable for any Markov-chain or dynamic-programming result over distributions.

Difficulty

The welfare $R^\top M_{k-1}\cdots M_1D_1$ is multilinear but not concave in the tuple, so one cannot simply solve one convex program. Splitting the problem layer by layer requires knowing the distribution arriving at each layer, which ranges over a continuum; replacing it by a net point introduces an error at every layer, and the argument must show that these errors add up linearly rather than compound. A second source of error is the budget: the optimal split of $B$ across layers is generally not on the grid, and moving it onto the grid must cost little welfare at each layer even though the matrices interact multiplicatively. The bookkeeping that keeps the total loss at $3(k-1)\varepsilon\|R\|_\infty$ is where a careless formalization fails.

Formalization scope

The development lives in the namespace PipelineInterv.Welfare. Transitions are indexed by Fin K with $K=k-1$, 0-based; matrices are Matrix (Fin w) (Fin w) ℝ with M i j the probability of moving from j to i, and $\mathcal M$ is Mathlib's Matrix.colStochastic. The $\ell_1$ norm and $\|R\|_\infty$ are written out, never the default sup norm. The standing assumptions of §2 (left stochastic $M^0_t$, $D_1\in\mathcal D$, $R\ge 0$) are one predicate; the paper's without-loss-of-generality conventions ($D_1>0$, distinct rewards) are not imposed. $OPT$ is expressed as "for every feasible tuple", equivalent by Remark 3. Algorithm 1 is a relation on tables: a table is a run when every stored entry is the product of a smaller-budget entry and a Program (7)-feasible matrix that maximizes the objective over all such choices; ties are arbitrary. The net is any finite $\varepsilon$-net contained in $\mathcal D$, and the budget grid is cut at $B$.

The goal cannot be satisfied trivially: the run relation contains the optimality clause (without it any table of feasible matrices would be a run), the net is a finite set, and the goal asserts that a run exists, so the guarantee is never vacuous. The running-time clause is a count of Program (7) instances, not an asymptotic time bound; solving each instance is a linear program in $O(w^2)$ variables.

A complete development needs: ℓ1 contraction of column-stochastic matrices, the Hölder bound $|R^\top x|\le\|R\|_\infty\|x\|_1$, the existence of maximizers of a linear function over the compact Program (7) feasible set, an explicit grid net of the simplex, and the two inductions (over transitions for Claim 1, backwards over layers for the invariant). Proofs of the milestones, alternative arguments and lemmas about the suffix and prefix products are welcome.

Selected references

• E. R. Arunachaleswaran, S. Kannan, A. Roth, J. Ziani, Pipeline Interventions, arXiv:2002.06592v2, 2020; Mathematics of Operations Research, 2022. https://arxiv.org/abs/2002.06592
• S. Kannan, A. Roth, J. Ziani, Downstream effects of affirmative action, Proceedings of FAT* 2019, pp. 240–248.
• S. F. Way, D. B. Larremore, A. Clauset, Gender, productivity, and prestige in computer science faculty hiring networks, Proceedings of WWW 2016, pp. 1169–1179.

Motivation

Why do financially constrained firms charge different markups from otherwise similar firms? A firm can use a low price to attract customers today, but it may also need current cash to pay for production and avoid costly outside financing. Dou and Ji put these two incentives into a dynamic model in which the customer base affects future demand and cash holdings affect financing choices. Their SSRN working paper derives a compact expression for the resulting firm-level markup. This mission isolates that expression and the pricing calculations that support it.

The question matters for interpreting observed prices. A high price need not reflect only weak product-market competition: it may also reflect the firm's current valuation of liquidity relative to future customers. Conversely, a firm with a valuable opportunity to build a customer base may discount its product even when doing so reduces immediate operating profit. Proposition 3.1 of Dou and Ji, in the monopolistically competitive part of their model, states this trade-off through a single markup wedge. The paper separately analyzes a monopoly industry and connects the model to quantitative and empirical exercises; those results are outside this mission.

Setting

A firm's customer base $M_{i,t}$ measures the stock of customers attracted by firm $i$ at time $t$. The firm sets its own price $P_{i,t}>0$ while treating the industry price index $P_t>0$ as given. The industry's price elasticity is $\epsilon$, and the elasticity of substitution among firms' goods is $\eta$, with $1<\epsilon<\eta$. The firm's demand is

$$C_{i,t}=M_{i,t}(P_{i,t}/P_t)^{-\eta}P_t^{-\epsilon}.\tag{2.4}$$

Sales add to the customer base at rate $\beta$, while customers leave at rate $\rho$. Production uses rented capital: productivity $A>0$ and rental rate $R>0$ give marginal cost $R/A$. The markup $\Lambda_{i,t}$ is the ratio of the firm's price to this cost, $P_{i,t}/(R/A)$. Firm cash $W_{i,t}$ changes with operating profit and with its return net of a cash-carrying cost. The expected drifts per unit time used here are

$$g_M(P)=\beta M(P/P_t)^{-\eta}P_t^{-\epsilon}-\rho M,$$ $$g_W(P)=(P-R/A)P^{-\eta}P_t^{\eta-\epsilon}M+(r-\lambda)W.$$

Here $P$ is the firm's proposed price, and $M$ and $W$ are its current customer base and cash. The marginal value of customer base $\mu$ and marginal value of corporate liquidity $\nu$ weight those drifts in the price-dependent objective $H(P)=\mu g_M(P)+\nu g_W(P)$. The paper calls them Lagrangian multipliers of the respective state evolutions. The markup wedge is $\Omega=(\beta A/R)(\mu/\nu)$. Under the stated sign conditions, it is nonnegative. These objects come from the model and the appendix to Proposition 3.1.

Formalization targets

Optimal markup under monopolistic competition

The goal states that a positive price globally maximizes $H$ over positive prices exactly when its markup satisfies Proposition 3.1:

$$\Lambda(P)=\frac{\eta}{\eta-1}(1-\Omega),\qquad \Omega=\frac{\beta A}{R}\frac{\mu}{\nu}\ge0.\tag{3.1–3.2}$$

The equivalence includes existence and uniqueness of the positive maximizing price under $\Omega<1$. The goal keeps the wedge as a quantity computed from the firm's parameters and marginal values. It does not designate the formula itself as the definition of an optimal price.

Appendix calculations

Four milestones follow the printed sequence of Online Appendix A.1: the derivative of expected customer-base growth (A.2), the derivative of expected cash growth (A.4), the equivalence between the resulting stationary condition and the price formula (A.5)–(A.6), and the conversion of that price formula into the markup expression (A.8). The SSRN version is the citation basis; printed page 33 is PDF page 34. The goal remains the proposition rather than any one appendix equation.

Significance

The formula separates two channels in a firm's price decision. The factor $\eta/(\eta-1)$ is the familiar constant-elasticity markup when attracting customers has no additional value. The nonnegative wedge reduces this markup according to the customer-base value $\mu$ relative to the liquidity value $\nu$. It therefore supplies a precise interpretation of how the firm's financial position and its incentive to expand its customer base interact in pricing. This is the paper's stated “sufficient statistic” interpretation of the wedge, within its equilibrium model (Dou and Ji, Proposition 3.1).

The result is proved in the paper. The work here is to give its model quantities, derivative identities, stationary-price equation, and global optimal-price characterization machine-checkable Lean statements. The appendix equations are individually useful when formalizing other pricing results from the same model. The current mission statements carry sorry placeholders: building them checks their syntax and types, while the proofs remain for solvers.

Difficulty

A zero price derivative gives a candidate price, but by itself does not establish a global maximum among all admissible prices. The objective includes a negative power of price and has an open domain $P>0$, so its behavior as price approaches zero or becomes large matters. Its candidate price is positive only in the regime $\Omega<1$. The paper gives the stationary relation in Appendix A.1; a complete formal proof of the goal must connect that relation to the global optimization claim without assuming the answer as an input.

Formalization scope

Lean represents the paper's real-valued parameters in one Params structure and uses Real.rpow for demand powers. The predicates and functions concern one firm at one instant; firm and time indices are suppressed. The industry price index, customer base, cash balance, and marginal values are supplied as real numbers. Prices range over positive reals, and IsOptimalPrice means a global maximum of $H$ over that domain. The model records the expected deterministic drift per unit time. Brownian noise, the separate payout or equity-issuance control, the equilibrium price-index aggregator, and the full stochastic HJB state equation are outside the price comparison because they do not enter these displayed appendix derivatives when the index and controls are fixed.

The source states $\beta>0$ in the model but explicitly discusses $\beta=0$ after Proposition 3.1, so the standing predicate allows $\beta\ge0$. It also describes $\nu\ge1$ in the equilibrium discussion; the formal theorem uses the weaker mathematical condition $\nu>0$. It takes $\mu\ge0$ and, as implicit economic domain conditions, $A,R,P_t,M>0$. The added condition $\Omega<1$ makes the proposed optimal price positive and the global maximizer finite. The firm-price domain is $P>0$. These commitments should be read as the domain of the formal claim, rather than as an assertion that every parameter choice produces an equilibrium of the full stochastic model.

An optimal price is defined by maximizing the drifts-based objective, not by the markup identity or stationary-price formula. The definition module, derivative milestones, and a proof of the global characterization are all available work. The real-power calculus and maximization arguments can be reused for other constant-elasticity pricing problems.

Selected references

• W. W. Dou and Y. Ji, External Financing and Customer Capital: A Financial Theory of Markups, SSRN working paper 2574953, version of May 11, 2020; published in Management Science (2021). SSRN preprint; journal DOI.

Motivation

Investors pay for information, and the amount of information they produce changes over time. In periods when many investors are informed, more information becomes available, which makes being informed cheaper and attracts still more informed investors; when few are informed, the reverse happens. Glasserman, Mamaysky and Shen, Dynamic Information Regimes in Financial Markets (Management Science), build an overlapping-generations (OLG) asset market in which this feedback produces persistent information regimes, and use it to explain sudden price drops that occur without a change in fundamentals.

The paper extends the noisy rational-expectations framework of Grossman and Stiglitz (1980) and the OLG market of Allen, Morris and Shin (2006) with a state variable that tracks how much of the next dividend is knowable. Before regimes, price drops or information choice can be studied, the market stage must have an equilibrium for every possible fraction of informed investors. This mission formalizes that existence result.

Setting

Dividend. $D_{t+1} = (1-\rho)\bar D + \rho D_t + M_{t+1}$, with $\mu_D = (1-\rho)\bar D$ and normal innovations $M_{t+1}$ of variance $\sigma_M^2$. The innovation splits as $M_{t+1} = m_t + \theta_t + \epsilon_{t+1}$: $m_t$ is known only to informed investors, $\theta_t$ is public, and $\epsilon_{t+1}$ is unknowable at time $t$. Their variances are $\phi f_t\sigma_M^2$, $(1-\phi)f_t\sigma_M^2$ and $(1-f_t)\sigma_M^2$.

Information state. The fraction $f_t$ of knowable innovation lives on the grid $\mathcal D = \{0, 1/m, \dots, 1\}$ and evolves as

$$f_{t+1} = \Pi_{\mathcal D}\big(a_f + b_f\lambda(f_t) + \kappa_f(f_t - a_f) + \epsilon_{f,t+1}\big),$$

where $\Pi_{\mathcal D}$ clips to $[0,1]$ and rounds up to the grid, and $\lambda(f) \in [0,1]$ is the fraction informed in state $f$.

Investors. Each generation lives one period, invests at the gross riskless return $R > 1$ and chooses a demand $q$ for the risky asset by a mean-variance criterion with risk aversion $\gamma > 0$. The variance of next period's price enters through a conjectured variance $V_B(f)$. Informed investors see $m_t$; uninformed investors see only $f_t$, $\theta_t$, $D_t$ and the price $P_t$, and update about $m_t$ from the price. The supply of the asset is $\bar X + X_t$ with $\bar X > 0$ and $X_t$ normal of variance $\sigma_X^2$.

Equilibrium. A linear price process is

$$P_t = a(f_t) + b(f_t)m_t + g\theta_t - c(f_t)X_t + dD_t .$$

It clears the market if the optimal demands satisfy $\lambda q^I + (1-\lambda)q^U = \bar X + X_t$ in every state and for every realization. The conjecture $V_B$ is self-consistent if

$$V_B(f) = b(f)^2\phi f\sigma_M^2 + g^2(1-\phi)f\sigma_M^2 + c(f)^2\sigma_X^2\quad\text{for all } f.$$

A market equilibrium is a price process and a positive self-consistent conjecture with market clearing. In Lean these are Clears, SelfConsistent and MarketEquilibrium in InfoRegimes.MarketEq.Model.

Formalization targets

Goal: Proposition 4.1 (p. 22)

Write $d = \rho/(R-\rho)$. If $1 < R \le 1.2$ and

$$(1+d)\gamma\sigma_M\sigma_X = \frac{R\gamma\sigma_M\sigma_X}{R-\rho} \le 0.28,$$

then for every $\lambda : \mathcal D \to [0,1]$ a market equilibrium exists. The shock law of $\epsilon_f$, the coefficients $a_f, b_f, \kappa_f$ and the grid size are arbitrary.

Milestones

1. (B.4): the mean-variance demand is $q_N/(\gamma q_D)$.
2. Footnote 32: the posterior variance $\operatorname{var}(m\mid P) = (1-Kb)\operatorname{var}(m)$ behind (B.7)–(B.8).
3. (B.10): clearing forces $d = \rho/(R-\rho)$ and $g = 1/(R-\rho)$.
4. (B.12): clearing forces $b/c = \lambda(1+d)/(\gamma q^I_D)$, and $c = \gamma q^U_D/R$ when $\lambda = 0$.
5. (B.19)–(B.21): the intercept $a(\cdot)$ is $(1+d)\mu_D/(R-1)$ minus the discounted expected net profits.
6. Lemma 4.1: for every $V_B > 0$ and $\lambda$, a clearing linear price process with these $d, g$ exists.
7. The reduction of p. 22: the coefficients (B.13)–(B.18) clear the market, and a fixed point of the self-consistency map gives a market equilibrium.
8. Footnote 15: in the special case $f \equiv 0$, $\lambda \equiv 0$, self-consistency is a quadratic in $V_B$ with two positive roots under (27).

Significance

Proposition 4.1 makes the fraction informed a free input of the market stage. The paper's information equilibrium (Proposition 4.2), its two-regime dynamics and its price-drop analysis all take a market equilibrium for a given $\lambda$ as their starting point. Footnote 15 shows that equilibria need not be unique: even in the single-state case there is a low-variance and a high-variance equilibrium.

The result is proved in the paper's Electronic Companion (Section EC.2), which states more general parameter conditions. No machine-checked version exists. A formalization pins down exactly what "market equilibrium" means here: optimal demands with Bayesian updating from prices, clearing for all realizations, and self-consistency of the variance conjecture. It also yields reusable components: the mean-variance demand, the Gaussian signal-extraction identity, and a present-value identity for finite Markov chains.

Difficulty

Market clearing alone is linear algebra: for a fixed conjecture $V_B$, collecting terms determines the price coefficients, and the intercept solves a linear equation with a discounted stochastic matrix. Self-consistency is the hard part. The coefficients $b$ and $c$ depend on $V_B$ through the expected variances $q^I_D$, $q^U_D$ and the uninformed investors' signal extraction, so (26) is a nonlinear fixed-point equation for $V_B$ on the grid, coupled across states through the transition kernel. Footnote 15 shows that it can have several solutions, and that without a bound such as (27) it can have no real solution at all. The obvious approach, iterating the map from a starting conjecture, need not converge to anything without a contraction estimate, and the paper reports that the high-variance root is unstable.

Formalization scope

All quantities are real. The grid is Fin (m+1) with $m \ge 1$ and $f_i = i/m$. The standing assumptions are $R > 1$, $\sigma_M, \sigma_X, \gamma, \bar X > 0$ and $0 \le \phi \le 1$, plus the added bound $-1 < \rho < 1$: the paper never states the range of $\rho$, while $d$ and (27) need $\rho < R$. The page's $R \in [1, 1.2]$ is read with the standing $R > 1$ as $1 < R \le 1.2$; $1.2$ and $0.28$ are written as $6/5$ and $7/25$. The law of $\epsilon_f$ is an arbitrary probability measure, and transition probabilities are its values on preimage sets. Conditional expectations given $f_t$ are finite sums against this kernel at the current state's $\lambda$.

Demands are maximizers of the explicit mean-variance objectives, not closed-form formulas. Uninformed demand depends only on $(f_t, \theta_t, D_t, P_t)$, and the Gaussian posterior mean and variance (B.7)–(B.8) are written in closed form. Clearing is required for every realization $(m_t, \theta_t, X_t, D_t) \in \mathbb R^4$. A trivializing formalization is ruled out: MarketEquilibrium does not hard-wire $d$, $g$, $b$ or $c$, and it is not "the self-consistency map has a fixed point", which is milestone 7's hypothesis, not the goal.

Useful infrastructure: positivity and row sums of the transition kernel, continuity of the self-consistency map in $V_B$, and a fixed-point theorem on a box. Brouwer's theorem is not in Mathlib, but it is Proved on the platform as AGT.brouwer_fixed_point and Plasticity.Ext.Brouwer. Proofs of any milestone, and alternative routes to the goal, are welcome.

Not in this mission: Proposition 4.2 (existence of an endogenous fraction informed), the microfoundation of §3, and the numerical analysis of §§5–6.

Selected references

• P. Glasserman, H. Mamaysky, Y. Shen, Dynamic Information Regimes in Financial Markets, Management Science; SSRN version of October 17, 2023. https://ssrn.com/abstract=3324789 , DOI https://doi.org/10.1287/mnsc.2021.01213
• S. J. Grossman, J. E. Stiglitz, On the Impossibility of Informationally Efficient Markets, American Economic Review 70(3), 1980. https://www.jstor.org/stable/1805228
• F. Allen, S. Morris, H. S. Shin, Beauty Contests and Iterated Expectations in Asset Markets, Review of Financial Studies 19(3), 2006. https://doi.org/10.1093/rfs/hhj036
• M. Spiegel, Stock Price Volatility in a Multiple Security Overlapping Generations Model, Review of Financial Studies 11(2), 1998. https://doi.org/10.1093/rfs/11.2.419

Motivation

When social-distancing rules cap how many members of an organization may be physically present, a school, office or plant of $2K$ members can host only $K$ at a time. A common response is rotation: split the members into two fixed groups and alternate which group is on site. How often to alternate is a design choice, and it matters because an infection that enters one group spreads only while that group is active, and is detected only after a delay, when symptoms appear or tests are run.

Ely, Galeotti and Steiner (2021) model this choice and show that the optimal rotation is extreme: either the groups alternate as often as possible, or one group is kept active throughout. Which extreme is optimal is decided by a single comparison between the organization's reaction time and the time a logistic epidemic needs to infect half a group. The model is a small continuous-time control problem with a switching activity coefficient, a logistic state equation and an expectation over the infection date; its main theorem is an exact optimality statement rather than an approximation.

Setting

Two groups $i \in \{0,1\}$ each have measure $K > 1$. A rotation schedule is a pair of measurable functions $r(0,\cdot), r(1,\cdot)$ with values in $[0,1]$ and $r(0,t) + r(1,t) = 1$ for every time $t$; $r(i,t)$ is the share of time group $i$ is active around $t$. The frequent rotation is $r(i,t) = 1/2$ for both groups and all $t$ (the limit of alternating very often); activating group $i$ throughout is $r(i,t) = 1$, $r(1-i,t) = 0$.

At a random time $t^* \ge 0$ with an arbitrary law $\mu$, one member of a group $\omega$ becomes infected; $\omega$ is $0$ or $1$ with probability one half each, independently of $t^*$. The prevalence $p_t$ of the infected group starts at $p_{t^*} = 1/K$ and follows the logistic equation

$$\dot p_t = \gamma\, r(\omega,t)\, p_t (1 - p_t), \qquad t \ge t^*, \tag{2}$$

with transmission rate $\gamma > 0$; the other group stays uninfected. The organization reacts at time $t^* + R$, where $R \ge 0$ is the reaction delay, and the rotation problem is

$$\min_r\ \mathrm E\, p^\omega_{t^*+R}(\omega), \tag{P1}$$

the expectation being over $t^*$ and $\omega$.

Two derived objects organize the analysis. The exposure time $\tau = \int_{t^*}^{t^*+R} r(\omega,t)\,dt$ is how long the infected group was active before the reaction. The loss and the half-infection time are

$$\ell(t) = \frac{e^{\gamma(t-b)}}{1+e^{\gamma(t-b)}}, \qquad b = \frac1\gamma \ln(K-1);$$

$\ell(t)$ is the prevalence after $t$ units of uninterrupted spread, and $b$ is the time at which it reaches one half.

Formalization targets

Goal: Proposition 1 (p. 10)

$$\frac R2 < b \;\Longrightarrow\; r(0,t) = r(1,t) = \tfrac12 \text{ solves (P1)}, \qquad \frac R2 > b \;\Longrightarrow\; r(i,t) = 1 \text{ for all } t \text{ solves (P1)}, \ i \in \{0,1\}.$$

Optimality is over all rotation schedules and holds for every law of $t^*$ on $[0,\infty)$. The boundary case $R/2 = b$ is not part of the statement.

Milestones, in the paper's order

1. $\ell$ solves $\dot\ell = \gamma \ell(1-\ell)$ with $\ell(0) = 1/K$ (§2.1, p. 7).
2. $\ell(b) = 1/2$; $\ell$ is convex below $b$ and concave above (§2.1, p. 7).
3. Lemma 1 (p. 7): the prevalence at the reaction time is $p^\omega_{t^*+R}(\omega) = \ell(\tau)$.
4. Lemma 2 (p. 8, in corrected form): $\mathrm E\,\tau = R/2$ and $\Pr(\tau \le T) = \Pr(\tau \ge R-T)$.
5. The exposure times of the two groups sum to $R$, and $\mathrm E\,\ell(\tau) = \tfrac12\mathrm E[\ell(\tau) + \ell(R-\tau)]$ (p. 8).
6. Lemma 3 (pp. 9–10): $\ell(\tau) + \ell(R-\tau)$ is U-shaped around $R/2$ if $R/2 < b$, hump-shaped if $R/2 > b$.
7. The relaxed problem (P2), $\min_F \mathrm E_F[\ell(\tau) + \ell(R-\tau)]$ subject to $\mathrm E_F \tau = R/2$ over laws on $[0,R]$, is solved by the point mass at $R/2$ when $R/2 < b$ and by $\tfrac12\delta_0 + \tfrac12\delta_R$ when $R/2 > b$ (proof of Proposition 1, pp. 10–11).
8. The frequent rotation gives expected terminal prevalence $\ell(R/2)$, and activating one group gives $(\ell(0) + \ell(R))/2$ (p. 11).

Significance

The result turns a control problem over all measurable switching schedules into a comparison of two numbers, $R/2$ and $b$. It says that intermediate rotation frequencies are never strictly better than both extremes, and it identifies the curvature of the logistic curve over the reaction window as the quantity that decides between them: frequent rotation equalizes the two groups' exposure and so insures against exposure-time risk, which is worth doing only while prevalence is still in its convex phase. The paper's Corollary 1 (comparative statics in $R$, $\gamma$ and $K$) follows from it.

The proposition is proved in the paper, in a few lines that rely on informal steps: solving (2) by a change of variable, the symmetry of the exposure-time distribution, and the "standard concavification argument" for (P2). To our knowledge none of it has been machine-checked. A formalization makes each step precise for measurable schedules, for which (2) holds only almost everywhere, and records one correction: the symmetry identity of Lemma 2 as printed, $F(\tau) = 1 - F(R-\tau)$, is false at atoms of the distribution, and the mission states the form the proof actually establishes.

Difficulty

The obvious argument treats (2) as a classical differential equation and substitutes $\hat t = \int r$. For a merely measurable schedule this needs absolute continuity, a chain rule for a Lipschitz time change, and uniqueness of solutions of a Carathéodory equation; Lemma 1 has to supply all three, including that every solution stays the composite $\ell(\int r)$. The second difficulty is that (P1) optimizes over schedules, not over distributions: the reduction to (P2) uses only the mean and the symmetry of $\tau$, and the optimum of (P2) must then be shown to be attained by an actual schedule. Lemma 3 holds on all of $\mathbb R$, but the solution of (P2) in the hump-shaped case uses that exposure times lie in $[0,R]$: off that interval $\ell(\tau) + \ell(R-\tau)$ falls below its endpoint values.

Formalization scope

All quantities are real numbers. The parameters $\gamma > 0$, $K > 1$, $R \ge 0$ are bundled as standing assumptions; $R \ge 0$ is added (a delay). Groups are Fin 2. Schedules are measurable functions on all of $\mathbb R$ satisfying $r(i,t) \in [0,1]$ and $r(0,t) + r(1,t) = 1$ at every $t$; the page's domain is $\mathbb R_+$, and the two readings agree for (P1) because $t^* \ge 0$. The law $\mu$ of $t^*$ is any probability measure on $\mathbb R$ with $\mu((-\infty,0)) = 0$, and the objective is $\tfrac12\sum_\omega \int p^{\omega,t^*}_{t^*+R}\,d\mu(t^*)$.

Equation (2) is used in integral form: a prevalence path is continuous and $[0,1]$-valued on $[t^*,\infty)$ and satisfies $p_t = 1/K + \int_{t^*}^t \gamma r(\omega,s) p_s(1-p_s)\,ds$; this admits the paper's periodic schedules, which have no classical derivative. A schedule is optimal when it has a prevalence family (one path for every $\omega$ and every $t^* \ge 0$) and, for every such family, its objective is at most that of any schedule with any family; the existence clause keeps optimality from holding vacuously. Terminal prevalence is the value of the solution of (2), never defined as $\ell(\tau)$: that identification is Lemma 1 and is part of the work. Lemma 2 is stated as $\Pr(\tau \le T) = \Pr(\tau \ge R-T)$ for all real $T$, not as the printed distribution-function identity.

A complete development needs: the logistic function and its derivative; FTC and change of variables for absolutely continuous functions; a Grönwall-type uniqueness argument for the integral equation; and an elementary concavification bound for a function that is monotone on each side of $R/2$. The logistic and uniqueness parts are reusable beyond this mission. Proofs of any milestone, and alternative routes to the goal, are welcome.

Not formalized here: Corollary 1 (p. 11), the numerical calibration remark of p. 11, and §4 on mixing between groups (Lemma 4, Propositions 2 and 3), which is a different model.

Selected references

• J. Ely, A. Galeotti, J. Steiner, Rotation as Contagion Mitigation, Management Science, 2021; cited from the authors' working paper of 29 October 2020. https://doi.org/10.1287/mnsc.2020.3910
• E. Kamenica, M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011 (the concavification technique used for (P2)). https://doi.org/10.1257/aer.101.6.2590