Discover · Prove2Me

Completed

Constructing algebraic Lie algebrasResearch Paper

Motivation

We give an algorithm for constructing the algebraic hull of a given matrix Lie algebra in characteristic zero. It is based on an algorithm for finding integral linear dependencies of the roots of a polynomial, that is probably of independent interest.

This mission is the statement-level formalization of Constructing algebraic Lie algebras (arXiv:math/0611414v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Trivial permutation component and power traces (Lemma 5: trivial permutation component and trace, 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

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

Abstract / §§2–3: construction of the algebraic hull: Algebraic subgroups of GL(n) over arbitrary characteristic-zero F, their tangent Lie subalgebras, and the intrinsic algebraic hull; effective exact number-field computations and a terminating executable construction (hard)
§2: algebraicity criterion using a basis: Algebraic subgroups of GL(n) over arbitrary characteristic-zero F, their tangent Lie subalgebras, and the intrinsic algebraic hull (hard)
Lemma 2: coefficient-space description of a semisimple hull: Algebraic subgroups of GL(n) over arbitrary characteristic-zero F, their tangent Lie subalgebras, and the intrinsic algebraic hull (hard)
Algorithm 3: exact splitting-field hull construction: Algebraic subgroups of GL(n) over arbitrary characteristic-zero F, their tangent Lie subalgebras, and the intrinsic algebraic hull; effective exact number-field computations and a terminating executable construction (hard)
Example 4: even quartic minimal polynomial: Algebraic subgroups of GL(n) over arbitrary characteristic-zero F, their tangent Lie subalgebras, and the intrinsic algebraic hull (hard)
Lemma 6: irreducible augmentation component: A valid scope for the irreducible augmentation lemma when the characteristic polynomial is reducible and n=2 (source-ambiguity)
Corollary 7: 2-transitive or prime-degree hull: Algebraic subgroups of GL(n) over arbitrary characteristic-zero F, their tangent Lie subalgebras, and the intrinsic algebraic hull (hard)
Proposition 8: all four non-S4/non-A4 quartic cases: Algebraic subgroups of GL(n) over arbitrary characteristic-zero F, their tangent Lie subalgebras, and the intrinsic algebraic hull (hard)
Proposition 9: sextic Magma-group formula: Proposition 9: sextic Magma-group formula with corrected source precision, scope or output contract (source-ambiguity)
§6: the two integral-dependency tasks: §6: the two integral-dependency tasks with corrected source precision, scope or output contract (source-ambiguity)
Algorithm 10: certified zero test: Algorithm 10: certified zero test with corrected source precision, scope or output contract (source-ambiguity)
Theorem 11: small integral relation basis: Theorem 11: small integral relation basis with corrected source precision, scope or output contract (source-ambiguity)
Algorithm 13: LLL relation-lattice algorithm: Algorithm 13: LLL relation-lattice algorithm with corrected source precision, scope or output contract (source-ambiguity)
§6: reduced-precision retry variant of Algorithm 13: §6: reduced-precision retry variant of Algorithm 13 with corrected source precision, scope or output contract (source-ambiguity)
Algorithm 14: Galois-assisted relation reconstruction: Algorithm 14: Galois-assisted relation reconstruction with corrected source precision, scope or output contract (source-ambiguity)
§6: extension to relations over number-field orders: §6: extension to relations over number-field orders with corrected source precision, scope or output contract (source-ambiguity)
§6 Remark: component-testing algorithm: §6 Remark: component-testing algorithm with corrected source precision, scope or output contract (source-ambiguity)
§7: hull construction avoiding exact splitting fields: §7: hull construction avoiding exact splitting fields with corrected source precision, scope or output contract (source-ambiguity)

Selected references

Constructing algebraic Lie algebras, arXiv:math/0611414v1, https://arxiv.org/abs/math/0611414v1

4 thms2 active usersReviewed

Quantum Information·Captain: Goku

Quantum communication using a bounded-size quantum reference frameResearch Paper

Motivation

Typical quantum communication schemes are such that to achieve perfect decoding the receiver must share a reference frame with the sender. Indeed, if the receiver only possesses a bounded-size quantum token of the sender's reference frame, then the decoding is imperfect, and we can describe this effect as a noisy quantum channel. We seek here to characterize the performance of such schemes, or equivalently, to determine the effective decoherence induced by having a bounded-size reference frame. We assume that the token is prepared in a special state that has particularly nice group-theoretic properties and that is near-optimal for transmitting information about the sender's frame. We present a decoding operation, which can be proven to be near-optimal in this case, and we demonstrate that there are two distinct ways of implementing it (corresponding to two distinct Kraus decompositions). In one, the receiver measures the orientation of the reference frame token and reorients the system appropriately. In the other, the receiver extracts the encoded information from the virtual subsystems that describe the relational degrees of freedom of the system and token. Finally, we provide explicit characterizations of these decoding schemes when the system is a single qubit and for three standard kinds of reference frame: a phase reference, a Cartesian frame (representing an orthogonal triad of spatial directions), and a reference direction (representing a single spatial direction).

This mission is the statement-level formalization of Quantum communication using a bounded-size quantum reference frame (arXiv:0812.5040v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

18 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Canonical-token effective channel (Paper result: canonical-token effective channel, Eqs.(1)–(3), (38)–(40), 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.

Deferred results

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

§V.B, Eqs.(73)–(92), continuing PDF p.14: The based joint multiplicity decomposition and explicit reciprocal Cartesian A_J of Eqs.(75),(79),(81),(84),(87), tied to the actual symmetric-tensor spin representation and paired canonical memory. (hard)
§III, sentence following the no-prior-information claim: A source-supported average-input restriction compatible with the fixed recovery D_R E†. (source-ambiguity)
§III.D continuation, first column: A purification or a changed encoding that could make the whole successful composite pure. (source-ambiguity)

Selected references

Quantum communication using a bounded-size quantum reference frame, arXiv:0812.5040v2, https://arxiv.org/abs/0812.5040v2

25 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

A non-smooth continuous unitary representation of a Banach-Lie groupResearch Paper

Motivation

In this note we show that the representation of the additive group of the Hilbert space $L^2([0,1],\R)$ on $L^2([0,1],\C)$ given by the multiplication operators $\pi(f) := e^{if}$ is continuous but its space of smooth vectors is trivial. This example shows that a continuous unitary representation of an infinite dimensional Lie group need not be smooth.

This mission is the statement-level formalization of A non-smooth continuous unitary representation of a Banach-Lie group (arXiv:0811.4234v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The phase representation is continuous and has only the zero smooth vector (Theorem 2.3, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Selected references

A non-smooth continuous unitary representation of a Banach-Lie group, arXiv:0811.4234v1, https://arxiv.org/abs/0811.4234v1

4 thms2 active usersReviewed

Quantum Information·Captain: Goku

Towards a Lie theory for locally convex groupsResearch Paper

Motivation

In this survey, we report on the state of the art of some of the fundamental problems in the Lie theory of Lie groups modeled on locally convex spaces, such as integrability of Lie algebras, integrability of Lie subalgebras to Lie subgroups, and integrability of Lie algebra extensions to Lie group extensions. We further describe how regularity or local exponentiality of a Lie group can be used to obtain quite satisfying answers to some of the fundamental problems. These results are illustrated by specialization to some specific classes of Lie groups, such as direct limit groups, linear Lie groups, groups of smooth maps and groups of diffeomorphisms.

This mission is the statement-level formalization of Towards a Lie theory for locally convex groups (arXiv:1501.06269v1). 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 Fundamental results of locally convex differential calculus (Proposition I.2.3, PDF p. 12). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

Proposition I.4.3: Graded differential forms on the actual curve tangent bundle; exterior derivative, contraction, and Lie derivative constructed from I.4.1–2, with the degree-zero contraction convention. (hard)
Theorem II.2.1: A type of Hausdorff Bastiani Lie structures on a fixed abstract group, with equality of smooth structures rather than equality of chosen chart presentations; local group multiplication on U before any global topology exists. (hard)
Corollary II.2.2: The actual locally defined product and injective local homomorphism; Lie structures on the subgroup generated by its image, with the entire image open and the source manifold structure preserved. (hard)
Corollary II.2.3: Lie structures extending the supplied normal-subgroup structure as an open subgroup; smooth conjugation automorphisms defined independently on that subgroup. (hard)
Corollary II.2.4: A topology-compatible Bastiani Lie structure transported along a covering homomorphism, with local smooth inverses and uniqueness on the receiving group. (hard)
Theorem II.2.8: Finite-order mapping spaces on compact manifolds with boundary; compact-open C^r topology and the locally convex direct-limit topology on compact-support maps; tangent Lie algebra identification with pointwise bracket. (hard)
Lemma II.3.3: Diffeomorphisms of a general locally convex manifold; joint smooth evaluation and inverse evaluation; left logarithmic derivative from the actual tangent map, and Ad as pushforward. (hard)
Lemma II.3.5: The same independently constructed diffeomorphism-valued differential as II.3.3, so equality of logarithmic derivatives is not a freely supplied relation; connectedness and the conditional common-value uniqueness conclusion. (hard)
Lemma II.3.10: Smooth diffeomorphism-valued evolution on arbitrary real intervals, its actual right logarithmic derivative and curve tangents, including the endpoint derivative convention; no general locally convex ODE uniqueness assumption. (hard)
Proposition II.4.1: The actual tangent-at-identity Lie functor, left Maurer–Cartan form and pullback logarithmic derivative; all three clauses, including connected uniqueness and the homomorphism criterion. (hard)
Corollary II.4.2: Ad(g) computed by differentiating conjugation at the identity; a freely chosen representation cannot encode the asserted equality with the group center. (hard)
Proposition II.4.3: The tangent-at-identity Lie algebra with bracket obtained from left invariant vector fields, rather than an unrelated Lie algebra parameter attached to a connected group. (hard)
Theorem II.4.4: The computed tangent Lie algebra and its lower central and derived series; both nilpotence and solvability must be compared with the corresponding group series. (hard)
Proposition II.5.6: Smooth curves on the closed interval with their compact-open C-infinity locally convex topology; regularity defined by the actual endpoint evolution map, including smooth dependence, and Mackey completeness by existence of antiderivatives. (hard)
Proposition II.5.7: An exponential supplied as a smooth one-parameter-group evolution; delta(exp) computed by inverse left translation of its differential and Ad by differentiated conjugation; represented pointwise weak integral with the minus sign. (hard)
Proposition II.5.11: The independent exponential, adjoint flow and kappa operator; fibers and isolated points, all C1 curves in the restricted kernel, and finite-dimensional discreteness; all five clauses including the conditional reverse centrality implication. (hard)
Lemma II.6.2: Initial Lie subgroup structures with injective differential and the universal finite-C^k lifting property for every source manifold; uniqueness of the induced intrinsic smooth structure. (hard)
Proposition II.6.3: The set of actual right derivatives of based C1 arcs [0,1] into H, defined before proving bracket closure; compatibility with the image of the actual initial inclusion differential. (hard)
Theorem III.1.2: Lie-algebra-valued forms, Maurer–Cartan equation, actual local primitives and their gluing; based piecewise smooth loop classes and the normalized lift gamma(0)=1 determining the period homomorphism. (hard)
Corollary III.1.6: Regularity as smooth endpoint evolution and a smooth Lie group isomorphism whose differential is the given topological Lie algebra isomorphism; 1-connectedness includes connectedness. (hard)
Corollary III.1.7: Closed topological Lie ideals and the quotient topology; actual adjoint invariance and integration of a quotient to a regular Bastiani Lie group. (hard)
Theorem III.4.1: Unresolved printed source statement: Theorem III.4.1 (source-ambiguity)
Proposition IV.1.2: The actual smooth exponential of a general Banach Lie group and a local diffeomorphism in its given manifold structure; an arbitrary function called exponential would be circular. (hard)
Theorem IV.1.8: Locally convex analyticity via complexification and continuous homogeneous polynomials, actual local exponential charts with analytic inverse, and Dynkin BCH convergence; smooth inverse alone is insufficient. (hard)
Corollary IV.1.10: A topology-compatible analytic Lie structure and analytic exponential chart for arbitrary Banach Lie groups, using the actual BCH criterion rather than a Boolean label. (hard)
Theorem IV.1.11: Continuous inverse algebras without imposed normability; unit-group analytic charts, actual exponential, Mackey completeness, and smooth evolution regularity with sequential completeness only in the second clause. (hard)
Theorem IV.1.12: Compactly supported gauge transformations of the actual principal bundle, support on the base, equivariant adjoint-bundle sections and their LF topology; local exponentiality, regularity and BCH inheritance. (hard)
Lemma IV.1.17: The actual tangent Lie bracket and group exponential, local exponential charts, and convergence in the given group topology of the positive-index Trotter and four-factor commutator sequences. (hard)
Theorem IV.1.18: Both the smooth locally exponential category and the analytic BCH category over possibly nonnormable model spaces; actual maps retain their prescribed continuous homomorphism. (hard)
Theorem IV.1.19: Lie group morphisms and their computed differential, smooth target exponential without regularity, and the locally exponential 1-connected source; uniqueness is for the supplied algebra morphism. (hard)
Corollary IV.1.20: Actual locally exponential group structures and tangent Lie algebra isomorphisms; a smooth group isomorphism, not merely an abstract group equivalence. (hard)
Theorem IV.1.24: The compact-open space Hom_c(R,G), with scalar rescaling and operations defined by the specified Trotter/commutator limits; all Lie and continuity laws without a manifold assumption. (hard)
Lemma IV.2.2: Local Lie products on convex balanced open subsets of the tangent algebra with guarded domains, radial one-parameter groups, and second derivative equal to the given bracket. (hard)
Theorem IV.2.6: Polynomial nilpotent BCH multiplication, actual exponential as a covering Lie morphism, the discrete central kernel and its fundamental-group identification, plus regularity and local exponentiality. (hard)
Proposition IV.2.7: The actual polynomial BCH group on the computed tangent Lie algebra, with no completeness hypothesis; a smooth group isomorphism for the 1-connected exponential nilpotent source. (hard)
Theorem IV.2.8: Formal homogeneous Dynkin BCH polynomials and Taylor coefficients of the independently specified local product; no unsupported assertion of convergence in a non-BCH algebra. (hard)
Theorem IV.2.9: Topological Lie quotient and local products; integrable adjoint flows and pointwise represented kappa; stability for every x and neighborhood equality kappa(x)n=n, plus the kernel factorization consequence. (hard)
Lemma IV.3.1: The differential tangent set from actual C1 arcs and the exponential tangent set from all real multiples, with their equality and closed Lie-subalgebra structure. (hard)
Theorem IV.3.3: Locally exponential structures on the actual closed subgroup inducing its subspace topology, an exponential slice chart, and the source closed-subspace notion of submanifold without a complement assumption. (hard)
Proposition IV.3.4: Actual subgroup Lie structures and preimage structure with subspace topology; the supplied smooth homomorphism and its differential cannot be treated as unrelated data. (hard)
Theorem IV.3.5: Quotient Lie structures inducing quotient topology, subgroup structures inducing subspace topology, and the quotient algebra and kappa neighborhood condition in the full three-way equivalence. (hard)
Corollary IV.3.6: BCH analytic structures on subgroups with subspace topology and group quotients with quotient topology; cannot assert only an algebraic quotient or only local exponentiality. (hard)
Theorem IV.3.8: The concrete subgroup generated by integrated adjoint automorphisms, an independently defined smooth structure with model g/z(g), and exponential of quotient classes; no ambient topology on Aut(g) is given. (hard)
Corollary IV.3.9: The intrinsic locally exponential structure on the actual group center with its subspace topology, plus its identification as the kernel of the computed Ad. (hard)
Corollary IV.3.12: The natural Banach manifold structure on GL(E), and a possibly nonsplit closed-subspace stabilizer as a Banach Lie submanifold with the induced topology. (hard)
Corollary IV.3.13: The natural Banach manifold structure on GL(E) and the actual vector stabilizer as a Banach Lie subgroup, with v=0 permitted. (hard)
Corollary IV.3.14: The Banach Lie group GL(E), the subgroup preserving the supplied continuous bilinear operation, and its tangent Lie algebra identified with exactly the continuous derivations. (hard)
Corollary IV.3.15: Unresolved printed source statement: Corollary IV.3.15 (source-ambiguity)
Lemma IV.4.2: Independent tangent Lie functor and exponential/adjoint flows on both groups, so stability of image and kernel is a conclusion, not a field in a morphism structure. (hard)
Lemma IV.4.3: Integrable adjoint operators and their smooth flows in the actual possibly different subalgebra and ambient topologies; BCH analyticity, finite (co)dimension, and all three clauses. (hard)
Theorem IV.4.9: Locally exponential topological Lie algebras, the actual smooth group exponential and derived injection; the discrete central preimage is a hypothesis, and the integral subgroup must have the prescribed derivative. (hard)
Corollary IV.4.10: The same prescribed-derivative integral subgroup construction without assuming closed range; the two alternative sufficient hypotheses must remain alternatives. (hard)
Theorem IV.4.14: Actual integral inclusion and differential, exponential tangent set, local exponential injectivity and separable source algebra; the stronger initiality conclusion requires locally exponential ambient G and closed differential range. (hard)
Theorem IV.4.16: An initial Lie topology on the closed subgroup that may be finer than the subspace topology; its identity component, tangent algebra, and prescribed integral inclusion. (hard)
Theorem IV.4.17: The actual finest required intrinsic initial Lie topology making the maximal contained vector subspace open; its identity component and equality with both actual tangent sets, rather than the original subgroup topology. (hard)
Theorem V.1.4: Locally smooth outer actions and their C2/C3 equations, actual twisted multiplication and unique local-product-compatible Lie atlas, extension equivalence classes, and abelian Baer sum as a fiber-product quotient. (hard)
Theorem V.1.8: Smooth locally trivial principal-bundle extensions and smooth endpoint evolution on all three groups; algebraic exactness alone does not define the extension category. (hard)
Theorem V.2.8: Normalized locally smooth cochains, coboundary quotient H_s^2, equivalence classes of principal-bundle extensions with the prescribed action, and the Baer group law; the isomorphism is the cocycle extension map. (hard)
Proposition V.2.10: Continuous alternating Lie cochains for the supplied joint continuous action, their differential and quotient, topologically split abelian extensions with the fixed action, and the computed twisted bracket. (hard)
Corollary V.3.2: Unresolved printed source statement: Corollary V.3.2 (source-ambiguity)
Theorem VI.1.8: Actual adjoint group, its pi2 period map for the central extension, period image in the topological center and enlargeability to a locally exponential group; no arbitrary subgroup labeled period group. (hard)
Proposition VI.1.9: The actual period subgroup and its inherited topology, for separable locally exponential algebras; closedness/discreteness equivalence requires the additional complete metrizable locally convex topology. (hard)
Theorem VI.1.10: Concrete Z(G,n), its normal locally exponential structure and computed algebra, normalized-loop period via represented weak integration, and generated exp(n) subgroup before closedness; retain all three equivalences without adding completeness. (hard)
Proposition VI.1.12: Canonical universal coverings of the adjoint groups, integration of the induced algebra map there, pi2 transport by covering isomorphisms, and naturality of the actual period maps and images. (hard)
Corollary VI.1.13: The actual period constructions on both topological Lie algebras and their product, with the canonical product identification of the centers. (hard)
Proposition VI.1.15: The actual central exponential kernel in a 1-connected locally exponential Frechet Lie group and an actual group isomorphism with pi1 of the center. (hard)
Theorem VI.1.17: Continuous based paths with the compact-open topology and pointwise bracket, local multiplication on that topology, enlargeability and the evaluation-at-1 quotient consequence. (hard)
Theorem VI.1.27: Completed projective tensor quotient cyclic homology, universal cyclic cocycle, stable K3 period map, and the actual topological Steinberg Lie algebras of all positive matrix sizes over the complete CIA. (hard)
Corollary VI.2.2: Stable ideals using actual integrated adjoint groups and the analytic locally convex Lie category with an analytic exponential, rather than ruling out every smooth integration. (hard)
Theorem VI.2.7: The actual semidirect topological Lie algebra with bracket (tDv-prime minus t-prime Dv,0), smooth joint R-actions and generator defined by directional differentiation, and integrability to arbitrary locally convex Lie groups. (hard)
Lemma VII.2.3: Compact-support diffeomorphism Lie structures, locally finite compact covers and the locally convex restricted direct-product topology; finite-support factorization with an existential terminal index for each input. (hard)
Theorem VIII.2: Unresolved printed source statement: Theorem VIII.2 (source-ambiguity)
Corollary IX.1.2: The natural LF manifold structure on compactly supported diffeomorphisms; continuity of the supplied homomorphism refers to that topology and smoothness refers to its actual charts. (hard)
Corollary IX.1.7: Unresolved printed source statement: Corollary IX.1.7 (source-ambiguity)
Theorem IX.1.9: Unresolved printed source statement: Theorem IX.1.9 (source-ambiguity)
Remark I.5.3 (explicit unnumbered result): The actual smooth vector-field space with the topology induced by all iterated tangent maps; finite-dimensional bracket continuity and the affine-field restriction proving failure on every nonempty open subset of an infinite-dimensional model. (hard)
Example II.1.4 (explicit unnumbered result): Continuous inverse algebra unit manifold as an open subset, smooth multiplication and inversion and the computed inversion derivative without imposing Mackey completeness or assuming an exponential. (hard)
Remark II.1.6 (explicit unnumbered result): The actual tangent bundle of a locally convex Lie group and tangent maps of multiplication and inversion, the zero identity vector, and zero-section/projection morphisms. (hard)
Remark II.3.7 (explicit unnumbered result): Smooth joint group actions and representations, actual infinitesimal derivatives with the left-action minus sign and linear-representation plus sign, and uniqueness of each action for a connected group. (hard)
Examples II.5.9 (explicit unnumbered result): Actual semidirect exponential and represented weak beta integral with beta(0)=id, the local-injectivity/surjectivity criteria, and both infinite diagonal-product examples in their product topologies. (hard)
Remark II.5.10 (explicit unnumbered result): Actual exponential of a Mackey-complete CIA unit group, tangent identification with A, and the differential represented by the integral of exp((1-t)x)y exp(tx) in precisely that noncommuting order. (hard)
Remark II.6.6 (explicit unnumbered result): The locally embedded subgroup definition via the smooth arc component of an identity neighborhood and its intrinsic Lie structure, and initiality for all finite orders. (hard)
Example IV.1.6 (explicit unnumbered result): The genuine homogeneous Dynkin BCH terms, finite polynomial sum for a nilpotent locally convex algebra, and its resulting group structure and identity exponential; H1 and H2 must not be counted twice. (hard)
Example IV.1.13 (explicit unnumbered result): Arbitrary projective systems of nilpotent topological Lie algebras with no uniform nilpotency bound, actual coordinatewise BCH products, and the induced smooth exponential group with exp=id. (hard)
Example IV.1.16 (explicit unnumbered result): The real sequence-space semidirect group, analytic structure and actual exp/log, smooth but nonanalytic inverse and exponential-coordinate multiplication; normed analyticity cannot be substituted on R^N. (hard)
Remark IV.2.5 (explicit unnumbered result): Independently chosen guarded local Lie products satisfying radial and second-order conditions, preservation by every continuous Lie algebra morphism near zero, and equality of their germs. (hard)
Example IV.4.5 (explicit unnumbered result): The Frechet smooth-function translation semidirect group, actual support-restricted subalgebra, generated subgroup C_c-infinity(R) semidirect R, and the exclusion of every exponential integration of the inclusion. (hard)
Example IV.4.6 (explicit unnumbered result): Unresolved printed source statement: Example IV.4.6 (explicit unnumbered result) (source-ambiguity)
Remark V.2.7 (explicit unnumbered result): Nonabelian group and Lie crossed cocycles with their actual infinitesimal differentiation map; normalized equivariant forms, injectivity for connected G, regular target integration and pointed-set exactness of the period sequence. (hard)
Remark V.2.9 (explicit unnumbered result): The stronger local cocycle smoothness at each g, H_ss^2 as the quotient by locally smooth coboundaries, and its actual extension-classification homomorphism without connectedness. (hard)
Remark V.2.16 (explicit unnumbered result): Unresolved printed source statement: Remark V.2.16 (explicit unnumbered result) (source-ambiguity)
Example V.3.5 (explicit unnumbered result): The actual torus area form, vector-field cocycle, period and flux maps, and the disconnected gauge kernel and principal circle bundle; the abelian extension must differentiate to that particular cocycle. (hard)
Remark VI.1.14 (explicit unnumbered result): Unresolved printed source statement: Remark VI.1.14 (explicit unnumbered result) (source-ambiguity)
Remark VI.1.22 (explicit unnumbered result): Unresolved printed source statement: Remark VI.1.22 (explicit unnumbered result) (source-ambiguity)
Example VI.2.8 (explicit unnumbered result): Formal vector fields with arbitrary constant term and coefficientwise Frechet topology, the formal derivative bracket and integrability to groups with exponential; the false split-sequence sentence is not an assumption. (hard)
Mapping groups as projective limits (unnumbered): Compact manifold-with-boundary exhaustion cofinal among all compact subsets, C^r mapping groups with the actual compact-open derivative topology and restriction bonding maps, and the topological-group limit universal property. (hard)
Lie algebra of the projective mapping group (unnumbered): The compact-open one-parameter-group Lie algebra of the projective mapping group, canonical identification with C^r(M,L(K)), and its actual pointwise exponential; no manifold structure on the noncompact full mapping group. (hard)
Holomorphic mapping-group projective limit (unnumbered): Unresolved printed source statement: Holomorphic mapping-group projective limit (unnumbered) (source-ambiguity)
Smooth structure from the pro-solvable coordinate chart (unnumbered): The actual pro-Lie integration functor and pro-solvable radical, closed commutator algebra and complemented weakly complete topology, and the specified exponential-product homeomorphism as a smooth group chart. (hard)

Selected references

Towards a Lie theory for locally convex groups, arXiv:1501.06269v1, https://arxiv.org/abs/1501.06269v1

7 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

The weighted hook length formulaResearch Paper

Motivation

Based on the ideas in [CKP], we introduce the weighted analogue of the branching rule for the classical hook length formula, and give two proofs of this result. The first proof is completely bijective, and in a special case gives a new short combinatorial proof of the hook length formula. Our second proof is probabilistic, generalizing the (usual) hook walk proof of Green-Nijenhuis-Wilf, as well as the q-walk of Kerov. Further applications are also presented.

This mission is the statement-level formalization of The weighted hook length formula (arXiv:1006.0043v1). 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 Four weighted branching identities (Theorem 2(a)–(d), PDF p. 6). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

§6.4, first new summation formula: An authoritative corrected first §6.4 summation formula with consistent coordinate and boundary conventions. (source-ambiguity)
§6.4, second new summation formula: An authoritative corrected second §6.4 summation formula with consistent coordinate and boundary conventions. (source-ambiguity)
§6.4, third new summation formula: An authoritative corrected third §6.4 summation formula with consistent coordinate and boundary conventions. (source-ambiguity)

Selected references

The weighted hook length formula, arXiv:1006.0043v1, https://arxiv.org/abs/1006.0043v1

12 thms2 active usersReviewed

Quantum Information·Captain: Goku

Unbounded generators of dynamical semigroupsResearch Paper

Motivation

Dynamical semigroups have become the key structure for describing open system dynamics in all of physics. Bounded generators are known to be of a standard form, due to Gorini, Kossakowski, Sudarshan and Lindblad. This form is often used also in the unbounded case, but rather little is known about the general form of unbounded generators. In this paper we first give a precise description of the standard form in the unbounded case, emphasizing intuition, and collecting and even proving the basic results around it. We also give a cautionary example showing that the standard form must not be read too naively. Further examples are given of semigroups, which appear to be probability preserving to first order, but are not for finite times. Based on these, we construct examples of generators which are not of standard form.

This mission is the statement-level formalization of Unbounded generators of dynamical semigroups (arXiv:1707.02266v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is No-event semigroups admit a C0 contraction implementation (Definition II.1, asserted realization of no-event semigroups, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

Abstract / Section IV: two concrete conservative non-standard generators: Concrete birth/diffusion models and standardness over all contraction generators (hard)
Section II.B, event expansion is the minimal semigroup: Completed event tensor powers, pathwise detection iterates, and trace-class partial traces (hard)
Proposition II.3: equivalent standard-form data: Exit rank-one lift, graph-continuous extension, Kraus and transit-basis correspondences (hard)
Section II.C, claimed converse resolvent characterization: Nondegeneracy of an abstract resolvent family (source-ambiguity)
Lemma II.6: gauge transformation: Corrected gauge data and equality of actual minimal standard semigroups (hard)
Proposition II.7: no additional nonzero rank-one factors: Standard jump realization with actual densely defined adjoints and forward equation (hard)
Section III.A: non-closable jump operators in a standard generator: Half-line H1 boundary trace and actual shift-generator jump composition (hard)
Section III.B.1: explicit quantum birth resolvent (32)–(33): Constructed quantum-birth standard semigroup and its actual Laplace resolvent (hard)
Lemma III.1: full birth-generator domain from matrix elements: Actual birth generator versus formal matrix-element action (hard)
Section III.B.2: conservativity and arrival transform: Quantum-birth arrival distribution and independent exponential waiting-time sum (hard)
Section III.B.3: boundary functionals and strict domain increase: Birth boundary coefficient functionals and constructed trace-class sigma (hard)
Proposition III.2: moderately growing rates support coherent escape: Moderately growing birth rates and trace-class coherent-shift operators (hard)
Section III.B.3, asserted stretched-exponential examples: A consistent quantitative moderate-growth condition (source-ambiguity)
Section III.B.3, Example: Exponentially growing rates: Exponential-rate birth generator and off-diagonal boundary functionals (hard)
Proposition III.3: no new rank-one operators for quantum birth: Computed actual birth and no-event domains on rank-one operators (hard)
Section III.C: diagonal-diffusion semigroup and resolvent kernels: Absorbing H2 half-line realization and a.e. trace-class kernel evolution (hard)
Section III.C: boundary regularity and normalization loss: Nuclear trace density, diffusion-domain regularity and boundary derivative (hard)
Section III.C: no new rank-one operators for diagonal diffusion: Actual Dirichlet adjoint realization and minimal diffusion rank-one domains (hard)
Section IV, conservative rank-one reset perturbation (52): Actual reset semigroups for both concrete nonconservative models (hard)

Selected references

Unbounded generators of dynamical semigroups, arXiv:1707.02266v1, https://arxiv.org/abs/1707.02266v1

9 thms2 active usersReviewed

Quantum Information·Captain: Goku

On Analytic Vectors for Unitary Representations of Infinite Dimensional Lie GroupsResearch Paper

Motivation

Let $G$ be a 1-connected Banach-Lie group or, more generally, a BCH--Lie group. On the complex enveloping algebra $U_\C(\g)$ of its Lie algebra $\g$ we define the concept of an analytic functional and show that every positive analytic functional $\lambda$ is integrable in the sense that it is of the form $\lambda(D) = \la \dd\pi(D)v, v\ra$ for an analytic vector $v$ of a unitary representation of $G$ . On the way to this result we derive criteria for the integrability of *-representations of infinite dimensional Lie algebras of unbounded operators to unitary group representations. For the matrix coefficient $\pi^{v,v}(g) = \la \pi(g)v,v\ra$ of a vector $v$ in a unitary representation of an analytic Fr'echet-Lie group $G$ we show that $v$ is an analytic vector if and only if $\pi^{v,v}$ is analytic in an identity neighborhood. Combining this insight with the results on positive analytic functionals, we derive that every local positive definite analytic function on a 1-connected Fr'echet--BCH--Lie group $G$ extends to a global analytic function.

This mission is the statement-level formalization of On Analytic Vectors for Unitary Representations of Infinite Dimensional Lie Groups (arXiv:1002.4792v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Analytic functionals: seminorm and Banach norm criteria (Proposition 3.4, PDF p. 9). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

Proposition 4.6: The actual smooth locally convex Lie group and its tangent Lie algebra, the smooth-vector subspace of the given continuous action on the same locally convex space V, and its computed tangent-derived action with values in that subspace. (hard)
Theorem 5.1: A paper-local locally convex analytic manifold interface: complexifications, continuous iterated directional derivatives, local holomorphic extension, actual tangent spaces and chart transitions. (hard)
Theorem 5.2: Analytic Frechet Lie groups in the source's locally convex calculus, continuous unitary actions on arbitrary complex Hilbert spaces, analytic full orbit maps, and their computed diagonal coefficients. No BCH hypothesis or derived-action interface is needed to state this criterion. (hard)
Corollary 5.3: Real analyticity of scalar functions on analytic Frechet Lie groups, local analyticity at the identity, and positive definiteness of the computed group kernel. No BCH, connectedness, tangent-derived action, or given Hilbert realization is needed to state the corollary. (hard)
Proposition 6.3: The canonical complexified enveloping algebra with its antilinear anti-automorphism x*=−x, canonical complex-linear extension of the given action, and positive coefficient functionals. (hard)
Proposition 6.5: The canonical complexified enveloping algebra with its antilinear anti-automorphism x*=−x, canonical complex-linear extension of the given action, and positive coefficient functionals. The canonical GNS construction from the supplied positive functional: null-space quotient, pre-Hilbert completion H_lambda, dense cyclic invariant domain D_lambda, and computed right regular action rho_lambda. (hard)
Lemma 6.7: A convergent BCH Lie algebra interface in the locally convex holomorphic calculus, linked to actual unitary Stone flows with full graph-closure generators. (hard)
Theorem 6.8: Actual BCH/analytic Lie group structure and tangent Lie algebra identification, exponential curves, smooth and analytic orbit maps, and derived actions computed from the same continuous representation on the same Hilbert space. A convergent BCH Lie algebra interface in the locally convex holomorphic calculus, linked to actual unitary Stone flows with full graph-closure generators. (hard)
Lemma 6.9: The canonical complexified enveloping algebra with its antilinear anti-automorphism x*=−x, canonical complex-linear extension of the given action, and positive coefficient functionals. The canonical GNS construction from the supplied positive functional: null-space quotient, pre-Hilbert completion H_lambda, dense cyclic invariant domain D_lambda, and computed right regular action rho_lambda. (hard)
Unnumbered assertion before Theorem 6.10: An analytic locally convex Lie group with its actual tangent Lie algebra, smooth and analytic orbit maps for the same continuous unitary action on the same Hilbert space, and the canonical complex enveloping extension of its derived action with antilinear anti-automorphism x*=−x. No BCH or connectedness hypothesis is required. (hard)
Theorem 6.10: Actual BCH/analytic Lie group structure and tangent Lie algebra identification, exponential curves, smooth and analytic orbit maps, and derived actions computed from the same continuous representation on the same Hilbert space. The canonical complexified enveloping algebra with its antilinear anti-automorphism x*=−x, canonical complex-linear extension of the given action, and positive coefficient functionals. The canonical GNS construction from the supplied positive functional: null-space quotient, pre-Hilbert completion H_lambda, dense cyclic invariant domain D_lambda, and computed right regular action rho_lambda. (hard)
Corollary 6.11: Actual BCH/analytic Lie group structure and tangent Lie algebra identification, exponential curves, smooth and analytic orbit maps, and derived actions computed from the same continuous representation on the same Hilbert space. The canonical complexified enveloping algebra with its antilinear anti-automorphism x*=−x, canonical complex-linear extension of the given action, and positive coefficient functionals. The canonical GNS construction from the supplied positive functional: null-space quotient, pre-Hilbert completion H_lambda, dense cyclic invariant domain D_lambda, and computed right regular action rho_lambda. (hard)
Theorem 6.12: Actual BCH/analytic Lie group structure and tangent Lie algebra identification, exponential curves, smooth and analytic orbit maps, and derived actions computed from the same continuous representation on the same Hilbert space. A convergent BCH Lie algebra interface in the locally convex holomorphic calculus, linked to actual unitary Stone flows with full graph-closure generators. (hard)
Example 6.14: A source-consistent real multiplication representation and a probability-space assumption forcing nondiscreteness. (source-ambiguity)
Remark 6.15: An abelian Banach Lie group with actual exponential curves, a continuous unitary action with dense analytic full orbit vectors, and its computed closed kernel and exponential Lie algebra {x : for all real t, pi(exp(t*x))=1}. The kernel is not assumed an embedded Lie subgroup. (hard)
Lemma 7.2: A paper-local locally convex analytic manifold interface: complexifications, continuous iterated directional derivatives, local holomorphic extension, actual tangent spaces and chart transitions. (hard)
Theorem 7.3: Analytic Frechet BCH Lie groups and scalar analyticity in the source's locally convex calculus; a connected open identity neighborhood V, the full domain V*V-inverse, its local positive definite kernel, and global positive definite analytic extension. A group representation or derived action is not part of the data needed to state the result. (hard)

Selected references

On Analytic Vectors for Unitary Representations of Infinite Dimensional Lie Groups, arXiv:1002.4792v2, https://arxiv.org/abs/1002.4792v2

10 thms2 active usersReviewed

Quantum Information·Captain: Goku

Energy-constrained diamond norms and their use in quantum information theoryResearch Paper

Motivation

We consider the family of energy-constrained diamond norms on the set of Hermitian-preserving linear maps (superoperators) between Banach spaces of trace class operators. We prove that any norm from this family generates the strong (pointwise) convergence on the set of all quantum channels (which is more adequate for describing variations of infinite-dimensional channels than the diamond norm topology). We obtain continuity bounds for information characteristics (in particular, classical capacities) of energy-constrained quantum channels (as functions of a channel) with respect to the energy-constrained diamond norms which imply uniform continuity of these characteristics with respect to the strong convergence topology.

This mission is the statement-level formalization of Energy-constrained diamond norms and their use in quantum information theory (arXiv:1706.00361v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

7 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 3 A–B: general-input ECD convergence and strong topology (Abstract topology result, precisely Proposition 3 A–B, PDF p. 6). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

§4, unnumbered: (2) is a norm on all L(A,B): A valid literal source claim on its printed domain; §4, unnumbered: (2) is a norm on all L(A,B) (source-ambiguity)
Remark 1: extension to operator-norm-bounded HP subsets: A valid literal source claim on its printed domain; Remark 1: extension to operator-norm-bounded HP subsets (source-ambiguity)
Proposition 4: output Holevo continuity and oscillator form: Adapters from accepted oscillator spectrum/entropy model to the closed-form coefficient-channel model, and actual sharpness constructions (hard)
Remark 3: existence of an optimal t: A valid literal source claim on its printed domain; Remark 3: existence of an optimal t (source-ambiguity)
Corollary 1: literal universal-metric claim: A valid literal source claim on its printed domain; Corollary 1: literal universal-metric claim (source-ambiguity)
Remark 4: any metric generating strong topology: A valid literal source claim on its printed domain; Remark 4: any metric generating strong topology (source-ambiguity)
Proposition 5: n-copy output QMI continuity: Adapters from accepted oscillator spectrum/entropy model to the closed-form coefficient-channel model, and actual sharpness constructions (hard)
Remark 5: full QCMI extension of Proposition 5: Adapters from accepted oscillator spectrum/entropy model to the closed-form coefficient-channel model, and actual sharpness constructions; full extended QCMI (hard)
Corollary 2: literal universal-metric claim: A valid literal source claim on its printed domain; Corollary 2: literal universal-metric claim (source-ambiguity)
Proposition 6: Holevo and regularized classical continuity: Adapters from accepted oscillator spectrum/entropy model to the closed-form coefficient-channel model, and actual sharpness constructions (hard)
Proposition 7 A–B: entanglement-assisted continuity: Adapters from accepted oscillator spectrum/entropy model to the closed-form coefficient-channel model, and actual sharpness constructions (hard)
Corollary 3 A–B: literal universal-metric claim: A valid literal source claim on its printed domain; Corollary 3 A–B: literal universal-metric claim (source-ambiguity)
§5.3: identity/vacuum sharpness examples: Adapters from accepted oscillator spectrum/entropy model to the closed-form coefficient-channel model, and actual sharpness constructions (hard)

Selected references

Energy-constrained diamond norms and their use in quantum information theory, arXiv:1706.00361v2, https://arxiv.org/abs/1706.00361v2

15 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

Minimal computational-space implementation of multi-round quantum protocolsResearch Paper

Motivation

A single-party strategy in a multi-round quantum protocol can be implemented by sequential networks of quantum operations connected by internal memories. Here provide the most efficient realization in terms of computational-space resources.

This mission is the statement-level formalization of Minimal computational-space implementation of multi-round quantum protocols (arXiv:1006.1780v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 1 and Eq.(8): Haar averaging preserves the optimum and yields covariance (Lemma 1 and Eq.(8): Haar averaging preserves the optimum and yields covariance, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

Theorem 2 and Eq.(4), continued on p.3: A general changing-support coherent network with the literal Eq.(4) stage maps and all-round memory minima. (hard)
Conclusion, algorithm steps 1-5: A defined full-comb-to-prefix recovery and the support-space Eq.(4) synthesis procedure, linked to an actual output network. (hard)

Selected references

Minimal computational-space implementation of multi-round quantum protocols, arXiv:1006.1780v1, https://arxiv.org/abs/1006.1780v1

7 thms2 active usersReviewed

Quantum Information·Captain: Goku

Structure of H-(co)module Lie algebrasResearch Paper

Motivation

Let $L$ be a finite dimensional Lie algebra over a field of characteristic $0$ . Then by the original Levi theorem, $L = B \oplus R$ where $R$ is the solvable radical and $B$ is some maximal semisimple subalgebra. We prove that if $L$ is an $H$ -(co)module algebra for a finite dimensional (co)semisimple Hopf algebra $H$ , then $R$ is $H$ -(co)invariant and $B$ can be chosen to be $H$ -(co)invariant too. Moreover, the nilpotent radical $N$ of $L$ is $H$ -(co)invariant and there exists an $H$ -sub(co)module $S\subseteq R$ such that $R=S\oplus N$ and $[B,S]=0$ . In addition, the $H$ -(co)invariant analog of the Weyl theorem is proved. In fact, under certain conditions, these results hold for an $H$ -comodule Lie algebra $L$ , even if $H$ is infinite dimensional. In particular, if $L$ is a Lie algebra graded by an arbitrary group $G$ , then $B$ can be chosen to be graded, and if $L$ is a Lie algebra with a rational action of a reductive affine algebraic group $G$ by automorphisms, then $B$ can be chosen to be $G$ -invariant. Also we prove that every finite dimensional semisimple $H$ -(co)module Lie algebra over a field of characteristic $0$ is a direct sum of its minimal $H$ -(co)invariant ideals.

This mission is the statement-level formalization of Structure of H-(co)module Lie algebras (arXiv:1205.0778v7). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

36 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 13 (abstract structural capstone; original seed) (Theorem 13 (abstract structural capstone; original seed), PDF p. 14). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

Example 4: Affine algebraic group coordinate Hopf algebra, rational actions and geometric reductivity (hard)
Example 7: Affine algebraic group coordinate Hopf algebra and the coaction constructed from a given rational action, with algebraic invariant-subspace correspondence (hard)
Example 10: Canonical Sweedler Hopf algebra, basis, and the specified action on sl2 plus its abelian adjoint copy (hard)
Theorem 5: Affine algebraic group coordinate Hopf algebra, rational actions and geometric reductivity (hard)
Theorem 11: Affine algebraic group coordinate Hopf algebra, rational actions and geometric reductivity (hard)
Corollary to Theorem 11: Affine algebraic group coordinate Hopf algebra, rational actions and geometric reductivity (hard)
Theorem 15: Affine algebraic group coordinate Hopf algebra, rational actions and geometric reductivity (hard)

Selected references

Structure of H-(co)module Lie algebras, arXiv:1205.0778v7, https://arxiv.org/abs/1205.0778v7

37 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

On the Fundamental Principles of Unbounded Functional CalculiResearch Paper

Motivation

In this paper, a new axiomatization for unbounded functional calculi is proposed and the associated theory is elaborated comprising, among others, uniqueness and compatibility results and extension theorems of algebraic and topological nature. In contrast to earlier approaches, no commutativity assumptions need to be made about the underlying algebras. In a second part, the abstract theory is illustrated in familiar situations (sectorial operators, semigroup generators, normal operators). New topological extension theorems are proved for the sectorial calculus and the Hille--Phillips calculus. Moreover, it is shown that the Stieltjes and the Hirsch calculus for sectorial operators are subcalculi of a (small) topological extension of the sectorial calculus.

This mission is the statement-level formalization of On the Fundamental Principles of Unbounded Functional Calculi (arXiv:2009.04733v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

31 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 6.1 (Extension Theorem) (Theorem 6.1 (Extension Theorem), 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.

Deferred results

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

Lemma 4.3: A source correction preserving the printed scope (source-ambiguity)
§10, classical elementary sectorial-calculus identity: A source correction preserving the printed scope (source-ambiguity)
§10, unnumbered: compatibility under sector restriction: Concrete elementary sectorial contour evaluation, meromorphic sector/germ algebra, and its canonical algebraic/topological extensions (hard)
Lemma 11.3: Concrete elementary sectorial contour evaluation, meromorphic sector/germ algebra, and its canonical algebraic/topological extensions (hard)
Theorem 11.4: Concrete elementary sectorial contour evaluation, meromorphic sector/germ algebra, and its canonical algebraic/topological extensions (hard)
Corollary 11.5: Concrete elementary sectorial contour evaluation, meromorphic sector/germ algebra, and its canonical algebraic/topological extensions (hard)
§11, unnumbered: uniform and bp extensions: Concrete elementary sectorial contour evaluation, meromorphic sector/germ algebra, and its canonical algebraic/topological extensions (hard)
Proposition 12.1: Finite-complex-measure strong operator integral, Stieltjes symbol construction, and concrete uniform sectorial extension (hard)
§12.2, unnumbered: Hirsch calculus inclusion: Weighted Radon complex measure integration, constructed Hirsch decomposition, and concrete uniform sectorial extension (hard)
Proposition 12.2: Principal complex powers, damped fractional holomorphic-semigroup evaluation, finite-complex-measure strong integration and the uniform sectorial extension (hard)
Proposition 13.1 (Complex inversion formula): A source correction preserving the printed scope (source-ambiguity)
Theorem 13.3: Finite-complex-measure Laplace image algebra, inverse Laplace measure selection, and strong-integral Hille–Phillips evaluation with its computed extensions (hard)
Remark 13.4: Finite-complex-measure Laplace image algebra, inverse Laplace measure selection, and strong-integral Hille–Phillips evaluation with its computed extensions (hard)
§13.3, unnumbered: HP and sectorial compatibility: Concrete elementary sectorial contour evaluation, meromorphic sector/germ algebra, and its canonical algebraic/topological extensions; Finite-complex-measure Laplace image algebra, inverse Laplace measure selection, and strong-integral Hille–Phillips evaluation with its computed extensions (hard)
Remarks 13.5(1): Finite-complex-measure Laplace image algebra, inverse Laplace measure selection, and strong-integral Hille–Phillips evaluation with its computed extensions; bounded Stieltjes algebra and meromorphic half-plane germs (hard)
Lemma 13.6: A source correction preserving the printed scope (source-ambiguity)
§13.3, unnumbered: semigroup reconstruction: Concrete elementary sectorial contour evaluation, meromorphic sector/germ algebra, and its canonical algebraic/topological extensions; Finite-complex-measure Laplace image algebra, inverse Laplace measure selection, and strong-integral Hille–Phillips evaluation with its computed extensions (hard)

Selected references

On the Fundamental Principles of Unbounded Functional Calculi, arXiv:2009.04733v1, https://arxiv.org/abs/2009.04733v1

38 thms2 active usersReviewed

Quantum Information·Captain: Goku

The entropy power inequality for quantum systemsResearch Paper

Motivation

When two independent analog signals, X and Y are added together giving Z=X+Y, the entropy of Z, H(Z), is not a simple function of the entropies H(X) and H(Y), but rather depends on the details of X and Y's distributions. Nevertheless, the entropy power inequality (EPI), which states that exp [2H(Z)] \geq exp[2H(X)] + exp[2H(Y)], gives a very tight restriction on the entropy of Z. This inequality has found many applications in information theory and statistics. The quantum analogue of adding two random variables is the combination of two independent bosonic modes at a beam splitter. The purpose of this work is to give a detailed outline of the proof of two separate generalizations of the entropy power inequality to the quantum regime. Our proofs are similar in spirit to standard classical proofs of the EPI, but some new quantities and ideas are needed in the quantum setting. Specifically, we find a new quantum de Bruijin identity relating entropy production under diffusion to a divergence-based quantum Fisher information. Furthermore, this Fisher information exhibits certain convexity properties in the context of beam splitters.

This mission is the statement-level formalization of The entropy power inequality for quantum systems (arXiv:1205.3409v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

17 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Entropy power inequality for the 50:50 beam splitter (Theorem VII.2, (89); paper-level seed pp.1–2, PDF p. 12). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

Lemma III.1: Hilbert-Schmidt space realization and closed domain of the canonical heat generator, including its quadrature double-commutator identification (hard)
Theorem III.3, (57): A correct source-level upper bound using the printed symplectic-eigenvalue data (source-ambiguity)
Equation (63): Correct entropy comparison and compatible majorization convention (source-ambiguity)
Lemma IV.5, (76)–(78): Spectral logarithm of a faithful infinite-dimensional density, unbounded Hamiltonian commutators, and weighted trace domains (hard)
Theorem V.1, (82): Finite entropy derivative domain with justified unbounded-log trace/derivative interchanges for the canonical heat flow (hard)
Appendix, (101)–(102): Specified generalized-function space or regularization/topology for the inverse-Q operator kernel (source-ambiguity)

Selected references

The entropy power inequality for quantum systems, arXiv:1205.3409v2, https://arxiv.org/abs/1205.3409v2

22 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

Canonical idempotents of multiplicity-free families of algebrasResearch Paper

Motivation

Any multiplicity-free family of finite dimensional algebras has a canonical complete set of of pairwise orthogonal primitive idempotents in each level. We give various methods to compute these idempotents. In the case of symmetric group algebras over a field of characteristic zero, the set of canonical idempotents is precisely the set of seminormal idempotents constructed by Young. As an example, we calculate the canonical idempotents for semisimple Brauer algebras.

This mission is the statement-level formalization of Canonical idempotents of multiplicity-free families of algebras (arXiv:1606.08900v5). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

20 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Introduction (1), made precise by Proposition 1.6: canonical partition and GT basis (Introduction (1), made precise by Proposition 1.6: canonical partition and GT basis, 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.

Deferred results

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

Algorithm 2.5: random central-element search (deferred stochastic specification): A specified effective sampling distribution on Z(A), and spectrum computation access for arbitrary characteristic-zero fields. (source-ambiguity)
Example 2.6: claimed Hecke center generator (source conflict): A corrected q-domain or a corrected Hecke element whose central spectrum is simple. (source-ambiguity)
Example 2.7: transposition sums stop generating the center: All-partition simple right modules of kS_n and their shape-labelled central spectra. (hard)
Proposition 4.2: transposition-sum eigenvalue: Tableaux, normalized row-column Young symmetrizers, and the actual right ideals y_T kS_n. (hard)
Proposition 4.3: symmetric-group JM contents: The identification of standard tableaux with actual branching paths and GT lines of the right group-algebra tower. (hard)
Corollary 4.5: symmetric-group JM-sequence: A constructed symmetric-group tower and its concrete unshifted JM sequence. (hard)
Proposition 4.6 (Young): central sum of Young idempotents: The sum of normalized Young idempotents over ALL tableaux of a fixed shape. (hard)
Proposition 4.7: equality with Young seminormal idempotents: An independent recursive construction of Young seminormal idempotents. (hard)
Examples 4.9: displayed symmetric-group central idempotents: Shape-labelled symmetric-group canonical central projectors and the complete finite list of displayed identities. (hard)
Theorem 5.1 (Green): simple modules of an idempotent corner: The actual right-module Schur functor M→Me for an arbitrary unital algebra, including simple-module isomorphism classes. (hard)
Proposition 5.2: corner induction and semisimple equivalence: Balanced tensor induction G(N)=N tensor_(eAe) eA and its natural inverse equivalence on M(AeA)=M. (hard)
Proposition 5.3: constructed irreducible Brauer modules: Brauer diagram multiplication, rank quotient bimodule V_k^n, and M^(lambda,n)=S^lambda tensor_(kS_k) V_k^n. (hard)
Remark 5.4: dangle tensor basis of constructed modules: Flat rank-k (k,n)-dangles and their actual tensor images in the constructed module. (hard)
Unnumbered multiplicity-free Brauer branching theorem: Restriction of the constructed Brauer tensor modules along the actual diagram inclusion. (hard)
Lemma 5.5: relative commutation, with corrected level subscript: Concrete Brauer relative centralizers, unshifted J_k, and the corrected predecessor level. (hard)
Proposition 5.6: Brauer JM commutation relations: Concrete Brauer s_k,e_k,J_l in the diagram algebra, with their ambient level embeddings. (hard)
Corollary 5.7: centrality of Brauer partial sums: Concrete Brauer partial sum z_n and membership in the full center of B_n. (hard)
Proposition 5.8: central scalar on constructed Brauer simples: Actual action of the concrete Brauer central partial sum on the tensor quotient simple M^(lambda,n). (hard)
Proposition 5.9: up/down JM eigenvalues: Canonical GT lines of actual constructed Brauer simples and valid up/down path identification. (hard)
Corollary 5.10: Brauer JM-sequence: Concrete Brauer Tower instance and the unshifted diagram JM sequence. (hard)
Examples 5.11: displayed Brauer central idempotents: Shape-labelled Brauer central projectors with level-dependent labels and all displayed n≤4 formulas. (hard)

Selected references

Canonical idempotents of multiplicity-free families of algebras, arXiv:1606.08900v5, https://arxiv.org/abs/1606.08900v5

21 thms2 active usersReviewed

Quantum Information·Captain: Goku

The Capacity of Symmetric Private Information RetrievalResearch Paper

Motivation

Private information retrieval (PIR) is the problem of retrieving as efficiently as possible, one out of $K$ messages from $N$ non-communicating replicated databases (each holds all $K$ messages) while keeping the identity of the desired message index a secret from each individual database. Symmetric PIR (SPIR) is a generalization of PIR to include the requirement that beyond the desired message, the user learns nothing about the other $K-1$ messages. The information theoretic capacity of SPIR (equivalently, the reciprocal of minimum download cost) is the maximum number of bits of desired information that can be privately retrieved per bit of downloaded information. We show that the capacity of SPIR is $1-1/N$ regardless of the number of messages $K$ , if the databases have access to common randomness (not available to the user) that is independent of the messages, in the amount that is at least $1/(N-1)$ bits per desired message bit, and zero otherwise. Extensions to the capacity region of SPIR and the capacity of finite length SPIR are provided.

This mission is the statement-level formalization of The Capacity of Symmetric Private Information Retrieval (arXiv:1606.08828v2). 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 SPIR capacity and common-randomness threshold (Theorem 1, (12), 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.

Selected references

The Capacity of Symmetric Private Information Retrieval, arXiv:1606.08828v2, https://arxiv.org/abs/1606.08828v2

13 thms2 active usersReviewed

Quantum Information·Captain: Goku

Classification of 3-graded causal subalgebras of real simple Lie algebrasResearch Paper

Motivation

Let $(\mathfrak{g},\tau)$ be a real simple symmetric Lie algebra and let $W \subset \mathfrak{g}$ be an invariant closed convex cone which is pointed and generating with $\tau(W) = -W$ . For elements $h \in \mathfrak{g}$ with $\tau(h) = h$ , we classify the Lie algebras $\mathfrak{g}(W,\tau,h)$ which are generated by the closed convex cones

C_{\pm}(W,\tau,h) := (\pm W) \cap \mathfrak{g}_{\pm 1}^{-\tau}(h),

where $\mathfrak{g}^{-\tau}_{\pm 1}(h) := \{x \in \mathfrak{g} : \tau(x) = -x, [h,x] = \pm x\}$ . These cones occur naturally as the skew-symmetric parts of the Lie wedges of endomorphism semigroups of certain standard subspaces. We prove in particular that, if $\mathfrak{g}(W,\tau,h)$ is non-trivial, then it is either a hermitian simple Lie algebra of tube type or a direct sum of two Lie algebras of this type. Moreover, we give for each hermitian simple Lie algebra and each equivalence class of involutive automorphisms $\tau$ of $\mathfrak{g}$ with $\tau(W) = -W$ a list of possible subalgebras $\mathfrak{g}(W,\tau,h)$ up to isomorphy.

This mission is the statement-level formalization of Classification of 3-graded causal subalgebras of real simple Lie algebras (arXiv:2001.03125v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

28 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 2.6: tube type and nonzero three-gradings (Lemma 2.6, PDF p. 6). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

Theorem 1.1: The complete Table 1 relation of concrete real symmetric-pair and output Lie algebras (hard)
Theorem 3.7: Table 3 as a paired concrete Jordan/Lie isomorphism classification (hard)
Proposition 3.23: Table 4 as a five-row relation of four concrete real Lie algebras (hard)
Proposition 3.25: Exhaustiveness for every row of the concrete Table 1 relation (hard)
Proposition 3.26: Realizability of every allowed concrete Table 1 output for each fixed involution (hard)

Selected references

Classification of 3-graded causal subalgebras of real simple Lie algebras, arXiv:2001.03125v2, https://arxiv.org/abs/2001.03125v2

30 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

A Practical Quantum Algorithm for the Schur TransformResearch Paper

Motivation

We describe an efficient quantum algorithm for the quantum Schur transform. The Schur transform is an operation on a quantum computer that maps the standard computational basis to a basis composed of irreducible representations of the unitary and symmetric groups. We simplify and extend the algorithm of Bacon, Chuang, and Harrow, and provide a new practical construction as well as sharp theoretical and practical analyses. Our algorithm decomposes the Schur transform on $n$ qubits into $O\left(n^4\log\left(\frac{n}{\epsilon}\right)\right)$ operators in the Clifford+T fault-tolerant gate set and uses exactly $2\lfloor\log_2(n)\rfloor-1$ ancillary qubits. We extend our qubit algorithm to decompose the Schur transform on $n$ qudits of dimension $d$ into $O\left(n^{d^2+2}\log^p\left(\frac{n^{d^2+1}}{\epsilon}\right)\right)$ primitive operators from any universal gate set, for $p\approx3.97$ .

This mission is the statement-level formalization of A Practical Quantum Algorithm for the Schur Transform (arXiv:1709.07119v6). 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 Exact three-register Schur encoding space (§3.3 Eqs.(24)–(27), PDF p. 14). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

Abstract; §4 Eqs.(35)–(36): A concrete source-compatible padded recursive Schur family together with a fixed-wire nuclear-norm H,T,CNOT compiler. (hard)
Erratum: The source recursive synthesis/analysis maps on fixed padded coordinates to which reversal can be attached. (hard)
§§3.1–3.3: Complete bodies for source spin-CG blocks, ancillary insertion and a compatible routing permutation including ghost coordinates at every stage. (hard)
§3 Eq.(19); §4 Eqs.(31)–(34): An exact shared-block program with matrix semantics tied to the source CG/routing construction. (hard)
§4 Eq.(34): A corrected source-endorsed refined polynomial in Eq.(34). (source-ambiguity)
§5 Eqs.(38)–(39); §6 item 3: A source-compatible general-d add-a-box encoding and exact shared CG-plus-routing program. (hard)
Abstract; §5 Eq.(40): The intended quantified class of qudit primitive alphabets and its synthesis/error convention. (source-ambiguity)

Selected references

A Practical Quantum Algorithm for the Schur Transform, arXiv:1709.07119v6, https://arxiv.org/abs/1709.07119v6

3 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

On the relation between states and maps in infinite dimensionsResearch Paper

Motivation

Relations between states and maps, which are known for quantum systems in finite-dimensional Hilbert spaces, are formulated rigorously in geometrical terms with no use of coordinate (matrix) interpretation. In a tensor product realization they are represented simply by a permutation of factors. This leads to natural generalizations for infinite-dimensional Hilbert spaces and a simple proof of a generalized Choi Theorem. The natural framework is based on spaces of Hilbert-Schmidt operators $\mathcal{L}_2(\mathcal{H}_2,\mathcal{H}_1)$ and the corresponding tensor products $\mathcal{H}_1\otimes\mathcal{H}_2^*$ of Hilbert spaces. It is proved that the corresponding isomorphisms cannot be naturally extended to compact (or bounded) operators, nor reduced to the trace-class operators. On the other hand, it is proven that there is a natural continuous map $\mathcal{C}:\mathcal{L}_1(\mathcal{L}_2(\mathcal{H}_2,\mathcal{H}_1))\to \mathcal{L}_\infty(\mathcal{L}(\mathcal{H}_2),\mathcal{L}_1(\mathcal{H}_1))$ from trace-class operators on $\mathcal{L}_2(\mathcal{H}_2,\mathcal{H}_1)$ (with the nuclear norm) into compact operators mapping the space of all bounded operators on $\mathcal{H}_2$ into trace class operators on $\mathcal{H}_1$ (with the operator-norm). Also in the infinite-dimensional context, the Schmidt measure of entanglement and multipartite generalizations of state-maps relations are considered in the paper.

This mission is the statement-level formalization of On the relation between states and maps in infinite dimensions (arXiv:0706.2617v1). 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 Finite-dimensional Jamiolkowski permutations are unitary and equivariant (Theorem 1; equations (12)–(17), PDF p. 6). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

§3, unnumbered construction (18)–(19): Complete Hilbert–Schmidt operator Hilbert space with bounded-operator realization and canonical conjugate-dual tensor equivalence (hard)
Proposition 1, (20)–(23): Matrix-element and four-factor pairing characterization with uniqueness for both completed B2 permutations (hard)
Example 1, (24)–(28): Hilbert–Schmidt sandwich superoperators and their rank-one J images (hard)
Proposition 2; examples on pp.9–10: Operator-norm compact extensions and failure of trace-class restriction for J and its inverse (hard)
Theorem 2, (29): Trace-norm Banach space of nuclear operators on B2 and the compact bounded-to-trace-class Choi operator (hard)
§3, state-to-Kraus conclusion: Density operators on B2 and nuclear-norm convergent Kraus sums under C (hard)
Theorem 3: Adjoint on the realized B2 Hilbert space and J Hermiticity criterion (hard)
Theorem 4; proof p.14: Positive cone on B2 inputs, countably separable density ensembles, and trace tests of J (hard)
Theorem 5; proof (33)–(35): Positivity of finite identity amplifications and fixed injective positive Hilbert–Schmidt Kraus amplifications (hard)
Proposition 4: Extended vector Schmidt rank and inverse twisted-J operator rank (hard)
Corollary 1; Definition 3 p.16: Pure countably separable density states and operator Schmidt rank of the twisted preimage (hard)
Equation (36) and following claim: A source-selected correction of the convex roof formula or claimed zero set (source-ambiguity)
§6, three-space displayed chain: Canonical six-factor rearrangements on three nested complete B2 spaces (hard)
§6, top horizontal arrow of four-space square: Canonical eight-factor middle swap on nested completed B2 spaces (hard)
§6, lower row of four-space square: A uniquely specified well-typed lower-left four-space operator expression (source-ambiguity)

Selected references

On the relation between states and maps in infinite dimensions, arXiv:0706.2617v1, https://arxiv.org/abs/0706.2617v1

4 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

Squashed entanglement for multipartite states and entanglement measures based on the mixed convex roofResearch Paper

Motivation

New measures of multipartite entanglement are constructed based on two definitions of multipartite information and different methods of optimizing over extensions of the states. One is a generalization of the squashed entanglement where one takes the mutual information of parties conditioned on the state's extension and takes the infimum over such extensions. Additivity of the multipartite squashed entanglement is proved for both versions of the multipartite information which turn out to be related. The second one is based on taking classical extensions. This scheme is generalized, which enables to construct measures of entanglement based on the {\it mixed convex roof} of a quantity, which in contrast to the standard convex roof method involves optimization over all decompositions of a density matrix rather than just the decompositions into pure states. As one of the possible applications of these results we prove that any multipartite monotone is an upper bound on the amount of multipartite distillable key. The findings are finally related to analogous results in classical key agreement.

This mission is the statement-level formalization of Squashed entanglement for multipartite states and entanglement measures based on the mixed convex roof (arXiv:0704.2236v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

19 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 4 / abstract: additivity of both multipartite q-squashed entanglements (Proposition 4 / abstract: additivity of both multipartite q-squashed entanglements, PDF p. 6). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

§IV.D equation (54): measured-correlation mixed roof example: Average-local-monotonicity premise for independent-measurement I_c (source-ambiguity)
Theorem 2: axiomatic quantum upper bound on distillable key: Unrestricted multipartite pdit distillation protocols, operational key capacity, and communication accounting (hard)
Example 1 / equation (75): normalized q-squashed key upper bound: Unrestricted multipartite pdit distillation protocols, operational key capacity, and communication accounting (hard)
Theorem 3 [13]: multipartite Devetak–Winter protocol (cited/background): Classicalization and preprocessing assumptions absent from the printed Devetak–Winter rate (source-ambiguity)
Lemma 3 and Remarks 1–2: communication and output support bounds: Correct support-space dimension and uniform dependence of the communication constant (source-ambiguity)
§V.C: unrestricted key-rate supremum equals linear-communication supremum: Unrestricted multipartite pdit distillation protocols, operational key capacity, and communication accounting (hard)
Theorem 4: axiomatic classical upper bound on distillable key: Multipartite adaptive LOPC capacity with Eve transcripts and full-l1 secrecy (hard)
§V.D: linear-communication classical protocols suffice: Multipartite adaptive LOPC capacity with Eve transcripts and full-l1 secrecy (hard)
Example 2 / equations (89)–(90): total intrinsic information bounds classical key: Multipartite adaptive LOPC capacity with Eve transcripts and full-l1 secrecy (hard)
Example 3 / equations (91)–(92): dual intrinsic information bounds classical key: Multipartite adaptive LOPC capacity with Eve transcripts and full-l1 secrecy (hard)
§VI: arbitrary convex extension-set claim (source ambiguity): Admissibility and local-operation/flag closure of an arbitrary convex extension family (source-ambiguity)
§VI: regularized mixed roof of I_c upper-bounds key: Multipartite I_c and private-state normalization of its regularized mixed roof (source-ambiguity)

Selected references

Squashed entanglement for multipartite states and entanglement measures based on the mixed convex roof, arXiv:0704.2236v3, https://arxiv.org/abs/0704.2236v3

31 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

Ramp-up of Hawking radiation in Bose-Einstein condensate analogue black holesResearch Paper

Motivation

Inspired by a recent experiment by Steinhauer and co-workers, we present a simple model which describes the formation of an acoustic black hole in a Bose-Einstein condensate, allowing an analytical computation of the evolution in time of the corresponding density-density correlator. We show the emergence of analog Hawking radiation out of a "quantum atmosphere" region significantly displaced from the horizon. This is quantitatively studied both at $T=0$ and even in the presence of an initial temperature T, as is always the case experimentally.

This mission is the statement-level formalization of Ramp-up of Hawking radiation in Bose-Einstein condensate analogue black holes (arXiv:2005.04443v3). 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 Sonic horizon and the two flow regions (Following (4), PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

Abstract and conclusion: Spatial origin in a significantly displaced quantum atmosphere (source-ambiguity)
Figures 2--4 and accompanying discussion: Vacuum ramp-up and finite-distance valley location (source-ambiguity)
Text following Figure 4: Length of the observed peak (source-ambiguity)
Comparison at T=TH following (20): Noticeable difference between T=TH and vacuum evolution (source-ambiguity)
Figure 5 and accompanying text: Finite-time appearance and thermal ramp-up delay (source-ambiguity)
Prose after incoming stationary-limit discussion: Positive thermal incoming contribution and smaller-than-outgoing comparison (source-ambiguity)
Example x=-xp=10 and following sentence: Smallness and one-order-of-magnitude thermal comparison (source-ambiguity)
Conclusion, reported onset scales: Observed onset times and atmosphere distance (source-ambiguity)

Selected references

Ramp-up of Hawking radiation in Bose-Einstein condensate analogue black holes, arXiv:2005.04443v3, https://arxiv.org/abs/2005.04443v3

11 thms2 active usersReviewed

Completed

Quantum Information·Captain: Goku

A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOLResearch Paper

Motivation

We formalize a multivariate quantifier elimination (QE) algorithm in the theorem prover Isabelle/HOL. Our algorithm is complete, in that it is able to reduce any quantified formula in the first-order logic of real arithmetic to a logically equivalent quantifier-free formula. The algorithm we formalize is a hybrid mixture of Tarski's original QE algorithm and the Ben-Or, Kozen, and Reif algorithm, and it is the first complete multivariate QE algorithm formalized in Isabelle/HOL.

This mission is the statement-level formalization of A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL (arXiv:2209.10978v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The coefficient-sum conversion equals the canonical univariate conversion (§3.3: lemma multivar_as_univar, PDF p. 11). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

Abstract / §§2.3, 5: complete multivariate real quantifier elimination: construct_NofI_M / construct_NofI_R (source-ambiguity)
§2.2.1: lemma multiv_tarski_query_correct: construct_NofI_M / construct_NofI_R (source-ambiguity)
§2.2.1: lemma multiv_tarski_queries_complete: construct_NofI_M / construct_NofI_R (source-ambiguity)
§2.2.2: lemma multivariate_calculate_data_correct: calculate_data_assumps_M / calculate_data_R (source-ambiguity)
§2.2.2: lemma multivariate_calculate_data_complete: calculate_data_assumps_M / calculate_data_R (source-ambiguity)
§2.3: theorem qe_correct: construct_NofI_M / construct_NofI_R (source-ambiguity)
§2.3: theorem qe_complete: construct_NofI_M / construct_NofI_R (source-ambiguity)
§2.1: exhaustive sign determination with limit samples (unnumbered main subresult): sign_determination / poly_p_in_branch / qe (source-ambiguity)
§2.2.2: size bound for the reduced multivariate matrix (unnumbered): Reduced multivariate matrix size (source-ambiguity)
§3.2: custom induction theorem spmods_multiv_aux_induct (named but not stated): spmods_multiv_aux_induct (source-ambiguity)

Selected references

A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL, arXiv:2209.10978v2, https://arxiv.org/abs/2209.10978v2

4 thms2 active usersReviewed

Quantum Information·Captain: Goku

Trace-Class and Nuclear OperatorsResearch Paper

Motivation

This paper explores the long journey from projective tensor products of a pair of Banach spaces, passing through the definition of nuclear operators still on the realm of projective tensor products, to the of notion of trace-class operators on a Hilbert space, and shows how and why these concepts (nuclear and trace-class operators, that is) agree in the end.

This mission is the statement-level formalization of Trace-Class and Nuclear Operators (arXiv:2204.06954v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

17 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Trace-class and nuclear operators coincide isometrically (§6, Theorem 6.1: trace-class equals nuclear, with equality of norms, PDF p. 17). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

§3, Theorem 3.1 (Grothendieck): countable projective representations: Completed projective tensor space with canonical pure tensors, actual convergence, and the projective norm (hard)
§3, Theorem 3.2: Universal Mapping Principle: Canonical restriction and extension isometry for the binary completed projective tensor product (hard)
§4, Theorem 4.1: canonical contraction, nuclear range, nuclear norm: Canonical completed-projective realization K and its quotient/range nuclear norm (hard)
§4 opening, unnumbered completed-projective embedding claim: Valid injectivity hypotheses for the completed projective realization map (source-ambiguity)
§4, Theorem 4.1(a), exact operator norm subclause: Nontriviality hypotheses for the exact norm-one subclause (source-ambiguity)
§4, Corollary 4.3(a): adjoint of a series representation: A convergence guard for termwise adjoints of a pointwise rank-one series (source-ambiguity)
§5, Remark 5.4(c): claimed failure of the converse to (b): A field-sensitive correction of the claimed every-basis diagonal counterexample (source-ambiguity)
§5, unnumbered printed trace-square display: Correct modulus parentheses and a finite trace-norm domain (source-ambiguity)

Selected references

Trace-Class and Nuclear Operators, arXiv:2204.06954v2, https://arxiv.org/abs/2204.06954v2

18 thms2 active usersReviewed

Quantum Information·Captain: Goku

Optimal quantum tomography for states, measurements, and transformationsResearch Paper

Motivation

We present the first complete optimization of quantum tomography, for states, POVMs, and various classes of transformations, for arbitrary prior ensemble and arbitrary representation, giving corresponding feasible experimental schemes.

This mission is the statement-level formalization of Optimal quantum tomography for states, measurements, and transformations (arXiv:0806.1172v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

17 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Optimal full-operation tomography: global lower bound and attainment ((34), first line; (36), PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

Final paragraph, claimed state eta: A consistent normalization for the asserted state-tomography eta (source-ambiguity)
Final paragraph, claimed POVM eta: A whole-POVM prior and definition of aggregate loss in the output-dimension-one limit (source-ambiguity)
Paragraph beginning With the same derivation: Rectangular analogue of the symmetric optimization data and explicit optimum (source-ambiguity)

Selected references

Optimal quantum tomography for states, measurements, and transformations, arXiv:0806.1172v1, https://arxiv.org/abs/0806.1172v1

21 thms2 active usersReviewed

Quantum Information·Captain: Goku

Covariant Quantum Dynamical Semigroups: Unbounded generatorsResearch Paper

Motivation

A survey of the probabilistic approaches to quantum dynamical semigroups with unbounded generators is given. An emphasis is made upon recent advances in the structural theory of covariant Markovian master equations. The relations with the classical Levy-Khinchin formula are elucidated. As an example, a complete characterizations of the Galilean covariant irreversible quantum Markovian evolutions is given in terms of the corresponding quantum master and Langevin equations. Important topics for future investigation are outlined.

This mission is the statement-level formalization of Covariant Quantum Dynamical Semigroups: Unbounded generators (arXiv:quant-ph/9701037v1). 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 Minimal backward dynamical-semigroup solution (§2: existence and CP-order minimality of the backward solution, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

Theorem 2: Galilean generator classification, common core and uniqueness (seed pinned from summary): Theorem 2: Galilean generator classification, common core and uniqueness (seed pinned from summary) (source-ambiguity)
§2: equivalence of matrix-element differentiability and rank-one generator domain: Full trace-class predual, trace-norm right-limit generator and rank-one span (hard)
§2: trace-norm core implies uniqueness of the backward master equation: Trace-norm graph core of the actual preadjoint generator (hard)
§2: forward equation and minimality under adjoint summability: Unbounded adjoint domains, square-summable noise adjoints, and forward trace-class weak equation (hard)
§3: Levy translation average is unital and has generator (20): Schroedinger momentum domain, real Levy laws, scalar expectation and weak generator integrals (hard)
§3: printed boundedness criterion after (20): §3: printed boundedness criterion after (20) (source-ambiguity)
§3: momentum/space covariance and classical fixed-algebra restriction: Bounded-Borel multiplication functional calculus and classical Levy restriction generator (hard)
§3: general half-line form (22), covariance and classical diffusion restriction: §3: general half-line form (22), covariance and classical diffusion restriction (source-ambiguity)
§3: killed half-line Brownian minimal solution is nonunital and nonunique: Dirichlet half-line realization, killed-Brownian multiplication restriction, and distinct weak-equation extensions (hard)
Theorem 1: covariant gauge representation and its continuity criterion: Theorem 1: covariant gauge representation and its continuity criterion (source-ambiguity)
§4: compact-group covariant splitting of the form-generator: §4: compact-group covariant splitting of the form-generator (source-ambiguity)
§5: classical Levy-driven Langevin dilation and random-unitary representation: §5: classical Levy-driven Langevin dilation and random-unitary representation (source-ambiguity)
§6: formal quantum-noise Langevin dilation example: §6: formal quantum-noise Langevin dilation example (source-ambiguity)
§6: classical dissipative stochastic representation of the minimal evolution: §6: classical dissipative stochastic representation of the minimal evolution (source-ambiguity)

Selected references

Covariant Quantum Dynamical Semigroups: Unbounded generators, arXiv:quant-ph/9701037v1, https://arxiv.org/abs/quant-ph/9701037v1

6 thms2 active usersReviewed

Quantum Information·Captain: Goku

One-mode Bosonic Gaussian channels: a full weak-degradability classificationResearch Paper

Motivation

A complete degradability analysis of one-mode Gaussian Bosonic channels is presented. We show that apart from the class of channels which are unitarily equivalent to the channels with additive classical noise, these maps can be characterized in terms of weak- and/or anti-degradability. Furthermore a new set of channels which have null quantum capacity is identified. This is done by exploiting the composition rules of one-mode Gaussian maps and the fact that anti-degradable channels can not be used to transfer quantum information.

This mission is the statement-level formalization of One-mode Bosonic Gaussian channels: a full weak-degradability classification (arXiv:quant-ph/0609013v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

20 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Full weak-degradability classification outside B2 (Abstract; §3.2; Fig.2, PDF p. 15). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

§3.2, cited B2 assertion: A correct noise-dependent replacement for the cited universal B2 non-anti-degradability assertion. (source-ambiguity)

Selected references

One-mode Bosonic Gaussian channels: a full weak-degradability classification, arXiv:quant-ph/0609013v2, https://arxiv.org/abs/quant-ph/0609013v2

27 thms2 active usersReviewed

Quantum Information·Captain: Goku

A strong converse for classical channel coding using entangled inputsResearch Paper

Motivation

A fully general strong converse for channel coding states that when the rate of sending classical information exceeds the capacity of a quantum channel, the probability of correctly decoding goes to zero exponentially in the number of channel uses, even when we allow code states which are entangled across several uses of the channel. Such a statement was previously only known for classical channels and the quantum identity channel. By relating the problem to the additivity of minimum output entropies, we show that a strong converse holds for a large class of channels, including all unital qubit channels, the d-dimensional depolarizing channel and the Werner-Holevo channel. This further justifies the interpretation of the classical capacity as a sharp threshold for information-transmission.

This mission is the statement-level formalization of A strong converse for classical channel coding using entangled inputs (arXiv:0903.2838v1). 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 Main result: exponential unassisted strong converse for the listed channel classes (Main result: exponential unassisted strong converse for the listed channel classes, 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.

Deferred results

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

Lemma II.10, Eq.(26): Nonempty-set and attainment hypotheses, or an explicitly chosen infimum/supremum formulation, for the arbitrary-set radius statement. (source-ambiguity)

Selected references

A strong converse for classical channel coding using entangled inputs, arXiv:0903.2838v1, https://arxiv.org/abs/0903.2838v1

22 thms2 active usersReviewed

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

Constructing algebraic Lie algebrasResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Quantum communication using a bounded-size quantum reference frameResearch Paper

Motivation

What is formalized

Deferred results

Selected references

A non-smooth continuous unitary representation of a Banach-Lie groupResearch Paper

Motivation

What is formalized

Selected references

Towards a Lie theory for locally convex groupsResearch Paper

Motivation

What is formalized

Deferred results

Selected references

The weighted hook length formulaResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Unbounded generators of dynamical semigroupsResearch Paper

Motivation

What is formalized

Deferred results

Selected references

On Analytic Vectors for Unitary Representations of Infinite Dimensional Lie GroupsResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Energy-constrained diamond norms and their use in quantum information theoryResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Minimal computational-space implementation of multi-round quantum protocolsResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Structure of H-(co)module Lie algebrasResearch Paper

Motivation

What is formalized

Deferred results

Selected references

On the Fundamental Principles of Unbounded Functional CalculiResearch Paper

Motivation

What is formalized

Deferred results

Selected references

The entropy power inequality for quantum systemsResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Canonical idempotents of multiplicity-free families of algebrasResearch Paper

Motivation

What is formalized

Deferred results

Selected references

The Capacity of Symmetric Private Information RetrievalResearch Paper

Motivation

What is formalized

Selected references

Classification of 3-graded causal subalgebras of real simple Lie algebrasResearch Paper

Motivation

What is formalized

Deferred results

Selected references

A Practical Quantum Algorithm for the Schur TransformResearch Paper