All missions

Motivation

We study analogues of Jucys-Murphy elements in cellular algebras arising from repeated Jones basic constructions. Examples include Brauer and BMW algebras and their cyclotomic analogues.

This mission is the statement-level formalization of On Cellular Algebras with Jucys Murphy Elements (arXiv:0907.3459v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 6.10 (see [4], Lemma 2.3) — degenerate affine skein power identity (Lemma 6.10 (see [4], Lemma 2.3), PDF p. 24). 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

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

• Lemma 2.3 — globalizing arbitrary cell-module bases: CellModule, involution-twisted right module, cell-layer bimodule quotient, and compatible tensor-layer equivalence (hard)
• Lemma 2.9 ([17], Lemma 2.20) — simple modules and filtration multiplicities: Coherent cellular tower, scalar-extended cell modules, cell filtrations and actual inclusion multiplicities (hard)
• Corollary 2.10 — independence and Frobenius reciprocity of cell-filtration multiplicities: Filtrations of the actual induction and restriction modules and their cell-isomorphism counts (hard)
• Corollary 2.12 — strong coherence implies multiplicity-free generic branching: Strong coherence and the actual generic inclusion matrices (hard)
• Proposition 2.18 — restriction rule for the constructed path bases: Inductively constructed path bases, actual branching paths, restriction coefficients and higher-tail spans (hard)
• Corollary 2.19 — restriction rule for globalized cellular path bases: Globalizations of constructed path bases and their cell-ideal quotient action (hard)
• Proposition 3.6 — multiplicative JM triangularity and central product: Multiplicative JM family, scalar actions on constructed cell modules and path-basis triangularity (hard)
• Proposition 3.7 — additive JM triangularity and central sum: Additive JM family and the constructed path-basis action (hard)
• Lemma 3.10 — characterization of Gelfand–Zeitlin idempotents: Finite split semisimple tower, actual branching paths, primitive central idempotents and canonical GZ products (hard)
• Proposition 3.11 — separating JM elements generate the GZ algebra: Scalar-extended separated JM family and the actual GZ subalgebra (hard)
• Theorem 4.1 ([17], Theorem 3.2) — cellularity from basic constructions: All-eight-axiom basic-construction tower and its constructed cellular structure, cell modules and reflected branching diagram (hard)
• Theorem 5.1 — lifting multiplicative JM families (paper headline): Strong-framework pair, quotient maps, multiplicative JM predicates and resulting A-cell structure (hard)
• Corollary 5.2 — constant multiplicative lifting factor: Basic-construction labels and uniquely determined product-action scalars (hard)
• Theorem 5.3 — lifting additive JM families: Strong-framework pair, additive JM predicates and the basic-construction cell action (hard)
• Lemma 6.14 — generic injectivity of multiplication by e_n: Concrete universal admissible integer-polynomial omega sequence and canonical cyclotomic level map (hard)
• Proposition 6.16 — degenerate cyclotomic BMW strong framework: Specific generic admissible degenerate tower, Hecke quotient and full strong framework predicate (hard)
• Corollary 6.17 — strong coherence and path-labelled cells for admissible degenerate cyclotomic BMW algebras: Admissibility as freeness of W_2 e_1 and a strongly coherent multipartition-labelled cellular tower (hard)
• Proposition 6.18 — explicit Temperley–Lieb cell ideals: Temperley--Lieb presentation, specialized basic-construction cellular datum and its named cell ideals (hard)
• Lemma 6.20 — the Hecke quotient is the Temperley–Lieb algebra: Generic Hecke Murphy cell ideal and concrete Temperley--Lieb algebra over the enlarged ring (hard)
• §2.7, unnumbered — existence of path bases and their globalizations: Coherent family of actual restriction-filtration lifts and cell-layer globalizations (hard)
• §5, unnumbered — general multiplicative scalar formula: Lifted product action on basic-construction cell modules with alternating gamma indices (hard)
• §5, unnumbered — additive scalar formula and constant-factor specialization: Lifted additive action on basic-construction cell modules and its scalar (hard)
• §6.2, unnumbered — strongly coherent BMW cellular tower: Generic BMW presentation ring and constructed strongly coherent Young-diagram cellular datum (hard)
• §6.2, unnumbered / (6.1) — BMW JM family and eigenvalues: Concrete BMW recursive L elements and their action on constructed up-down cell bases (hard)
• §6.3, unnumbered — strongly coherent Brauer cellular tower: Brauer diagram algebra with loop-count multiplication and its constructed strongly coherent cell datum (hard)
• §6.3, unnumbered / (6.2) — unshifted Brauer JM family and eigenvalues: Concrete unshifted Brauer recursion and its actual up-down cell-module action (hard)
• §6.4.5, unnumbered — cyclotomic BMW cellular tower: Universal admissible nondegenerate coefficient ring and concrete cyclotomic BMW cellular tower (hard)
• §6.4.6, unnumbered / (6.4) — cyclotomic BMW JM family: Concrete universal-admissible cyclotomic BMW tower, y_1 recursion and up-down cell action (hard)
• §6.5.6, unnumbered / (6.7) — degenerate cyclotomic BMW additive JM family: Specific generic degenerate coefficient polynomials and constructed cell action of x_j (hard)
• §6.6, unnumbered — Temperley–Lieb cellular tower and label order: Generic Temperley--Lieb presentation with specific reversed cell order and strong filtrations (hard)
• §6.6, unnumbered — comparison of the two Temperley–Lieb cellular structures: Both actual Temperley--Lieb cellular structures, Hecke quotient map and cell-module comparison (hard)
• §6.6, unnumbered — Temperley–Lieb JM triangularity, product scalar and local relation: Concrete Hecke-derived Temperley--Lieb L sequence and both identified cell structures (hard)
• Example 3.1 / (3.1) — classical Hecke JM properties (background): Hecke presentation and literal Murphy cell modules and bases (hard)
• §6.3, unnumbered — symmetric-group additive JM family (background): Actual symmetric group algebra, additive JM recursion and q=1 Murphy cell-module specialization (hard)
• §6.4.6 / (6.3), unnumbered — cyclotomic Hecke multiplicative JM family (background): Cyclotomic Hecke presentation in the corrected quadratic convention and actual Murphy-type modules (hard)
• §6.5.6 / (6.6), unnumbered — degenerate cyclotomic Hecke additive JM family (background): Degenerate cyclotomic Hecke quotient and its literal Murphy-type cellular tower and basis action (hard)
• §3.1.1, unnumbered — maximal abelian GZ algebra and canonical idempotents: Actual multiplicity-free split semisimple tower, canonical central projectors and generated GZ algebra (hard)

Selected references

• On Cellular Algebras with Jucys Murphy Elements, arXiv:0907.3459v2, https://arxiv.org/abs/0907.3459v2

Motivation

Lie's Third Theorem, asserting that each finite-dimensional Lie algebra is the Lie algebra of a Lie group, fails in infinite dimensions. The modern account on this phenomenon is the integration problem for central extensions of infinite-dimensional Lie algebras, which in turn is phrased in terms of an integration procedure for Lie algebra cocycles. This paper remedies the obstructions for integrating cocycles and central extensions from Lie algebras to Lie groups by generalising the integrating objects. Those objects obey the maximal coherence that one can expect. Moreover, we show that they are the universal ones for the integration problem. The main application of this result is that a Mackey-complete locally exponential Lie algebra (e.g., a Banach-Lie algebra) integrates to a Lie 2-group in the sense that there is a natural Lie functor from certain Lie 2-groups to Lie algebras, sending the integrating Lie 2-group to an isomorphic Lie algebra.

This mission is the statement-level formalization of Categorified central extensions, 'etale Lie 2-groups and Lie's Third Theorem for locally exponential Lie algebras (arXiv:0812.1673v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is A discrete generalized cocycle gives the explicit loop prolongation (Lemma II.3: discrete cocycle loop prolongation, PDF p. 12). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

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

• Abstract and Theorem VI.5: Lie's Third Theorem for Mackey-complete locally exponential Lie algebras: Mackey-complete locally exponential Lie algebra; actual etale Lie 2-group and its Lie differentiation (hard)
• Lemma I.5: cycles and spherical 3-cocycle: Inconsistent printed diagonal filling normalization (5) (source-ambiguity)
• Lemma I.6: comparison of filling systems: Comparison of filling systems satisfying the inconsistent printed (5) (source-ambiguity)
• Lemma I.7: convex-chart fillers and comparison: Inconsistent filler extension claim and unspecified corner value of formula (9) (source-ambiguity)
• Remark I.8: actual period-valued integrating cocycle: Actual simplex integral of a left-invariant locally convex 2-form and its spherical period homomorphism (hard)
• Lemma I.9: differentiating a generalized cocycle: Intrinsic Bastiani differential and critical-point Hessian of a locally smooth quotient-valued cochain (hard)
• Theorem I.11: constructed cocycle integrates omega: The computed integrating cocycle and its actual antisymmetric Hessian (hard)
• Remark I.12: chart and cohomology representative independence: Both explicit integral comparison cochains for chart choice and cocycle representative (hard)
• Lemma I.13: local triviality yields a subgroup-valued remainder: Lie differentiation of a local cocycle and subgroup-valued global remainder for an arbitrary coefficient subgroup (hard)
• Remark I.14: obstruction for merely connected groups: Actual universal-cover obstruction determined by the constructed local splitting (hard)
• Lemma I.15: period image is contained in the associativity subgroup: Actual period image and differentiated local cocycle, with arbitrary subgroup Gamma (hard)
• Lemma I.16: three coefficient-compatibility equivalences: All three coefficient-compatibility assertions for the constructed spherical cocycle (hard)
• Proposition I.17: unique period-compatible coefficient map: Universal spherical 3-cocycle and the unique induced coefficient homomorphism (hard)
• Corollary I.18: universal integrating cocycle: Actual comparison morphisms and uniqueness of their coefficient map (hard)
• Example II.4: no compatible globally smooth loop multiplication: Standard smooth SU(2) loop group, normalized Kac-Moody cocycle and compatible-global-smoothness obstruction (hard)
• Lemma II.7: quotient of a locally smooth loop prolongation: Smooth local loop charts and quotient Lie structure for a generated loop prolongation (hard)
• Remark II.8: Lie algebra of a locally associative loop: Canonical Lie algebra of a locally associative smooth local loop and independence of restriction (hard)
• Proposition II.9: locally associative loop integration: Integration to an actual locally smooth and locally associative loop prolongation (hard)
• Example III.4: loop prolongation to a 2-group: Missing strict common tensor inverse for a general loop prolongation (source-ambiguity)
• Remark III.5: associated groups and source fibres: General nonstrict III.1 2-group, isomorphism-class group, identity component arrows and source fibres (hard)
• Theorem IV.1: local-to-global smooth group structure: Locally convex maximal smooth structures, local charts and compatible local-to-global Lie structure (hard)
• Example IV.2: cocycle central Lie group extension: Actual cocycle central extension with locally convex smooth atlas and a smooth local section (hard)
• Example IV.2: path-section cocycle of universal cover: Compact-open based-path group, universal cover and its actual path-section cocycle (hard)
• Proposition IV.5: strict 2-group globalization: Globalization of a strict smooth 2-space including strong source and target submersions (hard)
• Lemma IV.6: trivial principal source-fibre bundle: Actual source-fibre submanifold, tensor action and trivial principal bundle for a nonstrict 2-group (hard)
• Lemma IV.7: locally constant associator arrow part: Globally smooth nonstrict associator and its tensor-inverse arrow component (hard)
• Example IV.10: Cartan 3-cocycle and string 2-group: Integral Cartan normalization and strict inverse-triple associator normalization (source-ambiguity)
• Remark V.3: generalized cocycle extension 2-group: Failure of the stated strict two-sided tensor inversion for allowed generalized cocycles (source-ambiguity)
• Lemma V.4: canonical central 2-group extension: Named extension object need not be a III.1 2-group (source-ambiguity)
• Remark V.5: tangent 2-functor on pointed smooth 2-spaces: Actual tangent 2-functor from pointed locally convex Lie groupoids to internal topological vector categories (hard)
• Lemma V.9: canonical smooth generalized central extension: Canonical smooth structure on the potentially invalid V.3 strict-inverse object (source-ambiguity)
• Proposition V.10: ordinary band for discrete coefficient image: Band of a genuine smooth generalized central extension with discrete inherited coefficient image (hard)
• Corollary V.12: band integrates central algebra extension: Band of the named potentially invalid V.3/V.9 2-group (source-ambiguity)
• Remark V.13: canonical Lie differentiation 2-functor: Canonical Lie differentiation 2-functor of etale Lie 2-groups with a locally smooth associator (hard)
• Proposition V.14: derived split central Lie algebra extension: Differentiated actual maps of a smooth generalized central extension and their continuous linear splitting (hard)
• Theorem V.16: split central Lie algebra extensions integrate: Existence of a genuine smooth generalized central extension integrating a topologically split Lie algebra extension (hard)
• Remark V.17: cover factorization exact diagram: Inverse-triple associator normalization for the zero-twist cover and the full factorization diagram (source-ambiguity)
• Theorem VI.3 (cited): actual adjoint Lie group: Actual exponential-generated adjoint group and its locally exponential topology (hard)
• Example VI.4: non-complemented center Banach Lie algebra: Uncontrolled Banach-space bracket series and invalid separating-vector assertion (source-ambiguity)
• Remark VII.2: Cech transgression and principal 2-bundle: Printed Cech coefficient type and the actual principal 2-bundle construction (source-ambiguity)
• Remark A.2: chain rules and intrinsic critical-point Hessian: Bastiani first/second differential, tangent bundle and intrinsic critical-point Hessian (hard)
• Lemma A.4: exponential naturality: Actual locally convex tangent map and ODE-defined exponential function (hard)

Selected references

• Categorified central extensions, 'etale Lie 2-groups and Lie's Third Theorem for locally exponential Lie algebras, arXiv:0812.1673v3, https://arxiv.org/abs/0812.1673v3

Motivation

A simple unifying view of the exceptional Lie algebras is presented. The underlying Jordan pair content and role are exhibited. Each algebra contains three Jordan pairs sharing the same Lie algebra of automorphisms and the same external su(3) symmetry. Eventual physical applications and implications of the theory are outlined.

This mission is the statement-level formalization of Exceptional Lie Algebras, SU(3) and Jordan Pairs (arXiv:1112.1258v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is G2: the external A2 hexagon and two weight triangles (§4 opening, Fig. 2: the g2 prototype, PDF p. 5). 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

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

• §§1,4, unnumbered main result: three Jordan pairs with a common reduced structure algebra, equation (4.1): Compatible concrete complex exceptional Lie, Hurwitz-Hermitian Jordan, and triple-preserving pair models (hard)
• §4, unnumbered uniqueness assertion, specialized in §4.1.3: Equivalence relation and normalization of embedding uniqueness (source-ambiguity)
• §4.1.3: parallel planes, Jordan pair and three shared-a2 copies of c3: Root-compatible complex F4/C3 models and the symmetric-matrix Jordan pair (hard)
• §4.1.4: nested pair inside the central a2: Transport of the 1+2 matrix block Jordan pair to the specified central a2 (hard)
• §4.2.3: A5 root correspondence, Jordan pair and three shared-a2+a2 copies: Root-compatible E6/A5 embeddings and full 3x3 matrix Jordan-pair equivalences (hard)
• §4.2.4: ambiguous nested-pair multiplicity in a2+a2: Number and placement of nested (2,2bar) pairs in a2+a2 (source-ambiguity)
• §4.3.3: three shared-a5 copies of d6 and quaternionic Hermitian Jordan pairs: Complexified quaternionic H3 Jordan pair and root-compatible E7/D6 embeddings (hard)
• §4.3.4: the nested 3x3 matrix pair inside central a5: Root-compatible transport of the 3+3 sl6 grading to central a5 (hard)
• §4.4.3: three shared-e6 copies of e7 and Albert Jordan pairs: Concrete complex Albert pair and compatible E8/E7 Lie embeddings (hard)
• §4.4.4: four a2 factors and six Jordan pairs, equation (4.8): Compatible nested Lie/module/Jordan decomposition of actual complex E8 (hard)

Selected references

• Exceptional Lie Algebras, SU(3) and Jordan Pairs, arXiv:1112.1258v2, https://arxiv.org/abs/1112.1258v2

Motivation

We study the product formula $(fg)(A) = f(A)g(A)$ in the framework of (unbounded) functional calculus of sectorial operators $A$. We give an abstract result, and, as corollaries, we obtain new product formulas for the holomorphic functional calculus, an extended Stieltjes functional calculus and an extended Hille-Phillips functional calculus. Our results generalise previous work of Hirsch, Martinez and Sanz, and Schilling.

This mission is the statement-level formalization of Product formulas in functional calculi for sectorial operators (arXiv:1309.0318v2). 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 Abstract regularised calculus product formula (Theorem 2.5, PDF p. 7). 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

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

• Theorem 3.1: Sector-local H0-infinity contour calculus, B(S_phi), and H(A) (hard)
• Corollary 3.2: Sector-local holomorphic values of the three rationally damped symbols (hard)
• Proposition 4.3: Order-indexed bounded Stieltjes operator integral from a finite complex representing measure (hard)
• Lemma 4.4: Both computed bounded Stieltjes and holomorphic evaluations (hard)
• Proposition 4.5: Normed bounded Stieltjes evaluation for A and its scalar shifts (hard)
• Proposition 4.6: The actual bounded Stieltjes integral map on the union algebra (hard)
• Lemma 4.8: Extended Stieltjes regularisation from the bounded integral representation (hard)
• Lemma 4.9: Extended Stieltjes graph value and actual powers of A (hard)
• Proposition 4.10: Weighted complex-Radon Hirsch integral on dom(A^n), its graph closure, and resolvent conjugation (hard)
• Proposition 4.11: Closed Hirsch evaluations for A and A+delta on the explicit common core (hard)
• Theorem 4.12: Three independent computed Stieltjes, Hirsch, and holomorphic graph values (hard)
• Corollary 4.13: Independent Stieltjes and Hirsch graph evaluations without injectivity (hard)
• Lemma 4.14: Banach quotient by ker(A) and induced Stieltjes graphs (hard)
• Remark 4.15: Closed induced quotient calculus graph with its exact common core (hard)
• Theorem 4.16: Computed extended Stieltjes calculus for the scalar T_tilde algebra (hard)
• Corollary 4.17: Ordered finite composition of computed extended Stieltjes values (hard)
• Corollary 4.19: Computed extended Stieltjes sum on the intersection domain (hard)
• Lemma 5.3: C0 semigroup quotient by ker(A) and its computed extended HP evaluations (hard)
• Theorem 5.4: The same-semigroup HP strong integral and psi_k-regularised extension (hard)
• Corollary 5.5: Ordered finite products in the computed psi_k-extended HP calculus (hard)
• Example 5.6: Periodic differentiation generator on complex L2[0,1] and its HP counterexample graphs (hard)
• Unnumbered weak product formula in Section 4.4: Strong regularisers for the actual extended Stieltjes graph evaluation (hard)
• Unnumbered consistency of (5.7) with extended HP calculus: Computed HP evaluation of the geometric-mean square and the scalar product (hard)

Selected references

• Product formulas in functional calculi for sectorial operators, arXiv:1309.0318v2, https://arxiv.org/abs/1309.0318v2

Motivation

These lecture notes provide an elementary introduction, within the framework of finite quantum systems, to recent developments in the theory of entropic fluctuations.

This mission is the statement-level formalization of Entropic Fluctuations in Quantum Statistical Mechanics. An Introduction (arXiv:1106.3786v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

49 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Paper seed: finite-time quantum Evans–Searles symmetry (Proposition 3.3(7)) (Paper seed: finite-time quantum Evans–Searles symmetry (Proposition 3.3(7)), PDF p. 74). 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

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

• §1.4: classical entropy balance and nonnegative mean production: Finite pinned harmonic-chain Hamiltonian, its coupled Gaussian measure and relative-density entropy. (hard)
• §1.6–1.7: scalar and vector finite-time Evans–Searles relations: Actual harmonic-chain time-averaged entropy law with measurable time-reversal and Radon–Nikodym cocycle. (hard)
• Exercise 1.4 (explicit main result): Joint law of the two harmonic-chain time-averaged reservoir currents. (hard)
• §1.7: generalized finite-time Evans–Searles symmetry: Extended logarithmic Laplace integral of the actual joint current law, including divergent moments. (hard)
• §1.8: harmonic-chain thermodynamic limit: Finite-to-infinite Dirichlet-chain operators and Gaussian cylinder-measure convergence on configuration space. (hard)
• §1.9: complete harmonic-chain wave operators and on-shell scattering matrix: Concrete coupled/decoupled infinite-chain generators, complete wave operators and their Fourier representation. (hard)
• §1.10: Gaussian NESS and positive entropy production: Gaussian steady state built from the incoming complete wave operator on the actual harmonic chain. (hard)
• Exercise 1.7 (explicit main result): Harmonic-chain NESS current observables, and arbitrary stationary states with finite local second moments. (hard)
• §1.11: explicit asymptotic harmonic-chain pressures: Actual thermodynamic-then-time log-Laplace limits and their extended convergence domain. (hard)
• Exercise 1.9 (explicit main result): Complex Fredholm log-determinant continuation of the actual harmonic finite-time pressure. (hard)
• §1.12: harmonic-chain current central limit theorem: Harmonic current fluctuation random vector centered by its finite-time mean and degenerate Gaussian limit. (hard)
• §1.13: Onsager, Einstein and Green–Kubo relations: Differentiable harmonic-chain Gaussian NESS family and equilibrium current correlation. (hard)
• Exercise 1.12 (explicit main result): Actual equilibrium harmonic-chain correlations and the triangular Cesàro Green–Kubo average. (hard)
• Exercise 1.13 (explicit main result): Discrete Klein–Gordon propagation matrix elements and symmetric improper current-correlation limits. (hard)
• §1.14: harmonic-chain current LDP and rate symmetry: Borel laws of actual harmonic-chain mean currents, with extended rate and topological event bounds. (hard)
• §1.14: local current fluctuation probabilities: Harmonic current laws and shrinking-interval logarithmic probabilities with ordered limits. (hard)
• §1.15: harmonic-chain Gallavotti–Cohen theorem: Harmonic NESS Gaussian generating integrals and full LDP in that singular steady state. (hard)
• Theorem 2.19: Resolved source hypotheses, conventions and consistent full compound statement (source-ambiguity)
• §2.10: norm-convergent Dyson expansions and Gibbs perturbation series: Complex-time ordered-simplex integrals and recursively constructed Gibbs quotient coefficients. (hard)
• §2.12.1–2: modular and Connes-cocycle identities: Corrected list of modular/cocycle identities specifying which evolution is implemented by conjugation, while retaining every valid claimed identity. (source-ambiguity)
• Proposition 3.9: Resolved source hypotheses, conventions and consistent full compound statement (source-ambiguity)
• Proposition 3.10: Canonical n-factor product-state embeddings and a joint commuting modular spectral law. (hard)
• §3.8: joint FCS and modular-law identification: Canonical product factors and joint entropy-projector two-measurement law with vector modular identification. (hard)
• §4.1: open-system entropy and current balance: Canonical sample/reservoir tensor model with commuting charges, local gauge-invariant couplings and product reference state. (hard)
• §4.2: energy/charge joint FCS, cumulants and TRI symmetry: Energy/charge joint spectral FCS with all tensor embeddings and explicit deformed transfer generator. (hard)
• Proposition 4.1: Coupled Gibbs reference on the actual sample/reservoir tensor algebra and four energy/charge transport blocks. (hard)
• §4.3: transient response without time reversal: Actual coupled sample/reservoir Gibbs family and complex Kubo–Mori correlations for arbitrary observables. (hard)
• Proposition 5.1: A1–A6 nested matrix embeddings into a norm-dense unital C*-algebra, with limiting dynamics and FCS measures. (hard)
• Proposition 5.2: Modular GNS representation, A7 convergence and infinite signed relative entropy. (hard)
• Proposition 5.3: A8 bounded modular perturbation of a closed infinite standard Liouvillean on its genuine domain. (hard)
• Proposition 5.4: Infinite normal-state cone, generalized relative-entropy pressure and A5 flux family. (hard)
• Proposition 5.5: Infinite A1–A7 flux family with C2 generalized pressure and normalized finite-time transport coefficients. (hard)
• Proposition 5.6: Resolved source hypotheses, conventions and consistent full compound statement (source-ambiguity)
• §5.5: resonance method (conditional outline): Resolved source hypotheses, conventions and consistent full compound statement (source-ambiguity)
• Theorem 5.7: Real-time, finite-volume projection-test errors with iterated M liminf/limsup then t limit. (hard)
• §5.6(iii)–(v): testing bounds in the enveloping von Neumann algebra: Resolved source hypotheses, conventions and consistent full compound statement (source-ambiguity)
• §5.6(vi): quantum Hoeffding exponents: Normal states and all projection-test families in the enveloping von Neumann algebra, with three distinct exponents. (hard)
• §5.6(vii): all Stein exponents and optimal error rates: Six separate epsilon/vanishing-error projection-testing exponents in the enveloping von Neumann algebra. (hard)
• Proposition 5.8: A10 infinite analytic parameter family, KMS mixing and symmetric improper correlation limits. (hard)
• §5.9: stability under local KMS perturbation of reference: Normalized bounded local Araki KMS perturbation of an infinite modular state, with conditional NESS existence. (hard)
• §5.10: FCS means, covariances and response comparison: Explicit transient-to-stationary covariance interchange hypotheses, a corrected factor, and actual infinite FCS/current interfaces. (source-ambiguity)
• Proposition 6.3: CAR representations on an arbitrary Hilbert space, including infinite-dimensional representation spaces and unitary intertwiners. (hard)
• Proposition 6.4: Generated CAR star-algebra in all bounded operators on a potentially infinite representation Hilbert space. (hard)
• §6.2: specified infinite-dimensional extensions: An explicit corrected infinite-Fock statement distinguishing bounded trace-class differential second quantization from genuinely unbounded generators, with domains and cores. (source-ambiguity)
• Exercise 6.4 (explicit main result): Resolved source hypotheses, conventions and consistent full compound statement (source-ambiguity)
• Proposition 6.7: Actual doubled fermionic Araki–Wyss representation with conjugate second factor and cyclic vector. (hard)
• Proposition 6.8: Doubled AW modular conjugation/parity, logarithmic determinant scalar and generator with conjugation bars. (hard)
• §6.4: infinite-dimensional AW extension: Infinite CAR state representation, unbounded modular domains and trace-class logarithmic differences. (hard)
• Exercise 6.6 (explicit main result): Finite spin–fermion tensor GNS model and explicit n-reservoir deformed generator (6.11). (hard)
• §6.5: Spin–Fermion large-time claims (outline, not SF1–SF3): Resolved source hypotheses, conventions and consistent full compound statement (source-ambiguity)
• §6.6.2–3: EBB current and entropy identities: Actual EBB lead/sample CAR dynamics, finite-rank commutator fluxes and one-particle reference evolution. (hard)
• §6.6.4: finite EBB determinant pressures: Actual finite EBB sample/lead matrices and their many-body pressures, at all finite p and infinity. (hard)
• Exercise 6.10 (explicit main result): EBB finite approximants, infinite AW relative-modular logarithm and characteristic Fredholm determinants. (hard)
• Exercise 6.9 (explicit main result): Embedded EBB one-particle finite approximants and trace-norm convergence of determinant perturbations. (hard)
• §6.6.6: EBB NESS via complete wave operators: Concrete EBB finite sample with half-line leads, complete incoming wave operators and limiting CAR state. (hard)
• Exercise 6.11(1,2,4,5): explicit large-time pressure formulas: All scattering pressure functionals of the actual EBB model, including multiparameter symbols. (hard)
• §6.6.6: EBB large-time pressure formula (6.19): Concrete EBB ordered-volume/time pressure limit with the same complete on-shell scattering matrix. (hard)
• §6.6.6: NESS entropy production and open-channel criterion: EBB NESS, outgoing entropy/current observables and positive-measure open-channel criterion. (hard)
• Exercise 6.13 (explicit main result): Concrete EBB NESS currents and lead-indexed scattering transmission integrals. (hard)
• Exercise 6.15 (explicit main result): Joint reservoir charge-transfer two-measurement law, its Fredholm determinant and scattering limit. (hard)
• Exercise 6.16: reflectionless equivalences: Resolved source hypotheses, conventions and consistent full compound statement (source-ambiguity)
• Exercise 6.17 (explicit main result): Reflectionless two-lead finite intervals, their Fourier phase conventions and actual limiting CAR pressures. (hard)
• Exercise 6.18(1): on-shell scattering for general EBB reservoirs: General contact spectral-measure leads, cyclic reduction and limiting resolvent boundary values. (hard)
• §6.6.7: locally interacting EBB dynamics and Dyson expansion: Infinite CAR norm dynamics for a sample-local quartic interaction and its ordered Dyson series. (hard)
• §6.7.2: finite XY chain is unitarily equivalent to free fermions: Actual finite XY tensor-spin Hamiltonian, Jordan–Wigner strings and unitary Fock intertwiner. (hard)
• §6.7.3: XY-chain finite/thermodynamic determinant formula: Coupled XY Gibbs reference and even-algebra thermodynamic inclusions with trace-class determinant perturbation. (hard)
• §6.7.3: explicit XY pressure, heat current and positive production: Resolved source hypotheses, conventions and consistent full compound statement (source-ambiguity)
• Exercise 6.21 (explicit main result): Resolved source hypotheses, conventions and consistent full compound statement (source-ambiguity)
• §6.7.3: dilogarithm expression and analytic strip: Resolved source hypotheses, conventions and consistent full compound statement (source-ambiguity)
• §6.7.3: Jordan–Wigner survives on the even algebra: Compatible even spin/CAR local inclusions and the thermodynamic Jordan–Wigner isomorphism. (hard)
• Theorem A.6: Varying multidimensional probability experiments, extended cumulant domain, gradient steepness and Borel LDP bounds. (hard)
• Theorem A.7: Distinct limsup finite domain and actual-convergence/differentiability set, gradient image and local Borel LDP. (hard)
• Theorem A.8: Analytic multidimensional cumulant family with actual finite-time means and a possibly singular Gaussian probability law. (hard)

Selected references

• Entropic Fluctuations in Quantum Statistical Mechanics. An Introduction, arXiv:1106.3786v1, https://arxiv.org/abs/1106.3786v1

Motivation

We present a generalized version of classical geometric invariant theory `a la Mumford where we consider an affine algebraic group $G$ acting on a specific affine algebraic variety $X$. We define the notions of linearly reductive and of unipotent action in terms of the $G$ fixed point functor in the category of $(G,\Bbbk [X])$--modules. In the case that $X=\{\star\}$ we recuperate the concept of lineraly reductive and of unipotent group. We prove in our "relative" context some of the classical results of GIT such as: existence of quotients, finite generation of invariants, Kostant--Rosenlicht's theorem and Matsushima's criterion. We also present a partial description of the geometry of such linearly reductive actions.

This mission is the statement-level formalization of Reductive and unipotent actions of affine groups (arXiv:1406.4446v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Extensions of subgroup translation actions and normalized twisted cocycles (Observation 5.4, equations (4)–(7), PDF p. 12). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

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

• Introduction, unnumbered main result: transitivity of linearly reductive actions: Closed affine subgroup restriction of the specified regular right action; coordinate rational (G,k[X])-modules and Definition 2.1. (hard)
• Theorem 2.4: six equivalent characterizations: The full arbitrary-dimensional rational relative-module category, rational fixed-part right derived functors, total integrals, and injectivity in rational G-modules. (hard)
• Observation 2.5: further equivalent conditions: Diagonal rational tensor coactions, rational cohomology, and G-linear splitting of arbitrary relative inclusions. (hard)
• Observation 2.6(1–2): Reynolds characterization and identity: Natural linear projections on every rational relative module, with naturality for all R-linear colinear morphisms, and commutative relative algebra objects. (hard)
• Observation 2.6(3): claimed G-equivariance of a K-Reynolds operator: Printed assertion fails on permitted inputs or has an unpinned essential hypothesis. (source-ambiguity)
• Example 2.7(1): classical group reductivity and trivial actions: Classical exactness on all rational G-modules and Definition 2.1 for arbitrary rational commutative algebras, with nonzero R in the trivial-action converse. (hard)
• Example 2.7(2–3): change of scalars and products: Rational scalar extension and diagonal tensor algebra coactions, together with the contravariant coordinate action of geometric equivariant maps and products. (hard)
• Example 2.7(4): quotient action with a trivially acting normal subgroup: Printed assertion fails on permitted inputs or has an unpinned essential hypothesis. (source-ambiguity)
• Example 2.7(5): translation action is linearly reductive: The actual coordinate Hopf algebra of the affine group, its regular translation coaction, and all relative Hopf modules. (hard)
• Example 2.7(6): equivariant cross-section gives a trivial product: The closed algebraic fiber Phi inverse of 1, its regular equivariant product isomorphism with the specified inverse, and relative linear reductivity. (hard)
• Corollary 2.8: equivariant augmentation and fixed points: Equivariant algebra augmentation, classical rational group reductivity, and the geometric fixed-point/augmentation correspondence. (hard)
• Corollary 2.9: reductive stabilizers of affine orbits: Affine algebraic homogeneous spaces and affine orbit/stabilizer isomorphisms, including separability and characteristic-zero reductivity only in the final consequence. (hard)
• Lemma 2.10: multiplicative integrals for unipotent groups: Unipotent affine groups, multiplicative R-valued total integrals, and the associated Sweedler contraction Reynolds operators on every relative module. (hard)
• Theorem 2.11: product characterization for unipotent groups: A closed subvariety of X and a regular U-equivariant isomorphism X to L times U, with the specified translation/trivial action. (hard)
• Observation 2.12: algebra version, orbits and quotient: Rational tensor algebra decompositions without finite-generation restriction and their geometric orbit and quotient realizations for affine varieties. (hard)
• Theorem 3.3: subgroup translations, exact induction and affine quotient: Rational induction as the K-fixed submodule of k[G] tensor M, its exactness, algebraic homogeneous space affineness, observability, and ideal extension in k[G]^K. (hard)
• Example 3.4: observability cannot be omitted: Printed assertion fails on permitted inputs or has an unpinned essential hypothesis. (source-ambiguity)
• Theorem 3.5: linear reductivity on a homogeneous space: Affine homogeneous-space translations, rational subgroup induction and classical linear reductivity, with affineness in the left-hand conjunction. (hard)
• Theorem 4.1: generalized Matsushima criterion: Restriction along a closed subgroup and the canonical quotient-group action on R^K for normal K, on full rational relative-module categories. (hard)
• Observation 4.2(2): converse to restriction fails: The algebraic product Gm times Ga, its closed Gm subgroup, and trivial actions on the base field in rational relative categories. (hard)
• Observation 4.2(3): affineness through subgroup towers: Algebraic homogeneous-space quotient constructions and affineness in a tower of closed subgroup inclusions. (hard)
• Observation 4.2(4): geometric transitivity: Canonical affine quotient with coordinate ring k[X]^K and its induced G/K-action, together with restriction along closed subgroups. (hard)
• Observation 4.2(5): extension criterion for groups: Closed normal algebraic subgroup quotients and classical exact fixed-part functors on rational modules. (hard)
• Corollary 4.3: classical Matsushima criterion: Unipotent radicals, reductive affine groups and algebraic homogeneous quotients over an algebraically closed characteristic-zero field. (hard)
• Corollary 4.4: tower with a normal first inclusion: Homogeneous spaces L/K and L/G and the descended G/K-action on L/K, requiring K normal only in G. (hard)
• Theorem 4.5: descent from induced algebras: The actual rational induction functor on arbitrary K-modules and K-module algebras, and exactness of that functor. (hard)
• Theorem 4.6: induced affine varieties: The contracted product as the algebraic geometric quotient of X times G under a*(x,g)=(xa,a inverseg), including its induced right G-action. (hard)
• Theorem 4.7: claimed reduction to the unipotent radical: Printed assertion fails on permitted inputs or has an unpinned essential hypothesis. (source-ambiguity)
• Theorem 5.2: claimed Levi decomposition criterion: Printed assertion fails on permitted inputs or has an unpinned essential hypothesis. (source-ambiguity)
• Observation 5.3 and its continuation: claimed conjugation-compatible splitting: Printed assertion fails on permitted inputs or has an unpinned essential hypothesis. (source-ambiguity)
• Theorem 5.5: claimed explicit cocycle classification: Printed assertion fails on permitted inputs or has an unpinned essential hypothesis. (source-ambiguity)
• Theorem 6.1: finite generation of invariants: The rational relative commutative-algebra category, invariant subalgebra construction, and algebra finite generation over R and k. The printed self-base S typo also needs a recorded correction. (hard)
• Theorem 6.2: invariant ideals: The invariant subalgebra and actual ideal extension/comap between S^G and S for arbitrary commutative relative algebra objects and G-stable ideals. (hard)
• Theorem 6.3 and unnumbered quotient-existence claim: The precise source-cited semi-geometric quotient predicate, and the canonical Spec of the invariant algebra with the map induced by inclusion. (source-ambiguity)
• Section 6, unnumbered conclusion: quotient in two stages: Canonical affine invariant quotients, the geometric quotient by the actual unipotent radical, and the canonical comparison morphism for invariants in stages. (hard)
• Section 7, unnumbered result: the translation action is unipotent: The coordinate algebra coaction of left translation as a right action xg=g inversex and its inversion identification with right translation, on all relative modules. (hard)
• Lemma 7.2: unipotency under change of scalars: Definition 7.1 on all nonzero rational relative modules, scalar restriction, and the induced coordinate map for a regular equivariant morphism. (hard)
• Theorem 7.3: unipotent restriction and observability: Rational induction and algebraic observability, plus rational restriction for both module algebras and affine varieties. (hard)
• Observation 7.4: point, augmentation and exact-subgroup consequences: Unipotent affine groups via rational modules, equivariant augmentations/fixed points, rational exact induction and normal subgroup restriction. (hard)
• Theorem 7.5: generalized Kostant–Rosenlicht theorem: Zariski orbit closedness and regular homogeneous-space isomorphisms with closed unipotent stabilizers, conditional on separability only for the latter. (hard)
• Observation 7.6: classical orbit and subgroup consequences: Classical unipotent affine algebraic groups, their closed subgroups, and orbit closedness for affine algebraic actions. (hard)
• Lemma 7.8: every character extends for a unipotent action: Regular algebraic character group and nonzero semi-invariants of the specified coordinate coaction, with nonempty X. (hard)
• Observation 7.10(1) and consequence in (2): unipotency versus observability: Observable actions as nonzero fixed vectors in stable ideals, observable subgroups, unipotent relative modules, orbit closedness, and extendible rational characters. (hard)
• Observation 7.10(3): observable but non-unipotent example: The affine Gm-action on A2 with weights 1 and minus 1, stable coordinate ideals, observable action and unipotent action predicates. (hard)
• Theorem 7.11: simultaneous unipotency and linear reductivity: Separable regular affine actions, relative linear reductivity and unipotency, and closed-orbit algebraic isomorphisms with G (without a global product conclusion). (hard)

Selected references

• Reductive and unipotent actions of affine groups, arXiv:1406.4446v1, https://arxiv.org/abs/1406.4446v1

Motivation

We give a fresh account of the astonishing interplay between abelian von Neumann algebras, L^\infty-spaces and measure algebras, including an exposition of Maharam's theorem from the von Neumann algebra perspective.

This mission is the statement-level formalization of Abelian von Neumann algebras, measure algebras and L^\infty-spaces (arXiv:2108.06406v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

14 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 4.1: Existence of measure support (Lemma 4.1, PDF p. 12). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

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

• Theorem 2.1: Canonical multiplication representation and monotone convergence: Canonical complex L-infinity C*-algebra, characteristic projection measure, canonical L1 duality and L2 multiplication maps (hard)
• Lemma 2.2: Measure-preserving transfer of dualizability: Canonical complex L-infinity C*-algebra, characteristic projection measure, canonical L1 duality and L2 multiplication maps (hard)
• Theorem 2.3: Four equivalent descriptions of localizable measure spaces: Bounded L-infinity products, measured star decompositions and the canonical L1 duality interface (hard)
• Lemma 3.1: Complete additivity is normality: Positive cone of actual L-infinity, extended-valued weights, integration descent, normality and complete additivity on that cone (hard)
• Lemma 3.2: Measures and sigma-normal weights: Positive cone of actual L-infinity, extended-valued weights, integration descent, normality and complete additivity on that cone (hard)
• Corollary 3.3: Integration is normal for localizable measures: Positive cone of actual L-infinity, extended-valued weights, integration descent, normality and complete additivity on that cone (hard)
• Lemma 4.3: Support, complete additivity and relative semifiniteness: Positive cone of actual L-infinity, extended-valued weights, integration descent, normality and complete additivity on that cone (hard)
• Theorem 4.4: Radon–Nikodym for localizable measures I: Positive cone of actual L-infinity, extended-valued weights, integration descent, normality and complete additivity on that cone (hard)
• Corollary 4.5: Radon–Nikodym for localizable measures II: Positive cone of actual L-infinity, extended-valued weights, integration descent, normality and complete additivity on that cone (hard)
• Corollary 4.6: Absolutely continuous measures give normal weights on a sigma-finite base: Positive cone of actual L-infinity, extended-valued weights, integration descent, normality and complete additivity on that cone (hard)
• Theorem 4.7: Radon–Nikodym for Dedekind measures: Positive cone of actual L-infinity, extended-valued weights, integration descent, normality and complete additivity on that cone (hard)
• Lemma 5.1: Monotone completeness and order separation in abelian W*-algebras: Abstract W*-algebra with a chosen Banach predual, induced weak-star topology and its spectral/projection order (hard)
• Theorem 5.2: Six equivalent descriptions of localizability: Canonical L-infinity-to-B(L2) star representation, faithful von Neumann/masa range, chosen predual and RN-weight interfaces (hard)
• Proposition 5.4: Stonean spectrum and projection density: Abstract W*-algebra with a chosen Banach predual, induced weak-star topology and its spectral/projection order (hard)
• Theorem 7.15: Loomis–Sikorski representation: Concrete measurable-sets-mod-null Boolean quotient with measure and its actual isomorphisms (hard)
• Proposition 7.16: Extending Boolean maps to star homomorphisms: Projection Boolean lattice of an abstract W*-algebra, canonical extension of Boolean maps to star homomorphisms, normality and trace comparison (hard)
• Theorem 7.17: Localizable measure algebras have Radon realizations: Concrete measurable-sets-mod-null Boolean quotient with measure and its actual isomorphisms (hard)
• Theorem 7.19: Dixmier characterization: Chosen Banach predual and isometric complex star realization of C(K) as an actual L-infinity algebra (hard)
• Corollary 7.20: Abelian W*-algebras admit classical L-infinity realizations: Abstract W*-algebra, faithful normal semifinite trace, concrete normal realization and localizable L-infinity star realization (hard)
• Theorem 7.21: Trace-preserving classical realization: State/trace-preserving classical L-infinity star realization with characteristic projections and genuine measure atomlessness (hard)
• Theorem 7.22: Normal functionals and the unique predual: All Banach preduals with dual-identification compatibility and positive normal bounded functionals on abstract abelian W*-algebras (hard)
• Proposition 7.23: Normality and trace preservation of extended Boolean maps: Projection Boolean lattice of an abstract W*-algebra, canonical extension of Boolean maps to star homomorphisms, normality and trace comparison (hard)
• Theorem 7.24: Equivalence of measured Boolean and abelian von Neumann categories: Actual measured/unmeasured categories and the constructed projection functor, morphism restrictions and direct-sum comparison (hard)
• Theorem 7.25: Equivalence without a chosen measure: Actual measured/unmeasured categories and the constructed projection functor, morphism restrictions and direct-sum comparison (hard)
• Theorem 7.27: Concrete commutative von Neumann subalgebras: Embedded L-infinity for a sub-sigma-algebra, canonical weak-star topology and ambient order-closed projection operations (hard)
• Corollary 7.28: Bade characterization: Concrete C*-generation, order-closed Boolean projection closure and generated von Neumann algebra in the same Hilbert representation (hard)
• Corollary 7.29: Generators of an algebra and of its projection lattice: Concrete C*-generation, order-closed Boolean projection closure and generated von Neumann algebra in the same Hilbert representation (hard)
• Theorem 8.1: L-infinity is W* without semifiniteness: L-infinity W*-structure, sum/supremum of actual normal positive functionals, trivialized measure on the constructed anti-semifinite part (hard)
• Theorem 9.2: Homogeneous measure-algebra uniqueness: Exact Maharam cardinal for complete Boolean algebras and principal ideals, homogeneity, measured Boolean isomorphism (hard)
• Lemma 9.3: Atomic–diffuse decomposition: Canonical concrete corners, bounded/measured direct products, projection generator and decomposability cardinals, homogeneous components and magnitude (hard)
• Proposition 9.4: Infinite diffuse trace splits into probability summands: Canonical concrete corners, bounded/measured direct products, projection generator and decomposability cardinals, homogeneous components and magnitude (hard)
• Lemma 9.6: Decomposability cardinal of a direct sum: Canonical concrete corners, bounded/measured direct products, projection generator and decomposability cardinals, homogeneous components and magnitude (hard)
• Theorem 9.8: Projection generators and countable dependence: Actual projection-generator cardinal, strong topology on Boolean projections and complete generated closure membership (hard)
• Lemma 9.10: Homogeneous types are zero or infinite: Canonical concrete corners, bounded/measured direct products, projection generator and decomposability cardinals, homogeneous components and magnitude (hard)
• Lemma 9.11: Every projection contains a homogeneous part: Canonical concrete corners, bounded/measured direct products, projection generator and decomposability cardinals, homogeneous components and magnitude (hard)
• Lemma 9.12: Homogeneous decomposition: Canonical concrete corners, bounded/measured direct products, projection generator and decomposability cardinals, homogeneous components and magnitude (hard)
• Lemma 9.14: Disjoint homogeneous components sum to one: Canonical concrete corners, bounded/measured direct products, projection generator and decomposability cardinals, homogeneous components and magnitude (hard)
• Lemma 9.15: A sigma-finite component of infinite type is homogeneous: Canonical concrete corners, bounded/measured direct products, projection generator and decomposability cardinals, homogeneous components and magnitude (hard)
• Theorem 9.16: Finite-trace homogeneous uniqueness: Canonical concrete corners, bounded/measured direct products, projection generator and decomposability cardinals, homogeneous components and magnitude (hard)
• Theorem 9.17: Classification by magnitudes and weighted atom counts: Canonical concrete corners, bounded/measured direct products, projection generator and decomposability cardinals, homogeneous components and magnitude (hard)
• Proposition 9.18: Bernoulli tensor building blocks: Specified Bernoulli C*-inductive-limit block, incomplete tensor Hilbert space, GNS representation, von Neumann closure and product state; compatible measured direct sums (hard)
• Corollary 9.19: Normalized homogeneous algebras are Bernoulli tensor blocks: Specified Bernoulli C*-inductive-limit block, incomplete tensor Hilbert space, GNS representation, von Neumann closure and product state; compatible measured direct sums (hard)
• Theorem 9.20: Maharam theorem for von Neumann measure algebras: Specified Bernoulli C*-inductive-limit block, incomplete tensor Hilbert space, GNS representation, von Neumann closure and product state; compatible measured direct sums (hard)
• Corollary 9.21: Classification after forgetting trace: Specified Bernoulli C*-inductive-limit block, incomplete tensor Hilbert space, GNS representation, von Neumann closure and product state; compatible measured direct sums (hard)
• Proposition 9.23: C*-tensor block is continuous functions on a Cantor cube: Specified Bernoulli C*-inductive-limit block, incomplete tensor Hilbert space, GNS representation, von Neumann closure and product state; compatible measured direct sums (hard)
• Corollary 9.24: Von Neumann tensor block is the classical Bernoulli L-infinity: Specified Bernoulli C*-inductive-limit block, incomplete tensor Hilbert space, GNS representation, von Neumann closure and product state; compatible measured direct sums (hard)
• Corollary 9.25: Countable Bernoulli block is the Lebesgue interval algebra: Specified Bernoulli C*-inductive-limit block, incomplete tensor Hilbert space, GNS representation, von Neumann closure and product state; compatible measured direct sums (hard)
• Example 2.4: a semifinite nonlocalizable measure: Countable/co-countable counting L-infinity inclusion and measure-preserving conditional expectation (hard)
• Remark 4.8(3): unproved set-theoretic equivalence: The paper-specific meaning of measurable cardinal in the announced equivalence (source-ambiguity)
• Remark 7.26: projection functor preserves direct sums: Actual measured/unmeasured categories and the constructed projection functor, morphism restrictions and direct-sum comparison (hard)
• Unnumbered Dedekind and Stonean characterization: Canonical L-infinity Gelfand spectrum, norm-preserving real/complex Banach injectivity, and concrete 0/infinity-measure realization (hard)
• Example 8.2: normal integration does not imply W*: The specific Dixmier quotient of bounded Borel functions by the meager-support ideal, its norm/order and trivial integration weight (hard)
• Remark 9.22: probability-algebra refinement: Specified Bernoulli C*-inductive-limit block, incomplete tensor Hilbert space, GNS representation, von Neumann closure and product state; compatible measured direct sums (hard)
• Unnumbered extension after Corollary 9.25: Specified Bernoulli C*-inductive-limit block, incomplete tensor Hilbert space, GNS representation, von Neumann closure and product state; compatible measured direct sums (hard)
• Remark 9.22: classical description of L-infinity star isomorphisms: Specified Bernoulli C*-inductive-limit block, incomplete tensor Hilbert space, GNS representation, von Neumann closure and product state; compatible measured direct sums (hard)

Selected references

• Abelian von Neumann algebras, measure algebras and L^\infty-spaces, arXiv:2108.06406v2, https://arxiv.org/abs/2108.06406v2

Motivation

The quantum Schur transform is a fundamental building block that maps the computational basis to a coupled basis consisting of irreducible representations of the unitary and symmetric groups. Equivalently, it may be regarded as a change of basis from the computational basis to a simultaneous spin eigenbasis of Permutational Quantum Computing (PQC) [Quantum Inf. Comput., 10, 470-497 (2010)]. By adopting the latter perspective, we present a transparent algorithm for implementing the qubit quantum Schur transform which uses $O(\log(n))$ ancillas and can be decomposed into a sequence of $O(n^3\log(n)\log(\frac{n}{\epsilon}))$ Clifford + T gates, where $\epsilon$ is the accuracy of the algorithm in terms of the trace norm. We discuss the necessity for some applications of implementing this operation as a unitary rather than an isometry, as is often presented. By studying the associated Schur states, which consist of qubits coupled via Clebsch-Gordan coefficients, we introduce the notion of generally coupled quantum states. We present six conditions, which in different combinations ensure the efficient preparation of these states on a quantum computer or their classical simulability (in the sense of computational tractability). It is shown that Wigner 6-j symbols and SU(N) Clebsch-Gordan coefficients naturally fit our framework. Finally, we investigate unitary transformations which preserve the class of computationally tractable states.

This mission is the statement-level formalization of Generalised Coupling and An Elementary Algorithm for the Quantum Schur Transform (arXiv:2305.04069v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is General coupling preserves normalization and orthogonality in M (§IV.A, unnumbered: generally coupled states are normalized and M-orthogonal, PDF p. 13). 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

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

• Abstract / §V / Appendix A: clean qubit Schur transform with logarithmic ancillas: The compared maps and nuclear-norm error after spectator padding (source-ambiguity)
• §III.A, Algorithms 1–2: original clean Schur synthesis: Total padded local pre-mapping permutations and original clean source gate schedule (hard)
• §III.B: PQC bases block diagonalize the two Schur–Weyl actions: All-tree SU(2) coupled basis with both irreducible Schur–Weyl actions (hard)
• §III.C, Algorithms 3–4: general clean PQC synthesis: Complete general-tree CG blocks, total local ordering, routing and gate lists (hard)
• §IV.B, unnumbered: GC1–GC6 imply computational tractability: Uniform exact amplitude-evaluation and exact classical-sampling model for GC3–GC6 (source-ambiguity)
• §IV.C, unnumbered: efficient preparation without GC4: Computational model for coefficient-driven unitary synthesis and its target accuracy (source-ambiguity)
• §IV.C, unnumbered: logarithmic ancillas for sequential individual-state preparation: Live-register schedule attached to sequential individual-state preparation (hard)
• §IV.D, unnumbered: fixed-rank SU(N) coupling conditions and preparation: Phase-fixed GT CG coefficients and uniform exact evaluation/preparation semantics (source-ambiguity)
• §IV.D, unnumbered: fixed-dimensional qudit extension of PQC circuits: All-label fixed-d qudit pre-mapping and clean SU(d)-CG gate schedule (hard)
• §IV.E, Eqs.(52)–(57): Wigner coupling conditions and failure of GC4: Normalized finite Racah tensor with admissible triangular domains and uniform coefficient programs (hard)
• §V, Eqs.(77)–(78): exact total qubit counts: Concrete original and compressed register-liveness traces whose maxima are counted (hard)
• Lemma VI.2: one Hadamard preserves a CT family: Operational CT-family model with exact amplitudes and conditional sampling (source-ambiguity)
• §VI, unnumbered: one arbitrary computable single-qubit gate preserves CT: Uniform computable one-qubit coefficient access in an exact CT-family model (source-ambiguity)
• Claim A.1: O(n^3) two-level rotations for Schur transform: Concrete source-compatible sequential pre-map and clean two-level circuit target (hard)
• Claim A.3: O(n^6) two-level rotations for general PQC unitary: Concrete arbitrary-tree source unitary and active two-level decomposition interface (hard)
• Claim A.4: O(n^3) two-level rotations for individual PQC state: Concrete general PQC state amplitudes and their active two-level preparation interface (hard)
• Appendix A, Table II: remaining Clifford+T bounds: Separate nuclear-norm circuit-map and prepared-state approximation conventions (source-ambiguity)

Selected references

• Generalised Coupling and An Elementary Algorithm for the Quantum Schur Transform, arXiv:2305.04069v3, https://arxiv.org/abs/2305.04069v3

Motivation

We give an efficient randomized algorithm for approximating an arbitrary element of $SU(2)$ by a product of Clifford+$T$ operators, up to any given error threshold $\epsilon>0$. Under a mild hypothesis on the distribution of primes, the algorithm's expected runtime is polynomial in $\log(1/\epsilon)$. If the operator to be approximated is a $z$-rotation, the resulting gate sequence has $T$-count $K+4\log_2(1/\epsilon)$, where $K$ is approximately equal to $10$. We also prove a worst-case lower bound of $K+4\log_2(1/\epsilon)$, where $K=-9$, so that our algorithm is within an additive constant of optimal for certain $z$-rotations. For an arbitrary member of $SU(2)$, we achieve approximations with $T$-count $K+12\log_2(1/\epsilon)$. By contrast, the Solovay-Kitaev algorithm achieves $T$-count $O(\log^c(1/\epsilon))$, where $c$ is approximately $3.97$.

This mission is the statement-level formalization of Efficient Clifford+T approximation of single-qubit operators (arXiv:1212.6253v2). 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 Units and totally nonnegative unit squares (Lemma 10: units and totally nonnegative unit squares, 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

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

• Abstract and §1: efficient ancilla-free Clifford+T approximation (seed): Uniform prime-candidate/seed law and a real-input access convention for the bundled efficient compiler. (source-ambiguity)
• Theorem 12: relative norm equation and randomized construction: Binary-cost randomized norm-solver execution on coefficient-encoded Z[omega]. (hard)
• Theorem 22: candidate count and efficient sampling: Full printed epsilon>0 candidate enumerator and efficient uniform sampler outside the intended small-error geometry. (source-ambiguity)
• Algorithm 23: returned-circuit correctness: Successful finite execution trace joining candidate generation, norm-solver attempts, checked acceptance and exact gate synthesis. (hard)
• §8.1: successful-output T-count bounds: Source exact-synthesis/normalization output interface with denominator exponent and actual returned-word T-count. (hard)
• Remark 28: fixed Clifford+T conjugation: Uniform slope-four z-rotation approximation family before fixed-word conjugation. (source-ambiguity)
• §8.2 and Hypothesis 29: expected runtime: Uniform pointwise probability law for Hypothesis 29 and source-specific bit-runtime input model. (source-ambiguity)
• §8.3: seeding and T-count overhead: Specified angle-seed and bounded-T-count-word seed laws with successful-seed probability and restart cutoff. (source-ambiguity)
• §10: additive overclocking claim: Quantified admissible additive decrement and successful-beta fraction for overclocked sampling. (source-ambiguity)

Selected references

• Efficient Clifford+T approximation of single-qubit operators, arXiv:1212.6253v2, https://arxiv.org/abs/1212.6253v2

Motivation

The celebrated Evans-Searles, respectively Gallavotti-Cohen, fluctuation theorem concerns certain universal statistical features of the entropy production rate of a classical system in a transient, respectively steady, state. In this paper, we consider and compare several possible extensions of these fluctuation theorems to quantum systems. In addition to the direct two-time measurement approach whose discussion is based on (LMP 114:32 (2024)), we discuss a variant where measurements are performed indirectly on an auxiliary system called ancilla, and which allows to retrieve non-trivial statistical information using ancilla state tomography. We also show that modular theory provides a way to extend the classical notion of phase space contraction rate to the quantum domain, which leads to a third extension of the fluctuation theorems. We further discuss the quantum version of the principle of regular entropic fluctuations, introduced in the classical context in (Nonlinearity 24, 699 (2011)). Finally, we relate the statistical properties of these various notions of entropy production to spectral resonances of quantum transfer operators. The obtained results shed a new light on the nature of entropic fluctuations in quantum statistical mechanics.

This mission is the statement-level formalization of Entropic Fluctuations in Statistical Mechanics II. Quantum Dynamical Systems (arXiv:2409.15485v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Finite ancilla tomography recovers the entropic functional (finite-ancilla-tomography, PDF p. 13). 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

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

• theorem-2.1: An unambiguous corrected source statement for theorem-2.1 (source-ambiguity)
• continuous-2tm-extension: An unambiguous corrected source statement for continuous-2tm-extension (source-ambiguity)
• proposition-2.2: The actual open-system Mat2(O) perturbed dynamics and Araki–Connes ancilla functional (hard)
• proposition-2.3: Canonical modular spectral probability and extended Araki entropy (hard)
• theorem-2.5: An unambiguous corrected source statement for theorem-2.5 (source-ambiguity)
• proposition-2.6: The quantum 2tm law and its speed-t full/local LDP (hard)
• weak-quantum-rigidity: Canonical extension of 2tm laws to singular NESS and reservoir modular averaging (hard)
• proposition-2.9: Unique O-valued analytic Connes extension and the NESS characteristic law for every real t (hard)
• ancilla-analytic-continuation: Conjugated-parameter cocycle product evaluated in an arbitrary singular algebraic state (hard)
• proposition-2.11: The analytic perturbation orbit and constructed Dyson cocycle of an open system (hard)
• proposition-2.12: Natural-cone comparison for the actual evolved reference and ancilla functional (hard)
• two-time-comparison: Modular Cesaro definition of 2tm statistics on evolved reference states (hard)
• ancilla-exchange-of-limits: Actual real-alpha ancilla functionals in a general NESS open system (hard)
• classical-exchange-of-limits: An unambiguous corrected source statement for classical-exchange-of-limits (source-ambiguity)
• classical-discrete-analogue: An unambiguous corrected source statement for classical-discrete-analogue (source-ambiguity)
• proposition-2.17: Relative Tomita construction and time-covariant Connes cocycle in the GNS algebra (hard)
• theorem-2.18: Unbounded modular logarithms and bounded relative Hamiltonian derived from Qu1; canonical quantum Cesaro NESS production positivity (p.26 Remark 1) (hard)
• open-system-entropy-observable: Unbounded logarithmic modular perturbation formula and modular derivation domain (hard)
• reference-functional-identity: The three canonically defined algebraic quantum functionals (hard)
• proposition-3.1: Canonical standard Liouvillean and quantum transfer group from the actual Connes family (hard)
• ancilla-generator-similarity: Modular spectral powers acting on the actual closed ancilla generator domain (hard)
• proposition-3.2: The distinct physical quantum transfer groups and finite-time functionals (hard)
• theorem-4.3: Canonical 1/2-Liouvillean weighted resolvent, D inverse domain, and algebraic NESS state (hard)
• theorem-4.4: Deform2 on actual quantum groups, singular NESS evaluations, and modular-power domains (hard)
• theorem-4.5: Deform3 and the physical cumulants of the genuine modular resonance family (hard)
• alternative-ancilla-resonance: An unambiguous corrected source statement for alternative-ancilla-resonance (source-ambiguity)
• proposition-4.6: Bounded weighted composition on L2 classes for a non-measure-preserving flow (hard)
• classical-transfer-representations: The L2 weighted transfer group and its actual generator, not just its scalar integral (hard)

Selected references

• Entropic Fluctuations in Statistical Mechanics II. Quantum Dynamical Systems, arXiv:2409.15485v2, https://arxiv.org/abs/2409.15485v2

Motivation

This paper attempts to develop a theory of sufficiency in the setting of non-commutative algebras parallel to the ideas in classical mathematical statistics. Sufficiency of a coarse-graining means that all information is extracted about the mutual relation of a given family of states. In the paper sufficient coarse-grainings are characterized in several equivalent ways and the non-commutative analogue of the factorization theorem is obtained. Among the applications the equality case for the strong subadditivity of the von Neumann entropy, the Imoto-Koashi theorem and exponential families are treated. The setting of the paper allows the underlying Hilbert space to be infinite dimensional.

This mission is the statement-level formalization of Sufficiency in quantum statistical inference (arXiv:math-ph/0412093v1). 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 Lemma 1: countable common-null-set subfamily (Lemma 1: countable common-null-set subfamily, 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

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

• Unnumbered: classical minimal sufficient sigma-algebra: An additional reference-measure condition for the claimed minimal sufficient density algebra (source-ambiguity)
• Theorem 1: five criteria for a sufficient subalgebra: Natural-cone PA, Connes cocycles, and the computed generalized conditional expectation (hard)
• Lemma 3: monotonicity of canonical cone overlap: Positive trace-class square-root realization and trace of the product of Hilbert-Schmidt square roots (hard)
• Lemma 4 and its concluding converse: equality in overlap monotonicity: Support-zero spectral imaginary powers, the actual Heisenberg adjoint, and canonical cone overlap (hard)
• Proposition 3: classical factorization criterion: Common-reference almost-everywhere factorization (source-ambiguity)
• Unnumbered: sufficiency survives support compression: Computed support-corner algebras and their normal 2-positive compression/extension maps (hard)
• Unnumbered: modular characterization of recovery fixed algebras: Constructed generalized dual, modular group, and fixed-point star algebras (hard)
• Theorem 2: six equivalent sufficiency and canonical-recovery conditions: Canonical generalized dual and computed multiplicative-domain image and recovery fixed algebras (hard)
• Remark after Theorem 2: relative-entropy equality iff canonical recovery: Computed canonical normal recovery channel for finite extended-relative-entropy equality (hard)
• Unnumbered: noncommuting experiments have no sufficient measurement: The computed minimal sufficient algebra and general commutative-domain sufficient measurements (hard)
• Equation (16): modular-invariant reference-state factorization: Canonical type-I trace densities and an affiliated positive central correction (hard)
• Theorem 3: noncommutative factorization criterion (seed main result): Canonical modular-invariant density factorization with a computed central affiliated factor (hard)
• Unnumbered: cocycle-generated minimal sufficient algebra: Cocycle-generated minimal sufficient algebra, modular invariance, and its canonical S-factorization (hard)
• Theorem 4: maximality of canonical S-factorization: The canonical S-factors and a possibly unbounded affiliated maximality correction R0 (hard)
• Unnumbered: canonical direct-sum tensor S-decomposition and uniqueness: A canonical countable orthogonal completed-Hilbert tensor decomposition and compatible uniqueness relation (hard)
• Theorem 5: sufficient channel block structure and induced S-decomposition: Canonical source and target S-blocks, their normal right maps, and the extended positive-weight dual (hard)
• Corollary 1: Kraus block criterion for finite-dimensional sufficiency: The actual finite-dimensional canonical S-decomposition and operator transport into its tensor blocks (hard)
• Corollary 2: claimed nondisturbance Kraus commutation criterion: A correct condition for right-factor stationary states (source-ambiguity)
• Example 4: claimed local unique entropy-constrained exponential fit: Nondegeneracy for the local moment map and multiplier uniqueness (source-ambiguity)
• Equations (23)–(25): variationally perturbed state, Gibbs formula and support: Normalized modularly perturbed states and their unnormalized positive vector functionals (hard)
• Theorem 6 [15]: sufficiency criteria for an exponential family: Normalized modularly perturbed states and their unnormalized positive vector functionals (hard)
• Unnumbered: minimum free energy, analyticity and derivative identity: Normalized modularly perturbed states and their unnormalized positive vector functionals (hard)
• Theorem 7: sufficient coarse-grainings of exponential families: Normalized modularly perturbed states and their unnormalized positive vector functionals (hard)
• Remark after Theorem 7: matrix logarithmic sufficiency criterion: A computed faithful quantum exponential family and correctly typed logarithmic trace-dual criterion (hard)
• Corollary 3: commutative sufficient subalgebras of exponential families: Normalized modularly perturbed states and their unnormalized positive vector functionals (hard)
• Theorem 8: countable Markov block structure at SSA equality: A countable completed-Hilbert Markov block decomposition of B and transported density equality (hard)
• Unnumbered: pure-state SSA equality yields a single product block: Support-level tensor splitting of a purification, with actual transported product vectors (hard)
• Equation (30): claimed non-atomic direct-integral normal density: A valid normal-state model for a non-atomic direct integral (source-ambiguity)
• Appendix: support-corner dual and generalized conditional expectation (31): Canonical support-corner generalized dual and its normal predual, including the CP specialization (hard)

Selected references

• Sufficiency in quantum statistical inference, arXiv:math-ph/0412093v1, https://arxiv.org/abs/math-ph/0412093v1

Motivation

We present a phase space formulation of quantum mechanics in the Schr"odinger representation and derive the associated Weyl pseudo-differential calculus. We prove that the resulting theory is unitarily equivalent to the standard "configuration space" formulation and show that it allows for a uniform treatment of both pure and mixed quantum states. In the second part of the paper we determine the unitary transformation (and its infinitesimal generator) that maps the phase space Schr"odinger representation into another (called Moyal) representation, where the wave function is the cross-Wigner function familiar from deformation quantization. Some features of this representation are studied, namely the associated pseudo-differential calculus and the main spectral and dynamical results. Finally, the relation with deformation quantization is discussed.

This mission is the statement-level formalization of Quantum mechanics in phase space: The Schr"odinger and the Moyal representations (arXiv:1209.1850v1). 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 Unitary equivalence with the window subspace (Abstract main result: unitary equivalence with configuration space, 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

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

• §3, unnumbered: mixed-state eigenspace and convex probability claim: Consistent mixed-state observable and projection conventions (source-ambiguity)
• §3, unnumbered: projection and collapse probability claim: Consistent mixed-state observable and projection conventions (source-ambiguity)
• Theorem 4.6: Continuous exterior distribution product, partial-Fourier Weyl kernel, and independent double-phase symbol transform (hard)
• Theorem 4.7: Schwartz tensor/contraction maps and their correct distribution transposes (hard)
• Corollary 4.8: Kernel-defined Weyl operators on Schwartz inputs and nonzero window-contraction interface (hard)
• Theorem 5.7: Independent Weyl-symbol submersion pullback and Schwartz/distribution U conjugation (hard)
• Corollary 5.10: Distribution-valued time derivative and independent star-product Hamiltonian action (hard)
• Corollary 5.11: Generic tempered Weyl/star operators and Schwartz-domain U/window intertwiners (hard)
• Corollary 5.9: Independently constructed tempered-symbol Moyal product and Moyal operator (hard)

Selected references

• Quantum mechanics in phase space: The Schr"odinger and the Moyal representations, arXiv:1209.1850v1, https://arxiv.org/abs/1209.1850v1

Motivation

The monotone complementarity problem (MCP) asks, for a continuous monotone map $f$ on the positive orthant, for a pair $(x,s)$ with $s=f(x)$, $x\ge0$, $s\ge0$ and $x_js_j=0$ for every $j$. It contains linear programming, convex quadratic programming, the monotone linear complementarity problem and the Karush–Kuhn–Tucker conditions of smooth convex programs. Interior-point methods solve it in polynomially many Newton-type steps when a strictly positive, well-centered starting point is known, but in general no such point is known, and the problem may be infeasible or feasible without any positive feasible point.

Andersen and Ye (Mathematical Programming 84, 1999) extended the homogeneous self-dual embedding of linear programming to the nonlinear MCP: one embeds the problem into a homogeneous problem that always has a trivial interior starting point, solves it by a path-following method, and reads off either a solution or a certificate of infeasibility. Section 8.4 of Ye, Interior Point Algorithms: Theory and Analysis (Wiley 1997, doi:10.1002/9781118032701) presents this construction, the convexity property of the residual set it rests on, and the analysis of one step of the algorithm. This mission formalizes that section.

Setting

Vectors are compared componentwise; $e$ is the all-ones vector, $X=\operatorname{diag}(x)$, $S=\operatorname{diag}(s)$, $\|\cdot\|$ the Euclidean norm and $\mathbb R^N_{++}=\{x\in\mathbb R^N: x>0\}$ the open orthant. A map $f:\mathbb R^n_{++}\to\mathbb R^n$ is monotone if $(x^1-x^2)^T(f(x^1)-f(x^2))\ge0$ for all $x^1,x^2>0$; $\nabla f(x)$ denotes its Jacobian.

The residual set is $R_{++}=\{s-f(x): x>0,\ s>0\}$, and for $r\in\mathbb R^n$ the slice $S_{++}(r)=\{(x,s)\in\mathbb R^{2n}_{++}: s=f(x)+r\}$.

The homogeneous map on $\mathbb R^{n+1}_{++}$, with points written $(x;\tau)$, is

$$\psi(x,\tau)=\begin{pmatrix}\tau f(x/\tau)\\-x^Tf(x/\tau)\end{pmatrix}.$$

The homogeneous model (HMCP) asks for $(x,\tau,s,\kappa)\ge0$ with $(s;\kappa)=\psi(x,\tau)$ minimizing $x^Ts+\tau\kappa$.

A map $g$ on $\mathbb R^N_{++}$ is scaled Lipschitz with a monotone increasing $v:(0,1)\to(1,\infty)$ if

$$\|X(g(x+d)-g(x)-\nabla g(x)d)\|_1\le v(\alpha)\,d^T\nabla g(x)d\quad\text{whenever }x>0,\ \|X^{-1}d\|_\infty\le\alpha<1.$$

The algorithm works in $\mathbb R^{n+1}$ with $x:=(x;\tau)$ and $s:=(s;\kappa)$. At an iterate $(x^k,s^k)>0$ let $r^k=s^k-\psi(x^k)$ and $\mu^k=(x^k)^Ts^k/(n+1)$. The direction $(d_x,d_s)$ solves

$$d_s-\nabla\psi(x^k)d_x=-\eta r^k,\qquad X^kd_s+S^kd_x=\gamma\mu^ke-X^ks^k,$$

and for a step size $\alpha$ the new iterate is $x^+=x^k+\alpha d_x$ and $s^+=s^k+\alpha d_s+\psi(x^+)-\psi(x^k)-\alpha\nabla\psi(x^k)d_x$.

Formalization targets

Goal: one step of the homogeneous algorithm stays centered (Theorem 8.29)

Assume $\psi$ is scaled Lipschitz with $v_\psi$, and let

$$\beta=\frac1{3+4v_\psi(\sqrt2/2)},\qquad\eta=\frac\beta{\sqrt{n+1}},\qquad\gamma=1-\eta,\qquad\alpha=1.$$

If $(x^k,s^k)>0$ and $\|X^ks^k-\mu^ke\|\le\beta\mu^k$, then $\beta\le1/3$ and

$$x^+>0,\qquad s^+=\psi(x^+)+(1-\eta)r^k>0,\qquad\|X^+s^+-\mu^+e\|\le\beta\mu^+,\quad\mu^+=\frac{(x^+)^Ts^+}{n+1}.$$

Milestones

• Lemma 8.20: for $(x^i,s^i)\in S_{++}(\theta^ir)$, $(\theta^2-\theta^1)r^T(x^2-x^1)\le(x^2-x^1)^T(s^2-s^1)$.
• Lemma 8.21: for $\theta^0\le\theta^1$ with nonempty slices, $\bigcup_{\theta\in[\theta^0,\theta^1]}\{(x,y)\in S_{++}(\theta r): x^Ty\le\delta\}$ is bounded.
• Theorem 8.23: $R_{++}$ is open and convex.
• Lemma 8.24: if $\nabla f$ is positive semi-definite, so is $\nabla\psi$.
• Theorem 8.25 (i): $\psi$ is continuous and homogeneous of degree 1, $(x;\tau)^T\psi(x,\tau)=0$ and $(x;\tau)^T\nabla\psi(x,\tau)=-\psi(x,\tau)^T$.
• Theorem 8.25 (ii): $\psi$ is continuous and monotone when $f$ is.
• Lemma 8.27: $d_x^Td_s=d_x^T\nabla\psi(x^k)d_x+\eta(1-\eta-\gamma)(n+1)\mu^k$.
• Lemma 8.28: $r^+=(1-\alpha\eta)r^k$ and $(x^+)^Ts^+=(x^k)^Ts^k(1-\alpha(1-\gamma))+\alpha^2\eta(1-\eta-\gamma)(n+1)\mu^k$.

Stronger: monotonicity of $f$ is not needed

The goal remains true when $f$ is only assumed differentiable on $\mathbb R^n_{++}$ and $\psi$ scaled Lipschitz; this variant is posed beside the goal (see Formalization scope).

Significance

Theorem 8.29 is the one-step invariant behind the $O(\sqrt n\log(1/\epsilon))$ iteration bound of the homogeneous algorithm: combined with Lemma 8.28 it shows that the infeasibility residual and the complementarity gap shrink by the same factor $1-\beta/\sqrt{n+1}$ per step while the iterates stay in a fixed neighborhood of the central path. Together with Theorem 8.25 (v)–(vi), which identifies solutions and infeasibility certificates of the MCP from maximal complementary solutions of the homogeneous model, this yields an algorithm that needs no feasible starting point and detects infeasibility. The convexity of $R_{++}$ (Theorem 8.23) is the structural fact that makes the homotopy path of the homogeneous model well defined.

These results are proved in the book (with Theorem 8.19, which Theorem 8.23 uses, left as an exercise). None of them is formalized on the platform: the existing Andersen–Ye material covers only the linear complementarity case, as a set-valued operator, and no statement about scaled Lipschitz maps or the nonlinear homogeneous map exists. A completed development gives a machine-checked analysis of an interior-point step for a nonlinear problem, with every constant explicit.

Difficulty

The algebra of Lemmas 8.27 and 8.28 depends on the identities $x^T\psi(x)=0$ and $x^T\nabla\psi(x)=-\psi(x)^T$, which require differentiating a map defined through $x/\tau$; working with $\nabla\psi$ as a Fréchet derivative rather than a hand-written block matrix is part of the work. In Theorem 8.29 the nonlinearity enters only through the scaled Lipschitz bound, which applies only when $\|X^{-1}d_x\|_\infty<1$, so the step must first be shown to stay well inside the orthant before the neighborhood estimate can be closed; the norms involved ($\ell_1$, $\ell_2$, $\ell_\infty$ and the scaled norms $\|D^{-1}d_x\|$, $\|Dd_s\|$) must be chained in the right order. Theorem 8.23 is of a different kind: its proof passes through the homeomorphism of Theorem 8.19, whose proof the book leaves as an exercise, and a compactness argument along a homotopy.

Two points in the printed text need care. The block matrix (8.24) displayed for $\nabla\psi$ has a spurious transpose in its lower-left block; with the printed matrix Lemma 8.24 would fail for nonsymmetric $\nabla f$, and the statements here use the true Jacobian. The printed proof of Theorem 8.25 (iii) (the scaled Lipschitz constant of $\psi$ from that of $f$) establishes the bound with $v_f(2\alpha/(1-\alpha))$, not the stated $v_f(2\alpha/(1+\alpha))$, and only for $\alpha<1/3$; that part is not in this mission, and Theorem 8.29 assumes the scaled Lipschitz property of $\psi$ directly, as the book does.

Formalization scope

Vectors are Fin N → ℝ, a point $(x;\tau)$ of $\mathbb R^{n+1}$ is z : Fin (n+1) → ℝ with Fin.init z $=x$ and z (Fin.last n) $=\tau$, and every Jacobian is Mathlib's fderiv. The standing assumptions of §8.4 are explicit hypotheses of every theorem: $f$ continuous and monotone on the open orthant $\mathbb R^n_{++}$, and differentiable there wherever $\nabla f$ or $\nabla\psi$ appears (the section assumes this silently). In the scaled Lipschitz condition, "monotone increasing" is read as nondecreasing on $(0,1)$ and $\alpha$ ranges over $(0,1)$. The direction is any solution of (8.42)–(8.43). The new dual iterate is defined by the first line of (8.47); its closed form is a conclusion. The book writes no $O(\cdot)$ in the statements of this mission: $\beta$, $\eta$, $\gamma$ and $\alpha=1$ are the book's explicit constants. $\psi$ is a total function in Lean (division by $\tau=0$ returns $0$), but every statement evaluates it and its derivative only at $\tau>0$.

A trivializing formalization is excluded: the scaled Lipschitz hypothesis is not vacuous (it holds, for instance, for $f\equiv0$ with any admissible $v$), the direction is not assumed to have any property beyond (8.42)–(8.43), and the monotonicity of $\psi$ and the identities (8.41) are proved milestones, not hypotheses of the goal.

Beyond the paper. One variant is posed: central_step_strong (strengthened) drops the continuity and monotonicity of $f$ from Theorem 8.29, because the scaled Lipschitz condition already forces $d^T\nabla\psi(x)d\ge0$, the only use the proof makes of monotonicity.

The development needs Fréchet derivatives of compositions with $x\mapsto x/\tau$, finite-dimensional norm inequalities, and, for Theorem 8.23, invariance of domain or a direct proof of Theorem 8.19. The definitions (monotone maps on the orthant, the scaled Lipschitz condition, the homogeneous map) are reusable for the remaining parts of Theorems 8.25 and 8.26. Contributions of a proof of Theorem 8.19, and of the faithful Theorem 8.25 (iii), are welcome.

Selected references

• Y. Ye, Interior Point Algorithms: Theory and Analysis, Wiley-Interscience, 1997, §8.4. doi:10.1002/9781118032701
• E. D. Andersen and Y. Ye, On a homogeneous algorithm for the monotone complementarity problem, Mathematical Programming 84 (1999), 375–399.
• O. Güler, Existence of interior points and interior paths in nonlinear monotone complementarity problems, Mathematics of Operations Research 18 (1993), 128–147. doi:10.1287/moor.18.1.128
• Y. Ye, M. J. Todd and S. Mizuno, An $O(\sqrt nL)$-iteration homogeneous and self-dual linear programming algorithm, Mathematics of Operations Research 19 (1994), 53–67. doi:10.1287/moor.19.1.53

Why the tail of an interior-point method matters

Primal-dual interior-point methods for linear programming come with two kinds of guarantee. The worst-case one is a bound of $O(\sqrt n\log(R/\epsilon))$ iterations to reduce the duality gap below $\epsilon$. The asymptotic one says what happens to the duality gap near the end of the run, where practical codes spend their final iterations. For the predictor-corrector method of Mizuno, Todd and Ye (1993), Ye, Güler, Tapia and Zhang (1993) showed that the same algorithm that achieves the best known worst-case bound also drives the duality gap to zero quadratically. The proof needs neither nondegeneracy nor convergence of the iterates. Chapter 7 of Yinyu Ye's Interior Point Algorithms: Theory and Analysis (Wiley 1997, DOI 10.1002/9781118032701) gives a self-contained account. This mission formalizes its LP core.

Timeline, as attributed in the chapter's notes (§7.5): Zhang, Tapia and Dennis first obtained superlinear convergence of a primal-dual method assuming the iterates converge, and quadratic convergence assuming nondegeneracy. Quadratic convergence for general LP, with neither assumption, was first established by Ye, Güler, Tapia and Zhang, and independently by Mehrotra and by Tsuchiya. The monotone LCP version (§7.3) is due to Ye and Anstreicher, who also showed that the predictor step cannot converge superlinearly when no strictly complementary solution exists (Proposition 7.13). Monteiro and Wright extended that negative result to Newton-like methods in general.

Setting

Fix a real $m\times n$ matrix $A$ of rank $m$, $b\in\mathbb R^m$ and $c\in\mathbb R^n$. Consider the standard-form pair

$$(\mathrm{LP})\ \min\{c^Tx: Ax=b,\ x\ge0\},\qquad(\mathrm{LD})\ \max\{b^Ty: A^Ty+s=c,\ s\ge0\}.$$

An interior point is a triple $(x,y,s)$ with $Ax=b$, $x>0$, $A^Ty+s=c$, $s>0$. Write $X=\operatorname{diag}(x)$, $S=\operatorname{diag}(s)$, $e$ for the all-ones vector and $\mu=x^Ts/n$. The neighbourhood of the central path is

$$\mathcal N_2(\eta)=\{(x,y,s)\text{ interior}:\ \|Xs-\mu e\|\le\eta\mu\}.$$

The strict complementarity partition $(P,Z)=(P^*,Z^*)$ collects the indices on which some optimal $x^*$ is positive ($P$) and those on which some optimal slack $s^*$ is positive ($Z$). The predictor direction at $(x,s)$ is the solution of

$$Xd_s+Sd_x=-Xs,\qquad Ad_x=0,\qquad -A^Td_y-d_s=0. \tag{7.4}$$

It is the case $\gamma=0$ of the direction $d(x,s,\gamma)$ defined by $Sd_x+Xd_s=\gamma\mu e-Xs$, $Ad_x=0$, $-A^Td_y-d_s=0$. The scaling is $D=X^{1/2}S^{-1/2}$, and $\|v_S\|$ denotes the Euclidean norm of the subvector of $v$ indexed by $S$. Algorithm 4.5 (predictor-corrector, $\eta=1/4$) starts in $\mathcal N_2(1/4)$. At each iteration it takes the largest step $\theta^k$ along $d(x^k,s^k,0)$ that keeps the iterate in $\mathcal N_2(1/2)$, then a full step along $d(\cdot,\cdot,1)$ back towards the central path.

The order of convergence of a sequence $r^k\to0$ (Definition 1.1) is the supremum of the $p\ge0$ with $\limsup_k|r^{k+1}|/|r^k|^p<\infty$. Quadratic convergence (Definition 1.2) means $\limsup_k|r^{k+1}|/|r^k|^2<\infty$.

Formalization targets

Goal: Theorem 7.5

For every $\mu^0>0$ there is a constant $C>0$, depending only on $(A,b,c)$ and $\mu^0$, such that at every $(x,y,s)\in\mathcal N_2(1/4)$ with $\mu\le\mu^0$ the predictor direction satisfies

$$\|(d_x)_P\|\le C\mu\qquad\text{and}\qquad\|(d_s)_Z\|\le C\mu .$$

Milestones

• Lemma 7.2. If $Xd_s+Sd_x=-Xs$ and $d_x^Td_s\ge0$, then $\|D^{-1}d_x\|^2+\|Dd_s\|^2\le x^Ts$.
• Relation (7.6). There is $\xi\in(0,1)$, independent of the point, with $\xi\le x_j\le1/\xi$ on $P$ and $\xi\le s_j\le1/\xi$ on $Z$ throughout $\mathcal N_2(1/4)\cap\{\mu\le\mu^0\}$.
• Lemma 7.3. $\|(d_x)_Z\|\le C\mu$ and $\|(d_s)_P\|\le C\mu$, with $C$ uniform as in the goal.
• Lemma 7.4. $(d_x)_P$ is the unique minimizer of $\tfrac12\|D_P^{-1}u\|^2$ subject to $A_Pu=-A_Z(d_x)_Z$. $d_y$ minimizes $\tfrac12\|D_ZA_Z^Tv\|^2$ subject to $A_P^Tv=-(d_s)_P$, and every minimizer gives $(d_s)_Z=-A_Z^Tv$.
• Proposition 7.1. For positive $r^k\to0$, the order of convergence equals $\liminf_k\log r^{k+1}/\log r^k$.
• Theorem 7.6. For Algorithm 4.5: (i) $(x^k)^Ts^k\le\epsilon$ once $k\ge\frac{1+\sqrt{1+4\sqrt2n}}{2}\log\frac{(x^0)^Ts^0}{\epsilon}$; (ii) $1-\theta^k\le C(x^k)^Ts^k$; (iii) $(x^k)^Ts^k\to0$ quadratically.
• Lemmas 7.9 and 7.10 (monotone LCP linear algebra). For $M=\begin{pmatrix}M_{PP}&M_{PZ}\\M_{ZP}&M_{ZZ}\end{pmatrix}$ with $v^TMv\ge0$: $M_{PP}x_P=0\iff M_{PP}^Tx_P=0$, which implies $(M_{ZP}+M_{PZ}^T)x_P=0$; and $\mathcal R\begin{pmatrix}M_{PP}&M_{PZ}\\0&I\end{pmatrix}=\mathcal R\begin{pmatrix}M_{PP}^T&M_{ZP}^T\\0&-I\end{pmatrix}$.

The goal fixes no value of $C$: it asserts only that one constant serves every point, which is the content the later results use.

Significance

Theorem 7.5, together with Lemma 7.3, says the whole predictor direction is $O(\mu)$. Through the step-size bound of Lemma 4.17 this gives $1-\theta^k=O(\mu^k)$ and hence $\mu^{k+1}=O((\mu^k)^2)$: quadratic convergence of the duality gap (Theorem 7.6). The same least-squares structure yields the LCP version (Theorem 7.12) and the variants of §7.4. Bounds of this kind on the directions near the optimal face also underlie finite termination and basis identification schemes.

On the formal side, no machine-checked development of interior-point asymptotics is known to the authors of this mission. Mathlib has the linear algebra (ranges, block matrices, least squares through orthogonal projection) but no linear-programming duality theory beyond what other missions supply. A formal proof would supply the Goldman–Tucker partition, the uniform bounds (7.6) and a Hoffman-type bound for least-squares solutions in reusable form.

Difficulty

Everything rests on a constant being uniform. For a single interior point, any bound $\|(d_x)_P\|\le C\mu$ holds with some $C$ depending on the point, so the content is entirely in choosing $C$ before the point. The natural first attempt bounds the direction through $\|D\|$ and $\|D^{-1}\|$ on all indices, and this fails: on $P$ the entries $D_j^2=x_j/s_j$ grow like $1/\mu$, and on $Z$ they shrink like $\mu$. Only the split along the optimal partition, with the least-squares characterization of the "large" components and the uniform bounds (7.6), balances the two. Relation (7.6) itself requires the partition to be strict (Goldman–Tucker) and an a priori bound on the iterates. For Theorem 7.6 the algorithm's step-size rule has to be carried as defined: a largest step over an interval of neighbourhood memberships.

Formalization scope

Vectors are Fin n → ℝ and matrices Matrix (Fin m) (Fin n) ℝ. All norms are Euclidean. $P^*$ and $Z^*$ are defined as unions of supports of optimal solutions; that they partition the indices is a consequence solvers must prove, not an assumption. The standing assumption $\operatorname{rank}A=m$ appears as a hypothesis.

Instantiations of the book's $O(\cdot)$ (p. 213: "may depend on $n$ and/or the original problem data, but … independent of the iteration $k$"):

• Theorem 7.5, Lemma 7.3: $\exists C>0$ quantified before the point; $C$ depends on $(A,b,c)$ and on a bound $\mu^0$ for $\mu$.
• Relation (7.6): $\exists\xi\in(0,1)$ quantified before the point, depending on $(A,b,c)$ and $\mu^0$. The book states it for the iterates; here it covers every point of $\mathcal N_2(1/4)$ with $\mu\le\mu^0$.
• Theorem 7.6(i): the constant of Theorem 4.18's proof, threshold $\frac{1+\sqrt{1+4\sqrt2n}}{2}\log((x^0)^Ts^0/\epsilon)$, with $R=(x^0)^Ts^0$. (ii): $\exists C>0$ before $k$. (iii): Definition 1.2.

A constant chosen after the point would make the goal trivially true; the statements quantify $\exists C$ first to rule this out. Algorithm 4.5 is run for every $k$ (no termination test), and its step is the greatest admissible $\theta$, not a supremum. The order of convergence and all limits superior take values in EReal, so infinite values are not collapsed to junk reals. Lemma 7.4's second problem is stated as corrected (the printed objective $\tfrac12\|D_Zv\|^2$ is ill-typed and the sign of $(d_s)_Z=A_Z^Tv$ is inconsistent with (7.4)); see the findings.

Beyond the paper. One strengthened variant: Theorem 7.5 on $\mathcal N_2(\eta)$ for every $\eta\in(0,1)$ and without the rank condition. The book's proof uses the neighbourhood only through $(1-\eta)\mu\le x_js_j\le(1+\eta)\mu$, and the rank of $A$ enters nowhere.

Needed infrastructure: LP duality and strict complementarity (Goldman–Tucker), a Hoffman-type bound for minimum-norm solutions, and weighted least squares. The definitions of the neighbourhood, the direction $d(x,s,\gamma)$ and Algorithm 4.5 are shared with the chapter 4 analysis and are reusable for other interior-point results. Contributions proving any milestone independently are welcome.

Selected references

• Y. Ye, Interior Point Algorithms: Theory and Analysis, Wiley-Interscience, 1997. https://doi.org/10.1002/9781118032701
• S. Mizuno, M. J. Todd, Y. Ye, On adaptive-step primal-dual interior-point algorithms for linear programming, Mathematics of Operations Research 18 (1993) 964–981. https://doi.org/10.1287/moor.18.4.964
• Y. Ye, O. Güler, R. A. Tapia, Y. Zhang, A quadratically convergent $O(\sqrt n L)$-iteration algorithm for linear programming, Mathematical Programming 59 (1993) 151–162. https://doi.org/10.1007/BF01582144
• A. J. Goldman, A. W. Tucker, Theory of linear programming, in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, Princeton, 1956. https://doi.org/10.1515/9781400881987-005
• A. J. Hoffman, On approximate solutions of systems of linear inequalities, Journal of Research of the National Bureau of Standards 49 (1952) 263–265. https://doi.org/10.6028/jres.049.027

Motivation

Worst-case analysis of interior-point methods gives iteration bounds of order $\sqrt n\,L$ or $\sqrt n\log(1/\epsilon)$, while practical codes finish in a number of iterations that barely grows with the problem size. Chapter 6 of Yinyu Ye's Interior Point Algorithms: Theory and Analysis (Wiley 1997, doi:10.1002/9781118032701) addresses the gap probabilistically. Its rigorous half (§6.2) takes the simplest nontrivial problem, the homogeneous linear feasibility problem with a random Gaussian matrix, and shows that it is solved in $O(\sqrt n\log n)$ iterations with high probability, then extends this to random linear programs through the homogeneous self-dual model.

That analysis rests on a geometric fact about random cones: the probability that $n$ random vectors lie in a common open half-space through the origin. The answer is Wendel's formula (J. G. Wendel, A problem in geometric probability, Math. Scand. 11 (1962), 109–111); Ye restates it as Corollaries 6.11–6.12 and draws from it Theorem 6.13: with probability one a random homogeneous system is strictly feasible on exactly one side of its theorem of the alternative. Strict feasibility is what makes the condition number of the problem finite, which is what an interior-point termination procedure needs.

Setting

Let $A$ be a real $m\times n$ matrix with columns $a_1,\dots,a_n$; vector inequalities are componentwise and $e$ is the all-ones vector. The homogeneous system (6.5) is

$$\mathcal X=\{x\in\mathbb R^n:\ Ax=0,\ x\ge0,\ x\ne0\},$$

and its alternative (6.11) is the system $s=A^Ty\ge0$, $s\ne0$ in $y\in\mathbb R^m$. An interior feasible point of (6.5) is an $x$ with $Ax=0$ and $x>0$; of (6.11), a $y$ with $A^Ty>0$.

In the standard Gaussian model (§6.2.2) the $mn$ entries of $A$ are independent $N(0,1)$ random variables. With $d=n-m$ the book defines

$$p_{nd}=\frac{\binom{n-1}{0}+\cdots+\binom{n-1}{d-1}}{2^{n-1}},$$

and $p_{nm}$ is the same sum with $d$ replaced by $m$.

A partition $A=(A_B,A_N)$ chooses $m$ columns for the $m\times m$ matrix $A_B$ and leaves the other $n-m$ in $A_N$. System (6.12) asks for $x=(x_B,x_{m+1})\in\mathbb R^{m+1}$ with

$$A_Bx_B+(A_Ne)\,x_{m+1}=0,\qquad x\ne0,\qquad x\ge0.$$

For the one-step analysis of §6.1, $F=[g,H]$ is an orthogonal $n\times n$ matrix with first column $g$, and $v$ is uniformly distributed on the unit sphere of $\mathbb R^{n-1}$.

The Lean development lives in the namespace YeIPA.Random: the module YeIPA.Random.Setting defines IsFeasible65, IsInterior65, IsFeasible611, IsInterior611, IsFeasible612, gaussianMatrix, pnd and uniformSphere.

Formalization targets

Goal: Theorem 6.13

For $1\le n$, $m\le n$ and standard Gaussian $A$,

$$\Pr\Big[\big(\mathcal X=\emptyset\ \wedge\ \exists y:\ A^Ty>0\big)\ \vee\ \big(\text{(6.11) infeasible}\ \wedge\ \exists x>0:\ Ax=0\big)\Big]=1 .$$

Milestones

1. Lemma 6.14 (p. 194): for $A$ of full row rank, (6.5) is feasible if and only if some partition $A=(A_B,A_N)$ makes (6.12) feasible.
2. Corollary 6.11 (p. 193): $\Pr[\mathcal X\ne\emptyset]=p_{nd}$.
3. Corollary 6.12 (p. 193): $\Pr[\exists x>0:\ Ax=0]=p_{nd}$.
4. Lemma 6.5 (p. 185): for every sequence of orthogonal $F=[g,H]$,

$$\Pr\Big(\|Hv\|_\infty\le\sqrt{3\log n/n}\Big)\to1\qquad(n\to\infty).$$

Significance

Theorem 6.13 is the input to the chapter's main results: Theorem 6.15 (a feasible point of a random system satisfies the scaling condition (6.9) with high probability) and the $O(\sqrt n\log n)$ iteration bounds of Theorems 6.16 and 6.23 for random feasibility and random LP problems. It turns a deterministic theorem of the alternative, which allows degenerate configurations, into a statement that such configurations have probability zero. Corollaries 6.11–6.12 are Wendel's formula in the form used for linear programming, and also give the exact probability that a random homogeneous system is feasible, a quantity that recurs in the analysis of random linear programs and of perceptron capacity. Lemma 6.5 is the concentration estimate behind the one-step analysis of predictor steps in §6.1.

None of these results is formalized on Prove2Me or, as far as a search shows, in Mathlib. Wendel's formula has no machine-checked proof that this mission could reference; the platform's PoissonDirichlet.Wendel.* items concern an unrelated identity. A complete development adds Gaussian random matrices, conic theorems of the alternative and an exact geometric probability to the platform.

Difficulty

The book cites Wendel's formula ("It is shown that …") and leaves its proof as Exercise 6.3, so Corollaries 6.11–6.12 must be proved from scratch. The natural first idea, conditioning on the column space or on a single column and integrating, does not close: the count of half-spaces is combinatorial, not an integral that evaluates in closed form. The probability-one statements need general position of Gaussian columns, which is the property that rules out the degenerate cases of the theorem of the alternative. Corollary 6.12 is not a consequence of Corollary 6.11 alone: the gap between "feasible" and "strictly feasible" is an event that must be shown to be null, and the book's own argument passes through the dual system and the identity $p_{nd}+p_{nm}=1$ for $m+d=n$, which is itself part of what must be proved. Lemma 6.5 is a uniform statement over all orthogonal completions $H$ of $g$, with an explicit threshold $\sqrt{3\log n/n}$ rather than an unspecified constant.

Formalization scope

Vectors are functions on Fin n (indices $0,\dots,n-1$), matrices are Matrix (Fin m) (Fin n) ℝ, and the Gaussian model is the product measure Measure.pi of gaussianReal 0 1 over the entries, a sample being read as Matrix.of A. Probabilities are values of this measure in $[0,\infty]$, compared with $p_{nd}$ through ENNReal.ofReal. "With probability one" in Theorem 6.13 is an almost-everywhere statement for that explicit measure; the failure set is null. The section's standing assumption that $A$ has full row rank (p. 187) is carried as $m\le n$ in the probabilistic statements, under which a Gaussian $A$ has rank $m$ almost surely, and as $\operatorname{rank}A=m$ in Lemma 6.14. Every probabilistic statement assumes $n\ge1$; for $n=0$ both systems are empty and $p_{nd}$ is undefined. In Lemma 6.14 a partition is an injection $\sigma$ from $\{1,\dots,m\}$ into the columns; the variable $x_{m+1}$ is the last coordinate of a vector on Fin (m+1). In Lemma 6.5 the sequence is indexed by $k=n-1$, the matrices $F_k$ are arbitrary with $F_k^TF_k=I$, $H_k$ deletes the first column, the uniform law is Lebesgue surface measure on the sphere normalized to mass one, $\log$ is natural, and $\|Hv\|_\infty\le t$ is written coordinatewise. No result of this chapter uses an $O(\cdot)$ bound in the stated items, so there are no constants to instantiate; Lemma 6.5's threshold $\sqrt{3\log n/n}$ is the book's own.

A trivializing formalization is ruled out: the probabilities are those of the explicit product Gaussian measure (not an arbitrary measure, nor "for almost every $A$" against an unspecified measure), interior points are required to be strictly positive in every coordinate, and Theorem 6.13 asserts both the emptiness of one system and an interior point of the other.

Beyond the paper. One variant is posed. YeIPA.Random.lemma_6_14_corrected (corrected, finding F1) adds $m<n$ to Lemma 6.14: as printed the lemma fails for $n=m$, where $A_N$ is empty and $x=(0,\dots,0,1)$ solves (6.12) for every $A$, e.g. $A=(1)$. The faithful Lemma 6.14 stays the milestone.

Infrastructure that a complete development needs and that is reusable beyond this mission: general position of Gaussian matrices (every $m\times m$ minor nonzero almost surely), Gordan's theorem of the alternative for $Ax=0,\ x\ge0,\ x\ne0$, Wendel's formula, and tail bounds for coordinates of a uniform point on the sphere. Proofs of any milestone, and of these supporting facts as separate lemmas, are welcome.

Selected references

• Yinyu Ye, Interior Point Algorithms: Theory and Analysis, Wiley-Interscience, 1997, Chapter 6. doi:10.1002/9781118032701
• J. G. Wendel, A problem in geometric probability, Mathematica Scandinavica 11 (1962), 109–111.
• S. I. Resnick, Extreme Values, Regular Variation, and Point Processes, Springer, 1987, pp. 42 and 71 (cited in the proof of Lemma 6.5).

Motivation

Karmarkar's 1984 algorithm solved linear programs in polynomial time by reducing a logarithmic potential function by a constant at every step (doi:10.1007/BF02579150). Its successors replaced Karmarkar's projective transformations with a primal-dual potential that measures the duality gap and the distance from the central path together. Tanabe, and Todd and Ye (1990, doi:10.1287/moor.15.3.508), introduced this potential. Ye (1991) and Kojima, Mizuno and Yoshise (1991) showed that one fixed reduction per step, for the parameter $\rho=\sqrt n$, gives the best known iteration bound $O(\sqrt n\log(1/\epsilon))$. The potential-reduction method needs no step that stays close to the central path. It became one of the standard interior-point methods, and its analysis was later carried over to semidefinite and conic programming.

Chapter 4 of Yinyu Ye's Interior Point Algorithms: Theory and Analysis (Wiley, 1997, doi:10.1002/9781118032701) proves this one-step estimate for two algorithms. The first is the primal-dual potential-reduction algorithm (§4.3), which alternates a primal projected-gradient step with an update of the dual lower bound. The second is the symmetric primal-dual algorithm (§4.4), which moves along the Newton direction toward a point of the central path. This mission formalizes both estimates and the lemmas they rest on.

Setting

Let $A$ be a real $m\times n$ matrix of rank $m$, $b\in\mathbb R^m$ with $b\ne0$, $c\in\mathbb R^n$, $n\ge1$. The standard-form pair is

$$(\mathrm{LP})\ \min\{c^Tx: Ax=b,\ x\ge0\},\qquad(\mathrm{LD})\ \max\{b^Ty: A^Ty+s=c,\ s\ge0\},$$

and both are assumed to have interior feasible points. Vector inequalities are componentwise, $e$ is the all-ones vector, $X=\operatorname{diag}(x)$, $S=\operatorname{diag}(s)$, $\|\cdot\|$ is the Euclidean norm and $\min(v)=\min_jv_j$. The interior $\mathring{\mathcal F}$ consists of the triples $(x,y,s)$ with $Ax=b$, $x>0$, $A^Ty+s=c$, $s>0$. For $\rho\ge0$, the primal-dual potential and the primal potential with lower bound $z$ are

$$\psi_{n+\rho}(x,s)=(n+\rho)\log(x^Ts)-\sum_{j=1}^n\log(x_js_j),\qquad\mathcal P_{n+\rho}(x,z)=(n+\rho)\log(c^Tx-z)-\sum_{j=1}^n\log x_j.$$

The potential-reduction step (§4.3, $\rho=\sqrt n$). At $(x^k,y^k,s^k)\in\mathring{\mathcal F}$ with $z^k=b^Ty^k$, let

$$p^k=p(z^k)=(I-X^kA^T(A(X^k)^2A^T)^{-1}AX^k)\,X^k\Big(\frac{n+\rho}{c^Tx^k-z^k}c-(X^k)^{-1}e\Big),\qquad x^{k+1}=x^k-\alpha\frac{X^kp^k}{\|p^k\|}.$$

The dual update is $s(z^k)=c-A^Ty(z^k)$ with $y(z^k)=y_2-\frac{c^Tx^k-z^k}{n+\rho}y_1$, $y_1=(A(X^k)^2A^T)^{-1}b$ and $y_2=(A(X^k)^2A^T)^{-1}A(X^k)^2c$.

The symmetric step (§4.4). With $\mu=x^Ts/n$ and $\gamma=n/(n+\rho)$, the direction $(d_x,d_y,d_s)$ solves $Sd_x+Xd_s=\gamma\mu e-Xs$, $Ad_x=0$, $-A^Td_y-d_s=0$. The step size is $\theta=\alpha\sqrt{\min(Xs)}/\|(XS)^{-1/2}(\frac{x^Ts}{n+\rho}e-Xs)\|$ for a constant $0<\alpha<1$.

Formalization targets

Goal: Theorem 4.9

There is a constant $\delta>1/20$ such that for every such LP and every $(x^k,y^k,s^k)\in\mathring{\mathcal F}$, with $\rho=\sqrt n$, $\alpha=0.3$ and $s^{k+1}=s(z^k)$,

$$\psi_{n+\rho}(x^{k+1},s^k)\le\psi_{n+\rho}(x^k,s^k)-\delta\qquad\text{or}\qquad\psi_{n+\rho}(x^k,s^{k+1})\le\psi_{n+\rho}(x^k,s^k)-\delta.$$

Milestones

• Lemma 3.1: for $\|d\|_\infty<1$, $e^Td\ge\sum_i\log(1+d_i)\ge e^Td-\|d\|^2/(2(1-\|d\|_\infty))$.
• The display after (4.10): for $0<\alpha<1$, $\mathcal P_{n+\rho}(x^{k+1},z^k)-\mathcal P_{n+\rho}(x^k,z^k)\le-\alpha\|p^k\|+\alpha^2/(2(1-\alpha))$.
• Lemma 4.8: with $\mu^k=(x^k)^Ts^k/n$ and $\mu=(x^k)^Ts(z^k)/n$, if $\|p(z^k)\|<\min(\eta\sqrt{n/(n+\eta^2)},1-\eta)$ then $s(z^k)>0$, $\|X^ks(z^k)-\mu e\|<\eta\mu$ and $\mu<(1-.5\eta/\sqrt n)\mu^k$.
• Lemma 4.11: the symmetric step stays in $\mathring{\mathcal F}$ and

$$\psi_{n+\rho}(x^+,s^+)-\psi_{n+\rho}(x,s)\le-\alpha\sqrt{\min(Xs)}\Big\|(XS)^{-1/2}\Big(e-\frac{n+\rho}{x^Ts}Xs\Big)\Big\|+\frac{\alpha^2}{2(1-\alpha)}.$$

• Lemma 4.12: for $v>0$ and $\rho\ge\sqrt n$, $\sqrt{\min(v)}\,\|V^{-1/2}(e-\frac{n+\rho}{e^Tv}v)\|\ge\sqrt{3/4}$.

Significance

Theorem 4.9 says that the potential can be lowered by a fixed amount no matter where the iterate is. Either the primal step makes progress, or the dual update produces a feasible, nearly central dual point with a smaller gap. Since $\psi_{n+\sqrt n}(x,s)\ge\sqrt n\log(x^Ts)+n\log n$, a constant decrease per step yields the $O(\sqrt n\log((x^0)^Ts^0/\epsilon))$ bound of Corollary 4.10 without any neighborhood of the central path. Lemmas 4.11 and 4.12 give the same conclusion for the symmetric algorithm, with decrease $\alpha\sqrt{3/4}-\alpha^2/(2(1-\alpha))$. These are the per-step facts behind practical potential-reduction codes and their conic extensions.

The platform has no statement of these results. LinearOptimization.interior_point_potential_reduction (proved) turns a constant decrease of a different potential into an iteration count. The Mizuno–Todd–Ye bounds on the second-order term of the Newton step, which are Ye's Lemmas 4.14, 4.15 and 4.19, are already formalized as AdaptiveStepIPM.PredCorr.lemma_1a, AdaptiveStepIPM.WideNbhd.lemma_1b, lemma_1c and lemma_2c. They belong to the path-following part of the chapter and are not repeated here. Formalizing Theorem 4.9 checks the case split and its numerical constants, and produces a reusable layer: the weighted projection $I-XA^T(AX^2A^T)^{-1}AX$, the dual estimates $y(z)$, $s(z)$, and the potential identities.

Difficulty

The case split is driven by $\|p(z^k)\|$, which is defined through a projection, but Lemma 4.8 reasons about it through the identity $p(z^k)=\frac{n+\rho}{c^Tx^k-z^k}X^ks(z^k)-e$ (4.11). The book states that identity without proof. It needs the normal equations for $y_1$, $y_2$, and so the invertibility of $AX^2A^T$. The primal case needs $x^{k+1}>0$ and $c^Tx^{k+1}-z^k>0$ before any logarithm is evaluated. It also needs the first-order term $\nabla\mathcal P^Td_x$ to equal $-\alpha\|p^k\|$ exactly, which uses that $p^k$ is an orthogonal projection. The dual case combines Lemma 3.1, applied to $X^ks^{k+1}/\mu-e$, with the arithmetic–geometric mean inequality and the bound $\sqrt n\log(1-.5\eta/\sqrt n)\le-\eta/2$. The constant must be checked for every $n\ge1$: with $\eta=.43$ and $\alpha=.3$ the two decreases are about $.054$ and $.053$, so the margin over $1/20$ is small. Lemma 4.11's proof is omitted in the book. Unlike its Chapter 3 analogue it needs no normalization $x^Ts=n$, but the exact cancellation of its first-order term has to be verified. Lemma 4.12 is left as an exercise.

Formalization scope

Vectors are Fin n → ℝ and matrices Matrix (Fin m) (Fin n) ℝ; indices are $0$-based. The Euclidean norm is written out as norm2. The rank of $A$, the existence of interior points (p. 63) and $b\ne0$ (Chapter 4 preamble, p. 109) are bundled as StandingAssumptions A b c and are a hypothesis of every theorem, together with $n\ge1$. The vector $p(z)$ is defined by its projection formula, not by (4.11), so (4.11) is something to prove. Matrix inverses are Mathlib's ⁻¹, which is $0$ on singular matrices and never reached under the rank assumption.

Explicit constants: Theorem 4.9 does not fix the step length $\alpha$, and the proof chooses $\alpha=.3$ (with $\eta=.43$ in the case split). The goal is stated for the step (4.10) with $\alpha=.3$. Its $\delta$ is quantified before $m$, $n$, $A$, $b$, $c$ and the iterate, so one number $\delta>1/20$ serves every instance. A formalization in which $\delta$ depends on the instance, or in which the step is any point that happens to lower the potential, would be trivial; both are ruled out by stating the theorem for the book's step (4.10) and dual update (4.12)–(4.13) with a uniform $\delta$. No result in this mission uses $O(\cdot)$.

Beyond the paper. One variant is posed: a strengthened Theorem 4.9 for every $\rho\ge\sqrt n$ with the same $\delta$ (finding F1). The proof uses $\rho=\sqrt n$ only through $(n+\rho)/n\ge1+1/\sqrt n$ and $\rho\log(1-.5\eta/\sqrt n)\le-\eta/2$, and both hold for $\rho\ge\sqrt n$.

Not in scope: the iteration-count statements (Theorems 4.4, 4.7, 4.13, 4.20, Corollary 4.10), which the book gives with $O(\cdot)$; Karmarkar's algorithm and the path-following analysis of §§4.1–4.2 (Proposition 4.2, Lemmas 4.5–4.6), which need the max-potential of the dual level set; and the predictor-corrector Lemmas 4.16–4.17 and Theorem 4.18, which are statements about an algorithm's sequence.

Selected references

• Y. Ye, Interior Point Algorithms: Theory and Analysis, Wiley-Interscience, 1997, Chapter 4. doi:10.1002/9781118032701
• N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4 (1984) 373–395. doi:10.1007/BF02579150
• M. J. Todd and Y. Ye, A centered projective algorithm for linear programming, Mathematics of Operations Research 15 (1990) 508–529. doi:10.1287/moor.15.3.508
• Y. Ye, An O(n³L) potential reduction algorithm for linear programming, Mathematical Programming 50 (1991) 239–258.
• M. Kojima, S. Mizuno and A. Yoshise, An O(√n L) iteration potential reduction algorithm for linear complementarity problems, Mathematical Programming 50 (1991) 331–342.