How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Vacuum emission Dyson convergence
Statement
Assume the Axiom of Countable Choice and the Axiom of Choice (The Axiom of Countable Choice (), The Axiom of Choice). Adopt the objects and hypotheses of Cutoff dipole relative bound: , Hermitian matrices on , cutoff , transverse vectors with and , coupling , all with domain so that and are self-adjoint on that domain. Fix , a unit vector and , and define the interaction-picture family For and let (iterated Bochner integral in ; ). Put and . Then:
(a) for all and ,
(b) the vectors lie in , the series converges in the graph norm of uniformly for in compact subsets of , and its sum satisfies
(c) the Dyson sum solves the actual self-adjoint evolution: for every ;
(d) explicit tail bound: for and ,
The convergence is proved for the actual self-adjoint on the stated domain; this is not a formal manipulation of divergent series, and no all-time weak-coupling, Markov or exponential-decay statement is made.
Facts & Assumptions
Given: the cutoff data, self-adjoint on , , , , , and the vacuum initial vector. Put ; let be the closed subspace with photon numbers at most , including the atomic factor, and . Define the coupling-independent constant , so .
The cutoff relative-bound theorem gives symmetry of , its relative bound zero, and self-adjointness of on (Cutoff dipole relative bound (a)-(c)). In particular is bounded for the graph norm, where ; since is bounded, the two graph norms are equivalent.
The sector formulas give on , and each changes photon number by one; their sum has bound (Closed adjoint sector domains (b),(c), Creation contraction bounds (a),(b)). Contraction is conjugate-linear in its vector argument and satisfies .
The free field operator is the positive closed sector sum with multiplier , and . Its sector projections commute with its unitary group (Transverse continuum free Fock Hamiltonian (a)-(c)). The Euclidean product identification, tensor density and permutation formulas are Euclidean L² product unitary: L²(R^a)⊗̂L²(R^b) ≅ L²(R^{a+b}), Hilbert tensor construction: inner product, completion and product bases and Permutation sector projections on the n-fold tensor power. AC supplies any DC prerequisite of the free-field supplier (AC implies DC implies countable choice).
A finite Hermitian matrix has an orthonormal eigenbasis (Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely). A self-adjoint operator's unitary group is strongly continuous, preserves its domain and commutes with it, and is differentiable on domain vectors (A self-adjoint operator generates a strongly continuous unitary group).
A continuous Banach-valued curve on a compact interval is Bochner integrable; its primitive has the curve as derivative, including one-sided endpoint derivatives, and the integral obeys the norm bound and linearity (Fundamental theorem of calculus for Banach-valued continuous curves, Bochner integrability criterion, Bochner integral norm inequality, Linearity of the Bochner integral). Bounded linear maps commute with such integrals: this holds for simple approximants by linearity and passes to their limits by the map's norm bound.
Proof
Given: The data of the statement and [F1]-[F5].
[Free flow and vertex bounds] Diagonalizing the finite Hermitian and using [F3], [F4] gives . Thus preserves each , commutes with on , and is isometric and strongly continuous for the graph norm: both and are continuous. On , the finite-sector extension of from [F2] satisfies and takes values in . Its free conjugate therefore satisfies . The factor is included exactly once in this bound; and contain no coupling.
[Cutoff commutator and graph-domain extension] For supported in , and . On symmetric elementary tensors with factors in , the sector multiplier and creation formula give . For contraction the removed factor contributes , so . These identities extend to every finite-photon graph vector, with no claim that all of lies in . Indeed, in sector first cut each mode to ; dominated convergence in the Euclidean representation [F3] gives convergence of both the vector and its energy multiplier. On that cutoff subspace, energy is bounded by , so finite sums of elementary cutoff tensors, symmetrized, approximate in graph norm by tensor density. This supplies a graph core in each . The field and its candidate commutator are bounded on by [F2], with respective bounds and . Applying the core identity to a graph-approximating sequence makes the output and its energy image converge; closedness of proves graph-domain preservation and the identity on the limit. Hence for , and
[Conjugated commutator and graph continuity] Since commutes with , step 1.2 gives on with . The conjugations in are retained. Equivalently, the sector formulas give and , with The same positive phase occurs in the annihilation vector argument because that argument is conjugate-linear, as in [F2]. The resulting graph bound is Thus is uniformly bounded in for these graph norms. Strong graph continuity of , the fixed graph-bounded between these spaces, and the expression show that is graph continuous. On the full , [F1] and the graph isometry of additionally give for one finite independent of , and strong continuity as a map . No global map is asserted.
[Chronological products and their graph bounds] Define , with . At the -th vertex, the earlier product is in , so steps 1.1 and 2.1 give a factor in its Hilbert bound. Consequently and . The graph commutator gives recursively ; since , induction yields . Each product is jointly continuous in its time variables for the graph norm: at each stage use strong graph continuity of the next on a fixed vector and its uniform graph bound to control the changing previous vector. For the Hilbert bound is and the energy bound is , including when .
[Graph Bochner terms and the genuine recurrence] The graph space is Banach: a graph-Cauchy sequence has limits of both the vectors and their images in the Hilbert space, and closedness of identifies them as a graph limit. Each is closed in it. Step 3.1 and [F5] therefore make every iterated chronological integral a Bochner integral in . Its graph and Hilbert norm bounds follow by integrating the preceding product bounds over the simplex; the volume is , obtained recursively from . Each factor of the integral contributes , giving For these bounds mean and . Integrating the latest vertex last gives the actual left-vertex recurrence For fixed , move through the inner integral as a bounded linear map by [F5]; the earlier vertices have times below , with on the left. This also proves graph continuity of each term, and proves (a) and graph-domain membership in (b).
[Uniform graph convergence] Fix and put . The graph majorant is . For the ratio of consecutive scalar terms tends to zero: it is . It is eventually at most , proving convergence by a geometric tail comparison. If , every positive-order term is zero and only the zeroth term remains. Thus the series converges uniformly for in the Banach graph space, and its sum is graph continuous and belongs to .
[Integral equation and Hilbert derivative] The uniform bound from step 2.1 makes converge uniformly in Hilbert norm on to . This limiting curve is continuous by graph continuity of , strong continuity of , and the same uniform bound. Sum the recurrences of step 4.1 and use the Bochner norm inequality [F5] to pass to the limit in their Hilbert integrals. The result is . The Banach-valued fundamental theorem now gives , with the right derivative at zero, and , . Along with step 5.1 this proves (b); graph continuity is used for domain control, while the differential equation is a Hilbert-space derivative.
[Identification with the self-adjoint dynamics] Put . It is graph continuous and belongs to . The difference quotient splits into the difference of the free group on the fixed domain vector and the free group times the difference quotient of , so [F4] and step 6.1 justify the product derivative in Hilbert norm. Thus and . By [F1], [F4], the Stone curve is another strong domain-valued solution because . For their difference , symmetry of gives Both initial values agree, so , proving (c) for every finite .
[Tail, vacuum and zero branches] By step 7.1 and unitarity, the truncation error at time equals in norm the interaction-picture tail, so it is at most ; for this is at most the stated tail, proving (d). The vacuum zeroth term has and norm one. At all positive-order integrals vanish. If , or if (all contributing or zero), then , all positive-order terms vanish, the interaction-picture sum is exactly , and the tail is zero for every . The argument supplies finite-time convergence and the actual self-adjoint evolution, with the original scope limitations retained.
Depends on
Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely
Creation contraction bounds
Euclidean L² product unitary: L²(R^a)⊗̂L²(R^b) ≅ L²(R^{a+b})
Linearity of the Bochner integral
Dominated convergence
Cauchy–Schwarz: , with equality exactly for dependent pairs
AC implies DC implies countable choice
Cutoff dipole relative bound
Closed adjoint sector domains
Transverse continuum free Fock Hamiltonian
Hilbert tensor construction: inner product, completion and product bases
Permutation sector projections on the n-fold tensor power
A self-adjoint operator generates a strongly continuous unitary group
Fundamental theorem of calculus for Banach-valued continuous curves
Bochner integrability criterion
Bochner integral norm inequality
Symmetric, self-adjoint and essentially self-adjoint operators
Adjoint of a densely defined operator
A bounded linear operator between normed spaces
The operator norm as the least bound and as the unit-sphere or unit-ball supremum
Hilbert space
The Axiom of Countable Choice ()
The Axiom of Choice
Dependency tree · 2 levels
Sources
- R. Fitzpatrick, Quantum Mechanics (University of Texas at Austin, author-hosted course text), Time-Dependent Perturbation Theory pp. 175-182 (Dyson series and interaction picture)
- G. Teschl, Mathematical Methods in Quantum Mechanics, 1st edition 2009, Chapter 5 pp. 123-131 (Stone's theorem, unitary dynamics and uniqueness)