Missions · Prove2Me

Completed

Dynamical Systems Machine Learning·Captain: mikedeng1

Geometric Deep Learning VIII: An RNN Seeded at a Fixed Point h⁽⁰⁾ = R(0, h⁽⁰⁾) Is Equivariant to Left Shifts of a Zero-Padded Input SequenceTextbook

Why sequence boundaries matter

A recurrent neural network (RNN) processes an ordered stream while retaining a summary of earlier inputs. The same update rule is applied at every time step, so it is natural to ask whether shifting the input stream simply shifts the resulting sequence of summaries. The answer depends on how the run begins. The first summary is supplied as an initial state, while the first input encountered after a shift can be different. Bronstein, Bruna, Cohen and Veličković use this boundary effect to explain a precise form of temporal translation equivariance for RNNs in §5.7 of Geometric Deep Learning (arXiv:2104.13478v2, pp. 90–93).

The claim matters when the same sequential model is applied to streams presented with different starting times. Without a specified boundary convention, the shared update rule alone does not guarantee that corresponding hidden states agree. The chapter's zero-padding construction makes that convention explicit. Its condition on the initial state can then be stated independently of a particular architecture or training procedure. The book numbers equations but no theorems or lemmas here; the mission's items are cited by section, equation, page, and, for a marginal statement, “side-note.”

RNN runs and padded sequences

Let $z(t)\in\mathbb R^k$ be the input at time $t$ , let $h(t)\in\mathbb R^m$ be its hidden summary, and let $R:\mathbb R^k\times\mathbb R^m\to\mathbb R^m$ be a shared update map. Given a seed $h_0$ , equation (38) defines a run by

h(0)=h_0,\qquad h(t+1)=R\bigl(z(t+1),h(t)\bigr).

The first processed input is $z(1)$ ; $z(0)$ is unused. This is the book's time convention, including the named state $h(0)$ (Bronstein et al., §5.7, p. 90, equation (38)). The update map is arbitrary: the results concern the recurrence itself, so they do not require the affine layer and activation used as one example in equation (39).

A left shift by $s$ steps replaces the input at time $t$ with the old input at time $t+s$ . A left-padded input of length $d$ is

\bar z(t)= \begin{cases} 0,&t\le d,\\ z(t-d),&t>d. \end{cases}

Here $0$ is the zero vector in $\mathbb R^k$ . The original input begins at time $d+1$ . The two runs being compared use the same update map and the same seed. This is the exact padding convention displayed on p. 93 of the book (Bronstein et al., §5.7, p. 93).

Formalization targets

The capstone is the chapter's one-step equivariance claim. For every update map, input sequence, and seed fixed by the zero-input update, one or more zero-padding steps suffice:

d\ge1,\qquad R(0,h_0)=h_0 \quad\Longrightarrow\quad h_{\bar z(\cdot+1)}(t)=h_{\bar z}(t+1) \quad\text{for every }t\ge0.

The multi-step side note extends the conclusion to every $s$ with $0\le s\le d$ :

h_{\bar z(\cdot+s)}(t)=h_{\bar z}(t+s) \quad\text{for every }t\ge0.

The milestone list also records the book's unpadded boundary counterexample and its observation that a contraction $\gamma(h)=R(0,h)$ has a unique attracting fixed point. The latter is represented by an already proved, reusable Banach fixed-point theorem rather than a second draft of the same result (Bronstein et al., §5.7, pp. 92–93, equations (40)–(42) and side-note).

What the result supplies

The equivariance theorem identifies a checkable condition under which the hidden-state sequence tracks a left-shifted input exactly, including at the first state. It also marks the limit of the informal idea that sharing the same update map across time automatically creates shift equivariance: the unpadded run can fail already at time $1$ . The fixed-point condition is therefore part of the mathematical claim, rather than an implementation preference (Bronstein et al., §5.7, pp. 92–93).

The RNN shift statements are targets for machine-checked proofs. The contraction milestone already has a machine-checked proof in the referenced CursoEDO.contraction_fixed_point theorem. A completed development would make the boundary convention and the arbitrary-update-map quantifiers available for later statements about sequential models. The recurrence and padding definitions are reusable whenever a discrete-time state update is compared before and after a shift.

The boundary difficulty

The tempting comparison takes two runs that begin with the same seed, then tries to pair the shifted run's state at $t$ with the original run's state at $t+1$ . At the first step, those states have encountered different input histories. Equations (40)–(41) display the mismatch: the original run has applied $R$ to its first input, while the shifted run still uses the supplied seed at the corresponding update. For an arbitrary $R$ and arbitrary first input, the states need not agree (Bronstein et al., §5.7, p. 92). A shift statement that omits its padding length or seed condition would therefore assert something the chapter explicitly rejects.

Formalization scope

Lean represents $\mathbb R^k$ and $\mathbb R^m$ as functions on Fin k and Fin m; time and padding lengths are natural numbers. The run uses $h(0)=h_0$ and consumes $z(t+1)$ at its next update. The padding function returns the zero vector through index $d$ and then the correspondingly indexed original input. These definitions cover every finite dimension, including zero-dimensional edge cases, while the unpadded counterexample uses one input and one hidden coordinate.

The target ranges over all update maps $R$ and all input sequences; it does not impose a special neural-network parameterization. The seed is any fixed point of $h\mapsto R(0,h)$ , not necessarily the zero state, and the zero-input update need not be the identity map. The formal statements include time $t=0$ and the endpoint $s=d$ . No contraction assumption is needed for shift equivariance itself; contraction enters only the separate existence-and-convergence milestone. The contraction theorem is stated for a nonempty complete metric space, which includes the finite-dimensional real hidden-state spaces used here.

The work requires a small discrete recurrence interface, an exact padding definition, and proofs for the boundary counterexample and shift identities. Those two definitions and the shift results can also support variants with a nonzero padding vector. The LSTM equations of §5.8 have a separate gated state model and are outside this mission's formalization scope. Contributions that keep the full fixed-point hypothesis and the stated boundary cases are welcome.

Selected references

M. M. Bronstein, J. Bruna, T. Cohen and P. Veličković, Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges, arXiv preprint, 2021, arXiv:2104.13478v2, §5.7, pp. 90–93.

5 thms3 active usersReviewed

Completed

Harmonic Analysis Linear algebra Machine Learning·Captain: mikedeng1

Geometric Deep Learning III: An n × n Matrix Commutes with the Cyclic Shift S if and only if It Is Circulant, So Convolution Is Shift EquivarianceTextbook

Why convolution, and why the shift

Convolutional neural networks process images, audio and time series with layers whose weights are shared across positions. The Geometric Deep Learning programme of Bronstein, Bruna, Cohen and Veličković (arXiv:2104.13478v2) explains this architecture by symmetry: on a grid the relevant symmetry is translation, and a linear layer that respects translations is forced to be a convolution. Section 4.2 of the book makes this precise in the simplest setting, a one-dimensional periodic grid, and then derives the discrete Fourier transform from the same symmetry, as the common eigenbasis of all convolution operators. The material is classical in signal processing (see the tutorial of Bamieh, arXiv:1805.05533), and the book uses it as the template that the later chapters generalise to groups, graphs and manifolds; for example, graph signal processing (Sandryhaila and Moura, arXiv:1210.4752) replaces the shift by an adjacency matrix.

This mission formalises the characterisation the book calls the basis of "the overall philosophy of Geometric ML": a matrix is circulant if and only if it commutes with the shift (§4.2, p. 37). It is the third mission of a series on the book. The book numbers no theorems, lemmas or definitions; every item is cited by section, equation or position, and printed page.

Setting

Fix $n \ge 1$ and the ring graph with nodes $\mathbb Z_n = \{0, 1, \dots, n-1\}$ , arithmetic taken modulo $n$ . A signal is a vector $x = (x_0, \dots, x_{n-1})$ with entries in a commutative ring $R$ , for instance $\mathbb R$ .

The circulant matrix of a vector $\theta = (\theta_0, \dots, \theta_{n-1})$ is $C(\theta) = (\theta_{u - v \bmod n})_{u, v}$ : each row is the previous one shifted circularly by one position.
The circular convolution of a signal $x$ with a filter $\theta$ is $(x \star \theta)_u = \sum_{v=0}^{n-1} x_v\, \theta_{u - v \bmod n}$ .
The right shift $S$ is the circulant matrix of $\theta = (0, 1, 0, \dots, 0)^\top$ . It moves a vector one position to the right, $(Sx)_u = x_{u-1}$ .
Over $\mathbb C$ , the discrete Fourier basis is $\varphi_k(u) = n^{-1/2} e^{2\pi i k u / n}$ for $k = 0, \dots, n-1$ . The Fourier matrix $\Phi = (\varphi_0, \dots, \varphi_{n-1})$ has the $\varphi_k$ as columns, and $\Phi^*$ is its conjugate transpose.

In Lean the index set is ZMod n with [NeZero n], $C(\theta)$ is Mathlib's Matrix.circulant θ, and the mission's definitions GeomDL.Grids.conv, GeomDL.Grids.shift, GeomDL.Grids.fourierVec and GeomDL.Grids.fourierMatrix are the four objects above.

Formalization targets

Goal: commuting with the shift characterises circulant matrices

For every $n \times n$ matrix $M$ over a commutative ring $R$ ,

M S = S M \iff M = C(\theta) \text{ for some } \theta \in R^n .

The book states the converse direction tentatively ("the opposite direction appears to be true as well"); it is a theorem, and it is stated here without the hedge.

Milestones, in attack order

Circulant matrices are convolutions, $C(\theta)x = x \star \theta$ , and $S = C(0, 1, 0, \dots, 0)$ shifts right, $(Sx)_u = x_{u-1}$ (p. 37).
The left shift is $S^\top$ , and $S^\top S = S S^\top = I$ (side-note, p. 37).
Shift equivariance of convolution, $S\,C(\theta)\,x = C(\theta)\,S\,x$ (p. 37).
The Fourier basis vectors are eigenvectors of $S$ : $S\varphi_k = e^{-2\pi i k/n}\varphi_k$ , with eigenvalues that are $n$ -th roots of unity (p. 38 and side-note).
These eigenvalues are pairwise distinct (side-note, p. 37).
$\Phi^*\Phi = I$ (side-note, p. 38).

Companion: the Convolution Theorem

With $(\mathcal F\theta)_k = \sum_w \theta_w e^{-2\pi i k w/n}$ ,

C(\theta)\varphi_k = (\mathcal F\theta)_k\,\varphi_k, \qquad C(\theta) = \Phi\,\operatorname{diag}(\mathcal F\theta)\,\Phi^* .

The book prints this with $\hat\theta = \Phi^*\theta = n^{-1/2}\mathcal F\theta$ in place of $\mathcal F\theta$ , which is off by a factor $\sqrt n$ for $n \ge 2$ ; the corrected identity is stated. The transform form of the Convolution Theorem, $\mathcal F(u \star v) = \mathcal F u \cdot \mathcal F v$ with Mathlib's ZMod.dft, is already Proved on the platform as IntMul.HvdH.dft_cyclic_conv and is included as a reference item.

Significance

The goal identifies the space of linear translation-equivariant maps on $R^{\mathbb Z_n}$ with the convolutions, an $n$ -dimensional space parametrised by the filter $\theta$ . This is the statement that lets the book define convolution as a translation-equivariant linear operation, and it is the grid case of the general principle the book develops in §4.3 and §5: a linear map that commutes with a group action is a group convolution. Milestones 4–6 and the companion are the other half of §4.2: the shift has distinct eigenvalues, so every matrix commuting with it is diagonal in the shift's eigenbasis, and that eigenbasis is the Fourier basis; hence the Fourier transform diagonalises every convolution.

Mathlib contains circulant matrices, their commutativity (Matrix.circulant_mul_comm) and the discrete Fourier transform on ZMod n, but neither the converse characterisation nor the diagonalisation of circulant matrices by the normalised Fourier matrix. The mission adds these, in a form that later missions of the series (group convolutions, graph Fourier transforms) can be compared against.

Difficulty

The direction " $\Leftarrow$ " is a one-line consequence of the commutativity of circulant matrices. The content is " $\Rightarrow$ ": the equation $MS = SM$ is an equation between matrices, and it has to be turned into the statement that the entries of $M$ are constant along every cyclic diagonal, with the indices handled modulo $n$ . The spectral argument of the book (commuting matrices with a common eigenbasis) only applies over a field containing the $n$ -th roots of unity in which $n$ is invertible; over a general commutative ring, such as $\mathbb Z$ or $\mathbb Z/2$ , the goal has to be proved without it. For the Fourier statements the work is in the geometric sums of roots of unity and in the bookkeeping between the representatives $\{0, \dots, n-1\}$ used in the exponents and the arithmetic of $\mathbb Z_n$ .

Formalization scope

Indices live in ZMod n with [NeZero n], so $n \ge 1$ and matrices are finite; no lower bound $n \ge 2$ is needed (for $n = 1$ , $S = I$ and every matrix is circulant, so the goal holds). Exponents use the representatives ZMod.val $\in \{0, \dots, n-1\}$ , as on the page.
The goal and milestones 1–3 are stated over an arbitrary commutative ring $R$ ; milestones 4–6 and the companion are over $\mathbb C$ .
"Circulant" means equal to Matrix.circulant θ for some θ. Defining a matrix to be circulant when it commutes with $S$ would make the goal true by definition; the mission does not do that. A sanity file checks that the shift moves vectors to the right on $\mathbb Z_3$ and that $\operatorname{diag}(1, 0)$ on $\mathbb Z_2$ does not commute with $S$ .
The side-note on p. 38 calls $\Phi$ "orthogonal"; the property it writes, $\Phi^*\Phi = I$ with the conjugate transpose, is unitarity, and that is what is stated.
The Fourier normalisation is the book's $n^{-1/2}$ in $\varphi_k$ ; the eigenvalues in the companion use Mathlib's unnormalised ZMod.dft, and the factor $\sqrt n$ is written out in its statement.

No new infrastructure beyond Mathlib is required. Proofs of any item, and proofs of the goal that avoid the spectral argument, are welcome; the shift and Fourier lemmas are reusable for the graph Fourier transform later in the book.

Selected references

