All missions

Motivation

A seller with one item and several buyers whose values are private but drawn from known, independent distributions can maximize expected revenue with Myerson's optimal auction (Myerson, 1981). That auction depends on every distribution through virtual values, asks buyers to report their values, and allocates through a computation that buyers must trust. A sequential posted-price (SPP) mechanism is far simpler: the seller fixes one take-it-or-leave-it price per buyer and approaches the buyers one at a time. Posted prices are common in practice, and no buyer reports anything. The natural question is how much revenue this simplicity costs, measured as the worst-case ratio between the best SPP revenue and the optimal revenue.

Timeline. Chawla, Hartline, Malec and Sivan (2010) showed that sequential posted prices earn at least $1 - (1 - 1/n)^n \ge 1 - 1/e \approx 0.632$ of the optimal revenue in the single-unit setting with $n$ independent buyers. Azar, Chiplunkar and Kaplan (2018) improved this to $0.6346$ for $n \ge 74$, which gave the best universal bound before the present paper. No SPP mechanism can guarantee more than about $0.745$ even for i.i.d. values (Hill and Kertz, 1982; Correa et al., 2017). Beyhaghi, Golrezaei, Paes Leme, Pál and Sivan (Operations Research, 2021; arXiv:1807.03435) proved the universal bound $0.6543$, valid for every $n$, together with $n$-dependent, multi-unit and matroid results and a bound of $0.6620$ for eager second-price auctions. This mission formalizes their single-unit universal bound.

Setting

There are $n$ buyers $i \in [n]$. Buyer $i$ has a value $v_i$ drawn from a probability distribution $\mu_i$ on $\mathbb R$, independently across buyers; the profile $v = (v_1,\dots,v_n)$ has law $\mu_1 \otimes \cdots \otimes \mu_n$.

SPP$(p)$. Given prices $p = (p_1,\dots,p_n)$, the mechanism approaches buyers in decreasing order of price, offers $p_i$ to buyer $i$ while the item is unsold, and sells to the first buyer with $v_i \ge p_i$ at price $p_i$. Its revenue at the profile $v$ is therefore $\max\{p_i : v_i \ge p_i\}$ (zero if nobody accepts), and $\mathrm{SPP}(p)$ denotes its expectation.

Threshold mechanisms (the benchmark). By the taxation principle (Lemma 1 of the paper, cited from Nisan et al.), a deterministic truthful mechanism is described by thresholds $t_i(v_{-i}) \ge 0$ depending only on the other buyers' values: buyer $i$ wins and pays $t_i$ when $v_i \ge t_i$. In the single-unit setting, almost surely at most one buyer weakly exceeds their threshold. The expected revenue is $\mathrm{Opt} = \mathbb E[\sum_i t_i \mathbf 1\{v_i \ge t_i\}]$. Define

$$s^\star_i(\tau) = \mathbb P[v_i \ge t_i \ge \tau], \qquad s^\star(\tau) = \sum_i s^\star_i(\tau),$$

so that $\mathrm{Opt} = \int_0^\infty s^\star(\tau)\,d\tau$ (Equation (1)).

Two pricing rules. Myersonian prices post to buyer $i$ the threshold $t'_i = t_i(v'_{-i})$ computed on an independent re-sample of the other buyers' values, freshly for each $i$; MP is the resulting expected revenue and $m(\tau)$ the probability that some buyer has $v_i \ge t'_i \ge \tau$. The uniform price rule posts the same price $\tau$ to everyone; $\mathrm{UP} = \sup_{\tau \ge 0}\mathrm{SPP}(\tau,\dots,\tau)$.

The factor-revealing program (FR). With $f(x) = 1 - e^{-x}$,

$$\mathrm{FR} = \max_{s}\ \int_0^\infty s(\tau)\,d\tau \quad\text{s.t.}\quad 0 \le s(\tau) \le \min(1, 1/\tau)\ \ \forall \tau \ge 0,\quad \int_0^\infty f(s(\tau))\,d\tau \le 1,\quad s \text{ weakly decreasing}.$$

Formalization targets

Goal: Theorem 1 (p. 13)

For every $n$, every independent value distributions and every single-unit threshold mechanism with finite expected revenue $\mathrm{Opt}$, there is a vector of nonnegative prices $p$ with

$$\mathrm{SPP}(p) \ \ge\ 0.6543 \cdot \mathrm{Opt}.$$

The prices depend on the instance; the constant does not.

Milestones, in the order the proof uses them

1. Equation (1), p. 12: $\mathrm{Opt} = \int_0^\infty s^\star(\tau)\,d\tau$ and $s^\star$ is weakly decreasing.
2. Inequality (2), p. 14: $\tau\, s^\star(\tau) \le \mathrm{SPP}(\tau,\dots,\tau)$ for $\tau \ge 0$, hence $\sup_{\tau \ge 0}\tau s^\star(\tau) \le \mathrm{UP}$; and $s^\star \le 1$.
3. Lemma 2, Inequality (5), p. 15: $\mathbb P[Z_\tau = 0] \le (1 - s^\star(\tau)/n)^n \le e^{-s^\star(\tau)}$, where $Z_\tau$ counts buyers with $v_i \ge t'_i \ge \tau$.
4. Inequalities (3)–(4), p. 14: $\mathrm{MP} = \int_0^\infty m(\tau)\,d\tau$ and $m(\tau) \ge 1 - e^{-s^\star(\tau)}$.
5. Solving Problem (FR), p. 15: the root $\tau^\star > 1$ of $(1 - e^{-1}) + \int_1^{\tau^\star}(1 - e^{-1/\tau})\,d\tau = 1$ is unique and lies in $[1.6955, 1.6965]$.
6. Solving Problem (FR), p. 15: the optimal value of (FR) is attained and equals $1 + \ln\tau^\star$, which is at most $1.5283$.

The intermediate statement $\max(\mathrm{MP}, \mathrm{UP}) \ge 0.6543 \cdot \mathrm{Opt}$, the "best of Myersonian and uniform" form shown first in the proof, is context only: Theorem 1 asserts one deterministic price vector, and that is the goal.

Significance

The result. Theorem 1 was the first improvement over $1 - 1/e$ for single-unit posted pricing that holds for every number of buyers and for arbitrary (regular or irregular) independent distributions. It quantifies the price of simplicity of posted pricing against the optimal auction, and its method (two pricing rules, each giving one constraint on the revenue curve $s^\star$, and a factor-revealing program over all curves meeting both) is reused in the paper for $n$-dependent, multi-unit, position-auction and eager second-price bounds.

Formalizing it. The result is proved on paper; no machine-checked version exists. A formalization checks the probabilistic core, the solution of an infinite-dimensional program, and the numerical constants. The printed constants carry rounding slips ($\tau^\star = 1.696$ is a rounding of $1.69572\ldots$; $1 + \ln\tau^\star = 1.52810\ldots$, printed as $1.5283$), which the milestones state precisely. The paper's normalization $\max(\mathrm{MP}, \mathrm{UP}) = 1$ silently assumes that Opt is finite; the formal statement makes that hypothesis explicit.

Difficulty

The Myersonian rule alone gives only $1 - 1/e$, and the paper's example (values uniform on $[1, 1+\epsilon]$) shows this is tight for it; the uniform rule alone is also bounded away from 1. The improvement comes only from combining them, and the combination is expressed as an optimization over all decreasing curves $s$: the step that the obvious argument misses is the exact solution of (FR), whose optimum must be guessed and certified for an infinite-dimensional program with a nonlinear constraint. The probabilistic step is subtle as well: the true thresholds $t_i$ are correlated across buyers, and Lemma 2 holds only for the independently re-sampled $t'_i$. Finally, the theorem claims a single deterministic price vector, so the random Myersonian prices and a possibly unattained best uniform price must both be converted into one concrete $p$, with the slack between $0.6543$ and $1/\mathrm{FR} = 0.65440\ldots$ absorbing the approximation.

Formalization scope

Buyers are Fin n; values have law Measure.pi μ with each μ i a probability measure on ℝ; values need not be nonnegative. Revenues and probabilities are in ℝ≥0∞ (lower Lebesgue integrals and measures), never Bochner integrals, so that a non-integrable revenue cannot become a junk zero. The SPP revenue at a profile is the closed form $\max\{p_i : v_i \ge p_i\}$ of the price-ordered sale. A threshold mechanism is a family t i v with t i measurable, nonnegative, independent of coordinate i, and almost surely at most one buyer with t i v ≤ v i. Myersonian prices are read from a fresh copy of the whole profile per buyer, independent of everything else. In (FR) the constraint $s(\tau) \le \min(1, 1/\tau)$ is encoded as $s(\tau) \le 1$ and $\tau s(\tau) \le 1$.

Benchmark. The goal is stated for every single-unit threshold mechanism, which is the taxation-principle form of Lemma 1; for the optimal mechanism's thresholds it is the printed theorem, and the paper's proof never uses optimality. Lemma 1 and Myerson's theorem are cited by the paper and are not part of the mission. The one added hypothesis on the goal, finiteness of Opt, is necessary: without it some single-unit threshold mechanisms have infinite revenue while every posted-price revenue is finite.

