ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generated

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.

A coherent-state trajectory: period, phase-space ellipse and constant spreads

Physical scope

The trajectory of a coherent preparation of the one-dimensional oscillator model with nonzero label: the exact period 2 pi/omega of the preparation, the quarter-period phase-space values, the invariant ellipse of the preparation means, and the constancy of the position and momentum spreads and their product hbar/2. The example is a conditional computation inside the adopted model; the mean values are preparation means and are not the coordinates of a measured particle trajectory.

Example

Adopt the state and composition postulate P1, the observable and probability postulate P2, the autonomous-dynamics postulate P4 and the kinematics and massive-particle model postulate P5, read through the one-dimensional oscillator model of The quadratic-potential oscillator model of the framework clauses (a), (b), (c), and the coherent-state family of The coherent states of the oscillator model; assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Fix a label $z = z_{1} + i z_{2}$ with $∣ z ∣ > 0$ , let $x_{0} : = \sqrt{2} ℓ z_{1}$ , $p_{0} : = \frac{\sqrt{2} ℏ}{ℓ} z_{2}$ , let $Ψ_{z} (t) : = U (t) Ψ_{z}$ be the evolved coherent state, and write $x (t) : = ⟨ Q Ψ_{z} (t), Ψ_{z} (t) ⟩$ , $p (t) : = ⟨ P Ψ_{z} (t), Ψ_{z} (t) ⟩$ . Then:

(a) the preparation is periodic with period $\frac{2 π}{ω}$ in the sense that the prepared state is the same pure preparation at times $t$ and $t + \frac{2 π}{ω}$ : $[U (2 π / ω) Ψ_{z}] = [Ψ_{z}], [Ψ_{z} (t + 2 π / ω)] = [Ψ_{z} (t)] (t \in R);$

(b) the mean pair is $x (t) = x_{0} \cos ω t + \frac{p_{0}}{m ω} \sin ω t, p (t) = p_{0} \cos ω t - m ω x_{0} \sin ω t,$ so that $x (0) = x_{0}$ , $p (0) = p_{0}$ , and at the quarter period $x (\frac{π}{2 ω}) = \frac{p_{0}}{m ω}$ , $p (\frac{π}{2 ω}) = - m ω x_{0}$ ; the phase-space ellipse $\frac{x (t)^{2}}{2 ℓ^{2}} + \frac{ℓ^{2} p (t)^{2}}{2 ℏ^{2}} = ∣ z ∣^{2}$ is invariant along the motion;

(c) the position and momentum spreads and their product are constant along the motion: $Δ_{Ψ_{z} (t)} Q = \frac{ℓ}{\sqrt{2}}, Δ_{Ψ_{z} (t)} P = \frac{ℏ}{ℓ \sqrt{2}}, Δ_{Ψ_{z} (t)} Q Δ_{Ψ_{z} (t)} P = \frac{ℏ}{2} (t \in R);$

(d) the displayed $x (t)$ and $p (t)$ are preparation means of the model's position and momentum observables in the evolving coherent preparation; they are not the coordinates of a measured particle trajectory, and no measurement record, apparatus or empirical value is asserted.

Facts & Assumptions

Given: the one-dimensional oscillator model with parameters $m, ω, ℏ > 0$ and length $ℓ$ ; the coherent states $Ψ_{z}$ and their evolution $Ψ_{z} (t) = U (t) Ψ_{z}$ ; the label $z = z_{1} + i z_{2} \neq 0$ and the numbers $x_{0} = \sqrt{2} ℓ z_{1}$ , $p_{0} = \frac{\sqrt{2} ℏ}{ℓ} z_{2}$ ; a real time $t$ .

[F1]

Coherent evolution and its statistics. For every $w \in C$ and $s \in R$ , $U (s) Ψ_{w} = e^{- i ω s / 2} Ψ_{w e^{- i ω s}}$ ; the preparation means of the evolved coherent preparation are $⟨ Q ⟩_{w (s)} = \sqrt{2} ℓ Re w (s)$ , $⟨ P ⟩_{w (s)} = \frac{\sqrt{2} ℏ}{ℓ} Im w (s)$ with $w (s) = w e^{- i ω s}$ ; and $Δ_{Ψ_{w (s)}} Q = ℓ / \sqrt{2}$ , $Δ_{Ψ_{w (s)}} P = ℏ / (ℓ \sqrt{2})$ with product $ℏ / 2$ (Evolution of the oscillator coherent states: classical mean motion and stationary fluctuations clauses (a), (b), (c); Fluctuations of the oscillator coherent states and the position-momentum relation of the model clauses (a), (b)).

[F2]

