ExampleConstruction: AI-adaptedVerification: 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.

Precession of a two-level preparation: exact phases, probabilities and a Bloch-vector rotation

Physical scope

A finite, exact model computation in the two-level state space of the framework: the assigned energy observable with two distinct energies in joules, its unitary flow, the exact evolution of a pure preparation, the outcome laws and expectations of three bounded self-adjoint observables, the resulting rotation of the expectation-value triple, and the explicit period of the laws. The energies are model parameters; the item asserts no apparatus realization, no detection model and no empirical value, and it identifies the two-level system with no specific physical species.

Example

Let $H = C^{2}$ carry the standard inner product $⟨ z, w ⟩ = z_{1} \overline{w_{1}} + z_{2} \overline{w_{2}}$ (Real and complex inner product spaces, with the inner product linear in the first argument, Hilbert space, The induced length is a norm), with orthonormal basis $u_{1} = (1, 0)$ , $u_{2} = (0, 1)$ and rank-one calculus $T_{u, v} x = ⟨ x, v ⟩ u$ (Rank-one operator calculus). Fix two distinct energies $E_{1} \neq E_{2}$ in joules (model parameters, not measured values), and consider the assigned energy observable of Assigned energy observable, unitary flow and the two pictures of autonomous evolution clause (a), $H_{o p} : = E_{1} T_{u_{1}, u_{1}} + E_{2} T_{u_{2}, u_{2}}, u_{H} = J,$ of an isolated system whose state space is the two-level state space of The state space of the framework: preparations, pure rays and density operators. Define the bounded self-adjoint observables $X : = T_{u_{1}, u_{2}} + T_{u_{2}, u_{1}}, Y : = i T_{u_{2}, u_{1}} - i T_{u_{1}, u_{2}}, Z : = T_{u_{1}, u_{1}} - T_{u_{2}, u_{2}},$ with the same dimensionless unit, and let $ψ_{0} = α u_{1} + β u_{2}$ be a unit vector. Writing $ω : = \frac{E_{2} - E_{1}}{ℏ} (units s^{- 1}),$ the example establishes the following exact model statements.

(i) The spectral projection-valued measure of $H_{o p}$ is $E_{H} (B) = 1_{E_{1} \in B} T_{u_{1}, u_{1}} + 1_{E_{2} \in B} T_{u_{2}, u_{2}}$ , and the flow is $U (t) = e^{- i E_{1} t / ℏ} T_{u_{1}, u_{1}} + e^{- i E_{2} t / ℏ} T_{u_{2}, u_{2}}$ .

(ii) $X, Y, Z$ are bounded self-adjoint with $X^{2} = Y^{2} = Z^{2} = I$ and $X Y = i Z$ ; their spectra are ${\pm 1}$ , with $Y$ and $Z$ obtained from $X$ by the same pattern.

(iii) The evolved preparation is $ψ (t) = U (t) ψ_{0} = α e^{- i E_{1} t / ℏ} u_{1} + β e^{- i E_{2} t / ℏ} u_{2}$ , of unit norm, and the expectations are $⟨ X ⟩ (t) = 2 Re (α \overline{β} e^{i ω t}), ⟨ Y ⟩ (t) = - 2 Im (α \overline{β} e^{i ω t}), ⟨ Z ⟩ (t) = ∣ α ∣^{2} - ∣ β ∣^{2} .$

(iv) The triple $v (t) : = (⟨ X ⟩ (t), ⟨ Y ⟩ (t), ⟨ Z ⟩ (t)) \in R^{3}$ has constant norm one and is the rotation of $v (0)$ about the third axis by the angle $- ω t$ : $v (t) = R_{3} (- ω t) v (0)$ , where $R_{3} (θ) (x, y, z) = (x \cos θ - y \sin θ, x \sin θ + y \cos θ, z)$ . Thus the expectation-value triple precesses with angular frequency $ω$ .

(v) The outcome law of $X$ in the preparation $[ψ (t)]$ is the two-point law $μ_{ψ (t)}^{X} ({+ 1}) = (1 + ⟨ X ⟩ (t)) / 2$ , $μ_{ψ (t)}^{X} ({- 1}) = (1 - ⟨ X ⟩ (t)) / 2$ ; in particular for $α = β = 1 / \sqrt{2}$ one has $μ_{ψ (t)}^{X} ({+ 1}) = (1 + \cos ω t) / 2$ .

