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.

Distinct preparations are separated by the statistics of a bounded sharp observable

Physical scope

A conditional separation statement for the framework's preparations: two distinct preparations of a declared system assign different probabilities to some outcome of some bounded sharp observable of the framework, namely to the outcome 1 of a rank-one orthogonal projection; the difference is bounded by the trace-norm distance of the two states. The item asserts no finite-measurement procedure that identifies a preparation, no apparatus realization and no empirical result; it concerns the model's state space under the state and observable postulates.

Statement

Adopt the state and composition postulate State and composition postulate P1: Hilbert spaces, preparations and composite systems (P1) and the observable and probability postulate Observable and probability postulate P2: self-adjoint observables, spectral probability and finite unsharp outcomes (P2), and assume the Axiom of Countable Choice and the Axiom of Choice (The Axiom of Countable Choice (ACω), The Axiom of Choice). Let H be the state space assigned to a declared system and let ρ≠σ be two preparations of the system in the sense of The state space of the framework: preparations, pure rays and density operators clauses (a)-(c). Then there is a bounded sharp observable of the framework, namely an orthogonal projection P of rank one, such that the outcome laws of Assigned sharp observables and the outcome law of the framework differ at the outcome set {1}: μρP({1})=tr⁡(ρP)≠tr⁡(σP)=μσP({1}). Moreover for every rank-one projection P one has ∣μρP({1})−μσP({1})∣≤∥ρ−σ∥1; consequently, if μρP=μσP for every bounded sharp observable P (or merely for every rank-one projection), then ρ=σ.

The statement is conditional on P1 and P2 and asserts no procedure that determines a preparation from finitely many measurements, no apparatus realization, no error rate and no empirical result.

Facts & Assumptions

[F1]

Mathematical separation. For distinct density operators ρ,σ there is a unit vector w∈H with ⟨ρw,w⟩≠⟨σw,w⟩; for the rank-one projection P=Tw,w the spectral law of P satisfies μρP({1})=tr⁡(ρP)=⟨ρw,w⟩ and likewise for σ, and ∣tr⁡((ρ−σ)Tw,w)∣≤∥ρ−σ∥1 (Distinct density operators are separated by the law of a bounded rank-one projection clauses (a)-(c)).

[F2]

The framework's outcome law and its reading. An assigned sharp observable has spectral PVM EA and outcome law μρA(B)=tr⁡(ρEA(B)), equal to ∥EA(B)ψ∥2 for a pure preparation; the law is a probability measure on the Borel sets of R, and the outcome-set reading of the model is that of Assigned sharp observables and the outcome law of the framework (The Born outcome law: probability measure, mixtures, atoms and spectral support clauses (a)-(c), clause (ii)).

[F3]

Projections are assigned bounded observables. An orthogonal projection P is a bounded self-adjoint operator with 0≤P≤I on H (The Hilbert orthogonal projection onto a closed subspace, Hilbert projections are linear, self-adjoint and contractive), hence qualifies as a sharp observable of the framework when assigned with the dimensionless unit of its spectral coordinate.

Proof

1.1givenF1F2F3algebra

[Existence of a separating bounded observable] Let w and P=Tw,w be as in [F1]: such a unit vector exists because ρ≠σ and ρ−σ is a nonzero self-adjoint trace-class operator. By [F3] the operator P is a bounded self-adjoint projection, hence an assigned sharp observable of the framework once its unit (the dimensionless spectral coordinate, which here takes the values 0 and 1) is declared; its spectral law at {1} is tr⁡(ρP) and tr⁡(σP) by [F2], and [F1] gives tr⁡(ρP)=⟨ρw,w⟩≠⟨σw,w⟩=tr⁡(σP).

2.1step 1.1givenF1F2algebra∎

[Uniform bound and separation] The bound ∣μρP({1})−μσP({1})∣=∣tr⁡((ρ−σ)P)∣≤∥ρ−σ∥1 is [F1] applied to the rank-one projection P. If all rank-one projections have equal laws for ρ and σ, then ⟨ρw,w⟩=⟨σw,w⟩ for every unit w by the same identification, contradicting the choice of w in [F1] unless ρ=σ; hence statistical identity for all such observables forces the preparations to coincide. This proves the statement, and the assertion involves no measurement procedure beyond the model's outcome law.

Depends on

Dependency tree · 2 levels

Sources