Trigonometric identities. For real $θ$ , $e^{- i θ} = \cos θ - i \sin θ$ , $\cos^{2} θ + \sin^{2} θ = 1$ , $\cos 0 = 1$ , $\sin 0 = 0$ , $\cos \frac{π}{2} = 0$ , $\sin \frac{π}{2} = 1$ , and $e^{- 2 π i} = 1$ ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ , Pythagorean and parity identities for all six trigonometric functions on their natural domains, Quarter-turn values and shifts by pi/2 and pi).

[F3]

Spread reading. The preparation spreads in [F1] are the outcome-law spreads of the assigned observables $(Q, m)$ and $(P, k g m s^{- 1})$ in the reading of Preparation variance and spread of an assigned sharp observable clauses (b), (c), and the means are the outcome-law means of Evolution of the oscillator coherent states: classical mean motion and stationary fluctuations clause (b).

Verification

Given: the data of the Example and [F1]-[F3].

1.1givenF1

[The evolved family] By [F1] applied with $w = z$ and $s = t$ , $Ψ_{z} (t) = U (t) Ψ_{z} = e^{- i ω t / 2} Ψ_{z (t)}$ with $z (t) = z e^{- i ω t}$ , and the means and spreads of the evolved preparation are those of the coherent label $z (t)$ .

1.2givenF2

[The complex label in real form] By [F2], $e^{- i ω t} = \cos ω t - i \sin ω t$ , so $z (t) = z (\cos ω t - i \sin ω t)$ has real part $z_{1} \cos ω t + z_{2} \sin ω t$ and imaginary part $z_{2} \cos ω t - z_{1} \sin ω t$ , and $\cos^{2} ω t + \sin^{2} ω t = 1$ ; also $e^{- 2 π i} = 1$ .

2.1step 1.1step 1.2F2

[Clause (a)] By step 1.1 and [F2], $z (t + 2 π / ω) = z e^{- i ω t} e^{- 2 π i} = z (t)$ and $e^{- i ω (t + 2 π / ω) / 2} = e^{- i ω t / 2} e^{- i π} = - e^{- i ω t / 2}$ , so $U (2 π / ω) Ψ_{z} = - Ψ_{z}$ ; a global phase does not change the pure preparation, hence $[U (2 π / ω) Ψ_{z}] = [Ψ_{z}]$ and $[Ψ_{z} (t + 2 π / ω)] = [Ψ_{z} (t)]$ for every $t$ .

2.2step 1.1step 1.2F1F2algebra

[Clause (b)] By step 1.1 and [F1], $x (t) = \sqrt{2} ℓ Re z (t)$ and $p (t) = \frac{\sqrt{2} ℏ}{ℓ} Im z (t)$ ; substituting the real and imaginary parts of step 1.2 and using $x_{0} = \sqrt{2} ℓ z_{1}$ , $\frac{p_{0}}{m ω} = \frac{\sqrt{2} ℏ z_{2}}{ℓ m ω} = \sqrt{2} ℓ z_{2}$ , $m ω x_{0} = \sqrt{2} m ω ℓ z_{1} = \frac{\sqrt{2} ℏ z_{1}}{ℓ}$ by $ℓ^{2} = ℏ / (m ω)$ gives the two displayed closed forms; at $t = 0$ they read $x_{0}, p_{0}$ , and at $t = \frac{π}{2 ω}$ they read $\frac{p_{0}}{m ω}$ and $- m ω x_{0}$ by the values in [F2]. For the ellipse, the closed forms give $\frac{x (t)^{2}}{2 ℓ^{2}} = (z_{1} \cos ω t + z_{2} \sin ω t)^{2}$ and $\frac{ℓ^{2} p (t)^{2}}{2 ℏ^{2}} = (z_{2} \cos ω t - z_{1} \sin ω t)^{2}$ ; adding, the cross terms cancel and $\cos^{2} ω t + \sin^{2} ω t = 1$ gives the sum $z_{1}^{2} + z_{2}^{2} = ∣ z ∣^{2}$ for every $t$ .

2.3step 1.1F1

[Clause (c)] By step 1.1 the evolved preparation is the coherent preparation of label $z (t)$ , so [F1] gives $Δ_{Ψ_{z} (t)} Q = ℓ / \sqrt{2}$ , $Δ_{Ψ_{z} (t)} P = ℏ / (ℓ \sqrt{2})$ and product $ℏ / 2$ for every $t$ .

3.1step 2.1step 2.2step 2.3F3∎

[Clause (d)] By [F3] the quantities $x (t)$ , $p (t)$ are outcome-law means of the model's position and momentum observables in the evolving preparation, and the spreads are outcome-law spreads; no measurement record, apparatus model or empirical value entered the computation.

A coherent-state trajectory: period, phase-space ellipse and constant spreads

Example

Facts & Assumptions

Verification

Depends on

Dependency tree · 2 levels

Sources