Ruled out. The SPP revenue is the revenue of the actual sequential sale, not a free function; thresholds may not depend on the buyer's own value (that would allow full surplus extraction) and must be single-unit feasible (otherwise Opt could be $n$ times any posted-price revenue); the constant is the explicit $0.6543$, not an existential one.

Out of scope. Theorem 2 ($n$-dependent bounds), Theorem 3 and Lemmas 3–4 (multi-unit), Lemmas 5–7 and Theorem 4 (position auctions), the partition-matroid claim and Proposition 1 (matroids), Lemma 8 and Theorems 5–6 (eager second-price auctions), Inequality (6) of Lemma 2, the $(1-1/e)$ illustration of §4.1, and the numerical tables.

Infrastructure. The development needs the layer-cake formula for lower integrals, independence under product measures, the AM–GM inequality and $(1 - y/n)^n \le e^{-y}$, all in Mathlib, plus a numerical certificate for the root of a transcendental equation. The threshold-mechanism and SPP definitions are reusable for the multi-unit and matroid results of the same paper. Proofs of any milestone, alternative arguments, and sharper constants are welcome.

Selected references

• H. Beyhaghi, N. Golrezaei, R. Paes Leme, M. Pál, B. Sivan, Improved Revenue Bounds for Posted-Price and Second-Price Mechanisms, Operations Research 69(6), 2021. arXiv:1807.03435v4. https://arxiv.org/abs/1807.03435
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
• S. Chawla, J. D. Hartline, D. L. Malec, B. Sivan, Multi-parameter Mechanism Design and Sequential Posted Pricing, STOC 2010. https://doi.org/10.1145/1806689.1806733
• Y. Azar, A. Chiplunkar, H. Kaplan, Prophet Secretary: Surpassing the 1 − 1/e Barrier, ACM EC 2018, 303–318. https://doi.org/10.1145/3219166.3219182
• J. Correa, P. Foncea, R. Hoeksma, T. Oosterwijk, T. Vredeveld, Posted Price Mechanisms for a Random Stream of Customers, ACM EC 2017, 169–186. https://doi.org/10.1145/3033274.3085137
• N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, Theorem 9.36.

Why congestion in matching markets matters

Online matching platforms (labor platforms such as Upwork or TaskRabbit, dating sites, short-term rental platforms) make it cheap to contact potential partners, but not cheap to find one who is still available. A worker who has already accepted a job, or a listing that is already booked, keeps receiving applications and keeps being screened. Arnosti, Johari and Kanoria, Managing Congestion in Matching Markets (M&SOM 23(3):620–636, 2021), build a stochastic game-theoretic model of this effect, in which applicants pay to apply and employers pay to screen, and employers cannot see which applicants have already matched. They prove that the model has a unique equilibrium, compute both sides' welfare in it in closed form, and use the formulas to evaluate platform interventions (application limits, application fees, a market-wide wage).

This mission formalizes the equilibrium characterization: the closed-form equilibrium welfare of Theorem 2, together with the existence and uniqueness results (Proposition 2, Theorem 1) and the identities from the paper's endnotes that connect them.

The stationary mean-field model

A market has four parameters: $r>0$, the number of applicants per employer; $\beta\in(0,1]$, the probability that an applicant is qualified for a given employer; $c_a$, the cost of one application; and $c_s$, the cost of screening one applicant. Throughout, Assumption 1 holds: $\max(c_a,c_s)<\beta$. Write $c'_s = c_s/\beta$.

Applicants choose an application intensity $m\ge0$: an applicant sends a Poisson($m$) number of applications, each of which becomes an offer independently with probability $p$, the acceptance probability. The applicant takes the first offer, so the expected payoff is

$$W_a(m,p) = 1-e^{-mp}-c_a m, \tag{2}$$

maximized by the applicant best response

$$\mathcal M(p) = 0 \ \text{ if } p\le c_a, \qquad \mathcal M(p)=\tfrac1p\log\bigl(\tfrac p{c_a}\bigr)\ \text{ if } p>c_a. \tag{3}$$

Employers receive a Poisson($rm$) number of applications. Each applicant is qualified with probability $\beta$ and still available with probability $q$. An employer either screens sequentially until it hires (screening probability $\alpha$) or exits. The employer best-response correspondence is

$$\mathcal A(q) = \{0\}\ \text{if } q<c'_s,\qquad [0,1]\ \text{if } q=c'_s,\qquad \{1\}\ \text{if } q>c'_s, \tag{4}$$

and the employer payoff is $W_e(\alpha,m,q) = \alpha(1-e^{-rm\beta q})(1-c'_s/q)$ (5).

With $E(x) = (1-e^{-x})/x$ ($E(0)=1$), the consistency conditions are

$$q = E(mp), \qquad p = \alpha\beta\,E(rm\beta q). \tag{6–7}$$

A solution $(p,q)$ is a mean-field steady state of the strategies $(m,\alpha)$. A mean-field equilibrium (MFE) is a pair $(m^*,\alpha^*)$ with a steady state $(p^*,q^*)$ such that $m^* = \mathcal M(p^*)$ and $\alpha^*\in\mathcal A(q^*)$ (Definition 1). Equilibrium welfare is $\Pi^*_a = W_a(m^*,p^*)$ and $\Pi^*_e = W_e(\alpha^*,m^*,q^*)$.

Formalization targets

Goal: Theorem 2 (p. 628)

There are unique $\hat p,\bar p>c_a$ with

$$r\Bigl(1-\frac{c_a}{\hat p}\Bigr) = 1-e^{-\frac{r\beta}{\hat p}\left(1-\frac{c_a}{\hat p}\right)}, \qquad 1-\frac{c_a}{\bar p}+\frac{c_s}{\beta}\log\Bigl(\frac{c_a}{\bar p}\Bigr)=0, \tag{13–14}$$

the MFE is unique, and in it

$$p^*=\min(\hat p,\bar p),\qquad \Pi^*_a = 1-\frac{c_a}{p^*}+\frac{c_a}{p^*}\log\frac{c_a}{p^*},\qquad \Pi^*_e = r\Bigl(1-\frac{c_a}{p^*}+\frac{c_s}{\beta}\log\frac{c_a}{p^*}\Bigr). \tag{15–16}$$

The theorem is exact; it has no constants to improve.

Milestones

1. Proposition 2 (p. 626): for fixed $m\ge0$, $\alpha\in[0,1]$, $r$, $\beta$, the system (6)–(7) has a unique solution.
2. Theorem 2, (13) and Theorem 2, (14) (p. 628): the two root equations each have a unique root above $c_a$.
3. Endnote 13 (p. 635): at the applicant best response, consistency (7) with every employer screening ($\alpha=1$) is equation (13).
4. §5.1 (p. 628): at the applicant best response, employers are exactly indifferent ($q=c'_s$) iff (14) holds.
5. Theorem 1 (p. 627): the MFE exists and is unique.
6. Endnote 12 (p. 635): the welfare identities (15) and (16) at the best response and a steady state.

Significance

Theorem 2 reduces equilibrium welfare on both sides to one scalar, $p^*=\min(\hat p,\bar p)$, and splits markets into two regimes (Definition 2): application-limited ($\bar p>\hat p$; all employers screen; applicants compete in a "tragedy of the commons") and screening-limited ($\bar p<\hat p$; employers are indifferent and their welfare is zero, by (14) and (16)). All of the paper's later results, including the welfare bounds of Theorem 3, the effect of application limits (Theorems 4–5), application costs (Theorem 6) and wages (Theorem 7), are computed from these formulas.

Proposition 2, Theorem 1 and Theorem 2 are stated in the article but their proofs are in a technical report (Arnosti, Johari, Kanoria 2019, SSRN), not reproduced in the article and not used here. To our knowledge none of these results has a machine-checked proof. A formal development would give a self-contained, checked proof of the equilibrium characterization from the article's definitions alone.

Where the difficulty lies

The welfare identities (15)–(16) are algebra once $m^*=\mathcal M(p^*)$ and $p^*>c_a$ are known. The root statements are one-variable analysis. The hard part is the equilibrium itself. Proposition 2 is a fixed-point problem: substituting (7) into (6) gives an increasing map $q\mapsto E(m\alpha\beta E(rm\beta q))$, and an increasing map can have several fixed points, so a monotonicity argument alone does not give uniqueness. Theorem 1 then has to handle the correspondence $\mathcal A$: an equilibrium may sit at the kink $q^*=c'_s$ with an interior $\alpha^*$, and the case analysis has to show that exactly one of the regimes $\alpha^*=1$, $\alpha^*<1$ applies and that it pins down $(m^*,\alpha^*)$.

Formalization scope

All objects live in the namespace MatchCongestion.Welfare, over ℝ. The conventions are:

• Positivity. Params.Standing is Assumption 1 together with $0<r$, $0<\beta\le1$, $0<c_a$, $0<c_s$, which the paper uses without listing them ("costs", $\beta$ a probability). Without $c_s>0$, (14) has no root above $c_a$.
• The ratio at zero. The page leaves (6)–(7) undefined at $mp=0$ and $rm\beta q=0$. They are written through $E$ with $E(0)=1$, the continuous extension.
• Definition 1. It composes $\mathcal M$ and $\mathcal A$ with the steady-state maps $\mathcal P,\mathcal Q$. IsMFE instead asks for some steady state $(p,q)$; by Proposition 2 the two readings agree.
• The correspondence. $\mathcal A(q)$ is a Set ℝ.
• Roots and welfare. $\hat p,\bar p$ are quantified (any roots above $c_a$), not chosen. $\Pi^*_a,\Pi^*_e$ are $W_a,W_e$ at the MFE's own steady state. $\log$ is Real.log.

Several formalizations would make the goal trivial or false, and none is used:

• a raw division (1 - exp (-x)) / x in (6)–(7) would make $(m,\alpha,p,q)=(0,0,0,0)$ a spurious second equilibrium;
• an "every MFE satisfies …" goal without the existence-and-uniqueness conjunct would be vacuous;
• choosing $\hat p,\bar p$ by Classical.choose, or $\mathcal P,\mathcal Q$ in Definition 1, would leave junk values unconstrained;
• $\mathcal A$ as a function would erase the screening-limited equilibrium, which has an interior $\alpha^*$;
• $\mathcal M$ without the case split $p\le c_a$ would make the best response negative.

Proposition 1 (the employer's sequential screening problem, specified only in an online appendix), the application-limit model (8)–(9) with Proposition 3, Theorems 3–7 and the finite-system limit theorems 8–10 are out of scope. Contributions of independent interest are a general lemma on unique roots of strictly convex or concave one-variable functions on an interval, and analytic facts about $E$ (positivity, strict monotonicity, $E\le1$ on $[0,\infty)$).

Selected references

• N. Arnosti, R. Johari, Y. Kanoria, Managing Congestion in Matching Markets, Manufacturing & Service Operations Management 23(3):620–636, 2021. https://doi.org/10.1287/msom.2020.0927
• N. Arnosti, R. Johari, Y. Kanoria, Managing Congestion in Matching Markets (full technical report), preprint, 2019. http://dx.doi.org/10.2139/ssrn.2427960

Motivation

A quantum memory stores logical qubits in many physical qubits so that errors can be detected and corrected. The overhead of doing so, measured by how many physical qubits are spent per logical qubit at a given error-correcting power, is one of the main costs of fault-tolerant quantum computation. Bivariate-bicycle (BB) codes are currently the leading low-overhead family: the gross code $[[144,12,12]]$ of Bravyi et al. (Nature, 2024) stores 12 logical qubits at distance 12 using 144 data qubits, roughly a tenth of the overhead of a surface code with the same distance, and it is the basis of a published hardware roadmap. The search for higher-rate members of the family is active, and the claims made in it are claims about the exact distance of explicit finite codes. These are finite but very large computations, and they are rarely checked independently.

Timeline.

• 2004 — MacKay, Mitchison and McFadden introduce bicycle codes: CSS codes built from a pair of circulant matrices.
• 2013 — Kovalev and Pryadko generalize the construction to commuting pairs of group-algebra elements (generalized bicycle codes).
• 2024 — Bravyi, Cross, Gambetta, Maslov, Rall and Yoder define BB codes over $\mathbb Z_l\times\mathbb Z_m$ and give the ladder $[[72,12,6]]$, $[[90,8,10]]$, $[[108,8,10]]$, $[[144,12,12]]$, $[[288,12,18]]$, with $[[360,12,\le 24]]$ left with only an upper bound.
• 2026 — An evolutionary search by Cruz-Benito et al. (arXiv:2606.02418) reports $[[288,16,12]]$ as its best indecomposable weight-6 code at distance 12.
• 2026 — Daugherty, Ryan and Ward give two new $[[336,20,12]]$ codes and a new $[[360,24,12]]$ code. They certify the exact distances of the whole ladder, establish $d=24$ for $[[360,12]]$, and show by enumeration that no connected three-term weight-6 BB code with $n\le 360$ and $k\ge 20$ has distance 13 or more.

Setting

Fix positive integers $l,m$ and let $G=\mathbb Z_l\times\mathbb Z_m$. The monomial $x^iy^j$ of the ring $\mathbb F_2[x,y]/(x^l-1,\,y^m-1)$ is identified with $(i,j)\in G$. A polynomial $P$ with coefficients in $\mathbb F_2$ is identified with its support, the finite set of monomials with coefficient $1$. The circulant of $P$ is the $G\times G$ binary matrix with a $1$ in row $g$, column $h$ exactly when $h-g\in P$.

Given two polynomials $A,B$, the BB code $\mathrm{BB}(A,B)$ acts on $n=2lm$ qubits, arranged in two blocks indexed by $G$. Its check matrices are

$$H_X=[\,A\mid B\,],\qquad H_Z=[\,B^{\mathsf T}\mid A^{\mathsf T}\,],$$

where $A$ and $B$ also denote their circulants. Because $G$ is abelian, $H_XH_Z^{\mathsf T}=AB+BA=0$ over $\mathbb F_2$, so this is a CSS code. Its parameters are:

1. the number of logical qubits $k=n-\operatorname{rank}H_X-\operatorname{rank}H_Z$, with ranks over $\mathbb F_2$;
2. the Z-distance $d_Z$, the least Hamming weight of a vector $v\in\mathbb F_2^n$ with $H_Xv=0$ and $v\notin\operatorname{row}(H_Z)$ (a nontrivial Z-logical);
3. the X-distance $d_X$, defined dually: $H_Zv=0$ and $v\notin\operatorname{row}(H_X)$.

The code is $[[n,k,d]]$ when $d_X=d_Z=d$. Each check of a code built from two three-term polynomials touches six qubits (weight 6). The Tanner graph joins each qubit to the X- and Z-checks acting on it, and the code is connected when this graph is connected.

Formalization targets

Goal: the three new codes

$$\mathrm{BB}_{\mathbb Z_2\times\mathbb Z_{84}}\!\left(1+y+xy^{5},\;1+y^{4}+y^{62}\right)=[[336,20,12]],$$ $$\mathrm{BB}_{\mathbb Z_2\times\mathbb Z_{84}}\!\left(1+y+xy^{5},\;1+y^{20}+y^{46}\right)=[[336,20,12]],$$ $$\mathrm{BB}_{\mathbb Z_6\times\mathbb Z_{30}}\!\left(1+y+xy^{2},\;1+y^{8}+x^{2}y^{16}\right)=[[360,24,12]],$$

each with $d_X=d_Z=12$ (Table 9 of the source). Each new code is also a milestone on its own.

Milestones

• Lemma 1 (minimality). In any parity system, no nonempty proper subset of a minimum-weight logical is even on every check.
• Table 3, the certified ladder. $[[72,12,6]]$, $[[90,8,10]]$, $[[108,8,10]]$, $[[144,12,12]]$, $[[288,12,18]]$ and $[[360,12,24]]$, all with $d_X=d_Z$, for the polynomials of Bravyi et al.
• Section 6, the weight-6 envelope. Every connected BB code built from two three-term polynomials with $n\le 360$ and $k\ge 20$ has a nontrivial X- or Z-logical of weight at most 12. In words, none has distance 13 or more.

Significance

The result. The new codes encode 25% and 50% more logical qubits at distance 12 than the best weight-6 code reported by evolutionary search, with figures of merit $kd^2/n$ of 8.57 and 9.60. The ladder distances turn published values, several of them previously supported only by heuristic searches or upper bounds, into exact statements. In particular $d([[360,12]])=24$ settles an upper bound left open by Bravyi et al. The envelope statement is a negative result: within this family and size range, distance 12 is the ceiling at $k\ge 20$.

Formalizing it. In the source, each lower bound on a distance is a DRAT refutation or a replayable proof tree, checked by external programs. Only the pruning lemma (Lemma 1) has a machine-checked proof, in Lean 4. A complete formalization would make the code parameters kernel-checked facts about explicit Mathlib objects, independent of every external checker. Upper bounds on distance and the values of $k$ are finite linear-algebra facts. Lower bounds are exhaustive statements over $\binom{n}{w}$-sized spaces and are the core of the work.

Difficulty

The upper bound $d\le 12$ needs one explicit weight-12 logical together with a proof that it lies outside the opposite row space. The lower bound $d\ge 12$ asks that no nontrivial logical of weight at most 11 exist among roughly $\binom{336}{11}\approx 10^{19}$ candidate supports. Direct enumeration is out of reach. A SAT encoding with a cardinality constraint is several orders of magnitude slower than the source's pruned search, and the resulting proof objects are large: hundreds of megabytes for the larger ladder codes. Kernel-checking such certificates, or finding structure that avoids them, is the central difficulty. Computing $k$ also requires an $\mathbb F_2$-rank of matrices with up to 180 rows and 360 columns, and Mathlib's Matrix.rank is not computable by decide. The envelope statement additionally quantifies over 971 group shapes and every pair of three-term polynomials on each.

Formalization scope

All objects are in the definition file BBCode_Setting. $G$ is ZMod l × ZMod m, and a polynomial is a Finset of monomials, which makes it a set of distinct terms. The circulant has entry 1 at $(g,h)$ iff $h-g\in P$. Qubits are G ⊕ G (left and right blocks). $H_X$ is Matrix.fromCols (circulant A) (circulant B) and $H_Z$ is Matrix.fromCols (circulant B)ᵀ (circulant A)ᵀ, over ZMod 2. The row space is the ZMod 2-span of the rows, and the weight counts nonzero coordinates. NumLogical A B k states $\operatorname{rank}H_X+\operatorname{rank}H_Z+k=n$ additively, avoiding truncated subtraction. HasZDistance A B d requires both a nontrivial Z-logical of weight exactly $d$ and the lower bound for every nontrivial Z-logical, so a code without logicals cannot satisfy it vacuously. IsCode A B n k d bundles $n=2lm$, $k$ and both distances.

The envelope quantifies over all $l,m\ge 1$ with $2lm\le 360$. The source enumerates 961 shapes; the 10 it omits ($lm\le 5$) cannot have $k\ge 20$, so the two ranges are equivalent.

Reusable infrastructure includes computable $\mathbb F_2$ rank certificates (explicit row-echelon or basis witnesses), a verified checker for DRAT or proof-tree certificates, and symmetry lemmas for group translations acting on BB codes. Contributions of any of these, of individual sectors ($d_X$ or $d_Z$ separately), or of upper and lower bounds as separate lemmas are welcome.

Selected references

• S. Bravyi, A. W. Cross, J. M. Gambetta, D. Maslov, P. Rall, T. J. Yoder, High-threshold and low-overhead fault-tolerant quantum memory, Nature 627, 778–782, 2024. https://doi.org/10.1038/s41586-024-07107-7 (arXiv: https://arxiv.org/abs/2308.07915)
• B. W. Daugherty, S. Ryan, G. Ward, New distance-12 bivariate-bicycle codes with 20 and 24 logical qubits: an exhaustive classification and checkable distances to 360 qubits, certificate release v1.0.0, Zenodo, 2026. https://doi.org/10.5281/zenodo.23382175
• D. J. C. MacKay, G. Mitchison, P. L. McFadden, Sparse-graph codes for quantum error correction, IEEE Trans. Inf. Theory 50(10), 2315–2330, 2004. https://arxiv.org/abs/quant-ph/0304161
• A. A. Kovalev, L. P. Pryadko, Quantum Kronecker sum-product low-density parity-check codes with finite rate, Phys. Rev. A 88, 012311, 2013. https://arxiv.org/abs/1212.6703
• J. Cruz-Benito et al., evolutionary search for bivariate-bicycle codes, arXiv:2606.02418, 2026. https://arxiv.org/abs/2606.02418

Motivation

Finite sums provide a concrete setting for practicing precise mathematical statements. The sum of cubes identity relates two quantities that can be computed independently: adding the cubes of consecutive positive integers, and squaring the sum of those integers. This practice mission asks for a formal treatment of that known result, together with two supporting identities. Its purpose is to make the definitions, quantifiers, and endpoints explicit enough that each statement can be checked against the supplied mathematical source.

The material is suitable for practicing finite sums and elementary arithmetic in Lean. No research novelty is claimed. The classification is Textbook because the target is a known result; the source for this particular exercise is the statement supplied by the requester, rather than a named textbook chapter or research paper.

Setting

Let $n$ be a natural number, with natural numbers understood to include zero. Define two natural-valued functions:

$$\operatorname{triangleSum}(n)=\sum_{k=1}^{n}k, \qquad \operatorname{cubeSum}(n)=\sum_{k=1}^{n}k^3.$$

Both sums run over the positive integers from $1$ through $n$, including the upper endpoint. An empty sum has value zero, so both functions take the value zero at $n=0$. These are actual finite sums, rather than formulas chosen to make a later theorem hold by definition.

For example, at $n=2$, the first function has value $1+2=3$, and the second has value $1^3+2^3=9$. At $n=3$, their values are $6$ and $36$. These computations clarify the indexing convention. They are examples of the definitions, and the theorem statements below quantify over every natural number without an upper bound.

Formalization targets

Milestone 1: Twice the triangular sum

For every natural number $n$,

$$2\operatorname{triangleSum}(n)=n(n+1).$$

This statement relates the finite sum of consecutive positive integers to a product. It is stated with a factor of two, exactly as supplied, so its formula involves only addition and multiplication of natural numbers.

Milestone 2: Successive squares of triangular sums

For every natural number $n$,

$$\operatorname{triangleSum}(n+1)^2 =\operatorname{triangleSum}(n)^2+(n+1)^3.$$

This statement specifies how the square of the triangular sum changes between consecutive inputs. The term added is the cube of the new endpoint, and the square on the right applies to the entire preceding sum.

Final goal: Sum of cubes identity

For every natural number $n$,

$$\operatorname{cubeSum}(n)=\operatorname{triangleSum}(n)^2.$$

This is the main goal. The two earlier targets are supporting milestones, and the two functions are shared definitions. Each theorem is stated without assuming another target as a hypothesis.

Significance

The result identifies the sum of the first $n$ positive cubes as a perfect square and specifies the natural number whose square it is. Together with the first milestone, it connects the same sum with the product $n(n+1)$. The second milestone records a separate arithmetic identity about consecutive values of the triangular sum, so it remains meaningful as an independently stated result.

The formalization work is to represent the two sums consistently and prove these three universal statements in Lean. The declarations in this proposal are proof targets, with theorem bodies left as placeholders. The proposal does not claim that those placeholders are completed proofs or that server verification has taken place. The shared definitions can be reused in later exercises about sums of positive integers or their powers.

Difficulty

The mathematical content is elementary. The main precision issue is keeping the summation endpoints and arithmetic expressions aligned across the definitions and the three targets. A sum ending at $n-1$ represents a different function; a square applied term by term represents a different quantity. Checking a few concrete inputs can expose transcription errors, but cannot establish a statement that quantifies over all natural numbers.

The zero input also requires consistent treatment. It is part of the domain of every declaration, even though the integers being summed are positive. At that input the definitions are empty sums, and the successor expression in the second milestone refers to the input one. No positivity assumption on $n$ is included or needed in the statements.

Formalization scope

The Lean representation uses natural numbers for inputs, summation indices, and outputs. Each sum is taken over the finite inclusive interval Finset.Icc 1 n. Arithmetic and powers remain in the natural numbers. The statements use no division, subtraction, infinite sums, or coercions into the integers or real numbers.

The declarations share the namespace SumOfCubesPractice. Each definition is kept in its own module, and theorem files import the definitions they use. The required library infrastructure consists of finite sums and finite intervals of natural numbers. The scope consists of two definitions, two supporting milestone theorems, and one main theorem. Completed proofs of those exact statements are the intended mathematical contributions; no extra hypotheses, bounded ranges, or replacement definitions are part of the scope.

Selected references

Source: the requester's supplied statement, definitions, Milestone 1, Milestone 2, and Final goal for “Sum of Cubes Identity (Practice).” No book, paper, author, page number, or external mathematical citation was supplied, and none is attributed to this exercise.

Motivation

A polynomial threshold function makes a Boolean decision by evaluating a real polynomial and keeping only its sign. Its average sensitivity measures how often that decision changes after one uniformly chosen input coordinate is reversed, summed over all coordinate choices. This is a basic quantitative question in the analysis of Boolean functions: how much can a low-degree decision rule vary across the edges of the Boolean cube?

The result collected here is a uniform bound with an explicit coefficient. The OpenAI weighted-grading development supplies a complete coefficient-eight construction. Lagdive, Aglave and Damre sharpen its probability estimate and obtain the sufficient coefficient 3.83. The present fixed-source development formalizes the refined estimate, extracts the coefficient 3.762, and connects it to the full polynomial-threshold statement.

This mission organizes that completed result and its reusable supporting theorems. Its goal and both milestones already have accepted Lean proofs. It does not present the coefficient as optimal, and it makes no claim of exhaustive historical priority.

Setting

Let $n,d$ be positive integers, and let $p$ be a real polynomial in $n$ variables with total degree at most $d$. Choose an input $x$ uniformly from the sign cube $\{-1,1\}^n$. For a coordinate $i$, write $x^{\oplus i}$ for the same input with coordinate $i$ negated. The threshold convention is

$$f(x)=\begin{cases}1,&p(x)\ge0,\\-1,&p(x)<0.\end{cases}$$

In particular, a zero of the polynomial is assigned the positive sign. The average sensitivity is

$$\operatorname{AS}(f)=\sum_{i=1}^{n}\Pr\{f(x)\ne f(x^{\oplus i})\}.$$

For the scalar supporting statements, let $B_n$ have the symmetric binomial distribution with parameters $n$ and $1/2$. Its mean absolute deviation is

$$b_n=\mathbb E|B_n-n/2|=2^{-n-1}\sum_{j=0}^{n}\binom nj|2j-n|.$$

The accompanying definition module fixes this finite sum and the normalized central coefficient $c_k=4^{-k}\binom{2k}{k}$. These definitions contain no estimates or unproved hypotheses.

Formalization targets

Goal — the coefficient 3.762 for arbitrary real polynomials

For every $n,d\ge1$ and every real polynomial of total degree at most $d$, prove

$$\operatorname{AS}(\operatorname{sign}p)\le\frac{1881}{500}\,d\sqrt n.$$

The goal is the published theorem AverageSensitivity.polynomial_bound_3762_general. It has no multilinearity hypothesis and no requirement that $d\le n$. The narrower range $1\le d\le n$ used by the Big O board is therefore included. The goal's fixed coefficient records this particular verified result; a future sharper coefficient would be a separate statement.

Milestone 1 — the refined finite one-sided coupling estimate

Let a finite set carry nonnegative probability weights $w$, and let real functions $U,V$ have identical weighted distributions. Let $m$ be any real centre and let $a\ge0$. If $V-U\le a$ on the support of the weights, prove

$$\mathbb E(U-V)^2\le4a\mathbb E|U-m|+a^2.$$

This is the finite form of the first estimate in Lemma 2 of Lagdive, Aglave and Damre. The centre is arbitrary; independence, exchangeability and a two-sided displacement bound are not hypotheses. Its published formalization is already proved.

Milestone 2 — exact extraction of the universal coefficient

For positive integers $n,d$ and a real number $A$, prove the scalar implication

$$A\le n,\qquad A\le8db_n+2d^2\quad\Longrightarrow\quad A\le\frac{1881}{500}d\sqrt n.$$

This is AverageSensitivity.extract_constant. Its statement is independent of the polynomial and matrix constructions. It records the coefficient extraction proved in this development, rather than attributing 3.762 to the earlier paper.

Significance and current status

The result gives one coefficient that works simultaneously for every positive dimension and degree. Such uniformity distinguishes it from estimates that hold only for a fixed degree or only as the dimension tends to infinity. It also preserves the stated convention at polynomial zeros, so the class of threshold functions is unchanged at the boundary.

The formal contribution is a complete connection from the polynomial and the actual finite cube to the numerical bound. The final theorem does not assume the existence of a grading, an energy bound, a coupling estimate or a small-dimension certificate. Those mathematical components are discharged inside the proof chain. The two supporting milestones are independently importable results, and the live dependency graph records both as actual prerequisites of the goal's accepted reduction.

All three theorem nodes are currently Proved. The closed repository proof was rebuilt with Lean 4.33.1 and the platform's Mathlib revision, and an independent Linux build also passed. The final theorem's axiom dependencies are exactly propext, Classical.choice and Quot.sound. These checks establish the formal result under the displayed definitions; they do not establish optimality of the coefficient or independent human peer review.

Difficulty

A one-sided bound on the difference of two variables does not by itself bound the difference in the opposite direction. The equal-distribution condition is therefore essential to the coupling milestone. Omitting it would change the problem into a false assertion. In the polynomial application, the relevant distributions also have to come from the actual block masses of the constructed grading; treating those masses or the grading properties as free assumptions would omit the central analytic work.

The constant extraction must cover all admissible dimension-degree pairs. A calculation for finitely many dimensions cannot establish the universal statement, while an asymptotic first-moment estimate can leave uncontrolled small dimensions or degree-dependent errors. The formal target includes both the infinite range and every exceptional finite case. Numerical optimization and floating-point experiments are not premises of the accepted result.

Formalization scope

Cube vertices are functions Fin n → Bool, interpreted coordinatewise as signs. A coordinate flip is an explicit function update, and each probability is a finite cardinality divided by $2^n$. The polynomial is a Mathlib MvPolynomial (Fin n) ℝ; the degree bound refers to its total degree. General polynomial inputs are included through a proved value-preserving, degree-nonincreasing multilinearization. Positive dimensions ensure the normalizing denominator is nonzero. Degree zero and dimension zero are outside the displayed goal's quantifiers.

The two definition references provide the original cube/threshold interface and the exact scalar moment interface. The coupling milestone uses finite weighted sums, so equality of distributions is stated for every real test function without additional measurability assumptions. The scalar milestone quantifies over an arbitrary real $A$ satisfying its two explicit upper bounds. The main goal has no analogous auxiliary assumptions.

This is a Research Paper mission for a completed fixed-source development, with the main theorem and both milestones linked by their existing identities. It creates no duplicate theorem statements. Alternative proofs and subsequent sharper bounds can reuse these interfaces, but they are not claimed as completed by this mission. The construction and earlier probability refinement remain attributed to their original sources. Proof development and source preparation used OpenAI Codex.

Selected references

• OpenAI, Average sensitivity of polynomial threshold functions, preprint and Lean source, 2026. Fixed Lean development.
• Prathmesh Lagdive, Vaibhav Aglave and Suraj Damre, An elementary improvement of the average sensitivity bound for polynomial threshold functions, 2026, Lemma 2 and the dimension-degree estimate. Fixed manuscript source.
• Anchen0823, Average sensitivity: a Lean proof with coefficient 3.762, source development, 2026. Verified source revision. Prove2Me accepted main submission: 0f539328-c783-4509-a78e-a86ac777468c.

Extend the sharp diagonal Hlawka formula to smaller exponents.

The foundation mission establishes the least uniform complex coordinate Hlawka constant for every real exponent p ≥ 256. This entry proposes the cutoff 32: the same cyclic constant must be optimal for every real exponent at or above the proposed cutoff, across all finite complex coordinate dimensions and arbitrary triples, including unequal norms.

Use the foundation's unchanged definitions of the coordinate norm, Hlawka constant, and cyclic constant. The goal combines admissibility and uniform optimality in a single IsLeast statement.

Foundation: https://prove2.me/missions/Sharp_diagonal_Hlawka_constants%3A_foundation_and_proved_cutoff_256

Motivation

When a decision rule is announced in advance, people may change the features on which the rule acts. A lender, for example, may offer loans with different probabilities to applicants with different reported characteristics. An applicant then weighs the greater chance of receiving a loan against the cost of changing those characteristics. The decision maker must account for this response when choosing the rule. Tsirtsis and coauthors study this problem with a finite feature set and a policy that specifies the probability of a positive decision at each value.

If moving to a better-outcome feature costs more and moving to a worse-outcome feature costs nothing, the paper shows that at least one optimal policy can be chosen to respect the ordering of outcomes. Section 5 asks what remains of that conclusion when change costs are general. Its three-value example answers the question sharply: an optimal policy exists, but no optimal policy respects outcome monotonicity. The example isolates the role played by the cost assumption in the earlier result. Source, §§4–5

Setting

There are $m$ feature values $x_1,\ldots,x_m$. An individual initially has value $x_i$ with probability $p(x_i)=P(x_i)$. At feature value $x_j$, the probability of a positive underlying outcome is $q(x_j)=P(y=1\mid x_j)$. A decision policy $\pi$ assigns a positive-decision probability $\pi(x_j)\in[0,1]$ to each value. The decision maker incurs a cost $\gamma\in(0,1)$ for a positive decision. This is the paper's base model: the individual benefit is $b(x)=\pi(x)$, and the outcome probability $P(y\mid x)$ does not change when an individual changes features. Source, §2, p. 3, equations (1)–(3)

An individual at $x_i$ may move to $x_j$, paying change cost $c(x_i,x_j)$. Their best response maximizes $\pi(x_j)-c(x_i,x_j)$ over all destinations. If several destinations tie, the paper selects one with the highest outcome probability $q(x_j)$. The resulting population distribution depends on $\pi$. The decision maker's strategic utility is the expected outcome surplus under that response:

$$u_{p,q,\gamma,c}(\pi)=\sum_{i=1}^{m}p(x_i) \bigl(q(\operatorname{br}_{c,q,\pi}(x_i))-\gamma\bigr) \pi(\operatorname{br}_{c,q,\pi}(x_i)).$$

This sum is equation (7) regrouped by each individual's initial value. An optimal policy maximizes it over every policy in $[0,1]^m$. The paper assumes a positive cost for moving to a distinct feature whose outcome is at least as good as the starting feature; its Section 5 matrix meets that assumption. Source, §3, pp. 4–5, equations (5) and (7)

The example has $m=3$, $\gamma=0.1$, $p=(0.1,0.4,0.5)$, and $q=(1,0.7,0.4)$. Rows of the following matrix are starting features and columns are destinations:

$$c=\begin{pmatrix} 0&0.2&0.3\\ 0.3&0&0.7\\ 1.2&1.1&0 \end{pmatrix}.$$

Moving from $x_1$ to the lower-outcome $x_2$ costs $0.2$. That violates the zero-cost requirement for such moves in the paper's outcome monotonic cost definition. A policy is called outcome monotonic here when a larger positive-decision probability implies a larger outcome probability: $\pi(x_i)<\pi(x_j)\Rightarrow q(x_i)<q(x_j)$. Source, §§2, 4–5, pp. 3, 6, 9

Formalization targets

The printed optimal family

For every admissible policy $\pi$ with $\pi(x_1)=1$, $\pi(x_2)\leq0.7$, and $\pi(x_3)=1$, the paper states that $\pi$ is optimal and that individuals initially at $x_2$ move to $x_1$:

$$\forall\pi\in[0,1]^3, \quad\bigl(\pi(x_1)=1\land\pi(x_2)\leq0.7\land\pi(x_3)=1\bigr) \Longrightarrow \bigl(\pi\text{ is optimal}\land\operatorname{br}_{c,q,\pi}(x_2)=x_1\bigr).$$

The endpoint $\pi(x_2)=0.7$ matters: the move from $x_2$ to $x_1$ ties with staying in benefit less cost, and the paper's outcome tie rule chooses $x_1$. Source, §5, p. 9

Goal: no outcome monotonic optimum

The principal target formalizes the Section 5 heading in this fixed instance:

$$\exists\pi\in[0,1]^3:\pi\text{ is optimal}, \qquad \forall\pi\in[0,1]^3:\pi\text{ is optimal}\Longrightarrow \neg\operatorname{OMPolicy}(q,\pi).$$

The existence clause rules out an empty optimal set. This formulation follows the heading's assertion that an outcome-monotonic optimum may fail to exist, while the printed family supplies concrete optima. Source, §5, p. 9

Significance

The result gives an explicit boundary for the earlier outcome-monotonic-policy guarantee. With the Section 5 costs, favoring the lowest-outcome value $x_3$ as much as the highest-outcome value $x_1$ can be optimal, because the response to a published policy changes where population mass receives decisions. Thus a search restricted to outcome-monotonic policies can miss every optimum in a general-cost instance. The milestone on the printed family records a full interval of optimal policies, including its tie endpoint. Source, §§4–5, pp. 6, 9

The paper proves its example informally; this mission asks for a machine-checked account of the fixed instance and the universal quantifiers behind “every” and “no.” The development also yields reusable definitions for finite strategic policies, the outcome-aware best response, and utility. The other missions in this series treat the additive-cost theorem and a stochastic-optimum example separately. No theorem in this mission is presented as an open research problem.

Difficulty

Checking that one displayed policy has high utility is insufficient to establish optimality over every policy in $[0,1]^3$. The best response changes at equality thresholds, so utility is piecewise defined and may jump when the tie rule changes the destination. The closed bound $\pi(x_2)\leq0.7$ makes one such threshold part of the statement. A finite numerical grid misses both arbitrary real policies and the exact tie behavior. The negative goal also requires excluding outcome monotonicity for every maximizer, rather than exhibiting one nonmonotonic maximizer.

Formalization scope

The features are Fin 3 in the example, with Lean indices $0,1,2$ representing $x_1,x_2,x_3$. The general model uses Fin m with a nonempty finite feature set. Probabilities, costs, and utility are real numbers; the example's decimals are exact rational reals. Policies range over all real-valued functions with each coordinate in $[0,1]$, and optimality uses IsMaxOn on precisely that set. The best response is constructed from the maximizers of $\pi(x_j)-c(x_i,x_j)$ and then the largest $q(x_j)$. If tied destinations also have equal $q$, the least index is chosen; the example has distinct outcome probabilities, so this final convention never affects its claims.

Equation (1) prints strict outcome and policy comparisons as a biconditional, although the paper's later policy class permits equal policy values at distinct outcomes. This mission uses its one-way implication from a strict policy comparison to a strict outcome comparison. Failure of this weaker condition is a stronger counterexample than failure of the printed biconditional. The cost definition applies its printed pair and triple comparisons only to distinct values and records $c(x_i,x_i)=0$, as required for free staying. The example's constants satisfy the paper's standing positive-upward-cost assumption. These readings are disclosed so the formal claim has a consistent, nonvacuous model.

A complete proof needs finite argmax reasoning, exact rational inequalities, a case analysis over real policy regions, and the semantics of IsMaxOn. The finite best-response and utility definitions can be reused for other strategic-decision instances. Contributions may establish the printed family, its transport claim, bounds for all admissible policies, or the final exclusion of monotonic maximizers. Policies are never restricted to a grid, and the best response is computed from the model data rather than supplied as a free variable. The paper's algorithms, complexity claims, empirical studies, and changes to $P(y\mid x)$ are outside this mission.

Selected references

• S. Tsirtsis, B. Tabibian, M. Khajehnejad, A. Singla, B. Schölkopf, and M. Gomez-Rodriguez, Optimal Decision Making Under Strategic Behavior, Management Science, 2024. arXiv:1905.09239v5, the source version used here.

Motivation

A component supplier may ask two downstream manufacturers to license their improvements to each other. Sharing raises each product's quality, but it can also reduce a manufacturer's reason to invest in its own improvement. The supplier must choose the licensing rule before those investments and before setting the wholesale price. Wang, Huang, and Lee study this choice in a two-manufacturer supply chain with unequal innovation costs. Their 2023 manuscript identifies cost regions in which the supplier gains from committing to cross-licensing and a region in which the choice depends on a further threshold. The question matters whenever a shared component provider controls a contract that changes both downstream competition and the incentive to improve products.

This mission targets Proposition 4 of the authors' SSRN manuscript, version of 2023-04-27. The appendix of that manuscript contains the proof and the explicit equilibrium formulas used here. The manuscript was later published in Manufacturing & Service Operations Management; the theorem and page labels in this mission belong to the held SSRN version.

Setting

There is one supplier and two manufacturers, $M_1$ and $M_2$. Manufacturer $i$ invests at innovation level $T_i\ge0$ and pays the quadratic cost $k_iT_i^2$. Manufacturer 2 has the lower innovation cost: $49/144<k_2<k_1$. If the manufacturers cross-license with effectiveness $\beta\in[0,1]$, the quality improvements of their products are $T_1+\beta T_2$ and $T_2+\beta T_1$. Without cross-licensing the same model uses $\beta=0$. The market-size intercept is normalized to one and unit production costs to zero, as in Section 3 of the manuscript.

After investment, the supplier selects a nonnegative wholesale price $r$. The manufacturers then choose nonnegative Cournot quantities $q_1,q_2$. Manufacturer $i$'s selling price is $1+T_i+\beta T_j-q_i-q_j$, and its operating profit is $(1+T_i+\beta T_j-q_i-q_j-r)q_i$. The supplier receives $r(q_1+q_2)$. A downstream duopoly has both quantities positive; at a downstream monopoly, only one manufacturer produces. The paper solves this sequence backward and distinguishes two equilibrium investment patterns within the duopoly: an interior outcome $T^I$ and a boundary outcome $T^B$. Their dividing cost is $\hat k_2(k_1\mid\beta)$. The paper's named innovation outcome is $T^B$ for $k_2<\hat k_2(k_1\mid\beta)$ and $T^I$ otherwise.

Write $P(k_2,\beta)$ for the supplier's optimal wholesale revenue at that named innovation outcome. Thus $P(k_2,0)$ is the same downstream model with no licensing. The choice to commit to cross-licensing is determined by comparing these two revenues.

Formalization targets

The three cost regions

Proposition 4 divides admissible $k_2$ into three regions. In the boundary region, licensing weakly benefits the supplier:

$$k_2<\hat k_2(k_1\mid\beta)\quad\Longrightarrow\quad P(k_2,0)\le P(k_2,\beta).$$

The threshold $\hat k_2(k_1\mid\beta)$ decreases as $\beta$ rises, and this boundary region eventually has no admissible $k_2$. In the middle region there is a single threshold $\tilde k_2$, fixed by $k_1$ and $\beta$, below which the supplier weakly prefers licensing:

$$\hat k_2(k_1\mid\beta)\le k_2<\hat k_2(k_1\mid0):\qquad P(k_2,0)\le P(k_2,\beta)\ \Longleftrightarrow\ k_2\le\tilde k_2.$$

In the third region the direction of the threshold reverses. For a threshold $\underline k_2$ fixed by $k_1$ and $\beta$,

$$k_2\ge\hat k_2(k_1\mid0):\qquad P(k_2,0)\le P(k_2,\beta)\ \Longleftrightarrow\ \underline k_2\le k_2.$$

When $\beta\ge2/5$, $P(k_2,\beta)\le P(k_2,0)$ throughout that last region. All three displays are restricted to $49/144<k_2<k_1$. The full proposition is the mission goal. The milestone list records the paper's threshold monotonicity, the two explicit supplier-profit formulas, and the cost-region facts used to state the comparison.

Significance

The result makes the supplier's contract decision depend on both innovation asymmetry and the effectiveness of sharing. It separates the direct benefit of higher quality from the loss associated with weaker investment incentives. In particular, the supplier can benefit from cross-licensing when the superior manufacturer's cost is low enough for a boundary investment outcome, yet full effectiveness does not make licensing uniformly attractive. These conclusions are specific to the supplier's choice before investment; the paper's earlier ex post comparison holds the innovations fixed and addresses a different decision.

The mathematical result is already proved in the authors' appendix. The work here is to formalize its exact conditions and the optimization value being compared, then obtain a machine-checked proof. A development can reuse the Cournot quantity response, wholesale-price optimization, and piecewise investment formulas for the paper's later welfare and manufacturer-profit results. The local draft theorem statements compile in Lean; the results themselves remain open proof obligations.

Difficulty

The supplier's price can change which manufacturers remain active, and the manufacturers choose investments while anticipating that price response. A simple comparison of demand intercepts at fixed investments therefore does not decide the initial contract: the investments on the two sides of the comparison can differ, and a cost change can move one side across the boundary between the two equilibrium regimes. The paper expresses the outcomes with rational functions containing $\sqrt3$ and analyzes three regions separated by $\hat k_2(k_1\mid\beta)$ and $\hat k_2(k_1\mid0)$. A faithful formalization must also preserve the order of quantifiers: each single-crossing threshold is chosen once for fixed $k_1,\beta$, before $k_2$ ranges over its region.

Formalization scope

The Lean model uses real parameters and explicit pairs ordered as $M_1,M_2$. It encodes the paper's displayed quantity formula for $T_2\ge T_1$, with $q_i,T_i,r\ge0$ and $0\le\beta\le1$. Its standing cost condition is $49/144<k_2<k_1$. The wholesale-price domain $r\ge0$ makes explicit the economic domain implicit in the manuscript. The two displayed investment formulas use Real.sqrt 3; no decimal approximation enters a statement. The named innovation outcome follows page A.2: boundary below $\hat k_2$, interior otherwise. A separate mission targets its Nash-equilibrium characterization.

Most importantly, the supplier's optimal profit is the supremum of actual revenue over nonnegative prices at that innovation outcome. It is not defined to equal either closed form; a milestone asserts that the maximum is attained and identifies its value. This prevents the preference theorem from becoming a comparison true only by definition. The $\tilde k_2$ and $\underline k_2$ thresholds are existential single-crossing statements because the latter's printed formula on page A.3 is malformed. The proof's weak profit comparisons determine the formal inequality. At $\beta\ge2/5$, the statement uses interior profit on both sides, correcting an apparent $\pi_s^B(\beta)$ slip in the final sentence of the proof.

Useful contributions include a proof of the attained supplier optimum, denominator positivity over the standing domain, exact inequalities involving $\sqrt3$, and the two single-crossing results. The general price-optimization facts and market-response lemmas can be reused beyond this mission.

Selected references

• J. Wang, T. Huang, and J. Lee, Cross-licensing in a Supply Chain with Asymmetric Manufacturers, SSRN manuscript 3053682, version of 2023-04-27, Proposition 4 and Appendix A.1–A.3. SSRN.
• J. Wang, T. Huang, and J. Lee, Cross-licensing in a Supply Chain with Asymmetric Manufacturers, Manufacturing & Service Operations Management, 2023. DOI: 10.1287/msom.2019.0477.

Motivation

Many consequential decisions, such as lending, hiring or admissions, are made by policies that map an individual's features to a probability of a positive decision. When the policy is published, individuals respond to it: they change their features, at a cost, to raise their chance of a positive decision. Tsirtsis, Tabibian, Khajehnejad, Singla, Schölkopf and Gomez-Rodriguez (arXiv:1905.09239, Management Science 2024) model this as a Stackelberg game and ask which policy maximizes the decision maker's utility once individuals best respond.

In the classical, non-strategic setting, where features do not react to the policy, the optimal policy is a deterministic threshold rule: decide positively exactly when the probability of a good outcome is at least a cost constant $\gamma$ (Corbett-Davies et al., KDD 2017; Valera, Singla and Gomez-Rodriguez, NeurIPS 2018). The paper shows that strategic behaviour breaks this picture. A three-value example in §3 (p. 5) exhibits an instance whose costs satisfy the natural outcome monotonicity condition and whose optimal policy is nevertheless stochastic. This mission formalizes that example.

Setting

There are $m$ feature values $x_1,\dots,x_m$, a feature distribution $P(x)$, an outcome probability $P(y=1\mid x)$, a constant $\gamma\in(0,1)$, and a cost $c(x_i,x_j)\ge0$ of changing from $x_i$ to $x_j$.

• A policy $\pi$ assigns to each feature value a probability $\pi(x)=\pi(d=1\mid x)\in[0,1]$ of a positive decision. The individual benefit is $b(x)=\pi(x)$.
• An individual starting at $x_i$ moves to a best response

$$x_j\in\operatorname*{argmax}_{k}\ \pi(x_k)-c(x_i,x_k)\qquad(5),$$

with ties broken toward the feature value with the highest $P(y\mid x_j)$ (standing assumption (ii)).

• The strategic utility is

$$u(\pi,\gamma)=\sum_{i}P(x_i)\,\bigl(P(y=1\mid x_{\mathrm{br}(i)})-\gamma\bigr)\,\pi(x_{\mathrm{br}(i)})\qquad(7),$$

and a policy is optimal if it maximizes $u$ over all policies.

• The non-strategic utility $u_{\mathrm{NS}}(\pi,\gamma)=\sum_x P(x)(P(y=1\mid x)-\gamma)\pi(x)$ is the same quantity when nobody moves.
• A cost is outcome monotonic (p. 6) if improving one's outcome requires increasing effort and worsening it requires none.

The instance of §3 has $x\in\{1,2,3\}$, $\gamma=0.1$, $P(x)=(0.1,0.4,0.5)$, $P(y=1\mid x)=(1.0,0.7,0.4)$ and

$$c(x_i,x_j)=\begin{pmatrix}0&0&0\\0.3&0&0\\1.2&0.3&0\end{pmatrix},$$

row $i$ being the origin. In Lean the feature values $1,2,3$ are Fin 3 indices $0,1,2$; the model lives in the namespace StrategicPolicy.StochasticOpt, with Policies, br, u, uNS, OMCost, StandingI and the instance γ0, p0, q0, c0.

Formalization targets

Goal: the optimal policies of the §3 instance

$$\pi\ \text{optimal}\iff \pi(x=1)=1,\ \pi(x=2)=0.7,\ \pi(x=3)\le 0.4,$$

every optimal policy is non-deterministic, and $u\bigl((1,0.7,0),\gamma\bigr)=0.66$. The paper prints a single optimal policy, $(1,0.7,0)$; the optimum is not unique, and the goal states the exact optimal set, which contains the printed policy and makes the "stochastic" claim a statement about every optimum.

Milestones

1. The instance's cost is outcome monotonic and satisfies standing assumption (i).
2. The non-strategic optimum is unique and equals the threshold policy $(1,1,1)$.
3. Under $\pi^*=(1,0.7,0)$ the individuals at $x=3$ move to $x=2$ and those at $x=2$ move to $x=1$.
4. $u_{\mathrm{NS}}((1,1,1))<u(\pi^*)$ and $u((1,1,1))<u(\pi^*)$: the strategic optimum beats its non-strategic counterpart under either reading of "counterpart".

Significance

The example separates two regimes. Without strategic behaviour the optimum is a deterministic threshold rule; with it, randomization is strictly necessary, even under the cost structure (outcome monotonicity) that the paper later uses to restrict the search for optimal policies to a structured family (Proposition 2, Theorem 3). It is the concrete witness for the paper's claim that "optimal decision policies are not always deterministic threshold rules", and it shows that the outcome monotonic binary policies of Theorem 3 must include fractional values such as $0.7=1-0.3$.

The paper reports the optimum from "a brute force search", that is, numerically. A formal proof replaces the search by an argument valid over the whole continuum $[0,1]^3$, determines the full optimal set rather than one optimizer, and certifies the tie-breaking at both thresholds. No part of this paper has a machine-checked proof that this mission is aware of.

Difficulty

The utility is piecewise linear in $\pi$ but discontinuous: it jumps whenever a best response switches, and the switching surfaces are exactly where the optimum sits. At $\pi(x=2)=0.7$ the individuals at $x=2$ are indifferent between staying and moving to $x=1$, and at $\pi(x=3)=0.4$ those at $x=3$ are indifferent between staying and moving to $x=2$. The optimum is attained only because tie-break (ii) resolves both indifferences upward. Checking finitely many candidate policies proves nothing about the rest of $[0,1]^3$, and a naive concavity or first-order argument does not apply to a discontinuous objective. An upper bound must hold for every policy, across all configurations of best responses.

Formalization scope

• Policies are functions Fin 3 → ℝ with values in $[0,1]$; optimality is IsMaxOn u (Policies 3) π, over the whole cube, never over a grid or over deterministic policies.
• The best response br is computed from $\pi$, $c$ and $P(y\mid x)$ as the maximizer of (5) with the highest outcome, then the least index; it is never a free function constrained by hypotheses. With the instance's distinct outcomes the least-index rule never fires.
• The model is the paper's base model: $b(x)=\pi(x)$, and $P(y\mid x)$ is unchanged by best responses (§2). Standing assumption (i) and outcome monotonicity are proved for the instance (milestone 1), not assumed.
• Outcome monotonicity is imposed for distinct feature values together with $c(x,x)=0$, since the printed zero-cost equivalence at $i=j$ would forbid free staying.
• All numbers are exact rationals ($1/10$, $7/10$, $2/5$, $6/5$, $3/10$).
• A formalization that states only "$(1,0.7,0)$ is optimal", or optimality against finitely many policies, would drop the stochasticity claim or trivialize the goal; neither is posed.
• Out of scope: Theorem 1 (NP-hardness), Proposition 2 and Theorem 3 (the structural results, mission 1 of this series), the general-cost example of §5 (mission 3), the algorithms and the experiments.

Needed infrastructure is small: finite sums over Fin 3, Finset.filter, Finset.min'. Lemmas evaluating br on regions of the policy cube are reusable across the series' examples.

Selected references

• S. Tsirtsis, B. Tabibian, M. Khajehnejad, A. Singla, B. Schölkopf, M. Gomez-Rodriguez, Optimal Decision Making Under Strategic Behavior, Management Science, 2024; read as arXiv:1905.09239v5, 2020. https://arxiv.org/abs/1905.09239v5
• S. Corbett-Davies, E. Pierson, A. Feller, S. Goel, A. Huq, Algorithmic Decision Making and the Cost of Fairness, KDD 2017. https://doi.org/10.1145/3097983.3098095
• I. Valera, A. Singla, M. Gomez-Rodriguez, Enhancing the Accuracy and Fairness of Human Decision Making, NeurIPS 2018. https://arxiv.org/abs/1805.10318
• M. Hardt, N. Megiddo, C. Papadimitriou, M. Wootters, Strategic Classification, ITCS 2016. https://doi.org/10.1145/2840728.2840730

Motivation

A lender or other decision maker may publish a rule that assigns a positive decision to an individual with some probability. Once the rule is visible, individuals can change the features on which it acts. The decision maker must therefore evaluate a rule under the distribution it induces after individuals respond, rather than only under the original population. Tsirtsis and coauthors study this problem with finitely many feature values and a cost for changing from one value to another. Their preprint gives a utility model, a best response rule, and structural results for costs that respect the ordering of outcomes.

This mission isolates Theorem 3 of that preprint. It asks whether, under additive and outcome monotonic costs, an optimal decision rule can be found among policies with a particular binary choice at each relevant feature value. The result concerns the structure of an optimum. It does not assert that an arbitrary starting policy is itself binary or that every optimum has this form.

Setting

There are $m\ge1$ feature values $x_1,\ldots,x_m$, indexed from highest to lowest positive-outcome probability. Write $p_i=P(x_i)$ for their original population masses and $q_i=P(y=1\mid x_i)$ for their outcomes. The masses are nonnegative and sum to one, $q_i\in[0,1]$, and the outcomes are distinct in this mission. A policy $\pi$ chooses a positive decision at $x_i$ with probability $\pi_i\in[0,1]$. Each positive decision costs the decision maker $\gamma\in(0,1)$.

An individual originally at $x_i$ can move to $x_j$ at change cost $c_{ij}$. In the paper's base model, the individual's benefit at a destination is $\pi_j$, so she maximizes $\pi_j-c_{ij}$. Ties go to a destination with higher $q_j$. If a tie remains, the formalization picks the smallest index. Write $r_\pi(i)$ for this best response. The outcome probabilities $q_j$ themselves do not change after the response; the response changes where the population mass is counted. The decision maker's utility is

$$u(\pi,\gamma)=\sum_{i=1}^{m}p_i\bigl(q_{r_\pi(i)}-\gamma\bigr)\pi_{r_\pi(i)}.$$

A policy is outcome monotonic here when $\pi_i<\pi_j$ implies $q_i<q_j$. An outcome monotonic cost obeys the paper's two conditions for distinct feature values: improving outcome through successive values has the specified strict cost ordering, and a move to a lower outcome has zero cost. An additive cost satisfies $c_{ij}+c_{jk}=c_{ik}$ when $q_i<q_j<q_k$. Staying costs zero. The section's standing assumption also makes a distinct move toward a weakly higher outcome cost strictly positive.

Formalization targets

Main goal: Theorem 3

If $\pi^*$ maximizes utility among all policies in $[0,1]^m$, and the cost is additive and outcome monotonic, then some outcome monotonic policy $\pi$ has $u(\pi,\gamma)=u(\pi^*,\gamma)$ and satisfies

$$\pi_i=\pi_{i-1} \quad\text{or}\quad \pi_i=\max\{0,\pi_{i-1}-c_{i,i-1}\} \qquad(i>1,\ q_i>\gamma).$$

The paper calls this an outcome monotonic binary policy. Binary describes the two allowed relationships between adjacent policy values; the probabilities themselves can be fractional. The goal is conditional on a maximizer $\pi^*$, exactly as Theorem 3 is stated. The preprint does not establish that an optimum always exists, and its best response tie thresholds make that question separate.

Milestones

The first milestone records the observation following Proposition 2: under an outcome monotonic policy, an individual never selects a destination with lower outcome than the origin. Proposition 2 then states that some outcome monotonic policy attains the utility of an optimal policy under outcome monotonic costs. The final two milestones formalize the two individual policy changes stated in Appendix A.3, one when a policy value lies between its predecessor and the cost threshold, and one when it lies below that threshold.

Significance

Theorem 3 narrows a continuous search over policy probabilities to a structured family without losing the optimal value, provided an optimum exists. The restriction depends on how feature changes affect the induced population distribution. It is therefore a statement about decision making with strategic responses, not merely about sorting policy values by outcome. Proposition 2 is independently useful: under outcome monotonic costs, the optimal utility can be attained by an outcome monotonic policy even without additivity.

The result is proved in the cited preprint, while the proposed Lean declarations are open proof targets. A complete formalization would make the finite best response rule, the tie convention, and the cost assumptions explicit, then give checked proofs of the structural claims. The definitions of the policy space, response rule, and induced utility may also support later work on the same paper's stochastic examples and algorithms. No machine-checked proof of these proposed statements is claimed here.

Difficulty

The utility depends on a best response selected by an argmax, so changing one policy probability can switch the destination of several population groups at once. The utility need not vary continuously across tie thresholds. A naive coordinate adjustment that improves the outcome probability at one destination can alter who moves there and change the contribution from other origins. This is why a direct appeal to monotonicity of the displayed sum does not establish Proposition 2 or Theorem 3.

The Appendix A.3 statements identify two threshold regimes for a policy value. Their comparisons must account for the tie rule and for all origins whose selected destination changes. The mission keeps these comparisons as separate targets because the conclusion about the whole policy depends on them.

Formalization scope

Lean represents the features by Fin m, with Lean index $0$ standing for $x_1$. The model requires $m>0$ so that the best response has a value. The initial distribution and the conditional outcome probabilities are real valued, with explicit probability bounds. Policies range over the full cube $[0,1]^m$. The best response is computed from the policy and cost, with the highest-outcome tie rule; it is not supplied as independent data. Optimality means membership in that cube and maximal utility over that cube.

The formalization records several readings needed to make the preprint's displays consistent. Formula (1) prints a strict biconditional, but formula (9) allows equal adjacent policy values, so policy monotonicity is the implication from a strictly larger policy value to a strictly larger outcome. The cost equivalences apply to distinct values; staying is free. Additivity applies along strictly improving outcome chains, since an all-triples equality would conflict with positive improvement cost. Outcomes are assumed distinct, as needed for this version of Theorem 3. These choices are stated on the definition item and checked against the source in the moderation notes.

The goal retains the optimal-policy hypothesis and every clause of the binary property. It cannot be satisfied by defining the best response arbitrarily, shrinking the policy set to a selected candidate, or asserting only that a binary policy exists. The model covers the paper's base case $b(x)=\pi(x)$ with unchanged $P(y\mid x)$. The algorithms, complexity claims, experiments, and the paper's other examples are outside this mission. Contributions on the best response interface, finite optimization lemmas, Proposition 2, and either Appendix comparison are welcome.

Selected references

• S. Tsirtsis, B. Tabibian, M. Khajehnejad, A. Singla, B. Schölkopf, and M. Gomez-Rodriguez, Optimal Decision Making Under Strategic Behavior, arXiv:1905.09239v5, 2020, §§2–4 and Appendix A.2–A.3; published in Management Science, 2024. arXiv preprint