M. M. Bronstein, J. Bruna, T. Cohen, P. Veličković, Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges, arXiv preprint, 2021 (v2). §4.2, pp. 35–38. https://arxiv.org/abs/2104.13478
B. Bamieh, Discovering Transforms: A Tutorial on Circulant Matrices, Circular Convolution, and the Discrete Fourier Transform, arXiv preprint, 2018. https://arxiv.org/abs/1805.05533
A. Sandryhaila, J. M. F. Moura, Discrete Signal Processing on Graphs, IEEE Transactions on Signal Processing, 2013. https://arxiv.org/abs/1210.4752
D. Harvey, J. van der Hoeven, Integer multiplication in time O(n log n), Annals of Mathematics, 2021 (source of the platform's proved IntMul.HvdH.dft_cyclic_conv). https://hal.science/hal-02070778

9 thms3 active usersReviewed

Category Theory Differential Geometry Mathematical Physics·Captain: mikedeng1

Categorified Symplectic Geometry and the Classical String: The Hamiltonian 1-Forms of a 2-Plectic Space Form a Hemistrict Lie 2-AlgebraResearch Paper

Motivation

Classical Hamiltonian mechanics describes an observable by a function on a phase space. Its Poisson bracket gives observables a Lie algebra: the bracket is antisymmetric and satisfies the Jacobi identity. In multisymplectic geometry, a higher-degree differential form replaces the symplectic two-form, and the appropriate observables may themselves be differential forms. This occurs in the geometric description of classical field theories, where quantities associated with spatially extended objects are naturally expressed through forms rather than functions. Baez, Hoffnung and Rogers use this setting to examine the classical bosonic string in their paper, §§1 and 5.

The same paper shows why the usual Lie algebra of observables is too narrow for a 2-plectic space. One bracket of Hamiltonian one-forms satisfies the Jacobi identity but is antisymmetric only up to an exact form; another is antisymmetric but has a Jacobi identity only up to an exact form. Theorem 4.3 packages the first bracket and its exact correction into a hemistrict Lie 2-algebra. The result is known mathematically; the mission is to give its construction a machine-checked statement and proof in Lean for a finite-dimensional vector-space model Baez–Hoffnung–Rogers, §§3–4.

Setting

Let $E$ be a finite-dimensional real normed vector space. A 2-plectic form $\omega$ on $E$ is a smooth three-form with $d\omega=0$ such that $\iota_v\omega=0$ implies $v=0$ at each point. The interior product $\iota_v$ places $v$ in the first argument of the form. This is the $n=2$ case of Definition 2.1 in the preprint, p. 6.

A smooth one-form $F$ is Hamiltonian when a smooth vector field $v_F$ satisfies

dF=-\iota_{v_F}\omega.

Nondegeneracy makes $v_F$ unique. Write $\operatorname{Ham}(E,\omega)$ for the vector space of these forms. The hemi-bracket is $\{F,G\}_h=\mathcal L_{v_F}G$ , where $\mathcal L_v$ is the Lie derivative. On functions its left and right actions are $\{F,f\}_h=\mathcal L_{v_F}f$ and $\{f,F\}_h=0$ . The alternator is the function $S_{F,G}=-(\iota_{v_F}G+\iota_{v_G}F)$ . These formulas are Definitions 3.1 and 3.3 and the data preceding Theorem 4.3 on pp. 11 and 16–17.

A Lie 2-algebra here has a two-term chain complex $L_0\xleftarrow{d}L_1$ , a bracket on its available degrees, an alternator witnessing antisymmetry up to chain homotopy, and a Jacobiator witnessing the Jacobi relation up to chain homotopy. Four further coherence diagrams constrain these homotopies. “Hemistrict” means that the Jacobiator is the identity homotopy, represented by the zero degree-one map Definitions 4.1–4.2, pp. 15–16.

Formalization targets

Hemistrict structure on Hamiltonian one-forms

For every 2-plectic $(E,\omega)$ , Theorem 4.3 constructs a hemistrict Lie 2-algebra with all components fixed:

L_0=\operatorname{Ham}(E,\omega),\qquad L_1=C^\infty(E),\qquad d_L f=df,\qquad [F,G]=\{F,G\}_h,

[F,f]=\mathcal L_{v_F}f,\qquad [f,F]=0,\qquad S_{F,G}=-(\iota_{v_F}G+\iota_{v_G}F),\qquad J_{F,G,H}=0.

The existential goal fixes the carriers and every operation; the Lie 2-algebra structure then requires the chain-map identities, the homotopy identities, and all four coherence equations. The milestones isolate the source statements that supply the main geometric identities: uniqueness of $v_F$ , Hamiltonian exact forms, Proposition 3.6, the bracket’s chain-map behavior, a mixed Jacobi identity, and the third coherence diagram Theorem 4.3 and its proof, pp. 17–18.

Significance

The theorem identifies the algebraic structure carried by 2-plectic observables. In particular, it retains the exact-form discrepancy in antisymmetry as an explicit operation instead of losing it by quotienting forms. The paper compares this hemistrict construction with a semistrict construction and then studies their relation; the present result is the first of those two constructions Theorems 4.3–4.6, pp. 17–19.

A formal proof would connect Mathlib’s exterior derivative on alternating forms to a reusable calculus of interior products, Lie derivatives, Hamiltonian vector fields, and higher algebraic coherence. The preprint already proves the theorem. The local proposal supplies statements for its finite-dimensional normed-space case; a proof in Lean and an extension from vector spaces to general smooth manifolds are further work. The current mission does not assert the separate semistrict theorem or the string application.

Difficulty

The obvious attempt to make Hamiltonian one-forms into a conventional Lie algebra fails: for the hemi-bracket, $\{F,G\}_h+\{G,F\}_h$ can be a nonzero exact form. The correction must also agree with the bracket on functions and with the Jacobi relation across degrees. A degree-zero calculation alone therefore does not establish a Lie 2-algebra. Its chain-map conditions and four coherence diagrams impose further identities involving the exterior derivative, Lie derivatives and the Hamiltonian vector fields Proposition 3.6 and Definition 4.1, pp. 12, 15–16.

Formalization scope

Lean uses $E$ with NormedAddCommGroup, NormedSpace ℝ E and FiniteDimensional ℝ E, in place of the paper’s arbitrary smooth manifold $X$ . Forms, functions and vector fields are defined on all of $E$ , and smoothness means ContDiff ℝ smooth with smooth the $C^\infty$ degree. This is the disclosed scope cut. The Lean name for the paper’s $\omega$ is Ω; this avoids a notation conflict from the imported definition module.

Mathlib represents a $k$ -form as a function into a continuous alternating $k$ -linear map. Its extDeriv supplies the exterior derivative, while the published ContWeatherall.grad supplies $df$ for functions. Interior product inserts in the first slot. The Lie derivative of a one-form uses its derivative and the derivative of the vector field, so Cartan’s identity is a mathematical assertion rather than the definition of the Lie derivative. The bracket of vector fields uses $[V,W]=DW\cdot V-DV\cdot W$ . The two-term chain complex uses the paper’s ordinary graded tensor-product differential and signed switch. Every formal statement about hamVF restricts its form to Hamiltonian inputs, where nondegeneracy gives a unique vector field; the default value on other inputs has no role in the theorem.

The goal requires all operations to have the paper’s values and requires every Lie 2-algebra axiom. An arbitrary pre-existing Lie 2-algebra or a structure with unconstrained operations would not establish this result. Reusable contributions include differential-form identities and the algebraic two-term interface. The separate semi-bracket construction and general-manifold extension remain outside this proposal.

Selected references

J. C. Baez, A. E. Hoffnung and C. L. Rogers, Categorified Symplectic Geometry and the Classical String, preprint arXiv:0808.0246v1, 2008; published in Communications in Mathematical Physics 293 (2010), 701–725. Preprint.

11 thms3 active usersReviewed

Completed

Algebra Category Theory Group Theory·Captain: mikedeng1

Crossed Product of Groups. Applications: The Skeleton of the Category E2(H, G) of Crossed Products Is Crossed(H, G) Modulo 2-EquivalenceResearch Paper

Motivation

The extension problem for groups asks for a description of all groups $E$ that contain a given group $H$ as a normal subgroup with quotient isomorphic to a given group $G$ . Schreier (1926) answered it by showing that every such extension can be rebuilt from $H$ , $G$ and two maps: a map $\alpha : G \to \mathrm{Aut}(H)$ and a map $f : G \times G \to H$ , subject to two compatibility conditions. The group built from this data is the crossed product $H \#_\alpha^f G$ . When $H$ is abelian, this becomes the cohomological classification of extensions by $H^2(G, H)$ ; for nonabelian $H$ it is the theory of Eilenberg and MacLane (1947).

The classical classification counts extensions up to isomorphisms that are the identity on $H$ and induce the identity on $G$ . Agore and Militaru (arXiv:0805.4077v2, 2008) also study a coarser notion, in which the isomorphism may act on $H$ and on $G$ by arbitrary automorphisms. The resulting classification, their Theorem 3.8, is the target of this mission. It is closer to the question "which groups arise as crossed products of $H$ and $G$ , up to isomorphisms respecting the extension structure", which is what is needed when listing groups of a given shape. The paper's applications include the description of all morphisms between two crossed products by explicit data.

Setting

Let $H$ and $G$ be groups. For a map $\alpha : G \to \mathrm{Aut}(H)$ write $g \triangleright h = \alpha(g)(h)$ . A crossed system is a pair $(\alpha, f)$ with $f : G \times G \to H$ such that, for all $g_1, g_2, g_3 \in G$ and $h \in H$ ,

g_1 \triangleright (g_2 \triangleright h) = f(g_1, g_2)\,\big((g_1g_2) \triangleright h\big)\,f(g_1, g_2)^{-1}, \qquad f(g_1, g_2)\, f(g_1g_2, g_3) = \big(g_1 \triangleright f(g_2, g_3)\big)\, f(g_1, g_2g_3).

Then $\alpha$ is called a weak action: it is a homomorphism only up to the inner automorphisms given by $f$ . The system is normalized if $f(1,1) = 1$ , and $\mathrm{Crossed}(H, G)$ is the set of normalized crossed systems. The crossed product $H \#_\alpha^f G$ is the set $H \times G$ with

(h_1, g_1)\cdot(h_2, g_2) = \big(h_1\,(g_1 \triangleright h_2)\,f(g_1, g_2),\; g_1g_2\big),

which is a group exactly when $(\alpha, f)$ is a crossed system.

The category $\mathcal{E}_2(H, G)$ has $\mathrm{Crossed}(H, G)$ as its objects. A morphism $(\alpha, f) \to (\alpha', f')$ is a triple $(\eta, \psi, \gamma)$ of group morphisms $\eta : H \to H$ , $\gamma : G \to G$ and $\psi : H \#_\alpha^f G \to H \#_{\alpha'}^{f'} G$ such that $\psi(h, 1) = (\eta(h), 1)$ and the $G$ -component of $\psi(h, g)$ is $\gamma(g)$ .

Two normalized crossed systems are 2-equivalent, $(\alpha, f) \approx_2 (\alpha', f')$ , if there are group automorphisms $\eta$ of $H$ and $\gamma$ of $G$ and a map $t : G \to H$ with

g \triangleright' h = \eta\Big(t(g)\big(\gamma^{-1}(g) \triangleright \eta^{-1}(h)\big)t(g)^{-1}\Big), \qquad f'(g_1, g_2) = \eta\Big(t(g_1)\big(\gamma^{-1}(g_1) \triangleright t(g_2)\big) f\big(\gamma^{-1}(g_1), \gamma^{-1}(g_2)\big) t(g_1g_2)^{-1}\Big).

Formalization targets

Goal: Theorem 3.8

\approx_2 \text{ is an equivalence relation on } \mathrm{Crossed}(H, G), \qquad \mathrm{Ob}\,\mathrm{Sk}\,\mathcal{E}_2(H, G) \;\cong\; \mathrm{Crossed}(H, G)/\!\approx_2,

with the bijection sending the isomorphism class of $(\alpha, f)$ to its $\approx_2$ -class. The statement holds for all groups $H$ , $G$ , finite or not, abelian or not.

Milestones, in the order of the paper

Lemma 1.2: the values $f(g, 1)$ , $f(1, g)$ and $1 \triangleright h$ in a crossed system.
Theorem 1.3: (8) is associative if and only if $(\alpha, f)$ is a crossed system, and then $H \#_\alpha^f G$ is a group with unit $(f(1,1)^{-1}, 1)$ .
Theorem 2.1: the crossed product is an initial object of one category and a final object of another.
Corollary 2.2 (1)–(2): group morphisms out of and into a crossed product.
Corollary 2.3: group morphisms $H \#_\alpha^f G \to H \#_{\alpha'}^{f'} G$ correspond to quadruples $(u, r, v, s)$ of maps.
Proposition 3.4: morphisms of $\mathcal{E}_2(H, G)$ with given $\eta$ , $\gamma$ correspond to maps $r : G \to H$ satisfying two conditions.
Corollary 3.5: a morphism of $\mathcal{E}_2(H, G)$ is an isomorphism iff $\eta$ , $\gamma$ are isomorphisms and the 2-equivalence conditions hold for a unique $t$ compatible with $\psi$ .
§3, p. 21: $\approx_2$ coincides with isomorphism in $\mathcal{E}_2(H, G)$ and is an equivalence relation.

Significance

The theorem replaces the categorical question "when are two crossed products isomorphic in $\mathcal{E}_2(H, G)$ " by an explicit system of equations in the data $(\alpha, f)$ . For finite $H$ and $G$ the quotient $\mathrm{Crossed}(H, G)/\!\approx_2$ is a finite, computable set, so the theorem turns the description of crossed products of $H$ by $G$ up to this isomorphism into a finite computation. The intermediate results are of independent use: Corollary 2.3 describes every group morphism between two crossed products, and Theorem 2.1 gives the two universal properties of the crossed product.

The results are proved in the paper. None of them has a machine-checked proof: Mathlib has GroupExtension and its equivalences, which correspond to the finer category $\mathcal{E}_1(H, G)$ of the paper, and SemidirectProduct, the special case $f = 1$ with $\alpha$ an action, but no crossed product with a cocycle, no weak actions, and no $\mathcal{E}_2$ -type classification. Formalizing the mission produces a reusable nonabelian crossed-product layer and an explicit classification of extensions up to automorphisms of both ends.

Difficulty

Each step is elementary group theory, but the computations are long and noncommutative. The central difficulty is Corollary 2.3: every group morphism between two crossed products must be reconstructed from its values on the generators $(h, 1)$ and $(1, g)$ , and the five compatibility conditions must be shown to be equivalent to multiplicativity, keeping track of the weak action and both cocycles in a nonabelian group. The tempting shortcut of treating $\alpha$ as an action fails: (2) only makes $\alpha$ multiplicative up to conjugation by $f$ , and this twist appears in every identity. In Corollary 3.5 the inverse of $\psi$ must itself be shown to be a morphism of $\mathcal{E}_2$ and the map $t$ extracted from it.

Formalization scope

Everything is in the namespace CrossedProductGroups.Classification, for arbitrary {H G : Type*} [Group H] [Group G].

The weak action is a plain map α : G → MulAut H, not a homomorphism; the cocycle is curried, f : G → G → H.
IsCrossedSystem α f records (2) and (3) with the factors in the printed order; Crossed H G is the subtype of pairs with f 1 1 = 1.
The crossed-product multiplication is the function crossedMul α f on H × G. No group instance is put on it; a morphism of groups between crossed products is a map preserving crossedMul.
E2 H G is a type synonym for Crossed H G with a Mathlib Category instance. Its morphisms (E2Hom) record η : H →* H, γ : G →* G and a multiplicative ψ with ψ (h, 1) = (η h, 1) and (ψ x).2 = γ x.2. The paper's inclusion $i_H(h) = (h f(1,1)^{-1}, 1)$ equals $(h, 1)$ on normalized systems, the only objects.
Equiv2 is Definition 3.7, with $\gamma^{-1}, \eta^{-1}$ as γ.symm, η.symm.
The goal uses Mathlib's CategoryTheory.Skeleton and Quot Equiv2, includes Equivalence Equiv2, and requires the bijection to send toSkeleton c to the class of c.
Theorem 2.1's categories are not built: initial and final are unfolded into existence and uniqueness of morphisms. In Corollary 3.5, the uniqueness of $t$ is stated together with the formula for $\psi$ , since (38) and (39) alone do not determine $t$ . The bijection of Corollary 2.3 is pinned to the paper's formula for $\psi$ .

A bare equality of cardinalities between the skeleton and the quotient, an isomorphism notion in $\mathcal{E}_2$ defined as $\approx_2$ , or morphisms $\psi$ that need not be multiplicative would each make the goal weaker than the paper's statement; the definitions above rule these out.

Contributions welcome: proofs of the milestones in any order, a reusable API for crossedMul (the group structure of Theorem 1.3 on a type synonym), and a bridge to Mathlib's GroupExtension.

Selected references

A. L. Agore, G. Militaru, Crossed product of groups. Applications, arXiv preprint, 2008. https://arxiv.org/abs/0805.4077v2
O. Schreier, Über die Erweiterung von Gruppen I, Monatshefte für Mathematik und Physik 34 (1926), 165–180.
S. Eilenberg, S. MacLane, Cohomology theory in abstract groups. II. Group extensions with a non-Abelian kernel, Annals of Mathematics 48 (1947), 326–341.
K. S. Brown, Cohomology of Groups, Graduate Texts in Mathematics 87, Springer, 1982 (Chapter IV).

11 thms3 active usersReviewed

Completed

Quantum Information Theoretical Computer Science·Captain: mikedeng1

A Meet-in-the-Middle Algorithm for Fast Synthesis of Depth-Optimal Quantum Circuits: Meet-in-the-Middle Search Returns a Minimal-Depth Circuit, Generating Only Circuits of Half the DepthResearch Paper

Motivation

A quantum algorithm is run as a quantum circuit: a sequence of elementary gates drawn from a fixed instruction set, such as the Hadamard, phase, controlled-NOT and $T$ gates. On fault-tolerant hardware every layer of gates costs time and error-correction overhead, so the depth of a circuit, its number of layers, is a primary cost measure. Compilers therefore want, for a given target unitary, a circuit of the least possible depth, not merely some circuit.

Amy, Maslov, Mosca and Roetteler (arXiv:1206.0758, IEEE TCAD 2013) gave an exact, depth-optimal synthesis algorithm, MITM-factor, based on a meet-in-the-middle search. With it they found the first $T$ -depth-3 circuit for the Toffoli gate and improved circuits for several standard gates. Approximate synthesis methods such as the Solovay–Kitaev algorithm (Dawson–Nielsen) produce short circuits but not optimal ones. The paper is a standard reference for exact, optimal synthesis over Clifford+ $T$ , and later depth- and $T$ -count-optimal search methods start from it.

Setting

Fix $n$ qubits. $U(2^n)$ is the group of $2^n \times 2^n$ complex matrices $U$ with $UU^\dagger = U^\dagger U = I$ , where $U^\dagger$ is the conjugate transpose. An instruction set $\mathcal G$ is a set of gates closed under inversion. A gate acts on some of the qubits and as the identity on the rest.

A depth-one circuit applies gates of $\mathcal G$ to pairwise disjoint sets of qubits at once. $\mathcal V_{n,\mathcal G}$ is the set of unitaries of depth-one circuits. A circuit of depth $m$ is a sequence of layers $U_1, \dots, U_m \in \mathcal V_{n,\mathcal G}$ , and it implements $U_1U_2\cdots U_m$ . Let

S_0 = \{I\}, \qquad S_i = \mathcal V_{n,\mathcal G}\, S_{i-1},

so $S_i$ is the set of unitaries implementable in depth $i$ , and write $S_i^\dagger U = \{X^\dagger U : X \in S_i\}$ .

MITM-factor $(\mathcal G, U, l)$ runs $i = 1, \dots, \lceil l/2\rceil$ . At step $i$ it builds $S_i$ and tests whether $S_{i-1}^\dagger U \cap S_i \ne \emptyset$ ; if so it returns the concatenation of the two witnessing circuits. Otherwise it tests $S_i^\dagger U \cap S_i \ne \emptyset$ in the same way. If no step succeeds, it returns nothing.

In the Lean development the layer set is a finite set V of unitaries standing for $\mathcal V_{n,\mathcal G}$ , S V i is $S_i$ , circuits V i is the set of circuits of $i$ layers (lists over V), and mitmFactor V U l is the algorithm.

Formalization targets

Goal: the main result (§2, p. 4)

For every finite $V$ , unitary $U$ and $l \ge 0$ , with $h = \lceil l/2\rceil$ :

\text{MITM-factor}(U,l) = \text{none} \iff U \notin S_1 \cup \cdots \cup S_{2h},

and a returned circuit $c$ lies over $V$ , implements $U$ , has $1 \le |c| \le 2h$ , and $|c| \le |c'|$ for every circuit $c'$ over $V$ of positive depth implementing $U$ . For even $l$ the decided range is exactly $1 \le d \le l$ . If $|V| \ge 2$ , the counted cost satisfies

\mathrm{cost}(U,l) \le 8\,|V|^{h}\log_2 |V|^{h}.

The goal fixes no instruction set and no gate. It is the paper's correctness and running-time claim for the search itself.

Milestones

In attack order:

$\mathcal V_{n,\mathcal G}$ is closed under adjoint (proof of Lemma 1).
$S_i^\dagger = S_i$ when the layer set is closed under adjoint.
The sets the algorithm generates are exactly the depth- $i$ circuits and their unitaries.
Lemma 1: $U$ has a depth- $l$ circuit iff $S_{\lfloor l/2\rfloor}^\dagger U \cap S_{\lceil l/2\rceil} \ne \emptyset$ .
Iteration $i$ tests depth $2i-1$ , then depth $2i$ .
The algorithm stops at the least positive depth.
$|S_i| \le |V|^i$ .
The two sum bounds of the running-time analysis.

Significance

The result. Searching all circuits of depth at most $l$ takes $|\mathcal V_{n,\mathcal G}|^l$ steps. MITM-factor needs only about $|\mathcal V_{n,\mathcal G}|^{\lceil l/2\rceil}$ , up to a logarithmic factor: a square-root saving that made exhaustive depth-optimal synthesis of three- and four-qubit gates feasible. Its correctness is what lets a computer search certify optimality: when the search fails up to depth $l$ , no shorter circuit exists. The paper's non-existence statements, such as the absence of shallower circuits for particular gates, rest on this.

Formalizing it. The result is proved in the paper, informally and briefly. No machine-checked version is known to exist. The mission produces a checked statement of what the search decides, which repairs two boundary cases of the printed claim (see Formalization scope), and a cost bound with an explicit constant in place of the $O$ . Lemma 1 and the generation step are reusable for any meet-in-the-middle search over a monoid generated by a finite set.

Difficulty

The mathematics is elementary; the difficulty is in stating exactly what the algorithm does. The obvious reading, "the algorithm decides depth at most $l$ ", is false for odd $l$ : the last step also tests depth $l + 1$ and may return a circuit of that depth. "Returns a circuit of minimal depth" is false for $U = I$ , whose minimal depth $0$ is never tested. A proof therefore has to track the loop's first success through two interleaved tests per step, and connect sets of unitaries to circuits as lists of layers. For the cost bound, the step from per-iteration costs to the total needs the geometric-sum bound in a form the paper misprints: $\sum_{i \le h} m^i \le m^h(1 + 1/(m^h - 1))$ fails at $m = 2$ , $h = 2$ .

Formalization scope

Unitaries are elements of Matrix.unitaryGroup (Fin n → Bool) ℂ; $U^\dagger$ is the group inverse.
The layer set V is an arbitrary Finset of unitaries. The paper's argument uses nothing about $\mathcal V_{n,\mathcal G}$ beyond finiteness, and milestone 1 relates $\mathcal V_{n,\mathcal G}$ , defined over the shared QAlgorithms gate and circuit layer, to this setting. Hypotheses on V appear only where used: closure under inverse for milestone 2, $|V| \ge 2$ for the cost clause.
Circuits are Lists of layers, implementing their List.prod, head leftmost, as " $U_1U_2\cdots U_m$ " on p. 4. The algorithm returns a circuit, not a unitary. The "any circuit" of the pseudocode is a choice of witnesses.
Corrections, each disclosed in the items:
- the decided range is $1 \le d \le 2\lceil l/2\rceil$ ;
- minimality is among circuits of positive depth;
- the second sum bound uses $1/(|V| - 1)$ .
Cost model. The running time is a counted cost, built from the sets $S_i$ the run actually generates:
- $|V|\,|S_{i-1}|$ to generate $S_i$ ;
- $|S_i|\log_2|S_i|$ to sort it;
- $(|S_{i-1}| + |S_i|)\log_2|S_i|$ for the lookups.
These are summed over the iterations executed, up to the first success. Logarithms are Real.logb 2. The constant $8$ is the mission's explicit form of the paper's $O$ .
Trivializing readings are ruled out: the cost is not defined from $|V|^i$ , which would make the bound an identity about powers, and the goal is not an existence claim about some algorithm with that cost. A circuit-valued output compared against every circuit over $V$ prevents a content-free minimality clause.
Not covered: Theorem 1 and Theorem 2 with Lemma 2 (controlled- $U$ costs and $T$ -depth with ancillas), the $T$ -depth variant of §3.1, the pruning of §4, and the computational results of §§5–6.
Welcome contributions: proofs of the milestones, lemmas on circuits and S (for instance $S_{i+j} = S_iS_j$ ), and a list-based model of the sort-and-search cost.

Selected references

M. Amy, D. Maslov, M. Mosca, M. Roetteler, A meet-in-the-middle algorithm for fast synthesis of depth-optimal quantum circuits, IEEE Trans. Computer-Aided Design 32(6), 2013; arXiv:1206.0758v3. https://arxiv.org/abs/1206.0758
C. M. Dawson, M. A. Nielsen, The Solovay–Kitaev algorithm, Quantum Inf. Comput. 6(1), 2006; arXiv:quant-ph/0505030. https://arxiv.org/abs/quant-ph/0505030

14 thms3 active usersReviewed

Mathematical Physics Quantum Information Representation Theory·Captain: mikedeng1

SU(2)-Irreducibly Covariant and EPOSIC Channels: EPOSIC Channels Are Exactly the Extreme Points of the Convex Set of SU(2)-Irreducibly Covariant ChannelsResearch Paper

Motivation

A quantum channel is a completely positive, trace-preserving linear map between matrix algebras; it models the most general physical transformation of a quantum system. When a group $G$ acts on the input and output systems, a channel is $G$ -covariant if it commutes with the group action. Covariant channels appear whenever a physical process respects a symmetry: rotation-invariant noise on spin systems, optimal cloning and estimation of spin states, and quantum reference frames for orientation. Because the covariant channels between two fixed representations form a convex set, the first structural question is what its extreme points are; they are the channels from which every covariant channel is obtained by mixing.

For $G = SU(2)$ acting irreducibly on input and output, the tensor product of the output representation with the dual of the input one is multiplicity free, so the commutant that controls covariant maps is abelian (Vollbrecht and Werner, 2001, arXiv:quant-ph/0010095). M. Al Nuwairan (arXiv:1306.5321, 2013) makes this concrete. She constructs explicit channels $\Phi_{m,n,h}$ , called EPOSIC channels, from Clebsch–Gordan isometries realized on polynomials. She computes their Choi matrices and shows that they are exactly the extreme points of the convex set of SU(2)-irreducibly covariant channels.

Setting

For $k \in \mathbb N$ , let $P_k$ be the space of homogeneous polynomials of degree $k$ in two variables $x_1, x_2$ . The group

SU(2)=\left\{\begin{pmatrix}a&b\\-\bar b&\bar a\end{pmatrix}: a,b\in\mathbb C,\ |a|^2+|b|^2=1\right\}

acts on $P_k$ by the representation $\rho_k$ ,

(\rho_k(g)f)(x_1,x_2)=f\big((x_1,x_2)g\big)=f(ax_1-\bar bx_2,\ bx_1+\bar ax_2).

With the inner product $\langle x_1^lx_2^{k-l},x_1^jx_2^{k-j}\rangle=l!(k-l)!\,\delta_{lj}$ , the canonical basis $f^k_l=x_1^lx_2^{k-l}/\sqrt{l!(k-l)!}$ , $0\le l\le k$ , is orthonormal and $\rho_k$ is unitary. The $\rho_k$ are the irreducible representations of $SU(2)$ .

The tensor product $P_m\otimes P_n$ is realized as the polynomials in $x=(x_1,x_2)$ and $y=(y_1,y_2)$ of bi-degree $(m,n)$ . On these polynomials act the operators

\Delta_{xy}=x_1\partial_{y_1}+x_2\partial_{y_2},\quad \Delta_{yx}=y_1\partial_{x_1}+y_2\partial_{x_2},\quad \Gamma_{xy}=(x_1y_2-y_1x_2)\cdot,\quad \Omega_{xy}=\partial_{x_1}\partial_{y_2}-\partial_{x_2}\partial_{y_1}.

Real coefficients $c_{m,n,h}$ are defined by the recursion $c_{m,0,0}=1$ and, for $n\ge 1$ , $c_{m,n,h}=\frac{1}{(m+1)n}\,c_{m+1,n-1,h}$ if $h=0$ , $\frac{1}{(m+1)n}\,(c_{m-1,n-1,h-1}+c_{m+1,n-1,h})$ if $0<h<n$ , and $\frac{1}{(m+1)n}\,c_{m-1,n-1,h-1}$ if $h=n$ . For $0\le h\le\min\{m,n\}$ and $r=m+n-2h$ , the map

\alpha_{m,n,h}:P_r\to P_m\otimes P_n,\qquad \alpha_{m,n,h}(f)=\sqrt{c_{m,n,h}}\;\Gamma_{xy}^h\Delta_{yx}^{n-h}f

is an explicit Clebsch–Gordan isometry. The EPOSIC channel is

\Phi_{m,n,h}(A)=\mathrm{Tr}_{P_n}\big(\alpha_{m,n,h}A\alpha_{m,n,h}^*\big),\qquad A\in\mathrm{End}(P_r).

For $r,m\in\mathbb N$ , $EC(r,m)$ is the set of the channels $\Phi_{m,n,h}$ with $r=m+n-2h$ and $0\le h\le\min\{m,n\}$ . The set $QC_{SU(2)}(\rho_r,\rho_m)$ consists of the quantum channels $\Phi:\mathrm{End}(P_r)\to\mathrm{End}(P_m)$ with $\Phi(\rho_r(g)A\rho_r(g)^*)=\rho_m(g)\Phi(A)\rho_m(g)^*$ for all $A$ and all $g\in SU(2)$ .

Formalization targets

Goal: Proposition 4.1

\operatorname{ext} QC_{SU(2)}(\rho_r,\rho_m)=EC(r,m)\qquad\text{for all } r,m\in\mathbb N.

The statement has no hypotheses and covers the degenerate cases: for $\min\{r,m\}=0$ the set $EC(r,m)$ is a single channel.

Milestones

In the order of the paper's argument:

the polynomial decomposition identity behind $c_{m,n,h}$ (Theorem 2.7), the adjoint of $\alpha_{m,n,h}$ and the resolution of the identity $\sum_h\alpha_{m,n,h}\alpha_{m,n,h}^*=I$ (Lemma 2.9);
$\alpha_{m,n,h}$ is an SU(2)-equivariant isometry (Proposition 2.10), so $\Phi_{m,n,h}\in QC_{SU(2)}(\rho_r,\rho_m)$ (Proposition 2.18), and $EC(r,m)=\{\Phi_{m,r+m-2l,m-l}:0\le l\le\min\{r,m\}\}$ (Proposition 2.21);
the orthogonal decomposition of $P_m\otimes\bar P_n$ into irreducible subspaces with projections $q$ (Corollary 2.13), covariance in terms of the Choi matrix (Proposition 1.15(1)), and the commutant of $\rho_m\otimes\check\rho_r$ (Proposition 3.9);
the Choi matrix $C(\Phi_{m,n,h})=\frac{r+1}{n+1}q_{m,r,m-h}$ (Lemma 3.12, Proposition 3.13);
$EC(r,m)$ spans the SU(2)-equivariant linear maps (Corollary 3.16), and $QC_{SU(2)}(\rho_r,\rho_m)=\operatorname{conv}EC(r,m)$ (Corollary 3.17).

Significance

The result shows that the covariant channels between two irreducible SU(2) representations form a simplex. Its $\min\{r,m\}+1$ vertices are given by closed formulas, so optimization problems over SU(2)-covariant channels reduce to finite-dimensional linear programs over the vertex weights: fidelities, output entropies, capacities restricted to covariant encodings. The explicit Choi matrices make the vertices computable in any basis. The same channels are used later in the paper to compute complementary channels and to exhibit a positive map that is not completely positive.

On the formal side, the mission produces the irreducible representations of $SU(2)$ on homogeneous polynomials, the polarization operators, and explicit Clebsch–Gordan isometries with their equivariance and isometry proofs. It also produces a Choi-matrix criterion for covariance and the extreme-point characterization. Theorem 2.7, Proposition 1.15 and Proposition 3.9 are cited in the paper from Procesi, from [4] and from Vollbrecht–Werner, and are proved neither there nor, as far as is known, in any proof assistant. Nothing in this mission is machine-checked yet.

Difficulty

That $\Phi_{m,n,h}$ is a covariant channel follows from equivariance of $\alpha_{m,n,h}$ . The real content lies elsewhere.

First, $\alpha_{m,n,h}$ is an isometry only because of the specific constants $c_{m,n,h}$ . The paper derives this from the polynomial identity of Theorem 2.7 and Schur's lemma, and neither is available off the shelf for these polynomial models.

Second, the extreme-point statement needs the full commutant of $\rho_m\otimes\bar\rho_r$ : the projections onto the irreducible summands must span it. Exhibiting the projections is not enough; one must show there is nothing else, which is multiplicity-freeness of the tensor product. This requires the irreducibility of each $\rho_k$ and the Clebsch–Gordan dimension count.

Third, matching each EPOSIC channel with a single projection (Proposition 3.13) requires a rank argument. The obvious approach, expanding the Choi matrix in coordinates, gives sums of products of signed binomial coefficients whose non-vanishing is the content of Lemma 3.12.

Formalization scope

Every space $P_k$ is represented by coordinates in its canonical orthonormal basis, indexed by Fin (k+1) with 0-based indices. So $\mathrm{End}(P_k)$ is the algebra of $(k+1)\times(k+1)$ complex matrices, and adjoints for the inner product above are conjugate transposes. The representation $\rho_k$ and the maps $\alpha_{m,n,h}$ are computed from the polynomials themselves in MvPolynomial (Fin 4) ℂ (variables $x_1,x_2,y_1,y_2$ , derivatives pderiv), then read off in the canonical bases. The action is the row-vector action $f\mapsto f((x_1,x_2)g)$ of the paper. $P_m\otimes P_n$ is indexed with the $P_m$ factor first. The conjugate space $\bar P_k$ has the same coordinates and carries the entrywise conjugate matrices. The coefficients $c_{m,n,h}$ are defined by the recursion, not by any closed formula. The input degree $r$ of $\alpha$ is an explicit argument, constrained by $r+2h=m+n$ in every statement.

Channels are maps on matrices given by a finite normalized Kraus family (the published QAlgorithms.IsChannel). The partial trace is the published WildeQIT.partialTraceRight, over the $P_n$ factor. The Choi matrix is $\sum_{ij}\Phi(E_{ij})\otimes E_{ij}$ with the output factor first. Convex hulls and extreme points are taken over $\mathbb R$ in the space of maps.

No statement replaces $\rho_k$ by an abstract irreducible representation. None defines $EC(r,m)$ through extreme points, Choi matrices or projections, defines $\alpha_{m,n,h}$ by its coefficient expansion, or assumes Schur's lemma, the commutant description or Theorem 2.7 as a hypothesis. Each of these would make the goal or a milestone true by definition.

A complete development needs:

the irreducibility and unitarity of $\rho_k$ ;
Schur's lemma for these matrix representations;
the Clebsch–Gordan decomposition and the polynomial identities of Theorem 2.7;
Kraus/Stinespring/Choi correspondences for finite-dimensional channels.

The SU(2) representation layer and the Choi-matrix covariance criterion are reusable beyond this mission. Proofs of the cited results (Theorem 2.7, Propositions 1.15 and 3.9) are welcome as independent contributions.

Selected references

M. Al Nuwairan, SU(2)-irreducibly covariant and EPOSIC channels, arXiv preprint, 2013. https://arxiv.org/abs/1306.5321
K. G. H. Vollbrecht and R. F. Werner, Entanglement measures under symmetry, Phys. Rev. A 64, 062307, 2001. https://arxiv.org/abs/quant-ph/0010095
C. Procesi, Lie Groups: An Approach through Invariants and Representations, Springer Universitext, 2007. https://doi.org/10.1007/978-0-387-28929-8
J. Watrous, The Theory of Quantum Information, Cambridge University Press, 2018. https://doi.org/10.1017/9781316848142

17 thms3 active usersReviewed

Linear algebra Quantum Information Representation Theory·Captain: mikedeng1

Commutant Structure of U⊗(n−1) ⊗ U* Transformations: The Operator Basis v^{ab}_{ij}(α) Is a Linear Combination of Partially Transposed Permutation Operators, and ConverselyResearch Paper

Motivation

Operators on $n$ copies of $\mathbb C^d$ that commute with every $U^{\otimes n}$ , $U$ unitary, are exactly the linear combinations of permutation operators $V(\sigma)$ , $\sigma\in S(n)$ (Schur–Weyl duality). Many protocols in quantum information carry a different symmetry: the first $n-1$ systems transform by $U$ and the last by the complex conjugate $\bar U$ . It is the symmetry of port-based teleportation (Ishizaka–Hiroshima 2008), whose optimal performance is computed from the representation theory of exactly this commutant (Studziński et al. 2017). The commutant of $U^{\otimes(n-1)}\otimes\bar U$ is the algebra $\mathcal A$ spanned by the partially transposed permutation operators $V'(\sigma)$ : the permutation operators with the transpose taken on the last system.

Studziński, Horodecki and Mozrzymas give an explicit operator basis of an ideal of $\mathcal A$ adapted to the irreducible representations of $S(n-2)$ . Their main structural result, Theorem 9, states that this basis and the partially transposed permutation operators are linear combinations of each other, with coefficients that are irrep matrix elements.

Setting

Let $\mathcal H=\mathbb C^d$ and $n\ge2$ . For $\sigma\in S(n)$ , the permutation operator $V(\sigma)$ on $\mathcal H^{\otimes n}$ is $V(\sigma)|i_1\dots i_n\rangle=|i_{\sigma^{-1}(1)}\dots i_{\sigma^{-1}(n)}\rangle$ . The partial transposition $X\mapsto X'$ transposes the last system: $(|x_1\dots x_n\rangle\langle y_1\dots y_n|)'=|x_1\dots x_{n-1}y_n\rangle\langle y_1\dots y_{n-1}x_n|$ . The algebra $\mathcal A$ is the span of all $V'(\tau)$ , $\tau\in S(n)$ . $S(k)$ is regarded inside $S(n)$ as the permutations fixing the systems after $k$ .

Fix $\pi_1,\dots,\pi_{n-1}\in S(n-1)$ with $\pi_k(n-1)=k$ , and write $\Pi_k=V(\pi_k)$ . For labels $a,b\in\{1,\dots,n-1\}$ , the maps $f_{ab}:S(n-2)\to S(n)$ are

f_{ab}(\sigma)=\pi_b\circ\sigma\circ(n\ n-1)\circ\pi_a^{-1}.

The standing data are a family of real orthogonal, irreducible, pairwise inequivalent matrix representations $\varphi^\alpha$ of $S(n-2)$ , of dimensions $d_\alpha$ , and a Schur basis: an orthonormal basis $|\phi_i(\alpha,r)\rangle$ of $\mathcal H^{\otimes(n-2)}$ , where $r$ ranges over the multiplicity of $\alpha$ , such that $V(\sigma)|\phi_j(\alpha,r)\rangle=\sum_i\varphi^\alpha_{ij}(\sigma)|\phi_i(\alpha,r)\rangle$ . With $|\Phi^+\rangle=\frac1{\sqrt d}\sum_l|ll\rangle$ on the last two systems, the paper defines

|\psi^k_i(\alpha,r)\rangle=\sqrt d\,\Pi_k|\phi_i(\alpha,r)\rangle|\Phi^+\rangle,\qquad v^{ab}_{ij}(\alpha)=\sum_r|\psi^a_i(\alpha,r)\rangle\langle\psi^b_j(\alpha,r)|,

and $E^\alpha_{ij}=\sum_r|\phi_i(\alpha,r)\rangle\langle\phi_j(\alpha,r)|$ . In Lean these are IrrepFamily, SchurBasis, psi, vOp, EOp, with ptLast for $'$ , fPerm for $f_{ab}$ and algA for $\mathcal A$ .

Formalization targets

Goal: Theorem 9

For all $a,b$ , $\alpha$ , $i,j$ :

v^{ab}_{ij}(\alpha)=\frac{d_\alpha}{(n-2)!}\sum_{\sigma\in S(n-2)}\varphi^\alpha_{ij}(\sigma)\,V'\big(f_{ba}(\sigma)\big)\in\mathcal A,

and for every $\sigma\in S(n-2)$ , with $\sigma_{ab}=f_{ab}(\sigma)$ ,

V'(\sigma_{ab})=\bigoplus_\alpha\sum_{i,j}\varphi^\alpha_{ij}\big(f_{ab}^{-1}(\sigma_{ab})\big)\,v^{ba}_{ij}(\alpha).

The goal is the whole theorem, both directions and the membership in $\mathcal A$ .

Milestones

Permutations of $S(n-1)$ are invariant under $'$ and pass through it: $V(\rho)V'(\tau)V(\rho')=V'(\rho\tau\rho')$ (proof of Lemma 26).
Lemma 26: $V'(\sigma_{ab})=\Pi_bV(f^{-1}_{ab}(\sigma_{ab}))V'(n\ n-1)\Pi_a^{-1}$ with $f^{-1}_{ab}(\sigma_{ab})\in S(n-2)$ .
Eq. (9): the $S_{ab}=f_{ab}(S(n-2))$ and $S(n-1)$ partition $S(n)$ , and each $f_{ab}$ is injective.
$V'(n-1,n)=\mathbb 1\otimes\sum_{l,l'}|ll\rangle\langle l'l'|$ .
Eq. (21): $E^\alpha_{ij}\in\mathbb C[S(n-2)]$ maps to $v^{ab}_{ij}(\alpha)=\Pi_a(E^\alpha_{ij}\otimes\mathbb 1)V'(n\ n-1)\Pi_b^{-1}\in\mathcal M$ .
Eq. (139): the orthogonality relation $\frac1{|G|}\sum_g\varphi^\alpha_{ij}(g)\varphi^\beta_{kp}(g^{-1})=\frac1{d_\alpha}\delta^{\alpha\beta}\delta_{ip}\delta_{jk}$ for $G=S(n-2)$ .
Eq. (86): $E^\alpha_{ij}=\frac{d_\alpha}{(n-2)!}\sum_\sigma\varphi^\alpha_{ij}(\sigma)V(\sigma)$ .
Eq. (86): $V(\sigma)=\bigoplus_\alpha\sum_{ij}\varphi^\alpha_{ij}(\sigma)E^\alpha_{ij}$ .

Significance

Theorem 9 shows that the $v^{ab}_{ij}(\alpha)$ span the same space as the operators $V'(\sigma)$ with $\sigma(n)\neq n$ . That space is the ideal of $\mathcal A$ on which the partial transposition acts non-trivially. Because the $v^{ab}_{ij}(\alpha)$ multiply like block matrices (Lemma 8 of the paper), the theorem converts questions about $\mathcal A$ into finite matrix computations indexed by irreps of $S(n-2)$ . The later constructions of the paper rest on this: the Gram matrices $Q(\alpha)$ , the biorthogonal basis and the explicit irreps of $\mathcal A$ . The same formalism underlies the eigenvalue analysis of port-based teleportation (Mozrzymas–Studziński–Horodecki 2018).

The result has a published proof but no machine-checked one. This mission adds that check, together with a reusable Lean vocabulary: the partial transpose on one site of $(\mathbb C^d)^{\otimes n}$ , the embeddings $S(k)\hookrightarrow S(n)$ , and Schur-basis data for permutation operators. It also pins down the conventions that the printed text leaves inconsistent (see Formalization scope).

Difficulty

The algebraic manipulations are short on paper; the work lies in the bookkeeping they hide. Lemma 26 requires checking that $\pi_b^{-1}\circ\sigma_{ab}\circ\pi_a\circ(n\ n-1)$ fixes both of the last two systems, which uses $\pi_k(n-1)=k$ in an essential way. The partial transposition is not multiplicative, so every step that moves an operator through $'$ needs the specific invariance of milestone 1. Eq. (86) is the identification of the Schur-basis matrix units with group-algebra elements; it needs completeness of the basis together with Schur's orthogonality relations for real irreps, and it is false without irreducibility and inequivalence. Mathlib has Schur's lemma but no coordinate form of the orthogonality relations for matrix representations, and nothing on partial transposes of tensor-power permutation operators.

Formalization scope

Indexing. The paper's $n$ is $m+2$ . $S(n-2)$ , $S(n-1)$ , $S(n)$ are Equiv.Perm (Fin m), Equiv.Perm (Fin (m+1)), Equiv.Perm (Fin (m+2)). Systems are 0-based, so systems $n-1,n$ are indices $m,m+1$ , and labels $a,b$ are Fin (m+1). Permutation products compose right to left.
Operators are complex matrices indexed by $\{1..d\}^k$ . $V(\sigma)$ is the published QAlgorithms.Schur.tensorPermutation. $'$ is on the last system only. groupAlg is the represented $\mathbb C[S(n-2)]$ ; algM spans the $V'(\tau)$ with $\tau(n)\ne n$ .
Standing data. IrrepFamily m contains real orthogonal matrix representations of $S(m)$ of positive dimension, irreducible over $\mathbb C$ and pairwise inequivalent over $\mathbb C$ (p. 7 and Notation 32 of the paper). SchurBasis F d is an orthonormal, spanning family of vectors on which $V(\sigma)$ acts by the $\varphi^\alpha$ . Multiplicities may be zero. The family is not required to list every irrep of $S(m)$ . Every $\pi_k$ satisfies $\pi_k(n-1)=k$ (Definition 24).
Constants are literal: $d_\alpha/(n-2)!$ , the factor $\sqrt d$ of $\psi$ and the $1/\sqrt d$ of $|\Phi^+\rangle$ . $\bigoplus_\alpha$ is a sum over all labels.
Ruled out. $v^{ab}_{ij}(\alpha)$ is defined from the vectors $\psi$ (Definition 5) and $E^\alpha_{ij}$ from the Schur basis (footnote 4). Neither is defined as a group sum or through $\mathcal F^t_{ab}$ , and the Schur basis carries no orthogonality relation. A formalization that builds (86) or (21) into the definitions makes Theorem 9 a tautology and is not this mission.
Source slips. Eq. (11) prints $\sigma_{ab}(n)=a$ , $\sigma^{-1}_{ab}[n]=b$ , contrary to Notation 1 and eq. (7); the Lean statements follow Notation 1 ( $\sigma_{ab}(a)=n$ , $\sigma_{ab}(n)=b$ ). Eq. (139) is stated with $1/|G|$ and a sum over $g$ , correcting the printed $1/n!$ and $\sum_h$ .
Welcome contributions: the coordinate Schur orthogonality relations for matrix representations of finite groups, and lemmas on ptLast and on liftPerm. Both are reusable beyond this paper.

Selected references

M. Studziński, M. Horodecki, M. Mozrzymas, Commutant structuture of $U^{\otimes(n-1)}\otimes U^*$ transformations, arXiv:1305.6183v2, 2013. https://arxiv.org/abs/1305.6183
S. Ishizaka, T. Hiroshima, Asymptotic teleportation scheme as a universal programmable quantum processor, Phys. Rev. Lett. 101, 240501, 2008. https://arxiv.org/abs/0807.4568
M. Studziński, S. Strelchuk, M. Mozrzymas, M. Horodecki, Port-based teleportation in arbitrary dimension, Sci. Rep. 7, 10871, 2017. https://arxiv.org/abs/1612.09260
M. Mozrzymas, M. Studziński, M. Horodecki, A simplified formalism of the algebra of partially transposed permutation operators with applications, J. Phys. A 51, 125202, 2018. https://arxiv.org/abs/1708.02434

11 thms3 active usersReviewed

Condensed Matter Physics Mathematical Physics Quantum Mechanics+1·Captain: mikedeng1

Density Matrix Numerical Renormalization Group for Non-Abelian Symmetries: Tracing Out a Site Keeps the Reduced Density Matrix Symmetric and Gives the dim(ĩ)/dim(u) Recursion for Its Kept BlockResearch Paper

Motivation

Wilson's numerical renormalization group (NRG) computes the low-energy states of quantum impurity models, such as the Kondo and Anderson models, by diagonalizing a semi-infinite chain one site at a time and keeping only the lowest multiplets after each step (Wilson 1975; review: Bulla, Costi, Pruschke 2008). Dynamical quantities (spectral functions, Green's functions) at finite temperature require, in addition, the reduced density matrix of each shorter chain, obtained by tracing the full density matrix over the sites that come later. This is the density matrix NRG (DM-NRG) (Hofstetter 2000), made exact with the complete basis of Anders and Schiller 2005.

Symmetries make NRG practical: when the Hamiltonian is invariant under a group, every iteration splits into blocks labelled by irreducible representations, and each multiplet is stored once instead of once per internal state. For non-Abelian groups (SU(2) spin, SU(2) charge, SU(3) channel symmetry) the saving is large, but only if the reduced density matrix can also be handled multiplet by multiplet. Tóth, Moca, Legeza and Zaránd (arXiv:0802.4332) show that it can, for essentially any symmetry: the reduced density matrix stays scalar under the symmetry after each tracing step, and its reduced matrix elements obey an explicit recursion, their eq. (45), whose only group-theoretic input is the ratio of multiplet dimensions.

Setting

A group $G$ acts on every multiplet through a labelled unitary irreducible representation: a label $Q$ has a dimension $\dim Q$ and unitary matrices $\pi_Q(g)$ of size $\dim Q$ , and states of a multiplet are indexed by an internal quantum number $Q^z\in\{0,\dots,\dim Q-1\}$ . Distinct labels carry inequivalent representations.

At iteration $n$ the new space is spanned by states $|u, Q^z_u;\mu, q^z_\mu\rangle$ , where $u\in K$ runs over the kept multiplets of iteration $n-1$ (block states, label $Q_u$ ) and $\mu\in\Lambda$ over the local multiplets of site $n$ (label $q_\mu$ ). The symmetry acts as

U(g) = V(g)\otimes L(g),\qquad V(g)=\bigoplus_{u\in K}\pi_{Q_u}(g),\quad L(g)=\bigoplus_{\mu\in\Lambda}\pi_{q_\mu}(g).

Generalized Clebsch–Gordan coefficients $\langle q\,q^z; Q\,Q^z\mid Q'\,Q'^z\rangle$ are, for each label $Q'$ in a coupling set of $(q,Q)$ , the entries of a matrix $C^{Q'}_{qQ}$ that is an isometry, intertwines $\pi_q\otimes\pi_Q$ with $\pi_{Q'}$ , and such that the $C C^\dagger$ sum to the identity. The canonical basis (21) is

|\tilde\imath, Q_{\tilde\imath}, Q^z_{\tilde\imath}\rangle = \sum_{Q^z_u, q^z_\mu}\langle q_\mu q^z_\mu; Q_u Q^z_u\mid Q_{\tilde\imath} Q^z_{\tilde\imath}\rangle\,|u, Q_u, Q^z_u;\mu, q_\mu, q^z_\mu\rangle,

one canonical multiplet $\tilde\imath = ((u,\mu),Q_{\tilde\imath})$ per kept multiplet, local multiplet and coupled label; one writes $\tilde\imath\Leftarrow u$ .

An operator $R$ on the new space is scalar if $U(g)RU(g)^\dagger = R$ for all $g$ . Its reduced matrix elements $\langle\tilde\imath\Vert\tilde R\Vert\tilde\jmath\rangle$ in the canonical basis are defined by $\langle\tilde\imath,Q^z\mid R\mid\tilde\jmath,Q^{z\prime}\rangle = \langle\tilde\imath\Vert\tilde R\Vert\tilde\jmath\rangle\,\delta_{Q_{\tilde\imath},Q_{\tilde\jmath}}\delta_{Q^z,Q^{z\prime}}$ . $\operatorname{Tr}_{\mathrm{site}}$ is the partial trace over the local states of site $n$ .

Formalization targets

Goal: one tracing step (§III, eqs. (42)–(45))

For every scalar $R$ : $\operatorname{Tr}_{\mathrm{site}}R$ is scalar under $V(g)$ ; $R$ has reduced matrix elements in the canonical basis; for kept multiplets $u,v$ with $Q_u=Q_v$ and every such family of reduced elements,

\langle u, Q^z\mid\operatorname{Tr}_{\mathrm{site}}R\mid v, Q^{z\prime}\rangle = \delta_{Q^z,Q^{z\prime}}\sum_{\mu}\ \sum_{\tilde\imath\Leftarrow(u,\mu)}\ \sum_{\tilde\jmath\Leftarrow(v,\mu)}\frac{\dim(\tilde\imath)}{\dim(u)}\,\langle\tilde\imath\Vert\tilde R\Vert\tilde\jmath\rangle\,\delta_{Q_{\tilde\imath},Q_{\tilde\jmath}};

and the entry vanishes when $Q_u\neq Q_v$ . The paper's truncated reduced density matrix $R^{[n]}$ of its eq. (38) is one instance of $R$ ; the statement fixes no Hamiltonian, energies or temperature.

Milestones

In proof order: the covariance of the partial trace (40); the invariance of $\operatorname{Tr}_{\mathrm{site}}R$ and of $R^{[n-1]}$ (39), (41)–(42); the Wigner–Eckart form of a scalar operator (43); orthonormality, completeness and the transformation law of the canonical basis (21); the Wigner–Eckart form in the canonical basis (44); and the Clebsch–Gordan sum rule that produces the factor $\dim Q'/\dim Q$ when the local states are traced out.

Significance

The recursion (45) computes the reduced density matrix of every iteration from that of the next, one number per pair of multiplets, so that all DM-NRG expectation values and spectral functions can be evaluated in the reduced (multiplet) representation. Its only group-dependent input is the dimension ratio $\dim(\tilde\imath)/\dim(u)$ ; the Clebsch–Gordan coefficients themselves drop out. This is what lets a DM-NRG code, such as the flexible code the paper describes, handle any number and type of symmetries without symmetry-specific density-matrix code.

The result is proved in the paper, in a few lines of physics notation that rely on the Wigner–Eckart theorem and on Clebsch–Gordan orthogonality. It has no machine-checked proof. The mission states it as a theorem about invariant matrices, unitary representations and Clebsch–Gordan isometries; its milestones include a Wigner–Eckart theorem for scalar operators on a space of labelled multiplets and a Clebsch–Gordan sum rule, both stated for an arbitrary group and reusable for other symmetry-adapted tensor-network and many-body computations.

Difficulty

The physics proof cites the Wigner–Eckart theorem; formally this is Schur's lemma in two forms: an equivariant map between inequivalent irreducible representations vanishes, and an equivariant endomorphism of an irreducible representation is a scalar. Neither is a hypothesis here, so both must be derived from irreducibility in its invariant-subspace form. The dimension factor is the second form applied to the partial trace of $CC^\dagger$ , together with a trace count. A direct computation from the definition of the canonical basis does not give (45): the Clebsch–Gordan coefficients are arbitrary matrices subject only to the three stated conditions, so no closed formula for them is available, and the dimension ratio appears only through the representation-theoretic argument. The bookkeeping is also non-trivial: internal quantum numbers of different multiplets live in different index types even when their labels coincide, and the tilde sum pairs canonical multiplets built with the same local multiplet.

Formalization scope

One abstract group $G$ with labelled irreducible unitary representations replaces the paper's product $G_1\times\dots\times G_\Gamma$ of eqs. (17)–(18); the product case is an instance, with the generalized Clebsch–Gordan coefficients of p. 4 as products. Irreducibility is Mathlib's Representation.IsIrreducible, inequivalence the emptiness of Representation.Equiv. The coupling is multiplicity-free, one Clebsch–Gordan matrix per label triple, exactly as (21) is written; with outer multiplicities (as in SU(3)) the printed (45) would need a multiplicity index. Operators on the new space are matrices indexed by (block, local) pairs, block first, and the partial trace over the site is the published WildeQIT.partialTraceRight; Clebsch–Gordan matrices are indexed local first. All index sets are finite. Internal quantum numbers of multiplets with equal labels are compared by their numerical value. No fermionic sign factors appear: the space is the tensor product in the ordering of (21), and (45) carries no sign.

The statement does not assume Schur's lemma, the Clebsch–Gordan sum rule, or a block form of $R$ ; the reduced matrix elements in (45) are not free parameters but any family satisfying the Wigner–Eckart identity for $R$ , whose existence is part of the goal. The Wilson chain, the complete basis and density matrix (32)–(38), the Green's function (46)–(48), the numerics of §V and the SU(2) appendix are outside the mission.

A complete development needs a usable Schur's lemma for matrix representations (Mathlib provides the module-theoretic version), Kronecker-product and block-diagonal matrix algebra, and partial-trace identities. Lemmas on partial traces of Kronecker products and on Wigner–Eckart for block-diagonal representations are reusable beyond this mission; contributions of either kind are welcome.

Selected references

A. I. Tóth, C. P. Moca, Ö. Legeza, G. Zaránd, Density matrix numerical renormalization group for non-Abelian symmetries, arXiv:0802.4332v1, 2008. https://arxiv.org/abs/0802.4332
K. G. Wilson, The renormalization group: Critical phenomena and the Kondo problem, Reviews of Modern Physics 47, 773, 1975. https://doi.org/10.1103/RevModPhys.47.773
W. Hofstetter, Generalized numerical renormalization group for dynamical quantities, Physical Review Letters 85, 1508, 2000. https://doi.org/10.1103/PhysRevLett.85.1508
F. B. Anders, A. Schiller, Real-time dynamics in quantum-impurity systems: a time-dependent numerical renormalization-group approach, Physical Review Letters 95, 196801, 2005. https://doi.org/10.1103/PhysRevLett.95.196801
R. Bulla, T. A. Costi, T. Pruschke, Numerical renormalization group method for quantum impurity systems, Reviews of Modern Physics 80, 395, 2008. https://arxiv.org/abs/cond-mat/0611651

9 thms3 active usersReviewed

Mathematical Physics Representation Theory·Captain: mikedeng1

Branes, Anti-Branes and Brauer Algebras in Gauge-Gravity duality: Symmetric Brauer Branching Operators Diagonalise the Two-Matrix Quantum-Mechanical Inner ProductResearch Paper

Motivation

Operators made from a complex matrix and its conjugate occur in the non-chiral sector of gauge theories. Their correlation functions involve many possible pairings of matrix entries, and those pairings become difficult to organize as the number of entries grows. Kimura and Ramgoolam use the walled Brauer algebra to label these operators and to describe their two-point functions in a basis adapted to both the tensor symmetries and the mixed fundamental–conjugate representation. The result targeted here is the orthogonality relation for that basis in the reduced two-matrix quantum mechanics Kimura and Ramgoolam, §7.1, p. 29.

The question is concrete: can the algebraic labels of an operator determine whether its state has zero inner product with another state, without expanding every matrix entry? Equation (7.12) says yes for the paper's symmetric branching operators. It is a known result in the cited paper. This mission asks for a machine-checked formalization of its precise tensor-space content, including the complex Gaussian covariance and the permutation sums on which the two-point function depends.

Setting

Let $V=\mathbb C^N$ , with basis indexed by $\operatorname{Fin}N$ . The mixed tensor space $V^{\otimes m}\otimes\bar V^{\otimes n}$ has a basis labelled by a pair of index tuples: an $m$ -tuple for the $V$ legs and an $n$ -tuple for the conjugate legs. Its operators are finite complex matrices; $\operatorname{tr}_{m,n}$ is their ordinary matrix trace. The group $S_m\times S_n$ permutes legs within each block. It is represented by matrices $P_{\sigma,\tau}$ , using the already published tensor-permutation definition used here.

A contraction $C_{i\bar j}$ pairs the $i$ th $V$ leg with the $j$ th conjugate leg. The image of the algebra generated by all such contractions and the $S_m\times S_n$ permutations is denoted $B_N(m,n)$ . This is the represented Brauer algebra used in the paper's tensor-space traces §3.2, pp. 8–9. The map $\Sigma$ exchanges the input and output indices of the conjugate block. In coordinates it is the partial transpose on that block; this matches the reflection shown in Figure 6 §3.3, pp. 11–12.

The paper's symmetric branching operators are denoted $Q^\gamma_{A,ij}$ . Here $\gamma$ labels a Brauer representation, $A$ an irreducible representation of $S_m\times S_n$ , and $i,j$ range over its multiplicity $M^\gamma_A$ . These operators belong to the represented Brauer algebra, are invariant under conjugation by every $P_{\sigma,\tau}$ , and obey the matrix-unit product $Q^{\gamma_1}_{A,ij}Q^{\gamma_2}_{B,kl}=\delta_{\gamma_1\gamma_2}\delta_{AB}\delta_{jk}Q^{\gamma_1}_{A,il}$ . The relation $(Q^\gamma_{A,ij})^\dagger=Q^\gamma_{A,ji}$ comes from their orthonormal-vector definition in (7.3) §7, pp. 27–28.

For two independent $N\times N$ complex matrices $Z_A,Z_B$ , put

f_X(Z_A,Z_B)=\operatorname{tr}_{m,n}\!\left(X\left(Z_A^{\otimes m}\otimes Z_B^{\otimes n}\right)\right), \qquad \langle X_2,X_1\rangle=\mathbb E\!\left[\overline{f_{X_2}(Z_A,Z_B)}f_{X_1}(Z_A,Z_B)\right].

Each matrix entry has independent real and imaginary parts of variance $1/2$ . This Bargmann–Fock Gaussian realization gives $\mathbb E|Z_{ij}|^2=1$ and reproduces the oscillator normalization of (7.8) p. 28.

Formalization targets

The goal is the orthogonality identity of (7.12), with the scalar written as a tensor-space trace:

\left\langle\Sigma(Q^{\gamma_2}_{A_2,i_2j_2}), \Sigma(Q^{\gamma_1}_{A_1,i_1j_1})\right\rangle =m!n!\,\delta_{\gamma_1\gamma_2}\delta_{A_1A_2} \delta_{i_1i_2}\delta_{j_1j_2} \operatorname{tr}_{m,n}(Q^{\gamma_1}_{A_1,j_1j_1}).

The paper writes the last factor as $d_{A_1}\operatorname{Dim}\gamma_1$ after invoking mixed-tensor Schur–Weyl duality. The trace version is the equality reached just before that last step in (7.13) p. 29. The mission's milestones cover the unit covariance (7.8), the Wick permutation formula of Figure 3, the trace sum in the second line of (7.13), symmetry preservation (3.37), the $m!n!$ collapse in the third line of (7.13), and the trace-pairing identity (3.20).

Significance

The formula assigns orthogonal states to different branching labels and multiplicity indices. It also fixes their norms by an explicit finite-dimensional trace. This makes the representation labels useful for organizing non-chiral two-point functions, rather than merely counting or naming operators §7, pp. 27–29. Without the Wick-to-trace identity, the same claim remains an expanding sum of matrix-entry pairings for each degree.

The paper proves the identity diagrammatically; this mission has no machine-checked proof of it yet. A completed formalization would give reusable finite-matrix interfaces for contractions, partial transpose, Gaussian polynomial states, and permutation-indexed Wick sums. The complex covariance and Wick results can be reused independently of the particular Brauer family. The represented algebra and branching interface can support later formalization of the paper's projectors and finite- $N$ examples.

Difficulty

The central obstacle is the passage from a Gaussian expectation of products of matrix entries to a sum of traces indexed by $S_m\times S_n$ . A direct expansion of the state polynomials creates many indices, and each Gaussian pairing must match the direction of the matrix entries and the inverse permutation in the tensor action. The $A$ and $B$ matrices are independent, so pairings cannot cross their blocks. After that conversion, the partial transpose and permutation symmetry must agree on the same index convention. A transposed covariance or reversed inverse produces a plausible looking expression with the wrong contractions.

Formalization scope

The Lean model uses finite matrices throughout, permits $N,m,n=0$ , and uses ordinary unnormalized traces. The index type is a pair of functions from $\operatorname{Fin}m$ and $\operatorname{Fin}n$ to $\operatorname{Fin}N$ ; its second component represents the conjugate legs. $\Sigma$ is the concrete partial transpose, and $B_N(m,n)$ is the image subalgebra generated inside the matrix algebra. The oscillator vacuum inner product is the Gaussian integral above, with two independent matrices and unit complex variance. It is defined from the measure, not from the Wick permutation formula. The measure's pushforward map is continuous. Matrix-entry polynomials have finite Gaussian moments, so the integral does not rely on Lean's default value for a non-integrable function.

The branching labels are abstract types, but each valid $Q^\gamma_{A,ij}$ must satisfy Brauer membership, the paper's symmetry and matrix-unit relations, and the adjoint relation derived from (7.3). Indices are natural numbers with explicit range conditions $i,j<M^\gamma_A$ . No completeness axiom, positivity condition, or lower bound on $N$ is added. These declarations exclude a trivialized inner product defined as the target permutation sum. The coefficient $d_A\operatorname{Dim}\gamma$ and the four-dimensional, normal-ordered version (7.16) are outside this mission. Contributions to the Gaussian Wick conversion, the partial-transpose trace identity, and the symmetric branching calculation are all in scope.

Selected references

Y. Kimura and S. Ramgoolam, Branes, Anti-Branes and Brauer Algebras in Gauge-Gravity duality, JHEP 11 (2007) 078; arXiv:0709.2158v2. The mission cites the version 2 preprint's printed page and equation numbers.

10 thms3 active usersReviewed

Linear algebra Quantum Information·Captain: mikedeng1

On a Family of a Linear Maps from Mₙ(ℂ) to Mₙ²(ℂ): Φ[α, β] on M₃(ℂ) Is 2-Positive and Not Completely Positive Exactly When β ≤ −0.2 and α Lies in an Explicit IntervalResearch Paper

Motivation

Positive linear maps on complex matrix algebras provide tests for quantum entanglement: applying such a map to one part of a bipartite state can expose a state that cannot be written as a mixture of product states. The distinction between ordinary positivity, positivity with an auxiliary matrix system, and complete positivity is therefore substantive. Collins, Osaka, and Sapra study an explicit two-parameter family that makes these distinctions visible through inequalities in the parameters. Their paper identifies the exact region where a map from three-by-three matrices to nine-by-nine matrices is 2-positive but fails to be completely positive. This is the stated main result of their 2018 paper, rather than an open conjecture.

Setting

Write $M_n(\mathbb C)$ for the algebra of $n\times n$ complex matrices. A matrix $X$ is positive semidefinite, written $X\geq0$ , when it is Hermitian and has no negative eigenvalues. A complex-linear map $\Psi:M_{d_1}(\mathbb C)\to M_{d_2}(\mathbb C)$ is positive when $X\geq0$ implies $\Psi(X)\geq0$ . It is $k$ -positive when the same condition holds after the identity map on $M_k(\mathbb C)$ is tensored with $\Psi$ . It is completely positive when it is $k$ -positive for every $k$ . A map is completely copositive when its composition with transpose on the source is completely positive. These are the paper's definitions on page 2.

Let $B_n=\sum_{i=1}^n e_i\otimes e_i$ be the unnormalized Bell vector, and let $B_{n^2}=B_nB_n^*$ denote its rank-one projector. For real $\alpha,\beta$ and $n\geq3$ , the family on page 3 is

\Phi_{\alpha,\beta,n}(A) =A^{\mathsf T}\otimes I_n+I_n\otimes A +\operatorname{Tr}(A)\bigl(\alpha I_{n^2}+\beta B_{n^2}\bigr).

The transpose belongs to the first tensor factor. The mission concentrates on $\Phi[\alpha,\beta]=\Phi_{\alpha,\beta,3}$ . Its Choi matrix is $C_\Psi=\sum_{i,j}e_{ij}\otimes\Psi(e_{ij})$ . For this finite-dimensional setting, the Choi criterion relates complete positivity to $C_\Psi\geq0$ ; it does not define complete positivity. The paper also identifies an equivariance property: unitary conjugation of the input corresponds to conjugation of the output by a matrix associated with the same unitary.

Formalization targets

For $\beta\in\mathbb R$ , define two boundary curves and a cubic root:

\ell_P(\beta)=\frac{-(2+3\beta)+\sqrt{9\beta^2-4\beta+4}}2, \qquad \ell_{CP}(\beta)=\frac{-(3+3\beta)+\sqrt{9\beta^2-10\beta+17}}2,

S_\beta=\min\{x\in\mathbb R:x^3+(-2-3\beta)x^2+(-2+4\beta)x+2\beta=0\}.

The goal is Theorem 3.9, page 10:

\Phi[\alpha,\beta]\text{ is 2-positive and not completely positive} \quad\Longleftrightarrow\quad \beta\leq-\tfrac15, \quad\alpha\in[\ell_P(\beta),\ell_{CP}(\beta)) \cap[1,\infty)\cap[-S_\beta,\infty).

The left endpoint of the first interval is included and the right endpoint is excluded. The milestones record the paper's earlier criteria for positivity, complete positivity, and 2-positivity, together with its general equivariance criterion and the computation for this family. Their inequalities are separate targets; none is built into the definitions of these map properties.

Significance

The goal gives an exact, parameter-level example of 2-positivity without complete positivity. It identifies all such members of this family on $M_3(\mathbb C)$ , including the boundary cases, rather than only exhibiting one map. The surrounding results locate the positive and completely positive regions and give a criterion for testing $k$ -positivity of equivariant maps. Together, they provide a compact source of concrete maps with different strengths of positivity, as described in Sections 2 and 3 of the paper.

The mathematical result was proved in 2018. This mission seeks a machine-checked account of the stated criteria, with the family, Choi matrix, Bell projector, and positivity predicates exposed as reusable declarations. A finished proof would connect elementary matrix positivity and tensor products to explicit real-algebraic parameter bounds. It would also make each boundary independently inspectable. The Lean theorem statements here are draft targets with sorry; they are not existing machine-checked proofs of the paper.

Difficulty

Testing only $\Phi[\alpha,\beta](e_{11})\geq0$ yields ordinary positivity, not 2-positivity. Testing only the Choi matrix addresses complete positivity, which is stronger than the desired property. The 2-positive condition quantifies over every positive semidefinite matrix in $M_2(\mathbb C)\otimes M_3(\mathbb C)$ ; the paper's criterion reduces that universal condition under equivariance to positivity of a specific block matrix. The block matrix has parameter-dependent eigenvalues, including roots of a cubic. This makes a simple comparison of the two square-root boundary curves insufficient: the smallest cubic root supplies an additional lower bound on $\alpha$ . The endpoint $\beta=-1/5$ also needs attention because the case descriptions for complete positivity meet there.

Formalization scope

The Lean model uses Matrix (Fin n) (Fin n) ℂ for $M_n(\mathbb C)$ and Fin n × Fin n for the output tensor indices, with the first coordinate corresponding to the transposed factor. The paper's one-based $e_{11}$ is Matrix.single 0 0 1. Positive semidefiniteness is Mathlib's Matrix.PosSemidef. The shared QAlgorithms.idTensorSuperop applies a map blockwise with the auxiliary index first, and the published QAlgorithms.Entanglement.IsCompletelyPositive quantifies over all auxiliary sizes. Size zero is harmless for that quantifier because the corresponding matrix type is empty. The paper's $n\geq3$ appears on the general-family results; the main goal fixes $n=3$ .

The Bell projector is unnormalized, matching the paper's $B_nB_n^*$ . The two square roots have positive radicands on the real parameter range. The cubic root $S_\beta$ is defined as the infimum of its real root set; the odd-degree cubic has a nonempty, finite set of real roots, so this is its least root. The proof development needs reusable facts about unitary conjugation of positive matrices, Kronecker products, Choi matrices, and positivity of the parameterized block matrix. Direct calculations of the boundary inequalities are also welcome. Defining $k$ -positivity by the block criterion, complete positivity by Choi positivity, omitting the transpose in $\Phi$ , or treating $S_\beta$ as an arbitrary parameter would make the targets lose their intended content.

Selected references

Benoît Collins, Hiroyuki Osaka, and Gunjan Sapra, On a family of a linear maps from Mn(C) to Mn2(C), Linear Algebra and its Applications, 2018; cited here from arXiv:1802.07553v1, pp. 2–10.

12 thms3 active usersReviewed

Machine Learning Probability·Captain: mikedeng1

Speculative Actions: A Lossless Framework for Faster Agentic Systems: Exact Expected Runtime Ratio of k-Branch Speculation Under Exponential LatenciesResearch Paper

Motivation

An agentic system may make several slow API calls in sequence: the answer to one call determines what to request next. A speculator can guess the current answer while the real call is running and start likely next calls early. When a guess is correct, the system can reuse a pending result; when it is wrong, it discards that result. This can shorten a run if concurrent calls do not interfere and incorrect calls have no lasting side effects. Ye and coauthors introduce this execution scheme for language-model and tool-using agents in Speculative Actions, §2.

The paper's Proposition 1 quantifies the expected latency of one-step speculation with exponential call times. Its proof in Appendix A states a stochastic timing model and computes a finite-horizon runtime ratio and its limit. The first author's existing Prove2Me mission, Speculative Actions: Cost-Latency Analysis for Agentic Speculation, contains proved algebraic identities for expressions named specTime and seqTime. Those expressions encode the values claimed for the expectations. This mission supplies the missing connection between random executions and those expressions, while reusing the published algebra.

Setting

There are $T$ real API calls, numbered $0$ through $T-1$ . The real-call latency of step $t$ is $B_t$ with exponential rate $\beta$ . At a speculation window during step $t$ , a speculator has latency $A_t$ with exponential rate $\alpha$ . It produces $k$ candidate next calls. Each candidate independently matches the actual next call with probability $p$ , so a hit means that at least one of the $k$ candidates matches. The hit probability is

p(k)=1-(1-p)^k.

All latencies and branch-correctness indicators are mutually independent. Proposition 1 assumes $0<\beta<\alpha$ and Assumption 1 gives $p>0$ ; as a probability, $p\le1$ . Assumption 2 permits concurrent API calls and reversible or side-effect-free pre-launching. The theorem also treats state transitions and construction of API parameters as having negligible duration. These conditions and the exponential laws are stated in §2 and Proposition 1.

The sequential runtime $T_{\mathrm{seq}}$ is $\sum_{t<T}B_t$ . The speculative runtime $T_s$ follows Appendix A's timing rule. At a window without a hit, the current step costs $B_t$ . At a hit, the block comprising steps $t$ and $t+1$ costs $\min(A_t,B_t)+B_{t+1}$ , and step $t+1$ opens no window. The last step cannot open a window. This is the model used in the paper's proof of Proposition 1, Appendix A, pp. 14–15. Its precise timing rule matters: reading Algorithm 1's awaits literally gives a different timeline, as does waiting for validation before accepting an early next-step result.

Let $S_n$ be the expected number of hits in $n$ potential windows, with a hit consuming the following window. The paper gives $S_0=0$ , $S_1=p(k)$ , and

S_n=p(k)(1+S_{n-2})+(1-p(k))S_{n-1}\qquad(n\ge2).

Formalization targets

Random-runtime identities

The new milestones identify the expectation of the sequential runtime, the saving from one correct speculation, and the expected hit count. The total-saving identity is

\mathbb E[T_s]=\frac{T}{\beta}-S_{T-1}\frac{\alpha}{\beta(\alpha+\beta)},\qquad T\ge1.

Here $S_{T-1}$ is the expectation of the random count defined by the execution model. The previously published expression SpecActions.specTime has this same algebraic form; proving equality with the integral of the random runtime is the new step. The closed form for $S_n$ and the algebraic ratio are linked as published milestones.

Proposition 1

For every integer $T\ge1$ , the goal is the Proposition 1 ratio for the actual expectations:

\frac{\mathbb E[T_s]}{\mathbb E[T_{\mathrm{seq}}]}=1-\frac1T\frac{\alpha}{\alpha+\beta}\left[\frac{(T-1)p(k)}{1+p(k)}+\frac{p(k)^2}{(1+p(k))^2}-\frac{p(k)^2}{(1+p(k))^2}(-p(k))^{T-1}\right].

The same goal states convergence of this random-runtime ratio as $T\to\infty$ to

1-\frac{p(k)}{1+p(k)}\frac{\alpha}{\alpha+\beta}.

The horizon condition protects the denominator: at $T=0$ , the sequential runtime is zero. The number of branches may be zero; then $p(0)=0$ and the ratio is one for positive horizons.

Significance

The formula describes how breadth $k$ , branch accuracy $p$ , and the two latency rates affect expected completion time, both for a finite sequence of calls and in a long run. It makes the expected benefit of extra branches a quantity that can be compared with their resource cost. The paper uses the time expression again in its cost–latency discussion, including Theorem 5, p. 20.

The author's existing mission has machine-checked proofs for the recurrence's closed form and for algebraic identities involving specTime and seqTime. It does not prove that those expressions are expectations of a random execution. Completing this mission adds that probabilistic interpretation and a reusable model of independent calls, branch indicators, skipped windows, and runtime. The proposed stochastic theorems remain open; their statements compile, while the published reference results are already proved.

Difficulty

The main issue is the dependence created by skipping a window after a hit. Hit indicators at different windows are independent, but the number of opportunities actually used is determined by earlier outcomes. Treating the hit count as an ordinary binomial count gives the wrong recurrence. Likewise, multiplying a mean saving by the number of potential windows ignores that skipped windows cannot hit. A formal proof must relate the random execution and hit count while preserving the independence between correctness indicators and latencies.

Formalization scope

Lean represents all primitive random variables on one probability space. An index type separates speculator latency, real-call latency, and each of the $k$ branch indicators at every window. IsSpecModel requires measurable variables, their exponential or real-valued Bernoulli laws, and mutual independence. A hit is an existential statement over the $k$ branch indicators. The runtimes and hit count are recursions on a finite horizon, and expectation is the real Bochner integral. The model has an explicit construction on a product probability space, so its hypotheses are satisfiable.

Windows start at index zero: a $T$ -step run has $T-1$ potential windows. The theorem keeps the paper's $\beta<\alpha$ and $p>0$ conditions, and specifies $p\le1$ . It adds $T\ge1$ wherever a runtime ratio is divided by its sequential denominator. Concurrency without interference and negligible non-call work are represented by the timing recurrence. The claim concerns integrals of those random runtimes; defining an “expected runtime” directly by the paper's closed form would omit the target of this mission.

The definition layer and hit-probability, baseline, saving, hit-count, and total-saving milestones are available as separate contributions. Mathlib supplies exponential probability measures, product measures, independence, and integration; the published SpecActions definition and algebraic theorems are referenced. Work on the probabilistic bridges, integrability, and the final composition is within scope.

Selected references

N. Ye, A. Ahuja, G. Liargkovas, Y. Lu, K. Kaffes, and T. Peng, Speculative Actions: A Lossless Framework for Faster Agentic Systems, arXiv preprint arXiv:2510.04371v2, 2026. arXiv

13 thms3 active usersReviewed

Economics Operations Research·Captain: mikedeng1

Sales Information Transparency and Trust in Repeated Vertical Relationships: Sharing Past Sales Information Benefits the Retailer if and only if Its Discount Factor Is at Most 1/(1+√(1+p))Research Paper

Why past sales information matters in a repeated supply relationship

A manufacturer that sells through a retailer usually knows less about end-customer demand than the retailer does. In the classical one-shot screening model (Laffont and Martimort, 2002) the manufacturer offers a menu of quantity–payment pairs, pays the well-informed retailer an information rent to reveal high demand, and distorts the low-demand quantity downward to keep that rent small. Real vertical relationships are repeated, and after each selling season the retailer can choose whether to share its past sales data (point-of-sale data, sell-through reports) with the manufacturer. Such data says nothing about future demand when demand is i.i.d., yet it lets the manufacturer check, after the fact, whether the retailer reported truthfully.

Shamir and Yehezkel (2023) ask when the retailer, who owns the data, wants to share it. The manufacturer can never lose from more information, since it can ignore it. The retailer's side is the interesting one: sharing lets the manufacturer punish misreports and so cut the retailer's rent for a given quantity, but it also lets the manufacturer raise the low-demand quantity, which increases the rent. The paper's main result, Proposition 3, gives an explicit threshold on the discount factor that separates the two cases. The question belongs to the literature on trust and information sharing in supply chains (for example Özer, Zheng and Chen, 2011).

The model

In every period demand is high ( $H$ ) with probability $p$ and low ( $L$ ) with probability $1-p$ , independently across periods. The inverse demand is linear, $P(q;\theta) = V_\theta - q$ with $V_H > V_L$ , so the retailer's revenue from quantity $q$ in state $\theta$ is $\pi_R(q;\theta) = (V_\theta - q)q$ , and $\Delta(q) = \pi_R(q;H) - \pi_R(q;L)$ . The retailer observes the state before ordering; the manufacturer does not.

The manufacturer offers a menu $\{(q_H,T_H),(q_L,T_L)\}$ : quantity $q_\theta$ for the payment $T_\theta$ . The per-period expected profits are

\Pi_R = p(\pi_R(q_H;H) - T_H) + (1-p)(\pi_R(q_L;L) - T_L), \qquad \Pi_M = pT_H + (1-p)T_L.

Both firms discount future periods by $\delta$ .

In the static problem the manufacturer maximizes $\Pi_M$ subject to participation $\pi_R(q_\theta;\theta) - T_\theta \ge 0$ and incentive compatibility $\pi_R(q_\theta;\theta) - T_\theta \ge \pi_R(q_{\tilde\theta};\theta) - T_{\tilde\theta}$ . Its solution has $q^S_H = V_H/2$ and $q^S_L = \frac{V_L}{2} - \frac{p}{1-p}\frac{V_H - V_L}{2}$ , and the retailer's expected profit is $\Pi^S_R = p\Delta(q^S_L)$ . The paper assumes $pV_H < V_L$ , so that $q^S_L > 0$ .

In the repeated game, the manufacturer offers the same menu every period and reverts to the static menu forever after a deviation. The dynamic participation constraint, common to both regimes, is

\pi_R(q_\theta;\theta) - T_\theta + \tfrac{\delta}{1-\delta}\Pi_R \ \ge\ \tfrac{\delta}{1-\delta}p\Delta(q^S_L).

Without sales information a misreport cannot be detected, so incentive compatibility stays static. With sales information a misreport is detected at the end of the period and punished:

\pi_R(q_\theta;\theta) - T_\theta + \tfrac{\delta}{1-\delta}\Pi_R \ \ge\ \pi_R(q_{\tilde\theta};\theta) - T_{\tilde\theta} + \tfrac{\delta}{1-\delta}p\Delta(q^S_L).

In each regime the manufacturer chooses a menu that maximizes $\Pi_M$ among all menus satisfying that regime's constraints. Write $\Pi^{D,ne}_R$ and $\Pi^{D,e}_R$ for the retailer's expected profit at the optimal menu without and with sales information.

Formalization targets

Goal: Proposition 3

For $0<p<1$ , $V_L<V_H$ , $pV_H<V_L$ and $0\le\delta<1$ , and for every optimal menu of each program,

\Pi^{D,e}_R \ \ge\ \Pi^{D,ne}_R \quad\Longleftrightarrow\quad \delta \ \le\ \tilde\delta = \frac{1}{1+\sqrt{1+p}}.

Milestones

The static optimal menu (4)–(5), and $\Pi^S_R = p\Delta(q^S_L)$ .
Without sales information: the transfers that make the low-state participation and high-state incentive constraints bind, (27), and the reduced profit (10); the other two constraints are slack (Appendix C).
Proposition 1: the unique optimal no-sharing menu (11)–(12).
The retailer's no-sharing profit (15).
With sales information: the binding transfers (29), the reduced profit (19), and slackness of the other constraints (Appendix C).
Proposition 2: the unique optimal sharing menu (20)–(21).
The retailer's sharing profit (30) and the gap (31),

\Pi^{D,e}_R - \Pi^{D,ne}_R = \frac{\delta p^3(1-\delta)(V_H - V_L)^2}{2(1-p)(1+\delta p)^2}\,\big[1 - \delta(2+\delta p)\big].

Significance

Proposition 3 answers the paper's central question: sharing past sales data can arise voluntarily, and it does so exactly when the retailer is impatient enough, $\delta \le \tilde\delta$ . For patient retailers the repeated relationship already sustains a large low-demand quantity without verification, and the retailer loses more rent from detection than it gains from the higher quantity. Since the manufacturer always gains, $\delta \le \tilde\delta$ is also the region where sharing is a Pareto improvement for the channel. The threshold depends on $p$ alone, not on $V_H$ or $V_L$ .

The results are proved in the paper by first-order conditions on the reduced profits and direct substitution. Nothing in this mission is machine-checked yet. The formalization would turn the paper's chain (binding constraints, slack constraints, reduced profit, maximizer, retailer profit, sign of the gap) into one verified argument, including the step the paper treats informally: that the relaxed program with two binding constraints has the same optimum as the full four-constraint program, and that the optimum is unique.

Difficulty

The algebra of (15), (30) and (31) is long but mechanical. The substantive step is optimality over all menus. The paper drops two of the four constraints, solves the remaining two with equality, and maximizes the resulting quadratic. A rigorous version must show that no feasible menu, at any quantities, earns more than the reduced profit, that the reduced profit has a unique maximizer, and that the two dropped constraints hold at the candidate (Appendix C). Proposition 3 itself is stated about any optimal menu, so it needs uniqueness, not only existence, before the closed forms can be substituted. The naive route of evaluating (31) at the closed-form menus proves the comparison only for those menus, not for the optimum of the program.

Formalization scope

Everything is over $\mathbb R$ with the linear demand of the paper. Parameters form a structure Params with fields p, VH, VL, δ; the predicate Params.Standing collects $0<p<1$ , $V_L<V_H$ , $pV_H<V_L$ (footnote 2 of the paper) and $0\le\delta<1$ . The bound $\delta<1$ is added to the paper's $0\le\delta\le1$ because the constraints divide by $1-\delta$ . A menu is a structure Menu with fields qH, TH, qL, TL; every program also requires $q_H, q_L \ge 0$ , a condition that does not bind at the optima. Constraints are weak inequalities as printed. "Optimal" means feasible and maximizing $pT_H + (1-p)T_L$ over all feasible menus (IsOptimalNE, IsOptimalE). The retailer's profit is the ex-ante per-period $\Pi_R$ , not the discounted sum.

The goal must not be stated at the closed-form menus menuNE, menuE: that version is the algebraic identity (31) and skips the optimization entirely. Likewise the retailer's profit is defined from the menu, never by the formulas (15) or (30).

All definitions live in one file, SalesTrust.Sharing.Model. Contributions are welcome on any milestone; the two relaxation arguments (milestones 2 and 5 with Appendix C) and the uniqueness parts of Propositions 1 and 2 are where the work is. The relaxation step is common to two-type screening models, so a general statement of it would be reusable beyond this mission.

Selected references

N. Shamir and Y. Yehezkel, Sales Information Transparency and Trust in Repeated Vertical Relationships, Manufacturing & Service Operations Management, 2023. https://doi.org/10.1287/msom.2023.1208
J.-J. Laffont and D. Martimort, The Theory of Incentives: The Principal-Agent Model, Princeton University Press, 2002. https://doi.org/10.1515/9781400829453
Ö. Özer, Y. Zheng and K.-Y. Chen, Trust in Forecast Information Sharing, Management Science 57(6), 2011. https://doi.org/10.1287/mnsc.1110.1348

12 thms3 active usersReviewed

Convex Optimization Economics Optimization·Captain: mikedeng1

Discrete Choice Prox-Functions on the Simplex: The Convex Conjugate of an Additive Random Utility Surplus Function Is a Prox-Function on the SimplexResearch Paper

Motivation

Prox-functions determine how subgradient and mirror-type optimization methods turn a direction of improvement into the next feasible point. On a probability simplex, that step should respect the geometry of probability vectors and be computable from the current direction. The entropic prox-function gives the softmax rule, familiar from the logit model of discrete choice. Müller, Nesterov and Shikhman ask whether a wider family of random-utility choice models supplies prox-functions with the same operational link between optimization and choice probabilities. Their 2019 preprint, published in Mathematics of Operations Research in 2022, states that it does: the convex conjugate of the model's surplus is a prox-function on the simplex.

This question matters to optimization because the random-utility law specifies a geometry and a computable update together. It matters to discrete-choice modeling because the update from an optimization problem can be interpreted as a vector of probabilities of choosing each alternative. The mission covers the general result in Section 2 of the preprint, rather than its later specialized generalized-extreme-value parameters or economic application.

Setting

There are $n\ge1$ alternatives. A deterministic utility vector $u\in\mathbb R^n$ is perturbed by a random shock vector $\epsilon\in\mathbb R^n$ with law $\mu$ . Assumption 1 requires a finite mean, absolute continuity with respect to Lebesgue measure, and full support in $\mathbb R^n$ . The surplus function is the expected best perturbed utility,

E(u)=\mathbb E_\mu\!\left[\max_{1\le i\le n}\bigl(u_i+\epsilon_i\bigr)\right].

The convex conjugate of this function is taken over every utility vector, with extended-real values:

E^*(p)=\sup_{u\in\mathbb R^n}\{\langle p,u\rangle-E(u)\},\qquad \langle p,u\rangle=\sum_i p_i u_i.

The candidate domain is the simplex $\Delta=\{p\in\mathbb R^n:p_i\ge0,\ \sum_i p_i=1\}$ . The model's choice probability $P_i(u)$ is the chance that $u_i+\epsilon_i$ attains the largest perturbed utility. Absolute continuity makes ties null, so including ties in this event does not change its probability. The paper identifies $P_i(u)$ with the $i$ th derivative of $E$ in equation (1).

A prox-function on $\Delta$ is continuous and strongly convex there, and the optimization step that maximizes $\langle p,u\rangle-E^*(p)$ over $p\in\Delta$ has a unique, directly available answer. Here strong convexity uses $\|p-q\|_1=\sum_i|p_i-q_i|$ . The relevant smoothness of $E$ uses the dual norm $\|u\|_\infty=\max_i|u_i|$ .

Formalization targets

The goal combines the three claims that form the paper's Section 2 main result. First, Theorem 1 says that the finite domain of $E^*$ is exactly $\Delta$ , and that $E^*$ is continuous even at the boundary of that simplex. Second, Theorem 2 supplies an explicit strong-convexity parameter. For distinct alternatives $i,j$ , let $g_{ij}$ be a density of $\epsilon_j-\epsilon_i$ and let $\bar z_{ij}$ be a mode of that density. Then

E^*(\alpha p+(1-\alpha)q)\le \alpha E^*(p)+(1-\alpha)E^*(q) -\frac{\beta}{2}\alpha(1-\alpha)\|p-q\|_1^2, \quad \beta=\frac{1}{2\sum_i\sum_{j\ne i}g_{ij}(\bar z_{ij})}

for $p,q\in\Delta$ and $\alpha\in[0,1]$ . The double sum is over ordered pairs. Third, under the strong-convexity premise stated at the opening of §2.2.3, Theorem 4 identifies the optimizer and the attained value:

\underset{p\in\Delta}{\operatorname{argmax}} \bigl(\langle p,u\rangle-E^*(p)\bigr)=P(u), \qquad \max_{p\in\Delta}\bigl(\langle p,u\rangle-E^*(p)\bigr)=E(u).

The milestones record Lemmas 1, 2, 3 and 5, equation (1), and Theorems 1, 2 and 4. They cover the paper's elementary surplus properties, the choice-probability identity, the relation between strong convexity and strong smoothness, the Hessian norm criterion, the matrix trace bound, and the three final clauses.

Significance

The result gives a family of simplex prox-functions indexed by shock laws, rather than by a single entropy formula. The optimizer in the auxiliary problem is a choice-probability vector, so a prox update has an explicit behavioral interpretation. The strong-convexity bound supplies the geometric constant used when such a function enters first-order optimization estimates. The paper's later sections derive parameters for generalized extreme-value models and apply the update to a consumption cycle; those consequences motivate the general theorem but are outside this mission's goal.

The result is proved in the cited paper; this mission asks for its Lean formalization. The current draft has compile-checked statements with proof placeholders. A complete development would add machine-checked proofs of the listed lemmas and goal, together with reusable results about conjugacy, probability laws of differences, and norms of finite matrices. No proof of this specific paper result is claimed here.

Difficulty

Continuity in the relative interior of a simplex does not by itself establish continuity at its boundary, which is part of Theorem 1. The choice-probability formula connects differentiation of an expected maximum with an event defined by inequalities; ties, measurability, and integrability must all be handled. The strong-convexity constant then depends on controlling the Hessian with the norm induced from $\ell_\infty$ to $\ell_1$ , while retaining the ordered-pair sum of density values. A direct substitution of the default norm on finite coordinate functions would change the theorem because that norm is $\ell_\infty$ .

Formalization scope

Alternatives are Fin n with [NeZero n]; vectors are Fin n → ℝ. The law $\mu$ is a probability measure on shock vectors. Assumption 1 explicitly includes coordinate integrability, absolute continuity and full support. Its integrability clause keeps the Bochner integral defining $E$ meaningful, rather than allowing the integral's default value on a nonintegrable function. The choice event includes ties, which have zero measure under Assumption 1. The conjugate is EReal valued and takes its supremum over all utility vectors; defining it by a maximum over the simplex or by an entropy formula would change the result.

The real value of $E^*$ is used only alongside its finiteness on $\Delta$ . Strong convexity uses an explicit $\ell_1$ sum, while Mathlib's norm on Fin n → ℝ represents $\ell_\infty$ . Coordinate derivatives and the Hessian are formed from Fréchet derivatives. The differences $\epsilon_j-\epsilon_i$ have fixed, nonnegative measurable density versions tied to their pushforward laws; each mode maximizes its selected version pointwise. Theorem 4 carries the positive strong-convexity premise stated in its section preamble. The paper uses twice differentiability of $E$ on page 7 without deriving it from Assumption 1. This mission explicitly adds ContDiff ℝ 2 E to the Hessian-dependent result and the goal. It is a necessary disclosed strengthening of the paper's stated assumptions.

For one alternative the simplex is a point, and the displayed denominator in $\beta$ is zero. Lean evaluates the reciprocal as zero. The strong-convexity inequality is then vacuous between distinct points; the draft asserts positivity of the displayed $\beta$ only when $n\ge2$ and separately asserts that some positive parameter exists for every $n\ge1$ , as Definition 1 requires. No empty set of alternatives is admitted. Contributions should keep the unrestricted conjugate, the law-dependent densities, the exact $\ell_1$ inequality, and the paper's constants. General finite-dimensional convex duality and induced matrix-norm lemmas would be reusable beyond this model.

Selected references

D. Müller, Yu. Nesterov and V. Shikhman, Discrete choice prox-functions on the simplex, arXiv:1909.05591v1, 2019; published in Mathematics of Operations Research, 2022. Preprint.

10 thms3 active usersReviewed

Dynamic Programming Economics Markov Chain+1·Captain: mikedeng1

An Analysis of “Buy X, Get One Free” Reward Programs: Without Transaction Utility, a Redemption Threshold Alone Cannot Raise the Firm's Long-Run Profit Above max{λqv, λ(v − v̄)}Research Paper

Why reward programs that give away a free unit

"Buy $X$ , get one free" (BXGO) programs are among the most common loyalty schemes: coffee shops, car washes, golf courses and hotel chains hand out a free unit after a fixed number of paid purchases. A long empirical literature documents that such programs change behaviour, most visibly through point pressure, the acceleration of purchases as a customer approaches the redemption threshold (Kopalle et al. 2012; Lewis 2004). Whether that acceleration is worth the free units given away is a question for the firm's pricing and marketing operations.

Liu, Sun and Zhang (2021) study the question in a fully rational model. A forward-looking consumer facing a BXGO program solves a dynamic program, and her optimal decisions induce a Markov chain on her point inventory. The paper shows that discounting alone produces point pressure, and then asks whether the program raises the firm's long-run profit. Its answer without transaction utility (the consumer's extra enjoyment of a free unit) is negative under explicit conditions: Proposition 3. This mission formalizes that result together with the structural lemmas its proof rests on.

Setting

A monopolist sells a nondurable product at marginal cost $0$ , so revenue and profit coincide. A BXGO program is a pair $(p,X)$ : a fixed price $p$ and a threshold $X\ge1$ . A consumer earns one point per purchase, and holding $X$ points she may redeem them for a free unit, returning to $0$ points.

In each period the consumer is in the market with probability $\lambda$ . In the market she values the product at $v$ and has an outside option $v_0$ , equal to $0$ with probability $q$ and to $\bar v$ otherwise, where $v\ge\bar v\ge0$ . A redemption gives her a transaction utility $k\ge0$ on top of $v$ . She discounts with factor $\delta\in(0,1)$ .

Her value function $J$ on the point inventories $x\in\{0,\dots,X\}$ solves the optimality equations

J(x)=\lambda q\max\{v-p+\delta J(x+1),\delta J(x)\}+\lambda(1-q)\max\{v-p+\delta J(x+1),\bar v+\delta J(x)\}+(1-\lambda)\delta J(x)

for $x<X$ , and the analogous equation at $X$ with $v+k+\delta J(0)$ (redemption) in place of $v-p+\delta J(x+1)$ . She buys, or redeems, when this is at least as good as the outside option. Her decisions turn the point inventory into a Markov chain on $\{0,\dots,X\}$ that moves from $x$ to $x+1$ (from $X$ to $0$ ) or stays put. The firm's profit is $p$ times the long-run purchase probability per period.

Two constants recur throughout:

A=\frac{\lambda q\delta}{1-\delta+\lambda q\delta},\qquad A_1=\frac{\lambda\delta}{1-\delta+\lambda\delta}.

So do the boundary prices $p^B(\tau)$ and $p^D(\tau)$ of the paper's p. 10, which separate the price ranges of the consumer's four response patterns (Proposition 2). The benchmark is the profit of the best price without a program, $\max\{\lambda qv,\ \lambda(v-\bar v)\}$ : selling to the consumer only when her outside option is $0$ , or always, at the price $v-\bar v$ .

Formalization targets

Goal: Proposition 3

Assume $k=0$ and either (a) $q\le\tfrac12$ and $\delta\ge\tfrac{2}{2+\lambda}$ , or (b) $q>\tfrac12$ and $v-\bar v\le\min\{Av,\ \tfrac{v}{1+A_1}\}$ . Then for every program $(p,X)$ and every solution $J$ of the optimality equations, the average expected revenue $\bar R_N$ over the first $N$ periods, of a consumer who starts with $0$ points, satisfies

\limsup_{N\to\infty}\bar R_N\ \le\ \max\{\lambda qv,\ \lambda(v-\bar v)\}.

The statement covers every price, including those between the ranges of Proposition 2, where the paper asserts but does not show that the consumer drops out.

