Discover · Prove2Me

Linear Optimization Mechanism Design Operations Research·Captain: iris

The Power of Simple Menus in Robust Selling Mechanisms: Robust Randomized Pricing over Fixed Price Levels Is a Finite Linear ProgramResearch Paper

Motivation

A seller offers one item to one buyer whose valuation lies in $[0,\bar v]$ and whose valuation distribution $F$ is not known. Robust mechanism design asks for a selling mechanism that performs well against every distribution consistent with the seller's partial information. Without restrictions on the menu, the optimal robust mechanism randomizes over a continuum of prices, which is hard to explain and to implement. S. Wang, The Power of Simple Menus in Robust Selling Mechanisms (arXiv:2310.17392v3, 2024; Management Science, 2025), asks how much is lost when the seller may randomize over at most $n$ prices only, and finds that very small menus (two or three prices) already recover most of the robust performance.

The paper's tool for this question is Theorem 1: once the $n$ price levels are fixed, the robust problem is a finite linear program. Every closed form in the paper (support, mean and quantile information) and every numerical study is a solution of that program.

The result extends Theorem 1 of Wang, Liu and Zhang (Minimax regret robust screening with moment information, 2024) from moment information and continuous menus to general ambiguity sets of the form (2) and finite menus.

Setting

An $n$ -level pricing mechanism posts price $v_l$ with probability $x_l$ , where $0\le v_1\le\dots\le v_n\le\bar v$ and $x$ lies in the probability simplex; $\Pi_n$ is the set of such mechanisms. A buyer with valuation $w$ pays in expectation $t(w)=\sum_{l:\,v_l\le w}x_lv_l$ , so the revenue against a distribution $F$ on $[0,\bar v]$ is $\mathrm{Rev}(\pi,F)=\int t\,dF$ . The clairvoyant benchmark is the best posted-price revenue $\mathrm{Rev}(\mathrm{OPT},F)=\max_{p\in[0,\bar v]}p\,(1-F(p-))$ .

The seller knows only that $F$ lies in the ambiguity set

\mathcal F=\Bigl\{F\in\mathcal P([0,\bar v]):\int\phi_k\,dF\ge0,\ k=1,\dots,K\Bigr\},

where each $\phi_k$ is bounded, piecewise continuous with finitely many segments, and nondecreasing within each segment (Assumption 1). Indicator constraints give support, quantile and multi-segment information; $\phi(w)=w-\mu$ gives a mean bound. The competitive ratio of $\pi$ is

\mathrm{CR}(\pi)=\inf_{F\in\mathcal F}\frac{\mathrm{Rev}(\pi,F)}{\mathrm{Rev}(\mathrm{OPT},F)} .

For Theorem 1, let $\mathcal B=\{b_1<\dots<b_m\}\subset(0,\bar v)$ be the breakpoints of the $\phi_k$ , let $u_1\le\dots\le u_{n+m}$ be the price levels and breakpoints in ascending order, $u_{n+m+1}=\bar v$ , let $\underline\phi_{k,j}=\lim_{w\to u_j-}\phi_k(w)$ and $S_j=\{l:v_l<u_j\}$ .

Formalization targets

Goal: Theorem 1 (Finite-LP), corrected

Under Assumption 1 with breakpoint set $\mathcal B$ , the constraint qualification and a common closing side (below), for every probability vector $x$

\mathrm{CR}(v,x)=\sup\Bigl\{r\ge0:\ \exists\lambda\ge0,\ \sum_k\underline\phi_{k,j}\lambda_{k,i}\le\sum_{l\in S_j}v_lx_l\ (j<i),\ r\,u_i+\sum_k\underline\phi_{k,j}\lambda_{k,i}\le\sum_{l\in S_j}v_lx_l\ (j\ge i)\Bigr\},

and $\sup_x\mathrm{CR}(v,x)$ equals the optimal value of the linear program (4).

Milestones, in proof order

Homogenization (proof of Proposition 1, p.ec6): $\inf_{F\in\mathcal F}\mathrm{Rev}(\pi,F)/(1-F(p-))$ equals a linear program over finite measures $H_p$ with $H_p([p,\bar v])=1$ .
Per-price strong duality (p.ec7), under the constraint qualification.
Proposition 1 (p.10): $\mathrm{CR}(\pi)$ equals the value of the semi-infinite program (3), for every $\pi\in\Pi_n$ and as optimal values.
Constraint reduction (proof of Theorem 1, p.ec8), under the common closing side: only the constraints at $w\to u_j-$ matter.
$\lambda$ -reduction (p.ec9): one multiplier column per grid cell gives (4).

Significance

Theorem 1 replaces a max-min problem over distributions and price densities with a linear program of $n+K(n+m+1)+1$ variables for each choice of price levels. The paper's Lemma 1 and Propositions 2–8 (optimal $n$ -level mechanisms for support, mean and quantile sets) and its grid searches over price levels are all solutions of this program, so a machine-checked Theorem 1 is the common foundation for each of them.

The mission also states which hypotheses the reformulation needs. As printed, Theorem 1 and Proposition 1 are false (counterexamples below), and the platform already records the predecessor statements, WangMinimaxRegret.Reformulation.theorem_1 and its duality step eq_3_4, as Disproved. The corrected statements keep the program (4) and the paper's support, quantile, multi-segment and mean examples. Each correction is necessary (a counterexample satisfies every other hypothesis); their sufficiency is argued but not yet proved, which is part of what this mission asks for. No part of this paper has been formalized before; the homogenization step has a Proved analogue for moment sets (WangMinimaxRegret.Reformulation.eq_2_3).

Difficulty

The printed proof dualizes nature's problem at each price $p$ by Sion's minimax theorem. Neither side is compact: $H_p$ has unbounded mass and the multipliers are unbounded. The step fails for $K=1$ , $0<c<\bar v$ , $\phi(w)=\min(w-c,0)$ , a single price $c$ : here $\mathcal F=\mathcal P([c,\bar v])$ and $\mathrm{CR}=c/\bar v$ , yet (3) and (4) have value $0$ , because the constraints at $w\uparrow c$ force $r\,p\le0$ . The same set written as $\phi=\mathbb 1[w\ge c]-1$ gives the correct $c/\bar v$ . The program depends on how $\mathcal F$ is written, the competitive ratio does not. The correction is a constraint qualification: every $\phi_k$ is a step function, or some $F_0\in\mathcal F$ satisfies the non-step constraints strictly.

The reduction to left limits assumes that $\sum_k\lambda_k\phi_k$ attains its supremum on each cell at the cell's right end. With $\phi_1=\mathbb 1[w\le\omega]-1$ , $\phi_2=\mathbb 1[w\ge\omega]-1$ and one price $v_1<\omega$ , $\mathcal F=\{\delta_\omega\}$ and $\mathrm{CR}=v_1/\omega$ , but (4) is unbounded: at $\omega$ the sum exceeds both of its one-sided limits. The correction is a common closing side: at each breakpoint all $\phi_k$ are left-continuous, or all are right-continuous.

A proof therefore needs a duality argument without compactness (a finite-dimensional reduction for step functions, a Slater-type argument otherwise), and limits at the grid points together with the closedness of finitely generated cones.

Formalization scope

Valuations, prices and the $\phi_k$ are real; laws are Borel probability measures on $\mathbb R$ that give no mass to the complement of $[0,\bar v]$ , and each constraint of (2) carries integrability. The payment is the step function $t(w)=\sum_{v_l\le w}x_lv_l$ , with the atom at $w$ included. All values (competitive ratio, the programs (3), (4) and the intermediate programs) lie in EReal, so an unbounded program has value $+\infty$ . The competitive ratio ranges over the laws with $\mathrm{Rev}(\mathrm{OPT},F)>0$ : a law with zero benchmark gives $0/0$ . The merged grid is a hypothesis (a monotone vector whose values are $\mathcal V+\mathcal B$ as multisets, ties kept), indices are 0-based, and at a grid point $u_j=0$ the left limit is replaced by $\phi_k(0)$ . The paper's " $0<b_1$ , $b_m<\bar v$ " is read as: no $\phi_k$ jumps at $0$ or $\bar v$ . $K=0$ , zero probabilities and tied prices are allowed; $\mathcal F$ is not assumed nonempty.

The theorems are statements of equality of values. A reading that compares only optimal values over $x$ would drop half of the goal; the goal states the per-mechanism equality as well. The verification files prove that the support example satisfies every hypothesis of the goal, that the indexing of (4) reproduces the ratio $c/\bar v$ of Proposition 2 for $n=1$ , and that the second counterexample violates the closing-side condition.

Needed infrastructure: Lebesgue integration against finite measures, Mathlib's Function.leftLim, stdSimplex, and LP duality for finitely many constraints (closedness of finitely generated cones is Proved on the platform as ConvexCone.isClosed_finite_cone). The duality milestone, a strong-duality theorem for measure programs with piecewise monotone constraint functions under a constraint qualification, is reusable beyond this mission. Proofs of any milestone are welcome, as are counterexamples if a corrected statement turns out to be false.

Selected references

S. Wang, The Power of Simple Menus in Robust Selling Mechanisms, arXiv:2310.17392v3, 2024; Management Science, 2025. https://arxiv.org/abs/2310.17392
S. Wang, S. Liu, J. Zhang, Minimax Regret Robust Screening with Moment Information, Manufacturing & Service Operations Management 26(3), 2024. https://doi.org/10.1287/msom.2023.0072
M. Sion, On general minimax theorems, Pacific Journal of Mathematics 8(1), 1958. https://doi.org/10.2140/pjm.1958.8.171
R. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58

25 thms1 active userReviewed

Convex Optimization Operations Research Optimization·Captain: iris

On the Equivalence and Performance of Distributionally Robust Optimization and Robust Satisficing Models: Every Robust Satisficing Optimum Is Optimal for Wasserstein DRO with Radius −1/α, α ∈ ∂κ(τ)Research Paper

Motivation

Data-driven decisions under uncertainty start from $S$ historical samples $\hat z_1,\dots,\hat z_S$ of a random outcome and a cost $f(x,z)$ of a decision $x$ . Minimizing the sample average cost overfits: the decision performs worse out of sample than the sample average suggests. Two models hedge against this with the type-1 Wasserstein distance around the empirical distribution $\mathbb P^\dagger$ .

Wasserstein distributionally robust optimization (DRO) fixes a radius $\theta$ and minimizes the worst expected cost over all distributions within distance $\theta$ of $\mathbb P^\dagger$ (Mohajerin Esfahani and Kuhn 2018; Gao and Kleywegt 2023). Robust satisficing (RS) fixes instead a cost target $\tau$ and minimizes the fragility $k$ , the rate at which the expected cost may exceed $\tau$ per unit of Wasserstein distance (Long, Sim and Zhou 2023). DRO suits a cost-driven decision maker who can name a plausible radius; RS suits a goal-driven one who can name a target. Sim, Zhao and Zhou (2023) observed that the two produce the same solutions in linear regression with an unbounded support.

Wang, Ran, Zhou and He (Manufacturing & Service Operations Management, 2025; this mission follows the authors' manuscript) show that the two models trace the same family of optimal solutions in general convex problems, and give the map between the parameters. The direction RS → DRO, Theorem 1, is the goal of this mission.

Setting

Let $\mathcal X$ be a set of decisions in a real vector space, $\mathcal Z$ a support set, $\rho(z,z')\ge0$ a transport cost with $\rho(z,z)=0$ , and $\hat z_1,\dots,\hat z_S\in\mathcal Z$ the samples. The worst-case loss of a decision $x$ and a multiplier $k\ge0$ is

h(x,k)=\frac1S\sum_{s\in[S]}\sup_{z\in\mathcal Z}\big\{f(x,z)-k\,\rho(z,\hat z_s)\big\}\in(-\infty,+\infty].

By Wasserstein duality the two models reformulate as follows (pp.7–8 of the paper).

Problem (DRO) with radius $\theta\ge0$ , written DRO( $\theta$ ): minimize $\tau+k\theta$ over triples $(\tau,k,x)$ with $x\in\mathcal X$ , $k\ge0$ and $h(x,k)\le\tau$ .
Problem (RS) with target $\tau$ , written RS( $\tau$ ): minimize $k$ over pairs $(x,k)$ with $x\in\mathcal X$ , $k\ge0$ and $h(x,k)\le\tau$ . Its optimal value is the RS value function $\kappa(\tau)\in[0,\infty]$ (written $k^*(\tau)$ in the appendix), which is $+\infty$ when RS( $\tau$ ) is infeasible.

Three constants frame the targets. The empirical optimum is $Z_0=\inf_{x\in\mathcal X}\frac1S\sum_s f(x,\hat z_s)$ . The robust optimum is $\bar\tau=\inf_{x\in\mathcal X}\sup_{z\in\mathcal Z}f(x,z)$ . The largest transport radius is $\bar\theta=\frac1S\sum_s\sup_{z\in\mathcal Z}\rho(z,\hat z_s)$ . The subdifferential $\partial\kappa(\tau)$ is the set of $\alpha$ with $\kappa(\tau)<\infty$ and $\kappa(\tau')\ge\kappa(\tau)+\alpha(\tau'-\tau)$ for all $\tau'$ .

In Lean the data form DRORSEquiv.Model (fields X, Z, ρ, zhat, f), and the objects are worstCaseLoss, IsFeasible, IsRSOptimal, IsDROOptimal, rsValue ( $\kappa$ ), empiricalOptimum ( $Z_0$ ), tauBar, thetaBar and subdiff.

Formalization targets

Goal: Theorem 1 (corrected)

Assume $\mathcal X$ is convex, $f(\cdot,z)$ is convex on $\mathcal X$ for every $z\in\mathcal Z$ , $\bar\tau$ is finite, and $Z_0\le\tau_{rs}\le\bar\tau$ .

(a) If $\tau_{rs}<\bar\tau$ , or $\tau_{rs}=\bar\tau$ and either $\bar\theta<\infty$ or $\kappa=\infty$ on $(-\infty,\tau_{rs})$ , then

\exists\,\theta^*\ge0\ \ \forall\,(x^*,k^*)\text{ optimal for RS}(\tau_{rs}):\quad(\tau_{rs},k^*,x^*)\text{ is optimal for DRO}(\theta^*).

(b) For every optimal $(x^*,k^*)$ of RS( $\tau_{rs}$ ) and every $\alpha\in\partial\kappa(\tau_{rs})$ : if $\tau_{rs}<\bar\tau$ then $\alpha<0$ ; and if $\alpha<0$ then $(\tau_{rs},k^*,x^*)$ is optimal for DRO( $-1/\alpha$ ).

The printed theorem is corrected in two places. At $\tau_{rs}=\bar\tau$ with $\bar\theta=\infty$ it fails ( $f=1-1/(1+z)$ on $[0,\infty)$ ) unless $\bar\tau$ is the left end of $\operatorname{dom}\kappa$ , where the radius $0$ works. The formula $\theta^*=-1/\alpha$ needs $\alpha<0$ , because $0\in\partial\kappa(\bar\tau)$ can occur ( $f=z$ on $[0,1]$ ). Each theorem item lists its differences from the source.

Milestones

The milestones follow the proof in Appendix A (pp.33–34): the boundary cases $\tau_{rs}=Z_0$ (radius $0$ ) and $\tau_{rs}=\bar\tau$ (radius $\theta\ge\bar\theta$ ); the rewriting of DRO( $\theta$ ) as $\min_{\tau\ge Z_0}\tau+\theta\kappa(\tau)$ ; Lemma 1 ( $\kappa$ convex, with $\mathcal X$ convex added); $\kappa$ nonincreasing; nonempty bounded $\partial\kappa$ on $\operatorname{int}(\operatorname{dom}\kappa)$ ; negativity of subgradients below $\bar\tau$ when RS( $\tau_{rs}$ ) has an optimum; and the fact that a negative subgradient $\alpha$ makes $\tau_{rs}$ minimize $\tau+\kappa(\tau)(-1/\alpha)$ .

Significance

Theorem 1 says that a decision maker who fixes a cost target loses nothing relative to one who fixes a Wasserstein radius: every RS solution is a DRO solution for the radius $-1/\alpha$ , with $\alpha$ a subgradient of the RS value function. Together with the easy converse (Proposition 1), it lets results proved for one model transfer to the other: out-of-sample guarantees, tractable reformulations, and the choice of a parameter by cross-validation. The paper builds on it the equivalence for adaptive two-stage models (Theorem 2) and for the globalized models GDRC and GRS (Theorems 3–5).

The paper's result is proved on paper, but the proof leaves gaps that a formal proof has to close: the endpoint $\bar\tau$ needs $\bar\theta<\infty$ ; $0\notin\partial\kappa$ needs attainment of $\kappa$ ; Lemma 1 uses convexity of $\mathcal X$ without stating it; and the left end of $\operatorname{dom}\kappa$ (where the radius $0$ works) is not treated. No part of the result has a machine-checked proof yet. The convex-analysis milestones (convexity of a parametric value function in $[0,\infty]$ , subgradients of an extended-valued convex function of one variable) are reusable for other value-function arguments.

Difficulty

The obvious argument is the paper's: make $\tau_{rs}$ a stationary point of $g(\tau)=\tau+\theta^*\kappa(\tau)$ . It fails in three places. First, $\kappa$ is an infimum that need not be attained, so convexity (Lemma 1) needs an $\varepsilon$ -argument in $[0,\infty]$ , and the sign argument for subgradients fails without an optimal RS solution. Second, a subgradient exists only in the interior of $\operatorname{dom}\kappa$ , which can start strictly above $Z_0$ . At its left end no subgradient need exist, and the radius $\theta^*=0$ must be used instead. Third, at $\bar\tau$ the subgradient can be $0$ , and the case needs a separate argument through $\bar\theta$ , which works only when $\bar\theta$ is finite. Clause (b) is short, since a DRO-feasible $(\tau,k,x)$ has $k\ge\kappa(\tau)$ . The case analysis behind clause (a) is the substance.

Formalization scope

The formalization works with the reformulated Problems (DRO) and (RS) themselves, not with the measure-level problems (1) and (2). The standing assumptions of p.7 (Polish $(\mathcal Z,\rho)$ , $f(x,\cdot)\in L^1(\mathbb P^\dagger)$ , bounded growth rate) are not used. The decision space is any real vector space, $\rho$ is any cost with $\rho\ge0$ and $\rho(z,z)=0$ , the samples lie in $\mathcal Z$ , and $S\ge1$ ; samples are indexed by Fin S. $h$ , $Z_0$ , $\bar\tau$ , $\bar\theta$ are computed in EReal, and $\kappa$ in ℝ≥0∞. RS-optimality and DRO-optimality range over the full feasible sets, with $\tau$ ranging over all reals in DRO. The subdifferential is empty where $\kappa=\infty$ . Each $-1/\alpha$ carries the hypothesis $\alpha<0$ , since Lean's $-1/0=0$ would otherwise make the radius $0$ by default.

Clause (a) quantifies one radius over all optimal RS solutions ( $\exists\theta^*$ before $\forall$ ). If RS( $\tau_{rs}$ ) has no optimal solution, clause (a) holds for any radius, and this is the intended reading, since the theorem speaks of "the optimal solution". The measure-level Wasserstein objects already on the platform are not imported.

Contributions are welcome on any milestone. Lemma 1 and the subdifferential facts are independent of the DRO setting and are natural first targets.

Selected references

Z. Wang, L. Ran, M. Zhou, L. He, On the Equivalence and Performance of Distributionally Robust Optimization and Robust Satisficing Models, Manufacturing & Service Operations Management, 2025 (authors' manuscript followed here). https://doi.org/10.1287/msom.2023.0531
D. Z. Long, M. Sim, M. Zhou, Robust Satisficing, Operations Research 71(1):61–82, 2023. https://doi.org/10.1287/opre.2021.0238
R. Gao, A. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, Mathematics of Operations Research 48(2), 2023. https://doi.org/10.1287/moor.2022.1275
P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Mathematical Programming 171, 2018. https://doi.org/10.1007/s10107-017-1172-1
M. Sim, L. Zhao, M. Zhou, Tractable Robust Supervised Learning Models, SSRN 3981205, 2023. https://ssrn.com/abstract=3981205
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

19 thms1 active userReviewed

Bandit Algorithms Convex Optimization Machine Learning+2·Captain: iris

Optimal Learning for Structured Bandits: DUSA Has Asymptotic Regret at Most (1+ε)(C(P)+ε(1+Σₓ∆(x,P))) log T, Matching the Lower Bound C(P) as ε → 0, with O(log T) Exploration RoundsResearch Paper

Why structured bandits

In a multi-armed bandit a learner repeatedly pulls one of finitely many arms and observes a random reward, trying to earn as much as an omniscient learner who knows the best arm. In many operations problems the arms are not unrelated: in dynamic pricing the probability of no sale is monotone in the price, in assortment or dosage problems mean rewards vary in a Lipschitz, linear or convex way across arms. Such structural information can make some arms cheap to rule out and others impossible to rule out without sampling them, and a learner that ignores it pays avoidable regret.

The asymptotic cost of learning under structure is known exactly. Graves and Lai (1997) showed that every uniformly good policy has regret at least $C(P)\log T$ , where $C(P)$ is the value of a semi-infinite optimization problem over exploration rates; Combes, Magureanu and Proutière (2017) gave an algorithm (OSSB) attaining it by solving that problem in every round. Van Parys and Golrezaei (Management Science, 2024; preprint arXiv:2007.07302v3) proposed DUSA, which reaches the same bound while solving the convex dual of a relaxation of the problem, and only in rounds where a cheap one-dimensional test says that the collected information is insufficient. This mission formalizes their main regret guarantee.

The model

There are finitely many arms $X$ and a finite set $\mathfrak R\subset[0,\infty)$ of possible rewards. A reward distribution is a table $Q=(Q(r,x))$ in

\mathcal P_\Omega=\Big\{Q\ge0:\ \sum_{r\in\mathfrak R}Q(r,x)=1\ \forall x\in X\Big\}.

In round $t$ the learner pulls $x_t$ and receives $R_t(x_t)$ , where the rewards $R_t(x)$ are independent across arms and rounds with law $P(\cdot,x)$ . The true $P$ is unknown except that it lies in a known structure set $\mathcal P\subseteq\mathcal P_\Omega$ , closed, convex and with non-empty interior (relative to the affine hull of $\mathcal P_\Omega$ ). Write $x^\star(P)$ for the set of optimal arms, $\mathrm{Rew}^\star(P)$ for the optimal mean, $\tilde X(P)$ for the suboptimal arms and $\Delta(x,P)$ for the gaps. The regret of a policy is $\mathrm{Reg}_\pi(T,P)=T\,\mathrm{Rew}^\star(P)-\sum_{t\le T}\mathbb E[\sum_r rP(r,x_t)]$ .

A distribution $Q\in\mathcal P$ is deceitful for an arm $x'$ if it agrees with $P$ on the optimal arms but makes $x'$ better than them. With the information distance $I$ (the Kullback–Leibler divergence), $\mathrm{Dist}(\eta,x',P)=\inf_{Q\in\mathrm{Deceit}(x',P)}\sum_{x\in\tilde X(P)}\eta(x)I(P(x),Q(x))$ , and the lower-bound constant is

C(P)=\inf_{\eta\ge0}\sum_{x\in\tilde X(P)}\eta(x)\Delta(x,P)\quad\text{s.t.}\quad\mathrm{Dist}(\eta,x,P)\ge1\ \ \forall x\in\tilde X(P).

Assumption 1 defines $\mathcal P'$ : distributions in the interior of $\mathcal P$ with a unique optimal arm and no borderline suboptimal arm.

DUSA keeps a counter $s_t$ of exploration rounds, reference rates $\eta'_t$ and dual certificates $\mu_t$ . In each round it checks, through a dual function $\mathrm{Dual}$ , whether the counts $N_t/\log t$ already certify $\mathrm{Dist}\ge1+\epsilon$ for every empirically deceitful arm. If so, it exploits; otherwise it explores, calling a shallow update (a projection, Algorithm 2) and a deep update (a strongly convex program, Algorithm 3).

Formalization targets

Goal: Theorem 3

For $P\in\mathcal P'$ and $0<\epsilon<1/|X|$ , every run of DUSA satisfies

\limsup_{T\to\infty}\frac{\mathrm{Reg}_\pi(T,P)}{\log T}\le(1+\epsilon)\Big(C(P)+\epsilon\big(1+\textstyle\sum_{x}\Delta(x,P)\big)\Big), \qquad \limsup_{T\to\infty}\frac{\mathbb E[s_T]}{\log T}\le(1+\epsilon)|X|^2\big(\|\eta'_\epsilon(P)\|_\infty+\epsilon\big).

Milestones

The milestones follow the proof in Appendix D:

Lemma 5 and Lemma 6, two concentration bounds (Hoeffding at a stopping time; the information distance of empirical distributions), stated for every non-anticipating policy.
Lemma 7, the finite regret of exploitation rounds with a badly estimated empirical optimum.
Lemma 1 (weak and strong duality between $\mathrm{Dual}$ and $\mathrm{Dist}$ ) and Lemma 8, which turns a passed test into the event (39).
Lemma 9, openness of the unique-optimum region and continuity of $\mathrm{Rew}_{\max}$ (corrected; see below).
Lemmas 10 and 11, deterministic counting facts about exploration rounds.
Propositions 4 and 5, existence and continuity of the deep update on $\mathcal P'$ and stability of the shallow update.

Significance

Clause (21) together with the Graves–Lai lower bound shows that DUSA is asymptotically optimal up to $\epsilon$ in every structured bandit of this class, which covers unstructured, Lipschitz, linear, convex, unimodal, dispersion and divergence structures. Clause (22) shows that the convex programs are solved only $O(\log T)$ times, which is the computational point of the algorithm. Lemma 6, a concentration inequality for $\sum_xN_t(x)I(P_t(x),P(x))$ for arbitrary discrete distributions, is of independent use in nonparametric bandits.

The result is proved in the paper. No part of it is machine-checked: the platform holds asymptotic optimality results for unstructured bandits (KL-UCB, Thompson sampling) but nothing for structured ones. A complete development would be the first formal proof of asymptotic optimality under structural information, and the duality and continuity milestones are reusable for other algorithms built on the Graves–Lai program.

Difficulty

The obvious approach, a per-arm regret decomposition with concentration of each arm's mean, does not reach $C(P)$ : the lower bound couples the arms through $\mathrm{Dist}$ , and the right exploration rate of one arm depends on the estimates of all of them. The proof needs (i) duality to relate the sufficient-information test to $\mathrm{Dist}$ at the empirical distribution, (ii) continuity of the deep update on $\mathcal P'$ and stability of the shallow update near $P$ , so that targets computed from estimates converge to the target at $P$ , and (iii) concentration of the information distance uniformly over random sample sizes. Each of these is a separate piece of analysis (convex duality with Slater's condition, parametric optimization, martingale concentration).

Formalization scope

Arms form a nonempty Fintype, rewards a Finset ℝ of nonnegative reals, and distributions are functions R → X → ℝ with the product topology. The paper's $\mathcal P$ is written S. Interior means the interior relative to the affine hull of $\mathcal P_\Omega$ (App. B). $I$ , $\mathrm{Dist}$ , $C$ , $\mathrm{Rew}_{\max}$ and $\mathrm{Dual}$ take values in EReal, with $\inf\emptyset=+\infty$ ; the shallow update returns an Option (none is $+\infty$ ). The environment is an independent reward table with law $P$ plus an independent randomization seed. DUSA is a policy built from a DusaRules structure: the order of the initial pulls, the initial values, each tie-break and the deep update's fallback are free fields, and every theorem holds for all of them. $\limsup a_T/\log T\le b$ is stated as "for every real $c>b$ , eventually $a_T\le c\log T$ ".

Three deviations are declared in the items. Assumption 1(2) is printed for all arms and is then never satisfied, so it is read over suboptimal arms; under the literal reading $\mathcal P'$ is empty and the goal would be vacuous. Lemma 9(ii) is false as printed when $P$ has two optimal arms and is stated for $P$ with a unique optimal arm, the case the proof treats. Lemma 7's proof bounds each gap by one, and as printed the lemma fails for large rewards (two Bernoulli-type arms with rewards $\{0,M\}$ , $M>2000$ ), so its bound is multiplied by $\max(1,\max_x\Delta(x,P))$ , which is the printed bound whenever every gap is at most one.

The development needs finite-dimensional convex duality, parametric continuity of strongly convex programs, and martingale concentration for empirical distributions of a non-anticipating policy. Contributions to any milestone, and general lemmas on these three topics, are welcome.

Selected references

B. Van Parys, N. Golrezaei, Optimal Learning for Structured Bandits, Management Science, 2024; preprint arXiv:2007.07302v3, 2023. https://arxiv.org/abs/2007.07302
T. L. Graves, T. L. Lai, Asymptotically efficient adaptive choice of control laws in controlled Markov chains, SIAM Journal on Control and Optimization 35(3):715–743, 1997.
R. Combes, S. Magureanu, A. Proutière, Minimal Exploration in Structured Stochastic Bandits, NeurIPS 2017. https://arxiv.org/abs/1711.00400
S. Magureanu, R. Combes, A. Proutière, Lipschitz Bandits: Regret Lower Bounds and Optimal Algorithms, COLT 2014, PMLR 35:975–999. https://proceedings.mlr.press/v35/magureanu14.html

20 thms1 active userReviewed

Dynamic Programming Operations Research Optimization+1·Captain: iris

Multi-product Dynamic Pricing with Limited Inventories under a Cascade Click Model: The Cascade Correction Policy Loses $O(\log k)$ Against the Deterministic BenchmarkResearch Paper

Selling a ranked list of products

Online retailers show products in a fixed order, and a customer reads the list from the top. Models of this behavior, the cascade click model, come from sponsored search (Craswell et al., 2008; Aggarwal et al., 2008) and now drive assortment and ranking decisions. Najafi, Duenyas, Jasin and Uichanco combine it with the classical problem of pricing a limited inventory over a finite horizon (Gallego and van Ryzin, 1994, 1997). They ask whether a simple, re-optimization-free policy can price a whole ranked list with a loss that grows only logarithmically in the scale of the problem. Earlier work reached logarithmic loss by a linear correction of the rates, for models whose deterministic problem is convex (Jasin, 2014). In the cascade model it is not convex.

Setting

There are $J$ products in a fixed order, and $T$ periods. In each period a customer arrives with probability $\lambda$ . She examines product $1$ ; at product $j$ she buys with the conditional purchase rate $\alpha_j\in[0,u]$ , set through the price $p_j(\alpha_j)$ , and otherwise continues with probability $\zeta_j$ . The arrival rate at $j$ and the expected purchase rate are

\sigma_j(a)=\lambda\prod_{i<j}(1-a_i)\zeta_i,\qquad v_j(a)=\sigma_j(a)a_j .

Let $r_j(\alpha)=\alpha p_j(\alpha)$ , the revenue rate, strictly concave with $|r_j''|\le w$ . The deterministic problem DET maximizes $\sum_t\sum_j\sigma_j(\alpha_t)r_j(\alpha_{tj})$ over schedules with $\sum_t\sigma_j(\alpha_t)\alpha_{tj}\le y_j$ , and its value is $V^D$ . It has a stationary optimal solution $a^D$ under mild conditions.

The Cascade Correction (CC) policy starts from $v^D=v(a^D)$ . In period $t$ it sets

\hat v_t=v^D-\delta^v_t,\qquad \delta^v_t=\sum_{s<t}\frac{\Delta_s}{T-s},\qquad \hat\sigma_{t,1}=\lambda,\quad \hat\sigma_{t,j+1}=\zeta_j(\hat\sigma_{tj}-\hat v_{tj}),

where $\Delta_s$ is the demand error of period $s$ , and it applies $\hat\alpha_{tj}=\hat v_{tj}/\hat\sigma_{tj}$ when the product is in stock and this rate is admissible, and the turn-off price otherwise.

In the asymptotic regime, horizon and inventory are scaled to $N=kT$ and $Y=ky$ , the values are $V^{k,D}$ for DET and $V^{k,CC}$ for the policy.

Formalization targets

Goal: the logarithmic loss (Theorem 3, p.25)

If $a^D\in[L,U]^J$ for some $0<L<U<1$ and $|r_j'|$ is bounded on $[L,U]$ , then there is $\Psi_2>0$ independent of $k\ge1$ with

V^{k,D}-V^{k,CC}\le\Psi_2(1+\log k).

The constant may depend on the instance, on $(T,y)$ and on $a^D$ . It is quantified before $k$ .

Stationarity of DET

Lemma EC.1, Claim EC.2, the domination of every schedule by a stationary one, Lemma 4 and Lemma 5 ( $a^D_j<u$ ), and the scaling $V^{k,D}=kV^D=kT\tilde V^D$ .

The analysis of the policy

The expansion (17), the bound $\|\delta^\sigma\|_\infty\le Q\|\delta^v\|_\infty$ , Lemma EC.2 (below a threshold the policy follows its ideal path), $\sum_t\mathbf E[(\delta^v_{tj})^2]=O(\log k)$ , Lemma EC.3 ( $\mathbf E[k-\tau^k]\le1+\Psi\log k$ ), Observation 1, the decomposition $\mathbf E[R^{k,CC}(1,\tau^k-1)]=\Phi_1+\Phi_2$ , Observation 6, and $\Phi_2\ge-O(\log k)$ .

Significance

Theorem 3 says that a policy which solves DET once, and only a triangular linear system in every period, loses $O(\log k)$ against an upper-bound benchmark. In particular the relative loss is $O(\log k/k)$ . The paper's other guarantee, for the fixed-price policy, is $O(\sqrt k)$ . The correction acts on the expected purchase rates and recovers conditional rates as a ratio of two corrected terms, and this is the idea that makes a linear correction work without convexity.

The result is proved on paper but has no machine-checked proof, and the formalization adds more than a check. The published proof needs repair at several points, each of which leaves the $O(\log k)$ intact: the reduction to binding constraints is not valid, the threshold conditions fail at $\lambda=1$ , Observation 1 claims an equality that is false, and Observation 2 uses an orthogonality that is false. Lemma 4 needs continuity of $r_j$ at $0$ , and Lemma 5 needs $\lambda>0$ . The items state the repaired results and record each repair. The mission also adds to the platform a finite path-law treatment of an adaptive pricing policy.

Difficulty

DET is not concave in the rates: the objective mixes the rates of different products through $\sigma_j$ . So the Jensen argument that gives stationarity in standard revenue management does not apply to the rates, and the argument has to go through the value function in the arrival rates and inventories.

For the policy, the natural idea is the linear correction of conditional rates, and it fails to apply: the demand errors are errors in $v$ , and $a=v/\sigma$ is a ratio of two random quantities. The applied rate is then nonlinear in the correction. A second-order expansion of the revenue gives linear terms in the correction summed up to a random time. These do not vanish, since a sum of martingale terms up to $\tau$ is not a stopped martingale. They have to be estimated against the tail of $\tau$ .

Formalization scope

Rates are the actions: rates lie in $[0,u]$ , covering $\Omega_\alpha=[0,u]$ and $(0,u]$ , and rate $0$ is the turn-off price, with revenue $0$ . Concavity is assumed on $(0,u]$ only. A period's outcome is a sold product or no sale, so the law of a policy is an explicit finite sum over outcome paths, with no measure theory in any statement; the general path law is its own definition. A policy maps the list of past outcomes to rates. The state of CC is a fold over the history, with natural-number inventories. Periods and products are 0-based in Lean. Scaling uses a real $k\ge1$ with $kT$ and $ky_j$ integers; the inventory $y$ is real.

$V^{k,D}$ in the goal is the supremum of DET for the scaled problem, not a formula in $a^D$ , and $V^{k,CC}$ is the realized revenue under the policy's own law, not a quantity at the ideal rates or a stopped sum. The verification files prove that the suprema are true suprema, that the path law is a probability, and that the hypotheses of the goal are jointly satisfiable on a worked instance, with $V^{2,D}=1/2$ and $V^{2,CC}=1/4$ . So the goal is not vacuous, and the correction is not trivial.

A complete development needs: the concavity of $R^D$ by induction on products; a Jensen argument for the domination; a compactness argument for Lemma 4; orthogonality of martingale differences and Doob's maximal inequality, for the finite path law (the platform has both on filtered measure spaces); and a stopped-sum estimate for Observation 1. The finite-path martingale lemmas are reusable beyond this mission. Contributions that prove them in general form are welcome, and so are proofs that avoid the printed reduction to binding constraints, as the items already do.

Theorem 1 ( $V^*\le V^D$ ), the fixed-price bound of Theorem 2, and the structural Lemmas 1–3 are not part of this mission.

Selected references

S. Najafi, I. Duenyas, S. Jasin, J. Uichanco, Multi-product Dynamic Pricing with Limited Inventories under a Cascade Click Model, SSRN abstract_id=3362921 (2023); Manufacturing & Service Operations Management (2023). https://ssrn.com/abstract=3362921, https://doi.org/10.1287/msom.2021.0504
G. Gallego, G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8) (1994). https://doi.org/10.1287/mnsc.40.8.999
G. Gallego, G. van Ryzin, A Multiproduct Dynamic Pricing Problem and Its Applications to Network Yield Management, Operations Research 45(1) (1997). https://doi.org/10.1287/opre.45.1.24
S. Jasin, Reoptimization and Self-Adjusting Price Control for Network Revenue Management, Operations Research 62(5) (2014). https://doi.org/10.1287/opre.2014.1294
N. Craswell, O. Zoeter, M. Taylor, B. Ramsey, An Experimental Comparison of Click Position-Bias Models, WSDM (2008). https://doi.org/10.1145/1341531.1341545
G. Aggarwal, J. Feldman, S. Muthukrishnan, M. Pál, Sponsored Search Auctions with Markovian Users, WINE (2008). https://doi.org/10.1007/978-3-540-92185-1_48

20 thms1 active userReviewed

Operations Research Optimization Probability+1·Captain: iris

A Pareto Dominance Principle for Data-Driven Optimization: Under an Exponential Family Whose Statistic Obeys an LDP, the Distributionally Robust Predictor-Prescriptor Pair Is Pareto DominantResearch Paper

Motivation

A decision-maker wants to solve $\min_{x\in X} c(x,\theta_\star)$ , but the model $\theta_\star$ of the data-generating process is unknown. All that is available is one observed trajectory $\xi_1,\dots,\xi_T$ of a process, possibly serially dependent, whose law belongs to a known family $\{\mathbb P_\theta:\theta\in\Theta\}$ . Sample average approximation, regularized estimators and distributionally robust optimization (DRO) are all ways to turn the data into a cost estimate and a decision, and each comes with its own tuning. Which of them is best, and in what sense, is the question of T. Sutter, B. P. G. Van Parys and D. Kuhn, A Pareto dominance principle for data-driven optimization (arXiv:2010.06606v4, Operations Research, 2024).

Timeline:

2017–2021. Van Parys, Mohajerin Esfahani and Kuhn (arXiv:1704.04118, Management Science 2021) showed, for finite-state i.i.d. data and the empirical distribution, that a DRO predictor with a relative-entropy ambiguity set is optimal among predictors that depend on the data through the empirical distribution.
2020–2023. The present paper removes the i.i.d. and finite-state restrictions. It works with any statistic satisfying a large deviation principle (LDP), and, under an exponential-family assumption, it compares against all ways of mapping data to decisions, not only those that factor through the statistic.

Setting

Data $\xi_t\in\mathbb R^m$ live on one measurable space $(\Omega,\mathcal F)$ , and $\mathcal F_T=\sigma(\xi_1,\dots,\xi_T)$ . The model space $\Theta\subseteq\mathbb R^d$ is the relative interior of a convex set, and $\mathbb P_\theta$ is a probability measure for each $\theta\in\Theta$ . The decision set $X\subseteq\mathbb R^n$ is compact, and the model-based predictor $c(x,\theta)$ is bounded and uniformly continuous on $X\times\Theta$ ; $c$ also denotes its extension to $X\times\operatorname{cl}\Theta$ .

A data-driven predictor $\widehat c=\{\widehat c_T(x)\}$ is continuous in $x$ , adapted to $\{\mathcal F_T\}$ , dominated by one integrable variable, and converges in probability under every $\mathbb P_\theta$ , as does $\min_x\widehat c_T(x)$ . A data-driven prescriptor $\widehat x_T\in\arg\min_{x}\widehat c_T(x)$ is an adapted minimizer of such a predictor; $\widehat{\mathcal X}$ is the set of these pairs. The meta-problem (2.4b) asks, for every $\theta\in\Theta$ at once, to minimize the asymptotic in-sample risk $\lim_T\mathbb E_\theta[\widehat c_T(\widehat x_T)]$ subject to an exponential decay of the out-of-sample disappointment:

\limsup_{T\to\infty}\frac1T\log\mathbb P_\theta\big[c(\widehat x_T,\theta)>\widehat c_T(\widehat x_T)\big]\le-r\qquad\forall\theta\in\Theta .

A feasible pair is Pareto dominant if its objective is no larger than that of every feasible pair, for every $\theta$ .

A statistic $\widehat S_T$ takes values in a closed state space $\mathbb S$ and converges in probability to $S_\infty(\theta)$ , with $S_\infty:\Theta\to\mathbb S$ a local homeomorphism. A rate function $I(s,\theta)$ governs its LDP; it is regular if it is radially monotone, continuous on $\mathbb S\times\Theta$ and level-compact on $\mathbb S\times\operatorname{cl}\Theta$ . The distributionally robust predictor is

\tilde c^\star(x,s)=\max_{\theta\in\operatorname{cl}\Theta}\{c(x,\theta):I(s,\theta)\le r\},

(with $\sup_{\operatorname{cl}\Theta}c(x,\cdot)$ when the $I$ -ball is empty), and a distributionally robust prescriptor $\tilde x^\star$ is a quasi-continuous selection of $\arg\min_x\tilde c^\star(x,s)$ . Under an exponential family (4.1) with statistic $\widehat S_T$ and log-moment generating functions satisfying the Gärtner–Ellis conditions (Assumption 4.2), the rate is $I(s,\theta)=\sup_\lambda\langle\lambda,s\rangle-\Lambda(\lambda,\theta)$ .

Formalization targets

Goal: Theorem 4.3

With $\widehat c^\star_T(x)=\tilde c^\star(x,\widehat S_T)$ and $\widehat x^\star_T=\tilde x^\star(\widehat S_T)$ , for every $r>0$ :

(\widehat c^\star,\widehat x^\star)\ \text{is feasible in (2.4b), and}\quad \lim_{T}\mathbb E_\theta[\widehat c^\star_T(\widehat x^\star_T)]\le\lim_T\mathbb E_\theta[\widehat c_T(\widehat x_T)]

for every feasible $(\widehat c,\widehat x)\in\widehat{\mathcal X}$ and every $\theta\in\Theta$ . The goal fixes no constants; it asserts the shape of the optimum. One correction to the printed statement is built in: $\tilde x^\star$ must be Borel measurable on $\mathbb S$ , otherwise $\widehat x^\star$ need not be adapted.

Milestones

the restricted result Theorem 3.2, optimality of $(\tilde c^\star,\tilde x^\star)$ among compressed pairs, under an abstract LDP with a regular rate function; with Proposition 3.1 (continuity of $\tilde c^\star$ ) and the §2.3 passage from compressed to data-driven pairs;
the Gärtner–Ellis theorem (Theorem 4.1) in the paper's form, with Lemmas 4.1, 4.2 and Remark 4.1 on gradients of $\Lambda$ ;
the exponential-family identities (4.2) and (E.3), the change-of-measure bound (E.9), and the identity $I(s_0,\theta^\star_0)=\langle\eta,s_0\rangle-\Lambda(\eta,\theta^\star_0)$ ;
the probabilistic tools Lemmas G.1, G.2 and the choice of the tilted model $\theta^\star_0$ (p.46).

Significance

The result. Multi-objective problems usually have only Pareto optimal points; here a single solution is best for every model simultaneously. Theorem 4.3 says that among all data-driven predictor-prescriptor pairs (non-convex problems and dependent data included), none achieves a smaller asymptotic in-sample cost at the same guaranteed decay of out-of-sample disappointment than the DRO pair built from the sufficient statistic and its rate function. This turns DRO from one heuristic among many into the optimal answer to a precisely stated question, and it separates estimation (compute $\widehat S_T$ ) from optimization (solve the DRO problem) without loss.

Formalizing it. The paper's proofs are complete in print but rely on cited results (Gärtner–Ellis, Berge's maximum theorem, quasi-continuous selections) and on several steps marked "readily verifies" or "details are omitted". No machine-checked version exists. The finite-state i.i.d. special case of Van Parys et al. has formal statements on this platform (DROOptimal.*); this mission covers the general statement. A formal proof would check the measurability conditions the paper leaves implicit; the Borel correction to Theorem 4.3 and §2.3 came out of exactly that check.

Difficulty

The obvious approach to optimality is a Rao–Blackwell argument: condition an arbitrary predictor on the sufficient statistic and use convexity. It fails because the out-of-sample disappointment is not convex in $\widehat c_T$ (p.26). A competitor is an arbitrary adapted process, need not factor through $\widehat S_T$ , and its prescriptor need not converge. Comparing it with $\widehat c^\star$ therefore needs quantitative information on how probabilities of $\mathcal F_T$ -events change from one model to another, at exponential scale. That in turn needs an LDP for the statistic that holds without the lower semicontinuity of $\Lambda$ that the textbook Gärtner–Ellis theorem assumes, and an exact identification of the rate (4.4) at the relevant models. The constraint is asymptotic and logarithmic, so events of probability zero (rate $-\infty$ ) and non-measurable events built from quasi-continuous selections must be handled with care.

Formalization scope

Points are in EuclideanSpace ℝ (Fin d). Time runs over $T\ge1$ ; conditions at $T=0$ are not imposed. Logarithms of probabilities are ENNReal.log into EReal, so $\log 0=-\infty$ ; probabilities of possibly non-measurable events are outer measures. $\Theta$ is intrinsicInterior ℝ C for a convex C. The model-based predictor is assumed bounded and uniformly continuous on $X\times\operatorname{cl}\Theta$ , and $X$ is nonempty. $\widehat S_T(\omega)\in\mathbb S$ for every $\omega$ . Interiors and closures in the LDP are relative to $\mathbb S$ . The exponential-family density (4.1) is stated setwise on $\mathcal F_T$ . "The rate function (4.4) is regular" means a regular $I$ on $\mathbb S\times\operatorname{cl}\Theta$ agreeing with (4.4) on $\mathbb S\times\Theta$ , and the goal holds for every such $I$ . The objectives are stated as "both limits exist and compare", never through limUnder.

The goal cannot be satisfied vacuously: it asserts feasibility of $(\widehat c^\star,\widehat x^\star)$ (membership in $\widehat{\mathcal X}$ and the rate constraint), and $\widehat{\mathcal X}$ ranges over all data-driven pairs, not only those that factor through $\widehat S$ .

A complete development needs the following, all reusable beyond this mission:

convergence in measure and uniform integrability (Lemma G.1);
restrictions of measures to sub- $\sigma$ -algebras and the Radon–Nikodym chain rule;
Legendre transforms of essentially smooth convex functions;
a Gärtner–Ellis theorem in $\mathbb R^d$ ;
Berge's maximum theorem for compact-valued correspondences;
density of continuity points of quasi-continuous maps.

Contributions to any milestone are welcome, and Gärtner–Ellis is the largest independent piece.

Selected references

T. Sutter, B. P. G. Van Parys, D. Kuhn, A Pareto dominance principle for data-driven optimization, arXiv:2010.06606v4 (2023); Operations Research (2024). https://arxiv.org/abs/2010.06606
B. P. G. Van Parys, P. Mohajerin Esfahani, D. Kuhn, From data to decisions: Distributionally robust optimization is optimal, Management Science 67(6), 2021. https://arxiv.org/abs/1704.04118
A. Dembo, O. Zeitouni, Large Deviations Techniques and Applications, 2nd ed., Springer, 1998, Theorem 2.3.6. https://doi.org/10.1007/978-1-4612-5320-4
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, Theorem 26.3. https://doi.org/10.1515/9781400873173

21 thms1 active userReviewed

Algorithmic Game Theory Machine Learning Operations Research+2·Captain: iris

Multi-Agent Online Learning in Time-Varying Games: Mirror Descent Converges Almost Surely to the Nash Equilibrium of a Strictly Monotone Limit GameResearch Paper

Motivation

Many systems in which several agents repeatedly make continuous decisions are modelled as games whose rules drift over time: bidders in repeated Kelly auctions whose valuations change with traffic, wireless users whose channel gains fluctuate, firms in Cournot markets with shifting demand. In such settings agents rarely know the game they are playing; they observe noisy estimates of their own payoff gradients and update their actions with a simple learning rule. The question is whether such myopic, decentralized learning still reaches a sensible outcome when the game itself keeps changing.

Duvocelle, Mertikopoulos, Staudigl and Vermeulen (arXiv:1809.03066v3, 2021; published in Mathematics of Operations Research, 2023) study mirror descent in this regime. Their first main result, Theorem 1, says that if the sequence of stage games converges to a strictly monotone limit game, sufficiently fast relative to the players' step sizes, then the realized actions converge almost surely to the unique Nash equilibrium of the limit game. The result extends earlier almost-sure convergence theorems for mirror descent in a fixed monotone game (Mertikopoulos and Zhou, Math. Program. 2019) to games that vary over time, to biased and noisy gradient feedback, and to step-size schedules that differ from player to player. The monotone-game setting goes back to Rosen's diagonal concavity condition (Econometrica 1965).

Setting

A finite set $\mathcal N$ of players. Player $i$ chooses an action $x_i$ in a nonempty compact convex set $\mathcal K_i$ of a finite-dimensional real normed space $\mathcal X_i$ ; $\mathcal K=\prod_i\mathcal K_i$ is the action space, and $\mathcal Y_i=\mathcal X_i^*$ carries the dual norm $\|\cdot\|_*$ . At stage $t=1,2,\dots$ the players face a stage game $\mathcal G_t$ with payoffs $u_{i,t}$ and individual payoff gradients $v_{i,t}(x)=\nabla_{x_i}u_{i,t}(x)\in\mathcal Y_i$ . Assumption 1 asks that the stage payoffs be $C^2$ and that $\|v_{i,t}\|_*\le G_i$ and $v_{i,t}$ be $L_i$ -Lipschitz on $\mathcal K$ .

A limit game $\mathcal G$ with $C^1$ payoffs $u_i$ and gradients $v_i$ is strictly monotone if $\langle v(x')-v(x),x'-x\rangle<0$ for $x\ne x'$ in $\mathcal K$ , where $\langle v(x),z\rangle=\sum_i\langle v_i(x),z_i\rangle$ . The stabilization gap is $R_{i,t}=\max_{x\in\mathcal K}\|v_{i,t}(x)-v_i(x)\|_*$ , and $\mathcal G_t$ converges to $\mathcal G$ when $R_{i,t}\to0$ . A Nash equilibrium is a profile $x^*\in\mathcal K$ from which no player can raise its payoff by a unilateral deviation.

Each player $i$ has a distance-generating function $h_i$ on $\mathcal K_i$ : continuous, $K_i$ -strongly convex, with a continuous selection $\nabla h_i$ of its subdifferential on the prox-domain $\mathcal K_{h_i}$ . It induces the Bregman divergence $D_i(p,x)=h_i(p)-h_i(x)-\langle\nabla h_i(x),p-x\rangle$ and the prox-mapping $\mathcal P_i(x;y)=\arg\min_{x'\in\mathcal K_i}\{\langle y,x-x'\rangle+D_i(x',x)\}$ . Mirror descent is the recursion

X_{i,t+1}=\mathcal P_i(X_{i,t};\gamma_{i,t}V_{i,t}),

where $\gamma_{i,t}>0$ is a non-increasing step size and $V_{i,t}=v_{i,t}(X_t)+Z_{i,t}$ is an oracle signal whose conditional bias, variance and second moment are bounded by deterministic $B_{i,t}$ , $\sigma_{i,t}$ , $M_{i,t}$ .

Formalization targets

Goal: Theorem 1

Assume (RC): $D_i(p,x_t)\to0$ whenever $x_t\to p$ in $\mathcal K_{h_i}$ ; (S1) $\sum_t\gamma_{i,t}=\infty$ ; (S2) $\sum_t|\gamma_{i,t}-\lambda_{ij}\gamma_{j,t}|<\infty$ for some $\lambda_{ij}>0$ ; and

\sum_t\gamma_{i,t}(R_{i,t}+B_{i,t})<\infty,\qquad\sum_t\gamma_{i,t}^2(M_{i,t}^2+\sigma_{i,t}^2)<\infty.\tag{S3}

Then the limit game has a unique Nash equilibrium $x^*$ and

\mathbb P\big(X_t\to x^*\big)=1.

Milestones

In proof order:

(SVI): a Nash equilibrium satisfies $\langle v(x^*),x-x^*\rangle\le0$ on $\mathcal K$ .
Existence and uniqueness: a strictly monotone game has exactly one Nash equilibrium.
Lemmas A.1–A.4: the subgradient comparison, the three-point identity, the one-step prox inequality $D(p,x^+)\le D(p,x)+\langle y,x-p\rangle+\frac1{2K}\|y\|_*^2$ , and the template inequality for weighted sums along a prox sequence.
Footnote 4: $D(p,x)\ge\frac K2\|x-p\|^2$ .
Lemma 1: under (S1)–(S2), $\lambda_{ij}=\lambda_i/\lambda_j$ with $\lambda_i=(\prod_j\lambda_{ij})^{1/N}$ .
Lemma 2: the energy $E(x)=\sum_iD_i(x^*_i,x_i)/\lambda_i$ satisfies the quasi-descent inequality (40).
Proposition 1: $E(X_t)$ converges almost surely to an integrable limit.
Proposition 2: $\liminf_t\|X_t-x^*\|=0$ almost surely.

Significance

The theorem shows that equilibrium convergence of decentralized gradient learning is robust to three departures from the textbook setting at once: the game drifts, the feedback is biased and noisy, and players use their own step sizes. The conditions are explicit: the drift enters only through $\sum_t\gamma_{i,t}R_{i,t}<\infty$ , the bias through $\sum_t\gamma_{i,t}B_{i,t}<\infty$ , and heterogeneity of step sizes through the compatibility condition (S2). The paper's later results (payoff-based learning in Theorem 3 and randomly evolving games in Theorem 4) build on it.

The result is proved in the paper. As far as the platform's catalogue shows, it has no machine-checked proof, nor does almost-sure convergence of stochastic mirror descent in games. A formalization would add a mirror-descent layer stated for an arbitrary norm with a subgradient selection, covering the entropic setup whose prox-domain is a relative interior, and a reusable stochastic Lyapunov argument for multi-agent learning. The printed proof has a gap a formal proof cannot copy: the argument for Proposition 2 treats a sum of noise terms as a martingale with respect to the natural filtration of the iterates, which that filtration does not support. The statements are unaffected.

Difficulty

The obvious argument fixes the Nash equilibrium $x^*$ , tracks $\sum_iD_i(x^*_i,X_{i,t})$ , and applies a supermartingale convergence theorem. It fails twice. First, players move on different clocks, so the plain sum of divergences does not decrease; the weights $\lambda_i$ of Lemma 1 are needed, and the mismatch between $\gamma_{i,t}/\lambda_i$ and the effective step produces the extra term in (40). Second, convergence of the energy does not by itself give convergence of the iterates: one must show that a subsequence approaches $x^*$ , using strict monotonicity, compactness, and (S1), and then transfer this back through (RC) and the strong convexity bound. Existence of the equilibrium of the limit game is part of the statement, and Mathlib provides no Brouwer fixed point theorem for it. The prox steps live on a prox-domain that may exclude the boundary, so differentiability arguments at interior points are not enough.

Formalization scope

Action spaces are finite-dimensional real normed spaces, not inner-product spaces; payoff gradients are elements of the dual E i →L[ℝ] ℝ, defined as the Fréchet derivative of $u_i$ restricted to the $i$ -th factor, and pairings are evaluations. Payoffs are given on explicit open neighbourhoods of $\mathcal K$ (one for the limit game, one per stage game). The profile norm in Assumption 1 is $\sqrt{\sum_j\|x_j\|^2}$ , written out. Each DGF $h_i$ is real-valued with only its values on $\mathcal K_i$ used; the subgradient selection is a parameter; the prox step is a relation (the minimizer of (13)). The filtration is any filtration to which the iterates are adapted, with the oracle statistics relative to it; the paper's natural filtration is a special case, and the initial point is any deterministic point of the prox-domains. Stage games form one deterministic sequence. Lean's time index starts at $0$ .

The goal states existence, uniqueness and almost-sure convergence; stating convergence to an arbitrary assumed equilibrium would be vacuous if none existed. The oracle hypotheses include measurability and square-integrability of the signals, without which Lean's conditional expectations would be $0$ . A verification instance (one player on $[-1,1]$ with the Euclidean DGF) shows that all hypotheses can hold together.

A complete development needs a supermartingale convergence theorem of Robbins–Siegmund type (an open item elsewhere on the platform), existence of solutions of monotone variational inequalities on compact convex sets, and convex-analysis facts about subdifferentials in finite dimensions. The Bregman lemmas of Appendix A and the existence and uniqueness result are reusable beyond this mission. Contributions of any milestone, of these general tools, or of proofs of the goal by other routes are welcome.

Selected references

B. Duvocelle, P. Mertikopoulos, M. Staudigl, D. Vermeulen, Multi-Agent Online Learning in Time-Varying Games, arXiv:1809.03066v3, 2021; Mathematics of Operations Research, 2023. https://arxiv.org/abs/1809.03066
J. B. Rosen, Existence and Uniqueness of Equilibrium Points for Concave N-Person Games, Econometrica 33(3), 1965. https://doi.org/10.2307/1911749
P. Mertikopoulos, Z. Zhou, Learning in games with continuous action sets and unknown payoff functions, Mathematical Programming 173, 2019. https://doi.org/10.1007/s10107-018-1254-8
A. Juditsky, A. Nemirovski, C. Tauvel, Solving variational inequalities with stochastic mirror-prox algorithm, Stochastic Systems 1(1), 2011. https://doi.org/10.1214/10-SSY011
H. Robbins, D. Siegmund, A convergence theorem for non negative almost supermartingales and some applications, in Optimizing Methods in Statistics, Academic Press, 1971. https://doi.org/10.1016/B978-0-12-604550-5.50015-8

17 thms1 active userReviewed

Operations Research Optimization Probability+1·Captain: iris

Learning-based Robust Optimization: Procedures and Statistical Guarantees: with n₂ ≥ log δ/log(1 − ϵ), the data-split order-statistic set covers 1 − ϵ of P with confidence 1 − δResearch Paper

Motivation

A chance-constrained program (CCP) asks for a decision $x$ minimizing a cost $f(x)$ subject to $P(g(x;\xi)\in A)\ge 1-\epsilon$ , where $\xi$ is a random parameter with law $P$ and $\epsilon$ is a tolerance level. Chance constraints model reliability requirements in operations, finance and engineering, but they are hard to solve: the feasible set is usually nonconvex, and $P$ is known only through data. A standard safe approximation replaces the chance constraint by a robust optimization (RO) constraint, $g(x;\xi)\in A$ for all $\xi$ in an uncertainty set $U$ . The question is how to build $U$ from data so that the robust solution is feasible for the chance constraint with a stated confidence, without parametric assumptions on $P$ and with a sample size that does not grow with the dimension.

Hong, Huang and Lam (arXiv:1704.04342, Management Science 2021) answer this with a two-phase, data-splitting procedure: one part of the data learns the shape of the set, the other calibrates its size through an order statistic. This mission formalizes the basic statistical guarantee of that procedure (Theorem 1) and the lemmas it rests on.

Setting

Let $P$ be a probability distribution of $\xi$ on a measurable space $E$ (the paper: $\mathbb R^m$ ), and let $0<\epsilon<1$ and $0<\delta<1$ .

A decision $x$ is CCP-feasible if $P(g(x;\xi)\in A)\ge 1-\epsilon$ , and RO-feasible for a set $U\subseteq E$ if $g(x;\xi)\in A$ for every $\xi\in U$ .
$U$ is a $(1-\epsilon)$ -content set if $P(\xi\in U)\ge 1-\epsilon$ .
The data are an i.i.d. sample from $P$ , split into $D_1=(\xi^1_1,\dots,\xi^1_{n_1})$ and $D_2=(\xi^2_1,\dots,\xi^2_{n_2})$ , so $D=(D_1,D_2)$ has law $P_D=P^{n_1}\otimes P^{n_2}$ . A data-driven set $U(D)$ satisfies requirement (3) if

P_D\big(P(\xi\in U(D))\ge 1-\epsilon\big)\ge 1-\delta .

A score map $t(D_1,\cdot):E\to\mathbb R$ is chosen using $D_1$ only (an ellipsoid or polytope gauge, or a minimum or maximum of such gauges). For reals $y_1,\dots,y_n$ , $y_{(r)}$ is the $r$ -th smallest value.
With $b_k=\binom{n_2}{k}(1-\epsilon)^k\epsilon^{n_2-k}$ , the calibration index (4) is

i^*=\min\Big\{r:\ \sum_{k=0}^{r-1}b_k\ge 1-\delta,\ 1\le r\le n_2\Big\},

and the learned uncertainty set is

U(D)=\{\xi:\ t(D_1,\xi)\le t(D_1,\xi^2_{(i^*)})\},

where $t(D_1,\xi^2_{(i^*)})$ is the $i^*$ -th smallest of the scores of $D_2$ .

Formalization targets

Goal: Theorem 1 (basic statistical guarantee)

If $n_2\ge \log\delta/\log(1-\epsilon)$ and, for every realization of $D_1$ , $t(\xi)$ with $\xi\sim P$ is a continuous random variable, then the event $\{P(\xi\in U(D))\ge1-\epsilon\}$ is measurable,

P_D\big(P(\xi\in U(D))\ge 1-\epsilon\big)\ge 1-\delta,

and on this event every RO-feasible decision is CCP-feasible, so with probability at least $1-\delta$ every feasible (in particular every optimal) solution of the robust program is feasible for the chance-constrained program. The statement holds for every $n_1\ge0$ , every such score map and every constraint $g$ , $A$ .

Milestones

Lemma 1: an RO-feasible decision for a $(1-\epsilon)$ -content set is CCP-feasible.
Lemma 2: if $U(D)$ satisfies (3), then with probability $\ge 1-\delta$ every RO-feasible decision is CCP-feasible.
The two displays in the proof of Lemma 3: for i.i.d. atomless $Y_1,\dots,Y_n$ and $q$ with $F(q)=1-\epsilon$ ,

P(Y_{(r)}\ge q)=\sum_{k=0}^{r-1}b_k,\qquad P(Y_{(r)}\le q)=\sum_{k=r}^{n}b_k .

Validity of (4): $i^*$ exists $\iff 1-(1-\epsilon)^{n_2}\ge1-\delta\iff n_2\ge\log\delta/\log(1-\epsilon)$ .
Lemma 3: $Y_{(i^*)}$ is a $1-\delta$ upper confidence bound for the $(1-\epsilon)$ -quantile, $Y_{(i_*)}$ a lower one, and when the corresponding sums fall below $1-\delta$ no order statistic is a valid bound.
(5): conditional on any realization of $D_1$ , $P_{D_2}(P(\xi\in U(D))\ge1-\epsilon\mid D_1)\ge1-\delta$ .
The display after (5): averaging over $D_1$ gives (3).

Significance

The guarantee is nonparametric and finite-sample: it holds for every distribution with continuous scores, and the Phase 2 sample size $\lceil\log\delta/\log(1-\epsilon)\rceil$ depends on neither the dimension of $\xi$ nor that of $x$ (59 points for $\epsilon=\delta=0.05$ ). The shape learning of Phase 1 can be arbitrary, including clustering or other heuristics, because the calibration step alone carries the statistical validity. This separation is what lets the paper combine tractable geometric sets with high-dimensional data, and it is the same mechanism as split conformal prediction.

The paper proves the theorem. No part of it is formalized: the platform has no order-statistic confidence bound, no binomial law for counts of i.i.d. events, and no split-sample calibration result. A formal development supplies all three, together with a precise statement of what "conditional on $D_1$ " and " $U$ satisfies (3)" mean measure-theoretically.

Difficulty

The argument is short on paper, and the work is in the measure theory it leaves implicit. First, the binomial law of the count $\#\{j: Y_j<q\}$ under a product measure must be derived from independence; Mathlib has product measures but not this count law. Second, the order statistic must be handled with ties, since the paper's strict ranking holds only almost surely. Third, the conditioning in (5) has to become a statement about sections of the product measure $P^{n_1}\otimes P^{n_2}$ , and the average over $D_1$ needs measurability of the event $\{P(\xi\in U(D))\ge1-\epsilon\}$ in $D$ , which in turn needs joint measurability of the score map and of the order statistic. A proof that fixes $D_1$ and simply cites Lemma 3 does not yet give (3): the measurability of the averaged event is a separate obligation.

Formalization scope

The data space $E$ is any measurable space; $D=(D_1,D_2)\in(\mathrm{Fin}\,n_1\to E)\times(\mathrm{Fin}\,n_2\to E)$ with law (Measure.pi fun _ => P).prod (Measure.pi fun _ => P). $n_1=0$ is allowed.
Order statistics are counted with multiplicity: $y_{(r)}$ is y (Tuple.sort y ⟨r - 1, _⟩) with 1-based rank $r$ and 0-based Fin positions. $i^*$ and $i_*$ are sInf/sSup over $\mathbb N$ , with junk value $0$ when the defining set is empty; in Theorem 1 the sample-size condition makes the set nonempty, and it is not replaced by an " $i^*$ exists" hypothesis.
"Continuous" is read as atomless (NullSingletonClass), for the law of $t(D_1,\xi)$ at every realization of $D_1$ ; atomlessness of $P$ follows and is not assumed. The score map is a jointly measurable function $t(D_1,\xi)$ , which never sees $D_2$ .
Conditioning on $D_1$ is the section of the product measure; the expectation over $D_1$ is a lower Lebesgue integral. Probabilities $1-\epsilon$ , $1-\delta$ enter via ENNReal.ofReal.
The RO consequence is stated for every feasible decision on the event of (3), which specializes to any optimal solution; the objective $f$ plays no role.
Lemma 3 is stated for every $q$ with $F(q)=1-\epsilon$ , which covers every quantile convention.

A trivializing encoding is excluded: the event of (3) is concluded measurable, so its probability is not an outer-measure artefact, and a proved sanity file checks that every hypothesis of the goal is met by $P$ uniform on $[0,1]$ with $t(D_1,\xi)=\xi$ .

Reusable beyond this mission: the binomial count law for i.i.d. samples, the order-statistic probabilities of Lemma 3, and the section/averaging step for split samples. Contributions of any of these as standalone lemmas are welcome.

Selected references

L. J. Hong, Z. Huang, H. Lam, Learning-based Robust Optimization: Procedures and Statistical Guarantees, arXiv:1704.04342v2, 2020; Management Science 67(6), 2021. https://arxiv.org/abs/1704.04342
A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
R. J. Serfling, Approximation Theorems of Mathematical Statistics, Wiley, 2009 (§2.6.1, order-statistic confidence bounds). https://doi.org/10.1002/9780470316481

10 thms1 active userReviewed

Mechanism Design Operations Research Revenue Management and Pricing·Captain: iris

Technical Note—On Revenue Management with Strategic Customers Choosing When and What to Buy: Every Dynamic Pricing Policy Earns at Most the Fluid Value $\bar J^1$ Research Paper

Why the bound matters

Network revenue management studies a seller of perishable capacity: flight legs, hotel nights, cloud resources. Products are bundles of resources, the inventory is fixed, and the season ends at a known time. Upper bounds on optimal revenue are the basic tool of the field, because an exact optimum is out of reach and every performance guarantee for a heuristic compares it with a bound (Talluri and van Ryzin, 2006). Classical fluid bounds assume myopic customers, who buy on arrival or leave.

Real customers can wait. A customer facing dynamic prices weighs today's price against what tomorrow's may be, and this makes the seller's problem a game. Chen and Trichakis give a revenue bound for a network seller facing customers who are strategic on both timing and product choice, with private valuations for every product and private rates of decay. The bound is the value of a deterministic problem of one line.

The model

A seller offers $n$ products over $[0,T]$ . Product $j$ uses $A_{ij}\in\{0,1\}$ units of resource $i$ , and the inventory $x_0$ is fixed. Customers arrive by a Poisson process of rate $\lambda$ . A customer's type is $\phi=(t_\phi,v_\phi,d_\phi)$ : the arrival time, valuations $v^j_\phi$ for each product upon arrival, and decay rates $d^j_\phi$ . The valuation for product $j$ has density $f_j$ and is independent of everything else in the type.

The seller commits to a policy $\pi$ , which posts prices depending on past sales only. A customer exits once, at a time $\tau_\phi\in[t_\phi,T]$ , buying at most one unit, with utility

U(\phi,y_\phi)=\sum_{j}v^j_\phi e^{-d^j_\phi(\tau_\phi-t_\phi)}a^j_\phi-p_\phi.

He sees prices only; the seller sees sales only. Customers follow a symmetric equilibrium, and $J^\pi$ is the expected revenue, with $J^\star=\sup_\pi J^\pi$ .

Formalization targets

Goal: Theorem 1

For any admissible policy $\pi$ and any equilibrium under it, under Assumption 1 (a non-decreasing virtual value $v-\bar F_j(v)/f_j(v)$ ),

J^\pi\le J^\star\le\bar J^1,

where, with $\chi=1$ ,

\bar J^\chi=\max\Big\{\lambda T\sum_{j}q^j\bar F_j(q^j):\ \sum_j\bar F_j(q^j)\le\chi,\ \ \lambda T\sum_jA_{ij}\bar F_j(q^j)\le x_0^i\ \forall i\Big\}.

Milestones

The proof passes through a chain of relaxations, $J^\star\le J^{\mathrm{md}}\le\hat J\le\tilde J^1\le\bar J^1$ , which the milestones follow:

Lemma 1(i) and (ii): properties of a best response.
Lemma 2: $J^\pi\le J^{\mathrm{md}}$ , a mechanism design relaxation.
Lemma 3: $J^{\mathrm{md}}\le\hat J$ , constraints decoupled by product.
Lemma 4: $\hat J\le\tilde J^1$ , a problem in virtual values.
Lemma 6: $\tilde J^\chi\le\bar J^\chi$ , the fluid problem.

What the result gives

The bound holds for arbitrary price paths and arbitrary policies, with multi-dimensional private information, a setting in which optimal mechanisms are not available in closed form. Its value has the form of a static pricing problem, which makes it usable for analysis: the paper uses it to compare static prices with the optimum.

The theorem was published in Operations Research (2020); the mission is based on the SSRN version of May 29, 2018. No machine-checked proof is known. The formal statement also records a repair of the proof. As printed, Lemma 1(ii) is false, the mechanism of a policy does not satisfy the printed problem (5), Lemma 4 needs a tail condition (it fails for $\bar F(v)=1/(1+v)$ ), and the last step of the proof of Lemma 6 has its inequality reversed. The theorem itself stands. Lemmas 1(ii), 2 and 4 are stated in corrected form; the statement of Lemma 6 is unchanged.

The central difficulty

Multi-dimensional private information. A type carries $2n$ private numbers, so the one-dimensional envelope argument of Myerson (1981) does not apply to the incentive constraints as they stand. Decoupling them product by product shrinks the feasible set rather than enlarging it, so the natural relaxation goes the wrong way. The paper's step is to decouple and simultaneously restrict the agents' reports to valuations, which together give a net relaxation.

A closed loop. Prices depend on sales, sales on rules, and rules on prices. Comparing the game with a mechanism needs a statement that one customer's presence does not move the price path he faces, and that the others he faces are a Poisson crowd of the same law.

Ties. Prices depend on sales strictly before $t$ , so a price drop can draw several buyers at one instant. The paper does not say what happens then, and read literally the seller oversells and the theorem fails.

Formalization scope

The Lean development fixes the following conventions.

The customers of a season are a Poisson crowd: a Poisson $(\lambda T)$ number of i.i.d. types with uniform arrival, which has the law of the Poisson process. $E_{-\phi}$ is an integral over a fresh crowd.
A purchase is an Option (Fin n); a price is in WithTop ℝ and has no sign constraint; the inventory is in $\mathbb N^m$ .
Rationing: attempts at one instant are served in the order of arrival while stock lasts, and a rationed customer leaves with nothing. Plays without excess demand are unchanged.
Equilibrium: a best response in expected utility, for every type, which the printed conditional best response implies. The theorem quantifies over all equilibria, since the paper proves neither existence nor uniqueness.
$\bar J^\chi$ is over $q\in[0,\infty]^n$ with $\infty\cdot0=0$ .
Assumption 1 is on the interior of the support, with $f_j>0$ a.e. there.

The formal statement is not vacuous. A proved instance of an equilibrium with a static policy accompanies the development, and the goal quantifies over all policies, not just static ones. Inventory is enforced by the rationing, not by a hypothesis on the equilibrium, and no moment assumption is made.

A complete development needs: Mecke's formula and Campbell's formula for the crowd, which are elementary here; the silent customer lemma for plays; uniqueness of a play by induction on sale events; an envelope theorem for a supremum of affine functions; and Myerson's payment identity with truncation. All but the first are specific to this model, and the Poisson crowd and its formulas are reusable. Contributions of any of these lemmas are welcome.

Selected references

Y. Chen and N. Trichakis, On Revenue Management with Strategic Customers Choosing When and What to Buy, SSRN 2959489, version of May 29, 2018. https://ssrn.com/abstract=2959489
Y. Chen and N. Trichakis, Technical Note—On Revenue Management with Strategic Customers Choosing When and What to Buy, Operations Research, 2020. https://doi.org/10.1287/opre.2020.2008
R. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
K. Talluri and G. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2006. https://doi.org/10.1007/b139000

15 thms1 active userReviewed

Linear algebra Operations Research Probability·Captain: iris

Processing Networks XVII: A Relative-Entropy Lower Bound for the Traffic Equations of a Transient Routing MatrixTextbook

Motivation

In a multiclass processing network, jobs of class $i$ arrive from outside at rate $\lambda_i$ and, after service, move to class $j$ with probability $P_{ij}$ or leave the network. The traffic equations $\alpha=\lambda+P'\alpha$ give the total arrival rate $\alpha_i$ into each class. Chapter 10 of Dai and Harrison's Processing Networks: Fluid Models and Stability proves that the fluid model of a network under proportionally fair bandwidth sharing is stable, using an entropy-like Lyapunov function of the form $\sum_i Z_i\log(\dot D_i/\alpha_i)$ . The decrease of that function rests on a family of inequalities collected in Section B.4 of the book's appendix. The authors note that, unlike the other appendix material, these "are not results that appear in standard reference works" (Dai & Harrison, draft 2020-4-2, p.268).

This mission formalizes Section B.4 together with the matrix fact it rests on (Appendix F). The book's Chapters 2–12 are already on the platform as the series Processing Networks I–XIV, whose proportional-fairness missions (IX, X) state the Lyapunov function but not these inequalities.

Setting

Fix an integer $I\ge1$ and the set of classes $\mathcal I=\{1,\dots,I\}$ . The data are

a vector $\lambda\in\mathbb R^I_+$ of external arrival rates;
a non-negative $I\times I$ routing matrix $P$ .

The spectral radius $\rho(Q)$ of a real $d\times d$ matrix $Q$ is the largest modulus of its complex eigenvalues; $Q$ is convergent if $Q^k\to0$ . Section B.4 assumes $\rho(P)<1$ , so $I-P'$ is invertible and the total arrival rates

\alpha:=(I-P')^{-1}\lambda

are the unique solution of $\alpha=\lambda+P'\alpha$ . The section further assumes $\alpha>0$ . The outside world is an extra class $0$ : $P_{i0}:=1-\sum_{j\in\mathcal I}P_{ij}$ is the outflow rate of class $i$ , $\mathcal I_+=\mathcal I\cup\{0\}$ , and the conventions $\alpha_0=d_0=1$ apply. The input classes are $\mathcal I_0=\{i:\lambda_i>0\}$ . Norms are $\ell^1$ : $|x|=\sum_i|x_i|$ .

In Lean, classes are Fin I, the class- $0$ terms are written out with outflow P i, $\alpha$ is traffic lam P, and the standing assumptions form the structure SectionB4Assumptions lam P.

Formalization targets

Goal: Lemma B.13

If, in addition, $P$ is substochastic ( $\sum_jP_{ij}\le1$ ), then for every $d\in\mathbb R^I$ with $d>0$ , writing $a:=\lambda+P'd$ ,

\sum_{i\in\mathcal I}(d_i-a_i)\log\frac{d_i}{\alpha_i}\ \ge\ \frac{1}{2\left(\sum_i d_i+\sum_i\lambda_i\right)}\Big(\sum_{i}\lambda_i\Big|1-\frac{d_i}{\alpha_i}\Big|+\sum_{i}\alpha_i\Big|\frac{d_i}{\alpha_i}-\sum_{j\in\mathcal I_+}P_{ij}\frac{d_j}{\alpha_j}\Big|\Big)^2 .

Milestones

Theorem F.1. For every real square $Q$ : $Q^k\to0$ $\iff$ $\rho(Q)<1$ $\iff$ $I-Q$ is invertible with $(I-Q)^{-1}=\sum_{k\ge0}Q^k$ .
Lemma B.9. Every class is reachable from an input class along a route of positive probabilities.
Lemma B.10. For arbitrary $d$ with $d_0=1$ :

\sum_i d_i+\sum_i\lambda_i=\sum_i\alpha_i\sum_{j\in\mathcal I_+}P_{ij}\frac{d_j}{\alpha_j}+\sum_i d_i\frac{\lambda_i}{\alpha_i}.

Lemma B.12 (linked to the existing platform statement SinkhornHall.lemma_1_1). For non-negative $p,q$ on a finite set with $q>0$ and $\sum p=\sum q$ : $D(p\|q)\ge\frac{1}{2\sum_ip_i}\big(\sum_i|p_i-q_i|\big)^2$ .
Lemma B.14. For $\alpha>0$ , $\delta>0$ , the minimum $\kappa(\alpha,\delta)$ of $\sum_i\alpha_i|d_i-\sum_{j\in\mathcal I_+}P_{ij}d_j|$ over $d\ge0$ with $|d-e|\ge\delta$ is attained and is strictly positive.
Lemma B.15. $x\log x$ is right continuous at $0$ , negative on $(0,1)$ , and $\inf_{x\ge0}x\log x=-1/e$ .
Lemma B.16. If $0\le a\le\hat a$ and $0<d\le\hat d$ , then $(a-d)\log d\le\hat a\log(1\vee\hat d)+1/e$ .

Lemma B.11 (Pinsker's inequality for probability vectors, $D(p\|q)\ge\frac12(\sum_i|p_i-q_i|)^2$ ) is the source of Lemma B.12. It is already posed on the platform in $L^1$ form (StabGen.Entropy.pinsker_L1, BousquetElisseeff.KLReg.pinsker_l1), so it is not restated here.

Significance

Lemma B.13 is the quantitative core of the stability proof for proportionally fair fluid models (Section 10.5). With $d=\dot D(t)$ one has $d-a=-\dot Z(t)$ , so its left side is minus the bound on the drift of the entropy Lyapunov function along a fluid path (Lemma 10.9). Its right side is non-negative and vanishes only at $d=\alpha$ . Lemmas B.14–B.16 supply the uniform bounds that turn that pointwise inequality into a strictly negative drift away from equilibrium. Theorem F.1 is the standard link between transience of a routing matrix, the Neumann expansion of $(I-P')^{-1}$ and the traffic equations. The platform already has the implication $Q^k\to0\Rightarrow(I-Q)^{-1}=\sum_kQ^k$ (SuttonTD.Convergence.theorem_A_1, proved), but not the three-way equivalence with the spectral radius.

All results here are proved in the book; none has a machine-checked proof yet. Formalizing them closes a gap in the published Processing Networks series, where the proportional-fairness missions use this section without stating it. It also exposes a hypothesis the printed text leaves implicit (next section).

Difficulty

The obvious argument for Lemma B.13 is the book's: rewrite the left side as a relative entropy $D(p\|q)$ of two vectors indexed by $\mathcal I\cup\mathcal I_0$ , check equal mass with Lemma B.10, and apply the unnormalized Pinsker inequality. The step that needs care is Jensen's inequality (B.30), $\sum_{j\in\mathcal I_+}P_{ij}\log(d_j/\alpha_j)\le\log\sum_{j\in\mathcal I_+}P_{ij}d_j/\alpha_j$ . It requires $(P_{ij})_{j\in\mathcal I_+}$ to be probability weights, hence $P_{i0}\ge0$ . The section's printed hypothesis (non-negative $P$ with $\rho(P)<1$ ) does not give this, and the lemma is then false. For example, $P=\begin{pmatrix}0&2\\0&0\end{pmatrix}$ , $\lambda=(1,0)$ , $\alpha=(1,2)$ , $d=(0.1,0.05)$ give a left side $\approx2.63$ and a right side $\approx6.61$ . The book's Guide (p.xv) defines spectral radius and transience for substochastic matrices only, so the goal assumes $P$ substochastic. Lemmas B.9, B.10 and B.14 hold as printed and are stated without it.

For Theorem F.1, the direction $\rho(Q)<1\Rightarrow Q^k\to0$ for an arbitrary real (not necessarily diagonalizable) matrix needs either the Jordan form or Gelfand's spectral radius formula, neither of which is available off the shelf for Matrix with its entrywise topology. Lemma B.14 needs a coercivity argument, since its feasible set is unbounded.

Formalization scope

Classes are Fin I with $I\ge1$ . The outside class $0$ is not an index: every sum over $\mathcal I_+$ is a sum over Fin I plus a term with outflow P i $=P_{i0}$ , using $d_0=\alpha_0=1$ .
$\rho$ is the published platform definition RobustToDynamics.specRadius: the largest modulus of a point of the spectrum of the matrix over $\mathbb C$ , i.e. of a complex eigenvalue. Matrix limits are entrywise. $\sum_{k\ge0}Q^k$ is the limit of partial sums.
$\alpha$ is defined as $(I-P')^{-1}\lambda$ , not assumed to solve the traffic equations. Its positivity is a standing assumption, as in (B.17).
$\log$ is the natural logarithm, with $0\log0=0$ . " $\inf=-1/e$ " is a greatest-lower-bound statement. " $\min$ … is strictly positive" asserts attainment and positivity.
Nothing can be satisfied vacuously: the standing assumptions hold for $I=1$ , $P=0$ , $\lambda=1$ , and the feasible set of Lemma B.14 is nonempty. The verification file proves these facts and the counterexample above.
Contributions welcome: proofs of the milestones; a general Gelfand-type lemma for real matrices, which is reusable well beyond this mission; and a proof of the finite-set Pinsker inequality, which would close Lemma B.12 and the finite-set case of Lemma B.11.

Selected references

J. G. Dai and J. M. Harrison, Processing Networks: Fluid Models and Stability, pre-publication draft 2020-4-2, Appendix B §B.4 and Appendix F, pp.268–273, 309; Cambridge University Press, 2020. https://spnbook.org
T. M. Cover and J. A. Thomas, Elements of Information Theory, 2nd ed., Wiley, 2006, Lemma 11.6.1 (Pinsker's inequality). https://doi.org/10.1002/047174882X
E. Isaacson and H. B. Keller, Analysis of Numerical Methods, Dover, 2012 (reprint), Theorems 4–5 (pp.14–15), cited for Theorem F.1. https://store.doverpublications.com/products/9780486680293
H. Hayashi, H. Hirai and K. Sakabe, Finding Hall blockers by matrix scaling, arXiv:2204.07425, Lemma 1.1 (the platform's unnormalized Pinsker statement). https://arxiv.org/abs/2204.07425

13 thms1 active userReviewed

Operations Research Optimal Transport Probability·Captain: iris

Convolution Bounds on Quantile Aggregation: The Worst-Case Quantile of a Sum with Given Marginals Is at Most the Convolution Bound, with Equality in Five CasesResearch Paper

Motivation

A bank or an insurer that holds $n$ risks $X_1,\dots,X_n$ usually has good statistical information about each risk separately and very little about how they depend on each other. Regulatory capital is computed from a quantile of the aggregate loss $X_1+\dots+X_n$ (the Value-at-Risk, VaR), so the question "how large can the quantile of the sum be, over all dependence structures consistent with the known marginals?" is a standard problem of quantitative risk management under dependence uncertainty.

The question has a long history:

1981–1982. Makarov (Theory Probab. Appl. 26(4)) and Rüschendorf (Adv. Appl. Probab. 14(3)) solved the case of two risks: the worst-case quantile of $X_1+X_2$ is an explicit inf-convolution of the two marginal quantile functions.
2006. Embrechts and Puccetti (Finance Stoch. 10) gave dual bounds for $n\ge3$ , which are in general not sharp.
2011–2016. Sharp values were obtained for homogeneous marginals with monotone densities, and by Jakobsons, Han and Wang (Scand. Actuar. J. 2016(8)) for heterogeneous marginals with decreasing densities, through a system of implicit ODEs. The theory of joint mixability (Wang and Wang, Math. Oper. Res. 41(3)) is the main tool behind these results.
2018. Embrechts, Liu and Wang (Oper. Res. 66(4)) proved an inf-convolution formula for the range value-at-risk (RVaR) in the context of risk sharing.

Blanchet, Lam, Liu and Wang (arXiv:2007.09320v5) turn the RVaR inequality of the risk-sharing problem around. They obtain an upper bound on the worst-case quantile of a sum for arbitrary marginals, the convolution bound. It is an $(n+1)$ -dimensional optimization over the marginals alone, and it is sharp in five cases that cover all previously known sharp results.

Setting

Let $\mathcal M$ be the set of Borel probability measures on $\mathbb R$ . For $\mu\in\mathcal M$ the left and right quantiles are

q^-_t(\mu)=\inf\{x:\mu(-\infty,x]\ge t\}\ (t\in(0,1]),\qquad q^+_t(\mu)=\inf\{x:\mu(-\infty,x]>t\}\ (t\in[0,1)),

with $q^+_0$ the essential infimum and $q^-_1$ the essential supremum (possibly $\mp\infty$ ). For $0\le\beta<\beta+\alpha\le1$ the RVaR

R_{\beta,\alpha}(\mu)=\frac1\alpha\int_\beta^{\beta+\alpha}q^+_{1-t}(\mu)\,\mathrm dt

is the average of the quantile over $[1-\beta-\alpha,1-\beta]$ ; it may be $\pm\infty$ .

For $\mu=(\mu_1,\dots,\mu_n)\in\mathcal M^n$ , a coupling is a probability measure $\pi$ on $\mathbb R^n$ with marginals $\mu_1,\dots,\mu_n$ ; the set of couplings is $\Gamma(\mu)$ . The aggregate set $\Lambda(\mu)$ consists of the laws of $x_1+\dots+x_n$ under $\pi\in\Gamma(\mu)$ . Finally

\Delta_n=\Bigl\{(\beta_0,\beta_1,\dots,\beta_n)\in(0,1)\times[0,1)^n:\ \sum_{i=0}^n\beta_i=1\Bigr\}.

The $t$ -tail distribution $\mu^{t+}$ has distribution function $\max\{(\mu(-\infty,x]-t)/(1-t),0\}$ . A measure admits a decreasing density if its support is bounded below and it has a non-increasing Lebesgue density on it, and symmetrically for increasing densities.

In Lean: qMinus, qPlus, R, Gam, Lam, Delta, convBound, tailDist, AdmitsDecDensity, AdmitsIncDensity, LowerME, UpperME in the namespace ConvBoundsQA.

Formalization targets

Goal: Theorem 2 (p.11)

For every $n\ge1$ , $\mu\in\mathcal M^n$ and $t\in[0,1)$ ,

\sup_{\nu\in\Lambda(\mu)}q^+_t(\nu)\ \le\ \inf_{\beta\in(1-t)\Delta_n}\ \sum_{i=1}^nR_{\beta_i,\beta_0}(\mu_i),

with equality when (i) $n\le2$ ; (ii) every $\mu_i$ admits a decreasing density beyond its $t$ -quantile; (iii) every $\mu_i$ admits an increasing density beyond its $t$ -quantile; (iv) $\sum_i\mu_i(q^+_t(\mu_i),q^-_1(\mu_i)]\le1-t$ ; (v) $\sum_i\mu_i[q^+_t(\mu_i),q^-_1(\mu_i))\le1-t$ .

Milestones

Display (7): quantiles as limits of RVaR as the window shrinks.
The monotonicity $R_{t,s}\le R_{t+s-\beta_0,\beta_0}$ for $\beta_0\in[s,t+s]$ (p.8).
Lemma EC.1: $R_{b,a}(\nu)\le\sum_iR_{\beta_i,\alpha_i}(\mu_i)$ for all $\nu\in\Lambda(\mu)$ , without finite means.
Display (13): RVaR and quantiles of the tail distribution.
Proposition 1: reduction of worst-case RVaR and quantile aggregation to level $0$ .
Existence of a lower mutually exclusive coupling (proof of Theorem 1(iii)).
Lemma EC.2: the LES of a lower mutually exclusive sum is a sum of RVaRs.
Theorem 1: the convolution bound for RVaR aggregation, sharp for $t=0$ , for decreasing densities, and under a mass condition.
Display (EC.6): reflection identity between worst-case right and best-case left quantiles.
Upper mutually exclusive couplings and the essential infimum of their sum (proof of Theorem 2(v)).

Significance

The inequality (14) holds for all marginals, including heavy-tailed ones without a mean, and its right side needs only the marginal quantile functions. The five equality cases show that it is the exact worst-case VaR in the settings that matter in practice: monotone densities in the tail, which include most parametric loss models, and the mutual-exclusivity regimes of credit portfolios with small default probabilities. Case (i) recovers the Makarov–Rüschendorf formula for two risks. The bound also yields the classical union bound $\mathbb P(\sum X_i\ge\sum z_i)\le\sum\mathbb P(X_i\ge z_i)$ as a special case (Remark 2, p.11).

All of these results are proved in the paper; none is known to be formalized. A formal development would add measure-theoretic infrastructure that Mathlib does not yet have: quantile functionals valued in the extended reals, RVaR and expected shortfall for arbitrary laws, couplings with prescribed marginals and their aggregate laws, and tail distributions.

Difficulty

The inequality (14) is the easy direction in spirit: it is the RVaR aggregation inequality (Lemma EC.1) followed by a limit $s\downarrow0$ . Even so, two steps are delicate. Lemma EC.1 must hold without finite means, which the paper obtains through weak continuity of RVaR and an approximation of couplings by couplings with integrable marginals. The limit uses (7) and the continuity of $R_{\beta_i,\beta_0}$ in $\beta_0$ .

The equality cases are where the work is. A first idea is that the comonotone coupling is the worst case. It is not: the worst-case quantile is attained by couplings that make the tails negatively dependent. Case (ii) relies on the construction of Jakobsons et al. (2016) of an extremal aggregate variable through implicit equations. Case (iii) reflects the problem to decreasing densities below a quantile and uses a cited minimization result. Cases (iv) and (v) need explicit mutually exclusive couplings. Case (i) is stated without a separate proof in the paper; it is the Makarov–Rüschendorf theorem.

Formalization scope

Measures. Marginals are probability measures on $\mathbb R$ with no further assumption; couplings are probability measures on Fin n → ℝ whose coordinate images are the marginals; $\Lambda(\mu)$ is the set of their images under the coordinate sum.
Extended reals. Quantiles, RVaR values, suprema and infima are in EReal. $R_{\beta,\alpha}$ is the difference of the integrals of the positive and negative parts of the quantile; when both are infinite (only for the mean $R_{0,1}$ ) the value is $-\infty$ and a predicate records that it is undefined.
The infimum in (14). It is taken over the $\beta$ whose terms do not contain both $+\infty$ and $-\infty$ . Plain EReal addition, where $-\infty+\infty=-\infty$ , would make (14) false for two Cauchy marginals, so that encoding is ruled out.
Parameters. $\beta=(\beta_0,(\beta_1,\dots,\beta_n))$ and $c\Delta_n$ is the pointwise scaling of the set. The goal uses the printed $(1-t)\Delta_n$ . Theorem 1 is stated with $\beta_0\in[s,t+s]$ , as in (11): with the printed set, its case (i) fails for $n=1$ , $\mu_1=\delta_0$ , $t=0$ , $s=1/2$ .
Densities. "Beyond the $t$ -quantile" is the condition on the tail distribution $\mu^{t+}$ ; "decreasing" means non-increasing.

Every definition (quantiles, RVaR, couplings, tail distributions, monotone densities, mutual exclusivity) is reusable for other work on risk aggregation and robust risk measures. Proofs of any milestone are welcome, as are proofs of the classical two-risk case and of the reflection identity (EC.6), which need no density assumption.

Selected references

J. Blanchet, H. Lam, Y. Liu, R. Wang, Convolution Bounds on Quantile Aggregation, arXiv:2007.09320v5, 2024. https://arxiv.org/abs/2007.09320
P. Embrechts, H. Liu, R. Wang, Quantile-based risk sharing, Operations Research 66(4), 2018. https://doi.org/10.1287/opre.2017.1716
E. Jakobsons, X. Han, R. Wang, General convex order on risk aggregation, Scandinavian Actuarial Journal 2016(8), 2016. https://doi.org/10.1080/03461238.2015.1012223
B. Wang, R. Wang, Joint mixability, Mathematics of Operations Research 41(3), 2016. https://doi.org/10.1287/moor.2015.0755
G. D. Makarov, Estimates for the distribution function of a sum of two random variables when the marginal distributions are fixed, Theory of Probability and Its Applications 26(4), 1981. https://doi.org/10.1137/1126086
L. Rüschendorf, Random variables with maximum sums, Advances in Applied Probability 14(3), 1982. https://doi.org/10.2307/1426677
P. Embrechts, G. Puccetti, Bounds for functions of dependent risks, Finance and Stochastics 10, 2006. https://doi.org/10.1007/s00780-006-0005-5

19 thms1 active userReviewed

Algorithmic Game Theory Economics Graph Theory+1·Captain: iris

Stability of Procurement Networks: A Network Is Rationalizable as Pairwise Stable with k-Anonymous Preferences If and Only If It Satisfies k-WARPSResearch Paper

Motivation

Procurement data record who buys from whom: public agencies and their contractors, manufacturers and their tier-1 and tier-2 suppliers. A basic question about such a network is whether it is stable, meaning that no firm would drop an existing relationship and no pair of unlinked firms would jointly gain from forming one. The standard notion is pairwise stability, introduced by Jackson and Wolinsky (1996) and widely used as the minimal equilibrium requirement in strategic network formation.

Preferences are not observed; only the network is. Revealed preference theory (Samuelson, Afriat, Varian; surveyed by Chambers and Echenique, 2016) asks which observations are consistent with some rational preferences. For networks the answer without restrictions is trivial: every network is pairwise stable for preferences that rank the observed network first (Remark 1 of the paper). Chiong and Qi restrict preferences by $k$ -anonymity, the assumption that agents occupying the same position in their local network have the same incentive to form links, and show that pairwise stability then has a simple, checkable empirical content, the Weak Axiom of Revealed Pairwise Stability ( $k$ -WARPS). The paper uses it to build an instability metric for procurement networks.

Setting

Let $V$ be a set of agents and $L : V \to T$ a map assigning each agent a type (for instance buyer or supplier). A network $h$ on $V$ is an undirected simple graph; $h + ij$ and $h - ij$ add and remove the link $ij$ . The observed network is $g$ . A network is adjacent to $g$ if it equals $g$ , $g + ij$ for a non-link $ij \notin g$ , or $g - ij$ for a link $ij \in g$ .

The $k$ -neighborhood $N^k_i(h)$ is the subgraph of $h$ induced on the agents at graph distance at most $k$ from $i$ . Write $(i, h) \simeq_k (i', h')$ if $h$ and $h'$ are both adjacent to $g$ and there is a type-preserving graph isomorphism $\sigma : N^k_i(h) \to N^k_{i'}(h')$ with $\sigma(i) = i'$ .

Each agent $a$ has a preference relation $\succeq_a$ , a complete and transitive relation on all networks on $V$ , with strict part $\succ_a$ . The network $g$ is pairwise stable for the profile $(\succeq_a)$ if $g \succeq_i g - ij$ and $g \succeq_j g - ij$ for every link $ij \in g$ , and $g \succ_i g + ij$ or $g \succ_j g + ij$ for every non-link $ij \notin g$ . The profile is $k$ -anonymous if, for all agents $i, i'$ , nodes $j, j'$ and networks $h, h'$ with $(i, h) \simeq_k (i', h')$ and $(i, h - ij) \simeq_k (i', h' - i'j')$ , either $h \succeq_i h - ij$ and $h' \succeq_{i'} h' - i'j'$ , or $h \prec_i h - ij$ and $h' \prec_{i'} h' - i'j'$ .

The observed network $g$ satisfies $k$ -WARPS if for all agents $i, j$ there is no non-link $i'j' \notin g$ with

(i, g) \simeq_k (i', g + i'j') \qquad\text{and}\qquad (j, g) \simeq_k (j', g + i'j').

Formalization targets

Goal: Theorem 1 (p.15)

g \text{ is rationalizable as pairwise stable with } k\text{-anonymous preferences} \iff g \text{ satisfies } k\text{-WARPS},

for every set of agents $V$ , every type map $L$ , every observed network $g$ and every $k \in \mathbb N$ , including $k = 0$ .

Milestones, in proof order

Definitions A.3 and A.4 are equivalent (p.OA-1), for $k \ge 1$ : $k$ -WARPS agrees with the alternate form that quantifies over links $ix, jy \in g$ and adds the conditions $(i, g - ix) \simeq_k (i', g)$ and $(j, g - jy) \simeq_k (j', g)$ .
Lemma 1 (p.12): rationalizable with $k$ -anonymous preferences $\Rightarrow$ $k$ -WARPS.
Theorem 3 (p.OA-4; Chambers–Echenique, Theorem 1.5): an order pair $\langle R, P\rangle$ ( $P \subseteq R$ ) has a weak-order extension $\langle \succeq, \succ\rangle$ iff it is acyclic.
Lemma 3 (p.OA-4): $g$ is rationalizable iff some profile of revealed preference relations has an acyclic extension under ExtendRevealed (Algorithm 1).
Lemma 4 (p.OA-5): under $k$ -WARPS some profile of revealed preference relations has an acyclic extension.
Lemma 2 (p.14): $k$ -WARPS $\Rightarrow$ rationalizable with $k$ -anonymous preferences.

The goal is Lemma 1 together with Lemma 2.

Significance

Theorem 1 is, in the authors' words, the first characterization of the testable restriction of pairwise stability. It turns an existential statement about unobserved preferences over exponentially many networks into a condition on the observed network alone: an algorithm that compares the $k$ -neighborhoods of agents before and after adding each missing link. The characterization underlies the paper's network instability metric, its weighted-network extension (Theorem 2, whose sufficiency proof calls Theorem 1) and its empirical application to public procurement data.

The result is proved on paper; no machine-checked proof of it, or of any revealed-preference characterization of network stability, is known. A formal proof would pin down the conventions on which the theorem depends (the meaning of $g - ij$ when $ij \notin g$ , the range of the witnesses in WARPS, the domain of the anonymity restriction), each of which changes whether the statement is true. A complete development also yields reusable statements: the order-pair extension theorem of Chambers and Echenique for arbitrary sets, and a vocabulary of rooted, typed $k$ -neighborhood isomorphisms on Mathlib's simple graphs.

Difficulty

Necessity is short. Sufficiency is where the work lies: one has to construct complete, transitive preferences on all networks that are $k$ -anonymous and make $g$ pairwise stable. Revealed preference does not settle the direction of preference at a missing link, since either endpoint, or both, may be the one refusing it, so there is a whole set of revealed profiles to choose from.

The natural route, closing a revealed profile under anonymity and extending it by Szpilrajn's theorem, does not close by itself. An arbitrary weak-order extension need not be $k$ -anonymous on comparisons the revealed profile leaves free, so the extension has to be chosen class by class of $\simeq_k$ -similar link events. The printed claim that every cycle of the closed profile has length two is not literally true (a chain may revisit $g$ ). What holds is that every cycle contains a cycle of length two, and showing this needs the structure of $\simeq_k$ : only networks adjacent to $g$ are related, and for $k \ge 1$ a rooted $k$ -neighborhood records the root's degree. The degenerate case $k = 0$ , where neighborhoods are single nodes, behaves differently and must be handled on its own.

Formalization scope

Agents form an arbitrary type V and types an arbitrary type T with L : V → T (T = Unit gives untyped networks); the paper's finite $N$ and finite type set are instances. Networks are SimpleGraph V. $h + ij$ is h ⊔ SimpleGraph.edge i j, and $h - ij$ is h.deleteEdges {s(i, j)}, edge deletion that leaves $h$ unchanged when $ij \notin h$ . The $k$ -ball uses the extended distance edist, so other components are excluded, and the $k$ -neighborhood is the induced subgraph. A preference profile is a relation pref a x y, read $x \succeq_a y$ , on all networks on $V$ . In $k$ -anonymity the networks $h, h'$ are universally quantified; the observed network appears only through the adjacency clause of $\simeq_k$ . In $k$ -WARPS the witnesses $i, j$ are arbitrary nodes, possibly equal and possibly unlinked. Restricting them to linked or distinct pairs makes the theorem false, as does restricting $k$ -anonymity to links $ij \in h$ at $k = 0$ .

The trivializations are excluded: $\simeq_k$ is nonempty (it is reflexive on $g$ ), $k$ -WARPS both holds and fails on small networks, and rationalizability is satisfiable. Each of these is checked by a proved sanity lemma in the development.

The revealed preference profiles $\mathcal R(g)$ are parametrized by a choice of revealing endpoints for each missing link. ExtendRevealed is the least profile closed under the two anonymity propagation rules. The equivalence of Definitions A.3 and A.4 is stated for $k \ge 1$ ; at $k = 0$ it fails on the two-node empty network.

Contributions welcome: proofs of any milestone, in particular the transfer of rooted isomorphisms between $N^k_i(g)$ and $N^k_i(g - ix)$ behind milestone 1, a proof of Theorem 3 from Mathlib's extend_partialOrder, and a direct proof of sufficiency through $\simeq_k$ -classes of link events.

Selected references

K. Chiong, A. Qi, Stability of Procurement Networks, authors' manuscript with online appendix, 2025; published in Manufacturing & Service Operations Management, 2025. https://doi.org/10.1287/msom.2024.0925
M. O. Jackson, A. Wolinsky, A Strategic Model of Social and Economic Networks, Journal of Economic Theory 71(1), 44–74, 1996. https://doi.org/10.1006/jeth.1996.0108
C. P. Chambers, F. Echenique, Revealed Preference Theory, Econometric Society Monographs, Cambridge University Press, 2016. https://doi.org/10.1017/CBO9781316104293
E. Szpilrajn, Sur l'extension de l'ordre partiel, Fundamenta Mathematicae 16, 386–389, 1930. https://doi.org/10.4064/fm-16-1-386-389

19 thms1 active userReviewed

Dynamic Programming Linear Optimization Operations Research+1·Captain: iris

Robust Online Selection with Uncertain Offer Acceptance: The Best Robust Ratio Equals the Value of an Explicit Linear Program, and Its Optimal Solutions Give Optimal PoliciesResearch Paper

Motivation

In the classical secretary problem a decision maker sees candidates in random order, learns only how each compares with those already seen, and must decide irrevocably whether to hire. Many real selection processes add one more source of uncertainty: the chosen candidate may refuse. Job offers are declined, customers ignore promotions, admitted students enrol elsewhere. Perez-Salazar, Singh and Toriello (arXiv:2112.00842) study the secretary problem with uncertain acceptance (SP-UA), in which each offer is accepted independently with a known probability $p$ , and ask for policies that perform well whatever the set of willing candidates turns out to be.

Earlier objectives for the same model were the probability of hiring the overall best candidate (Smith, 1975), which ignores the event that the best candidate refuses, and the probability of hiring the best willing candidate (Tamaki, 1991), which tends to be overly selective. The paper replaces both with a worst-case ratio over the top- $k$ scenarios, and shows that its optimal value and an optimal policy are computed by an explicit linear program.

Setting

There are $n\ge1$ candidates with distinct ranks $1,\dots,n$ (rank 1 is best). They arrive in a uniformly random order; $R_t$ is the rank of the $t$ -th arrival. On arrival the decision maker observes only the partial rank $r_t=1+\#\{u<t:R_u<R_t\}\in[t]$ . The state is $(t,r_t)$ . A policy assigns to each state $(t,s)$ , $t\in[n]$ , $s\in[t]$ , a probability $q(t,s)\in[0,1]$ of extending an offer; deterministic policies take values in $\{0,1\}$ . An offered candidate accepts with probability $p\in(0,1]$ , independently of everything else; acceptance ends the process, and a refusal moves on to the next candidate.

A policy collects a top $k$ candidate if some candidate of rank at most $k$ receives its offer and accepts. The robust ratio of a policy $\mathcal P$ is

\gamma_{\mathcal P}=\min_{k\in[n]}\frac{\mathbf P(\mathcal P\text{ collects a top }k\text{ candidate})}{\mathbf P(\text{at least one of the top }k\text{ candidates accepts})},

and the best robust ratio is $\gamma^*_n=\sup_{\mathcal P}\gamma_{\mathcal P}$ . The occupation probabilities of a policy are $x_{t,s}=\mathbf P(\text{reach }(t,s),\text{ offer})$ and $y_{t,s}=\mathbf P(\text{reach }(t,s),\text{ pass})$ .

Formalization targets

Goal: Theorem 2

\gamma^*_n=\max\Bigl\{\gamma:\ x\ge0,\ x_{t,s}\le\tfrac1t\bigl(1-p\textstyle\sum_{\tau<t}\sum_{\sigma\le\tau}x_{\tau,\sigma}\bigr),\ \gamma\le\tfrac{p}{1-(1-p)^k}\sum_{t,s}x_{t,s}\,\mathbf P(R_t\le k\mid r_t=s)\ \forall k\Bigr\},

with $\mathbf P(R_t\le k\mid r_t=s)=\sum_{i=s}^{k\wedge(n-t+s)}\binom{i-1}{s-1}\binom{n-i}{t-s}/\binom nt$ ; and for every optimal $(x^*,\gamma^*_n)$ , the policy offering at $(t,s)$ with probability $t\,x^*_{t,s}/(1-p\sum_{\tau<t}\sum_{\sigma\le\tau}x^*_{\tau,\sigma})$ is $\gamma^*_n$ -robust. The goal holds for every $n\ge1$ and every $p\in(0,1]$ , over all randomized Markov policies, and for every optimal solution.

Milestones

In proof order: the independence of partial ranks (§3, p.9); the closed form of $\mathbf P(R_t\le k\mid r_t=s)$ (Theorem 2); the policy polytope

\mathrm{POL}=\Bigl\{(x,y)\ge0:\ x_{1,1}+y_{1,1}=1,\ x_{t,s}+y_{t,s}=\tfrac1t\textstyle\sum_{\sigma=1}^{t-1}(y_{t-1,\sigma}+(1-p)x_{t-1,\sigma})\ \forall t\ge2\Bigr\}

and its two directions (Propositions 5 and 6, together Theorem 1); the linearity of collect probabilities in $x$ (Proposition 7); the denominator $1-(1-p)^k$ and the conditional form of the objective (§3, p.10); the three forms of $\gamma^*_n$ in (9); and the three steps of the proof of Theorem 7 (tightening into POL, projection of $(P')$ onto $(x,\gamma)$ , and the identity linking the two policy formulas).

Significance

The theorem turns a max–min problem over all policies into a linear program with $O(n^2)$ variables and constraints, so $\gamma^*_n$ and an optimal policy can be computed exactly for every finite $n$ and $p$ . The rest of the paper is built on it: the LP values converge to the value $\gamma^*_\infty$ of a continuous LP (Lemma 2), and the asymptotic bounds of Theorems 3 and 4, including the optimality of a threshold rule for $p\ge p^*\approx0.594$ , are proved for that limit. Theorem 1, the description of all policies of the SP-UA by an objective-free polytope, is reusable for any rank-based objective in this model.

The result is proved in the paper. No machine-checked proof of Theorem 2, of Theorem 1, or of the classical-secretary LP of Buchbinder et al. is known. Formalizing it means proving the combinatorial facts about random permutations that the paper calls "a simple calculation", the occupation-measure correspondence of Propositions 5–6 by induction on time, and the LP elimination that the paper leaves as "routine".

Difficulty

The obvious argument writes the robust ratio directly as a reward of a Markov decision process and solves the Bellman equations. This fails: the ratio is a minimum of $n$ objectives, not an expected sum of state rewards, so no single value function captures it. The paper's way around this needs two independent facts that are each nontrivial to make rigorous: that the occupation vectors of policies are exactly the points of POL, including the converse construction with its possibly vanishing denominators, and that $\mathbf P(\text{collect a top }k)$ is linear in $x$ , which needs the conditional law of the absolute rank given the entire history to depend only on the current partial rank. The index bookkeeping between arrival times, partial ranks and the LP's $(t,s)$ grid is the main practical hazard.

Formalization scope

The process is a finite probability space: $\mathrm{Perm}(\mathrm{Fin}\,n)\times\mathrm{Bool}^n\times\mathrm{Bool}^n$ , holding the arrival order, the policy's offer coins and the candidates' willingness coins, with an explicit product weight. No measure theory is needed. Arrival times are Fin n (0-based) while policies, POL and the LP use the paper's 1-based $(t,s)$ ; policies are functions ℕ → ℕ → ℝ read on the state space. $\gamma^*_n$ is IsLUB of the set of robust ratios, and each attained optimum is IsGreatest. The robust ratio is computed from event probabilities of the process, never from LP expressions, so the goal cannot be closed by unfolding definitions. Where a policy formula's denominator vanishes, the statements quantify over every completion and assert that one exists. POL and the constraints (19)/ $(P')$ are taken with the recursion for $t\ge2$ : the appendix prints " $\forall t\in[n]$ ", under which POL is empty.

A complete development needs counting lemmas for random permutations (the Lehmer-code bijection behind the independence of partial ranks), finite occupation-measure recursions, and elementary LP manipulations. The permutation lemmas and the occupation-measure correspondence are reusable for other rank-based online selection problems. Proofs of any milestone, and alternative routes to the goal such as LP duality with the dynamic-programming dual, are welcome.

Selected references

S. Perez-Salazar, M. Singh, A. Toriello, Robust Online Selection with Uncertain Offer Acceptance, arXiv:2112.00842v2, 2024; Mathematics of Operations Research, 2025. https://arxiv.org/abs/2112.00842
N. Buchbinder, K. Jain, M. Singh, Secretary problems via linear programming, Mathematics of Operations Research 39(1), 2014. https://doi.org/10.1287/moor.2013.0604
M. H. Smith, A secretary problem with uncertain employment, Journal of Applied Probability 12(3), 1975. https://doi.org/10.2307/3212730
M. Tamaki, A secretary problem with uncertain employment and best choice of available candidates, Operations Research 39(2), 1991. https://doi.org/10.1287/opre.39.2.274
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994 (Wiley Series reprint 2014). https://doi.org/10.1002/9780470316887

14 thms1 active userReviewed

Quantum Information·Captain: Gohan

Two-Categorical Bundles and Their Classifying SpacesResearch Paper

Motivation

For a 2-category 2C we associate a notion of a principal 2C-bundle. In case of the 2-category of 2-vector spaces in the sense of M.M. Kapranov and V.A. Voevodsky this gives the the 2-vector bundles of N.A. Baas, B.I. Dundas and J. Rognes. Our main result says that the geometric nerve of a good 2-category is a classifying space for the associated principal 2-bundles. In the process of proving this we develop a lot of powerful machinery which may be useful in further studies of 2-categorical topology. As a corollary we get a new proof of the classification of principal bundles. A calculation based on the main theorem shows that the principal 2-bundles associated to the 2-category of 2-vector spaces in the sense of J.C. Baez and A.S. Crans split, up to concordance, as two copies of ordinary vector bundles. When 2C is a cobordism type 2-category we get a new notion of cobordism-bundles which turns out to be classified by the Madsen-Weiss spaces.

This mission is the statement-level formalization of Two-Categorical Bundles and Their Classifying Spaces (arXiv:math/0612549v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Retracts of locally equiconnected spaces (Theorem 5.1, PDF p. 21). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

Theorem 1.1: Internal topological bicategory, geometric nerve, actual principal-bundle concordance quotient, and canonical realization comparison (hard)
Proposition 2.2: Principal transition data with quadruple-intersection coherence and a separately constructed geometric nerve (hard)
Proposition 2.5: Normalized colax functors on the normalized cover 2-category, with continuous total data (hard)
Proposition 2.7: Parenthesized free cover bicategory, strict continuous functors, and geometric nerve (hard)
Proposition 2.8: CW homotopy type; free cover bicategory; geometric realization; ordered Cech complex; ordered open cover; relative CW complex; simplicial deformation retract; simplicial space (source-ambiguity)
Example 3.1: The specified quotient topology on the unitary-line category and both induced realization maps (hard)
Example 3.2: Eilenberg-MacLane space; complex projective space; geometric nerve; line gerbe bicategory; local bundle gerbe; simplicial space; stable gerbe equivalence; topological bicategory (source-ambiguity)
Example 3.3: Kapranov–Voevodsky matrix bicategory and the BDR transition-data comparison (hard)
Example 3.4: MTSO(2) spectrum; bundle pullback; classifying comparison; concordance classes; constant simplicial space; continuous singular simplicial space; geometric realization; homotopy classes; ordered Cech complex; ordered open cover; realization unit; shifted infinite loop space; simplicial bundle; simplicial space; surface structure bicategory (hard)
Example 3.5: MTO(d) spectrum; bundle pullback; classifying comparison; concordance classes; constant simplicial space; continuous singular simplicial space; embedded cobordism category; geometric realization; homotopy classes; ordered Cech complex; ordered open cover; realization unit; shifted infinite loop space; simplicial bundle; simplicial space (hard)
Example 3.6: bundle pullback; classifying comparison; concordance classes; constant simplicial space; continuous singular simplicial space; geometric realization; graph cobordism category; homotopy classes; ordered Cech complex; ordered open cover; plus construction; realization unit; shifted infinite loop space; simplicial bundle; simplicial space; sphere spectrum; stable free-group automorphism group (hard)
Lemma 3.8: Topological bicategory of two-term chain complexes and the parallel-homotopy quotient (hard)
Lemma 3.10: Continuous normalized colax transformation and its induced realized nerve homotopy (hard)
Conclusion 3.11: BC adjoint-data fixed-complex bicategory; BC adjoint-data varying-complex bicategory; BC equivalence-data fixed-complex bicategory; BC equivalence-data varying-complex bicategory; BC strict fixed-complex bicategory; BC weak fixed-complex bicategory; Baez-Crans weak bicategory; K-theory construction; bundle pullback; complex vector bundle; concordance classes; geometric realization; ordered Cech complex; ordered open cover; parallel-homotopy quotient bicategory; simplicial bundle; simplicial space; topological category; topological category nerve (source-ambiguity)
Lemma 4.3: Finite-product cohorn subspace and canonical cohorn map with Serre lifting predicate (hard)
Theorem 4.4: Topological Kan predicate and the simultaneous singular diagonal functor (hard)
Remark 4.5: Dimension-two discrete horn compatibility in the simultaneous singular diagonal and Serre fibrations of the three faces (hard)
Corollary 4.6: Serre fibration; cohorn space; constant simplicial space; discrete singular diagonal; discrete singular simplicial set; simplicial augmentation; simplicial space; topological Kan condition (source-ambiguity)
Theorem 5.3: Hurewicz fibration; closed cofibration; locally equiconnected space; topological pullback (hard)
Corollary 5.4: Internal topological category and its composable-arrow nerve with Hurewicz source-map predicate (hard)
Theorem 5.6: Internal topological bicategory with G1–G4 and its geometric nerve (hard)
Lemma 5.7: Geometric-nerve simplices and the separately constructed compatible flag space (hard)
Lemma 5.8: Strict internal topological bicategories, G1-prime/G2-prime, and both realized nerve maps (hard)
Lemma 5.9: Topological adjoint-equivalence space and continuous whiskering maps on disk families (hard)
Theorem 5.10: SF1–SF5 as properties of actual total source-target and adjoint-equivalence maps (hard)
Proposition 6.6: Admissible category of spaces, raw excisive presheaf, relative-cylinder concordance, and induced quotient maps (hard)
Proposition 6.7: bundle pullback; ordered Cech complex; ordered open cover; simplicial bundle; simplicial space; topological pushout (source-ambiguity)
Corollary 6.8: Actual pullback on relative bundle concordance for the topological pushout (hard)
Lemma 6.9: Relative cylinder collapsing each A-fiber separately and endpoint pullback on concordance classes (hard)
Corollary 6.10: Computed relative bundle pullback on maps and relative homotopies (hard)
Lemma 6.11: Raw bundle restriction, relative concordance relation, and its extension data (hard)
Corollary 6.12: The three computed concordance restriction maps and their set-theoretic fiber (hard)
Proposition 6.13: bundle pullback; bundle restriction; inverse limit of sets; ordered Cech complex; ordered open cover; relative CW complex; relative concordance classes; relative cylinder; relative skeleton; simplicial bundle; simplicial space (source-ambiguity)
Lemma 6.15: Concordance category with raw bundles as objects and relative concordance classes as arrows (hard)
Proposition 6.16: Computed boundary transport via gluing and the homotopy extension map j (hard)
Lemma 6.17: Finite and unrestricted relative concordance quotients and their natural inclusion (hard)
Proposition 6.18: Finite disk-boundary class maps and the unrestricted relative comparison on CW-type pairs (hard)
Lemma 6.21: Shrinking with index deletion and inclusions of face-image subspaces for the extension homotopy (hard)
Proposition 6.22: Full ordered Cech simplicial space, shrinking inclusions, and levelwise strong deformation retracts (hard)
Corollary 6.23: Actual concordance pushforward for a degreewise strong deformation retract inclusion (hard)
Proposition 6.24: Boundary concordance computed from the supplied topological homotopy and its transport map (hard)
Theorem 6.25: Degreewise homotopy equivalence and the induced relative concordance comparison (hard)
Proposition 6.26: Actual horn pushout and finite zigzag of indexed shrinking covers with compatible maps (hard)
Corollary 6.27: Horn attachment as the actual simplicial pushout and its induced concordance class map (hard)
Lemma 6.28: Presented relative J-cell complex and finite subpresentation over the entire original Z (hard)
Proposition 6.29: The paper-specific presented J-cell complexes and induced relative concordance map (hard)
Lemma 6.30: Geometric realization of simplicial topological spaces and the specified relative J-cell maps (hard)
Theorem 6.31: Topological Kan replacement and its three induced properties, with optional goodness (hard)
Lemma 7.1: Compact-open continuous singular simplicial space, discrete topological lift of Mathlib singular sets, realized comparison maps, and a separation convention for closed degeneracies (source-ambiguity)
Proposition 7.2: bundle pullback; bundle restriction; constant simplicial space; ordered Cech complex; ordered open cover; relative concordance classes; relative cylinder; relative homotopy classes; simplicial bundle; simplicial space; underlying map (source-ambiguity)
Proposition 7.3: Compact-open continuous singular simplicial space, canonical constant-to-singular inclusion, and the computed bundle/concordance comparison (hard)
Corollary 7.4: Continuous singular pushforward and relative concordance for weakly equivalent target spaces (hard)
Lemma 7.5: Two simultaneous diagonals with different topologies and their realized natural maps (hard)
Lemma 7.7: Actual good-cover Cech maps into T and D and their topological homotopy (hard)
Lemma 7.8: Realization adjunction, strict boundary square, and extension homotopy relative to the realized boundary (hard)
Lemma 7.9: Ordered cover refinement with an order-preserving carrier and relative CW realization pair (hard)
Proposition 7.10: The realization unit on T(Z)-bundles and its disk-boundary concordance map (hard)
Corollary 7.11: Correctly typed T(Z)-boundary bundle and realization-unit concordance pushforward (hard)
Theorem 7.12: Actual simplicial-bundle concordance quotient and canonical geometric-realization class map (hard)
Relative extension after Theorem 7.12: bundle pullback; bundle restriction; classifying comparison; concordance classes; constant simplicial space; continuous singular simplicial space; geometric realization; homotopy classes; ordered Cech complex; ordered open cover; realization unit; relative CW complex; relative concordance classes; relative cylinder; relative homotopy classes; simplicial bundle; simplicial space (source-ambiguity)

Selected references

Two-Categorical Bundles and Their Classifying Spaces, arXiv:math/0612549v2, https://arxiv.org/abs/math/0612549v2

5 thms1 active userReviewed

Quantum Information·Captain: Gohan

Reverse reconciliation protocols for quantum cryptography with continuous variablesResearch Paper

Motivation

We introduce new quantum key distribution protocols using quantum continuous variables, that are secure against individual attacks for any transmission of the optical line between Alice and Bob. In particular, it is not required that this transmission is larger than 50 %. Though squeezing or entanglement may be helpful, they are not required, and there is no need for quantum memories or entanglement purification. These protocols can thus be implemented using coherent states and homodyne detection, and they may be more efficient than usual protocols using quantum discrete variables.

This mission is the statement-level formalization of Reverse reconciliation protocols for quantum cryptography with continuous variables (arXiv:quant-ph/0204127v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Finite-modulation asymmetric variance criteria (III.A, (38)–(44): finite-modulation variance advantage criteria, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

Abstract; I.A; V: reverse reconciliation beyond 3 dB against individual attacks: Uniform operational individual-attack security and the information-to-extraction step (source-ambiguity)
II.B, (6)–(14): conjugate conditional-variance tradeoffs: Common-domain canonical quadrature observables, normalized quantum second moments, and attained real-linear regression minima (hard)
II.C, (15)–(25): Alice variance and tight preparation minimum: Same-average-density squeezed/EPR preparation ensembles and their actual homodyne regression minima (hard)
II.D, (26)–(27): Eve variance bound independent of preparation: Density-independent individual quantum attack and alternative-preparation measurement coupling (hard)
II.E, (28)–(37): explicit saturating lossy entangling cloner: Full three-mode lossy Gaussian entangling cloner and the two-outcome Eve homodyne instrument (hard)
II.E: tightness assertion for every gain: Physical individual Gaussian dilation and per-quadrature attaining measurement for every gain (hard)
III.B, (45)–(48): measured Gaussian information balance: Actual Gaussian homodyne joint measures and their Shannon information from KL divergence (hard)

Selected references

Reverse reconciliation protocols for quantum cryptography with continuous variables, arXiv:quant-ph/0204127v1, https://arxiv.org/abs/quant-ph/0204127v1

7 thms1 active userReviewed

Quantum Information·Captain: Gohan

Butterflies I: morphisms of 2-group stacksResearch Paper

Motivation

Weak morphisms of non-abelian complexes of length 2, or crossed modules, are morphisms of the associated 2-group stacks, or gr-stacks. We present a full description of the weak morphisms in terms of diagrams we call butterflies. We give a complete description of the resulting bicategory of crossed modules, which we show is fibered and biequivalent to the 2-stack of 2-group stacks. As a consequence we obtain a complete characterization of the non-abelian derived category of complexes of length 2. Deligne's analogous theorem in the case of Picard stacks and abelian sheaves becomes an immediate corollary. Commutativity laws on 2-group stacks are also analyzed in terms of butterflies, yielding new characterizations of braided, symmetric, and Picard 2-group stacks. Furthermore, the description of a weak morphism in terms of the corresponding butterfly diagram allows us to obtain a long exact sequence in non-abelian cohomology, removing a preexisting fibration condition on the coefficients short exact sequence.

This mission is the statement-level formalization of Butterflies I: morphisms of 2-group stacks (arXiv:0808.3627v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 4.1.4: the two upper images commute (Proposition 4.1.4: the two upper images commute, PDF p. 26). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

Theorem 2.4.1: the plus construction is a stack: The explicit plus groupoid of generalized-cover descent data, its arrows on common refinements, restriction functors, and canonical map from the input prestack (hard)
Proposition 3.4.1: stackification preserves the gr-structure: A groupoid prestack with Cartesian coherent tensor/inverse/unit operations and the actual plus stackification on these operations and its canonical additive map (hard)
Proposition 3.4.5: the cocycle product defines the gr-stack structure: The crossed-module nerve and cocycle groupoids on generalized covers, their common-refinement quotient, and tensor induced by simplicial multiplication (3.4.3.1) (hard)
Theorem 3.4.9: torsor realization: The groupoid stack of right (G1,G0)-torsors, its bitorsor contracted tensor, and the descent-cocycle functor to the actual associated stack (hard)
Theorem 4.3.1: butterflies classify weak morphisms: Both butterfly and additive weak-morphism groupoids, the equivariant-lift functor Phi, and Psi with center the actual stack fiber product H0 times_(F,G) G0 (hard)
Claim 4.3.2: the lift sheaf is a torsor: The sheaf of H1-equivariant maps Q→E over t on every slice, its restriction maps and right G1-action, and local nonemptiness of an arbitrary input torsor Q (hard)
Lemma 4.4.1: full faithfulness of Φ: The actual functor Phi on butterfly groupoids and additive transformations of associated gr-stacks; sectionwise ButterflyIso alone does not define this functor (hard)
Proposition 4.4.2: the comparison on torsors: Psi(F) built from the stack fiber product, the two actual functors on all (H1,H0)-torsors, and the comparison natural transformation on their arrows (hard)
Proposition 4.5.3: strict morphisms correspond to split butterflies: The weak-morphism groupoid, the strict-to-weak realization and Psi, so that strictifiability and the split condition refer to the butterfly of the given weak morphism (hard)
Proposition 4.6.1: butterflies form a stack: The fibered butterfly groupoid on all slice sites with actual pullback functors and coherent comparisons, and its descent comparison (hard)
Corollary 4.6.2: weak morphisms form a stack: The fibered groupoid of Cartesian additive weak morphisms on associated stacks and its slice restriction and descent functors (hard)
Theorem 5.1.4: the butterfly bicategory: The butterfly composition sheaf quotient (F times_H0 E)/image(iotaPrime,kappa), the induced functor on isomorphisms, and the canonical associator and unit constraints (hard)
Lemma 5.2.1: reversible butterflies are equivalences: The actual Phi functor from a butterfly to its additive stack morphism and its flipped-butterfly inverse comparison, including unit and counit transformations (hard)
Proposition 5.3.1: fibered bicategory and its global sections: The pseudofunctor of slice butterfly bicategories, its coherent pullback homomorphisms, bicategory of Cartesian global sections, and specified comparison (hard)
Proposition 5.3.2: the pre-bistack property: The fibered crossed-module bicategory and Hom-stack descent on generalized covers, with all restriction/composition comparisons (hard)
Theorem 5.3.4: gr-stacks satisfy 2-descent: The fibered two-category of gr-stacks and effective two-descent including objects, additive equivalences, modifications, tensor, inverses and all coherence (hard)
Theorem 5.3.6: the butterfly model is biequivalent to gr-stacks: The specified associated-gr-stack homomorphism (5.3.5.1) on every level, fiberwise equivalences of Hom groupoids, and coherent effective object two-descent (hard)
Proposition 5.3.7: presentation of every gr-stack: The sheaf atlas, free-group sheaf with its actual additive extension, homotopy kernel crossed module, and the associated-stack equivalence to the given gr-stack (hard)
Lemma 5.3.8: a sheaf atlas: An underlying groupoid stack and its sheaf atlas construction with a locally essentially surjective Cartesian map; an atlas cannot be an input assumption (hard)
Lemma 5.3.9: extension to the free-group sheaf: The actual sheaf atlas of the preceding lemma, sheafification of the free-group presheaf, and coherent word evaluation into the given gr-stack (hard)
Lemma 5.4.1: quasi-isomorphisms are equivalences: The actual induced pi0 and pi1 sheaf maps of an additive Cartesian gr-stack morphism, together with additive equivalence data (hard)
Proposition 6.1.1: the homotopy kernel: The homotopy-kernel stack of pairs (Y,F(Y)≅I), the crossed module [H1→ker j], and an additive equivalence intertwining the specified inclusion J (hard)
Lemma 6.2.5: exactness passes to homotopy sheaves: A gr-stack complex with its given additive null transformation, local fullness/essential-surjectivity of the induced map to ker F, and induced homotopy-sheaf maps (hard)
Proposition 6.2.6: the connecting homomorphism: The actual connecting homomorphism from g composed etaF, transported along K≃ker F, and sheaf exactness of its entire six-term sequence (hard)
Proposition 6.3.3: the decomposition diagram: The constructed intermediate stack C=[H1→E]~, its maps pi and J, and the actual two-commuting decomposition diagram including the identity vertical maps (hard)
Lemma 6.3.5: the torsor homotopy pullback: The two-stacks of gr-stack torsors and relative torsors with equivariant 1-/2-morphisms, actual contracted-extension functor Fstar, and the pointed two-pullback comparison (hard)
Theorem 6.3.10: the homotopy fiber and its homotopy sheaves: The actual fiber two-stack, its basepoint homotopy sheaves, pointed right-orbit H0 sheaf, consecutive pointed two-pullbacks and all induced exact-sequence arrows (hard)
Proposition 6.3.11: equivalence of the two fiber models: The functor from Tors(C,G0) to relative Tors(H,G) descending (X,Y)↦piG(s(X)) tensor F(Y) through the contracted product on objects and 1-/2-morphisms (hard)
Proposition 6.4.1: cohomology without a fibration premise: The actual global pointed cohomology sets of gr-stack torsors and the connecting maps constructed using the canonical fibrational butterfly fraction, without assuming a fibration (hard)
Proposition 7.1.8: three models of braidings: The associated gr-stack braiding correspondence and the multiplication butterfly with its prescribed factor splittings and coherent bracket recovery (hard)
Proposition 7.2.2: symmetry as an additive transformation: The Cartesian tensor functors with the additive structures induced by the given braiding, and the additive-transformation condition on that same braiding (hard)
Proposition 7.2.3: symmetry of the multiplication butterfly: The multiplication butterfly for the given braiding and its swap isomorphism fixing beta and exchanging the prescribed splittings, rather than a bare extension isomorphism (hard)
Proposition 7.4.4: braided butterflies and braided weak morphisms: The specified weak stack morphism Phi(E), its inherited braidings and tensorator, and the exact braided-functor compatibility comparison (hard)
Lemma 7.4.5: braiding compatibility of a monoidal functor: The two additive composite functors induced by tensor and F with their braiding-dependent tensorators, and monoidality of the given lambda transformation (hard)
Theorem 8.3.1: the abelian correspondence: The actual Picard weak-morphism and abelian-butterfly groupoids and the induced converse correspondence, retaining arrows and tensor compatibility (hard)
Proposition 8.3.2: abelian presentation of a Picard stack: A Picard stack, sheafification of the free-abelian atlas, its kernel two-term abelian complex, and the actual additive braided presentation equivalence (hard)
Proposition 8.4.1: Picard crossed-module presentation: A presentation of an arbitrary Picard stack by a Picard crossed module, including the associated-stack Picard equivalence; component sheaves must not be forced abelian (hard)
Corollary 8.4.2: Picard weak morphisms and butterflies: The Picard weak-morphism groupoid and groupoid of braided butterflies with its actual comparison functor (hard)
Proposition 8.4.3: the three global Picard models: The three global bicategories with butterfly 1-morphisms and their specified Picard comparison homomorphisms and biequivalence data (hard)
Proposition 8.5.1: the abelian butterfly stack: The fibered abelian-butterfly groupoid on slice sites and its canonical Baer tensor, inverse, zero object and symmetry, together with stack descent (hard)
Theorem 8.5.2: abelian complexes form a bistack: The fibered abelian-complex butterfly bicategory and effective object two-descent, including transport and descent of the Picard bracket (hard)
Proposition 8.5.4: the three fibered Picard models: Coherent fibered Picard comparison homomorphisms on restrictions and modifications, beyond separate equivalences in each fiber (hard)
Proposition 8.5.5: forgetting to extensions (source defect): The full printed conclusion is false under its stated hypotheses (source-ambiguity)
Proposition 8.5.6: fibered forgetful sequence (source defect): The full printed conclusion is false under its stated hypotheses (source-ambiguity)
Proposition 8.6.3: locally free butterflies split locally: OS-linear sheaf butterflies, fixed finite-rank local freeness on generalized covers, slice module-sheaf restrictions and the local linear splitting property for the actual center (hard)
Corollary 8.6.4: extension stack is a point (source defect): The full printed conclusion is false under its stated hypotheses (source-ambiguity)
Claim A.2.1: additive 2-morphisms glue: The fibered two-category of Cartesian additive functors and transformations of gr-stacks, and its actual two-arrow Hom presheaves (hard)
Claim A.2.2: additive 1-morphisms satisfy descent: The same fibered two-category with object descent in each Hom prestack, including gluing of the tensorator and its unit/associator compatibilities (hard)
§2.2: hypercover descent reduces to Čech descent: Evaluation of a prestack on presheaves by Cartesian sections, both hypercover and Cech descent groupoids, and their induced comparison along the coskeleton augmentation (hard)
§3.2.5: the strict gr-groupoid construction: The right-action internal groupoid and its strict monoidal structure with categorical inverses, together with strict-morphism and homotopy realization functors (hard)
§3.2.6: homotopy groups of a crossed module: The sheaf image/cokernel of the boundary and induced quotient action on its central kernel, the sheaf exact sequence, and identification with the actual groupoid homotopy sheaves (hard)
§3.4.10: the canonical presentation square: The actual associated stack and trivial-torsor presentation map piG, its null comparison, and equivalence to its pointed two-pullback (hard)
§4.2.3: pointed suspension and torsor Hom groupoids: The stack suspension, torsor two-stack, pointed Cartesian Hom groupoids and both induced comparison functors including pointed transformations (hard)
§4.7: stackification of strict morphisms: The strict-morphism prestack with strict homotopies, its explicit stackification and the fibered locally homomorphically split butterfly groupoid with compatible arrows (hard)
§5.2: composition with a strict morphism: The actual balanced butterfly composite and its canonical comparisons with pullback along q0 and extension pushforward along p1, retaining endpoint structural maps (hard)
§5.4: butterflies as canonical fractions: The constructed fraction crossed module [H1 times G1→E], both actual strict projections Q,P, their kernel/cokernel sheaf maps and comparison with the original butterfly (hard)
§5.4: equivalence after quotienting 2-morphisms: The isomorphism-class quotients of the actual butterfly and additive-functor Hom groupoids, induced category composition, and specified associated-stack comparison (hard)
Remark 6.2.7: surjectivity at the right endpoint: The final induced pi0 sheaf map of the actual left-exact gr-stack sequence, its local epimorphism property and local essential surjectivity of the same F (hard)
Remark 6.3.12: the extended fiber sequence: The actual extended sequence of group sheaves, gr-stacks and pointed two-stacks, with connecting arrows and consecutive pointed homotopy-pullback comparisons (hard)
§6.3 conclusion: the fiber of a surjective morphism: The canonical comparison Tors(ker F)→Tors(C,G0) for the actual locally essentially surjective F, including its constructed action on morphisms and coherent two-gerbe equivalence (hard)
§7.3: diagonal criterion for a Picard braiding: The symmetry psi of the multiplication butterfly determined by the given braiding, its diagonal pullback and its comparison to the local sXX transformation (hard)
§7.3.4: commuting factor splittings give an abelian complex: The prescribed multiplication-butterfly splittings, their induced tau and bracket, splitting isomorphism, and the sheaf exact sequence with actual kernel/cokernel (hard)
§7.4: the bicategory of braided crossed modules: The balanced composition of braided butterflies on sheaves, associators and units, and the actual forgetful homomorphism to the butterfly bicategory (hard)
§8.2: symmetric gr-groupoids of abelian butterflies: The actual Baer addition, additive inverse and zero butterfly with symmetric monoidal coherence on the abelian-butterfly groupoid (hard)
§8.4 conclusion: the derived category of two-term complexes: The three flattened Picard/abelian-complex categories, the full derived subcategory defined by cohomological vanishing outside −1,0 and their induced equivalences (hard)
§8.6 conclusion: the locally free pre-bistack: The ring-linear fibered butterfly bicategory and its full fixed-finite-rank locally free sub-bicategory, with coherent restriction inclusion as pre-bistacks (hard)

Selected references

Butterflies I: morphisms of 2-group stacks, arXiv:0808.3627v2, https://arxiv.org/abs/0808.3627v2

5 thms1 active userReviewed

Quantum Information·Captain: Gohan

Central extensions of groups of sectionsResearch Paper

Motivation

If q : P -> M is a principal K-bundle over the compact manifold M, then any invariant symmetric V-valued bilinear form on the Lie algebra k of K defines a Lie algebra extension of the gauge algebra by a space of bundle-valued 1-forms modulo exact forms. In the present paper we analyze the integrability of this extension to a Lie group extension for non-connected, possibly infinite-dimensional Lie groups K. If K has finitely many connected components we give a complete characterization of the integrable extensions. Our results on gauge groups are obtained by specialization of more general results on extensions of Lie groups of smooth sections of Lie group bundles. In this more general context we provide sufficient conditions for integrability in terms of data related only to the group K.

This mission is the statement-level formalization of Central extensions of groups of sections (arXiv:0711.3437v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The universal invariant symmetric bilinear form (Definition B.1, PDF p. 41). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

Theorem 0.1: Actual Gau(P), its form-valued cocycle and central Lie group extensions whose differentiated bracket is that cocycle, together with Cartan sphere-integral periods (hard)
Proposition 1.1: Actual equivariant section Lie algebra, Frechet coefficient forms modulo exact forms, covariant derivative and continuous cochain differential (hard)
Proposition 1.7: The Diff(N)-frame bundle P_m=Diff(N,Q_m), inverse-precomposition action on C-infinity(N,G), actual associated smooth section group and s(f)(p)=f composed p as a Lie group isomorphism with the prescribed mapping topologies. (hard)
Lemma 2.1: Actual smooth twisted loops f(t+1)=phi-inverse(f(t)), their smooth compact-open topology, and evaluation at zero; identify its image with {k:phi(k)k-inverse belongs to K0}, equivalently fixed components, and assert openness. (hard)
Lemma 2.2: The twisted-loop Lie group atlas, actual evaluation into K^[phi], its kernel and smooth neighborhood-wise right inverses (hard)
Proposition 2.3: Both actual twisted-loop groups with smooth compact-open/continuous compact-open topologies, the canonical continuous inclusion and its induced maps on homotopy groups and components; assert weak homotopy equivalence of that map. (hard)
Corollary 2.4: The based twisted-loop groups as actual evaluation kernels in the two mapping spaces, their canonical continuous inclusion and the induced isomorphisms on every homotopy group and components. (hard)
Proposition 2.5: The actual evaluation fibration, its homotopy connecting maps and canonical based-twisted-loop/ordinary-loop adjunction identification (hard)
Lemma 2.8: Frechet-valued flat smooth circle forms and exact forms, the Mackey integral and the induced map [f dt] to [integral_0^1 f(t)dt] in coker(phi_V-id) (hard)
Lemma 2.10: Actual sphere-integral periods of Cartan and loop cocycles, canonical pi_3(K)/pi_2(based loop) adjunction and the oriented cylinder integral (hard)
Theorem 2.12: The actual loop and Cartan sphere periods and coefficient projection q_V (hard)
Corollary 2.13: The actual universal-form twisted loop cocycle, intrinsic Lie algebra identification, naturally induced phi_V and sphere-integral period subgroup (hard)
Lemma 3.5: The actual smooth homotopy of based loops, its horizontal lifts and beta(t)=Hol(F0)-inverse Hol(Ft) (hard)
Proposition 3.6: Actual curvature R(theta)=dtheta+one-half[theta,theta], its whole image under L(rho), eta_D and its sphere-integral periods (hard)
Corollary 3.7: The actual holonomy-period setup with three alternative sufficient conditions: torsion pi_2(K), inner infinitesimal action, or flat connection (hard)
Lemma 3.8: The universal cover, right deck action and monodromy rho_V composed delta_1, genuine closed flat forms and group one-cohomology (hard)
Proposition 3.11: The actual Pi_omega and the HdR^1 subspace of Omega-bar^1, plus canonical loop-integration maps (hard)
Theorem 3.14: The monodromy-trivializing cover Mhat from ker(rho_V composed delta_1), its actual test loops and twisted period groups (hard)
Corollary 3.16: The actual adjoint bundle Ad(P) with section/gauge identification, monodromy cover and the connection-specific period groups; state the finite-D reduction using loops in Mhat. (hard)
Theorem 3.17: Uniformly constructed section cocycles and sphere periods for all compact bases, bundles and admissible connections with finite coefficient image (hard)
Corollary 3.18: The universal coefficient bundle for intrinsic finite-dimensional k=L(K), the actual omega_kappa,nabla and its sphere-integral period subgroup (hard)
Theorem 3.21: Actual full Aut(P), its pullback actions on theta/forms/gau(P), the concrete central Lie algebra and pair formula (14) (hard)
Corollary 3.22: The concrete extended gauge Lie algebra and smooth action of the actual Gau(P) on it whose derivative is the adjoint gau(P) action (hard)
Theorem 3.23: Actual gauge extensions and geometric Cartan sphere periods for possibly infinite-dimensional locally exponential K with finite pi_0 and vanishing pi_2 (hard)
Theorem 3.24: The actual connected finite-dimensional principal/gauge bundle, universal coefficient bundle and differentiated central extension (hard)
Theorem 3.25: The actual displayed action uses a non-basic one-form and an undefined action on θ; the source changes from χθ to a covariant logarithmic derivative without a consistent identification. A faithful single corrected formula is not fixed by the displayed theorem and proof. (source-ambiguity)
Theorem 3.26: A correct basic covariant logarithmic derivative compatible with the given Lie connection and its smooth integrated adjoint action, plus actual section cocycles and integration predicate (hard)
Theorem A.1: Actual associated quotient bundle, smooth sections, iterated-tangent compact-open topology, locally exponential section-group atlas and pointwise exponential, with its intrinsic identity-tangent Lie algebra isomorphism to Lie algebra sections (hard)
Proposition B.10: The actual universal Cartan sphere-integral subgroup Pi_S in intrinsic V(s); state discreteness, pointwise fixation by Aut(s), and Pi_S iso Z except for s iso sl_2(R), where it is zero (hard)
Theorem B.11: The geometric universal period groups, their identification through the actual Levi factor inclusions and embedded V(s), and the induced coinvariant projection (hard)
Remark/Example 1.2: The displayed primitive η is not assumed H-equivariant. Consequently η(f,g) need not descend from P to the associated V-bundle, so the global bundle-valued formula d(η(f,g)) is not defined from the stated data. (source-ambiguity)
Remark/Example 1.3: The connection-difference derivation beta, its actual coefficient-valued one-form eta_beta(f,g)=kappa(f,beta g), its continuous cocycle and bundle-map interpretations, and omega-prime minus omega=q_Omega composed eta_beta, including the stated Lie-algebroid extension interpretation. (hard)
Remark/Example 1.4: The actual adjoint bundle and gau(P) identification, equivariant vector fields aut(P), projection onto vector fields on M and its exact kernel (hard)
Remark/Example 1.8: The H-reduced associated mapping-group bundle for the given principal total space, and the actual Lie group isomorphism s(f)(p)(h)=f(p.h), with the circle-bundle specialization and one consistent total-space name. (hard)
Remark/Example 2.6: Both actual short exact homotopy sequences, with coinvariants on pi_1/pi_3 and fixed points on pi_0/pi_2 and the specified evaluation/boundary arrows (hard)
Remark/Example 2.11: The normalized SU2 form -one-quarter trace(ad x ad y), its left invariant Cartan form, the identity sphere and actual loop cocycle (hard)
Remark/Example 2.14: The torus double-loop group, the actual h(s) connection and both double-integral cocycles, universal torus period coordinates and per_omega(m,n,u)=n+m integral h (hard)
Remark/Example 2.15: The actual homotopy exact sequence and period restriction image, then its factorization modulo one-half im(per_C,phi) through fixed pi_2(K) (hard)
Remark/Example 2.16: For an arbitrary diffeomorphism ψ of S¹, precomposition does not preserve ∫κg(f(t),g(t))dt up to orientation: a nonconstant Jacobian changes it. Thus φV=±id asserted in the setup is not compatible with κ, and the period claims are not pinned for the stated automorphisms. (source-ambiguity)
Remark/Example 3.3: The connection-defined horizontal lift alpha-hat, its actual group pullback, I_alpha on flat form classes, and equalities (9) and (10) for the cocycles and actual induced pi_2/period maps. (hard)
Remark/Example 3.4: Holonomy beta from the actual based homotopy, its twisted extension, Phi_beta, the concrete cocycle difference and eta_delta(beta) (hard)
Remark/Example 3.9: Actual Z^1 and B^1 cochains with pointwise topology, the flat exact/closed form spaces and their comparison topology (hard)
Remark/Example 3.12: Finite-index subgroup restriction H¹(π1(M),Vtrivial)→H¹(π1(Mhat),Vtrivial) need not be surjective. For a closed genus-2 surface with a nontrivial sign local system from a double cover, V^D=0 but twisted H¹ has real dimension 2. The final displayed isomorphism (13) is false. (source-ambiguity)
Remark/Example 3.15: Canonical cover restriction Phi, group-cohomology inflation and the exact kernel/image description; retain the reduction under injectivity and finitely generated H1(Mhat), and the finite-dimensional orthogonal property-(T) sufficient condition. (hard)
Remark/Example 3.19: The quotient V^0(k)=V(k)/span(der(k).V(k)), its induced form and actual Aut(k) coefficient action, finite component image and comparison of geometric Cartan period groups (hard)
Remark/Example 3.20: The actual trivial torus bundle with d_nabla f=df+beta Df, both cocycle terms and per_eta_beta=beta per_eta_D through the constant-section inclusion (hard)
Remark/Example B.4: The centroid as a real algebra and its R/C field classification, the two real-simple regimes and simplicity of the central-case complexification (hard)
Remark/Example B.7: The actual semidirect-product isomorphisms for Aut(s) and pi_0(Aut(s)), with the permutation groups and complex-conjugation actions on the simple coefficient factors (hard)
Remark/Example B.9: The maximal compact subgroup of connected K, its center torus and connected simple compact normal factors, the finite-kernel multiplication cover, and the induced pi_3(K) iso pi_3(C) iso product pi_3(Cj) iso Z^m, with m indexing these compact factors. (hard)
Remark/Example B.12: The geometric Pi_K iso product_i Pi_Si^(mi) identification, pointwise fixation by factorwise automorphisms and the actual permutation action through product_i Sym(mi) (hard)
Remark/Example C.2: Sphere-integral period maps, actual pullback cocycles and induced homotopy maps, with naturality (17)/(18) (hard)
Unnumbered appendix result D.holonomy: The actual four successive local flows closed by the reversed commutator curve, horizontal lifts, parallel transport and beta(t)=Hol(alpha_t) (hard)

Selected references

Central extensions of groups of sections, arXiv:0711.3437v2, https://arxiv.org/abs/0711.3437v2

6 thms1 active userReviewed

Quantum Information·Captain: Gohan

Crossed Module Bundle Gerbes; Classification, String Group and Differential GeometryResearch Paper

Motivation

We discuss nonabelian bundle gerbes and their differential geometry using simplicial methods. Associated to any crossed module there is a simplicial group NC, the nerve of the 1-category defined by the crossed module and its geometric realization |NC|. Equivalence classes of principal bundles with structure group |NC| are shown to be one-to-one with stable equivalence classes of what we call crossed module gerbes bundle gerbes. We can also associate to a crossed module a 2-category C'. Then there are two equivalent ways how to view classifying spaces of NC-bundles and hence of |NC|-bundles and crossed module bundle gerbes. We can either apply the W-construction to NC or take the nerve of the 2-category C'. We discuss the string group and string structures from this point of view. Also a simplicial principal bundle can be equipped with a simplicial connection and a B-field. It is shown how in the case of a simplicial principal NC-bundle these simplicial objects give the bundle gerbe connection and the bundle gerbe B-field.

This mission is the statement-level formalization of Crossed Module Bundle Gerbes; Classification, String Group and Differential Geometry (arXiv:math/0510078v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Twisting gauges characterize principal simplicial bundle isomorphisms (Section 1.3, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

Theorem 5.6 (abstract seed): classification and universal bundle/gerbe: Smooth crossed-module gerbes, their stable-isomorphism quotient, and the actual universal realization pullback (hard)
§1.2: twisted Cartesian presentation and canonical section: General principal simplicial torsors with a supplied pseudo-cross section and their identification with the constructed twisted product (hard)
§1.4: contractibility of WG: The actual total WG simplicial object, its contraction, and universal pullbacks (hard)
Theorem 1.5: simplicial bundle classification: Pullback classification on simplicial homotopy classes into WbarG (hard)
Proposition 2.3: reconstruction from local connection forms: Intrinsic Lie-algebra-valued connection forms on smooth simplicial principal bundles, including Frechet models (hard)
§2.4: curvature compatibility, equivariance and horizontality: Actual exterior derivative and bracket wedge of a simplicial connection, and its horizontal base curvature (hard)
§3 opening: assertion of automatic crossed action: A specified degreewise crossed action on the composite-face kernels for a general homotopy-1-type simplicial Lie group (source-ambiguity)
§3: face/degeneracy laws of ν: Differentiated crossed kernel action and actual simplicial curvature/Bbar forms (hard)
§4.2: nerve as simplicial Lie group and realized topological group: Smooth crossed-module nerve with the opposite horizontal multiplication and topological realization (hard)
§4.2: simplicial homotopy groups of the crossed-module nerve: Algebraic crossed-module nerve and its simplicial homotopy groups after forgetting topology (hard)
Proposition 4.3: classifying space of trivialized extended bundles: Pairs of principal H-bundles with chosen extended D-trivialization, their concordances, and the classifying map (hard)
Remark 4.4: commuting principal actions and product: Smooth commuting principal actions and their contracted product from chosen extended trivializations (hard)
Remark 4.4: compatibility of bundle product with classifying maps: Contracted product of actual crossed-module bundles and its concordance classifying maps (hard)
§4.5: the two displayed short exact sequences and their claimed collapse: A single specified classifying-space model and strict versus homotopy exactness of the displayed sequences (source-ambiguity)
§4.5: quotient/semidirect model for the realized group: EH as a topological group, its canonical H inclusion, descended actions and both balanced quotient groups (hard)
§4.5: path/loop crossed-module String model: The selected based-path/centrally extended loop crossed module and extension level (source-ambiguity)
§4.5 continuation: Stolz–Teichner projective-unitary model: The specified vacuum representation factor A_rho, its projective-unitary topology, and its comparison with EH/ker alpha (source-ambiguity)
§4.6: homotopy groups of the one-object 2-category nerve: The one-object crossed-module two-category, its full Duskin nerve and algebraic simplicial homotopy groups (hard)
Remark 5.3: local gerbe cocycles and pullback: Geometric gerbes, good-cover extraction of smooth nonabelian cocycles and actual pullback (hard)
Remark 5.3: stable equivalence via local cochains: Stable geometric gerbe isomorphisms and the corrected smooth local cochain comparison (hard)
Proposition 5.5: W̄ nerve identification: The full Wbar construction and the explicit natural isomorphism with the crossed-module two-category nerve (hard)
Remark 5.7: universal nonabelian H-gerbe specialization: The Lie/Frechet automorphism crossed module and the actual universal gerbe/bundle specialization (hard)
§5.8: delooped exact sequence: Explicit connecting maps and a chosen meaning of exactness after delooping (source-ambiguity)
§5.8: equivalence of bundle and gerbe lifting problems: Image/quotient coefficient topology, smooth change of coefficients, and linked lifting groupoids (source-ambiguity)
§5.8: String sequence and String structures as gerbe lifts: A fixed Spin rank, String crossed-module level/path model and its lifting comparison (source-ambiguity)
Remark 5.9: canonical gerbe module: Actual D-H gerbe-module data, its contracted-product action and all coherence axioms (hard)
Remark 5.10: local simplicial-map description of gerbe classes: Fixed-cover smooth Cech nerve maps to Wbar NC, their homotopies, and geometric stable classes (hard)
Proposition 6.2: connection correspondence: Connections on the actual twisting pullback over the smooth Cech nerve and local gerbe connections (hard)
Proposition 6.4: B̄-field and gerbe B-field correspondence: Full simplicial Bbar fields and gerbe B fields over the same fixed connection and cocycle (hard)
§6 after Proposition 6.4: equality of ν-fields: The two actual nu constructions and their equality under the Bbar/B correspondence (hard)
Remark 6.5: abelian gluing possibility and unspecified nonabelian condition: A quantified abelian existence/compatibility statement and a specified nonabelian replacement (source-ambiguity)

Selected references

Crossed Module Bundle Gerbes; Classification, String Group and Differential Geometry, arXiv:math/0510078v2, https://arxiv.org/abs/math/0510078v2

3 thms1 active userReviewed

Quantum Information·Captain: Gohan

G-gerbes, principal 2-group bundles and characteristic classesResearch Paper

Motivation

Let $G$ be a Lie group and $G\to\Aut(G)$ be the canonical group homomorphism induced by the adjoint action of a group on itself. We give an explicit description of a 1-1 correspondence between Morita equivalence classes of, on the one hand, principal 2-group $[G\to\Aut(G)]$ -bundles over Lie groupoids and, on the other hand, $G$ -extensions of Lie groupoids (i.e.\ between principal $[G\to\Aut(G)]$ -bundles over differentiable stacks and $G$ -gerbes over differentiable stacks). This approach also allows us to identify $G$ -bound gerbes and $[Z(G)\to 1]$ -group bundles over differentiable stacks, where $Z(G)$ is the center of $G$ . We also introduce universal characteristic classes for 2-group bundles. For groupoid central $G$ -extensions, we introduce Dixmier--Douady classes that can be computed from connection-type data generalizing the ones for bundle gerbes. We prove that these classes coincide with universal characteristic classes. As a corollary, we obtain further that Dixmier--Douady classes are integral.

This mission is the statement-level formalization of G-gerbes, principal 2-group bundles and characteristic classes (arXiv:0801.1238v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Closed-loop inclusion is a right crossed module of underlying groupoids (Example 2.5, PDF p. 6). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

Lemma 2.9: Smooth hypercovers and the raw finite hypercover-zigzag relation (hard)
Lemma 2.17: The category of strict smooth double Lie groupoids and its hypercover class (hard)
Lemma 2.18: Finite generalized zigzags, their least congruence, and hypercover spans (hard)
Proposition 3.2: Smooth principal G-extension, normal groupoid quotient and induced quotient functor (hard)
Theorem 3.4 (seed: abstract correspondence): The two constructed assignments on Morita quotients of extensions and two-group bundles (hard)
Proposition 3.8: The fibre-pair double Lie groupoid and conjugation morphism into the automorphism two-group (hard)
Lemma 3.9: Induced source-kernel crossed modules and the actual quotient functor of a hypercover (hard)
Proposition 3.10: Twisted semidirect groupoid and smooth orbit quotient extension (hard)
Lemma 4.1: Geometric nerve total de Rham complex and its geometric strict-map pullback (hard)
Lemma 4.2: Cohomology pullback of finite generalized zigzags (hard)
Proposition 4.5: The characteristic map defined by equation (13) for an actual principal two-bundle (hard)
Corollary 4.9: Geometric generalized base pullback, fibre-product Whitney sum, and homogeneous external products (hard)
Proposition 4.13: Centrality section, reduced Z(G)-extension and canonical two-group inclusion (hard)
Proposition 4.15: Principal connection differential forms, canonical reductive projection and cocycle descent (hard)
Theorem 4.18: Canonical central cohomology identification, reduced bundle and DD cocycle class (hard)
Corollary 4.20: Integral singular-to-de-Rham comparison and the central dual lattice (hard)
Lemma 4.21: The actual degree-two nerves and face maps of the four comparison groupoids (hard)
Lemma 4.22: Normalized circle connection, source angular form and signed geometric face pullbacks (hard)
Theorem 4.23: Comparison hypercover pullback and the cohomology classes of the descended cocycle and angular form (hard)
Lemma 4.24: The actual reduced subbundle inclusion and the central projection of the pulled-back connection (hard)
Proposition 4.25: DD descent for the original and reduced extensions with their computed connections (hard)
Lemma 4.26: Torus-derived coordinate projections, invariant-form generators and the tensor characteristic class (hard)
Proposition 4.27: Universal class of the reduced bundle and DD of its computed reduced connection (hard)
Example 2.4 and Example 2.6: Smooth automorphism group, inverse-evaluation right action and its explicit strict Lie two-group (hard)
Example 2.14: Two smooth triangle two-transformations and the zigzag equivalence congruence (hard)
Example 2.15: Canonical forward and reverse generalized morphisms of the same hypercover zigzag (hard)
Example 2.23: Ordinary principal bundle difference map, gauge-pair hypercover and transported bundle Morita relation (hard)
Example 2.24: Compatible nonabelian cocycle multiplication and coefficient functor (source-ambiguity)
Example 2.25: Smooth Cech cover groupoid with nonnormalized twisted units, inverses and circle two-bundle span (hard)
Remark 2.26: Wolfson local simplicial principal bundles, their equivalences and the concrete nerve comparison (hard)
Example 2.27: Smooth inertia weak two-action and quotient presentation with canonical principal bundle (hard)
Example 4.7: Actual classifying-space comparison and normalized Chern-Weil homomorphism (hard)
Example 4.8: Canonical circle-inertia quotient bundle and its integral generator comparison (hard)
Remark 4.10: Total singular nerve cochains with coefficient ring and characteristic pullback (hard)
Example 4.28: Specified affine loop action, holonomy comparison and basic-form lattice normalization (source-ambiguity)

Selected references

G-gerbes, principal 2-group bundles and characteristic classes, arXiv:0801.1238v3, https://arxiv.org/abs/0801.1238v3

2 thms1 active userReviewed

Quantum Information·Captain: Gohan

Equivalences of Smooth and Continuous Principal Bundles with Infinite-Dimensional Structure GroupResearch Paper

Motivation

Let K be a a Lie group, modeled on a locally convex space, and M a finite-dimensional paracompact manifold with corners. We show that each continuous principal K-bundle over M is continuously equivalent to a smooth one and that two smooth principal K-bundles over M which are continuously equivalent are also smoothly equivalent. In the concluding section, we relate our results to neighboring topics.

This mission is the statement-level formalization of Equivalences of Smooth and Continuous Principal Bundles with Infinite-Dimensional Structure Group (arXiv:math/0604142v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Cocycle reconstruction and its canonical equivalence (Remark I.2: cocycle reconstruction and canonical bundle equivalence, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

Introduction, unnumbered theorem: smooth and continuous principal bundles: Compatible Hausdorff Bastiani atlases on arbitrary real locally convex spaces, local smooth extensions at corners, and smooth maps between such manifolds; Smooth principal-bundle atlases and equivariant diffeomorphisms, compatible with the concrete continuous PrincipalAtlas data (hard)
Remark I.9: induced smooth structure on a smooth principal bundle: Smooth principal-bundle atlases and equivariant diffeomorphisms, compatible with the concrete continuous PrincipalAtlas data and the atlas generated by the prescribed local trivializations (hard)
Remark I.10: local description and smoothness of bundle equivalences: Smooth quotient bundles, local gauge representatives, and their induced equivariant diffeomorphisms (hard)
Lemma I.11: smooth and continuous homotopies coincide: Compatible Hausdorff Bastiani atlases on arbitrary real locally convex spaces, local smooth extensions at corners, and smooth maps between such manifolds and relative smooth maps on [0,1] times the base (hard)
Lemma I.12: smooth structures on classifying spaces: The actual orthogonal homogeneous-space direct limits EK and BK and their universal principal-bundle property (hard)
Proposition I.13: smoothing finite-dimensional principal bundles: Smooth finite-dimensional principal bundles on the source corner manifolds and continuous/smooth equivalences (hard)
Proposition II.2: smoothing: Compatible Hausdorff Bastiani atlases on arbitrary real locally convex spaces, local smooth extensions at corners, and smooth maps between such manifolds for Lie-group targets, smoothness near a closed subset, and the compact-convergence mapping topology (hard)
Lemma II.4: fading-out: Centered convex charts in an arbitrary locally convex Lie group, smooth scalar cutoffs on CornerAtlas bases, and smoothness of chart-composed extensions (hard)
Lemma II.9: suitable identity neighborhoods: A fixed locally convex Lie-group smooth atlas together with its specified convex centered chart and simultaneous chart-convex neighborhood families (hard)
Theorem II.11: smoothing continuous principal bundles: Smooth principal-bundle atlases and equivariant diffeomorphisms, compatible with the concrete continuous PrincipalAtlas data; supplied local smooth structure on P near C and an extension by an open embedding (hard)
Theorem II.12: smoothing continuous bundle equivalences: Smooth principal-bundle atlases and equivariant diffeomorphisms, compatible with the concrete continuous PrincipalAtlas data and smoothness on an ambient-open neighborhood in the total space (hard)
Corollary II.13: equivalences of smooth and continuous bundles: Compatible Hausdorff Bastiani atlases on arbitrary real locally convex spaces, local smooth extensions at corners, and smooth maps between such manifolds; Smooth principal-bundle atlases and equivariant diffeomorphisms, compatible with the concrete continuous PrincipalAtlas data (hard)
Theorem III.2: isomorphism for abelian Čech cohomology: Smooth/continuous abelian Cech complexes of function sheaves, refinement-limit cohomology groups, and their canonical forgetful homomorphism (source-ambiguity)
Theorem III.5: isomorphism for nonabelian Čech cohomology: Normalized nonabelian smooth/continuous Cech H1 over all covers and the canonical comparison map (hard)
Corollary III.8: smoothing PU(H)-bundles: Norm-topologized PU(H), integral Cech H3, and constructed compatible smooth/continuous Dixmier–Douady maps (hard)
Remark III.9, explicit application: smooth sections and homotopies compute twisted K-theory: The actual associated Fredholm fiber bundle, its sections and fiberwise homotopy quotient sets (hard)

Selected references

Equivalences of Smooth and Continuous Principal Bundles with Infinite-Dimensional Structure Group, arXiv:math/0604142v3, https://arxiv.org/abs/math/0604142v3

5 thms1 active userReviewed

Quantum Information·Captain: Gohan

Higher gauge theory I: 2-BundlesResearch Paper

Motivation

I categorify the definition of fibre bundle, replacing smooth manifolds with differentiable categories, Lie groups with coherent Lie 2-groups, and bundles with a suitable notion of 2-bundle. To link this with previous work, I show that certain 2-categories of principal 2-bundles are equivalent to certain 2-categories of (nonabelian) gerbes. This relationship can be (and has been) extended to connections on 2-bundles and gerbes. The main theorem, from a perspective internal to this paper, is that the 2-category of 2-bundles over a given 2-space under a given 2-group is (up to equivalence) independent of the fibre and can be expressed in terms of cohomological data (called 2-transitions). From the perspective of linking to previous work on gerbes, the main theorem is that when the 2-space is the 2-space corresponding to a given space and the 2-group is the automorphism 2-group of a given group, then this 2-category is equivalent to the 2-category of gerbes over that space under that group (being described by the same cohomological data).

This mission is the statement-level formalization of Higher gauge theory I: 2-Bundles (arXiv:math/0410328v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Pullbacks of one cospan have isomorphic vertices (Proposition 1, PDF p. 6). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

Proposition 5: Cover-descended composition of internal G-transition morphisms (hard)
Proposition 6: Category operations on transitions over varying covers (hard)
Proposition 7: Composition of bundle maps equipped with their transition maps (hard)
Proposition 8: Category of structured G-bundles with data-valued transition morphisms (hard)
Proposition 9: Covered quotient construction of the associated internal G-bundle (hard)
Proposition 10: Descent of a fixed transition morphism to a unique structured bundle map (hard)
Theorem 1: The specific transition-forgetting equivalence of ordinary bundle categories (hard)
Proposition 12: Bicategory of smooth internal categories, cover-based anafunctors and transformations (hard)
Proposition 13: Comparison of Disc(B)→BG anafunctors with transition data (hard)
Proposition 14: Weak slice bicategory with specified invertible projection cells (hard)
Proposition 15: Regular action of a coherent internal 2-group in a cartesian bicategory (hard)
Proposition 16: Smooth crossed-module construction with source d(h)k and target k (hard)
Proposition 17: Coherent descent of the composite G-2-transition morphism (hard)
Proposition 18: Hom categories of 2-transition morphisms with both compatibility laws (hard)
Proposition 19: Bicategory of transitions with chosen weak descent composites (hard)
Proposition 20: Composition of full G-2-bundle morphisms with constructed zeta (hard)
Proposition 21: Bicategory of full G-2-bundles and paired 2-morphisms (hard)
Proposition 22: Covered equivalence 2-relation quotient giving an associated 2-bundle (hard)
Proposition 23: Descent of a fixed G-2-transition morphism to full G-2-bundle data (hard)
Proposition 24: Unique lifting of a fixed transition 2-cell with projection and zeta compatibility (hard)
Theorem 2: The full transition-forgetting biequivalence on objects, Hom categories and 2-cells (hard)
Proposition 25: Prescribed semistrictification of coherent transition data (hard)
Proposition 26: The specified forward/backward normalization morphisms and invertible 2-cells (hard)
Theorem 3: Refinement-aware crossed-module gerbe bicategory and all-level comparison (hard)
spaces-as-2-spaces: Discrete embedding with equivalences of actual anafunctor Hom categories (hard)
§2.2.5; compare §2.1.5, p. 34: An invariant concrete notion of 2-cover satisfying all five stipulated axioms (source-ambiguity)
g-2-spaces-bicategory: Bicategory of internal actions with exactly the source G-2-map data (hard)
unit-from-associativity: Normalization of multiplicative nonunital transition data (hard)
discrete-bundle-construction: The full discrete lift of group, action, transition and bundle structures (hard)
vector-bundle-construction: Smooth fibrewise-additive 2-bundle with the corrected transition identity lift (hard)

Selected references

Higher gauge theory I: 2-Bundles, arXiv:math/0410328v3, https://arxiv.org/abs/math/0410328v3

7 thms1 active userReviewed

Quantum Information·Captain: Gohan

Operator Algebras and Conformal Field Theory III. Fusion of positive energy representations of LSU(N) using bounded operatorsResearch Paper

Motivation

Fusion of positive energy representations is defined using Connes' tensor product for bimodules over a von Neumann algebra. Fusion is computed using the analytic theory of primary fields and explicit solutions of the Knizhnik-Zamolodchikov equation.

This mission is the statement-level formalization of Operator Algebras and Conformal Field Theory III. Fusion of positive energy representations of LSU(N) using bounded operators (arXiv:math/9806031v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Standard real part of a cyclic separating algebra (§12: Lemma 1, PDF p. 18). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

§2: Lemma: HighestWeightModule: Construct V_f as the cyclic SU(N)-submodule generated by the explicit tensor of exterior highest-weight vectors e_f in §2, using a nonnegative representative of f; unitary equivalence class independent of common shifts. Do not freely supply an arbitrary representation named V_f.; ExteriorPowerRepresentation: The actual SU(N) action on Λ^k C^N with inherited exterior inner product and [k] the k-row column; 1≤k≤N, and Λ^N is the trivial SU(N) representation.; AddBoxesDistinctRows: Relation on unnormalized diagrams: g_i−f_i∈{0,1}, Σ_i(g_i−f_i)=k and both tuples decreasing; common-shift normalization only after enumerating successors.; BoundedIntertwiner: Closed complex subspace of continuous linear maps T:H₁→L[ℂ]H₂ satisfying Tπ₁(g)=π₂(g)T for every element of the specified represented subgroup. Do not assume intertwiner existence or density in its definition. (hard)
§2: Theorem: HighestWeightModule: Construct V_f as the cyclic SU(N)-submodule generated by the explicit tensor of exterior highest-weight vectors e_f in §2, using a nonnegative representative of f; unitary equivalence class independent of common shifts. Do not freely supply an arbitrary representation named V_f.; SURepresentationRing: Grothendieck ring of actual finite-dimensional unitary SU(N) representations, additive generators [V_f], multiplication tensor product and star conjugate dual; canonical integer basis indexed by normalized signatures.; ExteriorPowerRepresentation: The actual SU(N) action on Λ^k C^N with inherited exterior inner product and [k] the k-row column; 1≤k≤N, and Λ^N is the trivial SU(N) representation.; SchurCharacter: A single polynomial/Laurent-polynomial alternant quotient X_f for every integral tuple f: det(z_j^{f_i+N−i}) divided polynomially by the Vandermonde det(z_j^{N−i}). For dominant f this is the Schur character; for non-dominant f it is the signed extension used in §34. Never evaluate a raw 0/0 determinant ratio at coincident eigenvalues. Common shifts disappear on ∏z_i=1.; SymmetricCharacterRing: Integral symmetric Laurent polynomials in z₁,…,z_N with ∏z_i=1; equivalently ordinary symmetric integral polynomials modulo determinant=1. Characters are evaluated by polynomial continuation at coincident eigenvalues. (hard)
§3: Theorem (Segal’s equivalence criterion [3]): CARAlgebra: Unital complex star algebra generated linearly by creation symbols a(f), with a(f)a(g)+a(g)a(f)=0 and a(f)a(g)+a(g)a(f)=(f,g)I in the source first-linear convention. Algebraic and represented norm completions must be distinguished.; PolarizedFockSpace: F_P=Λ(PH) Hilbert graded-tensor Λ(conjugate(P⊥H)); the two factors carry the Koszul signs of the CAR construction.; PolarizedCARRepresentation: Actual representation π_P(a(f))=a(Pf)+a((P⊥f)) on the polarized Fock space, with the graded-tensor identification and conjugate-dual map spelled out.; UnitaryEquivalence: the actual source construction, including its domains and topology (hard)
§3: Corollary of proof: Pinned source/provenance obstacle: §3: Corollary of proof (source-ambiguity)
§3: Corollary (Segal’s quantisation criterion [3], [28],[40]): RestrictedUnitaryGroup: Unitary u on H with [u,P] Hilbert–Schmidt; topology combines strong convergence of u and Hilbert–Schmidt convergence of its commutator. Specify topology without treating a non-summable real tsum as a norm.; BogoliubovAutomorphism: CAR star-algebra automorphism a(f)↦a(uf) for unitary u, as a map on the actual generated algebra.; ImplementableUnitary: Existence of U∈U(F_P) with Uπ_P(a(f))U*=π_P(a(uf)) for every f; uniqueness only up to unit phase is a theorem from irreducibility. (hard)
§3: Lemma: RestrictedUnitaryGroup: Unitary u on H with [u,P] Hilbert–Schmidt; topology combines strong convergence of u and Hilbert–Schmidt convergence of its commutator. Specify topology without treating a non-summable real tsum as a norm.; BasicProjectiveRepresentation: Canonical homomorphism U_P(H)→PU(F_P) assigning the phase class of any implementer; construction from actual CAR action, not arbitrary projective representation satisfying continuity as an axiom.; StrongOperatorTopology: the actual source construction, including its domains and topology (hard)
§4: Lemma: BasicProjectiveRepresentation: Canonical homomorphism U_P(H)→PU(F_P) assigning the phase class of any implementer; construction from actual CAR action, not arbitrary projective representation satisfying continuity as an axiom.; GaugeQuantisation: Canonical quantisation of scalar multiplication z∈U(1) on L²(S¹,V), giving U_z on F_P; U_{−1} is parity.; ParityOperator: On Fock degree n, multiplication by (−1)^n; agrees with canonical gauge U_{−1}. (hard)
§4: Corollary: BasicProjectiveRepresentation: Canonical homomorphism U_P(H)→PU(F_P) assigning the phase class of any implementer; construction from actual CAR action, not arbitrary projective representation satisfying continuity as an axiom.; ParityOperator: On Fock degree n, multiplication by (−1)^n; agrees with canonical gauge U_{−1}. (hard)
§5: Lemma: LoopCentralExtension: Pullback {(g,u)∈LG×U(F_V):π(g)=[u]} of U(F_V)→PU(F_V), with circle kernel, actual tautological representation and the lifted local subgroups. Level-ℓ central character is ζ^ℓ.; MobiusAction: SU_±(1,1) matrices and fractional-linear action on S¹, with weighted one-particle action V_γ f(z)=(α−conj(β)z)^{-1}f(γ^{-1}z) in the source barred-matrix convention; preserve linear/antilinear quantisation distinction.; CanonicalQuantisation: Exterior functor applied to a linear isometry or conjugate-linear isometry for H_P, fixing the vacuum; commuting with P yields unitary and exchanging P with P⊥ yields antiunitary on F_P. (hard)
§6: Proposition: PositiveEnergyCircleAction: Strong circle action with Hilbert direct-sum eigenspaces H(n), n≥0, each finite-dimensional; normalized irreducibles also have H(0)≠0. Do not build irreducibility/decomposition into this definition.; UnitaryGroupAction: the actual source construction, including its domains and topology; RepresentationIrreducibility: No nonzero proper closed invariant subspaces for Hilbert representations; for algebraic finite-energy actions use all invariant linear subspaces instead, without a closure requirement.; HilbertDirectSum: Square-summable Hilbert sum of represented spaces with diagonal action; allow path-indexed repeated equivalent summands and explicitly retain their multiplicities. (hard)
§6: Corollary: ProjectiveRepresentation: Strongly continuous homomorphism G→PU(H), PU(H)=U(H)/unit scalar phases on a possibly infinite-dimensional Hilbert space. Accepted Gap20.P16 and Bridge50.P01 are finite-dimensional matrix interfaces and are not this object.; PositiveEnergyCircleAction: Strong circle action with Hilbert direct-sum eigenspaces H(n), n≥0, each finite-dimensional; normalized irreducibles also have H(0)≠0. Do not build irreducibility/decomposition into this definition.; MultiplicityRepresentation: In the isotypic Hilbert decomposition ⊕H_i⊗K_i, K_i carries its own positive energy rotation action, while LG acts trivially there. Distinguish normalized irreducible sector rotations from multiplicity energy.; HilbertDirectSum: Square-summable Hilbert sum of represented spaces with diagonal action; allow path-indexed repeated equivalent summands and explicitly retain their multiplicities. (hard)
§6: Lemma (coset construction): ProjectiveRepresentation: Strongly continuous homomorphism G→PU(H), PU(H)=U(H)/unit scalar phases on a possibly infinite-dimensional Hilbert space. Accepted Gap20.P16 and Bridge50.P01 are finite-dimensional matrix interfaces and are not this object.; HilbertDirectSum: Square-summable Hilbert sum of represented spaces with diagonal action; allow path-indexed repeated equivalent summands and explicitly retain their multiplicities.; HilbertTensorProduct: Hilbert completion of algebraic tensor product with product inner product; Fock tensor powers and multiplicity decompositions use it rather than a finite-dimensional tensor model.; StrongOperatorTopology: the actual source construction, including its domains and topology; BoundedIntertwiner: Closed complex subspace of continuous linear maps T:H₁→L[ℂ]H₂ satisfying Tπ₁(g)=π₂(g)T for every element of the specified represented subgroup. Do not assume intertwiner existence or density in its definition. (hard)
§6: Corollary: MobiusAction: SU_±(1,1) matrices and fractional-linear action on S¹, with weighted one-particle action V_γ f(z)=(α−conj(β)z)^{-1}f(γ^{-1}z) in the source barred-matrix convention; preserve linear/antilinear quantisation distinction.; LevelRepresentation: Irreducible unitary summand of the actual F_V^{⊗ℓ} representation of the fixed loop central extension, ℓ≥1, rotations shifted to have nonzero lowest energy zero. General sums retain the stated positive energy finite-multiplicity condition.; ProjectiveRepresentation: Strongly continuous homomorphism G→PU(H), PU(H)=U(H)/unit scalar phases on a possibly infinite-dimensional Hilbert space. Accepted Gap20.P16 and Bridge50.P01 are finite-dimensional matrix interfaces and are not this object. (hard)
§7: Theorem: FermionModes: v(n)=π_P(a(e^{-inθ}v)), with all integer n and the actual Hardy polarization; use the creation/annihilation relations at n=0 from the construction rather than the contradictory vacuum sentence on p.13.; CurrentModes: Locally finite normal-ordered E_ij(n)=Σ_{m>0}e_i(n−m)e_j(−m)*−Σ_{m≥0}e_j(m)*e_i(m+n), then X(n)=Σa_ij E_ij(n), on the exact finite-energy domain. Do not use a nonconvergent operator tsum or assume current commutators as fields.; EnergyOperator: Closed self-adjoint generator D of normalized rotations, with domain square-summability of energy-weighted spectral components; acts as n on H(n).; FiniteEnergyDomain: Algebraic direct sum of H(n), equivalently finite sums of rotation eigenvectors; distinct from the whole smooth-vector domain and from a single energy eigenspace.; LieAlgebraForm: Real positive inner product on su(N), (X,Y)=−Tr(XY); complex-bilinear extension on the complexified algebra when matrix units are used. (hard)
§8: Exponential lemma: SmoothLoopGroup: Smooth periodic matrix-valued maps g:S¹→SU(N), with pointwise product. This is the source C∞ loop group, not all continuous or measurable loops.; AlgebraicLoopLieAlgebra: Trigonometric-polynomial loops into su(N), complexification with integer modes X_n=e^{-inθ}X, plus rotation derivation d=−i∂θ. The real algebra and its complexification must not be conflated.; LoopExponential: Pointwise matrix exponential of a smooth su(N)-valued loop, with Lie-polynomial restriction where stated; unbounded current exponential uses its full Stone generator instead.; SmoothLoopTopology: Topology of uniform convergence of every angular derivative on the compact circle for matrix entries; include the rotation semidirect product action. (hard)
§8: Exponentiation Theorem: CurrentModes: Locally finite normal-ordered E_ij(n)=Σ_{m>0}e_i(n−m)e_j(−m)*−Σ_{m≥0}e_j(m)*e_i(m+n), then X(n)=Σa_ij E_ij(n), on the exact finite-energy domain. Do not use a nonconvergent operator tsum or assume current commutators as fields.; SobolevEnergyNorm: ‖ξ‖_s=‖(I+D)^sξ‖ for real s on finite-energy vectors, defined spectrally; bounds quantify s,x before the constant and before ξ.; OperatorSmoothVector: Intersection of domains of all powers of the closed skew-adjoint generator; source C∞ vector is for that actual flow, not merely a smooth abstract function supplied independently.; LoopExponential: Pointwise matrix exponential of a smooth su(N)-valued loop, with Lie-polynomial restriction where stated; unbounded current exponential uses its full Stone generator instead.; BasicProjectiveRepresentation: Canonical homomorphism U_P(H)→PU(F_P) assigning the phase class of any implementer; construction from actual CAR action, not arbitrary projective representation satisfying continuity as an axiom. (hard)
§8: Corollary: LevelRepresentation: Irreducible unitary summand of the actual F_V^{⊗ℓ} representation of the fixed loop central extension, ℓ≥1, rotations shifted to have nonzero lowest energy zero. General sums retain the stated positive energy finite-multiplicity condition.; CurrentModes: Locally finite normal-ordered E_ij(n)=Σ_{m>0}e_i(n−m)e_j(−m)*−Σ_{m≥0}e_j(m)*e_i(m+n), then X(n)=Σa_ij E_ij(n), on the exact finite-energy domain. Do not use a nonconvergent operator tsum or assume current commutators as fields.; OperatorSmoothVector: Intersection of domains of all powers of the closed skew-adjoint generator; source C∞ vector is for that actual flow, not merely a smooth abstract function supplied independently.; LoopExponential: Pointwise matrix exponential of a smooth su(N)-valued loop, with Lie-polynomial restriction where stated; unbounded current exponential uses its full Stone generator instead. (hard)
§8: Lemma: SkewAdjointOperator: Possibly unbounded densely defined closed operator whose graph equals the negative adjoint graph; an arbitrary bounded skew-Hermitian matrix is too restrictive.; OperatorCore: Dense subdomain whose restricted graph is dense in the full closed operator graph; for X|K retain exact restricted domain and graph norm. (hard)
§9: Proposition: LevelRepresentation: Irreducible unitary summand of the actual F_V^{⊗ℓ} representation of the fixed loop central extension, ℓ≥1, rotations shifted to have nonzero lowest energy zero. General sums retain the stated positive energy finite-multiplicity condition.; HighestWeightModule: Construct V_f as the cyclic SU(N)-submodule generated by the explicit tensor of exterior highest-weight vectors e_f in §2, using a nonnegative representative of f; unitary equivalence class independent of common shifts. Do not freely supply an arbitrary representation named V_f.; FiniteEnergyDomain: Algebraic direct sum of H(n), equivalently finite sums of rotation eigenvectors; distinct from the whole smooth-vector domain and from a single energy eigenspace.; UnitaryEquivalence: the actual source construction, including its domains and topology (hard)
§9: Corollary: LevelRepresentation: Irreducible unitary summand of the actual F_V^{⊗ℓ} representation of the fixed loop central extension, ℓ≥1, rotations shifted to have nonzero lowest energy zero. General sums retain the stated positive energy finite-multiplicity condition.; HighestWeightModule: Construct V_f as the cyclic SU(N)-submodule generated by the explicit tensor of exterior highest-weight vectors e_f in §2, using a nonnegative representative of f; unitary equivalence class independent of common shifts. Do not freely supply an arbitrary representation named V_f.; FiniteEnergyDomain: Algebraic direct sum of H(n), equivalently finite sums of rotation eigenvectors; distinct from the whole smooth-vector domain and from a single energy eigenspace. (hard)
§10: Proposition: FactorAlgebra: Center M∩M′ consists exactly of complex scalar multiples of identity; no type-I or finite-dimensional assumption.; RepresentationSubspace: the actual source construction, including its domains and topology; BoundedIntertwiner: Closed complex subspace of continuous linear maps T:H₁→L[ℂ]H₂ satisfying Tπ₁(g)=π₂(g)T for every element of the specified represented subgroup. Do not assume intertwiner existence or density in its definition. (hard)
§11: Proposition 1: StandardRealSubspace: Closed real-linear subspace K of complex H with K∩iK={0} and closure(K+iK)=H. This is neither a complex subspace nor the accepted operator-algebra StandardForm interface.; RealOrthogonalProjection: Orthogonal projections e onto K and f onto iK in the underlying REAL Hilbert space; they need not be complex-linear. r=(e+f)/2 and t=(e−f)/2 have different complex linearity.; ModularOperators: Construct j=phase(t) and δ^{it}=(I−r)^{it}r^{−it} from the real projections. For M,Ω first use K=closure_R(M_saΩ). Do not take a structure assuming jK=iK⊥, algebra duality, or KMS uniqueness.; PositiveFunctionalCalculus: the actual source construction, including its domains and topology (hard)
§11: Proposition 2 (characterisation of modular operators): StandardRealSubspace: Closed real-linear subspace K of complex H with K∩iK={0} and closure(K+iK)=H. This is neither a complex subspace nor the accepted operator-algebra StandardForm interface.; ModularOperators: Construct j=phase(t) and δ^{it}=(I−r)^{it}r^{−it} from the real projections. For M,Ω first use K=closure_R(M_saΩ). Do not take a structure assuming jK=iK⊥, algebra duality, or KMS uniqueness.; KMSStripExtension: Vector-valued bounded continuous extension to −1/2≤Im z≤0, holomorphic in the interior, boundary f(t−i/2)=j f(t); specify all t and actual real-parameter orbit. (hard)
§12: Lemma 2: ModularOperators: Construct j=phase(t) and δ^{it}=(I−r)^{it}r^{−it} from the real projections. For M,Ω first use K=closure_R(M_saΩ). Do not take a structure assuming jK=iK⊥, algebra duality, or KMS uniqueness. (hard)
§12: Corollary: ModularOperators: Construct j=phase(t) and δ^{it}=(I−r)^{it}r^{−it} from the real projections. For M,Ω first use K=closure_R(M_saΩ). Do not take a structure assuming jK=iK⊥, algebra duality, or KMS uniqueness. (hard)
§12: Theorem (Takesaki devissage [35]): ModularOperators: Construct j=phase(t) and δ^{it}=(I−r)^{it}r^{−it} from the real projections. For M,Ω first use K=closure_R(M_saΩ). Do not take a structure assuming jK=iK⊥, algebra duality, or KMS uniqueness.; InvariantVonNeumannSubalgebra: the actual source construction, including its domains and topology; CyclicCompression: the actual source construction, including its domains and topology (hard)
§13: Lemma: FermionicFockSpace: Hilbert orthogonal direct sum over n≥0 of antisymmetric n-particle tensor powers of the Hilbert space, including the one-dimensional vacuum summand; not merely algebraic ExteriorAlgebra.; LocalCliffordAlgebra: M(K) is the von Neumann algebra generated on ΛH by the actual c(ξ)=a(ξ)+a(ξ)* for ξ∈K, with real localization and fixed Fock representation.; VacuumVector: Unit vector 1 in degree zero of the Hilbert Fock construction; images under specified unitary intertwiners are only phase-dependent and their absolute overlap is well-defined.; StandardRealSubspace: Closed real-linear subspace K of complex H with K∩iK={0} and closure(K+iK)=H. This is neither a complex subspace nor the accepted operator-algebra StandardForm interface. (hard)
§13: Theorem: FermionicFockSpace: Hilbert orthogonal direct sum over n≥0 of antisymmetric n-particle tensor powers of the Hilbert space, including the one-dimensional vacuum summand; not merely algebraic ExteriorAlgebra.; SecondQuantisation: For a contraction A, Λ(A)=⊕_n A^{⊗n}|Λ^n H. For conjugate-linear T, tildeΛ(T)(ξ₁∧…∧ξ_n)=Tξ_n∧…∧Tξ₁, with order reversal; distinguish from ordinary Λ and include the vacuum block.; LocalCliffordAlgebra: M(K) is the von Neumann algebra generated on ΛH by the actual c(ξ)=a(ξ)+a(ξ)* for ξ∈K, with real localization and fixed Fock representation.; ModularOperators: Construct j=phase(t) and δ^{it}=(I−r)^{it}r^{−it} from the real projections. For M,Ω first use K=closure_R(M_saΩ). Do not take a structure assuming jK=iK⊥, algebra duality, or KMS uniqueness.; GradedCommutant: For a Z₂-graded represented algebra, graded commutant κM′κ^{-1}; retain source parity and the even vacuum. Do not replace with ordinary commutant.; KleinTransformation: Bounded unitary κ equal to 1 on even Hilbert vectors, i on odd Hilbert vectors. (hard)
§14: Theorem: HardyProjection: Orthogonal projection P onto that closed nonnegative-Fourier subspace, not pointwise holomorphic extension data supplied as a hypothesis.; PolarizedComplexStructure: Same real Hilbert space L² with scalar i acting as i(2P−I); construct its complex scalar action and inner product, including conjugation on P⊥H.; ArcSupportedL2: Closed subspace of ambient L² consisting of classes vanishing Haar-a.e. outside the chosen measurable arc; not pointwise support of a chosen representative and not only compactly supported smooth functions.; MobiusFlow: u_t on circle L² given by the weighted hyperbolic fractional transform spelled out in assumptions; multiplication factor (z sinhπt+coshπt)^{-1} and the ENTIRE quotient in the argument are fixed. Descends to a.e. classes by nonsingular smooth change of variable.; CircleFlip: Real-linear isometry Ff(z)=z^{-1}f(z^{-1}), unitary in original L² complex structure and conjugate-linear in H_P; distinguish reflection of argument from coefficient conjugation.; ModularOperators: Construct j=phase(t) and δ^{it}=(I−r)^{it}r^{−it} from the real projections. For M,Ω first use K=closure_R(M_saΩ). Do not take a structure assuming jK=iK⊥, algebra duality, or KMS uniqueness. (hard)
§15: Theorem: LocalFermionAlgebra: Von Neumann algebra generated by π_P(a(f)) for every f in localized L²(I,V), on polarized Fock space. Its equivalence to the real-Clifford M(K) is a theorem, not a defining assumption.; PolarizedFockSpace: F_P=Λ(PH) Hilbert graded-tensor Λ(conjugate(P⊥H)); the two factors carry the Koszul signs of the CAR construction.; ModularOperators: Construct j=phase(t) and δ^{it}=(I−r)^{it}r^{−it} from the real projections. For M,Ω first use K=closure_R(M_saΩ). Do not take a structure assuming jK=iK⊥, algebra duality, or KMS uniqueness.; GradedCommutant: For a Z₂-graded represented algebra, graded commutant κM′κ^{-1}; retain source parity and the even vacuum. Do not replace with ordinary commutant.; MobiusFlow: u_t on circle L² given by the weighted hyperbolic fractional transform spelled out in assumptions; multiplication factor (z sinhπt+coshπt)^{-1} and the ENTIRE quotient in the argument are fixed. Descends to a.e. classes by nonsingular smooth change of variable.; CircleFlip: Real-linear isometry Ff(z)=z^{-1}f(z^{-1}), unitary in original L² complex structure and conjugate-linear in H_P; distinguish reflection of argument from coefficient conjugation. (hard)
§16: Proposition: SecondQuantisation: For a contraction A, Λ(A)=⊕_n A^{⊗n}|Λ^n H. For conjugate-linear T, tildeΛ(T)(ξ₁∧…∧ξ_n)=Tξ_n∧…∧Tξ₁, with order reversal; distinguish from ordinary Λ and include the vacuum block.; HilbertTensorProduct: Hilbert completion of algebraic tensor product with product inner product; Fock tensor powers and multiplicity decompositions use it rather than a finite-dimensional tensor model.; MobiusFlow: u_t on circle L² given by the weighted hyperbolic fractional transform spelled out in assumptions; multiplication factor (z sinhπt+coshπt)^{-1} and the ENTIRE quotient in the argument are fixed. Descends to a.e. classes by nonsingular smooth change of variable.; VacuumVector: Unit vector 1 in degree zero of the Hilbert Fock construction; images under specified unitary intertwiners are only phase-dependent and their absolute overlap is well-defined. (hard)
§16: Corollary: LocalFermionAlgebra: Von Neumann algebra generated by π_P(a(f)) for every f in localized L²(I,V), on polarized Fock space. Its equivalence to the real-Clifford M(K) is a theorem, not a defining assumption.; ModularOperators: Construct j=phase(t) and δ^{it}=(I−r)^{it}r^{−it} from the real projections. For M,Ω first use K=closure_R(M_saΩ). Do not take a structure assuming jK=iK⊥, algebra duality, or KMS uniqueness.; FactorAlgebra: Center M∩M′ consists exactly of complex scalar multiples of identity; no type-I or finite-dimensional assumption.; TypeIII1Factor: A factor of type III whose Connes S invariant is [0,∞); requires actual normal positive weights/modular spectra, not merely the proved trivial fixed-point property renamed type III₁.; ConnesSpectrum: Connes invariant from intersection of spectra of actual modular operators over faithful normal semifinite weights (equivalently standard state formulation in this sigma-finite local setting); logarithmic positive spectrum is all R for type III₁. Fix the additive versus multiplicative form explicitly. (hard)
§17: Covering lemma: SmoothLoopGroup: Smooth periodic matrix-valued maps g:S¹→SU(N), with pointwise product. This is the source C∞ loop group, not all continuous or measurable loops.; LocalLoopGroup: Smooth loops equal to identity off a nonempty proper open arc I, and their full preimage in the fixed central extension; do not use compact support strictly inside I if it changes endpoint-flat loops.; FiniteOpenArcCover: Finite list of nonempty proper open arcs with union S¹; generated subgroup is algebraic, not a closure. (hard)
§17: Proposition (locality): LocalLoopGroup: Smooth loops equal to identity off a nonempty proper open arc I, and their full preimage in the fixed central extension; do not use compact support strictly inside I if it changes endpoint-flat loops.; LevelRepresentation: Irreducible unitary summand of the actual F_V^{⊗ℓ} representation of the fixed loop central extension, ℓ≥1, rotations shifted to have nonzero lowest energy zero. General sums retain the stated positive energy finite-multiplicity condition. (hard)
§17: Reeh–Schlieder theorem: LevelRepresentation: Irreducible unitary summand of the actual F_V^{⊗ℓ} representation of the fixed loop central extension, ℓ≥1, rotations shifted to have nonzero lowest energy zero. General sums retain the stated positive energy finite-multiplicity condition.; FiniteEnergyDomain: Algebraic direct sum of H(n), equivalently finite sums of rotation eigenvectors; distinct from the whole smooth-vector domain and from a single energy eigenspace.; LocalLoopGroup: Smooth loops equal to identity off a nonempty proper open arc I, and their full preimage in the fixed central extension; do not use compact support strictly inside I if it changes endpoint-flat loops. (hard)
§17: Theorem A (factoriality): LocalLoopAlgebra: π(L_I G)′′ on the given full or sector Hilbert space; use actual lifted actions so each generator is a unitary and its phase has no effect on the generated algebra.; FactorAlgebra: Center M∩M′ consists exactly of complex scalar multiples of identity; no type-I or finite-dimensional assumption. (hard)
§17: Theorem B (local equivalence): LocalLoopAlgebra: π(L_I G)′′ on the given full or sector Hilbert space; use actual lifted actions so each generator is a unitary and its phase has no effect on the generated algebra.; BoundedIntertwiner: Closed complex subspace of continuous linear maps T:H₁→L[ℂ]H₂ satisfying Tπ₁(g)=π₂(g)T for every element of the specified represented subgroup. Do not assume intertwiner existence or density in its definition. (hard)
§17: Theorem C (Haag duality): VacuumRepresentation: Closed cyclic loop-group subrepresentation of F_V^{⊗ℓ} generated by its unit vacuum; it is the actual level-ℓ H₀, not any sector with a chosen vector.; LocalLoopAlgebra: π(L_I G)′′ on the given full or sector Hilbert space; use actual lifted actions so each generator is a unitary and its phase has no effect on the generated algebra.; ModularOperators: Construct j=phase(t) and δ^{it}=(I−r)^{it}r^{−it} from the real projections. For M,Ω first use K=closure_R(M_saΩ). Do not take a structure assuming jK=iK⊥, algebra duality, or KMS uniqueness.; MobiusAction: SU_±(1,1) matrices and fractional-linear action on S¹, with weighted one-particle action V_γ f(z)=(α−conj(β)z)^{-1}f(γ^{-1}z) in the source barred-matrix convention; preserve linear/antilinear quantisation distinction. (hard)
§17: Theorem D (generalised Haag duality): VacuumProjection: Orthogonal projection e in the full tensor Fock space onto the actual vacuum subrepresentation closure(π^{⊗ℓ}(LG)Ω).; LocalFermionAlgebra: Von Neumann algebra generated by π_P(a(f)) for every f in localized L²(I,V), on polarized Fock space. Its equivalence to the real-Clifford M(K) is a theorem, not a defining assumption.; LocalLoopAlgebra: π(L_I G)′′ on the given full or sector Hilbert space; use actual lifted actions so each generator is a unitary and its phase has no effect on the generated algebra.; ObservableAlgebra: Global bicommutant π^{⊗ℓ}(LG)′′ on tensor Fock space, including the fixed parity. Distinct from the entire local CAR algebra. (hard)
§17: Theorem E (von Neumann density): LocalLoopAlgebra: π(L_I G)′′ on the given full or sector Hilbert space; use actual lifted actions so each generator is a unitary and its phase has no effect on the generated algebra.; TouchingArcs: I₁,I₂ are the two open components of I minus a single interior point; closures meet there and their union differs from I by that null singleton. (hard)
§17: Theorem F (irreducibility): LoopsFlatOnFiniteSet: L_A G consists of smooth loops whose identity-subtracted matrix entries and every angular derivative vanish at each point of the given finite A; lift via full preimage in the central extension.; LevelRepresentation: Irreducible unitary summand of the actual F_V^{⊗ℓ} representation of the fixed loop central extension, ℓ≥1, rotations shifted to have nonzero lowest energy zero. General sums retain the stated positive energy finite-multiplicity condition.; LocalLoopAlgebra: π(L_I G)′′ on the given full or sector Hilbert space; use actual lifted actions so each generator is a unitary and its phase has no effect on the generated algebra. (hard)
§18: Theorem: CanonicalFrobeniusSolutions: Unique Frobenius series f_i=z^{λ_i}Σ_{n≥0}ξ_i,n z^n, ξ_i,0=ξ_i normalized by φ=1, and the infinity analogue h_j=z^{µ_j}Σζ_j,n z^{−n}, followed by continuation on the positive-axis slit with arg∈(0,2π). Recurrence coefficients come from the ODE, not free solutions constrained by the desired result.; TransportMatrix: Change-of-basis coefficients c_ij between these actual normalized solution bases f_i=Σ_jc_ijh_j; fix evaluation at a regular slit-plane base point and branch. No Gamma formula in the definition.; ReciprocalGammaProduct: Explicit scalar Gamma products in the theorem with reciprocal Gamma entire continuation in denominator factors; numerator arguments are nonpoles under nonresonance. Mathlib Complex.Gamma returns 0 at nonpositive integers, so the reciprocal interpretation must be spelled out at those zeros. (hard)
§18: Corollary: ShiftedRankOneODEData: A,B with B=−αI+βQ, Q rank-one idempotent, β≠0, φ(v)=1; both A and B−A have simple nonresonant spectra and general position with Q. Use eigenvalues µ of A−B.; CanonicalFrobeniusSolutions: Unique Frobenius series f_i=z^{λ_i}Σ_{n≥0}ξ_i,n z^n, ξ_i,0=ξ_i normalized by φ=1, and the infinity analogue h_j=z^{µ_j}Σζ_j,n z^{−n}, followed by continuation on the positive-axis slit with arg∈(0,2π). Recurrence coefficients come from the ODE, not free solutions constrained by the desired result.; TransportMatrix: Change-of-basis coefficients c_ij between these actual normalized solution bases f_i=Σ_jc_ijh_j; fix evaluation at a regular slit-plane base point and branch. No Gamma formula in the definition.; ReciprocalGammaProduct: Explicit scalar Gamma products in the theorem with reciprocal Gamma entire continuation in denominator factors; numerator arguments are nonpoles under nonresonance. Mathlib Complex.Gamma returns 0 at nonpositive integers, so the reciprocal interpretation must be spelled out at those zeros. (hard)
§21: Proposition: TransportMatrix: Change-of-basis coefficients c_ij between these actual normalized solution bases f_i=Σ_jc_ijh_j; fix evaluation at a regular slit-plane base point and branch. No Gamma formula in the definition.; SpectralParameterDomain: Open set of labeled λ,µ with distinct, separately nonresonant spectra, cross-disjoint spectra for general position, and Σλ−Σµ≠0; use companion construction to realize actual admissible pairs. (hard)
§24: Theorem: CanonicalFrobeniusSolutions: Unique Frobenius series f_i=z^{λ_i}Σ_{n≥0}ξ_i,n z^n, ξ_i,0=ξ_i normalized by φ=1, and the infinity analogue h_j=z^{µ_j}Σζ_j,n z^{−n}, followed by continuation on the positive-axis slit with arg∈(0,2π). Recurrence coefficients come from the ODE, not free solutions constrained by the desired result.; TransportMatrix: Change-of-basis coefficients c_ij between these actual normalized solution bases f_i=Σ_jc_ijh_j; fix evaluation at a regular slit-plane base point and branch. No Gamma formula in the definition.; ReciprocalGammaProduct: Explicit scalar Gamma products in the theorem with reciprocal Gamma entire continuation in denominator factors; numerator arguments are nonpoles under nonresonance. Mathlib Complex.Gamma returns 0 at nonpositive integers, so the reciprocal interpretation must be spelled out at those zeros. (hard)
§25: Uniqueness Theorem: AlgebraicPrimaryField: Complex-linear map V^0⊗H_j^0→H_i^0 commuting with algebraic current and rotation action; modes φ(v,n):H_j^0→H_i^0 satisfy the corresponding linear covariance. No L² bound, initial-term bijection, braiding, or existence conclusion assumed in this definition.; InitialTerm: Restriction φ₀:V⊗H_j(0)→H_i(0), justified by energy preservation; not an arbitrary input with the extension theorem already assumed.; HighestWeightModule: Construct V_f as the cyclic SU(N)-submodule generated by the explicit tensor of exterior highest-weight vectors e_f in §2, using a nonnegative representative of f; unitary equivalence class independent of common shifts. Do not freely supply an arbitrary representation named V_f. (hard)
§25: Lemma: ExteriorCreationOperator: Bounded operator a(f)ω=f∧ω on the correctly normalized antisymmetric Hilbert Fock space, adjoint annihilation; linear in f with norm ‖f‖.; FermionicInitialTerm: Compressed exterior multiplication on W⊗ΛW, W=C^N⊗C^ℓ, with projections to permissible finite-dimensional summands and an equivariant (possibly scaled) charge embedding. One nonzero intertwiner spans the one-dimensional allowed Hom space.; BoundedIntertwiner: Closed complex subspace of continuous linear maps T:H₁→L[ℂ]H₂ satisfying Tπ₁(g)=π₂(g)T for every element of the specified represented subgroup. Do not assume intertwiner existence or density in its definition. (hard)
§25: Construction of all vector primary fields: AlgebraicPrimaryField: Complex-linear map V^0⊗H_j^0→H_i^0 commuting with algebraic current and rotation action; modes φ(v,n):H_j^0→H_i^0 satisfy the corresponding linear covariance. No L² bound, initial-term bijection, braiding, or existence conclusion assumed in this definition.; CompressedFermionField: Pi π_P(a(ι(f))) Pj on actual irreducible sector subspaces of F_W, with equivariant charge map ι:C^N→W and normalized sector identifications; dual uses adjoint creation. Construction has a complete body independent of the later existence theorem.; InitialTerm: Restriction φ₀:V⊗H_j(0)→H_i(0), justified by energy preservation; not an arbitrary input with the extension theorem already assumed.; SmearedPrimaryField: Bounded-operator-valued L² extension of the algebraic modes when the L² estimate holds; for vector/dual fields use the concrete compressed-fermion body. Correct source-target actions π_i φ_ij π_j*.; BoundedIntertwiner: Closed complex subspace of continuous linear maps T:H₁→L[ℂ]H₂ satisfying Tπ₁(g)=π₂(g)T for every element of the specified represented subgroup. Do not assume intertwiner existence or density in its definition. (hard)
§25: Theorem: AlgebraicPrimaryField: Complex-linear map V^0⊗H_j^0→H_i^0 commuting with algebraic current and rotation action; modes φ(v,n):H_j^0→H_i^0 satisfy the corresponding linear covariance. No L² bound, initial-term bijection, braiding, or existence conclusion assumed in this definition.; AdjointPrimaryField: Charge V* and reversed sectors, ψ(v*,n)=φ(v,−n)* on finite-dimensional energy blocks, with v*(w)=(w,v) in source convention.; CompressedFermionField: Pi π_P(a(ι(f))) Pj on actual irreducible sector subspaces of F_W, with equivariant charge map ι:C^N→W and normalized sector identifications; dual uses adjoint creation. Construction has a complete body independent of the later existence theorem.; SmearedPrimaryField: Bounded-operator-valued L² extension of the algebraic modes when the L² estimate holds; for vector/dual fields use the concrete compressed-fermion body. Correct source-target actions π_i φ_ij π_j*.; BoundedIntertwiner: Closed complex subspace of continuous linear maps T:H₁→L[ℂ]H₂ satisfying Tπ₁(g)=π₂(g)T for every element of the specified represented subgroup. Do not assume intertwiner existence or density in its definition. (hard)
§26: Proposition 1: FourPointFunction: F_k(z)=Σ_{n≥0}(φ^U_ik(u,n)φ^V_kj(v,−n)ξ,η)z^n for all lowest ξ,η, valued in Hom_G(U⊗V⊗V_j,V_i). Mode signs fixed by energy; analytic convergence for bounded vector/dual modes, otherwise formal series.; CircleConvolution: the actual source construction, including its domains and topology; SmearedPrimaryField: Bounded-operator-valued L² extension of the algebraic modes when the L² estimate holds; for vector/dual fields use the concrete compressed-fermion body. Correct source-target actions π_i φ_ij π_j*.; NormalizedAngularIntegral: the actual source construction, including its domains and topology (hard)
§26: Corollary: FourPointFunction: F_k(z)=Σ_{n≥0}(φ^U_ik(u,n)φ^V_kj(v,−n)ξ,η)z^n for all lowest ξ,η, valued in Hom_G(U⊗V⊗V_j,V_i). Mode signs fixed by energy; analytic convergence for bounded vector/dual modes, otherwise formal series.; CircleConvolution: the actual source construction, including its domains and topology; NormalizedAngularIntegral: the actual source construction, including its domains and topology (hard)
§26: Proposition 2: FourPointFunction: F_k(z)=Σ_{n≥0}(φ^U_ik(u,n)φ^V_kj(v,−n)ξ,η)z^n for all lowest ξ,η, valued in Hom_G(U⊗V⊗V_j,V_i). Mode signs fixed by energy; analytic convergence for bounded vector/dual modes, otherwise formal series.; BoundaryTransportRelation: For all coefficient vectors and θ∈(0,2π), F_k(e^{iθ})=Σ_h c_kh e^{iµ_kh θ}G_h(e^{−iθ}), with real µ and continuous cut-circle boundary extensions; no operator braiding built into the hypothesis.; SmearedPrimaryField: Bounded-operator-valued L² extension of the algebraic modes when the L² estimate holds; for vector/dual fields use the concrete compressed-fermion body. Correct source-target actions π_i φ_ij π_j*.; CutCirclePhase: e_µ(e^{iθ})=exp(iµθ), using unique θ∈(0,2π) off the cut point 1; multiply test functions as L² classes. Disclose arbitrary value at the measure-zero cut if a total function is needed. (hard)
§26: Proposition 3: SmearedPrimaryField: Bounded-operator-valued L² extension of the algebraic modes when the L² estimate holds; for vector/dual fields use the concrete compressed-fermion body. Correct source-target actions π_i φ_ij π_j*.; BoundaryTransportRelation: For all coefficient vectors and θ∈(0,2π), F_k(e^{iθ})=Σ_h c_kh e^{iµ_kh θ}G_h(e^{−iθ}), with real µ and continuous cut-circle boundary extensions; no operator braiding built into the hypothesis.; FiniteEnergyDomain: Algebraic direct sum of H(n), equivalently finite sums of rotation eigenvectors; distinct from the whole smooth-vector domain and from a single energy eigenspace. (hard)
§26: Corollary 1: SmearedPrimaryField: Bounded-operator-valued L² extension of the algebraic modes when the L² estimate holds; for vector/dual fields use the concrete compressed-fermion body. Correct source-target actions π_i φ_ij π_j*.; CutCirclePhase: e_µ(e^{iθ})=exp(iµθ), using unique θ∈(0,2π) off the cut point 1; multiply test functions as L² classes. Disclose arbitrary value at the measure-zero cut if a total function is needed.; OrderedDisjointArcs: Two disjoint intervals/supports in S¹ minus 1, with every angle of J larger than every angle of I in (0,2π); reverse order is a different hypothesis with the e^{2πiµ} coefficient correction. (hard)
§26: Corollary 2: SmearedPrimaryField: Bounded-operator-valued L² extension of the algebraic modes when the L² estimate holds; for vector/dual fields use the concrete compressed-fermion body. Correct source-target actions π_i φ_ij π_j*.; CutCirclePhase: e_µ(e^{iθ})=exp(iµθ), using unique θ∈(0,2π) off the cut point 1; multiply test functions as L² classes. Disclose arbitrary value at the measure-zero cut if a total function is needed.; OrderedDisjointArcs: Two disjoint intervals/supports in S¹ minus 1, with every angle of J larger than every angle of I in (0,2π); reverse order is a different hypothesis with the e^{2πiµ} coefficient correction. (hard)
§27: 27. Sugawara’s formula: SugawaraOperator: On H^0, L₀=(N+ℓ)^{-1}(−Σ_i X_i(0)^2/2−Σ_{n>0,i}X_i(−n)X_i(n)), locally finite on each input; do not put the theorem L₀=D+Δ/(2(N+ℓ)) into its definition.; CasimirEigenvalue: Δ_f=Σ_{i=1}^N(f_i²+f_i(N−2i+1))−(Σ_i f_i)²/N, N≥2 for the nontrivial SU(N) theory, real/integer tuple casts explicit; invariant under common shifts.; EnergyOperator: Closed self-adjoint generator D of normalized rotations, with domain square-summability of energy-weighted spectral components; acts as n on H(n).; FiniteEnergyDomain: Algebraic direct sum of H(n), equivalently finite sums of rotation eigenvectors; distinct from the whole smooth-vector domain and from a single energy eigenspace.; LieAlgebraForm: Real positive inner product on su(N), (X,Y)=−Tr(XY); complex-bilinear extension on the complexified algebra when matrix units are used. (hard)
§28: Theorem: FourPointFunction: F_k(z)=Σ_{n≥0}(φ^U_ik(u,n)φ^V_kj(v,−n)ξ,η)z^n for all lowest ξ,η, valued in Hom_G(U⊗V⊗V_j,V_i). Mode signs fixed by energy; analytic convergence for bounded vector/dual modes, otherwise formal series.; CasimirInteraction: Ω_ij=−Σ_p π_i(X_p)π_j(X_p), first on ambient fourfold Hom representation, then restrict the invariant contracted operator to W; do not assert individual π_i preserve W.; CasimirEigenvalue: Δ_f=Σ_{i=1}^N(f_i²+f_i(N−2i+1))−(Σ_i f_i)²/N, N≥2 for the nontrivial SU(N) theory, real/integer tuple casts explicit; invariant under common shifts.; FormalKZEquation: Identity of formal series after multiplying the displayed regular-singular ODE by z(z−1), with actual Casimir matrices and Δ scalars, not a type of arbitrary functions assumed to solve the equation. (hard)
§29: Proposition: FourPointFunction: F_k(z)=Σ_{n≥0}(φ^U_ik(u,n)φ^V_kj(v,−n)ξ,η)z^n for all lowest ξ,η, valued in Hom_G(U⊗V⊗V_j,V_i). Mode signs fixed by energy; analytic convergence for bounded vector/dual modes, otherwise formal series.; CasimirInteraction: Ω_ij=−Σ_p π_i(X_p)π_j(X_p), first on ambient fourfold Hom representation, then restrict the invariant contracted operator to W; do not assert individual π_i preserve W.; KZNormalizedSolutions: Gauge transformations f_k(z)=z^{λ_k}F_k(z), g_h(z)=z^{µ_h}G_h(z^{-1}), with spectral/Casimir exponents, sector intertwiners and branch fixed; distinguish formal and convergent realizations.; CanonicalFrobeniusSolutions: Unique Frobenius series f_i=z^{λ_i}Σ_{n≥0}ξ_i,n z^n, ξ_i,0=ξ_i normalized by φ=1, and the infinity analogue h_j=z^{µ_j}Σζ_j,n z^{−n}, followed by continuation on the positive-axis slit with arg∈(0,2π). Recurrence coefficients come from the ODE, not free solutions constrained by the desired result. (hard)
§29: Theorem A (generalised hypergeometric braiding): VectorDualBraiding: Operator identities for products of vector and dual-vector smeared fields on ordered disjoint supports, including sums over permissible channels and nonzero coefficients independent of smearings; this is a theorem conclusion predicate, not a field axiom.; SmearedPrimaryField: Bounded-operator-valued L² extension of the algebraic modes when the L² estimate holds; for vector/dual fields use the concrete compressed-fermion body. Correct source-target actions π_i φ_ij π_j*.; CutCirclePhase: e_µ(e^{iθ})=exp(iµθ), using unique θ∈(0,2π) off the cut point 1; multiply test functions as L² classes. Disclose arbitrary value at the measure-zero cut if a total function is needed.; CasimirEigenvalue: Δ_f=Σ_{i=1}^N(f_i²+f_i(N−2i+1))−(Σ_i f_i)²/N, N≥2 for the nontrivial SU(N) theory, real/integer tuple casts explicit; invariant under common shifts. (hard)
§29: Theorem B (hypergeometric braiding): VectorVectorBraiding: The analogous vector-vector product identities with α_gg₁ anomalies and allowed intermediate diagrams; distinguish non-Abelian two-channel and unique-path symmetric/antisymmetric cases.; SmearedPrimaryField: Bounded-operator-valued L² extension of the algebraic modes when the L² estimate holds; for vector/dual fields use the concrete compressed-fermion body. Correct source-target actions π_i φ_ij π_j*.; CutCirclePhase: e_µ(e^{iθ})=exp(iµθ), using unique θ∈(0,2π) off the cut point 1; multiply test functions as L² classes. Disclose arbitrary value at the measure-zero cut if a total function is needed.; CasimirEigenvalue: Δ_f=Σ_{i=1}^N(f_i²+f_i(N−2i+1))−(Σ_i f_i)²/N, N≥2 for the nontrivial SU(N) theory, real/integer tuple casts explicit; invariant under common shifts. (hard)
§29: Theorem C (Abelian braiding): VectorDualBraiding: Operator identities for products of vector and dual-vector smeared fields on ordered disjoint supports, including sums over permissible channels and nonzero coefficients independent of smearings; this is a theorem conclusion predicate, not a field axiom.; CutCirclePhase: e_µ(e^{iθ})=exp(iµθ), using unique θ∈(0,2π) off the cut point 1; multiply test functions as L² classes. Disclose arbitrary value at the measure-zero cut if a total function is needed.; CasimirEigenvalue: Δ_f=Σ_{i=1}^N(f_i²+f_i(N−2i+1))−(Σ_i f_i)²/N, N≥2 for the nontrivial SU(N) theory, real/integer tuple casts explicit; invariant under common shifts. (hard)
§29: Theorem D (Abelian braiding): Pinned source/provenance obstacle: §29: Theorem D (Abelian braiding) (source-ambiguity)
§29: Theorem: AnomalyCorrectedField: a_gf=φ^vector_gf(e_{−α_gf}F), α_gf=(Δ_g−Δ_f−Δ_vector)/(2(N+ℓ)); dual is the adjoint with conjugate test vector. It is a computed modification of an actual field, not an arbitrary family with braiding assumed.; VectorDualBraiding: Operator identities for products of vector and dual-vector smeared fields on ordered disjoint supports, including sums over permissible channels and nonzero coefficients independent of smearings; this is a theorem conclusion predicate, not a field axiom.; VectorVectorBraiding: The analogous vector-vector product identities with α_gg₁ anomalies and allowed intermediate diagrams; distinguish non-Abelian two-channel and unique-path symmetric/antisymmetric cases.; OrderedDisjointArcs: Two disjoint intervals/supports in S¹ minus 1, with every angle of J larger than every angle of I in (0,2π); reverse order is a different hypothesis with the e^{2πiµ} coefficient correction. (hard)
§29: Corollary: AnomalyCorrectedField: a_gf=φ^vector_gf(e_{−α_gf}F), α_gf=(Δ_g−Δ_f−Δ_vector)/(2(N+ℓ)); dual is the adjoint with conjugate test vector. It is a computed modification of an actual field, not an arbitrary family with braiding assumed.; VectorDualBraiding: Operator identities for products of vector and dual-vector smeared fields on ordered disjoint supports, including sums over permissible channels and nonzero coefficients independent of smearings; this is a theorem conclusion predicate, not a field axiom.; VectorVectorBraiding: The analogous vector-vector product identities with α_gg₁ anomalies and allowed intermediate diagrams; distinguish non-Abelian two-channel and unique-path symmetric/antisymmetric cases.; OrderedDisjointArcs: Two disjoint intervals/supports in S¹ minus 1, with every angle of J larger than every angle of I in (0,2π); reverse order is a different hypothesis with the e^{2πiµ} coefficient correction. (hard)
§30: Lemma: ConnesFusion: Separated Hilbert completion of the actual four-point sesquilinear form on Hom_{L_Ic}(H₀,X)⊗Hom_{L_I}(H₀,Y); quotient its null subspace. Do not substitute ordinary Hilbert tensor product or arbitrary objects satisfying fusion rules.; FusionPreinnerProduct: Sesquilinear form on algebraic bounded-intertwiner tensor product whose simple-tensor value is source (x₂x₁ y₂y₁Ω,Ω); translate argument order into Lean's second-linear convention. Positivity is a theorem, not an axiom supplied by users.; BoundedIntertwiner: Closed complex subspace of continuous linear maps T:H₁→L[ℂ]H₂ satisfying Tπ₁(g)=π₂(g)T for every element of the specified represented subgroup. Do not assume intertwiner existence or density in its definition.; LocalFusionAction: Action of L_I G·L_Ic G on the separated completion induced by gx⊗hy; check the shared central circle acts once at level ℓ. Continuity and level are conclusions to be stated. (hard)
§30: Lemma: ConnesFusion: Separated Hilbert completion of the actual four-point sesquilinear form on Hom_{L_Ic}(H₀,X)⊗Hom_{L_I}(H₀,Y); quotient its null subspace. Do not substitute ordinary Hilbert tensor product or arbitrary objects satisfying fusion rules.; VacuumRepresentation: Closed cyclic loop-group subrepresentation of F_V^{⊗ℓ} generated by its unit vacuum; it is the actual level-ℓ H₀, not any sector with a chosen vector.; BoundedIntertwiner: Closed complex subspace of continuous linear maps T:H₁→L[ℂ]H₂ satisfying Tπ₁(g)=π₂(g)T for every element of the specified represented subgroup. Do not assume intertwiner existence or density in its definition. (hard)
§30: Lemma: ConnesFusion: Separated Hilbert completion of the actual four-point sesquilinear form on Hom_{L_Ic}(H₀,X)⊗Hom_{L_I}(H₀,Y); quotient its null subspace. Do not substitute ordinary Hilbert tensor product or arbitrary objects satisfying fusion rules.; MobiusAction: SU_±(1,1) matrices and fractional-linear action on S¹, with weighted one-particle action V_γ f(z)=(α−conj(β)z)^{-1}f(γ^{-1}z) in the source barred-matrix convention; preserve linear/antilinear quantisation distinction.; FusionIntervalTransport: On dense tensors, x↦π_X(φ)xπ₀(φ)* and y↦π_Y(φ)yπ₀(φ)* for φ(I)=J; unitary extension is the theorem. Dependence on projective lifts is only scalar. (hard)
§30: Hilbert space continuity lemma: ConnesFusion: Separated Hilbert completion of the actual four-point sesquilinear form on Hom_{L_Ic}(H₀,X)⊗Hom_{L_I}(H₀,Y); quotient its null subspace. Do not substitute ordinary Hilbert tensor product or arbitrary objects satisfying fusion rules.; BoundedIntertwiner: Closed complex subspace of continuous linear maps T:H₁→L[ℂ]H₂ satisfying Tπ₁(g)=π₂(g)T for every element of the specified represented subgroup. Do not assume intertwiner existence or density in its definition.; FusionContinuityMaps: Canonical extensions of the dense map to 𝓧⊗Y and X⊗𝓨 with the two row-operator estimates in the source; mixed tensor topologies must be specified, never assumed as bounded maps without the estimates. (hard)
§30: Corollary (associativity of fusion): ConnesFusion: Separated Hilbert completion of the actual four-point sesquilinear form on Hom_{L_Ic}(H₀,X)⊗Hom_{L_I}(H₀,Y); quotient its null subspace. Do not substitute ordinary Hilbert tensor product or arbitrary objects satisfying fusion rules.; FusionAssociator: Dense-tensor reassociation map between the two separated fusion completions, required to intertwine local actions; the theorem establishes that it extends unitarily, not an axiom making arbitrary fusion associative. (hard)
§31: Theorem (transport formula): AnomalyCorrectedField: a_gf=φ^vector_gf(e_{−α_gf}F), α_gf=(Δ_g−Δ_f−Δ_vector)/(2(N+ℓ)); dual is the adjoint with conjugate test vector. It is a computed modification of an actual field, not an arbitrary family with braiding assumed.; LocalEquivalenceMap: The unique generator-matching star isomorphism a↦π_f(a) between vacuum and sector local algebras, constructed by restriction from the common Fock factor. Its existence and uniqueness are stated results, not fields assumed to define a generic representation.; PositiveTransportCoefficients: Finite real coefficients λ_g>0 of the generator-matching local-algebra transport identity, existentially chosen before all smearings; do not define λ_g to be arbitrary positive numbers assumed to satisfy the identity. (hard)
§31: Corollary: ConnesFusion: Separated Hilbert completion of the actual four-point sesquilinear form on Hom_{L_Ic}(H₀,X)⊗Hom_{L_I}(H₀,Y); quotient its null subspace. Do not substitute ordinary Hilbert tensor product or arbitrary objects satisfying fusion rules.; LevelRepresentation: Irreducible unitary summand of the actual F_V^{⊗ℓ} representation of the fixed loop central extension, ℓ≥1, rotations shifted to have nonzero lowest energy zero. General sums retain the stated positive energy finite-multiplicity condition.; AddBoxesDistinctRows: Relation on unnormalized diagrams: g_i−f_i∈{0,1}, Σ_i(g_i−f_i)=k and both tuples decreasing; common-shift normalization only after enumerating successors.; VacuumRepresentation: Closed cyclic loop-group subrepresentation of F_V^{⊗ℓ} generated by its unit vacuum; it is the actual level-ℓ H₀, not any sector with a chosen vector. (hard)
§32: Theorem: AnomalyCorrectedField: a_gf=φ^vector_gf(e_{−α_gf}F), α_gf=(Δ_g−Δ_f−Δ_vector)/(2(N+ℓ)); dual is the adjoint with conjugate test vector. It is a computed modification of an actual field, not an arbitrary family with braiding assumed.; PathFieldProduct: For P=(f₀,…,f_k), a_P=φ_{f_k f_{k−1}}(a_k)⋯φ_{f₁ f₀}(a₁), with actual anomaly-corrected fields and test functions; P₀=(0,[1],…,[k]) computed, not quantified independently.; PathTransportCoefficients: Finite coefficient vectors λ_P(g), and Hermitian matrices µ_PQ(g), for the displayed all-smearings transport equation. µ=conj(λ_P)λ_Q is a RESULT, as are rank≤1, zero outside distinct-row endpoints and all-entry nonvanishing.; LocalEquivalenceMap: The unique generator-matching star isomorphism a↦π_f(a) between vacuum and sector local algebras, constructed by restriction from the common Fock factor. Its existence and uniqueness are stated results, not fields assumed to define a generic representation. (hard)
§32: Corollary: ConnesFusion: Separated Hilbert completion of the actual four-point sesquilinear form on Hom_{L_Ic}(H₀,X)⊗Hom_{L_I}(H₀,Y); quotient its null subspace. Do not substitute ordinary Hilbert tensor product or arbitrary objects satisfying fusion rules.; PathTransportCoefficients: Finite coefficient vectors λ_P(g), and Hermitian matrices µ_PQ(g), for the displayed all-smearings transport equation. µ=conj(λ_P)λ_Q is a RESULT, as are rank≤1, zero outside distinct-row endpoints and all-entry nonvanishing.; AddBoxesDistinctRows: Relation on unnormalized diagrams: g_i−f_i∈{0,1}, Σ_i(g_i−f_i)=k and both tuples decreasing; common-shift normalization only after enumerating successors. (hard)
§33: Lemma (closure under fusion): ConnesFusion: Separated Hilbert completion of the actual four-point sesquilinear form on Hom_{L_Ic}(H₀,X)⊗Hom_{L_I}(H₀,Y); quotient its null subspace. Do not substitute ordinary Hilbert tensor product or arbitrary objects satisfying fusion rules.; FusionTensorPower: Recursive Connes fusion powers of the vector sector, power zero the vacuum and successor tensor with vector; closure and generation of all irreducibles are conclusions.; LevelRepresentation: Irreducible unitary summand of the actual F_V^{⊗ℓ} representation of the fixed loop central extension, ℓ≥1, rotations shifted to have nonzero lowest energy zero. General sums retain the stated positive energy finite-multiplicity condition.; FusionMultiplicity: Multiplicity of irreducible H_k in actual Connes fusion H_i⊠H_j, defined by intertwiner dimension after complete finite decomposition; finite-dimensionality and nonnegative finite counts are proved conclusions, not assumed classification axioms. (hard)
§33: Corollary: Pinned source/provenance obstacle: §33: Corollary (source-ambiguity)
§33: Braiding lemma: ConnesFusion: Separated Hilbert completion of the actual four-point sesquilinear form on Hom_{L_Ic}(H₀,X)⊗Hom_{L_I}(H₀,Y); quotient its null subspace. Do not substitute ordinary Hilbert tensor product or arbitrary objects satisfying fusion rules.; FusionBraidingUnitary: Dense map x⊗y↦R_π*[(R_π y R_π*)⊗(R_π x R_π*)], where domain conjugations also use vacuum rotation; extension to LG-intertwining unitary is the theorem.; RotationImplementation: Actual normalized rotation operators on each sector and then on the fused decomposition; R_π fixes vacuum and lowest energy. No arbitrary energy-character shifts when claiming uniqueness. (hard)
§33: Corollary 1: ConnesFusion: Separated Hilbert completion of the actual four-point sesquilinear form on Hom_{L_Ic}(H₀,X)⊗Hom_{L_I}(H₀,Y); quotient its null subspace. Do not substitute ordinary Hilbert tensor product or arbitrary objects satisfying fusion rules.; UnitaryEquivalence: the actual source construction, including its domains and topology (hard)
§33: Corollary 2: FusionGrothendieckRing: Free Z-module on normalized permissible sector classes, multiplication induced by actual finite fusion multiplicities; unit vacuum, star dual. Do not define via the target character ring and thereby trivialize the isomorphism theorem.; FusionMultiplicity: Multiplicity of irreducible H_k in actual Connes fusion H_i⊠H_j, defined by intertwiner dimension after complete finite decomposition; finite-dimensionality and nonnegative finite counts are proved conclusions, not assumed classification axioms. (hard)
§34: Proposition: SchurCharacter: A single polynomial/Laurent-polynomial alternant quotient X_f for every integral tuple f: det(z_j^{f_i+N−i}) divided polynomially by the Vandermonde det(z_j^{N−i}). For dominant f this is the Schur character; for non-dominant f it is the signed extension used in §34. Never evaluate a raw 0/0 determinant ratio at coincident eigenvalues. Common shifts disappear on ∏z_i=1.; RestrictedCharacterRing: T={D(h):h permissible normalized}, D(h) diagonal with centered h+δ divided by N+ℓ; S is the IMAGE of R(SU(N)) under restriction to this concrete finite T, not stipulated a free ring on symbols.; CharacterRestrictionMap: θ([V])=χ_V|T extended Z-linearly as a star ring map; actual character trace on the concrete diagonal set T. All evaluation characters in the theorem are complex-valued unital ring maps.; WallRepresentationIdeal: Two-sided ideal in the commutative classical representation ring generated by classes [V_f] with f₁−f_N=ℓ+1; exact first forbidden wall, not every nonpermissible representation by fiat.; AddBoxesDistinctRows: Relation on unnormalized diagrams: g_i−f_i∈{0,1}, Σ_i(g_i−f_i)=k and both tuples decreasing; common-shift normalization only after enumerating successors. (hard)
§34: Theorem: ConnesFusion: Separated Hilbert completion of the actual four-point sesquilinear form on Hom_{L_Ic}(H₀,X)⊗Hom_{L_I}(H₀,Y); quotient its null subspace. Do not substitute ordinary Hilbert tensor product or arbitrary objects satisfying fusion rules.; FusionGrothendieckRing: Free Z-module on normalized permissible sector classes, multiplication induced by actual finite fusion multiplicities; unit vacuum, star dual. Do not define via the target character ring and thereby trivialize the isomorphism theorem.; RestrictedCharacterRing: T={D(h):h permissible normalized}, D(h) diagonal with centered h+δ divided by N+ℓ; S is the IMAGE of R(SU(N)) under restriction to this concrete finite T, not stipulated a free ring on symbols.; CharacterRestrictionMap: θ([V])=χ_V|T extended Z-linearly as a star ring map; actual character trace on the concrete diagonal set T. All evaluation characters in the theorem are complex-valued unital ring maps.; FusionCharacterIsomorphism: The Z-linear map on the free sector basis [H_f]↦χ_f|T. Multiplicativity, bijectivity and star preservation are conclusions; they must not enter its definition.; FusionMultiplicity: Multiplicity of irreducible H_k in actual Connes fusion H_i⊠H_j, defined by intertwiner dimension after complete finite decomposition; finite-dimensionality and nonnegative finite counts are proved conclusions, not assumed classification axioms.; ContragredientSignature: f′i=−f{N−i+1}, then common-shift normalization when f_N=0 is required; corresponding finite representation is conjugate dual. Vacuum multiplicity-one is a result, not a property assumed of an arbitrary designated dual. (hard)
§34: Corollary 1 L(Verlinde formulas [38],[20]): ClassicalTensorMultiplicity: Actual finite-dimensional multiplicity dim Hom_SU(N)(V_h,V_f⊗V_g), or equivalent intertwiner convention; computed from ordinary tensor product and unrelated a priori to quantum fusion multiplicities.; FusionMultiplicity: Multiplicity of irreducible H_k in actual Connes fusion H_i⊠H_j, defined by intertwiner dimension after complete finite decomposition; finite-dimensionality and nonnegative finite counts are proved conclusions, not assumed classification axioms.; FusionGrothendieckRing: Free Z-module on normalized permissible sector classes, multiplication induced by actual finite fusion multiplicities; unit vacuum, star dual. Do not define via the target character ring and thereby trivialize the isomorphism theorem. (hard)
§34: Corollary 2 (Segal–Goodman–Wenzl rule [33],[13]): SURepresentationRing: Grothendieck ring of actual finite-dimensional unitary SU(N) representations, additive generators [V_f], multiplication tensor product and star conjugate dual; canonical integer basis indexed by normalized signatures.; FusionGrothendieckRing: Free Z-module on normalized permissible sector classes, multiplication induced by actual finite fusion multiplicities; unit vacuum, star dual. Do not define via the target character ring and thereby trivialize the isomorphism theorem.; CharacterRestrictionMap: θ([V])=χ_V|T extended Z-linearly as a star ring map; actual character trace on the concrete diagonal set T. All evaluation characters in the theorem are complex-valued unital ring maps.; WallRepresentationIdeal: Two-sided ideal in the commutative classical representation ring generated by classes [V_f] with f₁−f_N=ℓ+1; exact first forbidden wall, not every nonpermissible representation by fiat. (hard)
§2: Thus irreducible representations are classified by their signatures: HighestWeightModule: Construct V_f as the cyclic SU(N)-submodule generated by the explicit tensor of exterior highest-weight vectors e_f in §2, using a nonnegative representative of f; unitary equivalence class independent of common shifts. Do not freely supply an arbitrary representation named V_f. (hard)
§3: The complex wave representation is irreducible: CARAlgebra: Unital complex star algebra generated linearly by creation symbols a(f), with a(f)a(g)+a(g)a(f)=0 and a(f)a(g)*+a(g)*a(f)=(f,g)I in the source first-linear convention. Algebraic and represented norm completions must be distinguished.; FermionicFockSpace: Hilbert orthogonal direct sum over n≥0 of antisymmetric n-particle tensor powers of the Hilbert space, including the one-dimensional vacuum summand; not merely algebraic ExteriorAlgebra.; ExteriorCreationOperator: Bounded operator a(f)ω=f∧ω on the correctly normalized antisymmetric Hilbert Fock space, adjoint annihilation; linear in f with norm ‖f‖. (hard)
§3: Note that if [u, P ] = 0,: CanonicalQuantisation: Exterior functor applied to a linear isometry or conjugate-linear isometry for H_P, fixing the vacuum; commuting with P yields unitary and exchanging P with P⊥ yields antiunitary on F_P.; PolarizedFockSpace: F_P=Λ(PH) Hilbert graded-tensor Λ(conjugate(P⊥H)); the two factors carry the Koszul signs of the CAR construction. (hard)
§4: In fact if f ∈ C ∞: CircleMultiplicationOperator: m(f)g(z)=f(z)g(z) for smooth matrix f and L²-vector g; a bounded operator with the actual pointwise matrix action.; HardyProjection: Orthogonal projection P onto that closed nonnegative-Fourier subspace, not pointwise holomorphic extension data supplied as a hypothesis. (hard)
§19: Remarks. This argument applies also: CanonicalFrobeniusSolutions: Unique Frobenius series f_i=z^{λ_i}Σ_{n≥0}ξ_i,n z^n, ξ_i,0=ξ_i normalized by φ=1, and the infinity analogue h_j=z^{µ_j}Σζ_j,n z^{−n}, followed by continuation on the positive-axis slit with arg∈(0,2π). Recurrence coefficients come from the ODE, not free solutions constrained by the desired result. (hard)
§23: Using the beta function identity: EulerThomaeIntegral: The integrable cube (0,1)^{d−1} kernel and Beta/Gamma normalization in eq.(6), for real strictly ordered spectra with λ₁<µ_j<λ₁+1. Negative z or slit-plane branch fixed; no unguarded Bochner integral on nonintegrable powers.; CanonicalFrobeniusSolutions: Unique Frobenius series f_i=z^{λ_i}Σ_{n≥0}ξ_i,n z^n, ξ_i,0=ξ_i normalized by φ=1, and the infinity analogue h_j=z^{µ_j}Σζ_j,n z^{−n}, followed by continuation on the positive-axis slit with arg∈(0,2π). Recurrence coefficients come from the ODE, not free solutions constrained by the desired result.; ReciprocalGammaProduct: Explicit scalar Gamma products in the theorem with reciprocal Gamma entire continuation in denominator factors; numerator arguments are nonpoles under nonresonance. Mathlib Complex.Gamma returns 0 at nonpositive integers, so the reciprocal interpretation must be spelled out at those zeros. (hard)
§25: Adjoints of primary fields: AlgebraicPrimaryField: Complex-linear map V^0⊗H_j^0→H_i^0 commuting with algebraic current and rotation action; modes φ(v,n):H_j^0→H_i^0 satisfy the corresponding linear covariance. No L² bound, initial-term bijection, braiding, or existence conclusion assumed in this definition.; AdjointPrimaryField: Charge V* and reversed sectors, ψ(v*,n)=φ(v,−n)* on finite-dimensional energy blocks, with v*(w)=(w,v) in source convention.; InitialTerm: Restriction φ₀:V⊗H_j(0)→H_i(0), justified by energy preservation; not an arbitrary input with the extension theorem already assumed. (hard)
§27: Remark. Note that the operator C: CasimirEigenvalue: Δ_f=Σ_{i=1}^N(f_i²+f_i(N−2i+1))−(Σ_i f_i)²/N, N≥2 for the nontrivial SU(N) theory, real/integer tuple casts explicit; invariant under common shifts.; LieAlgebraForm: Real positive inner product on su(N), (X,Y)=−Tr(XY); complex-bilinear extension on the complexified algebra when matrix units are used.; HighestWeightModule: Construct V_f as the cyclic SU(N)-submodule generated by the explicit tensor of exterior highest-weight vectors e_f in §2, using a nonnegative representative of f; unitary equivalence class independent of common shifts. Do not freely supply an arbitrary representation named V_f. (hard)
§28: Now let (Xi ) be an orthonormal basis: CasimirInteraction: Ω_ij=−Σ_p π_i(X_p)π_j(X_p), first on ambient fourfold Hom representation, then restrict the invariant contracted operator to W; do not assert individual π_i preserve W.; CasimirEigenvalue: Δ_f=Σ_{i=1}^N(f_i²+f_i(N−2i+1))−(Σ_i f_i)²/N, N≥2 for the nontrivial SU(N) theory, real/integer tuple casts explicit; invariant under common shifts.; FourPointInvariantSpace: Actual finite-dimensional Hom_G(V₂⊗V₃⊗V₄,V₁) subspace with four commuting actions on ambient Hom; identify the fourth as a dual via the source first-linear inner convention. (hard)
§32: Proof. (1) The linear span: PathFieldProduct: For P=(f₀,…,f_k), a_P=φ_{f_k f_{k−1}}(a_k)⋯φ_{f₁ f₀}(a₁), with actual anomaly-corrected fields and test functions; P₀=(0,[1],…,[k]) computed, not quantified independently.; HilbertDirectSum: Square-summable Hilbert sum of represented spaces with diagonal action; allow path-indexed repeated equivalent summands and explicitly retain their multiplicities. (hard)
§32: (2) We have: PathTransportCoefficients: Finite coefficient vectors λ_P(g), and Hermitian matrices µ_PQ(g), for the displayed all-smearings transport equation. µ=conj(λ_P)λ_Q is a RESULT, as are rank≤1, zero outside distinct-row endpoints and all-entry nonvanishing.; PathFieldProduct: For P=(f₀,…,f_k), a_P=φ_{f_k f_{k−1}}(a_k)⋯φ_{f₁ f₀}(a₁), with actual anomaly-corrected fields and test functions; P₀=(0,[1],…,[k]) computed, not quantified independently.; LocalEquivalenceMap: The unique generator-matching star isomorphism a↦π_f(a) between vacuum and sector local algebras, constructed by restriction from the common Fock factor. Its existence and uniqueness are stated results, not fields assumed to define a generic representation. (hard)
§32: (3) If g >k f: PathTransportCoefficients: Finite coefficient vectors λ_P(g), and Hermitian matrices µ_PQ(g), for the displayed all-smearings transport equation. µ=conj(λ_P)λ_Q is a RESULT, as are rank≤1, zero outside distinct-row endpoints and all-entry nonvanishing.; AddBoxesDistinctRows: Relation on unnormalized diagrams: g_i−f_i∈{0,1}, Σ_i(g_i−f_i)=k and both tuples decreasing; common-shift normalization only after enumerating successors. (hard)
§3: Remark. The converse also holds: Pinned source/provenance obstacle: §3: Remark. The converse also holds (hard)
§8: We need the Glimm–Jaffe–Nelson commutator theorem: Pinned source/provenance obstacle: §8: We need the Glimm–Jaffe–Nelson commutator theorem (hard)
§10: von Neumann’s double commutant theorem states: Pinned source/provenance obstacle: §10: von Neumann’s double commutant theorem states (hard)
§12: The main theorem of Tomita–Takesaki asserts: Pinned source/provenance obstacle: §12: The main theorem of Tomita–Takesaki asserts (hard)
§17: Theorem B is a weaker version: Pinned source/provenance obstacle: §17: Theorem B is a weaker version (hard)

Selected references

Operator Algebras and Conformal Field Theory III. Fusion of positive energy representations of LSU(N) using bounded operators, arXiv:math/9806031v1, https://arxiv.org/abs/math/9806031v1

12 thms1 active userReviewed

Quantum Information·Captain: Gohan

Derived Algebraic Geometry II: Noncommutative AlgebraResearch Paper

Motivation

In this paper, we present an infinity-categorical version of the theory of monoidal categories. We show that the infinity category of spectra admits an essentially unique monoidal structure (such that the tensor product preserves colimits in each variable), and thereby recover the classical smash-product operation on spectra. We develop a general theory of algebras in a monoidal infinity category, which we use to (re)prove some basic results in the theory of associative ring spectra. We also develop an infinity-categorical theory of monads, and prove a version of the Barr-Beck theorem.

This mission is the statement-level formalization of Derived Algebraic Geometry II: Noncommutative Algebra (arXiv:math/0702299v5). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Finite-presentation closure over a left coherent ring (Lemma 4.7.17, PDF p. 164). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

Example 1.1.5: coCartesian monoidal envelopes, Segal fiber equivalences, and coherent algebra/functor section categories (hard)
Remark 1.1.6: coCartesian monoidal envelopes, Segal fiber equivalences, and coherent algebra/functor section categories (hard)
Remark 1.1.13: coCartesian monoidal envelopes, Segal fiber equivalences, and coherent algebra/functor section categories (hard)
Remark 1.1.16: coCartesian monoidal envelopes, Segal fiber equivalences, and coherent algebra/functor section categories (hard)
Remark 1.1.18: coCartesian monoidal envelopes, Segal fiber equivalences, and coherent algebra/functor section categories (hard)
Proposition 1.2.4: interval-diagram Cartesian monoidal envelopes and weak/lax Cartesian section categories (hard)
Proposition 1.2.8: interval-diagram Cartesian monoidal envelopes and weak/lax Cartesian section categories (hard)
Proposition 1.2.9: interval-diagram Cartesian monoidal envelopes and weak/lax Cartesian section categories (hard)
Corollary 1.2.10: interval-diagram Cartesian monoidal envelopes and weak/lax Cartesian section categories (hard)
Proposition 1.2.14: interval-diagram Cartesian monoidal envelopes and weak/lax Cartesian section categories (hard)
Remark 1.2.15: interval-diagram Cartesian monoidal envelopes and weak/lax Cartesian section categories (hard)
Remark 1.2.16: interval-diagram Cartesian monoidal envelopes and weak/lax Cartesian section categories (hard)
Remark 1.2.17: interval-diagram Cartesian monoidal envelopes and weak/lax Cartesian section categories (hard)
Proposition 1.3.1: coherent localization/colocalization, tensor compatibility, and induced monoidal subcategory fibrations (hard)
Remark 1.3.3: coherent localization/colocalization, tensor compatibility, and induced monoidal subcategory fibrations (hard)
Example 1.3.7: coherent localization/colocalization, tensor compatibility, and induced monoidal subcategory fibrations (hard)
Lemma 1.3.8: coherent localization/colocalization, tensor compatibility, and induced monoidal subcategory fibrations (hard)
Proposition 1.3.9: coherent localization/colocalization, tensor compatibility, and induced monoidal subcategory fibrations (hard)
Proposition 1.3.12: coherent localization/colocalization, tensor compatibility, and induced monoidal subcategory fibrations (hard)
Theorem 1.4.2: coherent free-algebra section categories, relative Kan extensions, and canonical tensor-power coproduct maps (hard)
Proposition 1.4.3: coherent free-algebra section categories, relative Kan extensions, and canonical tensor-power coproduct maps (hard)
Lemma 1.4.7: coherent free-algebra section categories, relative Kan extensions, and canonical tensor-power coproduct maps (hard)
Lemma 1.4.11: coherent free-algebra section categories, relative Kan extensions, and canonical tensor-power coproduct maps (hard)
Lemma 1.4.15: coherent free-algebra section categories, relative Kan extensions, and canonical tensor-power coproduct maps (hard)
Lemma 1.4.18: marked equivalence, marked slice C/p, and induced slice-restriction categorical equivalence (hard)
Lemma 1.4.19: quasicategorical localization unit, simplicial over-slice, and slice restriction (hard)
Lemma 1.4.20: coherent free-algebra section categories, relative Kan extensions, and canonical tensor-power coproduct maps (hard)
Lemma 1.4.23: coherent free-algebra section categories, relative Kan extensions, and canonical tensor-power coproduct maps (hard)
Remark 1.4.24: coherent free-algebra section categories, relative Kan extensions, and canonical tensor-power coproduct maps (hard)
Lemma 1.5.1: coherent algebra/lax-functor categories and absolute/relative infinity-categorical limits and colimits (hard)
Proposition 1.5.2: coherent algebra/lax-functor categories and absolute/relative infinity-categorical limits and colimits (hard)
Corollary 1.5.3: coherent algebra/lax-functor categories and absolute/relative infinity-categorical limits and colimits (hard)
Corollary 1.5.4: coherent algebra/lax-functor categories and absolute/relative infinity-categorical limits and colimits (hard)
Corollary 1.5.5: coherent algebra/lax-functor categories and absolute/relative infinity-categorical limits and colimits (hard)
Remark 1.5.6: coherent algebra/lax-functor categories and absolute/relative infinity-categorical limits and colimits (hard)
Lemma 1.5.8: coherent algebra/lax-functor categories and absolute/relative infinity-categorical limits and colimits (hard)
Lemma 1.5.9: coCartesian fibrations over arbitrary simplicial bases and fiberwise colimit cones in the section quasicategory (hard)
Proposition 1.5.10: coherent algebra/lax-functor categories and absolute/relative infinity-categorical limits and colimits (hard)
Corollary 1.5.11: coherent algebra/lax-functor categories and absolute/relative infinity-categorical limits and colimits (hard)
Proposition 1.5.12: coherent algebra/lax-functor categories and absolute/relative infinity-categorical limits and colimits (hard)
Corollary 1.5.13: coherent algebra/lax-functor categories and absolute/relative infinity-categorical limits and colimits (hard)
Lemma 1.5.14: coherent algebra/lax-functor categories and absolute/relative infinity-categorical limits and colimits (hard)
Proposition 1.5.15: coherent algebra/lax-functor categories and absolute/relative infinity-categorical limits and colimits (hard)
Proposition 1.6.3: fibrant simplicial monoidal envelope and coherent nerve with the Segal/coCartesian conditions (hard)
Proposition 1.6.5: compatible simplicial monoidal model presentations and their fibrant-cofibrant coherent nerves (hard)
Example 1.6.6: compatible simplicial monoidal model presentations and their fibrant-cofibrant coherent nerves (hard)
Remark 1.6.9: compatible simplicial monoidal model presentations and their fibrant-cofibrant coherent nerves (hard)
Lemma 1.6.13: ordinary monoidal model compatibility and the saturated tensor-generated morphism class Ubar (hard)
Proposition 1.6.14: ordinary combinatorial algebra-model transfer with an optional compatible simplicial enrichment (hard)
Lemma 1.6.15: compatible simplicial monoidal model presentations and their fibrant-cofibrant coherent nerves (hard)
Theorem 1.6.16: compatible simplicial monoidal model presentations and their fibrant-cofibrant coherent nerves (hard)
Example 1.6.17: compatible simplicial monoidal model presentations and their fibrant-cofibrant coherent nerves (hard)
Example 1.6.18: compatible simplicial monoidal model presentations and their fibrant-cofibrant coherent nerves (hard)
Example 1.6.19: compatible simplicial monoidal model presentations and their fibrant-cofibrant coherent nerves (hard)
Remark 1.6.20: compatible simplicial monoidal model presentations and their fibrant-cofibrant coherent nerves (hard)
Proposition 1.7.7: LinStar-indexed Segal monoidal and Segal algebra section categories with pullback along psi (hard)
Remark 1.7.11: LinStar-indexed Segal monoidal and Segal algebra section categories with pullback along psi (hard)
Proposition 1.7.15: LinStar-indexed Segal monoidal and Segal algebra section categories with pullback along psi (hard)
Example 2.1.3: coherent left-tensor actions and mapping/exponential objects with representing evaluation (hard)
Remark 2.1.10: coherent left-tensor actions and mapping/exponential objects with representing evaluation (hard)
Proposition 2.1.12: coherent left-tensor actions and mapping/exponential objects with representing evaluation (hard)
Lemma 2.1.13: coherent left-tensor actions and mapping/exponential objects with representing evaluation (hard)
Lemma 2.1.16: coherent left-tensor actions and mapping/exponential objects with representing evaluation (hard)
Remark 2.2.11: homotopies of coherent nonunital multiplication/unit maps (hard)
Proposition 2.2.16: nonunital/quasi-unital coherent algebra and module section categories (hard)
Lemma 2.3.1: relative p-limit cones and exponential simplicial-set adjunction (hard)
Proposition 2.3.2: relative limit and Kan-extension universal properties for coherent module section categories (hard)
Corollary 2.3.3: relative limit and Kan-extension universal properties for coherent module section categories (hard)
Remark 2.3.4: relative limit and Kan-extension universal properties for coherent module section categories (hard)
Corollary 2.3.5: relative limit and Kan-extension universal properties for coherent module section categories (hard)
Proposition 2.3.6: relative limit and Kan-extension universal properties for coherent module section categories (hard)
Corollary 2.3.7: relative limit and Kan-extension universal properties for coherent module section categories (hard)
Corollary 2.3.8: relative limit and Kan-extension universal properties for coherent module section categories (hard)
Remark 2.3.9: relative limit and Kan-extension universal properties for coherent module section categories (hard)
Lemma 2.3.10: right fibrations, full sub-quasicategories, and relative left Kan extensions (hard)
Lemma 2.3.11: dependent exponential over S, categorical fibration, and relative left Kan extensions (hard)
Proposition 2.4.2: coherent free-module adjunction, canonical action comparison, and mapping-space equivalence (hard)
Corollary 2.4.3: coherent free-module adjunction, canonical action comparison, and mapping-space equivalence (hard)
Corollary 2.4.4: coherent free-module adjunction, canonical action comparison, and mapping-space equivalence (hard)
Proposition 2.5.1: ordinary combinatorial model transfer to strict modules and both Quillen properties of the forgetful functor (hard)
Remark 2.5.2: ordinary left-Quillen monad algebra category and the transferred model structure (hard)
Remark 2.5.3: precise scope of the noncofibrant-algebra generalization, separating transferred model existence from left-Quillen preservation (source-ambiguity)
Theorem 2.5.4: transferred module model structures, Quillen adjoints, and coherent module comparison (hard)
Proposition 2.6.2: marked coCartesian model diagrams, coherent action categories, and unit evaluation (hard)
Proposition 2.6.4: marked coCartesian model diagrams, coherent action categories, and unit evaluation (hard)
Corollary 2.6.6: marked coCartesian model diagrams, coherent action categories, and unit evaluation (hard)
Corollary 2.6.7: marked coCartesian model diagrams, coherent action categories, and unit evaluation (hard)
Proposition 2.7.2: the constructed interval-star action envelope C[M], coherent modules, and right-fibration recognition (hard)
Proposition 2.7.3: the constructed interval-star action envelope C[M], coherent modules, and right-fibration recognition (hard)
Corollary 2.7.5: the constructed interval-star action envelope C[M], coherent modules, and right-fibration recognition (hard)
Proposition 2.7.6: the constructed interval-star action envelope C[M], coherent modules, and right-fibration recognition (hard)
Proposition 2.7.7: the constructed interval-star action envelope C[M], coherent modules, and right-fibration recognition (hard)
Corollary 2.7.8: the constructed interval-star action envelope C[M], coherent modules, and right-fibration recognition (hard)
Corollary 2.7.9: the constructed interval-star action envelope C[M], coherent modules, and right-fibration recognition (hard)
Remark 2.7.10: the constructed interval-star action envelope C[M], coherent modules, and right-fibration recognition (hard)
Lemma 2.7.11: fiberwise right fibrations between coCartesian fibrations and induced section map (hard)
Lemma 2.7.12: strict simplicial pullback and relative limit cones under a coCartesian fibration (hard)
Lemma 2.7.13: the constructed interval-star action envelope C[M], coherent modules, and right-fibration recognition (hard)
Lemma 2.7.14: categorical fibrations/equivalences and right fibrations of simplicial sets (hard)
Theorem 2.8.1: quasi-unital morphism subcategories and actual unital-to-nonunital restriction maps (hard)
Lemma 2.8.2: quasi-unital morphism subcategories and actual unital-to-nonunital restriction maps (hard)
Corollary 2.8.5: quasi-unital morphism subcategories and actual unital-to-nonunital restriction maps (hard)
Lemma 3.1.4: relative nerves of simplicial-set diagrams and the specific endofunctor/universal-action envelopes (hard)
Proposition 3.1.5: relative nerves of simplicial-set diagrams and the specific endofunctor/universal-action envelopes (hard)
Proposition 3.1.7: relative nerves of simplicial-set diagrams and the specific endofunctor/universal-action envelopes (hard)
Remark 3.1.10: relative nerves of simplicial-set diagrams and the specific endofunctor/universal-action envelopes (hard)
Lemma 3.2.9: two-colored coherent adjunction data with extracted functors, unit, and counit (hard)
Theorem 3.2.10: two-colored coherent adjunction data with extracted functors, unit, and counit (hard)
Proposition 3.3.5: pointed colored endofunctor envelopes, pointed/unpointed ADat, and strict fibers (hard)
Corollary 3.3.6: pointed colored endofunctor envelopes, pointed/unpointed ADat, and strict fibers (hard)
Lemma 3.3.7: pointed colored endofunctor envelopes, pointed/unpointed ADat, and strict fibers (hard)
Theorem 3.4.5: coherent ADat-induced monad/module comparison, G-split augmented diagrams, and geometric realization (hard)
Remark 3.4.6: coherent ADat-induced monad/module comparison, G-split augmented diagrams, and geometric realization (hard)
Corollary 3.4.8: coherent ADat-induced monad/module comparison, G-split augmented diagrams, and geometric realization (hard)
Proposition 3.4.9: coherent ADat-induced monad/module comparison, G-split augmented diagrams, and geometric realization (hard)
Remark 3.4.10: coherent ADat-induced monad/module comparison, G-split augmented diagrams, and geometric realization (hard)
Corollary 3.4.11: coherent ADat-induced monad/module comparison, G-split augmented diagrams, and geometric realization (hard)
Corollary 3.4.12: coherent ADat-induced monad/module comparison, G-split augmented diagrams, and geometric realization (hard)
Lemma 3.4.13: coherent ADat-induced monad/module comparison, G-split augmented diagrams, and geometric realization (hard)
Proposition 3.5.4: constructed colored I0-I3/J/M section diagrams and relative Kan-extension conditions (hard)
Proposition 3.5.5: constructed colored I0-I3/J/M section diagrams and relative Kan-extension conditions (hard)
Proposition 3.5.6: constructed colored I0-I3/J/M section diagrams and relative Kan-extension conditions (hard)
Lemma 3.5.8: constructed colored I0-I3/J/M section diagrams and relative Kan-extension conditions (hard)
Lemma 3.5.9: constructed colored I0-I3/J/M section diagrams and relative Kan-extension conditions (hard)
Lemma 3.5.10: constructed colored I0-I3/J/M section diagrams and relative Kan-extension conditions (hard)
Lemma 3.5.12: constructed colored I0-I3/J/M section diagrams and relative Kan-extension conditions (hard)
Lemma 3.5.13: constructed colored I0-I3/J/M section diagrams and relative Kan-extension conditions (hard)
Lemma 3.5.14: constructed colored I0-I3/J/M section diagrams and relative Kan-extension conditions (hard)
Lemma 3.5.15: constructed colored I0-I3/J/M section diagrams and relative Kan-extension conditions (hard)
Lemma 3.5.16: weak contractibility and relative colimit cones of coCartesian diagrams (hard)
Lemma 3.5.18: constructed colored I0-I3/J/M section diagrams and relative Kan-extension conditions (hard)
Lemma 3.5.20: constructed colored I0-I3/J/M section diagrams and relative Kan-extension conditions (hard)
Lemma 3.5.24: right-anodyne inclusions, right cone, pushout product, and Joyal categorical fibrations (hard)
Lemma 4.1.4: multilinear tensor product of presentable quasicategories and its functor-category universal property (hard)
Lemma 4.1.5: multilinear tensor product of presentable quasicategories and its functor-category universal property (hard)
Remark 4.1.6: multilinear tensor product of presentable quasicategories and its functor-category universal property (hard)
Proposition 4.1.7: multilinear tensor product of presentable quasicategories and its functor-category universal property (hard)
Remark 4.1.8: multilinear tensor product of presentable quasicategories and its functor-category universal property (hard)
Example 4.1.9: multilinear tensor product of presentable quasicategories and its functor-category universal property (hard)
Example 4.1.10: multilinear tensor product of presentable quasicategories and its functor-category universal property (hard)
Example 4.1.11: multilinear tensor product of presentable quasicategories and its functor-category universal property (hard)
Example 4.1.12: multilinear tensor product of presentable quasicategories and its functor-category universal property (hard)
Proposition 4.2.3: spectra/finite-spectra smash products, stabilization, and coherent presentable actions (hard)
Corollary 4.2.6: spectra/finite-spectra smash products, stabilization, and coherent presentable actions (hard)
Proposition 4.2.7: spectra/finite-spectra smash products, stabilization, and coherent presentable actions (hard)
Remark 4.2.8: spectra/finite-spectra smash products, stabilization, and coherent presentable actions (hard)
Remark 4.2.9: spectra/finite-spectra smash products, stabilization, and coherent presentable actions (hard)
Proposition 4.2.10: spectra/finite-spectra smash products, stabilization, and coherent presentable actions (hard)
Example 4.3.2: A-infinity rings as coherent algebras in spectra and their categorical/spectral truncations (hard)
Remark 4.3.4: A-infinity rings as coherent algebras in spectra and their categorical/spectral truncations (hard)
Lemma 4.3.5: A-infinity rings as coherent algebras in spectra and their categorical/spectral truncations (hard)
Proposition 4.3.8: A-infinity rings as coherent algebras in spectra and their categorical/spectral truncations (hard)
Proposition 4.3.9: A-infinity rings as coherent algebras in spectra and their categorical/spectral truncations (hard)
Remark 4.3.10: A-infinity rings as coherent algebras in spectra and their categorical/spectral truncations (hard)
Proposition 4.3.11: A-infinity rings as coherent algebras in spectra and their categorical/spectral truncations (hard)
Proposition 4.3.13: A-infinity rings as coherent algebras in spectra and their categorical/spectral truncations (hard)
Proposition 4.4.3: stable spectral module categories, their t-structures, and canonical derived-heart comparisons (hard)
Proposition 4.4.6: stable spectral module categories, their t-structures, and canonical derived-heart comparisons (hard)
Proposition 4.4.7: stable spectral module categories, their t-structures, and canonical derived-heart comparisons (hard)
Remark 4.4.8: stable spectral module categories, their t-structures, and canonical derived-heart comparisons (hard)
Theorem 4.4.9: stable spectral module categories, their t-structures, and canonical derived-heart comparisons (hard)
Remark 4.4.10: stable spectral module categories, their t-structures, and canonical derived-heart comparisons (hard)
Proposition 4.5.4: coherent balanced pairings and the full augmented two-sided bar realization (hard)
Proposition 4.5.8: coherent balanced pairings and the full augmented two-sided bar realization (hard)
Corollary 4.5.9: coherent balanced pairings and the full augmented two-sided bar realization (hard)
Proposition 4.5.10: coherent balanced pairings and the full augmented two-sided bar realization (hard)
Proposition 4.5.11: coherent balanced pairings and the full augmented two-sided bar realization (hard)
Lemma 4.5.12: coherent balanced pairings and the full augmented two-sided bar realization (hard)
Proposition 4.5.13: coherent balanced pairings and the full augmented two-sided bar realization (hard)
Corollary 4.5.14: coherent balanced pairings and the full augmented two-sided bar realization (hard)
Proposition 4.6.6: spectral flat/projective modules, graded Tor spectral sequences, and canonical spectral base change (hard)
Corollary 4.6.8: spectral flat/projective modules, graded Tor spectral sequences, and canonical spectral base change (hard)
Remark 4.6.11: spectral flat/projective modules, graded Tor spectral sequences, and canonical spectral base change (hard)
Proposition 4.6.13: spectral flat/projective modules, graded Tor spectral sequences, and canonical spectral base change (hard)
Remark 4.6.14: spectral flat/projective modules, graded Tor spectral sequences, and canonical spectral base change (hard)
Corollary 4.6.15: spectral flat/projective modules, graded Tor spectral sequences, and canonical spectral base change (hard)
Corollary 4.6.16: spectral flat/projective modules, graded Tor spectral sequences, and canonical spectral base change (hard)
Corollary 4.6.17: spectral flat/projective modules, graded Tor spectral sequences, and canonical spectral base change (hard)
Lemma 4.6.18: spectral flat/projective modules, graded Tor spectral sequences, and canonical spectral base change (hard)
Theorem 4.6.19: spectral flat/projective modules, graded Tor spectral sequences, and canonical spectral base change (hard)
Proposition 4.6.20: spectral flat/projective modules, graded Tor spectral sequences, and canonical spectral base change (hard)
Lemma 4.6.21: spectral flat/projective modules, graded Tor spectral sequences, and canonical spectral base change (hard)
Proposition 4.6.22: spectral flat/projective modules, graded Tor spectral sequences, and canonical spectral base change (hard)
Proposition 4.7.2: coherent perfect/almost-perfect spectral modules, duality, and Tor-amplitude (hard)
Proposition 4.7.3: coherent perfect/almost-perfect spectral modules, duality, and Tor-amplitude (hard)
Remark 4.7.4: coherent perfect/almost-perfect spectral modules, duality, and Tor-amplitude (hard)
Proposition 4.7.5: coherent perfect/almost-perfect spectral modules, duality, and Tor-amplitude (hard)
Corollary 4.7.6: coherent perfect/almost-perfect spectral modules, duality, and Tor-amplitude (hard)
Lemma 4.7.7: space-valued quasicategorical Yoneda embeddings and perfect-pairing image criteria (hard)
Proposition 4.7.8: coherent perfect/almost-perfect spectral modules, duality, and Tor-amplitude (hard)
Remark 4.7.9: coherent perfect/almost-perfect spectral modules, duality, and Tor-amplitude (hard)
Lemma 4.7.11: compactness to categorical truncation order and induced filtered-colimit functors (hard)
Proposition 4.7.13: coherent perfect/almost-perfect spectral modules, duality, and Tor-amplitude (hard)
Corollary 4.7.14: coherent perfect/almost-perfect spectral modules, duality, and Tor-amplitude (hard)
Proposition 4.7.19: coherent perfect/almost-perfect spectral modules, duality, and Tor-amplitude (hard)
Proposition 4.7.20: coherent perfect/almost-perfect spectral modules, duality, and Tor-amplitude (hard)
Remark 4.7.21: coherent perfect/almost-perfect spectral modules, duality, and Tor-amplitude (hard)
Proposition 4.7.22: coherent perfect/almost-perfect spectral modules, duality, and Tor-amplitude (hard)
Proposition 4.7.25: coherent perfect/almost-perfect spectral modules, duality, and Tor-amplitude (hard)
Remark 4.7.26: coherent perfect/almost-perfect spectral modules, duality, and Tor-amplitude (hard)
Example 4.7.27: coherent perfect/almost-perfect spectral modules, duality, and Tor-amplitude (hard)

Selected references

Derived Algebraic Geometry II: Noncommutative Algebra, arXiv:math/0702299v5, https://arxiv.org/abs/math/0702299v5

2 thms1 active userReviewed

Quantum Information·Captain: Gohan

Entanglement entropy of two disjoint intervals in conformal field theory IIResearch Paper

Motivation

We continue the study of the entanglement entropy of two disjoint intervals in conformal field theories that we started in J. Stat. Mech. (2009) P11001. We compute Trρ_A^n for any integer n for the Ising universality class and the final result is expressed as a sum of Riemann-Siegel theta functions. These predictions are checked against existing numerical data. We provide a systematic method that gives the full asymptotic expansion of the scaling function for small four-point ratio (i.e. short intervals). These formulas are compared with the direct expansion of the full results for free compactified boson and Ising model. We finally provide the analytic continuation of the first term in this expansion in a completely analytic form.

This mission is the statement-level formalization of Entanglement entropy of two disjoint intervals in conformal field theory II (arXiv:1011.5482v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Characteristic theta inversion with the analytic Gaussian branch (§4.1, equation (53), PDF p. 12). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

Abstract; §2.2 equation (11): all-integer Ising moments: Independently constructed critical Ising replica moment and its scaling normalization (hard)
§3 equations (16)–(22): general short-interval expansion: Complete local-field/state expansion on replica surfaces in arbitrary fixed backgrounds (hard)
§3 equation (25), specializations (29)–(30): Independent interval coefficients and primary conformal covariance (hard)
§3 identity fusion, even spin, integer sector support: Constructed fusion-to-identity block and replica-sector coefficients (hard)
§2.1 simple-zero assertion for analytically continued sectors: Canonical analytic continuation of every sector with controlled zero multiplicities (source-ambiguity)
§3/§3.1 equations (28),(31)–(32): local energy correction: Exclusion of competing order-ℓ² primary sectors in the claimed generality (source-ambiguity)
§3.1 equation (34): boundary primary term: Actual boundary one-point functions and sector extraction in the normalized moment (hard)
§3.2 equations (35)–(39), summary (9): Actual two-interval partition ratio and full ordered quasiprimary expansion (hard)
§3.2.1 equation (40): Stress-sector extraction from actual replica moments (hard)
§3.2.2 equations (41),(43)–(44), summary (13): Independent pair-sector coefficient, field dimensions and multiplicity (hard)
§3.2.2–3.2.3 equations (42)–(43),(45): Consistent rotation phase, complex-power branches, and replica divisibility statement (source-ambiguity)
§3.2.3 equations (30),(45)–(46): Actual OPE coefficient and replica three-primary sector (hard)
§3.2.4 equation (50): Normalized compact-boson vertex fields, correlators and actual interval d (hard)
§4.1 crossing symmetry: Independent Ising F_n tied to actual replica geometry (hard)
§4.1 equation (56): Specified transformation matrix and consistent congruence in (55)–(56) (source-ambiguity)
§5.1 equation (67): Actual compact-boson moments and fixed-theory scaling function (hard)
§5.3 equations (83)–(84): Independent Ising F_n and asymptotic sector identification (hard)
§5.4 equations (94)–(96): Independent compact-boson F_n and its four-primary asymptotic coefficient (hard)
§5.5 equations (99)–(112): Independent Ising F_n and normed four-spin sector (hard)
§5 equation (57): Physical sector continuation and differentiable uniform remainder near n=1 (source-ambiguity)
§2.3/§6 equations (14)–(15),(113)–(128): Physical Carlson-selected continuation, cutoff normalization and valid integral interchange (source-ambiguity)
§6.1 equation (129): Actual near-one replica continuation with differentiated O(x^(1/2)) remainder (source-ambiguity)
Appendix A equations (A.1)–(A.2): Slit-plane conformal modulus, sewn cylinder partition function and fixed UV convention (hard)
Appendix A equations (A.5)–(A.10): Compatible infinite-dimensional half-cylinder factorization and trace-class sewing (hard)
Appendix A equations (A.11)–(A.12): Normalized degenerate operator basis and necessary adjoint mixing convention (source-ambiguity)
Appendix A equations (A.13)–(A.14): Fixed UV normalization and compatible W-dependent infinite half-cylinder construction (source-ambiguity)
Appendix A equation (A.15): Exact normalized primary sewing trace proportionality (source-ambiguity)

Selected references

Entanglement entropy of two disjoint intervals in conformal field theory II, arXiv:1011.5482v1, https://arxiv.org/abs/1011.5482v1

6 thms1 active userReviewed

Quantum Information·Captain: Gohan

Twisted K-theory and K-theory of bundle gerbesResearch Paper

Motivation

In this note we introduce the notion of bundle gerbe K-theory and investigate the relation to twisted K-theory. We provide some examples. Possible applications of bundle gerbe K-theory to the classification of D-brane charges in non-trivial backgrounds are discussed.

This mission is the statement-level formalization of Twisted K-theory and K-theory of bundle gerbes (arXiv:hep-th/0106194v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Finite-codimension tensor avoidance (Lemma 6.2, PDF p. 10). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

§1: torsion and infinite-rank comparisons (paper seed): Finite-module Grothendieck K, Fredholm-section K, and UK-reduced lifting-gerbe module completion (hard)
Theorem 2.1: vanishing Dixmier–Douady obstruction: LocallySplitMap, FibrePowers, BundleGerbe, GerbeTrivialisation, IntegralCechCohomology, DDClass (hard)
Theorem 2.2: dual and tensor Dixmier–Douady classes: LocallySplitMap, FibrePowers, BundleGerbe, GerbeDual, GerbeTensor, IntegralCechCohomology, DDClass (hard)
§2.1: naturality of Dixmier–Douady class: Integral Cech DD cocycle and smooth gerbe pullback along a covering fibre map (hard)
§2.2: lifting-gerbe Dixmier–Douady obstruction: IntegralCechCohomology, DDClass, CentralExtension, PrincipalBundle, LiftingGerbe, LiftOfPrincipalBundle (hard)
Proposition 3.2: stable isomorphism iff equal class: IntegralCechCohomology, DDClass, StableGerbeIso (hard)
Theorem 3.3: classification by integral H^3: Stable-gerbe class quotient and the constructed integral DD class map (hard)
§3: morphisms induce stable isomorphisms: GerbeMorphism, StableGerbeIso (hard)
§3: composition of stable isomorphisms: GerbeTrivialisation, StableGerbeIso, StableComposition (hard)
Proposition 4.1: rank annihilates the twisting class: Finite-rank Hermitian gerbe modules, determinant action and integral DD class (hard)
§4: effective descent of Hermitian vector bundles: HermitianBundle, BundleDescentData (hard)
Proposition 4.2: modules for a trivial gerbe: Chosen-trivialisation descent map on finite module isomorphism classes (hard)
Proposition 4.3: stable transport of modules: Stable-isomorphism transport by descent of K* tensor E (hard)
Proposition 4.4: projectivisation modulo line bundles: FiniteModule, FiniteModuleClasses, VectorBundleClasses, LineBundleClasses, ProjectiveBundleClasses, Projectivisation (source-ambiguity)
Proposition 5.1: stable invariance of bundle-gerbe K: Grothendieck completion of the chosen stable module transport (hard)
Proposition 5.2: four bundle-gerbe K operations: Four constructed operations on gerbe-module Grothendieck groups (hard)
§6.1: Fredholm sections, equivariant maps and ordinary K: FredholmSpace, AssociatedFredholmBundle, EquivariantHomotopyClasses, TwistedK (hard)
§6.2: finite-dimensional projective reduction for torsion: IntegralCechCohomology, DDClass, PrincipalBundle, FiniteProjectiveReduction (hard)
Proposition 6.3: equivariant finite bundle embedding: HermitianBundle, FiniteModule, FiniteProjectiveReduction, UnitaryRepresentation, EquivariantBundleEmbedding (hard)
Proposition 6.4: torsion twisted K comparison: Norm-Fredholm section homotopy K and the equivariant index comparison (hard)
§6.2: asserted equivariant-K preimage description: EquivariantK, CentralWeightOnePart, RepresentationRing (source-ambiguity)
§6.3: compatible connections and descended closed characteristic forms: Smooth module connections, invariant-polynomial evaluation and form descent (hard)
§6.3: rational Chern-character claim: GrothendieckCompletion, BundleGerbeK, Curving, ChernWeilForm, RationalCohomology (source-ambiguity)
Proposition 7.1: uniqueness of unrestricted Hilbert modules: Full U(H) Hilbert-module isomorphism classes and their direct-sum completion (hard)
Proposition 7.2: five descriptions of reduced twisted K: PrincipalBundle, EquivariantHomotopyClasses, BUK, ReducedTwistedK, CovariantUKBundle, SemidirectBundle (source-ambiguity)
Note 7.1: Fredholm index annihilates the twist: Integer-index Fredholm sections and determinant gerbe action (hard)
Proposition 7.3: reduced K and UK module classes: Fixed-background UK reductions, covariant bundles and BUK section classes (hard)
Proposition 7.4: UK Grothendieck group comparison: Direct sum and inverses of UK-reduced module classes and their completion (hard)
Note 7.2(1): equivariant replacement and U1 modules: PU(H)-equivariant homotopy replacement and trace-ideal U1 module model (hard)
§7.2: local covariant UK cocycle: Smooth covariant UK bundle local sections and their induced transitions (hard)
§8 opening: canonical integral H^3 into K^1: IntegralCechCohomology, OddK, ThirdOddChernCharacter, StableUnitaryGroup (source-ambiguity)
§8.1.1: ordinary and twisted six-term Mayer–Vietoris: OrdinaryK, TopologicalKGroups, CompactOperatorBundle, TwistedMayerVietoris (hard)
§8.1: ordinary K-groups of S^3: Independent ordinary complex K0/K1 functors on the actual three-sphere (hard)
§8.1: nonzero-twist K-groups of S^3: OrdinaryK, TopologicalKGroups, IntegralGenerator (hard)
§8.1.2: obstruction to extending the twist over B^4: Restriction of norm-PU(H) principal bundles from B4 to its boundary S3 (hard)
§8.2: twisted K of S^1×S^2, including zero twist: Twisted K functors of S1 times S2 and its chosen integral H3 generator (hard)
§8.3: ordinary K of real projective spaces (8.14): OrdinaryK, TopologicalKGroups, RealProjectiveSpace, ReducedOrdinaryK (hard)
§8.3: nonzero-twist K of RP^3: Twisted K0/K1 on real projective three-space with integral twist (hard)
§8.3: equivariant K of the two-point complement: Compact-support equivariant complex K for the inherited antipodal complement action (hard)
§8.4: ordinary K of prime lens spaces (8.19): OrdinaryK, TopologicalKGroups, LensSpace (hard)
§8.4: nonzero-twist K of prime lens spaces (8.20): Twisted complex K on the free cyclic lens-space quotient (hard)
§8.5: kernel and image of the twisted d3 (8.21–8.22): Integral SU(n) cohomology generators and the actual twisted AHSS d3 (hard)
§8.5: claimed spectral-sequence term (8.23): After-d3 cohomology of the actual integral SU(n) twisted AHSS (hard)
§8.5: SU(2) twisted K and collapse (8.24): Actual SU(2) twisted AHSS collapse and twisted K groups (hard)
§8.5: claimed higher differentials for SU(n), n>2: A twist-qualified nonvanishing statement for the actual integral Atiyah-Hirzebruch spectral sequence computing complex twisted K-theory of SU(n): specify n > 2, the integer twist [H] = N c3, the additional conditions on N, and a higher differential d_r with r > 3 and a bidegree on which it is nonzero. This requires the constructed spectral-sequence pages, differentials and integral exterior generators, rather than an arbitrary differential supplied as data. PDF p. 20 gives no such twist conditions or differential degree. Its equation (8.23) makes every after-d3 group zero when N = 1, so all later differentials are zero in that allowed case; n > 2 alone cannot imply nonvanishing. Reference [14] is unpublished and the precise qualified result in [22] has not been certified. The missing interface is both the concrete twisted-K spectral sequence and the precise qualified cited theorem, not merely an unimplemented name TwistedAHSS. (source-ambiguity)
§9.2: unitary topology, contractibility and projective Lie group: IntegralCechCohomology, DDClass, PrincipalBundle, NormUnitaryGroup, ProjectiveUnitaryGroup (hard)
§9.3: fixed-form twisted cohomology and change of representative: Smooth differential-form algebra, parity complex and its concrete induced maps (hard)
§9.3: choice-free cohomology attached to an integral class: BFieldChainMap, IntegralClassTwistedCohomology, ConnectionCurvingQuadruple (source-ambiguity)
§9.4: existence of compatible relative trace-class module connections: U1-reduced Hilbert modules and admissible relative trace-class connection pairs (hard)
Proposition 9.1: relative Chern form and connection independence: Relative trace exponential form, descent, twisted closure and connection comparison (hard)
§9.4: change of gerbe connection and curving: Specified gerbe-connection and curving changes of the actual relative Chern form (hard)
§9.4: additivity of the relative character forms: U1 block direct sum, sum connections and relative Chern forms (hard)
§9.4: class-level functorial Chern-character proposal: GrothendieckCompletion, BUK, ReducedTwistedK, U1Module, U1ModuleK, IntegralClassTwistedCohomology, RelativeChernForm (source-ambiguity)
§9.1 and §9.4: characterisation of the twisted Chern character: BUK, ReducedTwistedK, IntegralClassTwistedCohomology, ChernCharacterAxioms (source-ambiguity)
§9.4: deferred compatibility with the K-module structure: OrdinaryK, BUK, ReducedTwistedK, IntegralClassTwistedCohomology, ChernCharacterAxioms (source-ambiguity)
§10: convolution C*-algebra associated to some bundle gerbes: CompactOperatorBundle, MeasuredGerbeFibres, GerbeConvolutionAlgebra, ContinuousTraceAlgebraK (source-ambiguity)
§10: finite-dimensional connected-fibre obstruction: LocallySplitMap, FibrePowers, BundleGerbe, IntegralCechCohomology, DDClass, FiniteDimensionalGerbeFibre (source-ambiguity)
Errata to [5]: odd twisted K as equivariant UK maps: Independent odd twisted K and equivariant UK homotopy classes on fixed Y (hard)
Errata to [5]: torsion descriptions and unitisation: CompactOperatorBundle, UnitisedSectionAlgebra, FlatClassifyingBundle (source-ambiguity)
§6.2: equivariant unitary contractibility: EquivariantHomotopyClasses, NormUnitaryGroup (hard)
§8.1: Bott periodicity used for Euclidean complements: Concrete degree-zero and degree-one complex topological K-groups with their compact-support convention for the Euclidean complement: K_c^j(R^4) = K_j(C_0(R^4)) (equivalently reduced K of the one-point compactification S^4), and ordinary K^j(B^4) = K_j(C(B^4)) for the closed ball, for j = 0, 1. The nonunital C_0 model must use unitisation and the kernel of the induced map to the scalar algebra, rather than ordinary unreduced K of contractible R^4. Needed are the Bott periodicity comparison for these independently constructed groups and homotopy invariance for the compact ball, yielding additive isomorphisms K_c^0(R^4) with Z and K^0(B^4) with Z and trivial degree-one groups in both cases, exactly as invoked on PDF p. 18. No equivariant action is required for this particular node. Neither these concrete functors nor an exact accepted declaration of the cited Bott result has been certified; substituting answer-defined groups would not state Bott periodicity. (hard)

Selected references

Twisted K-theory and K-theory of bundle gerbes, arXiv:hep-th/0106194v2, https://arxiv.org/abs/hep-th/0106194v2

2 thms1 active userReviewed

Algorithmic Game Theory Operations Research Probability·Captain: iris

Convergence and Stability of Coupled Belief–Strategy Learning Dynamics in Continuous Games: Beliefs and Strategies Converge Almost Surely to a Payoff-Consistent Equilibrium Fixed PointResearch Paper

Motivation

Many strategic systems learn two things at once. Travellers on a road network, firms in a market or bidders in an auction adjust their strategies to each other, and an information platform (a navigation service, a market maker, a public agency) estimates an unknown parameter of the environment from the payoffs those strategies produce. The payoffs are generated by the current strategies, so the data are not i.i.d. The strategies react to the current estimate, so the estimate is not computed from exogenous data. The question is whether this coupled process settles down, and if so, what it settles on.

Wu, Amin and Ozdaglar (arXiv:2206.05637v2, 2023; later in Mathematics of Operations Research, 2025) study this for continuous games with a finite set of candidate parameters. Their first main result, Theorem 1, says that any strategy dynamics that converges when the belief is held fixed still converges when the belief is learned. The limit belief is consistent with the payoff distribution of the limit strategies. It builds on the literature on learning in games (Fudenberg and Kreps 1993; Sandholm 2010) and on Bayesian learning with endogenous data, where a learner may settle on a self-confirming but incorrect belief.

Setting

A finite set $I$ of players repeatedly plays a game. Player $i$ chooses $q_i$ in a convex, closed and bounded set $Q_i\subseteq\mathbb R^{d_i}$ , and $Q=\prod_i Q_i$ . The payoffs depend on an unknown parameter $s$ in a finite set $S$ , with true value $s^*$ . At a profile $q$ , the payoff vector $y\in\mathbb R^I$ has payoff density $\varphi^s(y\mid q)$ , continuous in $q$ . Player $i$ 's average payoff $u_i^s(q)$ is continuous in $q$ .

A belief is $\theta\in\Delta(S)$ . In the game $G(\theta)$ , player $i$ maximizes the expected utility $\sum_{s}\theta(s)u_i^s(q)$ , and $EQ(\theta)$ is its set of pure equilibria in $Q$ .

The dynamics runs in stages $k=1,2,\dots$ , starting from $\theta^1$ with $\theta^1(s)>0$ for all $s$ and $q^1\in Q$ . At stage $k$ the profile $q^k$ is played and $y^k$ is drawn from $\varphi^{s^*}(\cdot\mid q^k)$ . At the update stages $k_1<k_2<\cdots$ the belief is updated by Bayes' rule from the strategies and payoffs since the previous update,

\theta^{k_{t+1}}(s)\propto\theta^{k_t}(s)\prod_{k=k_t}^{k_{t+1}-1}\varphi^s(y^k\mid q^k),

and it is constant in between. Strategies follow a set-valued update $q_i^{k+1}\in F_i(\theta^{k+1},q^k)$ with $F_i(\theta,q)\subseteq Q_i$ .

The KL divergence $D_{KL}(\varphi^{s^*}(\cdot\mid q)\,\|\,\varphi^s(\cdot\mid q))$ is defined as usual, with value $\infty$ when absolute continuity fails. The payoff-equivalent set is $S^*(q)=\{s: D_{KL}=0\}$ , and the support of a belief is $[\theta]=\{s:\theta(s)>0\}$ .

The standing assumptions are:

Assumption 1: each $F_i$ is upper hemicontinuous.
Assumption 2: for every $\theta$ , $EQ(\theta)\neq\emptyset$ , and every run of the update with $\theta$ held fixed converges to a point of $EQ(\theta)$ .
Assumption 3: for every $\theta$ , either $EQ(\theta)$ is a singleton, or its points are isolated and $F$ is single-valued near each of them.

Formalization targets

Goal: Theorem 1 (pp.12–13), with corrected sub-clauses

With probability 1, $(\theta^k,q^k)\to(\bar\theta,\bar q)$ with

[\bar\theta]\subseteq S^*(\bar q)\quad\text{(2a)},\qquad\bar q\in EQ(\bar\theta)\quad\text{(2b)}.

Two further clauses hold for every $s\notin S^*(\bar q)$ :

Rate. If $\varphi^{s^*}(\cdot\mid\bar q)\ll\varphi^s(\cdot\mid\bar q)$ , then $\frac1k\log\theta^k(s)\to-D_{KL}(\varphi^{s^*}(\cdot\mid\bar q)\|\varphi^s(\cdot\mid\bar q))$ .
Exclusion. Otherwise $\theta^k(s)=0$ from some finite stage on.

The rate and exclusion clauses are false as printed, and the goal states minimal corrections:

C0: the rate clause allows $\theta^k(s)$ to reach $0$ .
C1: the rate clause assumes $k_{t+1}/k_t\to1$ .
C2: the rate clause assumes that the KL divergence is continuous at $\bar q$ and that the squared log-likelihood ratio has a locally bounded mean.
C3: the exclusion clause assumes that $q\mapsto\Pr_{\varphi^{s^*}(\cdot|q)}(\varphi^s(y\mid q)=0)$ is lower semicontinuous at $\bar q$ .

Each correction comes with a one-player counterexample that satisfies every assumption of the paper. The convergence and (2a)–(2b) carry no added hypothesis.

Milestones (the proof's three steps, p.22)

Identity (7): the belief equals the every-stage auxiliary belief $\tilde\theta^k$ at update stages and is constant in between.
Lemma 1: the ratio $\tilde\theta^k(s)/\tilde\theta^k(s^*)$ is a supermartingale, and a martingale when $\varphi^s\ll\varphi^{s^*}$ . This is corrected: the printed "martingale" fails when $\varphi^s$ puts mass where $\varphi^{s^*}=0$ .
Lemma 2: $\theta^k\to\bar\theta\in\Delta(S)$ almost surely.
Lemma 3: $q^k\to\bar q\in EQ(\bar\theta)$ almost surely.
Lemma 4: (2a), and the corrected rate and exclusion clauses at the limit.

Significance

The theorem turns a known property, convergence of a strategy dynamics under a fixed belief, into convergence of the coupled belief–strategy dynamics. It covers belief-based best responses in Cournot, potential and supermodular games and no-regret learning in concave games (Table 1, p.11). Condition (2a) characterizes where learning can stop. It may stop at an incomplete-information fixed point, where a wrong parameter cannot be distinguished from $s^*$ at the limit strategies. The paper's later results build on this. Global stability (Proposition 1) holds exactly when no such fixed point exists, and the local stability result (Theorem 2) uses Theorem 1 in its proof.

No part of the result has been formalized. A machine-checked proof also settles the status of the printed statement. The rate and exclusion clauses need the corrections above. The strategy-convergence step (Lemma 3) contains a uniformity claim, " $L=\max_{\hat q^1\in Q}L(\hat q^1)$ is finite because $Q$ is compact" (p.24). No counterexample to it is known, and the convergence clause is posed as printed. A proof, or a counterexample that leads to a further correction, is a contribution.

Difficulty

The natural argument has three steps: martingale convergence for the belief, then the static convergence assumption for the strategies, then a law of large numbers for the log-likelihood ratios at the limit. Steps 2 and 3 do not go through as written. In step 2 the belief moves while the strategies move. Comparing the true path with paths of the fixed-belief dynamics needs a stability property that holds uniformly over starting points. Pointwise convergence on a compact set does not provide it, because convergence times blow up near unstable equilibria. In step 3 the payoffs are a non-stationary, adapted sequence. Convergence of $q^k$ alone does not make the log-likelihood ratios obey a law of large numbers: a density can be continuous in $q$ at every $y$ and still have a log-likelihood ratio whose mean jumps at $\bar q$ . This is why the rate clause needs a regularity hypothesis at $\bar q$ .

Formalization scope

Strategies and beliefs. Profiles live in $\prod_i\mathbb R^{d_i}$ (EuclideanSpace), with Lean's sup-type distance. Beliefs are vectors in stdSimplex ℝ S. Stages are indexed from $0$ .
Payoffs and KL. Payoff densities are functions on $\mathbb R^I$ with Lebesgue measure. $D_{KL}$ is Mathlib's klDiv of the two density measures, which equals Definition 1 for every pair of densities.
The process. A realization of the dynamics is a filtered probability space carrying:
- adapted profiles $q^k$ ;
- payoffs $y^k$ with conditional density $\varphi^{s^*}(\cdot\mid q^k)$ given $\mathcal F_k$ ;
- a random set of update stages that contains the first stage and is infinite almost surely;
- the update $q^{k+1}\in F(\theta^{k+1},q^k)$ almost surely.
The belief is not a free process. $\theta^k$ is the function of $(\theta^1,q,y,T)$ given by (θ-update). If the belief were a free variable, the theorem would be a claim about arbitrary sequences and would be false.
Generalizations. Two hypotheses of the paper are relaxed. $u_i^s$ is not required to be the mean of $y_i$ , since the proof never links them. Strategy updates may be any adapted, possibly randomized, selection.
Assumptions. Upper hemicontinuity uses the open-set definition, with no closed or nonempty values. Assumption 2 ranges over every selection. In Assumption 3(ii), $\bar\theta$ is read as the $\theta$ of the preamble.

The infrastructure is Mathlib's conditional expectation, (super)martingales and their almost-sure convergence, klDiv, and densities via withDensity. A complete development needs a martingale strong law with a conditional variance bound and a conditional Borel–Cantelli lemma. Both are reusable beyond this mission. Contributions are welcome on any milestone. Identity (7) and Lemma 1 are the natural entry points.

Selected references

M. Wu, S. Amin, A. Ozdaglar, Convergence and Stability of Coupled Belief–Strategy Learning Dynamics in Continuous Games, arXiv:2206.05637v2, 2023. https://arxiv.org/abs/2206.05637v2
D. Fudenberg, D. M. Kreps, Learning mixed equilibria, Games and Economic Behavior 5(3), 1993. https://doi.org/10.1006/game.1993.1018
W. H. Sandholm, Population Games and Evolutionary Dynamics, MIT Press, 2010. https://mitpress.mit.edu/9780262195874/
D. Fudenberg, J. Tirole, Game Theory, MIT Press, 1991. https://mitpress.mit.edu/9780262061414/

22 thms1 active userReviewed

Campaigns

All missions

Campaigns

All missions

Campaigns

All missions

The Power of Simple Menus in Robust Selling Mechanisms: Robust Randomized Pricing over Fixed Price Levels Is a Finite Linear ProgramResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (Finite-LP), corrected

Milestones, in proof order

Significance

Difficulty

Formalization scope

Selected references

On the Equivalence and Performance of Distributionally Robust Optimization and Robust Satisficing Models: Every Robust Satisficing Optimum Is Optimal for Wasserstein DRO with Radius −1/α, α ∈ ∂κ(τ)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (corrected)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Optimal Learning for Structured Bandits: DUSA Has Asymptotic Regret at Most (1+ε)(C(P)+ε(1+Σₓ∆(x,P))) log T, Matching the Lower Bound C(P) as ε → 0, with O(log T) Exploration RoundsResearch Paper

Why structured bandits

The model

Formalization targets

Goal: Theorem 3

Milestones

Significance

Difficulty

Formalization scope

Selected references

Multi-product Dynamic Pricing with Limited Inventories under a Cascade Click Model: The Cascade Correction Policy Loses O(log⁡k)O(\log k)O(logk) Against the Deterministic BenchmarkResearch Paper

Selling a ranked list of products

Setting

Formalization targets

Goal: the logarithmic loss (Theorem 3, p.25)

Stationarity of DET

The analysis of the policy

Significance

Difficulty

Formalization scope

Selected references

A Pareto Dominance Principle for Data-Driven Optimization: Under an Exponential Family Whose Statistic Obeys an LDP, the Distributionally Robust Predictor-Prescriptor Pair Is Pareto DominantResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.3

Milestones

Significance

Difficulty

Formalization scope

Selected references

Multi-Agent Online Learning in Time-Varying Games: Mirror Descent Converges Almost Surely to the Nash Equilibrium of a Strictly Monotone Limit GameResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Learning-based Robust Optimization: Procedures and Statistical Guarantees: with n₂ ≥ log δ/log(1 − ϵ), the data-split order-statistic set covers 1 − ϵ of P with confidence 1 − δResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (basic statistical guarantee)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Technical Note—On Revenue Management with Strategic Customers Choosing When and What to Buy: Every Dynamic Pricing Policy Earns at Most the Fluid Value Jˉ1\bar J^1Jˉ1Research Paper

Why the bound matters

The model

Multi-product Dynamic Pricing with Limited Inventories under a Cascade Click Model: The Cascade Correction Policy Loses $O(\log k)$ Against the Deterministic BenchmarkResearch Paper

Technical Note—On Revenue Management with Strategic Customers Choosing When and What to Buy: Every Dynamic Pricing Policy Earns at Most the Fluid Value $\bar J^1$ Research Paper