(vi) The energy law is time-independent, $μ_{ψ (t)}^{H_{o p}} ({E_{1}}) = ∣ α ∣^{2}$ and $μ_{ψ (t)}^{H_{o p}} ({E_{2}}) = ∣ β ∣^{2}$ for every $t$ , and every one of the displayed expectations is periodic in $t$ with period $2 π / ∣ ω ∣$ (when $ω \neq 0$ , which holds because $E_{1} \neq E_{2}$ ).

The computation is a model-internal one: the energies are parameters of the assigned observable, the probabilities are those of the framework's outcome law, and no laboratory measurement, apparatus or empirical value is asserted.

Facts & Assumptions

Given: The Hilbert space $H = C^{2}$ with the standard inner product and orthonormal basis $(u_{1}, u_{2})$ ; distinct real energies $E_{1} \neq E_{2}$ in joules, and the reduced Planck constant $ℏ$ with its value and unit, in the framework's quantity conventions (Dimensions, SI unit conventions and quantity types of the framework); the assigned energy observable $H_{o p} = E_{1} T_{u_{1}, u_{1}} + E_{2} T_{u_{2}, u_{2}}$ with unit $J$ ; the observables $X, Y, Z$ ; a unit vector $ψ_{0} = α u_{1} + β u_{2}$ ; the number $ω = (E_{2} - E_{1}) / ℏ$ ; the Axiom of Countable Choice and the Axiom of Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ ), The Axiom of Choice), the choice hypotheses of the cited spectral suppliers.

[F1]

Rank-one calculus and one-dimensional projections. $T_{u, v} x = ⟨ x, v ⟩ u$ is bounded with $T_{u, v}^{*} = T_{v, u}$ , and the assignment is linear in $u$ and conjugate-linear in $v$ ; for every nonzero $ψ$ the operator $T_{ψ, ψ}$ is self-adjoint positive trace class, and for every unit $u$ the operator $T_{u, u}$ is the Hilbert orthogonal projection onto the one-dimensional subspace $C u$ , so that $T_{u, u}$ is idempotent and $T_{u, u} ψ = ⟨ ψ, u ⟩ u$ (Rank-one operator calculus, Rays, unit vectors and rank-one Hilbert projections clause (b)).

[F2]

Finite spectral structure. For the bounded self-adjoint $H_{o p}$ with orthonormal eigenvectors $u_{1}, u_{2}$ at the distinct eigenvalues $E_{1}, E_{2}$ , the assignment $E^{'} (B) : = 1_{E_{1} \in B} T_{u_{1}, u_{1}} + 1_{E_{2} \in B} T_{u_{2}, u_{2}}$ takes orthogonal-projection values by [F1], satisfies $E^{'} (R) = I$ by [F7], and is additive and multiplicative over the two-point eigenvalue set, so it is a projection-valued measure: for a disjoint sequence each of its two atoms occurs in at most one member, giving strong countable additivity. Its scalar measures are finite sums of point masses and hence regular; its integral domain is all of $H$ , since $\int λ^{2} d E_{x}^{'} (λ) = \sum_{k = 1}^{2} E_{k}^{2} ∣ ⟨ x, u_{k} ⟩ ∣^{2} < \infty$ . Thus $\int λ d E^{'} (λ) = E_{1} T_{u_{1}, u_{1}} + E_{2} T_{u_{2}, u_{2}} = H_{o p}$ ; by the uniqueness of the spectral measure it is $E_{H}$ (Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely, Spectral theorem for unbounded self-adjoint operators (PVM form), Assigned energy observable, unitary flow and the two pictures of autonomous evolution clause (a)).

[F7]

Resolution of the identity. Since $(u_{1}, u_{2})$ is an orthonormal basis of the two-dimensional space $H$ , every $v \in H$ satisfies $v = ⟨ v, u_{1} ⟩ u_{1} + ⟨ v, u_{2} ⟩ u_{2}$ , and therefore $T_{u_{1}, u_{1}} + T_{u_{2}, u_{2}} = I$ (Bessel's inequality for a finite orthonormal list and Parseval's identity for an orthonormal basis).