Milestones

Structure of the value function. Proposition 1 ( $J$ increasing and convex for $p\ge0$ ), Corollaries 1–2 (purchase decisions are monotone in the point inventory), Lemmas 4–5 (redemption at the low outside option, and at the high one whenever she buys in state $X-1$ ).
The consumer's response. Proposition 2: four price ranges and the purchase and redemption rule in each. Its converse, from the proofs of Lemmas 6–9: each observed behaviour forces the price into its range.
Demand. Lemma 1 and the analogous case (c) computation: the stationary distribution of the induced chain and the purchase probabilities $\lambda qX/(\tau+q(X-\tau+1))$ and $\lambda qX/(X+q)$ .
Profit bounds. $\pi^*_a\le\lambda(v-\bar v)$ and $\pi^*_d\le\lambda qv$ ; Lemmas 2 and 3, which bound the profit of the threshold cases (b) and (c); and the inequality $q\le A$ under condition (a).

Significance

Proposition 3 separates two effects of a reward program. Point pressure raises the purchase probability above that of a consumer who never accelerates. Discounting forces the firm to lower its price to keep her in the program, and without transaction utility the second effect dominates. The paper's Proposition 4 shows that a small positive $k$ reverses the conclusion, and its §6 shows that an expiration term reverses it too. The result therefore locates exactly where the profitability of BXGO programs comes from: transaction utility or expiration, not the threshold alone.

The result is proved on paper but not machine-checked. The paper's proof of Proposition 3 works with the closed-form profits of four behavioural cases. Formalizing it requires connecting those closed forms to the consumer's dynamic program and to the long-run behaviour of the chain her decisions induce, and that connection is part of the mission. Machine-checked proofs of Propositions 1–2 also give a reusable template for monotone threshold policies in discounted point-accumulation problems.

Difficulty

The value function has no closed form until the consumer's behaviour is known, and her behaviour is defined by the value function. The paper breaks the circularity case by case: assume a behaviour, solve the linear equations it induces, and read off the price range in which that behaviour is consistent. A formal proof has to show that the four ranges, together with the gaps between them, account for every price. At a gap price the consumer either never buys from $0$ points or behaves as in a neighbouring case.

Reading profit as "price times stationary demand" also needs care. At high prices, at $\lambda=0$ or at $q=0$ the induced chain is reducible, and the long-run revenue from $0$ points need not equal the revenue under an arbitrary stationary law. Lemmas 2 and 3 bound only the four closed forms; turning them into a bound on the Cesàro averages of the actual chain is the remaining step.

Formalization scope

All quantities are real. Params bundles $(\lambda,q,\delta,v,\bar v,k)$ , and Params.Standing is the list of standing assumptions: $\lambda,q\in[0,1]$ , $\delta\in(0,1)$ , $v\ge\bar v\ge0$ , $k\ge0$ . The value function is a hypothesis, IsValueFn P p X J, meaning that J : ℕ → ℝ satisfies the optimality equations on $\{0,\dots,X\}$ . The equations have exactly one solution there, and its values beyond $X$ play no role. Decisions break ties in favour of buying or redeeming, as in the paper's Corollary 1 and Proposition 2. The chain lives on Fin (X+1). Profit is the Cesàro average avgRevenue of expected revenues from state $0$ , computed from the transition matrix of the consumer's own decisions. Stationary distributions use the published MarkovChain.IsStationary.

The goal cannot be made true by construction. Profit is computed from the decisions of $J$ , never from the paper's closed forms, and the goal quantifies over every price and every threshold with no assumed behaviour.

Hypotheses added to the paper's statements:

$p\ge0$ on Proposition 1 and Corollary 2. Both fail for negative prices.
$\lambda>0$ , $q>0$ on Proposition 2 and its converse. There the boundary prices divide by quantities that vanish when $A=0$ .
Pointwise statements. Lemmas 2–3 and the case (a)/(d) bounds are stated at every feasible price, because $\pi^*_b$ and the other optimal profits are suprema over possibly empty sets.
Uniqueness only for $\lambda,q>0$ . The stationary laws of Lemma 1 and case (c) are asserted unique only in that range, since at $\lambda=0$ or $q=0$ other stationary laws exist.

Proofs of individual milestones are welcome. So are general lemmas about Cesàro averages of finite stochastic matrices and the two-sided comparison of discounted value functions, both of which are reusable beyond this mission.

Selected references

Y. Liu, Y. Sun, D. Zhang, An Analysis of "Buy X, Get One Free" Reward Programs, Operations Research 69(6):1823–1841, 2021 (cited from the accepted manuscript of March 26, 2021). https://doi.org/10.1287/opre.2021.2128
P. K. Kopalle, Y. Sun, S. A. Neslin, B. Sun, V. Swaminathan, The joint sales impact of frequency reward and customer tier components of loyalty programs, Marketing Science 31(2):216–235, 2012. https://doi.org/10.1287/mksc.1110.0687
M. Lewis, The influence of loyalty programs and short-term promotions on customer retention, Journal of Marketing Research 41(3):281–292, 2004. https://doi.org/10.1509/jmkr.41.3.281.35986
Y. Sun, D. Zhang, A model of customer reward programs with finite expiration terms, Management Science 65(8):3889–3903, 2019. https://doi.org/10.1287/mnsc.2018.3115
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

19 thms3 active usersReviewed

Economics Mechanism Design Operations Research·Captain: mikedeng1

Simple and Approximately Optimal Contracts for Payment for Ecosystem Services: A Linear Contract with Per-Unit Price k/2 Achieves at Least Half of the Optimal Contract PayoffResearch Paper

Motivation

Payments for ecosystem services compensate landowners for conservation that a program values but cannot directly provide. A contract designer must decide how to pay when landowners differ in the amount of forest they would conserve without a payment. That baseline conservation type is privately known, so a contract can pay for forest that would have remained anyway. Li, Ashlagi and Lo study this problem for forest conservation and ask how much payoff a simple, uniform price can guarantee relative to an optimally tailored contract (Li, Ashlagi and Lo, 2022, §§1–2).

The paper's Theorem 1 establishes a guarantee that does not depend on the type distribution: a price equal to half the program's value per unit secures at least half of the optimal contract payoff. This matters to a designer who can estimate the conservation value but cannot reliably estimate the distribution of landowners' private baselines. The guarantee concerns the principal's payoff after payments, rather than the total area conserved or the agent's utility (Li, Ashlagi and Lo, 2022, §4, Theorem 1).

Setting

An agent owns an initial forest area $a_0>0$ . Their type $\theta$ is the fraction of that area they would conserve without incentives. The publicly known type distribution $\mu$ is supported on $[\underline\theta,\bar\theta]\subseteq[0,1]$ . The agent selects a conserved area $a\in[0,a_0]$ . Conservation above the baseline $\theta a_0$ has cost $c_h(a-\theta a_0)$ , where $h>0$ and

c_h(x)=\begin{cases}(h/2)x^2,&x\geq0,\\0,&x<0.\end{cases}

The principal values each conserved unit at $k>0$ . A direct revelation contract specifies an action $a(\theta)$ and payment $P(\theta)$ for each reported type. It is feasible when the action respects the forest-area bounds, payments are nonnegative, truthful participation gives nonnegative utility (individual rationality, IR), and truthfully reporting the type maximizes utility among all reports in the type interval (incentive compatibility, IC). Its payoff is $\mathbb E_\mu[k a(\theta)-P(\theta)]$ . These are the model and contract constraints on pages 4–5 of the source preprint.

A linear contract pays the same price $p\geq0$ for every unit of conserved area, including area the agent would conserve without incentives. The agent's action at price $p$ is $a_L(\theta;p)=\min\{\theta a_0+p/h,a_0\}$ on the type interval. The principal then receives $\operatorname{Obj}^L(p)=(k-p)\mathbb E_\mu[a_L(\theta;p)]$ ; the best such payoff is $\operatorname{Obj}^{L*}=\sup_{p\geq0}\operatorname{Obj}^L(p)$ . The price and payment apply to the whole action $a$ , as in Equation (3) of the source preprint.

Formalization targets

Distribution-free half guarantee

For every probability law $\mu$ on the stated type interval, every feasible direct contract $(a,P)$ with a defined expected payoff, and every best-response action $a_L$ to the price $k/2$ , Theorem 1 gives

\mathbb E_\mu[k a(\theta)-P(\theta)] \leq 2\mathbb E_\mu[(k-k/2)a_L(\theta)].

It follows that every feasible direct-contract payoff is at most $2\operatorname{Obj}^{L*}$ . The universal bound expresses the comparison with an optimal contract even if a maximum over contracts is not attained. The milestone list contains the linear best response, the doubled payoff identity of Equation (7), the information-rent-free upper bound of Equations (4)–(5), and the pointwise comparison from Appendix A.4. All four come from the paper's §4 and Appendix A.4.

Significance

The guarantee makes the price $k/2$ a distribution-independent benchmark for this conservation model. The paper's Example 3 gives a single type at $\theta=0$ where the factor of two is attained, so a larger universal fraction cannot be claimed under the same assumptions (Li, Ashlagi and Lo, 2022, p. 9). The result also implies the best linear contract has the same worst-case guarantee, even though finding its maximizing price may depend on the distribution.

The result is proved in the paper but is not yet machine checked in this mission. Formalizing it will give a reusable definition of this conservation-contract model, with explicit IR and IC constraints, and Lean statements for the price guarantee and its central comparisons. It can also support later formalizations of the paper's conditional contracts and convex-cost extensions, which are outside this mission.

Difficulty

The benchmark is the payoff of an optimally designed contract with actual payments, under private information. Replacing those payments by conservation cost changes the benchmark: the agent may receive an information rent. Likewise, optimizing $k a-c_h(a-\theta a_0)$ independently for each type describes an unconstrained surplus, not the direct contract in Theorem 1. A formal statement that uses either quantity as the goal's “optimal payoff” would miss the paper's claim. The paper compares the linear payoff with a bound on the contract payoff, and its Appendix treats type distributions that need not satisfy the monotone-hazard-rate condition used in the shorter proof sketch (Li, Ashlagi and Lo, 2022, pp. 10, 24–26).

Formalization scope

Lean represents types, areas, prices and payoffs as real numbers. The law $\mu$ is any probability measure on the reals concentrated on $[\underline\theta,\bar\theta]$ ; atoms, including a point mass, are allowed. The standing parameter conditions are $a_0>0$ , $h>0$ and $0\leq\underline\theta\leq\bar\theta\leq1$ . Positive $a_0$ is made explicit because the paper uses $1-p/(ha_0)$ . The theorem adds $k>0$ as stated in Theorem 1. Feasibility and best-response conditions range over supported types, and IC compares every pair of types in that interval. The contract's action and payment are integrable so their expected payoff is defined. The bounded best-response action needs no separate integrability assumption.

The formalization uses a supremum over nonnegative linear prices. Under the standing conditions its values are bounded above, so this is the ordinary best-payoff bound rather than a default value of a total supremum operation. The goal ranges over feasible direct contracts with IR, IC, action bounds and nonnegative payments; it retains the actual $P(\theta)$ in the payoff. A goal stated only for an unconstrained surplus or with an empty feasible class would not represent Theorem 1. Useful contributions include proofs of the four milestones, measure-theoretic facts about supported type laws, and lemmas about the price-payoff supremum.

Selected references

Wanyi Li, Itai Ashlagi and Iris Lo, Simple and Approximately Optimal Contracts for Payment for Ecosystem Services, Management Science, 2022. Formalization uses the SSRN preprint dated 2021-05-19: SSRN 3754041.

6 thms3 active usersReviewed

Combinatorics Economics Linear Optimization·Captain: mikedeng1

Every Choice Function Is Pro-Con Rationalizable: Disjoint Sets of Pro- and Con-Orderings Under Which Each Choice Set's Chosen Alternative Is the One with More Pros Than ConsResearch Paper

Motivation

Revealed-preference theory asks which observed choices can be explained by a decision procedure. The classical answer, maximization of a single preference, explains only choice functions that satisfy consistency conditions such as the weak axiom, and observed choices, including the menu effects in Luce and Raiffa's dinner example, often violate them. A large literature therefore studies richer procedures and characterizes the behaviour each one can generate.

The pro-con model of Dogan and Yildiz formalizes Benjamin Franklin's "prudential algebra": an agent lists reasons for and against each alternative and chooses the one whose reasons for outnumber its reasons against. Each reason is an ordering of the alternatives, and an ordering counts as a reason for (or against) an alternative at a menu when it ranks that alternative first among those available. The paper's main result is that this model is universal for deterministic choice: every choice function is pro-con rationalizable. The paper also proves the random-choice analogue (every random choice function is pro-con rational with signed weights in $[-1,1]$ ), derives that every choice function is plurality-rationalizable, and recovers McGarvey's theorem on majority relations as a corollary.

Setting

Let $X$ be a finite set of $n$ alternatives. A choice set is a nonempty $S \subseteq X$ , and a choice function $C$ assigns to every choice set an element $C(S) \in S$ . An ordering is a strict linear order $\succ$ of $X$ ; $\max(S, \succ)$ is the $\succ$ -top-ranked alternative of $S$ .

A pro-con model $\langle \succ, \rhd\rangle$ consists of two sets of orderings, the pro-orderings $\succ = \{\succ_1, \dots, \succ_m\}$ and the con-orderings $\rhd = \{\rhd_1, \dots, \rhd_q\}$ , with no ordering in both. For $x \in S$ ,

\mathrm{Pros}(x, S) = \{\succ_i \in \succ : x = \max(S, \succ_i)\}, \qquad \mathrm{Cons}(x, S) = \{\rhd_i \in \rhd : x = \max(S, \rhd_i)\}.

$C$ is pro-con rational (Definition 1) if one pro-con model serves every choice set: for every $S$ and every $x \in S$ , $C(S) = x$ if and only if $|\mathrm{Pros}(x, S)| > |\mathrm{Cons}(x, S)|$ .

The proof works with signed weights on classes of orderings. For $1 \le k \le n$ , a $k$ -prefix $[\succ^k]$ is the list of the first $k$ alternatives of an ordering, and $\Omega_k$ is the family of sets with more than $n - k$ elements. A weight function $\lambda_k$ on $k$ -prefixes represents a random choice function $p$ on $\Omega_k$ if $p(x, S)$ is the total weight of the prefixes along which $x$ is the first element of $S$ . The Möbius transform of $p$ is $q(a, S) = \sum_{S \subseteq T \subseteq X} (-1)^{|T|-|S|} p(a, T)$ , extended by $q(a, S) = q(a, S \cup \{a\})$ for $a \notin S$ .

Formalization targets

Goal: Theorem 1

\text{for every choice function } C \text{ on a finite set } X:\quad C \text{ is pro-con rational.}

Milestones

The milestones follow the paper's proof, which runs the inductive construction of Section 6 and makes each step integral in Section 7:

Lemma 2 (Möbius inversion over supersets) and Lemma 3: $\sum_{a \in X} |q(a, S)| \le 2^k$ when $|S| = n - k$ .
Theorem 4 (Ford–Fulkerson criterion), Lemma 1, and Theorem 3, the generalized Ford–Fulkerson theorem: for real $r_i \in [-1, 1]$ , $c_j \in [-m, m]$ with equal sums and $2m \ge \sum|r_i| + \sum |c_j|$ , a matrix with entries in $[-1,1]$ , these margins, and column bound $\sum_i |a_{ij}| \le |c_j| + \max\{0, (\sum|r_i| - \sum|c_j|)/n\}$ .
Steps 1–3 of the proof of Theorem 2: the system (RS)–(CS) gives the representation (15); its row and column totals agree (25); and the bound (29) $\sum_i |\lambda_k([\succ^k_i])| + \sum_j |q(x_j, S)| \le 2\,k!$ .
Lemma 5 (Heller–Tompkins), total unimodularity of the (RS)–(CS) matrix, and Lemma 4 (Hoffman–Kruskal, corrected).
The integral induction step of Section 7.
Remark 1, the strongest form: a model with $|\mathrm{Pros}(x, S)| - |\mathrm{Cons}(x, S)| = 1$ at the chosen alternative and $0$ at every other alternative of $S$ .

Significance

Theorem 1 says that pro-con rationality imposes no testable restriction on deterministic choice: no data set of single-valued choices can refute it. A characterization of a choice procedure is therefore informative only once the model is restricted further (fewer orderings, structured orderings), and the representation of Theorem 1 serves as a starting point for building other universal models, such as the plurality representation of Section 2.4. The paper shows that universality is delicate: it fails for multi-valued choice rules when each ordering may be used only once (Section 2.3).

The result is proved in the paper; nothing in this mission is open mathematics. No part of it has a machine-checked proof. The formal work is to verify the proof. That covers its combinatorial core (Möbius inversion, the $2^k$ estimate, the generalized Ford–Fulkerson theorem), the integrality step, and the corrections the formalization needed: Lemma 4 requires an integral right-hand side; the paper's description of the con-orderings in the random case (inverses of negative-weight orderings, p. 16) is not what the deterministic assembly uses; and the induction of Section 7 uses a bound for the previous step that the paper establishes only for the real-valued construction.

Difficulty

The obvious approach, assigning pro- and con-orderings menu by menu, fails because every ordering affects every menu at once: changing one ordering changes the top element of all sets. The paper therefore builds a signed measure on orderings level by level, prefix length $k = 1, \dots, n$ , and each level must solve a transportation problem with signed margins and box constraints $[-1, 1]$ . Classical Ford–Fulkerson theory covers nonnegative margins only. Moreover, a solution at one level has to leave the next level feasible, which is the role of the column bound in Theorem 3 and the source of the integrality gap noted above. The integrality itself rests on total unimodularity, which neither Mathlib nor the platform currently provides as a usable criterion (Heller–Tompkins) or vertex theorem (Hoffman–Kruskal).

Formalization scope

The alternative set is a type X with [Fintype X] [DecidableEq X]; it may be empty, in which case every statement holds trivially. An ordering is a rank bijection X ≃ Fin (Fintype.card X), rank $0$ being the best, and $x = \max(S, \sigma)$ means $x \in S$ and $\sigma(x) \le \sigma(y)$ for all $y \in S$ . A pro-con model is a structure with two Finsets of rank bijections and a disjointness proof. A choice function is C : Finset X → X with C S ∈ S for nonempty S; its value at $\emptyset$ is irrelevant. ProConRational C includes this choice-function condition. Random choice functions are real-valued p : X → Finset X → ℝ, $k$ -prefixes are injections Fin k ↪ X, and weight functions are maps from prefixes to ℝ (to ℤ in the integral step). Representation on $\Omega_k$ is stated with n < |S| + k to avoid natural-number subtraction. Matrices are Matrix (Fin m) (Fin n) ℝ or indexed by finite types; total unimodularity is Mathlib's Matrix.IsTotallyUnimodular, and vertices are Set.extremePoints ℝ.

The definition rules out each trivializing reading: orderings cannot be repeated (sets, not lists), cannot be both pro and con, are linear orders (unique top), count as cons at their top element, require a strict majority, and one model must serve all choice sets with the equivalence holding at every $x \in S$ . A formalization that drops any of these makes Theorem 1 easier or false in a different way and is not this mission's goal.

Theorem 2 (random choice) is not a target; its proof steps appear as milestones. Reusable beyond this mission: the Möbius transform and its bound, the generalized Ford–Fulkerson theorem, Heller–Tompkins, and Hoffman–Kruskal for box-constrained systems. Proofs of any milestone, alternative proofs of Theorem 1 (for instance, a direct induction avoiding the gap in Section 7), and Lean infrastructure for total unimodularity are welcome.

Selected references

Dogan, S. and Yildiz, K., Every choice function is pro-con rationalizable, SSRN 3085542, version of January 10, 2021; published in Operations Research, 2022. https://ssrn.com/abstract=3085542, https://doi.org/10.1287/opre.2022.2312
Ford, L. R. Jr. and Fulkerson, D. R., Flows in Networks, Princeton University Press, 1962 (reissued 2015).
Heller, I. and Tompkins, C. B., An extension of a theorem of Dantzig's, in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, Princeton University Press, 1956.
Hoffman, A. J. and Kruskal, J. B., Integral boundary points of convex polyhedra, in 50 Years of Integer Programming 1958–2008, Springer, 2010. https://doi.org/10.1007/978-3-540-68279-0_3
McGarvey, D. C., A theorem on the construction of voting paradoxes, Econometrica 21(4), 1953. https://doi.org/10.2307/1907925
Stanley, R. P., Enumerative Combinatorics, Volume 1, Cambridge University Press, 1997, Section 3.7 (Möbius inversion).

16 thms3 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

On the SRPT Scheduling Discipline in Many-Server Queues with Impatient Customers: In the Overloaded Many-Server Limit, SRPT Serves Short Jobs Without Waiting While Long Jobs AbandonResearch Paper

Why SRPT in many-server queues with abandonment

Shortest remaining processing time first (SRPT) is the scheduling rule that always works on the jobs closest to completion. For a single server it minimizes the number of jobs in the system at every time, on every sample path (Schrage 1968). Service systems with many parallel servers and customers who leave when they wait too long, such as call centers, hospital wards and cloud platforms, are a different setting. There an overloaded system must turn customers away somehow, and the scheduling rule decides who. How SRPT behaves in such systems had resisted analysis: the state of the queue is a vector of remaining service and patience times of unbounded dimension, and preemptions couple all customers together.

Dong and Ibrahim (2021) analyze SRPT in the $M/GI/s+GI$ queue in the overloaded many-server regime. They show that SRPT asymptotically behaves like a two-class priority system with a sharp threshold $\tau$ on the service time. Short jobs are served with vanishing delay, long jobs almost all abandon, and the resulting waiting-time measures depend on the patience distribution only through its mean. Under first-come-first-served, by contrast, performance depends on the whole patience distribution (Whitt 2006).

Setting

Customers arrive according to a Poisson process of rate $\lambda$ to $s$ identical servers. Customer $n$ brings a service time $S_n$ and a patience time $T_n$ . The $S_n$ are i.i.d. with a continuous law $\nu_S$ , density $g$ , cdf $G$ and mean $1/\mu$ ; the $T_n$ are i.i.d. with a continuous law $\nu_T$ and mean $1/\theta$ . Arrivals, services and patience times are mutually independent.

A schedule says which customers occupy the servers at each time. From it one reads off each customer's remaining processing time $R_n(t)$ and cumulative time in queue $Q_n(t)$ . Customer $n$ abandons when $Q_n(t)$ reaches $T_n$ . Her patience clock keeps running across preemptions and is not reset. Under SRPT, at every time the servers are busy whenever customers are waiting, and every customer in service has remaining work no larger than that of any waiting customer. Customer $n$ is served ( $\mathrm{Serv}$ ) if she completes service and abandons ( $\mathrm{Ab}$ ) otherwise. Her waiting time $W_n$ is the total time she is present but not in service.

The traffic intensity is $\rho = \lambda/(s\mu)$ . The paper fixes $\rho > 1$ and lets $\lambda$ and $s$ grow together, with $s = \lambda/(\rho\mu)$ . The threshold $\tau$ is defined by equation (1),

\lambda\,\mathbb E[S\,\mathbf 1(S \le \tau)] = s, \qquad\text{equivalently}\qquad \mathbb E[S\,\mathbf 1(S\le\tau)] = \frac{1}{\rho\mu},

so the work brought by jobs shorter than $\tau$ exactly matches capacity. Class 1 consists of the customers with $S \le \tau$ and class 2 of those with $S > \tau$ .

The analysis couples the SRPT queue with a loss system $L$ . This system has the same customers and $s$ servers but no waiting room. Class 1 customers preempt class 2 customers, and a class 1 customer who finds all servers busy with class 1 work is lost. Its class 1 throughput is $\mathrm{Th}_{L,1}$ .

Formalization targets

Goal: Theorem 2 (p. 10)

As $s \to \infty$ , under SRPT and for a tagged customer $c$ in steady state:

\text{(a)}\quad P(\mathrm{Serv}_c \mid S_c\le\tau)\to 1,\qquad P(\mathrm{Serv}_c\mid S_c>\tau)\to 0;

\text{(b)}\quad \mathbb E[W_c\mid\mathrm{Serv}_c]\to 0,\qquad \mathbb E[W_c\mid S_c\le\tau]\to 0;

\text{(c)}\quad \mathbb E[W_c\mid\mathrm{Ab}_c]\to 1/\theta,\qquad \mathbb E[W_c\mid S_c>\tau]\to 1/\theta;

\text{(d)}\quad \mathbb E[W_c]\to \frac{1-G(\tau)}{\theta}.

The goal states all four parts. The constants $1$ , $0$ , $1/\theta$ and $(1-G(\tau))/\theta$ are those of the paper.

Milestones

Proposition 1 (p. 8) is the coupling inequality $\mathrm{Th}_{L,1}\le\mathrm{Th}_O$ , where $\mathrm{Th}_O$ is the throughput of the SRPT queue. The capacity constraint (5) (p. 16) says that work is completed at rate at most $s$ . Two steps in the proof of Lemma 4 (p. 17) concern Erlang's loss formula. The first is the identity $E(r,C) = \bigl(\int_0^\infty(1+t/r)^C e^{-t}dt\bigr)^{-1}$ . The second is the limit $E(s,s)\to 0$ . Lemma 4 (p. 16) gives $\mathrm{Th}^\lambda_{L,1}/\lambda\to G(\tau)$ . Problem (7) (p. 18) is a linear program over service-probability profiles. Lemma 5 (p. 17) says the limiting service probability is $\bar\gamma(x) = \mathbf 1\{x\le\tau\}$ ; the mission states the analytic step that concludes its proof (p. 18), not Lemma 5 itself. Theorem 2(a) is the goal's first part.

Significance

Theorem 2 is a state-space collapse: an infinite-dimensional preemptive system becomes, in the limit, a two-class priority rule with an explicit threshold. Several consequences follow from it. SRPT asymptotically minimizes the waiting time of served customers and maximizes that of abandoning ones (Corollary 1). It also asymptotically maximizes throughput among all disciplines (Proposition 3). Its performance measures are insensitive to the patience law beyond its mean.

The paper proves Theorem 2 on paper. To our knowledge none of it is machine-checked. The mission asks for a formal model of a multi-server preemptive queue with abandonment and a formal proof of the coupling. It also asks for the Erlang-formula asymptotics and the variational step that pins down $\bar\gamma$ . Two parts of the published argument need care in a formal proof. The proof of (b) switches to patience laws with $f(0)>0$ , while the statement is for general patience laws. The proof of Lemma 5 presupposes that $\bar\gamma = \lim \gamma^\lambda$ exists. A complete development must close both points or replace them with arguments that avoid them.

Difficulty

The SRPT queue has no finite-dimensional Markov description. Preemptions mean that the order in which customers are served is not their arrival order, and a preempted customer's patience keeps running. Standard fluid or diffusion limits for many-server queues track the number of customers, or a measure-valued state under first-come-first-served, and SRPT fits neither. The coupling with the loss system avoids this, but proving it requires a matching argument along the sample path that survives every preemption. Converting throughput bounds into statements about conditional waiting times then requires control of steady-state quantities that the model does not provide in closed form.

Formalization scope

The model is a single definitions file in the namespace SRPTManyServer.Collapse, with these conventions.

Sample paths. A path lists arrival, service and patience times $(A_n, S_n, T_n)_{n\ge 0}$ . It is admissible if arrivals are strictly increasing from time $\ge 0$ and tend to infinity, and if $S_n, T_n > 0$ ; this holds almost surely.
Schedules. A schedule is a measurable $\{0,1\}$ -valued $\delta_n(t)$ . SRPT is the relational predicate "only present customers are served; $\min(s, \#\text{present})$ are in service; those in service have remaining work no larger than any waiting customer". Ties are broken arbitrarily. The page describes preemption at arrivals, and the predicate also fixes who takes a freed server.
The loss system. It is defined by recursion over arrivals.
The probability model. The seeds are i.i.d. $\mathrm{Exp}(1)$ variables $E_n$ , and system $s$ has arrivals $A_n = (E_0+\dots+E_n)/(\rho\mu s)$ . All systems share the service and patience times. The sequence is indexed by $s\in\mathbb N$ in place of $\lambda$ .
Standing assumptions. Both laws are carried by $[0,\infty)$ and have densities. The means are $1/\mu$ and $1/\theta$ , $\rho>1$ , and $\tau$ satisfies (1).
Steady state. Steady-state tagged-customer quantities are read as almost-sure customer long-run averages, for example the fraction served among customers $0,\dots,N-1$ with $S_n\le\tau$ as $N\to\infty$ . Their existence for each $s$ is a hypothesis, standing for the paper's assumption of a steady state. The theorems are about these limits as $s\to\infty$ .
Pathwise and analytic forms. Proposition 1 is stated for one deterministic admissible path and every SRPT schedule of it. The capacity constraint (5) is stated pathwise: completed work by time $t$ is at most $s t$ . Lemma 5 itself is not stated; the final step of its proof is, analytically and $g$ -almost everywhere: if $\int g\bar\gamma \ge G(\tau)$ and $\int xg\bar\gamma \le \mathbb E[S\mathbf 1\{S\le\tau\}]$ , then $\bar\gamma = \mathbf 1\{\cdot\le\tau\}$ a.e. where $g>0$ . Problem (7) is an IsLeast statement over measurable $\gamma$ .

The discipline in the goal is SRPT on the actual arrival stream. It is not the two-class priority system, the threshold $\tau$ does not appear in the scheduling predicate, and the throughputs and service probabilities are not free parameters: a statement in which they were would reduce the goal to Lemma 5. The non-idling clause is part of the SRPT predicate, so the empty schedule does not qualify.

A complete development needs a sample-path theory of preemptive multi-server queues with abandonment. It also needs renewal or regenerative arguments that connect time averages with customer averages, and the insensitivity of the $M/G/s/s$ blocking probability, which the paper cites from the literature and does not prove. These pieces are reusable beyond this mission. Contributions to any milestone are welcome. The Erlang identities, problem (7) and the final step of the proof of Lemma 5 are self-contained analysis.

Not formalized here: Corollary 1, Proposition 3 (Appendix B), inequality (4), and the numerical comparisons of §4.

Selected references

J. Dong and R. Ibrahim, On the SRPT scheduling discipline in many-server queues with impatient customers, arXiv:2102.05789v1, 2021 (published in Management Science). https://arxiv.org/abs/2102.05789
L. Schrage, A proof of the optimality of the shortest remaining processing time discipline, Operations Research 16(3), 687–690, 1968. https://doi.org/10.1287/opre.16.3.687
W. Whitt, Fluid models for multiserver queues with abandonments, Operations Research 54(1), 37–54, 2006. https://doi.org/10.1287/opre.1050.0227
O. Garnett, A. Mandelbaum and M. Reiman, Designing a call center with impatient customers, Manufacturing & Service Operations Management 4(3), 208–227, 2002. https://doi.org/10.1287/msom.4.3.208.7753

10 thms3 active usersReviewed

Algorithmic Game Theory Economics Operations Research+1·Captain: mikedeng1

Multimarket Cournot Equilibria with Heterogeneous Resource-Constrained Firms: The Unique Equilibrium in Closed Form via Augmented and Cutoff BudgetsResearch Paper

Motivation

Cournot competition is the standard model of firms that compete by choosing quantities: each firm picks an output, the total output sets the market price, and an equilibrium is a profile in which no firm can gain by changing its own output alone. In practice firms rarely compete in one market. A manufacturer allocates a limited production capacity across regions, an advertiser allocates a budget across channels, a retailer allocates inventory across stores. The capacity couples the markets: what a firm sells in one market it cannot sell in another, so the markets can no longer be analysed one at a time.

Existence of equilibria in such games follows from general fixed-point arguments, and uniqueness under concave demand is known in several settings (for example Alsabah, Bernard, Capponi, Iyengar and Sethuraman, Multiregional oligopoly with capacity constraints, 2019–2021). What is usually missing is a description of the equilibrium itself: which firms enter which markets, and how much each firm allocates. R. Caldentey and M. B. Haugh (Operations Research, 2024) give that description for linear demand. Their Theorem 1 states the unique equilibrium in closed form, in terms of two scalar quantities per firm and per market, the augmented budgets and the cutoff budgets. The rest of their paper (participation thresholds, monotonicity, the limit of many small firms with a fixed aggregate budget, and merger effects) is read off from this formula.

Setting

There are $N$ firms and $M$ markets. Firm $i\in[N]$ has a budget $B_i>0$ and chooses an allocation $x_{ij}\ge 0$ to each market $j\in[M]$ subject to $\sum_{j=1}^M x_{ij}\le B_i$ . Market $j$ has linear inverse demand

r_j(X)=R_j-\frac{X}{\beta_j},\qquad \beta_j>0,

where $X_j=\sum_{i=1}^N x_{ij}$ is the total allocated to market $j$ . Firm $i$ 's profit is $\sum_{j=1}^M r_j(X_j)\,x_{ij}$ . Markets are ranked $0\le R_1\le\cdots\le R_M$ and budgets $B_1\ge\cdots\ge B_N>0$ .

A Cournot equilibrium is a profile of feasible allocations such that, for every firm $i$ , no feasible allocation of firm $i$ yields a higher profit when the other firms keep their allocations.

Three derived quantities appear in the answer.

The augmented budget of firm $i$ is $\mathcal B_i=i\,B_i+\sum_{k=i}^N B_k$ .
The cutoff budget of market $j$ is $\mathbb B_j=\sum_{k=j}^M\beta_k(R_k-R_j)$ .
The water-level function is $H(x)=\inf\{z\ge 0:\ \sum_{j=1}^M\beta_j(R_j-z)^+\le x\}$ for $x\ge 0$ : the lowest level $z$ at which the "volume" $\sum_j\beta_j(R_j-z)^+$ above $z$ fits into $x$ .

Finally $n^*_j=\max\{i\in[N]:\mathcal B_i>\mathbb B_j\}$ , with $n^*_j=0$ when no firm qualifies, is the threshold index used in the formula. For $R_j>0$ it counts the firms active in market $j$ ; at $R_j=0$ the threshold index can be positive while every allocation to that market is zero.

Formalization targets

Goal: Theorem 1 (p. 8)

Under the standing assumptions there is exactly one Cournot equilibrium, and it is

x^*_{ij}=\beta_j\Big[\frac{R_j}{1+n^*_j}-\frac{H(\mathcal B_i)}{i+1}+\sum_{k=1}^{n^*_j}\frac{H(\mathcal B_k)}{k(k+1)}-\sum_{k=1}^{i}\frac{H(\mathcal B_k)}{k(k+1)}\Big]^+ .

It is stated as an equivalence: a profile $x$ is a Cournot equilibrium if and only if $x=x^*$ . This single statement contains existence, uniqueness and the formula.

Milestones

The milestones follow the proof in Appendix B.

Properties of $H$ (remark after Definition 3.2): continuous, non-increasing, piecewise linear on $[0,\infty)$ , and $H(\mathbb B_j)=R_j$ .
$H(x)$ is the least $z\ge 0$ with $\sum_j\beta_j(R_j-z)^+\le x$ , and the inequality is tight when $H(x)>0$ (proof of Theorem 1, after (B-17)).
(B-4): a firm's best response is $x_{ij}=(\beta_jR_j-\beta_j\lambda_i-X_{ij-})^+/2$ with a budget multiplier $\lambda_i\ge 0$ .
(B-5)–(B-7): in equilibrium the multipliers are non-decreasing, the active firms in a market are the first $n_j$ , and $x_{ij}=\frac{\beta_j}{n_j+1}\big[R_j-\lambda_i(n_j+1)+\sum_{k\le n_j}\lambda_k\big]^+$ .
(B-10) ⇒ (B-11): with $\alpha_i=i\lambda_i-\sum_{k<i}\lambda_k$ , one has $\lambda_i=\alpha_i/i+\sum_{k<i}\alpha_k/(k(k+1))$ .
The identity after (B-12): $\sum_{k\le n}\lambda_k/(1+n)=\sum_{k\le n}\alpha_k/(k(k+1))$ .
Lemma 1 (B-18): for the allocations (B-12) built from any non-decreasing $\alpha\ge 0$ and every vector $V$ , $(i+1)\sum_jV_jx_{ij}+\sum_{k>i}\sum_jV_jx_{kj}=\sum_{j:\alpha_i<R_j}V_j\beta_j(R_j-\alpha_i)$ .
(B-16): in equilibrium $\alpha_i=H(\mathcal B_i)$ for every firm.

Significance

Theorem 1 turns an $N\times M$ equilibrium problem with coupled constraints into a formula that can be evaluated in closed form once $H$ is computed at $N$ points. It shows that firm $i$ 's allocation depends on the budgets only through $\mathcal B_i,\dots,\mathcal B_N$ , so a firm's behaviour is unaffected by the sizes of larger firms, only by their number. The paper's Proposition 1 (participation iff $\mathcal B_i>\mathbb B_j$ , monotonicity of allocations, and which budget constraints bind) and Proposition 2 (the limit of many firms with a fixed aggregate budget) are corollaries, as are its comparative statics on consumer surplus and welfare.

The result is proved in the paper, by a derivation through Lagrange multipliers. It has no machine-checked proof. A formalization would check the derivation, including the case of tied budgets, which the paper's proof sets aside in a footnote ("straightforward to handle"), and would make the closed form and the function $H$ available for the follow-up results.

Difficulty

Each firm's problem is a strictly concave quadratic program, so best responses are easy to describe one firm at a time. The difficulty is that the best responses are coupled through the market totals and through which firms are active in which market. The obvious approach, solving the first-order conditions market by market, requires knowing the set of active firms in each market, and that set depends on all the multipliers at once, while the multipliers depend on which budget constraints bind. Uniqueness requires showing that every equilibrium has multipliers of this form; existence requires that the formula's profile satisfies every firm's optimality conditions, including the inactive markets.

Formalization scope

Firms are Fin N and markets Fin M; the paper's firm $i$ is the Lean index i.val + 1, so the factors $i+1$ and $k(k+1)$ in (6) become i + 2 and (k+1)(k+2). Profiles are firm-first, x i j. All quantities are real numbers. The price $R_j-X_j/\beta_j$ is not truncated at zero. The equilibrium notion is the published CarbonDoubleCount.Planner.IsPureNash, which compares a firm's payoff against every feasible unilateral deviation.

The standing assumptions are bundled in one predicate: $R$ monotone, $R_j\ge 0$ , $\beta_j>0$ , $B$ antitone, $B_i>0$ . The orderings that §2 makes "without loss of generality" are hypotheses, because the formulas (5) and (6) depend on them. Ties among budgets are allowed (the paper's proof assumes distinct budgets in a footnote; the theorem does not). $N=0$ and $M=0$ are allowed.

Pinned readings: the empty maximum in $n^*_j$ is $0$ ; $H$ is a real infimum, used only at nonnegative arguments; "the smallest real such that the budget holds" for a multiplier is complementary slackness; Lemma 1 is an identity for any non-decreasing $\alpha\ge 0$ and does not assume the market ordering; "greater than one" after (B-17) is read as "greater than zero".

The sentence after (7) calls $n^*_j$ the number of firms operating. At the allowed boundary $R_j=0$ this is not literally true: a one-market instance with positive budgets has $n^*_j=N$ and $x^*_{ij}=0$ for every firm. The formal goal retains (7) and the closed form (6), and does not assert the false boundary interpretation.

The formula $x^*$ is a definition computed from the data. A statement that only asserts the existence of a unique equilibrium, or that defines $x^*$ by choice from an equilibrium, would not be Theorem 1; the goal is the equivalence with the explicit formula.

A complete development needs: KKT conditions for a separable concave quadratic program with one linear constraint (milestone 3), elementary properties of a water-filling level function (milestones 1–2), and finite summation identities (milestones 5–7). The water-filling lemmas and the summation identities are reusable beyond this mission. Proofs of any milestone, and alternative proofs of the goal that bypass the multiplier derivation, are welcome.

Selected references

R. Caldentey and M. B. Haugh, Technical Note—Multimarket Cournot equilibria with heterogeneous resource-constrained firms, Operations Research, 2024. https://doi.org/10.1287/opre.2022.0664 (cited from the authors' version of January 20, 2024).
A. Cournot, Recherches sur les principes mathématiques de la théorie des richesses, Hachette, Paris, 1838.
H. Alsabah, B. Bernard, A. Capponi, G. Iyengar and J. Sethuraman, Multiregional oligopoly with capacity constraints, SSRN 3280688, 2020. https://doi.org/10.2139/ssrn.3280688

11 thms3 active usersReviewed

Completed

Quantum Information·Captain: Goku

Fast and efficient exact synthesis of single qubit unitaries generated by Clifford and T gatesResearch Paper

Motivation

In this paper, we show the equivalence of the set of unitaries computable by the circuits over the Clifford and T library and the set of unitaries over the ring $\mathbb{Z}[\frac{1}{\sqrt{2}},i]$ , in the single-qubit case. We report an efficient synthesis algorithm, with an exact optimality guarantee on the number of Hadamard and T gates used. We conjecture that the equivalence of the sets of unitaries implementable by circuits over the Clifford and T library and unitaries over the ring $\mathbb{Z}[\frac{1}{\sqrt{2}},i]$ holds in the $n$ -qubit case.

This mission is the statement-level formalization of Fast and efficient exact synthesis of single qubit unitaries generated by Clifford and T gates (arXiv:1206.5236v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

17 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Exact single-qubit H/T synthesis characterization (Theorem 1 (abstract seed): exact single-qubit synthesis characterization, PDF p. 2). 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

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

Conjecture 1: n-qubit extension with one clean ancilla: Conjecture 1: n-qubit extension with one clean ancilla (source-ambiguity)
§2 unnumbered examples: rotations requiring approximation: §2 unnumbered examples: rotations requiring approximation (source-ambiguity)
Corollary 1: synthesis size, arithmetic cost and bit cost: Canonical input encoding, resource-counted Algorithm-1 execution, and uniform length/arithmetic/bit bounds in the true minimum exact H/T length. (hard)
§5 unnumbered: finite exhaustive verification claim: §5 unnumbered: finite exhaustive verification claim (source-ambiguity)
Proposition 2: base extraction property: Proposition 2: base extraction property (source-ambiguity)
Theorem 2: simultaneous H/T optimality and exact count formulas: Returned-word G synthesis/HT-normalization interface with simultaneous H/T optimality and the two exact count formulas. (hard)
Conclusion unnumbered: combined Pauli-X/Y output bound: Conclusion unnumbered: combined Pauli-X/Y output bound (source-ambiguity)

Selected references

Fast and efficient exact synthesis of single qubit unitaries generated by Clifford and T gates, arXiv:1206.5236v4, https://arxiv.org/abs/1206.5236v4

20 thms3 active usersReviewed

Quantum Information·Captain: Goku

Norm-attaining tensors and nuclear operatorsResearch Paper

Motivation

Given two Banach spaces $X$ and $Y$ , we introduce and study a concept of norm-attainment in the space of nuclear operators $\mathcal{N}(X,Y)$ and in the projective tensor product space $X \widehat{\otimes}_\pi Y$ . We exhibit positive and negative examples where both previous norm-attainment hold. We also study the problem of whether the class of elements which attain their norms in $\mathcal{N}(X,Y)$ and in $X\widehat{\otimes}_\pi Y$ is dense or not. We prove that, for both concepts, the density of norm-attaining elements holds for a large class of Banach spaces $X$ and $Y$ which, in particular, covers all classical Banach spaces. Nevertheless, we present Banach spaces $X$ and $Y$ failing the approximation property in such a way that the class of elements in $X\widehat{\otimes}_\pi Y$ which attain their projective norms is not dense. We also discuss some relations and applications of our work to the classical theory of norm-attaining operators throughout the paper.

This mission is the statement-level formalization of Norm-attaining tensors and nuclear operators (arXiv:2006.09871v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

44 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Abstract main negative result, pinned to Theorem 5.1 (Abstract main negative result, pinned to Theorem 5.1, PDF p. 20). 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

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

Example 4.12(d): absolute sums: Computed absolute normalized sum X ⊕a Y, with its normed and complete structures derived from a on R². (hard)
Remark 4.13: uniform crossnorm stability: A uniform family of reasonable crossnorms on all Banach pairs, its tensor-map metric mapping property, and the actual alpha completion. (hard)
Corollary 4.14: unrestricted final factor (source ambiguity): A source-supported hypothesis or proof for the unrestricted final factor Y. (source-ambiguity)

Selected references

Norm-attaining tensors and nuclear operators, arXiv:2006.09871v4, https://arxiv.org/abs/2006.09871v4

46 thms3 active usersReviewed

Completed

Partial Differential Equations Symplectic Geometry·Captain: Mazecto

Lectures on Symplectic Field Theory VII: Finite-Energy Pseudoholomorphic Curves in SymplectizationsTextbook

Motivation

Let $S\subset\mathbb{R}^{2n+2}$ be a hypersurface that is strictly star-shaped about the origin. The standard Liouville form restricts to a contact form on $S$ , and its Reeb vector field $R$ is a reparametrization of the Hamiltonian flow of any function with $S$ as a regular level. Weinstein conjectured in 1978, motivated by results of Rabinowitz, that Reeb flows on closed contact manifolds have periodic orbits; H. Hofer established this for the three-sphere and further three-dimensional cases in 1993 (Invent. Math. 114), with finite-energy pseudoholomorphic curves in the symplectization $\mathbb{R}\times S$ as the central objects. Since then these curves have been the main source of periodic orbits, global surfaces of section and invariants of Reeb flows, for example in U. Hryniewicz's characterization of the Reeb orbits that bound disk-like global surfaces of section (arXiv:1105.2077).

The basic fact about these curves is their behaviour near a puncture: a finite-energy curve on a punctured disk either extends over the puncture or approaches a periodic Reeb orbit there. This mission formalizes that statement for the symplectization of a strictly star-shaped level in $\mathbb{R}^{2n+2}$ , following C. Wendl, Lectures on Symplectic Field Theory, Lecture 9 (arXiv:1612.01009), together with the results on planes, cylinders and energy concentration that accompany it in Hofer's and Hryniewicz's papers. It is the seventh mission in a series on symplectic field theory and builds on the sixth, which defines almost complex structures and pseudoholomorphic maps on open subsets of a vector space.

Setting

Linear data. $V=\mathbb{R}^{2n+2}$ with coordinates $(q_1,p_1,\dots,q_{n+1},p_{n+1})$ , the complex structure $j_0$ (multiplication by $i$ on $q_k+ip_k$ ), $\omega_0=\sum_kdq_k\wedge dp_k$ and $\lambda_0=\tfrac12\sum_k(q_k\,dp_k-p_k\,dq_k)$ .
The level. $H:V\to\mathbb{R}$ is smooth, every ray from $0$ meets $S=H^{-1}(1)$ exactly once, and $dH(x)x>0$ on $S$ . The Reeb field is $R=X_H/\lambda_0(X_H)$ with $X_H=j_0\nabla H$ , and $\xi_x=\ker\lambda_0(x)\cap\ker dH(x)$ is the contact plane.
Symplectization. $\mathbb{R}\times S$ is identified with $V\setminus\{0\}$ by $(a,x)\mapsto e^{2a}x$ . A smooth $J$ that is a $d\lambda_0$ -compatible complex structure on each $\xi_x$ determines the almost complex structure $\tilde J$ on $V\setminus\{0\}$ with $\partial_a\mapsto R$ , $R\mapsto-\partial_a$ , and $J$ on $\xi$ .
Energy. For a map $u$ from an open $U\subseteq\mathbb{C}$ , with $a$ and $w=\mathrm{proj}\circ u$ its two components, Hofer's energy is $E(u)=\sup_\varphi\int_Uu^*d(\varphi(a)\lambda_0)$ over smooth nondecreasing $\varphi:\mathbb{R}\to[0,1]$ , and the $d\lambda$ -energy is $\int_Uw^*d\lambda_0$ .
Finite-energy curves. Smooth maps $u:U\to V\setminus\{0\}$ with $\partial_su+\tilde J(u)\partial_tu=0$ and $E(u)<\infty$ .
Periodic Reeb orbits $P=(x,T)$ , $T>0$ not necessarily minimal, the trivial cylinder $F_P(e^{2\pi(s+it)})=e^{2Ts}x(Tt)$ , and the charge of a puncture: the limit of the actions $\int\lambda_0$ of the image loops of small clockwise circles around it.

Formalization targets

Goal: asymptotics of finite-energy punctured disks

Let $u$ be a finite-energy $\tilde J$ -holomorphic curve on the punctured unit disk $D\setminus\{0\}$ . Then either $u$ extends smoothly and $\tilde J$ -holomorphically over $0$ with values in $V\setminus\{0\}$ , or the charge $Q$ at $0$ exists and is nonzero, $a(u(z))\to\pm\infty$ as $z\to0$ with the sign of $Q$ , and for every sequence $\rho_k\to0^+$ a subsequence of the loops $t\mapsto\mathrm{proj}\,u(\rho_ke^{-2\pi it})$ converges in $C^\infty$ to $t\mapsto x(Qt+c)$ for a periodic Reeb orbit $(x,|Q|)$ (Wendl, Theorem 9.8, without the nondegenerate and Morse–Bott clause and without the linear asymptotics of $a$ along the end).

Milestones

Structure of the symplectization. $\tilde J$ is a smooth almost complex structure on $V\setminus\{0\}$ , invariant under $y\mapsto cy$ ; the radial coordinates are smooth (Hryniewicz § 2.2).
Reeb field. $\lambda_0(R)=1$ and $\omega_0(R,\cdot)=0$ on $TS$ (Hofer § 1).
Compatibility. $\omega_0$ is compatible with $\tilde J(y)$ for every $y\ne0$ .
Energy densities. The energy integrands of finite-energy curves are nonnegative, $\int u^*d\lambda\le E(u)$ , and $E(u)=0$ forces a constant map on a connected domain (Hryniewicz (17)).
Periods. The periods of periodic Reeb orbits on $S$ have a positive lower bound.
Hofer's lemma for continuous nonnegative functions on complete metric spaces (Wendl, Lemma 9.4).
Monotonicity. For $J$ on an open subset of a finite-dimensional space and $K$ compact, proper $J$ -holomorphic maps into a small ball $B_r(p)$ , $p\in K$ , passing through $p$ , have $\int\|Du\|^2\ge cr^2$ (Zinger, Proposition 3.12).
Removal of singularities for $J$ -holomorphic punctured disks of finite energy with values in a compact set (Wendl, Theorem 9.2).
Zero $d\lambda$ -energy, negative punctures. Such curves on $\mathbb{C}\setminus\Gamma$ are $F_P\circ p$ for a polynomial $p$ (Hryniewicz, Theorem 2.18).
Planes. Nonconstant finite-energy planes have positive $d\lambda$ -energy (Hryniewicz, Corollary 2.19).
Cylinders. A nonconstant finite-energy cylinder with zero $d\lambda$ -energy is $z\mapsto F_P(cz^k)$ (Wendl, Lemma 9.9).
Bubbling-off points. Gradient blow-up of curves with bounded energy concentrates $d\lambda$ -energy at least the period of some Reeb orbit of period $\le$ the energy bound (Hryniewicz, Lemma 2.20).
Isolated orbits. If loops at a nonremovable puncture converge along one sequence of radii to an isolated orbit, they converge to it up to phase for all small radii (Wendl, Lemma 9.18).
Asymptotics of planes. A nonconstant finite-energy plane has a positive puncture at $\infty$ with charge equal to its $d\lambda$ -energy (Hofer, Theorem 31).
Bridge to $\mathbb{R}^4$ . For $n=1$ , star-shapedness and periodic orbits agree with the HryniewiczCriterion setting, with period equal to action.

Significance

The results. The goal is the local half of SFT compactness and of the Fredholm theory of punctured curves: it says every finite-energy end is cylindrical over a Reeb orbit, which is what makes asymptotic operators, Conley–Zehnder indices and the index formula of the earlier missions applicable to actual curves. Milestones 9–14 (from Hofer, Hryniewicz and Wendl) describe planes, cylinders and bubbling in the form in which they enter Hofer's work on the Weinstein conjecture for $S^3$ and Hryniewicz's work on global surfaces of section; milestone 15 connects them to the open HryniewiczCriterion mission. Milestones 6–8 are general results about pseudoholomorphic maps into any finite-dimensional space.

Formalizing them. All results are classical and proved in the cited sources. None of them has been formalized in a proof assistant, as far as a literature search shows; Mathlib has no symplectizations, no Hofer energy and no Reeb dynamics. The mission produces these objects in general dimension $2n+2$ , with the energies as lower Lebesgue integrals.

Difficulty

The target $V\setminus\{0\}$ is not compact and $\tilde J$ is not the standard structure, so the curves can escape to $0$ or to infinity; the goal has to decide which happens and produce a limit orbit, though the limit orbit is not assumed nondegenerate and may depend on the chosen sequence of radii. Hofer's energy is a supremum over a family of integrands rather than a single integral, and its finiteness does not bound the Euclidean area of the curve. The Euclidean size of the derivative grows with $e^{2a}$ , so all scale-sensitive statements are made with the size $\|D(a\circ u)\|+\|D(\mathrm{proj}\circ u)\|$ , which is invariant under $y\mapsto cy$ . Milestones 7–8 hold for an arbitrary norm on the target and an almost complex structure defined only on an open set.

Formalization scope

Namespace FiniteEnergyPlane; the definition module FiniteEnergyPlane_Setting imports JHolomorphic_Setting (the sixth mission) for IsAlmostComplexOn and IsJHolomorphicOn. The bridge item also imports HryniewiczCriterion_Basic.
Space. $V$ is Fin (2 * (n + 1)) → ℝ with interleaved coordinates; $n=1$ matches HryniewiczCriterion.R4. Its default norm is the sup norm.
Radial coordinates. scaleToS H y is the $r>0$ with $H(ry)=1$ (default $1$ , used only at $y=0$ ), proj H y = scaleToS H y • y, aCoord H y = -½ log (scaleToS H y).
Energies are ℝ≥0∞-valued lower integrals of ENNReal.ofReal of the integrands, so $E(u)<\infty$ is a genuine restriction (a Bochner integral would return $0$ on non-integrable integrands and make it vacuous).
Punctures and loops. All finite punctures use clockwise loops $t\mapsto z_0+\rho e^{-2\pi it}$ , and $\infty$ uses counterclockwise loops $t\mapsto Re^{2\pi it}$ ; at a negative puncture the limit $x(Qt+c)$ with $Q<0$ therefore runs the orbit backward. Removability requires an extension that avoids $0$ .
Not included. The statement in Wendl's Theorem 9.8 that $a\mp|Q|s$ converges in $C^\infty$ along the end, convergence for all radii at nondegenerate or Morse–Bott orbits, exponential convergence and the asymptotic eigenvector are left to a later mission.

Contributions welcome: general lemmas on lower integrals over planar domains and on radial projections to star-shaped hypersurfaces.

Selected references

C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009 (2016), Lecture 9. https://arxiv.org/abs/1612.01009
H. Hofer, Pseudoholomorphic curves in symplectizations with applications to the Weinstein conjecture in dimension three, Invent. Math. 114 (1993), 515–563. https://doi.org/10.1007/BF01232679
U. Hryniewicz, Systems of global surfaces of section for dynamically convex Reeb flows on the 3-sphere, J. Symplectic Geom. 12 (2014), § 2.2. https://arxiv.org/abs/1105.2077
A. Zinger, Notes on J-holomorphic maps, arXiv:1706.00331 (2017), §§ 3.3 and 5.1. https://arxiv.org/abs/1706.00331
H. Hofer, K. Wysocki, E. Zehnder, Properties of pseudoholomorphic curves in symplectisations I: Asymptotics, Ann. Inst. H. Poincaré Anal. Non Linéaire 13 (1996), 337–379. https://doi.org/10.1016/S0294-1449(16)30108-1

73 thms3 active usersReviewed

Completed

Combinatorics Complexity Theory·Captain: yousofy

Block Sensitivity vs. Sensitivity: Reach $2.1308255793978239\ldots$ Open Problem

Comparing single-coordinate and block changes

A Boolean function can react differently to changing one input coordinate and changing several coordinates together. Measuring this difference is a question about the local complexity of total Boolean functions. The Block Sensitivity vs. Sensitivity campaign records exponents that quantify how large this difference can become along families of functions with increasing sensitivity.

This mission records the exact exponent

\alpha=\frac{\log(14055^8)}{\log(3738277295413674)} =2.130825579397823947629976285043\ldots.

Its construction is already accepted and public. The mission expresses that result using the campaign's shared definition, so that its value can enter the same record as earlier entries. The logarithmic expression is the target; the displayed decimal is an approximation. No optimality claim is part of this mission.

Boolean functions and sensitive blocks

A total Boolean function on $n$ coordinates is a map $f:\{0,1\}^n\to\{0,1\}$ , defined on every binary input. For an input $x$ and a set $B$ of coordinates, write $x\oplus B$ for the input obtained by flipping exactly the bits indexed by $B$ .

A coordinate $i$ is sensitive at $x$ if $f(x\oplus\{i\})\ne f(x)$ . The sensitivity $s(f,x)$ counts those coordinates, and $s(f)$ is the maximum of $s(f,x)$ over all inputs. A nonempty coordinate set $B$ is a sensitive block at $x$ if $f(x\oplus B)\ne f(x)$ . The block sensitivity $\operatorname{bs}(f,x)$ is the largest number of pairwise disjoint sensitive blocks at that input. The quantity $\operatorname{bs}(f)$ is its maximum over all inputs.

Every block in one block-sensitivity witness is tested at the same input. The blocks are disjoint as coordinate sets; their sizes need not be equal. These conventions are those of the shared foundation mission, rather than complexity measures defined only on selected inputs or on a promise domain.

Formalization target

The goal is the campaign proposition $\operatorname{AchievesExponent}(\alpha)$ . Explicitly, for every real $\varepsilon>0$ and every natural number $S\ge2$ , there must exist a natural number $n$ and a total Boolean function $f:\{0,1\}^n\to\{0,1\}$ satisfying

s(f)\ge S,\qquad \operatorname{bs}(f)\ge s(f)^{\alpha-\varepsilon}.

Both the dimension and the function may depend on $\varepsilon$ and $S$ . The sensitivity threshold is essential: a favorable ratio for one bounded example does not establish this statement. For example, choosing successively smaller positive losses and increasing thresholds produces a sequence of finite total Boolean functions with unbounded sensitivity and exponents approaching $\alpha$ .

The exact numerator is the natural number

14055^8=1522813785050025472152230187890625.

The denominator inside the logarithm is $3738277295413674$ . Both logarithm arguments exceed one. There is no division by a zero logarithm, and the result uses ordinary real powers. The goal does not assume a finite construction certificate or the existence of a suitable labeling as a hypothesis.

Improvement and verification status

The accepted construction theorem also proves the strict comparison

\frac{\log(14055^8)}{\log(3738289747988852)}<\alpha.

It improves the earlier public exponent, approximately $2.130320333220366$ , by approximately $0.000505246$ . The full proof constructs actual Boolean functions and establishes the asymptotic quantifiers; the numerical approximation alone is not the evidence for the separation.

The complete construction has passed local Lean kernel verification and Prove2Me verification. Its accepted submission is a9d25c46-43bd-4fb1-826b-0ed075b8cf0a. The source uses ordinary checked proofs with the standard axioms propext, Classical.choice, and Quot.sound. Its final statement spells out sensitivity and block sensitivity directly through finite sets. The campaign goal uses the existing shared definitions for those same quantities, and its proof explicitly establishes the equivalence needed to transfer the accepted result.

Why the full statement matters

A lower bound on block sensitivity at one input must be combined with an upper bound on sensitivity over every input. Local calculations that ignore the latter maximum can overstate the separation. Likewise, overlapping sensitive blocks cannot be counted as a disjoint family. These requirements persist through the construction and the passage to arbitrarily large sensitivity.

The exponent also depends on exact integer growth rates. Rounded numerical scores can identify candidates, but they do not establish the final real-power inequality. A complete proof must account for finite construction constraints, the complexity measures of the resulting functions, and the exponent loss allowed in the asymptotic statement. The accepted result includes these steps. This mission records that established result rather than a proposed stronger threshold awaiting construction.

Formalization scope

The development targets Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Inputs are functions Fin n → Bool, and outputs are Bool. Sensitivity and block sensitivity are natural numbers obtained by finite maxima. The campaign proposition quantifies over positive real losses and natural sensitivity thresholds.

Dimension zero is permitted by the representation, but its sensitivity is zero and it cannot witness any required threshold $S\ge2$ . Empty block families contribute zero; every counted block is nonempty. There are no hypotheses that can make the target vacuous. The shared definition and finite-certificate references are retained from the campaign template. The only new result recorded here is the improved separation exponent and its exact campaign formulation. Attribution to the original OpenAI development and Robin Kothari/Codex is retained in the accepted construction source; the new construction is credited to yousofy with Codex.

Selected references

Prove2Me community, Block Sensitivity vs. Sensitivity, collaborative campaign, 2026. Campaign and template.
Prove2Me community, Sensitivity foundation, formal definitions. Shared foundation mission.
yousofy with Codex, Six shared defect tolerances improve the sensitivity exponent to 2.1308255794, Prove2Me, 2026. Accepted complete construction.
yousofy with Codex, Earlier strict exponent checkpoint, Prove2Me, 2026. Public comparison theorem.

6 thms3 active usersReviewed

Completed

Category Theory Differential Geometry Mathematical Physics·Captain: Alien60

Weatherall 2016: Newtonian Gravitation vs. Newton-Cartan Theory (Trautman Geometrization and Categorical Equivalence)Research Paper

Motivation

Newtonian gravitation can be written in two ways. In Newtonian gravitation (NG), spacetime has a flat derivative operator $\nabla$ and a scalar potential $\varphi$ obeying Poisson's equation, and bodies are pushed off the straight lines of $\nabla$ by the force $-\nabla^a\varphi$ . In geometrized Newtonian gravitation (GNG), also called Newton–Cartan theory, the potential is absorbed into a curved derivative operator $\tilde\nabla$ whose geodesics are the trajectories of freely falling bodies. This is the same geometrization that general relativity performs. Trautman (1965) proved that the two pictures pass into each other.

Weatherall (2016) asks whether NG and GNG are the same theory. He represents each theory by a category of models and calls two theories equivalent when there is an equivalence of categories that preserves empirical content. The answer depends on the arrows chosen for NG:

NG₁ treats the potential as physical. Its arrows are diffeomorphisms preserving $t_a$ , $h^{ab}$ , $\nabla$ and $\varphi$ , and NG₁ is not equivalent to GNG.
NG₂ treats the potential as a gauge quantity, as Newton's Corollary VI suggests. Its arrows are pairs $(f,\psi)$ with $\nabla^a\nabla^b\psi = 0$ , and NG₂ is equivalent to GNG (Prop. 6.1).

This is the gravitational twin of the electromagnetic question "potentials vs. field strengths" treated in the companion missions on Weatherall's Understanding Gauge. The other side of the Newton–Cartan story, the classical limit of general relativity, is described under Significance.

Setting

Following Weatherall (p. 3), spacetime is $\mathbb R^4$ , here in one global chart E = Fin 4 → ℝ with index 0 for time. The classical metrics are $t_a = dx^0$ (tt) and $h^{ab} = \mathrm{diag}(0,1,1,1)$ (hh). Their $t = \text{const}$ slices are complete copies of $\mathbb R^3$ , as Weatherall requires.

A derivative operator is a smooth field of Christoffel symbols Γ x a b c $=\Gamma^a{}_{bc}(x)$ , symmetric in $b,c$ , acting by

\nabla_b\xi^a = \partial_b\xi^a + \Gamma^a{}_{bn}\xi^n .

It is compatible when $\nabla_a t_b = 0$ and $\nabla_a h^{bc} = 0$ . Curvature uses Malament's sign convention:

\xi^bR^a{}_{bcd} = -2\nabla_{[c}\nabla_{d]}\xi^a, \qquad R_{bc} = R^n{}_{bcn}.

Other notation:

Geometrization: $\tilde\nabla = (\nabla, -t_bt_c\nabla^a\varphi)$ , that is $\tilde\Gamma^a{}_{bc} = \Gamma^a{}_{bc} + t_bt_c\,h^{an}\partial_n\varphi$ (geomΓ).
Gauge transformation: $(\nabla, t_bt_c\nabla^a\psi)$ (gaugeΓ).
Curves: a massive body has unit timelike tangent, $t_a\xi^a = 1$ . Curves are smooth on an open interval.

The objects of the categories are:

NG (IsNG Γ φ): compatible, flat $\nabla$ and a smooth potential $\varphi$ . The mass density is $\rho = \nabla^a\nabla_a\varphi/4\pi$ .
GNG (IsGNG Γ): compatible $\tilde\nabla$ satisfying, for some smooth $\rho$ ,

(1)\ R_{ab} = 4\pi\rho\,t_at_b,\qquad (2)\ R^a{}_b{}^c{}_d = R^c{}_d{}^a{}_b,\qquad (3)\ R^{ab}{}_{cd} = 0 .

The arrows are diffeomorphisms $f$ of $\mathbb R^4$ that preserve $t_a$ and $h^{ab}$ and carry one derivative operator to the other through the transformation law

\partial_b\partial_c f^a + \Gamma'^a{}_{de}(f(x))\,\partial_bf^d\,\partial_cf^e = \partial_nf^a\,\Gamma^n{}_{bc}(x)

(IsGNGArrow). NG₁ arrows also preserve $\varphi$ (IsNG1Arrow). NG₂ arrows are pairs $(f,\psi)$ with $\nabla^a\nabla^b\psi = 0$ , where $f$ carries the gauge-transformed pair $\big((\nabla,t_bt_c\nabla^a\psi),\ \varphi+\psi\big)$ to $(\nabla',\varphi')$ (IsNG2Arrow).

Formalization targets

Goal: NG₂ ≃ GNG (`ng2_equiv_gng`, Weatherall Prop. 6.1)

Geometrization $E(\nabla,\varphi) = \tilde\nabla$ , $E(f,\psi) = f$ has these properties:

It sends NG₂ objects to GNG objects with the same allowed trajectories, and NG₂ arrows to GNG arrows.
It is full and faithful: every GNG arrow $f : E(A)\to E(A')$ is $E(f,\psi)$ for a unique $\psi$ .
It is essentially surjective: every GNG object is isomorphic to a geometrization.

This is exactly the "full, faithful, essentially surjective" route of Weatherall's proof in App. A. These three properties together are equivalent to an equivalence of categories.

Milestones (source order)

geometrization, Prop. 2.1 (Trautman). For flat compatible $\nabla$ $\nabla$ and Poisson's equation, $\tilde\nabla$ $\tilde{\nabla}$ has these properties:
- it is a classical spacetime;
- its timelike geodesics are exactly the curves with $\xi^n\nabla_n\xi^a = -\nabla^a\varphi$ ;
- it is the unique derivative operator with that property;
- it satisfies (1)–(3).
recovery, Prop. 2.2 (Trautman). Every classical spacetime satisfying (1)–(3) comes from some flat $\nabla$ and potential $\varphi$ obeying Poisson's equation.
gauge_iff, the non-uniqueness remark after Prop. 2.2. A second pair $(\varphi',\nabla')$ works iff $\nabla^a\nabla^b(\varphi'-\varphi)=0$ and $\nabla' = (\nabla, t_bt_c\nabla^a(\varphi'-\varphi))$ . Weatherall states the "if" direction and his proof of Prop. 6.1 uses the "only if" direction. The iff is Malament's Prop. 4.2.5. Note that $\psi = g(x^0)\,x^1$ is allowed: the gauge includes time-dependent uniform accelerations (Corollary VI).
geom_naturality, the key computation in App. A. A metric-preserving diffeomorphism carrying $\varphi$ to $\varphi'$ carries $\nabla$ to $\nabla'$ iff it carries $\tilde\nabla$ to $\tilde\nabla'$ .
ng1_not_equiv_gng, the NG₁ row of Table 1 (§6, p. 18). No object map NG₁ → GNG preserves empirical content while inducing bijections of hom-sets. Weatherall states this in prose without a proof. The intended argument is that two NG₁ models related by a nonzero gauge share a geometrization but have no NG₁ arrow between them.

Significance

Philosophy of physics. This is the standard worked example for categorical criteria of theoretical equivalence: Glymour's criterion versus equivalence of categories. It also shows how "excess structure" (here the potential) is detected by fullness.
Physics. Newton–Cartan geometry is the non-relativistic limit of general relativity. Fletcher, Manchak, Schneider and Weatherall (2018), Thm 8 restates Malament's (1986) theorem in Künzle's (1976) framework. If a family $g_{ab}(\lambda)$ of Lorentzian metrics has $g_{ab}\to t_at_b$ and $\lambda g^{ab}\to -h^{ab}$ , and its Einstein tensors converge, then the limit derivative operator satisfies (1) and (2), but not necessarily (3). GR limits therefore land in a slightly larger class than GNG, and condition (3) is exactly what the recovery theorem needs. This makes the present mission the Newtonian half of a planned GR-limit mission.
Lean. This is a reusable coordinate model of Galilean/Newton–Cartan structures, Christoffel transformation laws and curvature, none of which exist in Mathlib.

Difficulty

Milestones 1, 3 and 4 are long but elementary tensor computations. The uniqueness clause in 1 needs local existence of solutions of the trajectory ODE (Mathlib's Picard–Lindelöf).
Milestone 2 is the heart. Compatibility forces $\tilde\Gamma$ to be a rotation field $\omega_{ij}$ plus an acceleration field $g_i$ . Condition (3) forces $\omega$ to be spatially constant, and condition (2) makes $g$ , minus the inertial terms of a rotating frame, a closed form on each slice. The Poincaré lemma, smoothly in the time parameter, then produces $\varphi$ . The degree-1 Poincaré lemma on convex sets is in Mathlib, and the companion mission Weatherall 2016: Potentials vs. Field Strengths (continuum) develops the homotopy operator.
The goal then assembles 2, 3 and 4.

Formalization scope

Single global chart. Weatherall's spacetime is $\mathbb R^4$ with arbitrary $t_a, h^{ab}$ . Here $t_a$ and $h^{ab}$ are fixed to their standard form in one global chart, a choice of Galilean coordinates; the derivative operators remain arbitrary. Arrows are genuine diffeomorphisms of $\mathbb R^4$ .
Normalized curves. Massive bodies have unit tangent $t_a\xi^a = 1$ , as in Malament (Ch. 4). Without this normalization the geodesic and force laws are not equivalent.
No category instances. Categories are encoded by their hom-predicates, and "equivalence of categories" by the full / faithful / essentially-surjective data of App. A. Composition laws are not required by any item.
Out of scope: Weatherall's footnote 32 (spatially compact matter), Glymour's criterion, and the GR limit (planned as a separate mission).

Selected references

J. O. Weatherall, Are Newtonian Gravitation and Geometrized Newtonian Gravitation Theoretically Equivalent?, Erkenntnis 81 (2016) 1073–1091. Primary source: Props. 2.1, 2.2, 6.1, Table 1, App. A.
D. B. Malament, Topics in the Foundations of General Relativity and Newtonian Gravitation Theory, University of Chicago Press (2012), Ch. 4 (Props. 4.2.1, 4.2.5). Conventions.
D. B. Malament, Classical General Relativity, in Handbook of the Philosophy of Physics (2007).
A. Trautman, Foundations and current problems of general relativity, in Brandeis Summer Institute 1964, Prentice-Hall (1965).
S. C. Fletcher, J. B. Manchak, M. D. Schneider, J. O. Weatherall, Would Two Dimensions be World Enough for Spacetime?, Stud. Hist. Philos. Mod. Phys. 63 (2018) 100–113. Thm 8 is the Newtonian limit.
H. P. Künzle, Covariant Newtonian limit of Lorentz space-times, Gen. Rel. Grav. 7 (1976) 445–457.

26 thms3 active usersReviewed

Quantum Information·Captain: Goku

Structure of states which satisfy strong subadditivity of quantum entropy with equalityResearch Paper

Motivation

We give an explicit characterisation of the quantum states which saturate the strong subadditivity inequality for the von Neumann entropy. By combining a result of Petz characterising the equality case for the monotonicity of relative entropy with a recent theorem by Koashi and Imoto, we show that such states will have the form of a so-called short quantum Markov chain, which in turn implies that two of the systems are independent conditioned on the third, in a physically meaningful sense. This characterisation simultaneously generalises known necessary and sufficient entropic conditions for quantum error correction as well as the conditions for the achievability of the Holevo bound on accessible information.

This mission is the statement-level formalization of Structure of states which satisfy strong subadditivity of quantum entropy with equality (arXiv:quant-ph/0304007v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

12 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 6: structure of equality in strong subadditivity (original seed) (Theorem 6: structure of equality in strong subadditivity (original seed), 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.

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

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

Theorem 3 (Petz [15]): recovery equality and transpose formula: Finite-relative-entropy hypothesis and globally CPTP support completion (source-ambiguity)
Remark 5: cited near-optimal transpose-channel recovery: The fidelity/error objective, averaging convention, and reference ensemble for the transpose map (source-ambiguity)
Theorem 10 (Koashi–Imoto [7]): states and every invariant dilation: Support-qualified dilation-unitary block identity (source-ambiguity)
Proposition 11: equivalence of global dilation and channel block properties: Support-qualified equivalence between a channel property and a dilation property (source-ambiguity)
Section VII: claim that infinite A and C are covered while infinite B is open: Well-defined saturation for infinite outer registers and a completed-Hilbert structural interface (source-ambiguity)

Selected references

Structure of states which satisfy strong subadditivity of quantum entropy with equality, arXiv:quant-ph/0304007v2, https://arxiv.org/abs/quant-ph/0304007v2

25 thms3 active usersReviewed

Completed

Quantum Information·Captain: Goku

Jensen's Operator InequalityResearch Paper

Motivation

We establish what we consider to be the definitive versions of Jensen's operator inequality and Jensen's trace inequality for functions defined on an interval. This is accomplished by the introduction of genuine non-commutative convex combinations of operators, as opposed to the contractions used in earlier versions of the theory. As a consequence, we no longer need to impose conditions on the interval of definition. We show how this relates to the pinching inequality of Davis, and how Jensen's trace inequlity generalizes to C*-algebras..

This mission is the statement-level formalization of Jensen's Operator Inequality (arXiv:math/0204049v1). 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 Jensen’s operator inequality: four equivalent conditions (Theorem 2.1 (Jensen’s Operator Inequality), 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.

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

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

§4, unnumbered: continuous-field extension of Theorem 2.1: A source-pinned domain for the right-hand integral of a_t* f(x_t) a_t, or an explicitly specified extended operator integral. (source-ambiguity)
Theorem 4.1: Jensen inequality for a centralizing positive functional: A source-pinned domain for the right-hand integral of a_t* f(x_t) a_t, or an explicitly specified extended operator integral. (source-ambiguity)

Selected references

Jensen's Operator Inequality, arXiv:math/0204049v1, https://arxiv.org/abs/math/0204049v1

12 thms3 active usersReviewed

All missions

Geometric Deep Learning VIII: An RNN Seeded at a Fixed Point h⁽⁰⁾ = R(0, h⁽⁰⁾) Is Equivariant to Left Shifts of a Zero-Padded Input SequenceTextbook

Why sequence boundaries matter

RNN runs and padded sequences

Formalization targets

What the result supplies

The boundary difficulty

Formalization scope

Selected references

Geometric Deep Learning III: An n × n Matrix Commutes with the Cyclic Shift S if and only if It Is Circulant, So Convolution Is Shift EquivarianceTextbook

Why convolution, and why the shift

Setting

Formalization targets

Goal: commuting with the shift characterises circulant matrices

Milestones, in attack order

Companion: the Convolution Theorem

Significance

Difficulty

Formalization scope

Selected references

Categorified Symplectic Geometry and the Classical String: The Hamiltonian 1-Forms of a 2-Plectic Space Form a Hemistrict Lie 2-AlgebraResearch Paper

Motivation

Setting

Formalization targets

Hemistrict structure on Hamiltonian one-forms

Significance

Difficulty

Formalization scope

Selected references

Crossed Product of Groups. Applications: The Skeleton of the Category E2(H, G) of Crossed Products Is Crossed(H, G) Modulo 2-EquivalenceResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.8

Milestones, in the order of the paper

Significance

Difficulty

Formalization scope

Selected references

A Meet-in-the-Middle Algorithm for Fast Synthesis of Depth-Optimal Quantum Circuits: Meet-in-the-Middle Search Returns a Minimal-Depth Circuit, Generating Only Circuits of Half the DepthResearch Paper

Motivation

Setting

Formalization targets

Goal: the main result (§2, p. 4)

Milestones

Significance

Difficulty

Formalization scope

Selected references

SU(2)-Irreducibly Covariant and EPOSIC Channels: EPOSIC Channels Are Exactly the Extreme Points of the Convex Set of SU(2)-Irreducibly Covariant ChannelsResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 4.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Commutant Structure of U⊗(n−1) ⊗ U* Transformations: The Operator Basis v^{ab}_{ij}(α) Is a Linear Combination of Partially Transposed Permutation Operators, and ConverselyResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 9

Milestones

Significance

Difficulty

Formalization scope

Selected references

Density Matrix Numerical Renormalization Group for Non-Abelian Symmetries: Tracing Out a Site Keeps the Reduced Density Matrix Symmetric and Gives the dim(ĩ)/dim(u) Recursion for Its Kept BlockResearch Paper

Motivation

Setting

Formalization targets

Goal: one tracing step (§III, eqs. (42)–(45))

Milestones

Significance

Difficulty

Formalization scope

Selected references

Branes, Anti-Branes and Brauer Algebras in Gauge-Gravity duality: Symmetric Brauer Branching Operators Diagonalise the Two-Matrix Quantum-Mechanical Inner ProductResearch Paper