Why payment timing matters

A retailer can pay a supplier when it places an order or after the supplier delivers it. When production yield is uncertain, the choice changes who bears the cost of missing units. It can also change the supplier's production decision and, through the amount available for sale, the surplus received by consumers. Geng, Guo, Xiao and Yang study these effects in a decentralized supply chain and show that payment postponement can help all three parties, hurt all three, or benefit some while hurting others, depending on production cost and the retailer's pricing rule. Their Proposition 4 gives the precise cost intervals for these outcomes in the SSRN author version, pp. 19–20.

The result matters to contract design in supply chains where realized output can be below planned production. Paying for units ordered and paying for units delivered allocate that shortage differently. A comparison based only on the retailer's expected profit would miss the effects on the upstream supplier and final consumers. Proposition 4 keeps all three outcomes visible while holding the retailer's pricing policy fixed.

The supply-chain game

There is one supplier and one retailer. The supplier chooses a wholesale price $w$ and plans production $Q$ at cost $cQ$. The retailer orders $q$ and sells to a market with linear demand $d(p)=a-bp$, where $a,b>0$ and $p$ is the retail price. The yield factor $Y$ equals $1$ with probability $\theta$ and $\alpha$ with probability $1-\theta$, with $0<\alpha,\theta<1$. Thus $\mu=\mathbb E Y=\alpha(1-\theta)+\theta$. The retailer receives $\widehat q=\min\{YQ,q\}$ units; the production cost applies to planned $Q$, including units lost to yield risk §3.1–3.2.

Under pay-by-order, the retailer transfers $wq$ to the supplier and the supplier produces $Q=q$. Under pay-by-delivery, the transfer is $w\widehat q$ and the supplier can choose a larger production quantity. Under ex ante pricing, the retailer fixes $p$ before yield is known. Under responsive pricing, the retailer sets $p$ after observing delivery. Combining payment and pricing gives OA (order, ex ante), OR (order, responsive), DA (delivery, ex ante), and DR (delivery, responsive). The supplier first sets $w$, the retailer next orders and possibly fixes a price, the supplier chooses production, yield is realized, and responsive pricing occurs last Table 1, p. 9.

Both firms maximize expected profit at every stage. A subgame-perfect equilibrium is a complete plan of choices after every history in which each choice is optimal at that history. For scenario $k$, write $\pi_R^k$ and $\pi_S^k$ for equilibrium retailer and supplier profit. The consumer surplus $CS^k$ is expected surplus from sales: for delivered stock $X$ and market price $p$, the model integrates inverse demand less $p$ from zero to $\min\{d(p),X\}$. This is the paper's priority allocation convention for consumers with the highest willingness to pay p. 10.

Formalization targets

The main target is Proposition 4, which compares OA with DA and OR with DR. Let $\Delta(\pi_R,\pi_S,CS)$ mean the delivery-payment outcome minus its order-payment counterpart. A plus sign below means a strict increase, a minus sign a strict decrease, and zero equality. The admissible cost range is $0<c<a\mu/b$.

For ex ante pricing, with no restriction $\alpha\ge9/16$, the paper gives a threshold $0<\overline C<c^{DA}$ and the following pattern:

$$\begin{array}{c|c} \text{cost interval}&\operatorname{sign}\Delta(\pi_R,\pi_S,CS)\\ (\max\{0,c^{OA}_2\},\max\{\overline C,c^{OA}_2\}) &(+,+,+)\\ (\max\{\overline C,c^{OA}_2\},c^{DA}) &(+,+,-)\\ (0,\max\{0,c^{OA}_1\})\text{ or }(c^{DA},a\mu/b)&(0,0,0). \end{array}$$

For responsive pricing, assuming $\alpha\ge9/16$, the pattern is $(+,+,+)$ on $(0,\widetilde C)$, $(-,-,-)$ on $(\widetilde C,c^{DR}_1)$, $(+,-,+)$ on $(c^{DR}_1,c^{DR}_2)$, and $(0,0,0)$ on $(c^{DR}_2,a\mu/b)$. The thresholds are those specified in the paper: $\widetilde C$ is equation (6), $\overline C$ is equation (8), and the scenario cost thresholds come from Appendix B. The first ex ante interval can be empty for some parameters; its printed endpoints are retained. The milestones establish the supplier's production and responsive pricing rules, the four scenario outcomes, and the threshold ordering used in the comparison Appendices B–C.

What the result provides

The theorem separates the effect of changing the payment contract from the effect of changing the pricing rule. For advance pricing it identifies an interval where payment postponement helps both firms and consumers, then an interval where consumers lose despite both firms gaining. For responsive pricing the direction of every effect can reverse as cost passes successive thresholds. At high cost the change in payment timing leaves all three equilibrium outcomes unchanged Proposition 4, pp. 19–20.

The paper derives the equilibrium formulas in Appendix B and proves the comparisons in Appendix C. The result is therefore a known mathematical claim, while this mission asks for a machine-checked development from the sequential game through the cost-dependent equilibrium outcomes and final comparisons. The definitions of a two-point yield game and its complete contingent strategies can support other formal studies of payment or pricing postponement. There is no claim that Proposition 4 already has a machine-checked proof.

Where the formal work is difficult

The supplier's production payoff has kinks at $Q=q$ and $Q=q/\alpha$. The retailer's best order changes when those production choices change, and responsive pricing adds another kink when delivered stock crosses $a/2$. As wholesale price varies, the supplier must compare outcomes on both sides of these changes. Consequently a single first-order condition for a smooth objective does not characterize the equilibrium. The cost thresholds also depend on square roots and comparisons among several formula pieces, including the larger root chosen for $c^{OA}_2$ Appendix B, pp. 33–37.

Formalization scope

Lean represents expectation by the two weighted yield outcomes. Production cost $c$ is a separate argument, so thresholds depend only on $(a,b,\alpha,\theta)$. Parameters satisfy $a,b>0$, $0<\alpha,\theta<1$, and $0<c<a\mu/b$. Wholesale and retail prices obey the strict admissibility bounds of equation (3). Orders are nonnegative; pay-by-delivery production is nonnegative; pay-by-order production equals the order. Consumer surplus is a real interval integral. Every comparison quantifies over actual subgame-perfect equilibria, and the goal separately asserts that the compared equilibria exist at every admissible cost. Equilibrium profits are computed from strategies and transfers, rather than defined to equal the Appendix B formulas.

The paper's statements require care at ties. The model selects $Q=q$ when that is a profit-maximizing pay-by-delivery production choice, including the indifferent DR regime. The printed middle DR consumer-surplus expression combines outcomes from different production choices; the equilibrium-consistent expression is used here, and Proposition 4(R)'s comparison remains valid under either expression. Equation (2) swaps the scenario labels of committed and responsive prices, so consumer surplus uses the actual ex ante price in OA and DA and the price after delivery in OR and DR. The printed $[x]^+$ in Appendix B.1 is read as $\max\{0,x\}$, as in Lemma 1. Outcome claims use open cost intervals because uniqueness at exact thresholds fails; equilibrium existence remains part of the targets there. The threshold $c^{OA}_2$ is the larger root of the relevant quadratic factor, and $\overline C$ and $\widetilde C$ use the paper's explicit formulas. These conventions are recorded in the local moderation notes.

The development calls for real inequality reasoning, optimization of piecewise objectives, and careful handling of interval integrals. Contributions that prove the production and price best responses, establish the four equilibrium lemmas, or verify the threshold order each advance the final comparison.

Selected references

• X. Geng, X. Guo, G. Xiao and N. Yang, Supply Risk Mitigation in a Decentralized Supply Chain: Pricing Postponement or Payment Postponement?, Manufacturing & Service Operations Management 25(3), 2023. SSRN author version 3546872; DOI: 10.1287/msom.2022.0198.

Motivation

A retailer that buys from a supplier with unreliable production has two contractual levers against supply risk, and both postpone a decision until after the yield is known. Payment postponement means paying only for the units actually delivered (pay-by-delivery) instead of the units ordered (pay-by-order). This moves the yield risk upstream. Pricing postponement means setting the retail price after the delivery is observed (responsive pricing) instead of committing to it in advance (ex ante pricing). This moves the risk downstream to consumers. Both practices are common in procurement, and the natural intuition is that two ways of shedding the same risk should be substitutes: once one lever is in use, the other should be worth less.

Geng, Guo, Xiao and Yang (MSOM 25(3), 2023; author version SSRN 3546872) compute the subgame-perfect equilibria of all four combinations of the two levers in a stylized supplier–retailer game. Their Proposition 3 shows that the intuition fails at intermediate production cost. When full yield is likely and yield loss is mild, the two postponements are complements there: postponing payment is worth more when pricing is also postponed. This mission formalizes that result together with the four equilibrium characterizations it rests on.

Setting

A supplier sells one product to a retailer, who sells it in a market with linear demand $d(p)=a-bp$, $a,b>0$. The supplier plans production $Q$ at unit cost $c$ and realizes the fraction $Y$ of it, where

$$Y=1 \text{ with probability } \theta,\qquad Y=\alpha \text{ with probability } 1-\theta,\qquad 0<\alpha,\theta<1,$$

and $\mu=\alpha(1-\theta)+\theta$ is the mean yield. The retailer orders $q$ and receives $\hat q=\min\{YQ,q\}$.

The four scenarios are OA, OR, DA and DR. The first letter is the payment rule: by order (O, the transfer is $wq$) or by delivery (D, the transfer is $w\hat q$). The second letter is the pricing rule: ex ante (A, the price is fixed before the yield) or responsive (R, the price is set after $\hat q$ is observed). Each scenario is a sequential game. The supplier posts a wholesale price $w$. The retailer orders $q$, and also commits to a price $p$ in the ex ante scenarios. The supplier then chooses $Q$; under pay-by-order it produces exactly $q$. The yield realizes, and under responsive pricing the retailer then sets $p$. The retailer earns $p\min\{d(p),\hat q\}$ minus the transfer, and the supplier earns the transfer minus $cQ$. Both are risk neutral. Admissible actions follow the paper's standing ranges: $0<c<a\mu/b$, $0<p<a/b$, and $w$ between $c$ (or $c/\mu$ under pay-by-delivery) and $a/b$.

Write $\pi^k_R$ for the retailer's expected profit in a subgame-perfect equilibrium of scenario $k$. The paper's Definition 1 measures the interaction of the two postponements by

$$V=\big(\pi^{DR}_R-\pi^{OR}_R\big)-\big(\pi^{DA}_R-\pi^{OA}_R\big):$$

the value of payment postponement under responsive pricing, minus its value under ex ante pricing. The postponements are substitutes if $V<0$ and complements if $V>0$.

The parameter region of the result is $\alpha\ge 9/16$ together with $\mathcal H_3=\{\theta_2(\alpha)<\theta<1\}$, where $\theta_2(\alpha)$ is the largest real root of the cubic $-\alpha^3+\alpha^2(5+\alpha)x+(16-19\alpha-6\alpha^2)x^2-25(1-\alpha)x^3$. The cost thresholds $c^{DR}_1<c^{DR}_2$ (scenario DR) and $c^{DA}$ (scenario DA) are explicit algebraic functions of $(a,b,\alpha,\theta)$ given in the paper's Appendix B.

Formalization targets

Goal: Proposition 3

For $\alpha\ge9/16$ and $(\alpha,\theta)\in\mathcal H_3$, every scenario has an equilibrium at every cost $0<c<a\mu/b$, and there is a cost $0<\hat C<a\mu/b$ such that, at every choice of the four equilibria,

$$V<0 \text{ on } (0,c^{DR}_1)\cup(\hat C,c^{DA}),\qquad V>0 \text{ on } (c^{DR}_1,\hat C),\qquad V=0 \text{ on } (c^{DA},a\mu/b).$$

$\hat C$ is existential, as in the paper, and depends only on the parameters.

Milestones

• the supplier's production response (4) under pay-by-delivery and the ex post price (5);
• Lemmas 1–4: existence of the equilibrium of each scenario, and its outcome $(\pi_R,\pi_S,CS)$ in closed form on each cost interval;
• Lemma 1(i): on $\mathcal H_3$ the threshold $c^{OA}_2$ is nonpositive, so scenario OA has one regime;
• the threshold claims of Appendix C: $c^{OR}<0$ and $c^{DR}_1<c^{DR}_2<c^{DA}$ for $\alpha\ge9/16$.

Significance

The result separates the first-order question (which lever the retailer prefers, the subject of the paper's Proposition 2) from the second-order one (whether one lever raises the value of the other). It shows that two risk-shifting instruments can reinforce each other. On $(c^{DR}_1,\hat C)$, adopting one postponement raises the value of the other. So whenever the retailer gains from adopting either lever alone, it gains even more from adopting both. Below $c^{DR}_1$ and above $\hat C$ the reverse holds. Above $c^{DA}$, payment postponement is irrelevant, because the supplier never inflates production there.

The paper proves Lemmas 1–4 by backward induction in Appendix B and the proposition by comparing closed forms in Appendix C. None of it is machine-checked. A formal proof requires the four backward inductions with every kink and tie handled, and the polynomial inequalities between the thresholds over the parameter region. The formalization also corrects the record: the paper's explicit formula (7) for $\hat C$ does not locate the sign change of $V$ (at $(\alpha,\theta)=(0.6,0.75)$ it exceeds $c^{DA}$), while the existential statement of Proposition 3 holds at every sampled point.

Difficulty

Once Lemmas 1–4 are available, $V$ is a difference of explicit piecewise functions of $c$. The difficulty lies in those lemmas and in the thresholds. Each lemma is a three-stage optimization. The supplier's profit is piecewise linear in $Q$, with kinks at $q$ and $q/\alpha$. The retailer's profit is piecewise in $(q,p)$, with kinks where it becomes worth inflating the order. The supplier's value function in $w$ is piecewise quadratic, and its maximum can sit at a kink. In scenario DR it sits exactly at the price where the supplier is indifferent to inflating production. A naive reading of the paper's tie rule removes the equilibrium there altogether. On the middle DR interval the sign of $V$ changes inside the interval, at a root of a polynomial with nested square roots. On the other pieces, the signs of $V$ and the ordering $c^{DR}_1<c^{DR}_2<c^{DA}$ are polynomial inequalities in $(\alpha,\theta)$, with $\theta_2(\alpha)$ defined implicitly as a cubic root.

Formalization scope

• Parameters and cost. The parameters $(a,b,\alpha,\theta)$ form a structure. The cost $c$ is a separate argument, and every threshold depends on the parameters only.
• Expectation. The expectation over the yield is the explicit two-point sum $\theta f(1)+(1-\theta)f(\alpha)$.
• Equilibrium. Strategies are functions of all earlier moves, and optimality is required at every node over the full admissible action sets.
• Production ties. Under pay-by-delivery the supplier's production is a best response. When producing exactly $q$ is optimal, it produces $q$. The paper's display (4) assigns that tie to inflation, but under that rule scenario DR has no equilibrium for intermediate cost. The convention reproduces the paper's DR profits.
• Consumer surplus. It is the integral $\int_0^{\min\{d(p),\hat q\}}(p(t)-p)\,dt$. It uses the ex post price in the responsive scenarios and the committed price in the ex ante ones; the labels of the paper's display (2) are swapped.
• Closed forms. Two printed consumer-surplus values are corrected to the equilibrium values: the middle piece of OA ($8b\alpha^2$ for $8b\alpha^3$) and the middle piece of DR (one factor $\alpha^2(1-\theta)+\theta$ fewer).
• Cost intervals. Every statement is on open cost intervals, because at a threshold the outcome is not unique.
• Thresholds. $c^{OA}_2$, "the second root" of a quartic, is the larger root of the quadratic factor that defines it. $\theta_2$ is the supremum of the cubic's real roots, a finite nonempty set.

The equilibrium profits are outcomes of the equilibrium predicate. They are never defined by their closed forms, and the goal carries the existence of an equilibrium in each scenario. Without that, the comparison would be vacuous whenever the predicate is unsatisfiable.

Every object is elementary: real arithmetic, square roots, min/max, one interval integral and one sSup. The equilibrium predicate and the four lemmas are shared with the three companion missions of this paper (Propositions 2, 4 and 5). Proofs of the lemmas, of the threshold inequalities and of the goal are all welcome.

Selected references

• X. Geng, X. Guo, G. Xiao, N. Yang, Supply Risk Mitigation in a Decentralized Supply Chain: Pricing Postponement or Payment Postponement?, Manufacturing & Service Operations Management 25(3), 2023. https://doi.org/10.1287/msom.2022.0198 ; author version SSRN 3546872, https://ssrn.com/abstract=3546872

Motivation

Machine-learning systems are increasingly placed beside human experts — physicians reading scans, loan officers screening applications, judges assessing risk — rather than replacing them. The machine processes the structured data it can see; the human also has access to information the algorithm cannot observe, but her attention is limited. Whether such a partnership improves the decision is a question about how the human reallocates scarce cognitive effort once part of the information is handed to her for free.

Boyacı, Canyakmaz and de Véricourt (ESMT Working Paper 20-02, 2020; published in Management Science, 2024) model the human as a rationally inattentive decision-maker in the sense of Sims (2003): she chooses how much information to process, and pays a cost proportional to the mutual information between the state and her decision. In the binary-choice setting, Matějka and McKay (2015) showed that such problems reduce to choosing conditional choice probabilities, with logit-form solutions. The paper uses this reduction to compare a decision-maker who decides alone with one who first sees a machine's assessment. This mission formalizes its first comparison, Proposition 1: the machine never lowers the decision-maker's accuracy or her expected value.

Setting

A decision-maker (DM) must announce whether the state of the world $\omega\in\{g,b\}$ is good ($a=y$) or bad ($a=n$). A correct choice pays $1$, an incorrect one $0$. Her prior that the state is good is $\mu\in[0,1]$, and $\lambda\ge0$ is the information cost.

A strategy is a pair $(p_g,p_b)\in[0,1]^2$ of conditional probabilities of choosing $y$ in state $g$ and in state $b$. It induces the choice probability $p=\mu p_g+(1-\mu)p_b$, the accuracy $A=\mu p_g+(1-\mu)(1-p_b)$, the cognitive cost

$$C=\lambda\big[H(p)-(1-\mu)H(p_b)-\mu H(p_g)\big],\qquad H(x)=-x\log x-(1-x)\log(1-x),$$

(the mutual information between state and action, in nats) and the expected value $V=A-C$. The DM maximizes $V$. The optimal accuracy $A^\star(\mu)$ and optimal value $V^\star(\mu)$ are the accuracy and value at a maximizer. Two thresholds organize the solution:

$$\underline\mu=\frac{1}{e^{1/\lambda}+1},\qquad \bar\mu=\frac{e^{1/\lambda}}{e^{1/\lambda}+1}.$$

The machine. Information is aggregated into two binary variables: $X_1$, which the machine and the DM can both evaluate, and $X_2$, which only the DM can assess. Realizations are $x_1,x_2\in\{-,+\}$ and the state is good iff $x_1=x_2=+$. The DM's prior on $(X_1,X_2)$ is $\pi$, with $\pi(x_1,x_2)>0$ for all four realizations, so $\mu=\pi(+,+)$. The machine reveals $x_1$ at no cost; the DM updates by Bayes' rule to $\mu^x=P(\omega=g\mid X_1=x)$ and then solves her problem with prior $\mu^x$. The machine-assisted accuracy and value are the ex-ante expectations

$$A^\star_m=\sum_{x}P(X_1=x)\,A^\star(\mu^x),\qquad V^\star_m=\sum_{x}P(X_1=x)\,V^\star(\mu^x).$$

Formalization targets

Goal: Proposition 1

For every $\lambda\ge0$ and every prior $\pi$ with positive entries,

$$A^\star_m\ge A^\star(\mu)\qquad\text{and}\qquad V^\star_m\ge V^\star(\mu).$$

Milestones

1. Equation (3). $\mu^-=0$ and $\mu^+=\mu/(\mu+\pi(+,-))>\mu$.
2. Corollary 2, (13). For $\lambda>0$: $A^\star(\mu)=1-\mu$ on $[0,\underline\mu]$, $e^{1/\lambda}/(e^{1/\lambda}+1)$ on $(\underline\mu,\bar\mu)$, and $\mu$ on $[\bar\mu,1]$.
3. Corollary 2, (15). For $\lambda>0$: $V^\star(\mu)=1-\mu$ on $[0,\underline\mu]$, $\lambda[\log(e^{1/\lambda}+1)-H(\mu)]$ on $(\underline\mu,\bar\mu)$, and $\mu$ on $[\bar\mu,1]$.
4. Lemma 2 (accuracy and value). $A^\star_m=1-\mu/\mu^++(\mu/\mu^+)A^\star(\mu^+)$, and the same identity for $V^\star_m$.
5. Convexity of $A^\star$ on $[0,1]$ (proof of Proposition 1).
6. Slopes at the thresholds. The middle branch of (15) has derivative $-1$ at $\underline\mu$ and $1$ at $\bar\mu$.
7. Convexity of $V^\star$ on $[0,1]$.

Significance

The result. Proposition 1 is the baseline against which the paper's other findings are measured: although accuracy and value always improve, the machine can lower the probability of choosing the good state, raise false positives, and increase the DM's cognitive effort (Theorems 2–4 of the paper). Without Proposition 1 those effects would not be separable from a simple loss of decision quality. The closed forms (13) and (15) also show that, where the DM processes information, her accuracy depends on $\lambda$ alone and not on her prior.

Formalizing it. The proposition and its milestones are proved in the paper, in Appendix A, and the closed forms rely on the logit characterization of the optimum. None of this is machine-checked. A complete development produces a verified closed-form solution of the binary rational-inattention problem with entropy cost, with accuracy and value as explicit functions of the prior, and a verified value-of-information inequality for that problem. Both are reusable by the other four missions of this series and by any binary rational-inattention model.

Difficulty

The obvious argument — more information cannot hurt — is not available off the shelf: the DM is not a Bayesian with free information but optimizes an entropy-penalized program, and the comparison is between optimal values of two such programs at different priors. $A^\star$ and $V^\star$ are values at an optimum of a non-linear program over $[0,1]^2$. Their closed forms require identifying exactly when the corner solutions $p_g=p_b=0$ and $p_g=p_b=1$ are optimal and handling the degenerate priors $\mu=0,1$, where the maximizer is not unique. Both functions are piecewise in $\mu$, so their shape on $[0,1]$ does not follow from the shape of each piece: the behaviour at the kinks $\underline\mu$ and $\bar\mu$ decides it. Accuracy is a component of the objective, not the objective itself, so statements about $A^\star$ do not follow from optimality alone.

Formalization scope

• Decision problem. The paper's general information-processing problem (2) is not formalized. The DM chooses $(p_g,p_b)\in[0,1]^2$ directly — the paper's own §4 reduction (Matějka & McKay 2015), not a restriction. $H$ is Mathlib's Real.binEntropy (natural logarithm); $\lambda$ is lam.
• Starred metrics. $A^\star$ and $V^\star$ are accuracy and value at a chosen maximizer (Classical.epsilon); every maximizer yields the same values. They are defined for every real $\mu$ and used on $[0,1]$.
• Machine. $\{-,+\}$ is Bool with true $=+$; the prior is π : Bool → Bool → ℝ with positive entries summing to $1$. Posteriors are defined by Bayes' rule; $A^\star_m$, $V^\star_m$ are expectations over $x_1$.
• Parameters. The goal keeps the printed $\lambda\ge0$ (at $\lambda=0$ the cost vanishes); all milestones assume the model's standing $\lambda>0$, needed for $1/\lambda$. The paper's parameter set $\mathcal S=\{(\mu,\mu^+)\in[0,1]^2:\mu<\mu^+\}$ is replaced by priors with positive entries, which realize exactly $0<\mu<\mu^+<1$.
• Ruled out. Defining $A^\star$, $V^\star$ by the closed forms (13), (15); defining $A^\star_m$, $V^\star_m$ by the right-hand sides of Lemma 2; or assuming convexity as a hypothesis — each makes the corresponding statement true by definition, and none of them is used here.
• Infrastructure. Calculus of Real.binEntropy (derivative, concavity) is in Mathlib. Needed: existence of a maximizer on the square, the first-order characterization of the interior optimum, and convexity of piecewise functions glued with matching slopes. Contributions of general lemmas on these points are welcome.

Selected references

• T. Boyacı, Y. Canyakmaz, F. de Véricourt, Human and Machine: The Impact of Machine Input on Decision-Making Under Cognitive Limitations, ESMT Working Paper 20-02, 2020; Management Science 70(2), 2024. https://doi.org/10.1287/mnsc.2023.4744
• F. Matějka, A. McKay, Rational Inattention to Discrete Choices: A New Foundation for the Multinomial Logit Model, American Economic Review 105(1), 2015. https://doi.org/10.1257/aer.20130047
• C. A. Sims, Implications of Rational Inattention, Journal of Monetary Economics 50(3), 2003. https://doi.org/10.1016/S0304-3932(03)00029-1
• T. M. Cover, J. A. Thomas, Elements of Information Theory, 2nd ed., Wiley, 2006. https://doi.org/10.1002/047174882X

Motivation

When a supplier's production is subject to random yield, only part of a planned production run turns into usable output. A retailer sourcing from such a supplier bears the resulting shortage risk unless the contract or the selling strategy moves it elsewhere. Random yield is a classical topic in production planning (Yano and Lee, 1995), and postponing a decision until uncertainty resolves is a classical risk-mitigation tool (Van Mieghem and Dada, 1999).

Geng, Guo, Xiao and Yang study two postponements available to a retailer facing an unreliable supplier. Payment postponement replaces payment for the ordered quantity by payment for the delivered quantity, which shifts the yield risk to the supplier. Pricing postponement (responsive pricing) sets the retail price after the delivery is known, which shifts the risk to consumers. Their Proposition 2 answers which of the four combinations the retailer prefers, as a function of the production cost, when the yield loss is not too severe. This mission formalizes that proposition and the equilibrium results it rests on.

Setting

A supplier sells to a retailer, who sells to a market with linear demand $d(p)=a-bp$, $a,b>0$. The supplier's yield factor $Y$ takes the value $1$ with probability $\theta$ and $\alpha$ with probability $1-\theta$, with $\alpha,\theta\in(0,1)$, and has mean $\mu=\alpha(1-\theta)+\theta$. The supplier plans production $Q$, pays $c$ per planned unit, and delivers $\hat q=\min\{YQ,q\}$ against an order $q$. Throughout, $0<c<a\mu/b$.

There are four scenarios, written $k\in\{OA,OR,DA,DR\}$:

• O (pay-by-order): the retailer pays $wq$, and the supplier produces exactly $Q=q$;
• D (pay-by-delivery): the retailer pays $w\hat q$, and the supplier chooses $Q$ and may inflate production above $q$;
• A (ex ante pricing): the retailer commits to the retail price $p$ when it orders;
• R (responsive pricing): the retailer sets $p$ after seeing $\hat q$, maximizing $p\min\{d(p),\hat q\}$.

Each scenario is a Stackelberg game. The supplier sets the wholesale price $w$, the retailer orders (and, ex ante, prices), the supplier produces, the yield realizes, and under responsive pricing the retailer prices. Both firms are risk neutral. The solution concept is subgame-perfect equilibrium, and $\pi^k_R$ denotes the retailer's expected equilibrium profit in scenario $k$. Admissible prices are those of the paper's standing assumption (3): $0<p<a/b$, and $c<w<a/b$ under pay-by-order or $c/\mu<w<a/b$ under pay-by-delivery.

The cost thresholds of the comparison are

$$\tilde C=\frac{a\alpha\big(1-\sqrt{\alpha^2(1-\theta)+\theta}\big)}{b(1+\alpha)},\qquad c^{DR}_2=\frac{a\alpha\mu(1-\theta)}{b(\mu+\theta)},$$ $$c^{DR}_1=\frac{a\alpha(1-\theta)\big(\mu^2+\theta-2\theta\sqrt{\alpha\mu(1-\alpha)(1-\theta)}\big)}{b\big(\alpha^2(1-\theta)^3+4\alpha\theta(1-\theta)+\theta(1+\theta)^2\big)}.$$

Formalization targets

Goal: Proposition 2 (p. 16)

For $9/16\le\alpha<1$ and every $0<c<a\mu/b$, equilibria of OR, DA and DR exist, and every choice of equilibria satisfies

$$\begin{aligned} &\pi^{OR}_R<\pi^{DR}_R=\pi^{DA}_R && 0<c<\tilde C,\\ &\pi^{DA}_R=\pi^{DR}_R<\pi^{OR}_R && \tilde C<c<c^{DR}_1,\\ &\pi^{DA}_R<\pi^{OR}_R<\pi^{DR}_R && c^{DR}_1<c<c^{DR}_2,\\ &\pi^{DA}_R<\pi^{DR}_R=\pi^{OR}_R && c^{DR}_2<c<a\mu/b. \end{aligned}$$

Milestones

1. (4): the supplier's production under pay-by-delivery is $q$ below the wholesale price $c/(\alpha(1-\theta))$ and $q/\alpha$ above it.
2. (5): the responsive price is $(a-\hat q)/b$ for $\hat q<a/2$ and $a/(2b)$ otherwise.
3. Lemmas 2, 3, 4: existence of equilibria of OR, DA and DR, and their outcomes $(\pi_R,\pi_S,CS)$ in closed form on each open cost interval (Lemma 4 for $\alpha\ge 9/16$).
4. Threshold order (proof of Propositions 1–2): for $\alpha\ge 9/16$, $c^{OR}<0$ and $c^{DR}_1<c^{DR}_2<c^{DA}$.
5. Position of $\tilde C$ (proof of Proposition 4): for $\alpha\ge 9/16$, $0<\tilde C<c^{DR}_1$.

Significance

The proposition describes a preference cycle. Payment postponement (DA) is best when production is cheap, because the supplier then absorbs yield risk by inflating production. Pricing postponement (OR) is best at intermediate cost. Using both (DR) is strictly best on $(c^{DR}_1,c^{DR}_2)$, where the two postponements are worth more together than either alone. Above $c^{DR}_2$ the supplier stops inflating, DR and OR coincide, and pricing postponement suffices. These are the paper's managerial conclusions on contract and pricing choice under supply risk, and the other three missions of the series (strategic complementarity, and the effect of each postponement on the whole chain) rest on the same equilibria.

The paper derives the four equilibria in its Appendix B and proves the propositions in Appendix C as direct comparisons of closed forms. None of this has been machine-checked. The mission produces a formal model of the four games and a verified link from the game to the closed forms. Lemmas 2–4 are reusable by every statement about this model.

Difficulty

Once the closed forms are known, the comparison is polynomial algebra in $(\alpha,\theta,c)$ with square roots. The work lies upstream. Each equilibrium requires a backward induction over piecewise-linear objectives in $Q$ and $q$ and piecewise-quadratic objectives in $p$ and $w$. Optima occur at kinks such as the inflation threshold $w_0=c/(\alpha(1-\theta))$, and the supplier's value function is discontinuous there, so the maximum can sit at a boundary rather than at the center of a piece. In scenario DR the equilibrium wholesale price on $(c^{DR}_1,c^{DR}_2)$ sits exactly at $w_0$, where the supplier is indifferent among all productions in $[q,q/\alpha]$, so existence depends on how that tie is resolved. Uniqueness of outcomes, which the comparison needs, holds only on open cost intervals, because at each threshold two wholesale prices tie with different outcomes. The threshold inequalities for $\alpha\ge 9/16$ are not visible from the formulas and need careful estimates of the radicals.

Formalization scope

Parameters are a structure $(a,b,\alpha,\theta)$ with validity predicate $a,b>0$, $\alpha,\theta\in(0,1)$; the cost $c$ is a separate real argument. The expectation over $Y$ is the two-term sum $\theta f(1)+(1-\theta)f(\alpha)$, with no measure theory. A strategy profile consists of a wholesale price and rules for production $Q(w,q)$, the order $q(w)$, the ex ante price $p(w)$ and the ex post price $p^{\mathrm r}(w,q,\hat q)$. Equilibrium requires optimality at every admissible history over the admissible sets of (3). Consumer surplus is the integral $\int_0^{\min\{d(p),X\}}(p(t)-p)\,dt$, evaluated at the ex post price under responsive pricing and at the committed price under ex ante pricing.

Conventions and disclosed departures from the page:

• Tie rule. Under pay-by-delivery, when producing exactly $q$ is optimal, the supplier produces $q$. Display (4) assigns the tie at $w_0$ to inflation, under which DR has no equilibrium on $(c^{DR}_1,c^{DR}_2)$. Lemma 4's printed profits there are those of the convention.
• $CS^{DR}$ on the middle piece is stated with denominator $8b\alpha^2(1-\theta)^2(\alpha^2(1-\theta)+\theta)$; the page prints the last factor squared, which is the surplus of no single equilibrium. Proposition 2 does not involve $CS$.
• Open intervals. Lemmas are stated on open cost intervals; at the thresholds outcomes are not unique.
• $\tilde C$ is instantiated by (6), as Appendix C does; the page introduces it through Proposition 1's existential.
• Display (2) prints the scenario labels of $CS$ swapped; the Appendix B reading is used.

$\pi^k_R$ is the retailer's profit along an equilibrium of the game, never its closed form; a formalization that defines the profits by the Appendix B formulas, or an equilibrium predicate that no profile satisfies, would make the goal trivial. The goal therefore also asserts existence of equilibria of the three scenarios.

Contributions welcome: proofs of the milestones; general lemmas on maximizing piecewise-linear and piecewise-quadratic functions with kinks; the threshold inequalities. Proposition 1 (OA versus the others) is not part of this mission.

Selected references

• X. Geng, X. Guo, G. Xiao, N. Yang, Supply Risk Mitigation in a Decentralized Supply Chain: Pricing Postponement or Payment Postponement?, SSRN 3546872 (author version), 2022; published in Manufacturing & Service Operations Management 25(3), 2023. https://ssrn.com/abstract=3546872, https://doi.org/10.1287/msom.2022.0198
• C. A. Yano, H. L. Lee, Lot Sizing with Random Yields: A Review, Operations Research 43(2), 1995. https://doi.org/10.1287/opre.43.2.311
• J. A. Van Mieghem, M. Dada, Price Versus Production Postponement: Capacity and Competition, Management Science 45(12), 1999. https://doi.org/10.1287/mnsc.45.12.1631

Complete Single-Life Annuity Valuation, Payment Timing and Relationships

Motivation

A life annuity pays instalments conditional on an annuitant surviving to specified instants. As discussed in Dickson, Hardy and Waters (2020), actuarial value depends on the exact timing of the payments. For a pension payable in arrears, the payment event is at the end of the period. A contractual guarantee can preserve payments for the estate after death, but only once the entitlement has commenced. Those conditions must be explicitly modelled before calculating actuarial factors.

Setting

Take a finite distribution over last survived anniversaries $K=0,\ldots,h$ with nonnegative probabilities $p_k$ summing to one. The final state is right-censored: it does not assert death at the terminal age. Define $S(t)=\sum_{k=t}^{h}p_k$. A schedule has its first index $a$, up to $n$ instalments, an amount $b_j$ for each instalment, and an annual discount factor $v$ with $0<v\le1$. Advance instalments fall at $j$ and arrears instalments at $j+1$.

The first $g$ scheduled instalments are guaranteed only when survival to commencement $a$ activates the annuity. They continue to the estate after death during that period. Later instalments depend on survival at their actual payment instant. No spouse benefit is assumed.

Formalization targets

Payment events and survival

Define the realised random variable $Z(K)$ by summing actual payment indicators across the finite schedule. Derive its expectation independently from the lifetime-state mass function. Define a second valuation using survival to each payment instant, and prove the equivalence by interchanging finite sums.

$$\mathbb{E}[Z]=\sum_{k=0}^{h}p_kZ(k)= \sum_{j=a}^{a+n-1} b_j v^{j+\delta} \begin{cases} S(a),&j<a+g,\\ S(j+\delta),&j\ge a+g. \end{cases}$$

The instalment sum is truncated at the finite horizon. The timing offset $\delta$ equals zero for advance and one for arrears.

Duration, guarantee and varying benefits

Partition a non-guaranteed whole-horizon annuity into temporary and deferred periods. For a guaranteed annuity, split payments into the activated period-certain amount and the strictly later survival-contingent amount. If $g\ge n$, its entire value is survival to commencement multiplied by the corresponding annuity-certain present value. The benefit kernel supports level, arithmetic increasing or decreasing, geometric and piecewise step-up instalments.

Arrears, fractional survival and moments

The exact finite level-annuities relationship includes the terminal payment:

$$\ddot a_{\overline{h}|}-a_{\overline{h}|}=1-v^hS(h).$$

Expected squares of realised present values yield second moments and variance. The uniform distribution of deaths (UDD) provides a separate linear interpolation of observed annual survival probabilities at fractional instants.

Continuous survival laws and a controlled limit

At a fixed payment frequency, split each annual death-state mass equally across its subperiods under UDD. The same resulting micro-lifetime distribution can be used for fractional instalments and continuous benefit-rate integrals, so their actual cashflow representations share exact event boundaries. The construction agrees with annual survival at integer anniversaries. Placing the unsplit annual masses directly at integer death times would give a different, stepwise survival model within a year.

The zero-interest level annuity has an exact finite correction to the integral of linearly interpolated UDD survival. If $C$ is that integral, $S$ annual absolute survival and $m>0$, the due value equals $C+(S(0)-S(h))/(2m)$, and the arrears value equals $C-(S(0)-S(h))/(2m)$. Both have an explicit $O(1/m)$ error and converge to $C$. Under the fixed micro-atom lifetime law, continuously paid GBP 1 per year instead equals the same-frequency arrears value at zero interest, because the real-time survival indicator is constant between atom times. The limit of these finite-atom laws recovers the UDD linear-survival valuation.

A separate real-time lifetime-state model represents a continuous benefit rate in money per year rather than discrete money per instalment. Its actual realised annuity present value is integrated across the entitlement interval, with a guarantee activated by survival at commencement and payments then continuing to the estate before expiry. A finite probability expectation of the realised integral is reconciled with independently integrated survival weights. The continuous certain value is a comparison under the same deterministic discount force.

The discrete and real-time laws are connected at annual and fractional instalment boundaries through exact survivor-event identities. A bounded continuous payment-rate function admits an appropriate Riemann-sum limit under the specific regularity assumptions in the formal declaration. A twice differentiable integrand with uniformly bounded second derivative admits the two-term Woolhouse-type endpoint correction with a finite-horizon quadrature error bound. These limiting and approximation statements remain open formal theorem obligations, with no universal error claim for arbitrary discontinuous mortality laws.

Capstone

The unified capstone reconciles actual annual advance and arrears payments and UDD subperiod payments with independent survival-weighted sums. It also reconciles the same finite lifetime-state law with real-time survival at anniversaries and continuous integrated benefit valuations, including an activated guarantee. Separate milestones handle second moments, terminal-censored assurance-annuity identity, Riemann convergence and the explicit quadrature error bound. The earlier finite due-minus-arrears relationship remains a supporting target. These obligations follow from the separately defined probability masses and cashflow events, rather than assuming any valuation equality.

Significance

The classical distinction between annuity-certain and life-annuity present values is explained by Promislow (2015) through an explicit interest-and-survivorship discount mechanism. The present model makes this accounting precise at the level of individual payment events. It is consequently possible to compare a certain payment stream with a contingent one using exactly the same instalment schedule. It is also possible to alter the instalment amount without silently altering the survival law or guarantee entitlement.

The resulting mathematical foundation is suitable for retirement income and defined benefit pension cashflows where timing and benefit continuation clauses materially affect value. It separates annual unit amount from each instalment, and survival at commencement from survival at later payment events.

Difficulty

A death before commencement cannot activate a deferred guarantee. A death during the guarantee permits payments to the estate. An arrears instalment requires survival at the subsequent instant and the final one cannot silently disappear. Proving these relationships from true payment indicators is harder than defining annuity factors so the desired equations hold automatically. Finite lifetime censoring and the last surviving anniversary must remain visible in all derivations.

Formalization scope

The proposed Lean representation is an indexed real-valued finite probability mass function, a survival indicator and Finset-based cashflow sums. The canonical scope is a single namespace and targeted imports of Mathlib's real-number and finite-big-operator files. The environment revision is pinned in the manifest, but remains subject to live remote verification. Periods are integer anniversaries, amounts are per actual instalment, and the valuation origin is zero. Only finite sums are asserted without convergence hypotheses. The existing classical annuity formulae appear in the cited books. Their underlying mathematics is known, while the original finite cashflow encoding and its Lean theorem obligations are open and unproved.

These primitives are intended to supply later work on DB pension guarantee periods, future life-insurance premium annuities and pension escalation. A future separate mission could reuse the actual realised-cashflow event semantics to value survival-contingent spouse benefits with a two-life entitlement law, while keeping spouse entitlement fixed at the policyholder's death under the scheme rules. The current work limits itself to the single-life estate-continuation benefit and therefore does not risk silently importing joint-life assumptions.

The extended finite discrete formalisation constructs an actual UDD subperiod death-state law. Its fractional annuity valuations follow from realised subperiod payment events, with each instalment equal to the nominal annual pension divided by frequency. Separate theorems reconcile second moments with pairwise survival-event intersections, derive the incremental value of guarantees and reconcile finite annual assurance with the life-annuity due while retaining the terminal censored-state residual. The separate continuous law and a quantitative two-term Woolhouse-type error inequality are now included as remotely elaborated open theorem declarations, still requiring genuine proofs. General commutation-column identities, noninteger-year deferrals under arbitrary interpolation, unbounded whole-life convergence and classical higher-order Woolhouse estimates need further formal models. An unconfirmed Foundation A owner Draft is not an importable dependency. Every theorem declaration is an open proof obligation and no accepted proofs are asserted.

Selected references

• David C. M. Dickson, Mary R. Hardy and Howard R. Waters (2020), Actuarial Mathematics for Life Contingent Risks, third edition, Chapters 4–5, Cambridge University Press. https://doi.org/10.1017/9781108784184
• S. David Promislow (2015), Fundamentals of Actuarial Mathematics, third edition, Chapter 4, Wiley, https://www.wiley.com/en-us/Fundamentals+of+Actuarial+Mathematics%2C+3rd+Edition-p-9781118782521
• David C. M. Dickson, Mary R. Hardy and Howard R. Waters (2013), Actuarial Mathematics for Life Contingent Risks, second edition, Chapter 5, sections 5.3–5.13. https://assets.cambridge.org/97811070/44074/frontmatter/9781107044074_frontmatter.pdf

Motivation

Best subset selection fits a linear model using at most $k$ of $p$ available predictors, choosing the $k$ that minimize the residual sum of squares. Mixed-integer optimization made it computable at moderate scale (Bertsimas, King & Mazumder, 2016), which reopened the statistical question of when it should be used. Empirical comparisons (Hastie, Tibshirani & Tibshirani, 2020) found that best subsets predicts poorly when the signal-to-noise ratio (SNR) is low: by fitting the noise exactly within its chosen support it overfits, and shrinkage methods such as the Lasso do better there.

Mazumder, Radchenko & Dedieu propose to add a shrinkage penalty to the cardinality-constrained problem. Their Theorem 2 quantifies the effect of an $\ell_2$ (Euclidean-norm) penalty: it proves prediction-error bounds that are linear in the penalty level and therefore remain small in the low-SNR regime where best subsets fails. This mission formalizes that theorem.

Setting

The data follow the model

$$y=f^*+\epsilon,$$

where $y,f^*,\epsilon\in\mathbb R^n$, $f^*$ is an unknown deterministic mean and $\epsilon$ is a noise vector (in the paper, with independent $N(0,\sigma^2)$ entries, $\sigma>0$). The design $X\in\mathbb R^{n\times p}$ is deterministic and its columns have unit Euclidean norm. Write $\|\cdot\|$ for the Euclidean norm, $\|\beta\|_0$ for the number of nonzero coordinates of $\beta$, and $B_0(s)=\{u\in\mathbb R^p:\|u\|_0\le s\}$.

For a model size $k$ and a penalty level $\lambda\ge0$, the $\ell_2$-regularized best-subsets estimator is any solution

$$\hat\beta_2\in\arg\min_{\beta}\ \|y-X\beta\|^2+\lambda\|\beta\|\quad\text{s.t.}\quad\|\beta\|_0\le k.$$

The penalty is the norm $\|\beta\|$, not its square, and the loss carries no factor $1/2$. The quantity of interest is the prediction error $\|f^*-X\hat\beta_2\|^2$.

The minimal $s$-sparse eigenvalue of $X$ is $\gamma_s=\min_{u\neq0,\,u\in B_0(s)}\|Xu\|/\|u\|$. For $u\in\mathbb R^p$, $u^\sharp_1\ge\dots\ge u^\sharp_p$ is the non-increasing rearrangement of $|u_1|,\dots,|u_p|$. Given $\delta_0\in(0,1]$, three noise events are sets of noise vectors:

$$\mathcal E_s=\big\{\epsilon^\top Xu\le[4+\sqrt2]\sigma\sqrt{s\log(2ep/s)}\,\|u\|,\ \forall u\in B_0(s)\big\},$$ $$\mathcal F=\Big\{\epsilon^\top Xu\le[4+\sqrt2]\sigma\max\Big(\textstyle\sum_{j=1}^p u^\sharp_j\sqrt{\log(2p/j)},\ \sqrt{\log(1/\delta_0)}\,\|Xu\|\Big),\ \forall u\in\mathbb R^p\Big\},$$ $$\mathcal G_s=\big\{\epsilon^\top Xu\le\sigma\sqrt{5s\log(ep/s)+\log(1/\delta_0)}\,\|Xu\|,\ \forall u\in B_0(s)\big\}.$$

The paper's Theorem 1 shows these events have high probability; Theorem 2 is a deterministic statement on each of them. The symbol $\lesssim$ means "up to a positive universal multiplicative constant", one that does not depend on $n,p,k,X,f^*,\sigma,\lambda$ or $\delta_0$.

Formalization targets

Goal: Theorem 2 (p. 14)

Let $1\le k\le p$.

(A) Slow rate. If $\lambda\ge[8+2\sqrt2]\sigma\sqrt{2k\log(ep/k)}$, then on $\mathcal E_{2k}$

$$\|f^*-X\hat\beta_2\|^2\le\inf_{\beta\in B_0(k)}\big[\|f^*-X\beta\|^2+2\lambda\|\beta\|\big],$$

and on $\mathcal F$

$$\|f^*-X\hat\beta_2\|^2\lesssim\inf_{\beta\in B_0(k)}\big[\|f^*-X\beta\|^2+\lambda\|\beta\|\big]+\sigma^2\log(1/\delta_0).$$

(B) Fast rate. For every $\lambda\ge0$, on $\mathcal G_{2k}$

$$\|f^*-X\hat\beta_2\|^2\lesssim\inf_{\beta\in B_0(k)}\|f^*-X\beta\|^2+\sigma^2k\log(ep/k)+\gamma_{2k}^{-2}\lambda^2+\sigma^2\log(1/\delta_0).$$

The bounds hold for every minimizer $\hat\beta_2$ and for misspecified models: $f^*$ need not lie in the column span of $X$.

Milestones

The steps of the printed proof (Supplement B.2, pp. 39–40), in the order the proof uses them: the basic inequality (29); the bound (30) on $\mathcal E_{2k}$ and its consequence (31); the dichotomy on $\mathcal F$, where (30) implies (31) and (32) implies (33); the elementary inequality (34); the basic inequality on $\mathcal G_{2k}$ (p. 40); and the bound of $\lambda\|\beta-\hat\beta_2\|$ through $\gamma_{2k}$ (p. 40).

Significance

The result. The slow-rate bound of part (A) is linear in $\lambda$. When the signal $\|\beta^*\|$ is small compared with $\sigma$, the term $\lambda\|\beta^*\|$ is smaller than the rate $\sigma^2 k\log(ep/k)$ that best subsets attains, and the paper's Theorem 4 shows that in this regime the prediction error of best subsets is at least of order $\sigma^2\gamma_k^2k\log(ep/k)$. Together the two results explain the empirical finding that shrinkage helps best subsets at low SNR. Part (B) shows nothing is lost at high SNR: the fast rate is the minimax rate $\sigma^2k\log(ep/k)$ over $k$-sparse vectors plus the shrinkage term $\gamma_{2k}^{-2}\lambda^2$. Combined with Theorem 1, the bounds give the high-probability statements of the paper's Corollaries 1 and 3.

Formalizing it. The theorem is proved in the paper; no machine-checked version is known to exist. The mission produces a checked deterministic core: once the events are granted, every constant ($8+2\sqrt2$, the factor $2\lambda$, the threshold $2k\log(ep/k)$) is verified exactly. Together with the companion mission on Theorem 1 it would yield fully checked high-probability oracle inequalities for a cardinality-constrained estimator, which no current formal library contains.

Difficulty

Every step is elementary, but the bookkeeping is exact. The obvious reading "insert the event's inequality into (29)" does not by itself work on $\mathcal F$: the event's right-hand side is a maximum of a sorted weighted sum and a prediction-norm term, and the first branch has to be compared with $\sqrt{2k\log(ep/k)}\,\|u\|$ for the $2k$-sparse difference $u=\hat\beta_2-\beta$, including when $2k$ exceeds $p$. That comparison is a combinatorial estimate on sorted sums, not a substitution. On $\mathcal G_{2k}$, the penalty difference $\lambda(\|\beta\|-\|\hat\beta_2\|)$ is not controlled by the event at all and has to be converted into prediction errors through $\gamma_{2k}$. In both parts the final constant must not depend on $k$, $p$ or $\delta_0$.

Formalization scope

All objects are explicit Lean definitions in the namespace SubsetShrink.L2:

• vectors are functions on Fin n and Fin p with 0-based indices, and $X$ is a real Matrix (Fin n) (Fin p);
• the Euclidean norm, $\|\cdot\|_0$ and the inner product are explicit finite sums, since Mathlib's norm on Fin m → ℝ is the sup norm;
• $\sum_j u^\sharp_j\sqrt{\log(2p/j)}$ is encoded as a maximum over permutations, which equals the sorted sum by the rearrangement inequality;
• $\gamma_s$ is a real infimum over the nonzero vectors of $B_0(s)$, a nonempty set when $p,s\ge1$.

The model consists of $X$ with unit columns, $f^*$, $\epsilon$, $\sigma>0$ and $y=f^*+\epsilon$. The estimator is a predicate that every minimizer satisfies; no minimizer is chosen and existence is not assumed. "On the event" is a hypothesis that the noise vector satisfies the event's printed inequality, so no probability measure appears. $\mathcal G_{2k}$ is the event as printed on p. 13; the correction of its probability bound belongs to the mission on Theorem 1 and does not affect these deterministic statements.

Committed conventions:

• each $\lesssim$ is an existential constant $C>0$ quantified before all other data;
• an infimum over $B_0(k)$ is stated as a bound for every $\beta\in B_0(k)$;
• $\delta_0\in(0,1]$ is universally quantified;
• the model size satisfies $1\le k\le p$.

Part (B) assumes $\gamma_{2k}>0$ or $\lambda=0$. When $\gamma_{2k}=0<\lambda$ the paper's bound is vacuous ($\gamma_{2k}^{-2}\lambda^2=+\infty$), but Lean's $0^{-1}=0$ would turn it into a false claim.

A formalization that lets the constant depend on $k$, $p$ or $\delta_0$, fixes a particular minimizer, weakens an event (for example drops "for all $u\in B_0(s)$"), or computes the infimum as a real ⨅ over an unbounded set would trivialize the theorem and is ruled out.

Not formalized here: the probability bounds of Theorem 1, the $\ell_1$-penalized Theorem 3, the lower bound of Theorem 4, the data-driven choice of $k$ (Theorem 5), and the corollaries and numerical experiments. These are separate missions or follow-ups. Contributions of reusable lemmas (the rearrangement bound for the sorted sum, properties of $\gamma_s$, the elementary absorption inequality (34)) are welcome.

Selected references

• R. Mazumder, P. Radchenko, A. Dedieu, Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low, arXiv:1708.03288v4, 2022; Operations Research, 2023. https://arxiv.org/abs/1708.03288
• D. Bertsimas, A. King, R. Mazumder, Best subset selection via a modern optimization lens, Annals of Statistics 44(2), 2016. https://doi.org/10.1214/15-AOS1388
• T. Hastie, R. Tibshirani, R. Tibshirani, Best subset, forward stepwise or Lasso? Analysis and recommendations based on extensive comparisons, Statistical Science 35(4), 2020. https://doi.org/10.1214/19-STS733
• P. C. Bellec, G. Lecué, A. B. Tsybakov, Slope meets Lasso: improved oracle bounds and optimality, Annals of Statistics 46(6B), 2018. https://doi.org/10.1214/17-AOS1670

Motivation

Best subset selection fits a linear model $y\approx X\beta$ using at most $k$ of the $p$ available features: it minimizes the residual sum of squares subject to the sparsity constraint $\|\beta\|_0\le k$, where $\|\beta\|_0$ counts the nonzero coordinates of $\beta$. Mazumder, Radchenko and Dedieu (arXiv:1708.03288v4; Operations Research, 2023) show that best subsets overfits when the signal-to-noise ratio is low, and propose adding a shrinkage penalty $\lambda\|\beta\|_q$ with $q\in\{1,2\}$ to the same constrained problem. Their statistical results (oracle inequalities, a lower bound for best subsets, a BIC-type choice of $k$) are the subject of the companion missions II–VI of this series.

The estimator is a mixed-integer program. To compute it in practice, and to warm-start the mixed-integer solver that certifies optimality, the paper uses a discrete first-order (DFO) method: a proximal-gradient iteration in which the proximal step is a projection-like operation onto the set of $k$-sparse vectors with a norm penalty. The method descends from iterative hard thresholding (Blumensath & Davies, 2009), from proximal gradient methods for composite problems (Nesterov, 2013), and from the discrete first-order algorithms of Bertsimas, King and Mazumder (Annals of Statistics, 2016). This mission formalizes the paper's convergence guarantee for it, Proposition 2.

Setting

Vectors live in $\mathbb R^p$ with the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|_2$. Write $\|\beta\|_0$ for the number of nonzero coordinates and $\|\beta\|_1=\sum_i|\beta_i|$. For $q\in\{1,2\}$ the penalty is the norm $\|\beta\|_q$ itself, not its $q$-th power.

Let $f:\mathbb R^p\to\mathbb R$ be a differentiable convex function whose gradient is $L_0$-Lipschitz:

$$\|\nabla f(\beta)-\nabla f(\alpha)\|_2\le L_0\|\beta-\alpha\|_2\qquad\forall\,\beta,\alpha .$$

The motivating case is $f(\beta)=\tfrac12\|y-X\beta\|_2^2$ with $L_0=\sigma_{\max}(X)^2$. The composite problem (7) is

$$\text{minimize}\quad F(\beta):=f(\beta)+\lambda\|\beta\|_q\quad\text{s.t.}\quad\|\beta\|_0\le k .$$

For $L\in\mathbb R$ the quadratic model of $f$ around $\alpha$ is

$$Q_L(\beta;\alpha)=f(\alpha)+\langle\nabla f(\alpha),\beta-\alpha\rangle+\tfrac L2\|\beta-\alpha\|_2^2 ,$$

and the thresholding operator is the set of minimizers

$$\mathrm S(u;k;\mu\ell_q)=\operatorname*{arg\,min}_{\|b\|_0\le k}\ \tfrac12\|b-u\|_2^2+\mu\|b\|_q ,$$

which can contain several points when the $|u_j|$ have ties. A DFO sequence with constant $L>0$ starts at a $k$-sparse $\beta^{(1)}$ and, for $m\ge1$, picks any

$$\beta^{(m+1)}\in\mathrm S\Big(\beta^{(m)}-\tfrac1L\nabla f(\beta^{(m)});\,k;\,\tfrac\lambda L\ell_q\Big).$$

Formalization targets

Goal: Proposition 2 (p. 10)

Assume in addition $f\ge0$ and $\lambda\ge0$. For every DFO sequence:

(a) if $L\ge L_0$, then $F(\beta^{(m)})$ is non-increasing in $m\ge1$ and converges to some $F^*\ge0$;

(b) if $L>L_0$, then for every $M\ge1$

$$\min_{1\le m\le M}\|\beta^{(m+1)}-\beta^{(m)}\|_2^2\le\frac{2\big(F(\beta^{(1)})-F^*\big)}{M(L-L_0)} .$$

The statement holds for any $f$ of the stated class and any choice in the set-valued operator; nothing about least squares is assumed.

Milestones (proof in Supplement A.1, p. 35)

1. (9), p. 8: $f(\beta)\le Q_L(\beta;\alpha)$ for all $\alpha,\beta$ and every $L\ge L_0$, the bound the paper takes from Nesterov (2004).
2. (20)–(21), p. 35: completing the square, $Q_L(\eta,\beta)+\lambda\|\eta\|_q=\tfrac L2\|\eta-(\beta-\tfrac1L\nabla f(\beta))\|_2^2-\tfrac1{2L}\|\nabla f(\beta)\|_2^2+f(\beta)+\lambda\|\eta\|_q$. Hence the minimizers of $Q_L(\cdot,\beta)+\lambda\|\cdot\|_q$ over $\|\eta\|_0\le k$ are exactly $\mathrm S(\beta-\tfrac1L\nabla f(\beta);k;\tfrac\lambda L\ell_q)$.
3. (22), p. 35: for $\|\beta\|_0\le k$ and $\hat\eta$ in that set, $F(\beta)\ge\tfrac{L-L_0}2\|\hat\eta-\beta\|_2^2+F(\hat\eta)$.
4. (23) and the next display, p. 35: summed over $m=1,\dots,M$,

$$F(\beta^{(1)})-F(\beta^{(M+1)})\ge\tfrac{M(L-L_0)}2\min_{m\le M}\|\beta^{(m+1)}-\beta^{(m)}\|_2^2 .$$

5. Proposition 1, p. 9 (companion, not used by the goal): every $\hat\beta\in\mathrm S(u;k;\lambda\ell_q)$ keeps the $k$ largest entries of $u$ in magnitude, for some ordering of ties. For $q=1$ it soft-thresholds them coordinatewise, and for $q=2$ it shrinks them as a group by $\max\{\tau_u-\lambda,0\}/\tau_u$, with $\tau_u$ the norm of those $k$ entries.

Significance

Proposition 2 is what makes the DFO method a sound component of the paper's computational pipeline. The objective values never increase, so every iterate is a feasible point at least as good as the warm start. Part (b) says that the step length $\|\beta^{(m+1)}-\beta^{(m)}\|_2^2$ is small after $O(1/\epsilon)$ iterations. A point whose step vanishes is a fixed point of the update, which the paper calls a first-order stationary point (Definition 1). The stopping rule of the algorithm ($\|\beta^{(m+1)}-\beta^{(m)}\|_2^2\le\tau$) is therefore reached in at most $\lceil 2(F(\beta^{(1)})-F^*)/(\tau(L-L_0))\rceil$ steps.

The result is proved in the paper, in half a page that defers its central inequality (22) to Proposition 6 of Bertsimas, King & Mazumder (2016). It has not been formalized. A machine-checked version produces three reusable pieces: a descent lemma for functions with Lipschitz gradient on $\mathbb R^p$, the variational characterization of the sparse proximal step, and a sufficient-decrease-to-rate argument for any descent method. These are the same pieces that iterative hard thresholding, proximal gradient, and block-coordinate methods for $\ell_0$ problems need.

Difficulty

The difficulty is moderate, and it lies in the infrastructure rather than in any single step. The descent lemma (9) needs the fundamental theorem of calculus along a segment for a function on a Euclidean space, combined with the Lipschitz bound on the gradient. The feasible set $\{\|\beta\|_0\le k\}$ is not convex, so no convex-analysis argument (subgradient optimality, firm nonexpansiveness of a proximal map) applies to the thresholding step. Inequality (22) must instead be obtained by comparing the minimizer $\hat\eta$ with the feasible competitor $\beta$ itself, which is why the hypothesis $\|\beta\|_0\le k$ appears. Part (a) also needs a lower bound on $F$ for its limit to exist and be nonnegative, which the general class of $f$ does not provide on its own.

Formalization scope

$\mathbb R^p$ is EuclideanSpace ℝ (Fin p), the gradient is Mathlib's gradient f, and coordinates are $0$-based. Membership in $\mathrm S(u;k;\mu\ell_q)$ is a predicate: feasibility plus minimality against every $k$-sparse competitor. No selection from the set is fixed, and existence of minimizers is not assumed. A DFO sequence is any β : ℕ → ℝᵖ satisfying the update for every $m\ge1$, indexed from $1$ as printed. The stopping rule and the support-restricted polishing Step 2 are not part of it. The penalty is $\|\cdot\|_1$ for $q=1$ and the Euclidean norm for $q=2$, and every theorem assumes $q\in\{1,2\}$ and $k\ge1$. The minimum over $1\le m\le M$ is a finite infimum over a nonempty index set.

Three hypotheses are added to Proposition 2 as printed, each disclosed in the item. The proof's claim "$F(\beta)\ge0$" is false for a general convex $f$ with Lipschitz gradient ($f(\beta)=-\beta_1$ sends $F$ to $-\infty$), so $f\ge0$ and $\lambda\ge0$ are assumed. The update divides by $L$, and $L\ge L_0$ allows $L=0$, so $L>0$ is assumed. "Decreasing" is read as non-increasing. Convexity of $f$ is kept as in the paper's setting (7)–(8), though only the gradient bound is used. Proposition 1 is stated with an existential ordering: for a fixed sorting permutation the printed claim fails under ties.

The statement cannot be trivialized by restricting $f$ or the run. The goal quantifies over every $f$ of the class and every sequence obeying the update, the limit $F^*$ in (b) is the actual limit of the objective values, and the rate holds for every $M\ge1$. Not formalized here: the mixed-integer formulations, the continuation and local-search heuristics of §2.4, Definition 1, and the paper's statistical results (missions II–VI). Contributions of reusable infrastructure, such as a general descent lemma or a lemma turning summed decrease into a $1/M$ rate, are welcome as separate theorems.

Selected references

• R. Mazumder, P. Radchenko, A. Dedieu, Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low, arXiv:1708.03288v4, 2022; Operations Research 71(1), 2023. https://arxiv.org/abs/1708.03288v4
• D. Bertsimas, A. King, R. Mazumder, Best Subset Selection via a Modern Optimization Lens, Annals of Statistics 44(2), 2016. https://doi.org/10.1214/15-AOS1388
• Y. Nesterov, Gradient Methods for Minimizing Composite Functions, Mathematical Programming 140, 2013. https://doi.org/10.1007/s10107-012-0629-5
• Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
• T. Blumensath, M. E. Davies, Iterative Hard Thresholding for Compressed Sensing, Applied and Computational Harmonic Analysis 27(3), 2009. https://doi.org/10.1016/j.acha.2009.04.002