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.

Coarse and fine declared measurements of a degenerate subspace: the Lueders update is not eigenvector selection

Physical scope

An exact finite model computation contrasting two declared ideal sharp measurements of a three-level system: a coarse readout of a degenerate two-dimensional subspace and a fine readout resolving it. The example shows that the Lueders update by the subspace projection retains the coherent superposition while the fine measurement selects basis states, and that the two declared measurements give different statistics for a suitable bounded observable. It asserts no apparatus realization and no empirical result.

Example

Declare a three-level system with assigned Hilbert space $H = C^{3}$ and orthonormal basis $(e_{1}, e_{2}, e_{3})$ , and put $K : = span (e_{1}, e_{2}), P : = T_{e_{1}, e_{1}} + T_{e_{2}, e_{2}}, ψ : = \frac{e_{1} + e_{2}}{\sqrt{2}}, w^{'} : = \frac{e_{1} - e_{2}}{\sqrt{2}},$ with $T_{x, y} z = ⟨ z, y ⟩ x$ (The state space of the framework: preparations, pure rays and density operators, Real and complex inner product spaces, with the inner product linear in the first argument, Hilbert space, Rank-one operator calculus). Declare the two ideal sharp measurements $C : = (P, I - P) (coarse readout of K), G : = (T_{e_{1}, e_{1}}, T_{e_{2}, e_{2}}, T_{e_{3}, e_{3}}) (fine readout),$ and consider the pure preparation $ρ = T_{ψ, ψ}$ and the bounded self-adjoint observable, declared dimensionless with spectral unit $1$ , $W : = T_{ψ, ψ} - T_{w^{'}, w^{'}}$ with spectral projections $T_{ψ, ψ}$ at $+ 1$ , $T_{w^{'}, w^{'}}$ at $- 1$ and $I - T_{ψ, ψ} - T_{w^{'}, w^{'}}$ at $0$ (Declared ideal measurements and instruments of the framework, Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely). Then:

(i) In the coarse measurement $C$ the outcome $K$ has probability $1$ , and the conditional state is again $ρ = T_{ψ, ψ}$ : the coarse readout leaves the coherent superposition inside the degenerate subspace intact.

(ii) In the fine measurement $G$ the outcomes $e_{1}$ and $e_{2}$ have probabilities $\frac{1}{2}$ each (and $e_{3}$ has probability $0$ ), with conditional states $T_{e_{1}, e_{1}}$ and $T_{e_{2}, e_{2}}$ : the fine readout selects a basis state.

(iii) For the observable $W$ the two declared measurements give different model predictions: after the coarse outcome the value $+ 1$ has probability $1$ ; the mixture $\frac{1}{2} T_{e_{1}, e_{1}} + \frac{1}{2} T_{e_{2}, e_{2}}$ (the discarded ensemble of the fine measurement) assigns probability $\frac{1}{2}$ to $+ 1$ and $\frac{1}{2}$ to $- 1$ . Hence the coarse Lueders update is not equivalent to selecting one eigenvector of the degenerate subspace with probability $\frac{1}{2}$ and forgetting the other: that replacement destroys the coherence of $ψ$ and changes the statistics of $W$ .

(iv) The fine measurement refines the coarse outcome structure: grouping outcomes $e_{1}, e_{2}$ gives $K$ , and outcome $e_{3}$ gives $K^{⊥}$ , since $P = T_{e_{1}, e_{1}} + T_{e_{2}, e_{2}}$ and $I - P = T_{e_{3}, e_{3}}$ . It is nevertheless a different declared measurement with more detailed outcomes. The coarse outcome "the system is in $K$ " does not itself report whether the fine outcome was $e_{1}$ or $e_{2}$ ; replacing the coarse Lueders update by the discarded fine ensemble is a different model, with the observable consequence exhibited in (iii). No apparatus is asserted to realize either declared measurement, and no empirical comparison is made.

Facts & Assumptions

Given: The three-level Hilbert space $H = C^{3}$ with orthonormal basis $(e_{1}, e_{2}, e_{3})$ ; the projection $P = T_{e_{1}, e_{1}} + T_{e_{2}, e_{2}}$ ; the unit vectors $ψ, w^{'}$ ; the declared measurements $C, G$ ; the preparation $ρ = T_{ψ, ψ}$ ; the observable $W$ .

[F1]

Rank-one calculus. $T_{x, y} z = ⟨ z, y ⟩ x$ is trace class with $T_{x, y}^{*} = T_{y, x}$ ; for unit vectors $x, u$ the operator $T_{x, x}$ is an orthogonal projection with $tr (T_{x, x} S) = ⟨ S x, x ⟩$ for bounded $S$ , and $tr (T_{x, x} T_{u, u}) = ∣ ⟨ x, u ⟩ ∣^{2}$ (Rank-one operator calculus clauses (b)-(d), Hilbert space).

[F2]

Declared measurements and updates. For a declared ideal sharp measurement $(P_{a})$ the outcome probabilities are $p_{a} = tr (ρ P_{a}) = ∥ P_{a} ξ ∥^{2}$ for a pure preparation of the unit vector $ξ$ , and the conditional state after a positive-probability outcome is $P_{a} ρ P_{a} / p_{a}$ (Declared ideal measurements and instruments of the framework clauses (a)-(b), Consequences of a declared ideal sharp measurement: repeatability and discarded ensembles clauses (a)-(b)).

[F3]

Selective update of a supported pure state. Under Countable Choice, for an orthogonal projection $P$ and a unit vector $ξ$ with $P ξ \neq 0$ , the normalized compression of $T_{ξ, ξ}$ is $T_{P ξ, P ξ} / ∥ P ξ ∥^{2}$ (The selective Lueders update by an orthogonal projection clause (d)). Its physical interpretation as the conditional state of the declared measurement is exactly [F2]. This lemma requires no assigned observable or spectral-eigenspace hypothesis.

[F4]

Spectral projections of $W$ . $ψ$ and $w^{'}$ are orthonormal, and $W = T_{ψ, ψ} - T_{w^{'}, w^{'}}$ is bounded and self-adjoint with $W ψ = ψ$ , $W w^{'} = - w^{'}$ , so $T_{ψ, ψ}$ and $T_{w^{'}, w^{'}}$ are its spectral projections at $+ 1$ and $- 1$ (Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely, [F1]).

[F5]

Elementary overlaps. $⟨ e_{1}, ψ ⟩ = ⟨ e_{2}, ψ ⟩ = 1 / \sqrt{2}$ , $⟨ e_{1}, w^{'} ⟩ = 1 / \sqrt{2}$ , $⟨ e_{2}, w^{'} ⟩ = - 1 / \sqrt{2}$ , and $⟨ e_{3}, ψ ⟩ = ⟨ e_{3}, w^{'} ⟩ = 0$ (The induced length is a norm, Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

Verification

technique · direct; compute the outcome laws and conditional states of the two declared measurements and the induced law of the observable $W$

1.1givenF1F2F3algebra

[Clause (i)] $P ψ = ψ$ , so [F2] gives $tr (ρ P) = ∥ P ψ ∥^{2} = 1$ ; by [F3] and [F2] the conditional state after the outcome $K$ is $T_{P ψ, P ψ} / ∥ P ψ ∥^{2} = T_{ψ, ψ} = ρ$ , unchanged. This is (i).

2.1step 1.1givenF1F2F5algebra

[Clause (ii)] By [F2] and [F1], the fine outcome probabilities are $tr (T_{ψ, ψ} T_{e_{i}, e_{i}}) = ∣ ⟨ e_{i}, ψ ⟩ ∣^{2}$ , equal to $\frac{1}{2}$ for $i = 1, 2$ and $0$ for $i = 3$ by [F5]; the conditional states are $T_{e_{i}, e_{i}}$ . This is (ii).

3.1step 2.1givenF1F2F4F5algebra

[Clause (iii)] By [F4] and [F2], in the coarse conditional state $ρ = T_{ψ, ψ}$ the value $+ 1$ of $W$ has probability $tr (T_{ψ, ψ} T_{ψ, ψ}) = 1$ . The mixture $σ = \frac{1}{2} T_{e_{1}, e_{1}} + \frac{1}{2} T_{e_{2}, e_{2}}$ gives $tr (σ T_{ψ, ψ}) = \frac{1}{2} ∣ ⟨ e_{1}, ψ ⟩ ∣^{2} + \frac{1}{2} ∣ ⟨ e_{2}, ψ ⟩ ∣^{2} = \frac{1}{2}$ and $tr (σ T_{w^{'}, w^{'}}) = \frac{1}{2} ∣ ⟨ e_{1}, w^{'} ⟩ ∣^{2} + \frac{1}{2} ∣ ⟨ e_{2}, w^{'} ⟩ ∣^{2} = \frac{1}{2}$ by [F1] and [F5], so the mixture assigns probability $\frac{1}{2}$ to each of $+ 1$ and $- 1$ . The two laws for $W$ differ; the discarded ensemble of the fine measurement is this mixture, whereas the coarse conditional state is the coherent state $ρ$ , so replacing the coarse Lueders update by eigenvector selection is a distinct model with different predictions. This is (iii).

4.1step 3.1givenF1F2algebra∎

[Clause (iv) and scope] By the displayed definitions, the sum of the first two fine projections is $P$ and the third is $I - P$ , so grouping the fine outcomes as stated gives the coarse outcome structure; thus $G$ refines $C$ . The instruments are still distinct because the coarse Lueders outcome $K$ leaves $ρ$ unchanged while the fine measurement, when its label is discarded, gives the mixture in step 3.1. The coarse outcome alone supplies no finer label. No apparatus was used and no record is reported. This is (iv).

Remarks

Degeneracy is a property of the declared measurement, not of the state alone. The superposition $ψ$ inside $K$ is unchanged by the coarse readout because the update uses the projection onto the whole eigenspace; a fine measurement whose projections lie inside $K$ is a different apparatus model with different outcomes.
No preferred basis. The coarse readout has no rule that selects $e_{1}$ or $e_{2}$ ; the model contains no such rule, and the example shows that adding one changes predictions for a suitable later observable.

Coarse and fine declared measurements of a degenerate subspace: the Lueders update is not eigenvector selection

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources