All missions

Motivation

Since Naor's 1969 model of queue joining, the literature on pricing congestible services has assumed that a customer judges a time-consuming service by its full price: the money price $r$ plus a constant multiple $\eta$ of the time commitment $\delta$, $r+\eta\delta$. Revenue-maximizing and welfare-maximizing prices for queues, priority schemes and capacity choices (Afèche and Mendelson 2004; Allon and Federgruen 2007; Nazerzadeh and Randhawa 2018; Gurvich et al. 2019) are all derived under this assumption, usually with $\eta$ identified with a customer type such as a wage. Allon and Federgruen describe it as "tantamount to assuming that all consumers assign a specific cost value to their waiting time and that the cost of waiting is simply proportional to the total waiting time."

Li, Lariviere and Bassamboo ask when this assumption is actually implied by a consumer's own optimization. They embed the purchase decision in a Becker (1965) style allocation of time and money, and show that the full-price model is exact for consumers who choose freely how long to work at a constant wage (gig workers), while it fails for shift workers. The result gives the full-price model a microfoundation and identifies the waiting cost $\eta$ with the wage $\theta$.

Setting

A consumer has $T$ units of time per day. She chooses a plan $(t_l,c_l,t_w,c_O)$: leisure time $t_l$, leisure consumption $c_l$, work time $t_w$ and overhead expenditure $c_O$, and a purchase decision $y\in\{0,1\}$ for a discrete service with value $V$, price $r$ and time commitment $\delta$. Her problem (PC) is

$$\max\ U(t_l,c_l)+Vy\quad\text{s.t.}\quad t_w+O(c_O)+t_l+\delta y\le T,\quad c_O+c_l+ry\le \Pi_\theta(t_w),\quad t_l,c_l,t_w,c_O\ge 0 .$$

Here $U$ (StandingAssumptions) is continuous, non-decreasing and concave in each argument on the closed quadrant with $U(0,c_l),U(t_l,0)\ge0$; $O(c_O)$, the time spent on chores when $c_O$ is spent to reduce them, is decreasing and strictly convex; $\Pi_\theta$ is the compensation function. For gig workers it is linear, $\Pi_\theta(t_w)=\theta t_w$ (linearCompensation), with wage $\theta>0$.

A pair $(r,\delta)$ is feasible (IsFeasiblePair) when the buyer's problem ($y=1$) has a feasible plan (IsFeasiblePlan). The buyer's leisure utility $u^B(\theta,r,\delta)$ (buyerUtility) is the supremum of $U(t_l,c_l)$ over the buyer's feasible plans. The consumer is a full-price decision-maker (Definition 1, IsFullPriceDecisionMaker) if there is $\eta>0$ with $u^B(\theta,r,\delta)=u^B(\theta,\hat r,\hat\delta)$ whenever $(\hat r,\hat\delta)$ is feasible and $r+\eta\delta=\hat r+\eta\hat\delta$. An optimal plan (IsOptimalPlan) of the buyer ($j=B$, $y=1$) or the non-buyer ($j=NB$, $y=0$) maximizes $U(t_l,c_l)$ over the feasible plans of that problem. The marginal rate of substitution of time for money (mrs) is

$$\chi(t_l,c_l)=\frac{\partial U/\partial t_l}{\partial U/\partial c_l}.$$

Formalization targets

Goal: Proposition 1 (p.8)

For $\theta>0$ and $\Pi_\theta(t_w)=\theta t_w$:

1. the consumer is a full-price decision-maker;
2. with $\eta=\theta$: for all $r,\delta,\hat r,\hat\delta\ge0$ with $(\hat r,\hat\delta)$ feasible,

$$r+\theta\delta=\hat r+\theta\hat\delta\ \Longrightarrow\ u^B(\theta,r,\delta)=u^B(\theta,\hat r,\hat\delta);$$

3. at every optimal plan of the buyer (any $r,\delta\ge0$) and of the non-buyer with $t_l>0$, $c_l>0$, at which $U$ is differentiable with $\partial U/\partial c_l\ne0$,

$$\chi(t^j_l,c^j_l)=\theta,\qquad j\in\{NB,B\}.$$

Milestones: Lemma 4 (p.32)

Part 1 (buyer) and part 2 (non-buyer): at an optimal plan where $U$ is differentiable with $\partial U/\partial c_l\ne0$, both constraints bind; if moreover $t_l>0$ and $c_l>0$, then $\chi=\theta$ at the paper's point $(T-t^j_w-O(c^j_O)-\delta y,\ \theta t^j_w-c^j_O-ry)$; and $O'(c^j_O)=-1/\theta$ whenever $c^j_O>0$ and $O$ is differentiable there.

Significance

The proposition says that, for gig workers, the purchase decision depends on $(r,\delta)$ only through $r+\theta\delta$: the iso-utility curves in the $(r,\delta)$ plane are parallel lines of slope $\theta$. This is exactly the structure that the queueing-pricing literature assumes, with waiting cost per unit of time equal to the wage (Remark 1 of the paper recovers the standard model $v(\theta)-r-\theta\delta$ from it). The paper's later results (Lemma 2, Proposition 2, §4) show that shift workers are not full-price decision-makers and that pricing them as if they were loses revenue; Proposition 1 is the benchmark those comparisons are measured against.

The result is proved in the paper, not formalized anywhere. The mission adds a machine-checked version of the model and of the proposition, with a corrected first-order clause: the paper states $\chi=\theta$ at every optimum, but at corner optima ($t_l=0$ or $c_l=0$) it is false, and $O'(c_O)=-1/\theta$ also needs $c_O>0$. The formal statement carries exactly these interiority hypotheses, each only on the equation that needs it.

Difficulty

The full-price part is an exact change of variables, but the obvious one fails: substituting $t_w$ from the time constraint gives a set that seems to depend on $r$ and $\delta$ separately, and the sign constraint $t_w\ge0$ must be shown never to bind for non-negative prices (with negative prices it does bind, and the property fails). The supremum has to be compared as a supremum: attainment is not available, since $O$ is not assumed continuous.

The first-order part requires care that the paper skips. An optimum of (PC) is a maximizer of a constrained problem, not of the paper's reduced unconstrained function; one must first show that both constraints bind at an interior optimum where $\partial U/\partial c_l\ne0$, then perturb along feasible curves on which the reduced objective is differentiable, which uses only differentiability of $U$ at one point and of $O$ at one point.

Formalization scope

All quantities are real numbers. $U$ is a function on $\mathbb R\times\mathbb R$ with all assumptions imposed on the closed quadrant; "concave in both arguments" is read as concave in each argument separately (the weaker reading). The purchase decision is a real $y$ entering (PC) as $\delta y$ and $ry$, with $y\in\{0,1\}$ imposed where used. Feasibility of $(r,\delta)$ refers to the buyer's problem. $u^B$ is a supremum in EReal, so infeasible pairs give $-\infty$ rather than a junk value. Prices and time commitments are non-negative throughout. An optimal plan is a maximizer of $U$ over all four variables with $y$ fixed; binding constraints are a conclusion, never part of the definition. $\chi$ is computed from the Fréchet derivative of $U$, and every statement about it assumes differentiability and $\partial U/\partial c_l\ne0$ at the point, so neither fderiv's junk value nor division by zero can make a conclusion true.

A trivializing formalization would define $u^B$ or feasibility through the full price $r+\theta\delta$, or define an optimal plan as one satisfying the first-order conditions; neither is done here: $u^B$ is the supremum over plans satisfying the two constraints of (PC) literally.

A complete development needs elementary real analysis only: supremum manipulation in EReal, one-variable derivatives of compositions along curves, and the vanishing derivative at a local maximum. The time-allocation model is new to the platform and is reusable for the paper's shift-pay results (Lemma 2, Proposition 2). Proofs of Lemma 4 and of Proposition 1 are welcome, as are formal versions of the paper's shift-pay results.

Selected references

• S. Li, M. A. Lariviere, A. Bassamboo, Is Full Price the Full Story When Consumers Have Time and Budget Constraints?, SSRN 4223388 (2022); Manufacturing & Service Operations Management (2023). https://ssrn.com/abstract=4223388, https://doi.org/10.1287/msom.2022.0357
• P. Naor, The Regulation of Queue Size by Levying Tolls, Econometrica 37(1), 1969. https://doi.org/10.2307/1909200
• G. S. Becker, A Theory of the Allocation of Time, The Economic Journal 75(299), 1965. https://doi.org/10.2307/2228949
• G. Allon, A. Federgruen, Competition in Service Industries, Operations Research 55(1), 2007. https://doi.org/10.1287/opre.1060.0335
• P. Afèche, H. Mendelson, Pricing and Priority Auctions in Queueing Systems with a Generalized Delay Cost Structure, Management Science 50(7), 2004. https://doi.org/10.1287/mnsc.1040.0230

Motivation

Many dynamic programs are solved faster after the Bellman equation has been rewritten. The Q-factor form of reinforcement learning moves the maximization inside an expectation over state-action pairs; Rust's expected value function for discrete choice models (Rust 1987) integrates out the next state before maximizing; optimal stopping problems are routinely solved through a continuation value instead of the value function. Each such transformation changes the space on which fixed-point iteration runs, often to a lower-dimensional one, and each comes with its own ad hoc argument that the transformed equation still yields optimal policies.

Ma and Stachurski (arXiv:1811.01940v2, published in Operations Research in 2021) give one abstract framework covering all of these transformations, the plan factorization, and state conditions under which a transformed Bellman equation keeps its link to optimality. The framework builds on the abstract dynamic programming of Bertsekas (Abstract Dynamic Programming, Athena Scientific, 2013), and applies to models with recursive or risk-sensitive preferences, where the standard theory does not apply directly.

Setting

A dynamic program consists of a nonempty state space $\mathsf X$, a nonempty action space $\mathsf A$, a nonempty-valued feasible correspondence $\Gamma$ with state-action pairs $\mathsf F=\{(x,a): a\in\Gamma(x)\}$, a set $\mathcal V\subseteq\mathbb R^{\mathsf X}$ of candidate value functions, and a state-action aggregator $H:\mathsf F\times\mathcal V\to\mathbb R\cup\{-\infty\}$. The Bellman operator is $Tv(x)=\sup_{a\in\Gamma(x)}H(x,a,v)$.

A feasible policy is a selection $\sigma(x)\in\Gamma(x)$ satisfying a regularity condition; $\Sigma$ is the set of feasible policies. Given $v$, $\sigma$ is $v$-greedy if $H(x,\sigma(x),v)=Tv(x)$ for all $x$. Assumption 2.1 fixes a set $\mathbb V\subseteq\mathcal V$ that $T$ maps into itself and on which greedy policies exist. Assumption 2.2 asks that each $\sigma\in\Sigma$ have exactly one $\sigma$-value function $v_\sigma\in\mathcal V$, $v_\sigma(x)=H(x,\sigma(x),v_\sigma)$. The value function is $v^*=\sup_{\sigma}v_\sigma$, and $\sigma$ is optimal if $v_\sigma=v^*$.

A plan factorization is a pair $(W_0,W_1)$ with $W_1W_0v=H(\cdot,\cdot,v)$ on $\mathsf F$ for every $v\in\mathcal V$. With $Mh(x)=\sup_{a\in\Gamma(x)}h(x,a)$ and $M_\sigma h(x)=h(x,\sigma(x))$ this gives $T=MW_1W_0$. Rotating the cycle gives the refactored Bellman operator $S=W_0MW_1$ on $\mathbb G=W_0\mathbb V$, and the refactored $\sigma$-value operators $S_\sigma=W_0M_\sigma W_1$ on $\mathcal G=W_0\mathcal V$. The fixed point $g_\sigma$ of $S_\sigma$ is the refactored $\sigma$-value function, $g^*=\sup_\sigma g_\sigma$ is the refactored value function, and $\sigma$ is $g$-greedy if $M_\sigma W_1g=MW_1g$.

Formalization targets

Goal: Theorem 3.3

Let $\tau$ be a Hausdorff topology on $\mathcal G$ under which the pointwise order is closed. If $W_0$ and $W_1$ are monotone, $S$ is asymptotically stable on $\mathbb G$ (a unique fixed point to which all iterates converge under $\tau$) and every $S_\sigma$ is asymptotically stable on $\mathcal G$, then

$$g^*\in\mathbb G,\qquad g^*=Sg^*\ \text{uniquely in }\mathbb G,\qquad S^kg\xrightarrow{\ \tau\ }g^*\ \ (g\in\mathbb G),$$

an optimal policy exists, and a feasible policy is optimal if and only if it is $g^*$-greedy.

Milestones

1. Lemmas 6.1–6.2: fixed points, unique fixed points and iterates pass around a cycle of three maps $\tau_0,\tau_1,\tau_2$.
2. Proposition 2.3: $S_\sigma$ has a unique fixed point in $\mathcal G$ iff $T_\sigma$ has one in $\mathcal V$, and then $g_\sigma=W_0v_\sigma$, $v_\sigma=M_\sigma W_1g_\sigma$.
3. Display (19): $M_\sigma h\le Mh$.
4. Theorem 3.1: $v^*$ solves the Bellman equation in some $\mathbb V$ iff the principle of optimality holds and an optimal policy exists.
5. Theorem 3.2: for monotone $W_0,W_1$, $g^*\in\mathbb G$ with $Sg^*=g^*$ iff $v^*\in\mathbb V$ with $Tv^*=v^*$; then $g^*=W_0v^*$, optimal policies exist, and optimal $\iff$ $g^*$-greedy $\iff$ $v^*$-greedy.
6. Existence of a $g$-greedy policy for every $g\in\mathbb G$ (p.14), and monotonicity of $S_\sigma$ on $\mathcal G$ (p.28).

Significance

Theorem 3.3 is a sufficient condition for computing with the refactored equation: it says that value iteration with $S$ converges to the refactored value function and that a policy read off from $g^*$ is optimal, without ever computing $v^*$. The paper's applications (consumer bankruptcy, optimal stopping) use it to replace iteration over state functions by iteration over a smaller space and report large speed gains; Theorem 3.6 on refactored optimistic policy iteration builds on it.

All results are proved in the paper. No machine-checked version exists: related Prove2Me results cover finite MDPs (SuttonBartoRL.FiniteMDP.bellman_optimality, FoundationsRL.RLBasics.bellman_optimality) and Bertsekas- or Denardo-style abstract models with monotone or contracting $H$ (MonotoneDP.Decrease.prop6_bellman_equation, DenardoDP.NStage.theorem4, BertsekasShreve.Generalized.prop6_4_contraction_fixed_point). This mission formalizes the plan-factorization theory itself, under the paper's weak assumptions: no monotonicity of $H$, no contraction, arbitrary state and action sets.

Difficulty

The monotonicity hypothesis is where a naive transfer argument fails. Lemma 6.1 moves fixed points between $T$ and $S$ without any order structure, so one might expect $g^*$ and $\hat g=W_0v^*$ to coincide in general. They do not: the paper's Section 6.4 shows dynamic programs with $\hat g\ne g^*$, with $Tv^*=v^*$ but $Sg^*\ne g^*$, and with the converse. The proof of Theorem 3.2 compares $g_\sigma=W_0v_\sigma$ with $W_0v^*$ and $MW_1g_\sigma$ with $MW_1g^*$, which needs monotonicity of $W_0$ at every $v_\sigma\in\mathcal V$ and of $W_1$ at every $g_\sigma\in\mathcal G$, not only on $\mathbb V$ and $\mathbb G$. Theorem 3.3 then needs a limit argument: $\bar g\ge S_\sigma^k\bar g$ for all $k$ passes to $\bar g\ge g_\sigma$ only because the order is closed under $\tau$, and the iterates $S_\sigma^k\bar g$ leave $\mathbb G$.

Formalization scope

• The dynamic program is the structure DPDeconstructed.DynProg X A with arbitrary types X, A (no finiteness, no measurability), Γ : X → Set A, 𝒱 : Set (X → ℝ), and H valued in EReal with H ≠ ⊤ on $\mathsf F\times\mathcal V$. $\mathsf F$ is a subtype of X × A; feasible policies form a subtype of X → A.
• $T$, $M$, $v^*$ and $g^*$ are suprema in EReal. "$v^*\in\mathbb V$" and "$g^*\in\mathbb G$" mean that a real function in $\mathbb V$ (resp. $\mathbb G$) equals $v^*$ (resp. $g^*$) pointwise. $S$ applies toReal to $MW_1g$, which is real on $\mathbb G$; $S$ is only applied to elements of $\mathbb G$.
• "Monotone" means MonotoneOn W₀ 𝒱 and MonotoneOn W₁ 𝒢. This corrects the paper, whose p.14 takes monotonicity on $\mathbb V$, $\mathbb G$ and $\mathbb H$: on those sets alone Theorems 3.2 and 3.3 are false (a one-state counterexample is recorded in the items), and the paper's own proofs use the wider domains.
• $g_\sigma$ is defined as the unique fixed point of $S_\sigma$ in $\mathcal G$, not as $W_0v_\sigma$, and $g^*$ as the supremum of the $g_\sigma$; the identity $g^*=W_0v^*$ is a conclusion of Theorem 3.2, not part of a definition.
• $\tau$ is any topology on the subtype $\mathcal G$ that is Hausdorff and has a closed order graph in $\mathcal G\times\mathcal G$; asymptotic stability on $\mathbb G$ uses the subspace topology. A proved sanity instance (one state, two actions, Q-factor factorization, product topology) satisfies every hypothesis of the goal, so the goal is not vacuous.
• Lemmas 6.1–6.2 are stated for an arbitrary triple of maps at index $0$, which covers the paper's three indices by rotation.

