Alphabeta Math
Physics theoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass
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.

The Schroedinger-picture flow: unitarity, domain invariance and the domain-qualified equation

Physical scope

A conditional consequence of the state and composition postulate P1 and the autonomous-dynamics postulate P4 for a declared isolated system of the framework: the flow generated by the assigned energy observable is a strongly continuous unitary group, it preserves the operator domain and commutes with the energy there, the Schroedinger equation holds in the norm-differentiable sense exactly on the domain, and the evolution of a density-operator preparation is a trace-one density operator at every time. The item asserts no dynamics for driven or open systems, no measurement or apparatus realization, no isolation claim about any laboratory system and no empirical result; all statements are conditional on P1 and P4 and on the cited mathematics.

Statement

Adopt the state and composition postulate State and composition postulate P1: Hilbert spaces, preparations and composite systems (P1), the observable and probability postulate in the reading of Assigned sharp observables and the outcome law of the framework, and the autonomous-dynamics postulate Autonomous dynamics postulate P4: self-adjoint generators and unitary evolution (P4), and assume the Axiom of Countable Choice and the Axiom of Choice (The Axiom of Countable Choice (ACω), The Axiom of Choice), the choice hypotheses of the cited spectral suppliers. Let H be the state space assigned to a declared isolated system of the massive-matter sector (The state space of the framework: preparations, pure rays and density operators), let (Hop,uH) be its assigned energy observable with spectral projection-valued measure EH (Assigned energy observable, unitary flow and the two pictures of autonomous evolution clause (a)), and let U(t)=exp⁡ ⁣(−iℏtHop)=∫Re−itλ/ℏ dEH(λ),ψ(t):=U(t)ψ(0),ρ(t):=U(t)ρ(0)U(t)∗ be the flow and the state evolutions of clauses (b) and (c) of Assigned energy observable, unitary flow and the two pictures of autonomous evolution, with ℏ>0 and the energy unit in the sense of Dimensions, SI unit conventions and quantity types of the framework. Then:

(a) Unitary flow. U is a strongly continuous one-parameter unitary group (Strongly continuous one-parameter unitary group) with U(0)=I, U(t+s)=U(t)U(s) and U(t)∗=U(t)−1=U(−t); every orbit has constant norm, ∥ψ(t)∥=∥ψ(0)∥, so for ψ(0)≠0 the ray [ψ(t)] is a pure preparation of the model for every t (The state space: density operators, pure and mixed states, and purity).

(b) Domain invariance. U(t)D(Hop)=D(Hop) for every t and HopU(t)=U(t)Hop on D(Hop): the flow preserves the energy domain and commutes with the energy there.

(c) Schroedinger equation on the domain. For ψ(0)∈D(Hop) the curve t↦ψ(t) is norm-differentiable at every t∈R, it stays in D(Hop), and iℏ ddtψ(t)=Hopψ(t)=HopU(t)ψ(0); for ψ(0)∈H∖D(Hop) the curve is norm-differentiable at no t∈R, so the equation is not asserted there, although the evolution t↦ψ(t) remains continuous.

(d) Density-operator evolution. For every preparation ρ (The state space of the framework: preparations, pure rays and density operators) and every t the operator ρ(t)=U(t)ρ(0)U(t)∗ is again a preparation: self-adjoint, positive, trace class with tr⁡ρ(t)=1 (Trace class operator, Self-adjoint, positive, unitary and normal operators). Moreover for every bounded operator B the identity tr⁡(ρ(t)B)=tr⁡(ρ(0)U(t)∗BU(t)) holds.

(e) Status. Clauses (a)-(d) are conditional consequences of P1 and P4 and the cited mathematics. They assert no evolution for a prescribed time-dependent Hamiltonian, no non-unitary reduced dynamics, no measurement, apparatus or detector model, no claim that any laboratory system is isolated, and no empirical result.

Facts & Assumptions

Given: The adopted postulates P1 and P4 (State and composition postulate P1: Hilbert spaces, preparations and composite systems, Autonomous dynamics postulate P4: self-adjoint generators and unitary evolution); the Axiom of Countable Choice and the Axiom of Choice; the assigned energy observable (Hop,uH) with PVM EH and flow U(t) of Assigned energy observable, unitary flow and the two pictures of autonomous evolution; the state space D(H) of The state space of the framework: preparations, pure rays and density operators; a vector ψ(0)∈H; a preparation ρ; a bounded operator B.

[F1]

P4, read through the definition. Clause (i) of P4 assigns the energy operator: Hop is self-adjoint with a declared energy unit; clause (ii) fixes U(t)=exp⁡(−itHop/ℏ) as the strongly continuous unitary group generated by it, with D(T)=D(Hop) for T=−Hop/ℏ; clause (iii) fixes ψ(t)=U(t)ψ(0) and ρ(t)=U(t)ρ(0)U(t)∗ and states the Schroedinger equation as holding exactly for initial vectors in D(Hop) (Autonomous dynamics postulate P4: self-adjoint generators and unitary evolution clauses (i)-(iii), Assigned energy observable, unitary flow and the two pictures of autonomous evolution clauses (a)-(c)).

[F2]

Flow calculus. For the self-adjoint T=−Hop/ℏ with U(t)=eitT: U is a strongly continuous one-parameter unitary group with U(t)D(T)=D(T) and TU(t)=U(t)T on D(T); for u∈D(T) the curve t↦U(t)u is differentiable at every t with derivative iU(t)Tu=iTU(t)u; for u∉D(T) it is differentiable at no point (Flow calculus of a self-adjoint generator: commutation, invariance and differentiability clauses (a) and (c), A self-adjoint operator generates a strongly continuous unitary group).