[F3]

Bounded calculus for the two-point measure. For bounded Borel $f : R \to C$ , put $g = f (E_{1}) 1_{{E_{1}}} + f (E_{2}) 1_{{E_{2}}}$ . The simple integral is $Φ_{E_{H}} (g) = f (E_{1}) T_{u_{1}, u_{1}} + f (E_{2}) T_{u_{2}, u_{2}}$ . By [F2], $E_{H} (R ∖ {E_{1}, E_{2}}) = 0$ , so $g = f$ almost everywhere for every scalar measure $B \mapsto ⟨ E_{H} (B) x, x ⟩$ , $x \in H$ . The constant sequence $g_{n} = g$ is bounded uniformly by $∥ f ∥_{\infty}$ and converges to $f$ in that almost-everywhere sense; clause (4) of Pvm integral is a star homomorphism therefore gives $Φ_{E_{H}} (f) = Φ_{E_{H}} (g)$ , proving the formula without uniform approximation on $R$ .

[F4]

Flow and state evolution. The flow is $U (t) = \exp (- i t H_{o p} / ℏ) = Φ_{E_{H}} (e^{- i t λ / ℏ})$ and the preparation evolves as $ψ (t) = U (t) ψ_{0}$ , with $∥ ψ (t) ∥ = ∥ ψ_{0} ∥ = 1$ ; the energy law is time-independent (The Schroedinger-picture flow: unitarity, domain invariance and the domain-qualified equation clauses (a) and (d), Energy conservation, conserved sharp observables and the stationary eigenrays clause (a), Assigned energy observable, unitary flow and the two pictures of autonomous evolution clauses (b) and (c)).

[F5]

Outcome law. For an assigned sharp observable $(A_{0}, u_{A_{0}})$ the law of the pure preparation of a unit vector $ψ$ is $μ_{ψ}^{A_{0}} (B) = ∥ E_{A_{0}} (B) ψ ∥^{2}$ , and the mean for a unit vector in $D (A_{0})$ is $⟨ A_{0} ψ, ψ ⟩$ ; the law depends only on the ray (Assigned sharp observables and the outcome law of the framework clauses (b) and (e), State vectors, unit vectors, rays, normalization and phases of a Hilbert space).

[F6]

