Operations Research

Interior point methods solve linear programs by moving through the interior of the feasible set instead of along its edges — the approach that turned Karmarkar's 1984 breakthrough into today's practical large-scale solvers. This mission formalizes the primal path following algorithm of Chapter 9 of Bertsimas–Tsitsiklis. For $\mu > 0$ the logarithmic barrier

replaces the constraint $\mathbf{x} \ge \mathbf{0}$; the minimizers $\mathbf{x}(\mu)$ of $B_\mu$ over $\{A\mathbf{x} = \mathbf{b}\}$ trace the central path, characterized by the KKT conditions (9.17): $A\mathbf{x} = \mathbf{b}$, $\mathbf{x} \ge \mathbf{0}$, $A'\mathbf{p} + \mathbf{s} = \mathbf{c}$, $\mathbf{s} \ge \mathbf{0}$, $XS\mathbf{e} = \mu\mathbf{e}$ (Lemma 9.5). The algorithm follows the path with one Newton step of the barrier problem per shrink $\mu^{k+1} = \alpha\mu^k$, maintaining the proximity invariant

. The goal theorem is Theorem 9.7: with $\alpha = 1 - \frac{\sqrt{\beta}-\beta}{\sqrt{\beta}+\sqrt{n}}$ and a $\beta$-close start, after $K = \Big\lceil \frac{\sqrt{\beta}+\sqrt{n}}{\sqrt{\beta}-\beta}\,\log\frac{(\mathbf{s}^0)'\mathbf{x}^0(1+\beta)}{\varepsilon(1-\beta)} \Big\rceil$ iterations the algorithm reaches primal and dual feasible solutions with duality gap $(\mathbf{s}^K)'\mathbf{x}^K \le \varepsilon$ — the explicit form of the celebrated $O(\sqrt{n}\log(1/\varepsilon))$ iteration bound. Alongside it we formalize the generic potential-reduction scheme (Theorem 9.4): any algorithm cutting $G(\mathbf{x},\mathbf{s}) = q\log\mathbf{s}'\mathbf{x} - \sum_j \log x_j - \sum_j \log s_j$ by $\delta$ per step reaches gap $\varepsilon$ within an explicit $K$.

Can the feasibility of a system of linear inequalities be decided in a provably small number of iterations? The ellipsoid method — the algorithm with which Khachiyan showed in 1979 that linear programming is polynomially solvable — answers this with pure convex geometry. This mission formalizes Chapter 8 of Bertsimas–Tsitsiklis. An ellipsoid is

with $D$ symmetric positive definite. The geometric engine is Theorem 8.1: the half-ellipsoid $E \cap \{\mathbf{x} \mid \mathbf{a}'\mathbf{x} \ge \mathbf{a}'\mathbf{z}\}$ is contained in the explicitly constructed ellipsoid $E' = E(\bar{\mathbf{z}}, \bar{D})$,

and the volume contracts:

. Two integer-data estimates make the contraction decisive: every extreme point of $P = \{\mathbf{x} \mid A\mathbf{x} \ge \mathbf{b}\}$ with entries bounded by $U$ has coordinates in $[-(nU)^n, (nU)^n]$ (Lemma 8.2), and a full-dimensional bounded such polyhedron has $\mathrm{Vol}(P) > n^{-n}(nU)^{-n^2(n+1)}$ (Lemma 8.4). The goal theorem is Theorem 8.2: started on a ball $E(\mathbf{x}_0, r^2 I)$ of volume at most $V$ containing $P$, with $v$ a lower bound on $\mathrm{Vol}(P)$ when $P$ is nonempty, the ellipsoid method correctly decides whether $P$ is empty within $t^* = \lceil 2(n+1)\log(V/v) \rceil$ iterations — the explicit iteration count behind the polynomial-time headline.

How does the optimal cost of a linear program respond when the problem data change? Chapter 5 of Bertsimas-Tsitsiklis studies the standard form problem $\min\{c'x \mid Ax = b,\ x \ge 0\}$ (rows of $A$ linearly independent) as the requirement vector $b$ and the cost vector $c$ vary. On the convex set $S = \{b \mid P(b) \neq \emptyset\}$ of feasible right-hand sides, and under the standing assumption that the dual feasible set is nonempty, the optimal cost $F(b)$ is finite and convex (Theorem 5.1) — indeed $F(b) = \max_{i} (p^i)'b$ over the extreme points $p^1, \dots, p^N$ of the dual feasible set, a piecewise linear convex function whose breakpoints are exactly where the dual optimum is non-unique. The capstone (Theorem 5.2) identifies the generalized gradients of $F$: if the primal at $b^*$ is feasible with finite optimal cost, then $p$ is an optimal solution of the dual if and only if $p$ is a subgradient of $F$ at $b^*$ (Definition 5.1: $F(b^*) + p'(b - b^*) \le F(b)$ for all $b \in S$) — the precise sense in which dual variables are marginal costs. Dually (Theorem 5.3), the set $T$ of cost vectors with finite optimal cost is convex, the optimal cost $G(c)$ is concave on $T$, and near any $c$ with a unique primal optimum $x^*$, $G$ is linear with gradient $x^*$. Local ranging (Section 5.1) and parametric programming (Section 5.5) are the procedural companions, folded into the design notes.

Every linear programming problem has a shadow. To the primal $\min c'x$ we associate the dual $\max p'b$, whose variables price the primal constraints: one dual variable per primal constraint and one dual constraint per primal variable, with signs governed by the correspondence of Table 4.1. This mission formalizes §4.1–4.5 of Bertsimas–Tsitsiklis: the dual of a general-form linear program, the involution "the dual of the dual is the primal" (Theorem 4.1), and weak duality $p'b \le c'x$ for any primal-feasible $x$ and dual-feasible $p$ (Theorem 4.3) with its two corollaries — an unbounded primal forces an infeasible dual (Corollary 4.1), and feasible $x, p$ with $p'b = c'x$ are automatically both optimal (Corollary 4.2). The goal theorem is strong duality (Theorem 4.4): if a linear programming problem has an optimal solution, so does its dual, and the respective optimal costs are equal — proved in the book by running the simplex method with the lexicographic pivoting rule of Mission IV on a standard-form transform. The statement is deliberately the book's attainment form: by Table 4.2 the primal and the dual can be simultaneously infeasible (Example 4.5), so an unguarded equality of optimal values is false. The mission closes with complementary slackness (Theorem 4.5): feasible $x$ and $p$ are simultaneously optimal if and only if $p_i(a_i'x - b_i) = 0$ for all $i$ and $(c_j - p'A_j)x_j = 0$ for all $j$ — the certificate structure behind the dual simplex method and every LP optimality check.

How does one actually solve a linear program? Chapter 2 showed that if a standard-form problem $\min c'x$ subject to $Ax = b$, $x \ge 0$ has an optimal solution, it has an optimal basic feasible solution; the simplex method searches among basic feasible solutions, moving along edges of the feasible set in cost-reducing directions. This mission formalizes the mathematics of Chapter 3 of Bertsimas–Tsitsiklis: feasible directions, the reduced costs

measuring the cost rate along the basic directions, the optimality conditions of Theorem 3.1 ($\bar{c} \ge 0$ implies optimality, and conversely at nondegenerate optima), the basis change of Theorem 3.2, and the pivot iteration itself — encoded as a predicate relating a basis/BFS pair to its successor, so that every theorem covers every pivoting rule. The goal theorem is Theorem 3.3: if the feasible set is nonempty and every basic feasible solution is nondegenerate, the simplex method terminates after a finite number of iterations, ending either with an optimal basis and an associated optimal basic feasible solution, or with a direction $d$ satisfying $Ad = 0$, $d \ge 0$, $c'd < 0$ certifying optimal cost $-\infty$. The secondary capstone, Theorem 3.4, removes the nondegeneracy assumption: under the lexicographic pivoting rule every tableau row other than the zeroth stays lexicographically positive, the zeroth row strictly increases lexicographically, and the simplex method terminates on every problem — the anticycling guarantee that also supplies the optimal-basis existence used by the strong duality theorem of Mission V.

Every linear programming problem asks to minimize a linear cost $c'x$ over a polyhedron — a set of the form $P = \{x \in \mathbb{R}^n \mid Ax \ge b\}$, or in standard form $\{x \mid Ax = b,\ x \ge 0\}$. Chapter 2 of Bertsimas–Tsitsiklis develops the geometry of these feasible sets, and its central achievement is making the intuitive notion of a "corner point" rigorous. There are three natural candidates: the extreme point — a point of $P$ that cannot be written as a convex combination of two other points of $P$ (purely geometric, representation-independent); the vertex — the unique minimizer of some linear cost $c'y$ over $P$ (geometric, via supporting hyperplanes); and the basic feasible solution — a feasible point at which $n$ linearly independent constraints are active (algebraic, the object the simplex method actually computes with). This mission formalizes polyhedra, active constraints, vertices and basic (feasible) solutions, and proves the fundamental Theorem 2.3: for a nonempty polyhedron all three notions coincide. Around the capstone sit the supporting pillars: polyhedra are convex (Theorem 2.1), the characterization of points pinned down by $n$ linearly independent active constraints (Theorem 2.2), finiteness of the set of basic solutions (Corollary 2.1), and the basis-column characterization of basic solutions in standard form (Theorem 2.4) — the combinatorial engine behind the simplex method of Chapter 3 and the root of the entire series.

How quickly does the empirical mean of independent random variables concentrate around the true mean? This question is the analytic engine of the entire theory of stochastic bandits: every optimistic algorithm (Explore-Then-Commit, UCB and its relatives) is calibrated by a tail bound on the sample mean. This mission formalizes the subgaussian framework of Chapter 5 of Lattimore–Szepesvári's Bandit Algorithms: a random variable $X$ is $\sigma$-subgaussian when $\mathbb{E}[e^{\lambda X}] \le e^{\lambda^2\sigma^2/2}$ for all $\lambda$, and the Cramér–Chernoff method converts this moment-generating-function control into the exponential tail $\mathbb{P}(X \ge \varepsilon) \le e^{-\varepsilon^2/(2\sigma^2)}$. The goal theorem is the Hoeffding-type bound: the sample mean of $n$ independent $\sigma$-subgaussian deviations exceeds the true mean by $\varepsilon$ with probability at most $\exp(-n\varepsilon^2/(2\sigma^2))$, together with its confidence form $\mathbb{P}\big(\hat\mu + \sqrt{2\sigma^2\log(1/\delta)/n} \le \mu\big) \le \delta$ — the exact bound every UCB index is built from. These few lines of analysis are cited by every regret bound in the series.

Multi-agent reinforcement learning approximates a global value function by summing per-agent local value functions learned independently — a trick that works surprisingly well in practice (ride-hailing dispatch, restless bandits) but had no general theoretical justification. Chen and Peng (arXiv:2506.02385) explain why: they define a Markov entanglement measure for the joint transition dynamics of a multi-agent MDP, directly analogous to quantum entanglement of a two-party state, and show it controls exactly how much error this value-decomposition trick incurs. This mission formalizes their sharpest quantitative bound (Theorem 4): the error of decomposing the global Q-function into per-agent local Q-functions is controlled, entrywise, by the agent-wise total-variation measure of Markov entanglement.

A platform sourcing items from monopolistic sellers with private quality cannot tractably maximize its true profit: the bundle revenue $Rev(v_S)$ is neither monotone, submodular, supermodular, subadditive, nor superadditive. Theorem 4.6 of Buying to Bundle: Optimal Sourcing from Monopolistic Sellers shows that the simple surrogate threshold mechanism — maximize the linearized objective $\varpi(x)=N\,E[x(\mu)(\mu-\varphi(\mu))]$ — is profit-optimal up to a $1+O(N^{-1/3})$ factor in large markets. Prove it: Bernoulli concentration for the bundle quality plus sub-exponential control of the dispersion gap $|Rev(v)-E[v]|$ (Lemma 4.5).

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:

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:

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$:

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:

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

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

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

• The strategic utility is

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

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

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

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

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

Why the timing of personalized pricing matters

Firms can use information about individual customers to quote different prices. That ability changes their price competition, but it can also change where they locate their products or services in a market. For a firm deciding whether to invest in personalized pricing (PP), the order of those decisions matters: a positioning choice made after the investment can respond to a rival's new pricing capability. Li, Wang and Nault study this issue in a two-firm location game. In their August 3, 2021 manuscript, Section 6 reverses the timing of their basic model: firms decide whether to acquire PP before choosing positions. This mission concerns that Section 6 result, Proposition 5, rather than the similarly titled result as it may appear in the later Management Science article.

The question has a direct strategic interpretation. A technology can be useful in a pricing contest at fixed locations yet be unattractive when both firms can subsequently reposition. The mission asks for a precise equilibrium statement covering every nonnegative implementation cost, including the costless case. The three positioning subgames and the implementation payoff table are part of the target because they determine what an initial PP choice earns. The paper states these outcomes on pages 23–25 of the manuscript.

Market and game

Consumers form a unit mass uniformly distributed on the interval $[0,1]$. Each consumer buys one unit from one of two firms, A and B. Firm $i$ chooses a real position $x_i$; locations outside the consumer interval are allowed. A consumer at $x$ faces a quadratic misfit cost $t(x-x_i)^2$, where $t>0$, in addition to the firm's price. The reservation value is assumed large enough for the whole market to buy. It therefore cancels from the gross profit expressions used here. These conventions come from Section 3.

A firm choosing PP can quote a price to each consumer according to that consumer's location. A firm choosing U quotes one uniform price. PP incurs a fixed cost $F\ge0$. In the game studied here, the firms simultaneously decide between PP and U first, simultaneously choose real positions second, and compete in prices third. If exactly one firm has PP, the uniform-price firm posts its price before the PP firm sets its targeted prices. If both firms make the same PP choice, prices are set simultaneously. The cost $F$ is sunk by the positioning stage and is deducted only when stage-1 net payoffs are computed.

Write $a_i(x)=t(x-x_j)^2-t(x-x_i)^2$ for the misfit advantage of firm $i$ over firm $j$ at equal prices. With PP at both firms, firm $i$'s gross profit is the integral of $\max\{0,a_i(x)\}$ over consumers. With one PP firm, the uniform-price leader chooses a price maximizing its price times the measure of consumers it serves; the targeted follower obtains the remaining gross profit. With two uniform prices, demand comes from consumers who prefer each firm's full price, with equal division at a tie. Positioning equilibria compare each firm's profit with moves to every real location, with the appropriate pricing continuation. The construction matches the pricing cases in Section 4 and Appendix A.

Formalization targets

The benchmark with two uniform-price firms places A at $-1/4$ and B at $5/4$, with both prices equal to $3t/2$ and gross profit $3t/4$ for each. With PP at both firms, the positioning subgame places them at $1/4$ and $3/4$, with gross profit $t/8$ each. When A alone has PP, it follows in the pricing stage and locates at $-1/2$, while B leads and locates at $1/2$; their respective gross profits are $t/4$ and $t/2$. The reflected outcome applies when B alone has PP. These are the milestones from Sections 4 and 6.

Those outcomes give the stage-1 net payoff matrix, ordered as (A, B):

The main target is Proposition 5: for every $t>0$ and $F\ge0$, both firms choose U in the equilibrium implementation game. The formal goal also states the pricing and positioning outcomes that generate this matrix, the existence of optimal uniform-leader prices in both asymmetric subgames, strict dominance of U, and uniqueness of the pure implementation equilibrium. The numerical constants belong to the source's specific quadratic-misfit model.

What the result establishes

The theorem separates the value of a pricing capability at fixed positions from its value in a game where competitors can reposition. In the paper's short-run positioning game, adopting PP cannot improve either firm's equilibrium implementation payoff: U is strictly preferred against either choice of the rival. The conclusion holds even when acquiring PP costs nothing. It also explains why the observed no-PP outcome has the same positions, prices and profits as the uniform-pricing benchmark. The manuscript discusses this contrast immediately after Proposition 5.

The result is proved in the source, while the Lean statements in this proposal remain open proof obligations. A complete formalization would connect consumer-level demand, pricing optimality, positioning equilibria, the payoff matrix and the final Nash equilibrium within one model. The price and position predicates can be reused for other timing rules or cost assumptions built on the same Hotelling market. This mission does not claim to formalize the paper's later welfare comparisons or the costly-PP regimes under the original positioning-first timing.

Where the difficulty lies

The payoff matrix makes the final comparison short, but treating the matrix as a definition would hide the economic claim. Each cell must instead come from an equilibrium of the appropriate pricing and positioning subgame. Uniform-pricing demand changes when the indifferent consumer reaches an endpoint, and a firm can move across its rival; an argument using only interior demand formulas or ordered positions cannot establish the full position equilibrium. In the one-PP subgame, the targeting firm can make a reflected location move that ties its equilibrium payoff, so the position comparison must allow equality. A leader may also have several optimal prices at coincident locations, which makes the choice of an off-path pricing continuation material.

Formalization scope

Lean uses real positions and prices, a two-element PP-choice type, Lebesgue measure for uniform consumer shares, and interval integrals for targeted gross profits. It assumes $t>0$, $F\ge0$, unit demand and full market coverage. PP cost appears only in net stage-1 payoffs. The reservation value is omitted because it cancels under full coverage. At a uniform-price tie, consumers are split equally; at a tie with a targeted follower, the follower serves the consumer. These rules make the demand functions defined even at coincident firm positions, although individual tie points have zero measure when positions differ.

The displayed closed-form prices require interior-demand conditions, stated explicitly on their milestone. Position deviations range over all of $\mathbb R$. The asymmetric positioning predicate requires an optimal pricing continuation after each deviation; this is a choice of continuation when the leader has multiple optima. It is recorded explicitly because the paper does not specify off-path tie selection. The goal's two asymmetric outcomes are mirror images under $x\mapsto1-x$, as the source's “without loss of generality” convention requires.

Gross profits are defined from consumer shares and integrals; stage-1 payoffs evaluate those primitives at the source's subgame positions. The target cannot be satisfied by inserting Table 1's numbers as payoff definitions, by restricting position deviations to ordered pairs, or by assuming the desired equilibrium as a hypothesis. Contributions to measurable demand, interval integration, leader optimality, the uniform and PP position games, and the reflected asymmetric game are all within scope.

Selected references

• X. Li, X. (Shane) Wang and B. R. Nault, Is Personalized Pricing Profitable When Firms Can Differentiate?, manuscript submitted to Information Systems Research, August 3, 2021, SSRN abstract 3881900. Source for Sections 3–4, Section 6, Proposition 5, Table 1 and Appendix A.

Why the final licensing choice matters

A component supplier can influence a product market through both the wholesale price it charges and the technology its customers may share. Wang, Huang and Lee study a supply chain with one upstream supplier and two downstream manufacturers that invest in product quality and then compete in quantities. A cross-licensing policy lets each manufacturer use some of the other's innovation. The supplier may promise a policy before the investments, or leave the decision until after the investments and wholesale price are fixed. The latter choice creates a precise comparison: at that final stage, does permitting cross-licensing reduce the supplier's revenue? The authors answer it in Proposition 1 of their SSRN manuscript, version of 2023-04-27. Its proof is in the attached appendix, p. A.1.

This mission concerns that final-stage comparison. It is one part of the paper's broader study of how a supplier's licensing commitment affects manufacturers' innovation incentives and downstream market structure. The later innovation and initial-contract comparisons are separate questions. Here, investments and wholesale price are fixed, so the result isolates the direct quantity-market effect of licensing at the moment the supplier chooses its policy.

The downstream quantity game

Manufacturers $M_1$ and $M_2$ have already selected nonnegative innovation levels $T_1$ and $T_2$, with $T_1\le T_2$ in the presentation of equations (2) and (3). Each chooses a nonnegative production quantity $q_i$. The wholesale price $r$ is the amount each manufacturer pays the common supplier for one unit. The market-size intercept is normalized to one and per-unit manufacturing cost to zero. If licensing effectiveness is $\beta\in[0,1]$, manufacturer $i$ receives a quality improvement $T_i+\beta T_j$; $\beta=0$ represents no cross-licensing. Its inverse demand is $1+T_i+\beta T_j-q_1-q_2$. These are the model's conventions on pp. 9–10.

At fixed $T_1,T_2,\beta,r$, the manufacturers play a simultaneous quantity game. Their respective profits are

A Nash equilibrium is a pair $(q_1,q_2)\in[0,\infty)^2$ for which neither manufacturer increases its profit by changing its own nonnegative quantity while the other's quantity stays fixed. The supplier's profit at a quantity profile is $r(q_1+q_2)$. The supplier's comparison must therefore account for the manufacturers' responses under each licensing policy; it cannot compare profit at an arbitrary fixed quantity pair.

Formalization targets

The first milestone gives the exact equilibrium quantities of equation (2). Write $r_1=1+T_1(2-\beta)-T_2(1-2\beta)$ and $r_2=1+\beta T_1+T_2$. For $r\le r_1$ both manufacturers can sell; for $r_1<r\le r_2$ only $M_2$ sells; above $r_2$ neither sells. The statement characterizes every equilibrium and thereby gives existence and uniqueness across the two threshold boundaries, including the cases where a manufacturer's equilibrium quantity is zero.

The second milestone identifies the supplier's revenue at an equilibrium with the piecewise expression $\pi_s^{\mathrm{cl}}(r)$ in equation (3). Setting $\beta=0$ in that expression gives the paper's no-licensing expression $\pi_s^{\mathrm n}(r)$ in equation (4). This milestone links the paper's algebraic profit comparison to the strategic quantity game, while keeping the equilibrium property as the premise.

The goal is the supplier's ex-post preference in Proposition 1. If $q^{\mathrm{cl}}$ is any equilibrium with licensing effectiveness $\beta$ and $q^{\mathrm n}$ is any equilibrium at $\beta=0$, then both equilibria exist and

This weak inequality is intentional. At $\beta=0$ the two games coincide, and there are other parameter values at which the profits tie. The comparison holds at the same innovation levels and the same wholesale price; it is not a comparison after re-optimizing the supplier's price or the manufacturers' investment decisions.

What the result establishes

For fixed investments and price, the supplier need not lose revenue by enforcing cross-licensing after observing the manufacturers' innovation. This gives mathematical content to the paper's claim that, without an initial commitment, the supplier will choose to enforce licensing at the final contract stage. The model does not specify a separate final-contract bargaining game, so the formal goal is the profit comparison that supports that interpretation. The result does not settle whether committing to licensing before innovation is preferable: changing the initial policy can change the innovation levels themselves, which the ex-post comparison holds fixed.

The authors prove Proposition 1 by comparing the supplier-profit expressions (3) and (4) in the manuscript's appendix. A machine-checked development would additionally secure the connection from the manufacturers' Nash conditions to those expressions, including the monopoly and zero-sales regimes. These statements are currently posed as open formalization targets; a Lean file with sorry only checks that the statements are well formed, not that the paper's argument has been verified by Lean. The general two-player Nash definition can be reused for other real-strategy games; the payoff and threshold definitions are specific to this supply chain.

Where the argument has to account for cases

The quantity equilibrium changes form as the wholesale price crosses $r_1$ and $r_2$. An argument confined to the two-selling-firms region misses cases in which $M_1$ sells nothing, or neither manufacturer sells. Comparing only the duopoly formulas cannot establish an inequality at every nonnegative price. The first milestone therefore covers all three regimes, and the goal compares the profits of actual equilibria. The fact that $T_2\ge T_1$ orders the possible monopoly toward $M_2$ under the paper's chosen labels; a formulation that silently assumes both equilibrium quantities are strictly positive would lose part of Proposition 1.

Formalization scope

All parameters and quantities are real. The permitted quantity strategies and wholesale prices are nonnegative. The paper treats $r$ as a wholesale price without writing a bound in Proposition 1; $r\ge0$ is made explicit because a negative price can reverse the supplier-profit inequality. The innovation ordering $0\le T_1\le T_2$ is the convention immediately preceding equation (2). Licensing effectiveness lies in $[0,1]$. Innovation costs $k_iT_i^2$ and the paper's bound $k_2>49/144$ are unnecessary once innovation levels are fixed, so they do not enter this mission's statements.

The formalization uses an explicit pair $(q_1,q_2)$, with the first coordinate for $M_1$. The quantity-game equilibrium is defined by unilateral payoff comparisons over $[0,\infty)$, and it is not defined by equation (2). Equation (2) is instead a theorem characterizing the equilibrium. The supplier's profit is defined as $r(q_1+q_2)$ for any pair, independently of equation (3). These choices prevent the goal from becoming an inequality between two expressions whose connection to the game has merely been assumed. Equation (2)'s missing closing parenthesis in the manuscript is interpreted as the displayed first quantity divided by three. No division in the model's displayed formulas has a variable denominator.

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, pp. 9–11 and Appendix p. A.1; published in Manufacturing & Service Operations Management, 2023. Manuscript; DOI.

Motivation

Distributed energy resources (DERs) — rooftop solar, home batteries, electric vehicles — turn electricity consumers into prosumers who can both buy and sell power. Their individual capacities are far too small to bid in a wholesale electricity market directly, so regulators have opened these markets to DER aggregators, intermediaries that pool many small resources and trade on their behalf (FERC Order 2222, 2020). An aggregator is a monopolist toward the prosumers it serves, and a profit-seeking monopolist between a market and its suppliers ordinarily distorts quantities: with a single unit price, the aggregator buys less than the efficient amount, and social welfare falls (Alshehri, Ndrio, Bose, Başar 2019, 2020).

Gao, Alshehri and Birge ask whether this loss can be avoided without regulating the aggregator. Their answer is that it can, provided the aggregator uses two-part pricing: a participation fee plus a per-unit price. This mission formalizes that efficiency result.

Setting

A power network has a finite set $K$ of nodes and a finite set $L$ of transmission lines. The ISO chooses nodal net injections $h\in\mathbb R^K$; the DC approximation of the AC network gives a matrix $B$ and line capacities $f$, and the network constraints are (5b): $\mathbf 1^\top h=0$ and $Bh\le f$.

A finite set $I$ of prosumers sits at the nodes. Prosumer $i$ owns a DER capacity $C_i\ge0$ and has a utility of consumption $u_i$ on $[0,Z]$, $Z>C_i$. Assumption 1: $u_i$ is increasing, strictly concave and continuous on $[0,Z]$, differentiable on $(0,Z)$, with $u_i'(z)\to\infty$ as $z\to0^+$ and $u_i'(z)\to0$ as $z\to Z^-$. A finite set $J$ of conventional generators sits at the nodes; generator $j$ produces $y_j\in[\underline y_j,\overline y_j]$ at cost $c_j(y_j)$. Assumption 2: $c_j$ is increasing, strictly convex and continuous on its interval, differentiable inside, with $c_j'\to0$ at the lower end and $c_j'\to\infty$ at the upper end.

Benchmark (direct participation). Prosumer $i$ sells $x_i$ and buys $d_i$ directly in the market at the locational price; only the net sale $z_i=x_i-d_i$ matters. Writing $X^k$, $D^k$, $Y^k$ for the nodal totals of sales, purchases and generation, the ISO solves the economic dispatch problem (9):

The wholesale prices $\lambda\in\mathbb R^K$ are the optimal Lagrange multipliers of the nodal balance constraints (5a).

Unregulated aggregation. Each prosumer sells only to the aggregator $\mathcal A$, which offers her a fee $P_i$ and a unit price $p_i$. At wholesale price $\lambda$ she maximizes the payoff (10), $p_ix_i-P_i+u_i(d_i+C_i-x_i)-\lambda d_i$ if she sells $x_i>0$ and $u_i(d_i+C_i)-\lambda d_i$ otherwise, over $x_i\in[0,C_i]$, $d_i\in[0,Z-C_i+x_i]$ (11). The aggregator earns (13) $P_i\mathbf 1\{x_i>0\}+(\lambda-p_i)x_i$ and chooses nonnegative offers anticipating the responses: a Stackelberg game $\mathcal G(\lambda)$ (Definition 1). The ISO now dispatches $x$ and $d$ separately, solving (21): maximize $\mathcal W_A=\sum_i u_i(d_i+C_i-x_i)-\sum_j c_j(y_j)$ subject to (5a), (5b) and (18) $0\le x\le C$, $0\le d\le Z-C+x$, $\underline y\le y\le\overline y$; its wholesale prices are again the multipliers of (5a).

Formalization targets

Goal: Theorem 1 (p. 14)

Under Assumptions 1–3 (Assumption 3: (9) is feasible), with $(h^*,z^*,y^*)$ the optimal solution of (9),

every optimal solution of (21) has $x-d=z^*$, $y=y^*$, $h=h^*$, the split $([z^*]^+,[-z^*]^+)$ is optimal for (21), and a price vector is a multiplier of (5a) for (21) if and only if it is one for (9).

Milestones

1. Lemmas 1 and 2 (pp. 5–6): a price-taking prosumer's problem (1) and generator's problem (3) have unique optima, characterized by $u'(C-z^*)=\lambda$ (2) and $c'(y^*)=\lambda$ (4).
2. Proposition 1 (p. 8): (9) has a unique optimum, and at every multiplier vector of (5a) it is a competitive equilibrium.
3. Lemma 3 (p. 10): the prosumer's optimal response to a two-part offer, in terms of $u'(z_1)=\lambda$, $u'(z_2)=p$.
4. Lemma 4 (p. 11): the aggregator's optimal offer is

5. Proposition 2 (p. 12): these offers form a Stackelberg equilibrium of $\mathcal G(\lambda)$.
6. Proposition 3 (p. 14): (21) has an optimum consistent with Lemmas 3, 4 and (4) at its multipliers.

Significance

The result. Theorem 1 shows that the efficiency loss attributed to profit-seeking aggregators is a consequence of one-part pricing, not of aggregation itself. With two-part pricing the aggregator passes the locational marginal price through as its unit price and extracts its profit only through participation fees, so welfare, dispatch and locational prices are exactly those of direct participation. The paper builds on this to analyse a regulated aggregator (§4) and the interaction of prosumer participation with generators' market power (§5, the companion mission of this series).

Formalizing it. The result is proved on paper, in a short argument relying on unstated conventions; no machine-checked version exists. A formal proof must make precise what "optimal Lagrange multiplier" means for a nonsmooth-at-the-boundary concave program on a network, handle the indicator in the prosumer's payoff (10) and the ties it creates, and settle the edge cases (nonpositive locational prices, capacity below the efficient consumption level) that the printed statements pass over.

Difficulty

The welfare identity is the easy part: the objective (20) and the balance (5a) of (21) depend on $(x,d)$ only through $x-d$, and the box (18) projects onto the box (6). The work lies elsewhere. Price equality requires an argument about saddle points of the Lagrangian on two different domains, not just optimal values. The prosumer's two-part problem (11) is discontinuous at $x=0$ because of the fee, so its optimal responses must be found by comparing branches, and the aggregator's optimality in Lemma 4 must hold against every nonnegative offer — including unit prices above the wholesale price — and every optimal response to it, not a selected one. The first-order conditions (2) and (4) require interior optima, which follow from the derivative limits in Assumptions 1–2 but only at positive prices.

Formalization scope

Everything lives in the namespace DERAggregation.Unregulated, in one definition file Setting. Nodes, prosumers, generators and lines are finite types; the node of prosumer $i$ is loc i. All quantities are real. Optimality is "feasible and at least as good as every feasible point", never a supremum. A multiplier vector of (5a) is a saddle point of the partial Lagrangian: (5a) and (5b) are dualized (with $\nu\ge0$ and complementary slackness for $Bh\le f$), the participant box is kept as the domain, and $h$ is free. Prices are never free variables and never defined by a closed form.

Assumptions 1–2 read "differentiable" as differentiable on the open interval and continuous on the closed one, since the derivative limits rule out differentiability at the endpoints; $0\le C_i$ and $\underline y_j<\overline y_j$ are added. Theorem 1 names no assumptions; it is stated under Assumptions 1–3. Problem (21) determines only $x-d$, so "the same $x^*,d^*$" is stated as equality of $x-d$ plus optimality of the canonical split. The first-order conditions are stated at nodes with positive price, Lemma 3 adds $P\ge0$ and $0<p\le\lambda$, and Lemma 4's second part adds the standing restriction $p\le\lambda$; each addition is disclosed in its item. Problem (21) is written in the separate variables $x$ and $d$ with the constraint $d\le Z-C+x$ exactly as printed: a formalization through $z=x-d$ would make Theorem 1 true by unfolding and is ruled out.