[F3]

P1, read through the state-space vocabulary. Pure preparations are the unit rays of the assigned Hilbert space and general preparations are exactly the states ρ∈D(H): self-adjoint positive trace-class operators with trace one (State and composition postulate P1: Hilbert spaces, preparations and composite systems clauses (ii)-(iii), The state space of the framework: preparations, pure rays and density operators, The state space: density operators, pure and mixed states, and purity, Density operators and scalar spectral probability clause (a)).

[F4]

Trace-class calculus. The trace-class operators form a two-sided operator ideal, so UρU∗ is trace class for a preparation ρ and a unitary U; the trace is linear and cyclic, tr⁡(SA)=tr⁡(AS) for trace-class S and bounded A (Trace class is a two sided Banach operator ideal, Nuclear bounded cyclicity for trace-class operators clause (b)); a self-adjoint operator B is positive exactly when ⟨Bx,x⟩≥0 for all x (Self-adjoint, positive, unitary and normal operators).

Proof

technique · direct; translate P4 into the mathematical generator $T=-H_{\mathrm{op}}/\hbar$, apply the flow calculus of [Flow calculus of a self-adjoint generator: commutation, invariance and differentiability](/physics/item/lem-nrqm-autonomous-dynamics-flow-calculus), and verify the density-operator claims with the trace-class calculus

Given: P1, P4, the assigned energy observable (Hop,uH), its flow U(t), a vector ψ(0), a preparation ρ, a bounded operator B, and [F1]-[F4].

1.1givenF1F2F3algebra

[The flow and the orbits] Put T:=−Hop/ℏ, a self-adjoint operator with D(T)=D(Hop); by clause (b) of Assigned energy observable, unitary flow and the two pictures of autonomous evolution the flow is U(t)=eitT. By [F2], U is a strongly continuous one-parameter unitary group with the displayed inverse and group laws, and ∥ψ(t)∥=∥U(t)ψ(0)∥=∥ψ(0)∥ because U(t) is unitary. If ψ(0)≠0 then ψ(t)≠0, and by the normalization clause (ii) of P1 (State and composition postulate P1: Hilbert spaces, preparations and composite systems) the unit ray [ψ(t)] is a pure preparation; this is (a).

1.2givenF1F2algebra

[Domain invariance] D(Hop)=D(T) and Hop=−ℏT, so the invariance U(t)D(T)=D(T) and the commutation TU(t)=U(t)T on D(T) of [F2] read as U(t)D(Hop)=D(Hop) and HopU(t)=U(t)Hop on D(Hop); this is (b).

1.3givenF3F4algebra

[Preparations evolve to preparations] Let ρ be a preparation, so ρ is self-adjoint, positive and trace class with tr⁡ρ=1 by [F3]. Then ρ(t)=U(t)ρU(t)∗ is trace class by the ideal property of [F4]. It is self-adjoint because ρ(t)∗=U(t)ρ∗U(t)∗=ρ(t); it is positive because ⟨ρ(t)x,x⟩=⟨ρ U(t)∗x,U(t)∗x⟩≥0 for every x, using positivity of ρ and unitarity of U(t); and its trace is tr⁡ρ(t)=tr⁡(U(t)ρU(t)∗)=tr⁡(ρU(t)∗U(t))=tr⁡ρ=1, where the second equality is trace cyclicity from [F4] applied to the trace-class operator ρU(t)∗ and the bounded operator U(t). Hence ρ(t) is again a preparation.

2.1givenstep 1.2F2algebra

[Schroedinger equation] Let ψ(0)∈D(Hop)=D(T). By [F2] the curve is differentiable at every t with ddtψ(t)=iU(t)Tψ(0), and ψ(t)=U(t)ψ(0)∈D(T)=D(Hop) by step 1.2. Substituting T=−Hop/ℏ and using the commutation of step 1.2 gives iℏddtψ(t)=iℏ⋅iU(t)Tψ(0)=−ℏU(t)(−1ℏHop)ψ(0)=U(t)Hopψ(0)=HopU(t)ψ(0)=Hopψ(t).

2.2givenstep 1.3F4algebra

[Two-picture statistics identity] For bounded B, cyclicity from [F4] applied to the trace-class operator ρU(t)∗B and the bounded operator U(t) gives tr⁡(ρ(t)B)=tr⁡(U(t)ρU(t)∗B)=tr⁡(ρU(t)∗BU(t)), which is the displayed identity of (d).

3.1givenstep 2.1F2

[Outside the domain] If ψ(0)∈H∖D(Hop)=H∖D(T), then by [F2] the curve t↦U(t)ψ(0) is differentiable at no point of R; this completes (c).

4.1step 1.1step 1.2step 2.1step 3.1step 1.3step 2.2∎

Steps 1.1, 1.2, 2.1, 3.1, 1.3 and 2.2 establish (a)-(d); clause (e) records what the statement does not assert, in agreement with clauses (iv) and (v) of P4.

Remarks

  • Isolated idealization. P4 is adopted only for an isolated autonomous system; the model equation (c) is a statement about the model's evolution operator, not evidence that a given laboratory system is isolated.
  • No state reduction. Nothing in this item is a measurement postulate: the evolution ρ↦UρU∗ is applied to a preparation, and no outcome, apparatus or conditioning is introduced.

Depends on

Dependency tree · 2 levels

Sources