Complex exponential algebra. For real $θ, ϕ$ : $e^{i θ} = \cos θ + i \sin θ$ , $e^{i (θ + ϕ)} = e^{i θ} e^{i ϕ}$ , $∣ e^{i θ} ∣ = 1$ and $\overline{e^{i θ}} = e^{- i θ}$ ; for complex $z$ , $2 Re z = z + \overline{z}$ and $2 i Im z = z - \overline{z}$ (Euler's formula: $\exp (i θ) = \cos θ + i \sin θ$ for every real $θ$ , $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential, $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ , Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive). Moreover $\ker (\exp) = 2 π i Z$ , so for real $θ$ one has $e^{i θ} = 1$ exactly for $θ \in 2 π Z$ ( $\ker (\exp) = 2 π i Z$ , and $\exp z = \exp w$ exactly when $z - w \in 2 π i Z$ ).

Verification

technique · direct; compute the spectral measure, the flow, the algebra and the laws of the explicit two-dimensional model

1.1givenF1F2F3F7algebra

[Spectral measure and flow] $H_{o p}$ is bounded and self-adjoint because $T_{u_{1}, u_{1}}, T_{u_{2}, u_{2}}$ are self-adjoint projections by [F1] and $E_{1}, E_{2} \in R$ , and $H_{o p} u_{k} = E_{k} u_{k}$ ; on the two-point spectrum the assignment $E^{'}$ of [F2] has orthogonal-projection values with $E^{'} (R) = I$ by [F7] and is additive and multiplicative, so [F2] identifies $E_{H}$ , and [F3] with $f (λ) = e^{- i t λ / ℏ}$ gives $U (t) = \sum_{k} e^{- i E_{k} t / ℏ} T_{u_{k}, u_{k}}$ . This is (i).

1.2givenF1F7algebra

[The three observables] By [F1] each of $X = T_{u_{1}, u_{2}} + T_{u_{2}, u_{1}}$ , $Y = i T_{u_{2}, u_{1}} - i T_{u_{1}, u_{2}}$ , $Z = T_{u_{1}, u_{1}} - T_{u_{2}, u_{2}}$ is bounded and self-adjoint. Composing rank-one operators from their definition, $T_{u, v} T_{w, z} x = ⟨ ⟨ x, z ⟩ w, v ⟩ u = ⟨ w, v ⟩ ⟨ x, z ⟩ u$ , so with orthonormality $T_{u_{1}, u_{2}} T_{u_{2}, u_{1}} = T_{u_{1}, u_{1}}$ , $T_{u_{2}, u_{1}} T_{u_{1}, u_{2}} = T_{u_{2}, u_{2}}$ and all products of two distinct rank-one terms $T_{u_{j}, u_{k}} T_{u_{l}, u_{m}}$ with $k \neq l$ vanish; hence $X^{2} = T_{u_{1}, u_{1}} + T_{u_{2}, u_{2}} = I$ by [F7], $Y^{2} = I$ , $Z^{2} = I$ and $X Y = i (T_{u_{1}, u_{1}} - T_{u_{2}, u_{2}}) = i Z$ . The eigenvalues of $X$ are $\pm 1$ with eigenvectors $e_{\pm} = (u_{1} \pm u_{2}) / \sqrt{2}$ . For $Y$ , the vectors $f_{\pm} = (u_{1} \pm i u_{2}) / \sqrt{2}$ satisfy $Y f_{\pm} = \pm f_{\pm}$ ; for $Z$ , one has $Z u_{1} = u_{1}$ and $Z u_{2} = - u_{2}$ . Since each of $X, Y, Z$ is self-adjoint and squares to $I$ , its spectrum is contained in ${- 1, + 1}$ , and these explicit eigenvectors show that both values occur for each operator. This proves (ii).

2.1givenstep 1.1F4F6algebra

[Evolved preparation] By [F4] and step 1.1, $ψ (t) = \sum_{k} c_{k} e^{- i E_{k} t / ℏ} u_{k}$ with $c_{1} = α$ , $c_{2} = β$ ; all coefficients have modulus $∣ c_{k} ∣$ because $∣ e^{- i E_{k} t / ℏ} ∣ = 1$ by [F6], so $∥ ψ (t) ∥^{2} = ∣ α ∣^{2} + ∣ β ∣^{2} = 1$ . This is the first assertion of (iii).

3.1givenstep 1.2step 2.1F5F6algebra

[Expectations] With $θ_{k} : = E_{k} t / ℏ$ and $ψ (t) = α e^{- i θ_{1}} u_{1} + β e^{- i θ_{2}} u_{2}$ , the actions $X u_{1} = u_{2}$ , $X u_{2} = u_{1}$ , $Y u_{1} = i u_{2}$ , $Y u_{2} = - i u_{1}$ , $Z u_{k} = \pm u_{k}$ from step 1.2 give $⟨ X ψ (t), ψ (t) ⟩ = α \overline{β} e^{i (θ_{2} - θ_{1})} + \overline{α \overline{β} e^{i (θ_{2} - θ_{1})}} = 2 Re (α \overline{β} e^{i ω t})$ and $⟨ Y ψ (t), ψ (t) ⟩ = i α \overline{β} e^{i (θ_{2} - θ_{1})} - i \overline{α \overline{β} e^{i (θ_{2} - θ_{1})}} = - 2 Im (α \overline{β} e^{i ω t})$ and $⟨ Z ψ (t), ψ (t) ⟩ = ∣ α ∣^{2} - ∣ β ∣^{2}$ , using $i (w - \overline{w}) = - 2 Im w$ for $w = α \overline{β} e^{i ω t}$ and [F6]; by [F5] these are the means of $X, Y, Z$ in $[ψ (t)]$ , which is (iii).

4.1givenstep 3.1F6algebra

[Precession of the triple] Write $c : = α \overline{β} = a + i b$ with $a, b \in R$ and $z : = ∣ α ∣^{2} - ∣ β ∣^{2}$ . By [F6], $c e^{i ω t} = (a \cos ω t - b \sin ω t) + i (a \sin ω t + b \cos ω t)$ , so step 3.1 gives $v (t) = (2 a \cos ω t - 2 b \sin ω t, - 2 a \sin ω t - 2 b \cos ω t, z)$ . This equals $R_{3} (- ω t) v (0)$ for $v (0) = (2 a, - 2 b, z)$ by the displayed definition of $R_{3}$ . Its squared Euclidean norm is $∥ v (t) ∥^{2} = 4 ∣ c e^{i ω t} ∣^{2} + z^{2} = 4 ∣ α ∣^{2} ∣ β ∣^{2} + (∣ α ∣^{2} - ∣ β ∣^{2})^{2} = (∣ α ∣^{2} + ∣ β ∣^{2})^{2} = 1$ by [F6]; taking the nonnegative square root gives $∥ v (t) ∥ = 1$ . This proves (iv), including $c = 0$ .

4.2givenstep 1.2step 3.1F1F5F6algebra

[Law of the flip observable] By step 1.2, $X = Q_{+} - Q_{-}$ with the orthogonal projections $Q_{\pm} = T_{e_{\pm}, e_{\pm}}$ onto the eigenspaces of the eigenvalues $\pm 1$ , so $E_{X} ({+ 1}) = Q_{+}$ and, by [F1], $Q_{+} ψ = ⟨ ψ, e_{+} ⟩ e_{+} = \frac{1}{\sqrt{2}} (⟨ ψ, u_{1} ⟩ + ⟨ ψ, u_{2} ⟩) e_{+}$ . For $ψ = ψ (t)$ this gives $∥ Q_{+} ψ (t) ∥^{2} = \frac{1}{2} ∣ α e^{- i θ_{1}} + β e^{- i θ_{2}} ∣^{2} = \frac{1}{2} (1 + ⟨ X ⟩ (t))$ by [F6] and step 3.1, and by [F5] this is $μ_{ψ (t)}^{X} ({+ 1})$ ; the minus case is the complement, and for $α = β = 1 / \sqrt{2}$ the value is $(1 + \cos ω t) / 2$ . This is (v).

4.3givenstep 1.1step 3.1F4F6algebra

[Energy law and periodicity] By [F4], $μ_{ψ (t)}^{H_{o p}} ({E_{k}}) = ∥ E_{H} ({E_{k}}) ψ (t) ∥^{2} = ∥ c_{k} e^{- i E_{k} t / ℏ} u_{k} ∥^{2} = ∣ c_{k} ∣^{2}$ using step 1.1 and [F6], so the two-point energy law is time-independent; the displayed expectations and probabilities are functions of $e^{i ω t}$ , and $e^{i ω (t + 2 π / ∣ ω ∣)} = e^{i ω t}$ because $\pm 2 π i \in \ker (\exp)$ by [F6], so they are periodic with period $2 π / ∣ ω ∣$ ; here $ω \neq 0$ because $E_{1} \neq E_{2}$ . This is (vi).

5.1step 1.1step 1.2step 2.1step 3.1step 4.1step 4.2step 4.3∎

Steps 1.1, 1.2, 2.1, 3.1, 4.1, 4.2 and 4.3 establish (i)-(vi) for the explicit model data.

Remarks

"Precession" is a bookkeeping device. The rotation of $v (t)$ is a statement about three expectation values of three bounded observables of a two-level system; no rotating rigid body, magnetic moment or specific species is asserted. The frequency $ω = (E_{2} - E_{1}) / ℏ$ is fixed by the two energy parameters.
Relative versus global phase. The evolution multiplies the two components by different phases; the relative phase $e^{i ω t}$ is what moves the observables $X$ and $Y$ , while a common phase of the whole vector would change no outcome law. For $α = 0$ or $β = 0$ the preparation is an eigenray and the triple is constant, in agreement with the stationary-state theorem.
No detector is modeled. The probabilities displayed are model outcome laws for the declared observables; no measurement interaction, resolution, efficiency or record is introduced.

Precession of a two-level preparation: exact phases, probabilities and a Bloch-vector rotation

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources