All missions

Motivation

Before the thermodynamic limit, macroscopic averages need not commute for a quantum system. As a consequence, aspects of macroscopic fluctuations or of constrained equilibrium require a careful analysis, when dealing with several observables. We propose an implementation of ideas that go back to John von Neumann's writing about the macroscopic measurement. We apply our scheme to the relation between macroscopic autonomy and an H-theorem, and to the problem of equivalence of ensembles. In particular, we show how the latter is related to the asymptotic equipartition theorem. The main point of departure is an expression of a law of large numbers for a sequence of states that start to concentrate, as the size of the system gets larger, on the macroscopic values for the different macroscopic observables. Deviations from that law are governed by the entropy.

This mission is the statement-level formalization of Quantum Macrostates, Equivalence of Ensembles and an H-Theorem (arXiv:math-ph/0601027v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

16 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 3.1: equivalence of the three quantum ensembles (Theorem 3.1: equivalence of the three quantum ensembles, PDF p. 8). 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:

• §2.1.4: printed spin microcanonical projection construction: A source-corrected directional spin shell and its physical domain. (source-ambiguity)
• §3 opening: equality iff a concentrating canonical maximizer exists: An admissibility/attainment domain for equality of canonical entropy suprema. (source-ambiguity)
• §4.3: printed product-shell Kac microcanonical macrostate: A source-corrected spin factor and domain for the Kac product-shell macrostate. (source-ambiguity)

Selected references

• Quantum Macrostates, Equivalence of Ensembles and an H-Theorem, arXiv:math-ph/0601027v2, https://arxiv.org/abs/math-ph/0601027v2

Motivation

A connected algebraic group in characteristic 0 is uniquely determined by its Lie algebra. In this paper an algorithm is given for constructing an algebraic group in characteristic 0, given its Lie algebra. Using this an algorithm is presented for finding a maximal reductive subgroup and the unipotent radical of an algebraic group.

This mission is the statement-level formalization of Constructing algebraic groups from their Lie algebras (arXiv:math/0612557v1). 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 Chevalley: connected algebraic subgroups generate by uniformly bounded products (Theorem 1 (Chevalley), 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

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

• Unnumbered main result: reconstruct the connected group from its algebraic Lie algebra: Effective presentation of arbitrary characteristic-zero F, splitting extension access and complete rational eigenvalue relations (source-ambiguity)
• Algorithm 3: terminating closed-product construction of the generated algebraic group: Executable base-field polynomial product-closure, geometric equality testing, and terminating Algorithm 3 loop (hard)
• Algorithm 7: semisimple hull defining polynomials: Effective presentation of arbitrary characteristic-zero F, splitting extension access and complete rational eigenvalue relations (source-ambiguity)
• Unnumbered main application: compute maximal reductive subgroup and unipotent radical: Effective presentation of arbitrary characteristic-zero F, splitting extension access and complete rational eigenvalue relations; transport/recompute a Levi factor compatible with the newly computed toral complement (source-ambiguity)
• Unnumbered algorithmic consequence of Lemma 11: compute bases of d′ and n: Executable Jordan decomposition, finite Fitting bracket iteration, and finite basis extraction relative to the cited Cartan primitive (hard)

Selected references

• Constructing algebraic groups from their Lie algebras, arXiv:math/0612557v1, https://arxiv.org/abs/math/0612557v1

Motivation

In this note we collect several characterizations of unitary representations $(\pi, \mathcal{H})$ of a finite dimensional Lie group $G$ which are trace class, i.e., for each compactly supported smooth function $f$ on $G$, the operator $\pi(f)$ is trace class. In particular we derive the new result that, for some $m \in \mathbb{N}$, all operators $\pi(f)$, $f \in C^m_c(G)$, are trace class. As a consequence the corresponding distribution character $\theta_\pi$ is of finite order. We further show $\pi$ is trace class if and only if every operator $A$, which is smoothing in the sense that $A\mathcal{H}\subseteq \mathcal{H}^\infty$, is trace class and that this in turn is equivalent to the Fr'echet space $\mathcal{H}^\infty$ being nuclear, which in turn is equivalent to the realizability of the Gaussian measure of $\mathcal{H}$ on the space $\mathcal{H}^{-\infty}$ of distribution vectors. Finally we show that, even for infinite dimensional Fr'echet-Lie groups, $A$ and $A^*$ are smoothing if and only if $A$ is a Schwartz operator, i.e., all products of $A$ with operators from the derived representation are bounded.

This mission is the statement-level formalization of On the characterization of trace class representations and Schwartz operators (arXiv:1512.02451v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 1.1: integrated operators preserve smooth vectors (Lemma 1.1, 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

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

• Theorem 1.3: Finite-order test topology and canonical Nelson resolvent (hard)
• Unnumbered main consequence: Distribution character on the finite-order test-function topology (hard)
• Theorem 1.4 (Nelson–Stinespring): L1 integrated action and canonical compact Nelson resolvent (hard)
• Unnumbered smoothing factorization, equation (5): Bounded integrated action and the smoothing complex submodule (hard)
• Proposition 1.6: Trace-class representation predicate tied to the actual bounded integrated action (hard)
• Proposition 1.7: Hilbert-Schmidt topology and restricted left action (hard)
• Corollary 1.8: Hilbert-Schmidt joint orbits and the arbitrary-representation Schwartz form (hard)
• Lemma 1.9: Actual derived action, derivative topology and continuous anti-dual (hard)
• Proposition 1.10: Complex trace sandwich pairing on the HS smooth-vector Frechet space (hard)
• Proposition 1.11: Locally convex nuclearity and real distribution dual Gaussian realization (hard)
• Proposition 2.2: Nonnormable locally convex Lie representation and derived sandwich (hard)
• Unnumbered quantitative estimate (7) for derivative sandwiches: Maximal generator weights, unbounded square roots and canonical bounded extensions (hard)
• Remark 2.3(a,b): Locally convex joint C1 calculus and operator-norm orbit derivatives (hard)
• Theorem 2.4: Nonnormable Frechet-Lie smoothness and bounded-form Schwartzness (hard)
• Remark 2.5: Form-defined bounded sandwich and squared maximal-generator domain (hard)
• Theorem 2.6: Merely metrizable locally convex Lie algebra and operator-norm joint smoothness (hard)
• Proposition 2.7: Arbitrary Frechet-Lie Schwartz predicate with actual positive square root (hard)
• Proposition 3.1: Constructed polarized Heisenberg Schrodinger representation and derivative algebra (hard)
• Unnumbered comparison: Coordinate transport and equality of the HS and KKW Schwartz topologies (hard)
• Unnumbered general consequence: General trace-class representation and arbitrary derived Schwartz sandwiches (hard)

Selected references

• On the characterization of trace class representations and Schwartz operators, arXiv:1512.02451v1, https://arxiv.org/abs/1512.02451v1

Motivation

In this paper we consider the $\chi$-function (the Holevo capacity of constrained channel) and the convex closure of the output entropy for arbitrary infinite dimensional channel. It is shown that the $\chi$-function of an arbitrary channel is a concave lower semicontinuous function on the whole state space, having continuous restriction to any set of continuity of the output entropy. The explicit representation for the convex closure of the output entropy is obtained and its properties are explored. It is shown that the convex closure of the output entropy coincides with the convex hull of the output entropy on the convex set of states with finite output entropy. Similarly to the case of the $\chi$-function, it is proved that the convex closure of the output entropy has continuous restriction to any set of continuity of output entropy. Some applications of these results to the theory of entanglement are discussed. The obtained properties of the convex closure of the output entropy make it possible to generalize to the infinite dimensional case the convex duality approach to the additivity problem.

This mission is the statement-level formalization of On entropic quantities related to the classical capacity of infinite dimensional quantum channels (arXiv:quant-ph/0411091v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

27 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §6, unnumbered Theorem: convex-duality additivity equivalence and consequences (§6, unnumbered Theorem: convex-duality additivity equivalence and consequences, PDF p. 19). 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

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

• Section 7, unnumbered energy-continuity assertion: The Hamiltonian domain intended by the unqualified Section 7 mean-energy-continuity sentence. (source-ambiguity)

Selected references

• On entropic quantities related to the classical capacity of infinite dimensional quantum channels, arXiv:quant-ph/0411091v1, https://arxiv.org/abs/quant-ph/0411091v1

Motivation

We show that for a fixed amount of entanglement, two-mode squeezed states are those that maximize Einstein-Podolsky-Rosen-like correlations. We use this fact to determine the entanglement of formation for all symmetric Gaussian states corresponding to two modes. This is the first instance in which this measure has been determined for genuine continuous variable systems.

This mission is the statement-level formalization of Entanglement of formation for symmetric Gaussian states (arXiv:quant-ph/0304042v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Symmetric Gaussian entanglement of formation (Proposition 2: entanglement of formation of symmetric two-mode Gaussian states, 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.

Selected references

• Entanglement of formation for symmetric Gaussian states, arXiv:quant-ph/0304042v1, https://arxiv.org/abs/quant-ph/0304042v1

Motivation

Previous work on the classical information capacities of bosonic channels has established the capacity of the single-user pure-loss channel, bounded the capacity of the single-user thermal-noise channel, and bounded the capacity region of the multiple-access channel. The latter is a multi-user scenario in which several transmitters seek to simultaneously and independently communicate to a single receiver. We study the capacity region of the bosonic broadcast channel, in which a single transmitter seeks to simultaneously and independently communicate to two different receivers. It is known that the tightest available lower bound on the capacity of the single-user thermal-noise channel is that channel's capacity if, as conjectured, the minimum von Neumann entropy at the output of a bosonic channel with additive thermal noise occurs for coherent-state inputs. Evidence in support of this minimum output entropy conjecture has been accumulated, but a rigorous proof has not been obtained. In this paper, we propose a new minimum output entropy conjecture that, if proved to be correct, will establish that the capacity region of the bosonic broadcast channel equals the inner bound achieved using a coherent-state encoding and optimum detection. We provide some evidence that supports this new conjecture, but again a full proof is not available.

This mission is the statement-level formalization of Classical capacity of bosonic broadcast communication and a new minimum output entropy conjecture (arXiv:0706.3416v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Conditional coherent-state capacity region (Section IV, Eqs. (1), (16)-(17); PDF pp.1,3-5, PDF p. 1). 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

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

• Section V / Figure 4, PDF pp.6-7: The exact MAC photon-budget/power-allocation constraint defining the envelope compared with the coherent bosonic broadcast region. (source-ambiguity)

Selected references

• Classical capacity of bosonic broadcast communication and a new minimum output entropy conjecture, arXiv:0706.3416v1, https://arxiv.org/abs/0706.3416v1

Motivation

We introduce a new form for the bosonic channel minimal output entropy conjecture, namely that among states with equal input entropy, the thermal states are the ones that have slightest increase in entropy when sent through a infinitesimal thermalizing channel. We then detail a strategy to prove the conjecture through variational techniques. This would lead to the calculation of the classical capacity of a communication channel subject to thermal noise. Our strategy detects input thermal ensembles as possible solutions for the optimal encoding of the channel, lending support to the conjecture. However, it does not seem to be able to exclude the possibility that other input ensembles can attain the channel capacity.

This mission is the statement-level formalization of The bosonic minimum output entropy conjecture and Lagrangian minimization (arXiv:0906.2758v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Thermal and displaced thermal stationary witnesses and local output-entropy minima (Unnumbered main result: thermal stationarity and local output-entropy minima, PDF p. 1). 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

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

• Section I: finite conjecture: A proved unrestricted global vacuum-output entropy bound, rather than its conjecture. (hard)
• Section I: infinitesimal fixed-entropy conjecture: A proved global fixed-entropy instantaneous-rate inequality. (hard)
• Section VIII: claimed equivalence: A reverse implication from the finite pure-input minimum to the positive-entropy rate conjecture. (source-ambiguity)
• Section II, Eq.(5): entropy trace expansion: A source-specified trace differentiability domain and controlled second-order entropy remainder. (source-ambiguity)
• Section IV, Eqs.(6)–(8): all-cutoff stationarity: An exact N-to-N+1 cutoff dynamics, its rectangular dual, and order-of-time convention. (source-ambiguity)
• Section IV: energy-minimum attainment in a connected minimum manifold: A source-supported attainment condition on every connected minimum component. (source-ambiguity)
• Section V, Eqs.(9)–(13): double-stationary classification: Consistent complete primal/dual stationarity equations and common unbounded domains for all candidate solutions. (source-ambiguity)
• Section VI, Eq.(14): full thermal perturbation expansion: Norm/domain and remainder bound for the complete infinite-dimensional Eq.(14). (source-ambiguity)
• Section VII: attributed stationarity sufficiency: A valid second-order or convexity sufficiency hypothesis for Eq.(16). (source-ambiguity)
• Appendix 1: cutoff-independent stationary solutions and their limit: Consistent cutoff CCR, truncated Gibbs normalization, and a stationary-limit theorem. (source-ambiguity)
• Appendix 2: unqualified boundary asymptotic coefficient: A pinned, correct general boundary leakage coefficient and its trace domain. (source-ambiguity)

Selected references

• The bosonic minimum output entropy conjecture and Lagrangian minimization, arXiv:0906.2758v3, https://arxiv.org/abs/0906.2758v3

Motivation

A Nash equilibrium problem (NEP) asks for strategies of several players such that no player can lower its own cost by deviating while the others keep theirs fixed. NEPs model competition in electricity markets, environmental agreements, and the training of generative adversarial networks. When the players' problems are nonconvex, an equilibrium requires every player's strategy to be a global minimizer of a nonconvex problem, and even the special case of multilinear objectives over simplices is PPAD-complete (Daskalakis, Goldberg, Papadimitriou 2009). A second, less studied question is how to certify that a NEP has no equilibrium at all.

Nie and Tang treat NEPs in which all data are polynomials. They replace the equilibrium conditions by a polynomial system built from Lagrange multiplier expressions (Nie 2019), minimize a positive definite quadratic over it, and cut off candidates that are not equilibria. Their Theorem 3.3 states that for generic polynomial data this procedure stops after finitely many loops, either with an equilibrium or with a certificate that none exists. The paper also notes that a player problem (3.8) may have no minimizer, leaving the next cut undefined. This mission formalizes the finite loop bound and makes the attainment condition for an answer explicit.

Setting

There are $N$ players. Player $i$ chooses $x_i\in\mathbb R^{n_i}$; the joint strategy is $x=(x_1,\dots,x_N)\in\mathbb R^n$, $n=n_1+\dots+n_N$, and $(v,x_{-i})$ is $x$ with block $i$ replaced by $v$. Player $i$ solves

$$F_i(x_{-i}):\ \min_{x_i} f_i(x_i,x_{-i})\ \ \text{s.t.}\ \ g_{i,j}(x_i)=0\ (j\in E_i),\ \ g_{i,j}(x_i)\ge0\ (j\in I_i),$$

with $f_i\in\mathbb R[x]$, $g_{i,j}\in\mathbb R[x_i]$ and $E_i\sqcup I_i=[m_i]$. Its feasible set is $X_i$. A Nash equilibrium is a point $x^*\in X_1\times\dots\times X_N$ with $f_i(x^*)\le f_i(v,x^*_{-i})$ for all $i$ and all $v\in X_i$; $G^*$ is the set of all of them.

Let $G_i(x_i)$ be the $(n_i+m_i)\times m_i$ polynomial matrix whose column $j$ is $\nabla_{x_i}g_{i,j}$ above $g_{i,j}e_j$, and $\hat f_i(x)=(\nabla_{x_i}f_i(x),0)$. If a matrix polynomial $H_i(x_i)$ satisfies $H_iG_i=I_{m_i}$, the multiplier expressions are $\lambda_{i,j}(x)=(H_i(x_i)\hat f_i(x))_j$. The set $G$ consists of the $x$ with

$$\nabla_{x_i}f_i(x)=\sum_j\lambda_{i,j}(x)\nabla_{x_i}g_{i,j}(x_i),\quad g_{i,j}=0\ (j\in E_i),\quad 0\le\lambda_{i,j}(x)\perp g_{i,j}(x_i)\ge0\ (j\in I_i).$$

Algorithm 3.1 fixes a positive definite $\Theta$ and cut sets $K_i=\emptyset$. It repeatedly minimizes $[x]_1^T\Theta[x]_1$, $[x]_1=(1,x)$, over the points of $G$ satisfying $f_i(x)\le f_i(v,x_{-i})$ for all $v\in K_i$ (problem (3.10)). If (3.10) is infeasible it reports that there is no equilibrium. Otherwise it tests the minimizer $u$: it stops if $u$ is an equilibrium, and else adds to $K_i$ optimizers of $\min_{v\in X_i}f_i(v,u_{-i})$ for every player $i$ that can improve, and loops.

Generic data: fix degrees $a_{i,j}$ of $f_i$ in the block $x_j$ and degrees $d_{i,j}$ of $g_{i,j}$; the input is the vector $c$ of all coefficients, and a property is generic if it holds for all $c$ outside a Lebesgue-null set.

Formalization targets

Goal: Theorem 3.3

For positive degrees $a,d$, for almost every $c$, for all labels $E$, all $H$ with $H_iG_i=I$ and all positive definite $\Theta$:

$$\exists L^*\ \forall\ \text{runs completing } L \text{ loops}:\ L\le L^*,$$

At the end of every run, infeasibility of (3.10) implies $G^*=\emptyset$ while feasibility implies that (3.10) has a minimizer. If (3.8) attains a minimum for every player at every candidate in $G$, each partial run extends to a terminal run within the same loop bound, ending with an equilibrium or a correct infeasibility report. This qualification corrects the paper's unconditional answer claim.

Milestones

1. (3.6): if $H_iG_i=I$ for all $i$, then $G^*\subseteq G$.
2. Every equilibrium is feasible for (3.10) whenever the cut sets consist of feasible strategies.
3. (3.10) has a minimizer whenever it is feasible.
4. Theorem 3.2 (corrected): if $G\setminus G^*$ is finite, every run completes at most $|G\setminus G^*|$ loops; with attainment of (3.8), each partial run extends to a terminal one within that bound.
5. Generic nonsingularity: for almost every $c$, $G_i(\xi)$ has full column rank for every $\xi\in\mathbb C^{n_i}$ (the paper cites Nie, Ranestad 2009, Proposition 2.1).
6. Theorem A.1: for almost every $c$, the equality-constrained KKT system (A.1) has finitely many complex solutions $(x,\lambda)$.
7. For almost every $c$ and every $E$, the set of real KKT points is finite.

Significance

Theorem 3.3 is the termination guarantee for a method that computes Nash equilibria of nonconvex polynomial games and certifies their nonexistence; outside convex or special structured classes such guarantees are rare. Its two ingredients are of independent use. Theorem 3.2 bounds the loop count of a cutting-plane scheme by the number of KKT points that are not equilibria. Theorem A.1 is a generic finiteness result for multi-player KKT systems, the type of statement behind finite convergence of Moment-SOS hierarchies.

None of these results has a machine-checked proof. The mission provides a Lean model of polynomial NEPs, KKT points, multiplier expressions and nondeterministic algorithm runs, and a measure-theoretic notion of genericity for polynomial data, all reusable for the paper's companion results (Algorithm 3.7 for finding all equilibria, generalized NEPs).

Difficulty

The combinatorial part (Theorem 3.2) is short: each loop removes its candidate from a finite set. The difficulty lies in genericity. Milestone 7 needs Theorem A.1 for every sub-tuple of active constraints. Theorem A.1 is a dimension count in a product of projective spaces: the paper intersects a codimension-$\sum m_i$ variety with determinantal varieties and argues through birational maps and generic hyperplane sections. Converting "codimension $n$" into "finitely many points outside a Lebesgue-null set of real coefficients" requires showing that the bad coefficient set lies in a proper algebraic subset, and that such a subset is null. The naive route, a Bézout count, does not apply directly: the multipliers enter bilinearly and the system is not square in the usual sense when $m_i<n_i$. Milestone 1 needs KKT necessity for mixed equality and inequality constraints under LICQ, derived from $H_iG_i=I$.

Formalization scope

• Joint strategies are functions on $\Sigma_i\,\mathrm{Fin}(n_i)$; players and constraints are indexed from $0$; $I_i$ is the complement of the finset $E_i$. Gradients are formal partial derivatives.
• Nash equilibria are global and require feasibility. KKT points include $x\in X$, in particular $g_{i,j}=0$ for $j\in E_i$, which display (2.5) leaves implicit.
• $H_i$ is data with entries in $\mathbb R[x_i]$, and $H_iG_i=I$ is an identity of polynomial matrices, not a pointwise condition. The goal does not assert that such $H_i$ exists: for coefficient vectors where none exists it is vacuous, and the paper cites [Nie 2019] for existence under nonsingularity.
• The coefficient space has one real coordinate per admissible monomial with degree at most $a_{i,j}$ in block $x_j$ (resp. at most $d_{i,j}$), with product Lebesgue measure. Exact degree is itself generic, so this matches the paper's "degree $a_{i,j}$". The null set may depend only on the degrees, never on $E$, $H$ or $\Theta$. The goal holds for every positive definite $\Theta$, not only a generic one.
• A run of Algorithm 3.1 is any sequence of choices it permits: minimizers $u$ of (3.10), and nonempty sets of optimizers of (3.8) for players with $\omega_i<0$. The loop count is the number of completed Step 3's. "$\omega_i<0$" is the existence of a strictly improving feasible point; no real infimum is formed. Step38Solvable requires a minimizer of (3.8) for every player at every point of $G$; under it, every partial run has a terminal extension that preserves its earlier candidates and cut sets.
• Ruled out as trivializing: a run not tied to minimizing (3.10) or to cuts from (3.8); genericity as an arbitrary exceptional set; multipliers as free variables; finiteness of $G$ assumed instead of derived; local equilibria.
• Needed infrastructure: KKT necessity under LICQ for polynomial constraints, coercivity of positive definite quadratics, dimension theory of affine and multiprojective varieties over $\mathbb C$, and nullity of proper real algebraic subsets of coefficient space (a platform theorem covers the zero set of one nonzero polynomial). Contributions to any of these are welcome; the genericity layer is reusable for any "generic polynomial data" result.

Selected references

• J. Nie, X. Tang, Nash Equilibrium Problems of Polynomials, Mathematics of Operations Research, 2024; arXiv:2006.09490v2 (2023). https://arxiv.org/abs/2006.09490
• J. Nie, Tight relaxations for polynomial optimization and Lagrange multiplier expressions, Mathematical Programming 178 (2019). https://doi.org/10.1007/s10107-018-1276-2
• J. Nie, K. Ranestad, Algebraic degree of polynomial optimization, SIAM Journal on Optimization 20(1) (2009). https://doi.org/10.1137/080716670
• C. Daskalakis, P. W. Goldberg, C. H. Papadimitriou, The complexity of computing a Nash equilibrium, SIAM Journal on Computing 39(1) (2009). https://doi.org/10.1137/070699652
• F. Facchinei, C. Kanzow, Generalized Nash equilibrium problems, Annals of Operations Research 175 (2010). https://doi.org/10.1007/s10479-009-0653-x