Proofs of the milestones in any order are welcome, as are the companion results not in this mission (Propositions 2.1–2.2, Proposition 3.4's contraction criterion, Theorems 3.5–3.6). The rotation lemmas and the abstract dynamic program are reusable for any transformed Bellman equation.

Selected references

• Q. Ma and J. Stachurski, Dynamic Programming Deconstructed: Transformations of the Bellman Equation and Computational Efficiency, arXiv:1811.01940v2, 2019; Operations Research, 2021. https://arxiv.org/abs/1811.01940
• D. P. Bertsekas, Abstract Dynamic Programming, Athena Scientific, 2013 (book; no DOI).
• J. Rust, Optimal Replacement of GMC Bus Engines: An Empirical Model of Harold Zurcher, Econometrica 55(5), 1987. https://doi.org/10.2307/1911259

Motivation

A brand-name product sold through a supplier and a retailer suffers from double marginalization: each firm adds its own margin, so the retail price is too high and both firms earn less than an integrated firm would. Anand, Anupindi and Bassok (Management Science 2008) showed that, in a two-period channel where the supplier sets each period's wholesale price at the start of that period, the retailer buys more than she sells in period 1 and carries the surplus forward. This strategic inventory is carried not to meet demand but to weaken the supplier's period-2 pricing power, and it raises the supplier's profit as well. Without competitors it exists exactly when the unit holding cost satisfies $h<1/4$.

Successful products attract copycats: lower-quality imitations that enter after the brand has proven itself (Pun and DeYong, MSOM 2017). Jin, Wu and Chen (SSRN 3826955, 2023; MSOM 2023) ask what copycat entry does to strategic inventory. Their Proposition 2 answers it with a closed-form subgame-perfect equilibrium: copycats lower the holding-cost cutoff below which strategic inventory survives, and they remove it entirely once their quality is high enough.

Timeline: Anand et al. (2008) solve the channel without copycats (cutoff $h<1/4$, dynamic contract only). Jin, Wu and Chen (2023) add a Stackelberg copycat entrant in period 2 and obtain the cutoff $h_1(\beta)$ of this mission.

Setting

There are two selling periods. In each, a unit mass of short-lived customers arrives; a customer's valuation $\theta$ of the brand-name product is uniform on $[0,1]$, and each buys at most one unit, in its own period. In period 1 the brand is alone: a customer buys iff $\theta\ge p_1$. In period 2 copycats enter, and a customer values the copycat at $\beta\theta$, with copycat quality $0\le\beta<1$; she buys the brand iff $\theta-p_2\ge 0$ and $\theta-p_2\ge\beta\theta-p_C$, and the copycat iff $\beta\theta-p_C\ge 0$ and $\beta\theta-p_C>\theta-p_2$. Demands $D_1$, $D_2$, $D_C$ are the Lebesgue measures of these sets of $\theta$.

The supplier charges wholesale prices $(w_1,w_2)$. The retailer orders $(q_1,q_2)$, sets prices $(p_1,p_2)$, sells $s_1=\min(q_1,D_1)$, carries the inventory $I=q_1-s_1$ at unit cost $h$, and sells $s_2=\min(I+q_2,D_2)$; the copycats sell $s_C=D_C$. Profits are $\pi_S=w_1q_1+w_2q_2$, $\pi_R=p_1s_1+p_2s_2-w_1q_1-w_2q_2-hI$ and $\pi_C=p_Cs_C$. There is no network externality ($\gamma=0$).

Two contracts fix the move order. Under the commitment contract the supplier announces $(w_1,w_2)$, the retailer chooses $(q_1,q_2,p_1,p_2)$, and the copycats, seeing $p_2$, choose $p_C$. Under the dynamic contract the supplier announces $w_1$, the retailer chooses $(q_1,p_1)$, the supplier, seeing $q_1$ and $p_1$, announces $w_2$, the retailer chooses $(q_2,p_2)$, and the copycats choose $p_C$. The solution concept is subgame-perfect equilibrium (SPE). The benchmark $h=\infty$ means that period-1 leftovers cannot be carried.

Formalization targets

Goal: Proposition 2

With $\beta^*=(\sqrt{73}-5)/6\approx0.5907$ and

$$h_1(\beta)=\frac{1-\beta}{(2-\beta)(4-3\beta)}\Bigl(2-\beta-\frac{\beta}{2}\sqrt{\frac{17-13\beta}{1-\beta}}\Bigr),$$

for every $0\le\beta<1$ and $h\ge0$: under the commitment contract an SPE exists and every SPE has the Table 1 outcome; under the dynamic contract an SPE exists, and every SPE has the Table 2 outcome with $I>0$ if $\beta<\beta^*$ and $h<h_1(\beta)$, and the Table 1 outcome with $I=0$ if $\beta>\beta^*$ or $h>h_1(\beta)$; on the boundary $h=h_1(\beta)$ both outcomes occur. Moreover $h_1>0$ on $[0,\beta^*)$ and $h_1$ is strictly decreasing on $[0,\beta^*]$.

Milestones

1. Proposition 1: with $h=\infty$ both contracts give Table 1.
2. Proposition 2(i): the commitment contract gives Table 1 for every finite $h$.
3. The cutoff clause: $h_1>0$ below $\beta^*$, strictly decreasing on $[0,\beta^*]$.
4. §3.1: the supplier's equilibrium profit is continuous in $(\beta,h)$, and his two strategies give equal profit at $h=h_1$.
5. Condition I: the Table 2 equilibrium with inventory.
6. Condition II: the Table 1 equilibrium without inventory.

Three rows of the printed Table 2 are corrected. The $h$-term of $q_2$ has the wrong sign: the table's own rows give $q_2=s_2-I$, and at $\beta=0$, $h=1/10$ the printed value is $5/34$ against $7/34$. The rows $s_C$ and $\pi_C$ are inconsistent with the table's own $p_2$ and $p_C$: the copycat demand there is $p_2/(2(1-\beta))$, and $\pi_C$ must equal $p_Cs_C$. At $(\beta,h)=(3/10,1/20)$ the printed $s_C\approx0.389$ and $\pi_C\approx0.0311$, against $0.419$ and $0.0369$. The corrected rows agree with Table 1's identities and with Anand et al. at $\beta=0$.

Significance

The result shows that external competition reaches inside the channel. Copycat entry lowers the brand's period-2 demand, which weakens the retailer's reason to hold inventory against the supplier: the range of holding costs with strategic inventory shrinks as $\beta$ grows and is empty for $\beta\ge\beta^*$. At the cutoff the supplier switches from tolerating inventory to pricing it away. His profit is continuous across the switch, while the retailer's profit jumps down. Under the commitment contract nothing of this happens for any $h$. These facts are the basis of the paper's contract comparisons.

The paper states the result with proofs in an online supplement, which this mission does not use. Nothing in it has been formalized. The mission produces a machine-checked equilibrium analysis of a two-period vertical channel with inventory carry-over and a Stackelberg entrant, from the customer model up.

Difficulty

Each subgame is elementary, but the equilibrium must hold at every history, including off-path ones: large inventories, zero prices, retailer stock-outs. The copycat's best response $p_C=\beta p_2/2$ must be derived from the demand sets before the retailer's period-2 problem becomes a linear-quadratic program. The supplier's period-1 problem is not concave: his reduced profit in $w_1$ has a concave piece with inventory and a concave piece without, meeting at a convex kink. The global maximum is a comparison of two local maxima, and $h_1$ is the root of the resulting quadratic indifference equation. The naive plan of solving the first-order conditions once yields only Table 2 and misses the switch, and the tie at $h=h_1$ (including the point $\beta=\beta^*$, $h=0$) admits two equilibria. Uniqueness of the outcome has to be proved over all equilibria, not only for one constructed profile.

Formalization scope

The Lean development is in the namespace CopycatSI. Model defines the demands as volume of subsets of $[0,1]$ (as reals), sales, inventory, holding cost and profits; Holding.infinite is the paper's $h=\infty$. Game defines strategy profiles of both contracts as functions of observed histories, IsSPE (optimality at every history), and the on-path outcome. ClosedForms defines $\beta^*$, $h_1$ and the predicates MatchesTable1, MatchesTable2. The tables appear only as right-hand sides; equilibria are never defined by them.

Conventions: $\gamma=0$ throughout; zero production costs; the copycats observe $p_2$ only, and their demand is not rationed by the retailer's stock; prices and orders are non-negative; customers indifferent between the products buy the brand (a null set). The copycat rows are asserted for $\beta>0$ only, since at $\beta=0$ every copycat price earns zero. Under the commitment contract no inventory value is asserted, because at $\beta=h=0$ the timing of purchases is undetermined.

Every theorem asserts existence of an equilibrium, so no statement holds vacuously.

Contributions welcome: the copycat best-response lemma, the period-2 subgame solution for arbitrary inventory, the supplier's piecewise problem, and the real-analysis lemmas on $h_1$. The game layer (contracts, histories, SPE) is reusable for other two-period channel models.

Selected references

• C. Jin, C. A. Wu, Y.-J. Chen, Managing Competition from Within and Outside: Using Strategic Inventory and Network Externality to Combat Copycats, SSRN 3826955, version of 2023-05-17. https://ssrn.com/abstract=3826955 ; Manufacturing & Service Operations Management (2023), https://doi.org/10.1287/msom.2021.0182
• K. Anand, R. Anupindi, Y. Bassok, Strategic Inventories in Vertical Contracts, Management Science 54(10), 2008. https://doi.org/10.1287/mnsc.1070.0767
• H. Pun, G. D. DeYong, Competing with Copycats When Customers Are Strategic, Manufacturing & Service Operations Management 19(3), 2017. https://doi.org/10.1287/msom.2016.0610

Motivation

New drugs, medical devices and patented technologies reach the market only after a phase of costly testing, and they can be withdrawn later when evidence of harm accumulates. Societies control this process with three instruments: an approval standard (how strong the evidence must be before adoption), a withdrawal standard (how bad the evidence must become before the product is pulled), and liability (a payment the firm owes when the product turns out to be harmful). Viscusi, Vernon and Harrington (1995) point out that these instruments interact and that liability can chill research. Henry, Loseto and Ottaviani build a model in which the firm learns from the same public signal before and after approval, and ask which mix of the three instruments a regulator should use. Their main result (Proposition 6, called "our main result" on pp.4 and 26 of the working paper) is the goal of this mission.

Setting

The state is good ($G$) or bad ($B$). Beliefs are written as log-odds $\sigma=\log\frac{q}{1-q}$, where $q$ is the probability of $G$, so $\pi_G(\sigma)=e^\sigma/(1+e^\sigma)$. Information is a Brownian signal with drift $\pm\mu_n$ and variance $\rho^2$; with $\lambda_n=2\mu_n^2/\rho^2$ the log-odds belief has drift $\pm\lambda_n$ and variance $2\lambda_n$. Phase $n=1$ is ex ante experimentation, which costs $c>0$ per unit of time and ends with rejection (payoff $0$) or adoption. Phase $n=2$ is ex post learning on the market, which is free and ends with withdrawal. Payoffs are discounted at rate $r>0$.

On the market the planner earns $v^G_p>0$ per unit of time in state $G$ and $v^B_p<0$ in state $B$. The firm earns $v_i=(1-e)v^G_p$ in both states, minus a liability $L\in[0,\,v_i-v^B_p]$ in state $B$. Here $e\in[0,1]$ is the externality rate: the share of the social gain that the firm does not capture.

Policies are standards: a rejection standard $s$, an adoption standard $S$ and a withdrawal standard $z$. With $r_{1,2}=\tfrac12(1\mp\sqrt{1+4r/\lambda_2})$, a player with flows $(a_G,a_B)$ who adopts at belief $S$ and withdraws at $z\le S$ gets the ex post value

$$u^2(S,z)=\pi_G(S)\tfrac{a_G}{r}\bigl(1-e^{-r_2(S-z)}\bigr)+\pi_B(S)\tfrac{a_B}{r}\bigl(1-e^{r_1(S-z)}\bigr).$$

From a prior $\sigma_0\in(s,S)$ the ex ante value $u^1(\sigma_0;s,S,z)$ is the expected discounted payoff of experimenting until the belief reaches $s$ or $S$. It is written with the closed-form hitting kernels $\Psi,\psi$ of the paper's footnote 37 and the roots $R_{1,2}=\tfrac12(1\mp\sqrt{1+4r/\lambda_1})$. Welfare is $u^1_p$, computed with the planner's flows.

The planner's first best (Proposition 1) is a triple $s^*\le z^*\le S^*$ with $z^*=-\ln\frac{v^G_p r_2}{v^B_p r_1}$. In the regulated game the planner commits to $(S,z,L)$ and the firm chooses only its rejection standard $s$, as a best reply. An optimal mix maximizes welfare over commitments and the firm's best replies.

Formalization targets

Goal: Proposition 6 (corrected)

For first-best standards $(s^*,S^*)$ there is $\hat e\in(0,1)$, independent of the prior, such that for every $e\in[0,1]$ and every prior $\sigma_0\in(s^*,S^*)$:

$$\text{first best achieved}\iff e\le\hat e;\qquad e<\hat e\ \Rightarrow\ L>0\ \text{in every optimal mix};$$ $$e\ge\hat e\ \Rightarrow\ L=0,\qquad S\le S^*,\ z\le z^*\ \text{in every optimal mix where the firm experiments } (s<\sigma_0<S).$$

The printed statement needs three minimal corrections:

1. "iff $e<\hat e$" becomes "iff $e\le\hat e$". The paper's own Step 2 (p.42) and p.22 achieve the first best at $e=\hat e$ with $L=0$.
2. Clauses (a)(ii) and (b) are restricted to optimal mixes under which the firm experiments. For $e$ near $1$ and $\sigma_0\in(s^*,z^*)$, the best attainable welfare is $0$. Every mix under which the firm rejects at once is then optimal, including $(S^*+1,\,z^*+1,\,\bar L/2)$.
3. Priors are restricted to $(s^*,S^*)$. For $\sigma_0\ge S^*$ the mix $(S=\sigma_0,z^*,0)$ makes the firm adopt at once, which is first best for every $e<1$.

Milestones (in proof order)

• the optimal withdrawal standard $z^*$ (Proof of Prop. 1, Step 1);
• the shape of $u^2_p(\cdot,z^*)$ (Step 3);
• Proposition 1 itself;
• strict monotonicity of the firm's rejection standard in $e$ (Proof of Prop. 3, Step 2) and in $L$ (Proof of Prop. 6, Step 2);
• the critical externality $\hat e$ (Step 1);
• first best with liability $L(e)\in(0,\hat L)$ for $e\le\hat e$ (Step 2);
• for $e>\hat e$, zero liability and strictly lenient standards $S<S^*$, $z<z^*$ (Step 3).

Significance

Proposition 6 says that liability is used only to discourage research, never to encourage it. When the externality is small, the firm experiments too much, and liability brings it back to the social optimum. When the externality is large, the firm experiments too little; the regulator then drops liability and becomes more lenient at both ends, approving sooner and withdrawing later. This matches the observed pattern that liability and ex post regulation are rarely used together, and that regulators depart from first-best standards in the direction of leniency. Proposition 7 (costly lying) of the paper follows from this result.

The paper's proof is heuristic: it argues "by continuity" and through a second-order/first-order trade-off. The statement as printed has the slips listed above, and no machine-checked proof exists. The mission states the corrected result over the paper's explicit closed forms. A proof will settle whether the corrected statement holds in full, including the strict leniency of Step 3.

Difficulty

Every object is an explicit combination of exponentials, so the statements are elementary. The proofs are not:

• Existence and the threshold ordering of the planner's optimum (Proposition 1) is a smooth-pasting argument on explicit kernels.
• The firm's comparative statics in $e$ and $L$ rest on cross-partial signs. The paper quotes them through coefficients $a,b,f,g$ that are defined only in another paper, so they must be derived from the closed forms.
• Step 3 is a statement about a bilevel optimum: the planner optimizes over the firm's best replies. The paper's envelope argument is local. Moving $S$ away from $S^*$ at the firm's reply $s_{pp}\ne s^*$ has a first-order direct effect, so the "second-order loss" claim does not carry over directly.

Formalization scope

Beliefs, standards and the prior are real log-odds. Values are the paper's closed forms for threshold policies (footnote 17 defines the first best this way). The Brownian layer and the paper's reduction to thresholds (Lemmas 1–2) are not formalized. The closed forms are extended by the stopping rules at the boundary: immediate rejection when $\sigma_0\le s$, immediate adoption when $S\le\sigma_0$, immediate withdrawal ($\psi=1$) when $S<z$.

Further conventions:

• $r>0$ and $c>0$; $e=1$ is allowed.
• "First best achieved" means that some feasible mix and firm best reply attain the maximal welfare.
• "Optimal mix" is a strong-Stackelberg optimum over $(S,z,L)$ and the firm's best replies $s\in\mathbb R$, and "all three instruments are used" means $L>0$.
• The critical externality $\hat e$ is quantified before the prior.

The goal is not vacuous: the prior interval $(s^*,S^*)$ is non-empty for the true first best. Comparing optimal mixes only against mixes with the same $L$, or letting $\hat e$ depend on $\sigma_0$, would change the theorem and is excluded.

The development needs only Real.exp, Real.log and Real.sqrt. Lemmas on the hitting kernels (positivity, monotonicity, $\Psi+\psi<1$) and on single crossing are reusable for other Wald-type problems. Contributions on any milestone are welcome, as are sketches of the Proposition 1 verification argument.

Selected references

• E. Henry, M. Loseto, M. Ottaviani, Regulation with Experimentation: Ex Ante Approval, Ex Post Withdrawal, and Liability, working paper, November 2018; later Management Science 68 (2022), https://doi.org/10.1287/mnsc.2021.4164
• E. Henry, M. Ottaviani, Research and the Approval Process: The Organization of Persuasion, American Economic Review 109 (2019), https://doi.org/10.1257/aer.20171919
• N. Stokey, The Economics of Inaction: Stochastic Control Models with Fixed Costs, Princeton University Press, 2009, https://doi.org/10.1515/9781400829712
• W. K. Viscusi, J. M. Vernon, J. E. Harrington, Economics of Regulation and Antitrust, 2nd ed., MIT Press, 1995.

Motivation

Mean-field control (MFC) models a large population of identical, cooperating agents through a single representative agent whose transitions and rewards depend on the distribution of the whole population. It is the limit of cooperative $N$-agent problems as $N\to\infty$, and it is used for systems such as ride-sharing fleets, resource allocation and equilibrium pricing, where interactions pass through aggregate quantities. When the transition law and the reward are unknown and must be learned, the natural tool is reinforcement learning, and the first question is which Q function obeys a Bellman equation.

The classical Q function on states and actions does not: Example 3.1 of Gu, Guo, Wei and Xu shows it is time inconsistent for MFC. The paper lifts the problem to the space of state distributions, with local policies as actions, and proves the dynamic programming principle (DPP) for the resulting integrated Q (IQ) function.

Timeline. Laurière and Pironneau (2014) and Pham and Wei (2016) proved DPPs for the value function of McKean–Vlasov control with strict controls over a finite horizon, by enlarging the state space; Pham and Wei work in discrete time. Djete, Possamaï and Tan (2019) proved one in a more general framework. Gu, Guo, Wei and Xu (arXiv 2019, v6 2022) gave the DPP for the IQ function with relaxed controls and stochastic rewards over an infinite horizon, the first for MFC with learning.

Setting

Let $\mathcal S$ and $\mathcal A$ be the state and action spaces and $\mathcal P(X)$ the probability measures on $X$. A model consists of a transition law $P(s,\mu,a,\nu)\in\mathcal P(\mathcal S)$, a reward law $R(s,\mu,a,\nu)\in\mathcal P(\mathbb R)$, both measurable in $(s,\mu,a,\nu)\in\mathcal S\times\mathcal P(\mathcal S)\times\mathcal A\times\mathcal P(\mathcal A)$, and a discount factor $\gamma\in(0,1)$.

An admissible control $\pi=\{\pi_t\}\in\Pi$ is a sequence of measurable maps $\pi_t:\mathcal S\times\mathcal P(\mathcal S)\to\mathcal P(\mathcal A)$ (relaxed feedback controls). Under $\pi$ the representative agent follows the McKean–Vlasov dynamics (2.7)

$$s_{t+1}\sim P(s_t,\mu_t,a_t,\nu_t),\qquad a_t\sim\pi_t(s_t,\mu_t),\qquad r_t\sim R(s_t,\mu_t,a_t,\nu_t),$$

where $\mu_t$ and $\nu_t$ are the laws of $s_t$ and $a_t$ themselves. The value of $\pi$ from $s_0\sim\mu$ is $v^\pi(\mu)=\mathbb E^\pi[\sum_t\gamma^tr_t]$, and $v(\mu)=\sup_{\pi\in\Pi}v^\pi(\mu)$.

A local policy $h\in\mathcal H$ is a measurable map $h:\mathcal S\to\mathcal P(\mathcal A)$. With $\nu(\mu,h)=\int h(s)\,\mu(ds)$, the lifted transition and integrated reward are

$$\Phi(\mu,h)=\int\mu(ds)\int h(s)(da)\,P(s,\mu,a,\nu(\mu,h)),\qquad \widehat r(\mu,h)=\int\mu(ds)\int h(s)(da)\int r\,R(s,\mu,a,\nu(\mu,h))(dr).$$

The IQ function is $Q(\mu,h)=\sup_{\pi\in\Pi_1}Q^\pi(\mu,h)$, where $Q^\pi(\mu,h)$ is the expected discounted reward when $s_0\sim\mu$, $a_0\sim h(s_0)$ and $a_t\sim\pi_t(s_t,\mu_t)$ for $t\ge1$. Throughout, Outstanding Assumption (A) holds: for every $\mu$, $\sup_{\pi}\mathbb E^\pi[\sum_t\gamma^t|r_t|]<\infty$.

Formalization targets

Goal: Theorem 3.1 (DPP for the IQ function)

$$Q(\mu,h)=\widehat r(\mu,h)+\gamma\sup_{h'\in\mathcal H}Q\big(\Phi(\mu,h),h'\big)\qquad\text{for all }\mu\in\mathcal P(\mathcal S),\ h\in\mathcal H.$$

Milestones, in proof order

1. Lemma 2.1 (flow property): the state laws of every realization of (2.7) satisfy $\mu_{t+1}=\Phi(\mu_t,\pi_t(\mu_t))$, $\mu_0=\mu$, and the canonical path law is such a realization.
2. Lemma 2.2 (law invariance): $\mathbb E[\sum_t\gamma^tr_t]=\sum_t\gamma^t\widehat r(\mu_t,\pi_t(\mu_t))$ for every realization.
3. (3.6): $v^\pi(\mu)=\widehat r(\mu,\pi_0(\mu))+\gamma v^{\pi_-}(\Phi(\mu,\pi_0(\mu)))=Q^{\pi_-}(\mu,\pi_0(\mu))$.
4. (3.7): $v(\mu)=\sup_{h\in\mathcal H}Q(\mu,h)$.
5. Proof of Theorem 3.1: $Q(\mu,h)=\widehat r(\mu,h)+\gamma\,v(\Phi(\mu,h))$.

Significance

The DPP says that mean-field control with learning is a reinforcement-learning problem whose state is the population distribution and whose action is a local policy. It justifies Q-learning on $\mathcal P(\mathcal S)\times\mathcal H$, which the paper uses to design its learning algorithms for MFC (Algorithms 1–2). It is the necessary condition; the paper's verification theorem (Theorem 3.2) is the sufficient one and is not part of this mission.

The result is proved in the paper, with the proof given in outline ("we highlight the key step"). This mission formalizes it, with no machine-checked version existing before. The formal development adds a discrete-time McKean–Vlasov control layer with a genuine path law, built on Mathlib's Ionescu-Tulcea construction, and states the law-invariance lemmas for every realization of the dynamics, which the paper asserts with a short sketch.

Difficulty

The DPP is short once the problem is known to be a deterministic control problem on $\mathcal P(\mathcal S)$. Establishing that is the work. The population laws enter the kernels, so a path law cannot be written down before the flow of laws is known. One must show that the flow fed into the kernels is the flow the kernels produce (Lemma 2.1), and that every process satisfying (2.7) has that flow. Lemma 2.2 then exchanges expectation and an infinite series under (A), which bounds $\sum\gamma^t|r_t|$ in expectation for each $\mu$ but not uniformly. The remaining steps are supremum arguments at fixed $(\mu,h)$: an $\varepsilon$-optimal tail control is joined to a first-step local policy. Since the flow is deterministic, no measurable selection is needed.

Formalization scope

$\mathcal S$ and $\mathcal A$ are arbitrary measurable spaces (the paper's compact separable metric spaces are an instance; no metric is used), and $\mathcal P(X)$ is ProbabilityMeasure X with the Giry $\sigma$-algebra. $P$, $R$, local policies and controls are Markov kernels; $R$ is a law on $\mathbb R$, so rewards are stochastic. $\Pi_1$ is encoded by $\mathbb N$-indexed controls shifted by one, with $Q^\pi(\mu,h)$ the value of the control that plays $h$ first and then $\pi$.

$v^\pi$ and $Q^\pi$ are Bochner integrals of $\sum_t\gamma^tr_t$ under the canonical path law (Kernel.trajMeasure). They are not defined as $\sum_t\gamma^t\widehat r(\mu_t,h_t)$: with that definition Lemmas 2.1–2.2 become tautologies and the goal is bookkeeping. (A) is a lintegral with $|r_t|$ inside the sum. All suprema are real; under (A) they are bounded, which milestone (3.7) states.

The paper also asserts that $\Phi$, $\widehat r$ and $Q$ are measurable on $\mathcal P(\mathcal S)\times\mathcal H$ without naming a $\sigma$-algebra on $\mathcal H$. For uncountable $\mathcal S$ this fails for every $\sigma$-algebra on $\mathcal H$ (a diagonal argument). The milestones therefore state measurability in $\mu$ for fixed $h$, and joint measurability for countable $\mathcal S$; the goal does not claim measurability of $Q$, and its proof does not use it.

Needed infrastructure: kernel composition and products, the Ionescu-Tulcea trajectory measure, lintegral_tsum and integral_tsum. A reusable lemma identifying finite-dimensional marginals of trajMeasure with time-dependent kernels would serve other discrete-time McKean–Vlasov and MDP missions. Proofs of the milestones in any order are welcome.

Selected references

• H. Gu, X. Guo, X. Wei, R. Xu, Dynamic Programming Principles for Mean-Field Controls with Learning, arXiv:1911.07314v6, 2022 (Operations Research). https://arxiv.org/abs/1911.07314
• H. Pham, X. Wei, Discrete time McKean–Vlasov control problem: a dynamic programming approach, Applied Mathematics & Optimization, 2016. https://arxiv.org/abs/1511.09273
• M. Laurière, O. Pironneau, Dynamic programming for mean-field type control, Comptes Rendus Mathématique, 2014. https://doi.org/10.1016/j.crma.2014.07.008
• M. F. Djete, D. Possamaï, X. Tan, McKean–Vlasov optimal control: the dynamic programming principle, arXiv:1907.08860, 2019. https://arxiv.org/abs/1907.08860
• R. J. Aumann, Borel structures for function spaces, Illinois Journal of Mathematics, 1961. https://doi.org/10.1215/ijm/1255631584

Motivation

On public blockchains, pending transactions wait in a public mempool before a block includes them. Anyone who sees a profitable transaction there can send a competing one with a higher fee and have it executed first. This is front running. It is a large, measured source of losses on decentralized exchanges and in other smart contracts (Daian et al., 2020). A standard defence is the commit-reveal protocol. The user first publishes a hash of her message, which hides its content, and reveals the message one block later. The contract executes a revealed message only if it matches an earlier commitment from the same address.

Canidio and Danos (arXiv:2301.13785v3) model this protocol as a game between a victim and an attacker. They ask when the protocol removes front running. Their answer is a threshold: compare the cost of a commit message with the value of a guess the attacker must commit to before seeing anything. This mission formalizes that threshold result, Proposition 2, together with the lemmas of §3.1 that lead to it.

Setting

A state of the world $s\in S$ is drawn from a prior $p$ and observed only by player $A$ (Alice). Messages range over $\Sigma$. Both $S$ and $\Sigma$ are finite and non-empty.

• When $A$'s message $\tilde\sigma_A$ is executed, she earns $\tilde P_A(\tilde\sigma_A,s)$.
• $A$ sends $\sigma_A(s)$, the unique maximizer of $\tilde P_A(\cdot,s)$. Distinct states have distinct maximizers, so $A$'s message reveals the state. Her payoff is $P_A(s)=\tilde P_A(\sigma_A(s),s)$.
• If player $B$ (Bob) gets his message $\tilde\sigma_B$ executed before hers, he earns $\tilde P_B(\tilde\sigma_B,\tilde\sigma_A,s)$ and $A$ earns nothing.
• A regular message costs $c>0$. A fast message costs $f>c$ and lands before $A$'s regular message with probability $q$.
• Payoffs earned one block later are discounted by $\beta\in[0,1]$.
• No state has $P_A(s)\in[c,c+c/\beta]$.

The protocol has two blocks.

• Commit block. $A$ either commits (cost $c$) or stays out, in which case both players get $0$. $B$ sees that $A$ committed, but not the state. He may stay out, clone $A$'s commitment, or commit a guess $\sigma\in\Sigma$. Either commit costs $c$.
• Reveal block. $A$ reveals $\sigma_A(s)$ at cost $c$ and earns $P_A(s)$. If $B$ committed a guess $\sigma$, he sees her message and may fire the reveal of $\sigma$ as a fast message at cost $f$. With probability $q$ it lands first: he earns $\tilde P_B(\sigma,\sigma_A(s),s)$ and $A$ earns $0$. A clone can never be revealed validly from $B$'s address.

Strategies are behavior strategies. For $A$: probabilities $\mathrm{commit}(s)$ and $\mathrm{reveal}(s)$. For $B$: a lottery $\mu$ over his commit options and firing probabilities $\mathrm{fire}(\sigma,m)$. An equilibrium is a Nash equilibrium of the ex-ante expected payoffs. Write $\sigma^{**}_A(s)\neq\emptyset$ for $P_A(s)\ge c$, eq. (3). The value of a blind guess is

$$\pi=\max_{\sigma\in\Sigma}E_s\big[\max\{q\,\tilde P_B(\sigma,\sigma_A(s),s)-f,0\}\,\big|\,P_A(s)\ge c\big].$$

The front-running threat of $B$'s strategy is $\sum_s p(s)\,\mathbf 1[P_A(s)\ge c]\,\sum_\sigma\mu(\sigma)\,\mathrm{fire}(\sigma,\sigma_A(s))$. It is the probability that $B$ fires at $A$'s message in the states where she has one to send.

Formalization targets

Goal: Proposition 2 (corrected)

1. An equilibrium exists (footnote 16).
2. If $\beta\pi\le c$, some equilibrium has zero on-path front running and zero threat; it is the backward-induction one, in which $B$'s firing and $A$'s reveal are optimal at every information set, reached or not.
3. If $\beta\pi>c$, every equilibrium has a strictly positive threat.

So an equilibrium free of front running exists if and only if $\beta\pi\le c$.

The printed proposition reads: "If $\pi\le c/\beta$, then there is no front-running in equilibrium. If instead $\pi>c/\beta$, front running occurs with strictly positive probability in equilibrium." Both sentences fail under their natural readings, for any model satisfying every assumption of §§2–3.

• "No front-running in every equilibrium" fails. Take $S=\Sigma=\{1,2,3\}$, $p=(1/10,8/10,1/10)$, $c=2$, $f=3$, $q=1/2$, $\beta=1$, $P_A=(100,6,100)$. Guess 1 earns $\tilde P_B=26$ in state 1, $31/5$ in state 2, and nothing elsewhere. Then $\pi=27/25\le 2$. Yet there is an equilibrium where $A$ stays out in state 2, where an attack would leave her at $-1$, and $B$ commits guess 1 and fires at it. Front running then has probability $1/10$. The paper's own argument on p.15 shows that the profile without front running is an equilibrium, i.e. the existential form.
• "Front running occurs with positive probability" fails. Take one state and one message, $c=1$, $f=2$, $q=1/2$, $\beta=1$, $P_A=3$, $\tilde P_B=10$. Then $\pi=3>1$. But whenever $A$ commits, $B$ guesses and fires, which leaves her $-1/2$, so she never commits. On-path front running is $0$ in every equilibrium, while the threat is $1$. This is the deterrence effect the paper describes on p.11.

Both counterexamples are checked as Lean proofs.

Milestones

• Lemma 1: no cloning, and no commit without reveal.
• $B$'s reveal rule: fire exactly when $q\tilde P_B>f$ (at equality $B$ is indifferent).
• $A$'s best payoff when unthreatened: $\max\{-c+\beta(P_A(s)-c),0\}$.
• $A$'s reply when unthreatened: $\sigma^{**}_A$.
• The value $\beta\pi-c$ of a committed guess.
• Existence of equilibrium.

Significance

The threshold measures how much the protocol protects. The attacker must commit before seeing the victim's message, so his relevant information is the prior, not the message. Attacks that rely mostly on observing the victim, where guessing is hard, are removed. Attacks in which the attacker would profit anyway are not. Section 4 of the paper builds its comparison of attackers with legitimate competitors, and of hidden commitments, on this threshold.

A formal proof settles which version of the claim holds. The printed proposition mixes "some equilibrium" with "every equilibrium" and on-path behavior with threats. The corrected statement separates these. Its two halves together give a sharp characterization. No part of this paper has been machine-checked before.

Difficulty

The obvious argument fixes the "no front running" profile and checks deviations. That gives clause 2. It does not give clause 3, and the obvious converse is false. When guessing is easy, the attacker's threat can keep the victim out entirely, so nothing happens on path. Clause 3 instead argues by contradiction from an equilibrium with zero threat. In that case the victim must commit exactly where $P_A(s)\ge c$, which is where the interval assumption enters. Then a committed guess earns the attacker $\beta\pi-c>0$.

Ex-ante Nash equilibrium places no constraint on zero-probability states or information sets. Every per-state statement must be weighted by its probability, and handling this is a large part of the work.

Existence is Nash's theorem for this finite game, in behavior strategies. It can be proved from the normal form, or directly with Kakutani's fixed point theorem on the product of simplices.

Formalization scope

The formalization commits to the following conventions:

• $S$ and $\Sigma$ are Fintypes with DecidableEq and Nonempty, and the prior is a real vector summing to $1$, possibly with zeros.
• $\sigma_A$ is injective; the paper's bijection specializes to this.
• The interval assumption reads $P_A(s)<c\ \lor\ c<\beta(P_A(s)-c)$, so $\beta=0$ is allowed.
• The threshold is written $\beta\pi\le c$ rather than $\pi\le c/\beta$.
• $\pi=0$ when $\Pr(P_A(s)\ge c)=0$, where the paper's $\pi$ is undefined.
• Payoffs are ex ante.

Equilibrium is the plain Nash condition over all unilateral deviations. It is not defined through the paper's answer, and $B$'s firing and $A$'s revealing are free probabilities, so the milestones are not true by definition.

Everything is finite sums over finite types; no measure theory is needed. Mathlib's simplices and Brouwer/Kakutani-type fixed points, or the platform's AGT.nash_existence for finite normal-form games, are possible routes to existence. Proofs of any milestone are welcome.

Selected references

• A. Canidio, V. Danos, Commitment Against Front-Running Attacks, arXiv:2301.13785v3, 2023. https://arxiv.org/abs/2301.13785v3
• P. Daian et al., Flash Boys 2.0: Frontrunning in Decentralized Exchanges, Miner Extractable Value, and Consensus Instability, IEEE S&P, 2020. https://doi.org/10.1109/SP40000.2020.00040
• J. Nash, Equilibrium points in n-person games, PNAS 36(1), 1950. https://doi.org/10.1073/pnas.36.1.48