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 position-momentum preparation relation of the massive spin-s model

Physical scope

The position-momentum preparation relation of the massive spin-s particle model of the framework, for one particle of mass parameter m>0 and spin label s: for every unit state vector in D(Q_j) cap D(P_j) the product of the preparation spreads of the j-th position and j-th momentum is at least hbar/2, with no product-domain hypothesis, together with the equality characterization by linear dependence of the centered vectors and the exact imaginary part -hbar/2. The statement is a conditional consequence of P1, P2, P5, P6 and the cited mathematics; P1 assigns pure preparations to unit rays, P2 supplies the outcome laws and spread reading, and P5/P6 assign this massive spin-s model. It concerns the spreads of the two separately assigned outcome laws and asserts no joint sharp observable with the exact spectral marginals, no claim about unsharp joint measurements, no apparatus realisation, no disturbance relation and no empirical result.

Statement

Adopt the state and composition postulate P1, the observable and probability postulate P2, the kinematics and massive-particle model postulate P5, and the internal-factor assignment P6 of the framework, read for the spin-s model of The massive spin-s particle model of the framework: state space, operators, units and frame readings with mass parameter m>0, spin label s∈{0,12,1,… } and r=2s+1 (State and composition postulate P1: Hilbert spaces, preparations and composite systems, Observable and probability postulate P2: self-adjoint observables, spectral probability and finite unsharp outcomes, Kinematics and massive-particle model postulate P5: Newtonian frames and one-particle operators, Identical-particle and spin assignments P6: permutation sectors and finite-spin representations), and assume the Axiom of Countable Choice and the Axiom of Choice (The Axiom of Countable Choice (ACω), The Axiom of Choice). Let Qj,Pj be the model's j-th position and j-th momentum operators with their maximal domains, and let ΔψQj and ΔψPj be their preparation spreads in the reading of Preparation variance and spread of an assigned sharp observable. Let ψ∈D(Qj)∩D(Pj) be a unit vector and put a:=⟨Qjψ,ψ⟩,b:=⟨Pjψ,ψ⟩,x:=(Qj−a)ψ,y:=(Pj−b)ψ. Then:

(a) ΔψQj and ΔψPj are defined and ΔψQj ΔψPj≥ℏ2;

(b) if in addition ψ∈D(QjPj)∩D(PjQj), then (QjPj−PjQj)ψ=iℏψ and the bound of (a) follows from the Robertson relation for the two observables;

(c) for every unit ψ∈D(Qj)∩D(Pj) the centered pairing has the exact imaginary part Im⁡⟨x,y⟩=−ℏ2; consequently equality ΔψQjΔψPj=ℏ/2 holds if and only if x and y are linearly dependent and Re⁡⟨x,y⟩=0;

(d) Scope. The statement is conditional on P1, P2, P5, P6 and the cited mathematics. It concerns the two separately assigned position and momentum outcome laws in one preparation, needs no hypothesis on the products QjPj or PjQj. The compatibility results of this page show that no joint sharp observable with the exact spectral marginals of Qj and Pj exists; this statement makes no claim about existence or nonexistence of unsharp joint measurements or their outcome laws. It asserts no apparatus realization, no disturbance relation, no dynamics and no empirical result. Massless, relativistic, singular-potential and boundary realizations are separate models for which no such relation is asserted.

Facts & Assumptions

Given: The postulates P1, P2, P5 and P6 read through The massive spin-s particle model of the framework: state space, operators, units and frame readings; the Axiom of Countable Choice and the Axiom of Choice; the operators Qj,Pj of the model with their maximal domains; a unit vector ψ∈D(Qj)∩D(Pj); the numbers a,b and the centered vectors x,y.

[F1]

Model operators. Qj and Pj are the componentwise position and momentum operators of Componentwise position and momentum operators on the component-valued wave-function space clause (a), self-adjoint with domains D(Qj)={f:xjfl∈L2 ∀l} and D(Pj)={f:Djfl∈L2 ∀l}, and the model assigns to them the status of assigned sharp observables in the reading of Assigned sharp observables and the outcome law of the framework clause (a) (The massive spin-s particle model of the framework: state space, operators, units and frame readings clause (b)).

[F2]

Moments and spreads. For a unit vector in D(Qj) the mean and variance of the position law exist with ΔψQj=∥(Qj−a)ψ∥ where a=⟨Qjψ,ψ⟩ is real, and likewise for Pj (Mean, second moment and variance of an assigned observable in a preparation clauses (a) and (b), Preparation variance and spread of an assigned sharp observable clauses (b) and (c)).

[F3]

Product domain and commutator. D(QjPj)∩D(PjQj)={f:Djf,xjf,xjDjf∈L2} and on it (QjPj−PjQj)f=iℏf (The position-momentum commutator identity on the product domain clauses (b) and (c)).

[F4]

Approximation. For every unit ψ∈D(Qj)∩D(Pj) there is a sequence (φn) of unit vectors in D(QjPj)∩D(PjQj) with φn→ψ, Qjφn→Qjψ and Pjφn→Pjψ in Hs, and with ⟨Qjφn,φn⟩→⟨Qjψ,ψ⟩, ∥Qjφn∥→∥Qjψ∥ and the analogous momentum limits (Approximation of Q-P graph-domain vectors by product-domain vectors).

[F5]

Robertson relation. For two assigned sharp observables and a unit vector in the intersection of the two operator domains and the two product domains, the spread product is at least half the absolute value of the commutator pairing (The Robertson relation for preparation spreads of assigned sharp observables clause (b)).

[F6]

Cauchy-Schwarz and its equality case. In a complex inner product space, ∥v∥ ∥w∥≥∣⟨v,w⟩∣≥∣Im⁡⟨v,w⟩∣ and ∣⟨v,w⟩∣2=(Re⁡⟨v,w⟩)2+(Im⁡⟨v,w⟩)2, with equality in the first inequality if and only if v,w are linearly dependent (Cauchy–Schwarz: ∣⟨u,v⟩∣≤∥u∥∥v∥, with equality exactly for linearly dependent vectors, Hilbert space).

Proof

technique · prove the bound first on the product domain from the commutator identity and the Robertson relation, transfer it to the full maximal domain of the pair by the cutoff approximation, and compute the exact imaginary part of the centered pairing along the approximating sequence

Given: The data of the statement and [F1]-[F6].

1.1givenF1F3F5algebra

[Product-domain case] Let φ be a unit vector in D(QjPj)∩D(PjQj). By [F1] the operators Qj,Pj are the model's assigned sharp observables with their maximal domains, so the preparation spreads and the Robertson relation of [F5] apply to them. By [F3], (QjPj−PjQj)φ=iℏφ, so ⟨[Qj,Pj]φ,φ⟩=iℏ∥φ∥2=iℏ. By [F5] the product of the preparation spreads of the two assigned observables satisfies ΔφQjΔφPj≥12∣iℏ∣=ℏ/2.

2.1givenstep 1.1F2F3F4algebra

[Approximation] Let ψ∈D(Qj)∩D(Pj) be a unit vector and let (φn) be the approximating sequence of [F4]. For every n, φn is a unit product-domain vector, so step 1.1 gives ΔφnQjΔφnPj≥ℏ/2. By [F2] and [F4], ΔφnQj2=∥Qjφn∥2−⟨Qjφn,φn⟩2→∥Qjψ∥2−⟨Qjψ,ψ⟩2=ΔψQj2, and the analogous identity holds for Pj with the momentum limits of [F4]; taking square roots and products gives ΔφnQjΔφnPj→ΔψQjΔψPj. Hence the limit satisfies ΔψQjΔψPj≥ℏ/2, which is (a); and on the product domain the same computation together with [F3] is the derivation of (b).

3.1givenstep 2.1F1F2F3F4algebra

[Exact imaginary part] Keep the notation of step 2.1 and put an:=⟨Qjφn,φn⟩, bn:=⟨Pjφn,φn⟩, xn:=(Qj−an)φn, yn:=(Pj−bn)φn. Since φn lies in both product domains, symmetry of Qj and Pj gives ⟨[Qj,Pj]φn,φn⟩=⟨Pjφn,Qjφn⟩−⟨Qjφn,Pjφn⟩=−2iIm⁡⟨Qjφn,Pjφn⟩. The means an,bn are real by [F2], and expanding with the inner product linear in the first argument gives ⟨xn,yn⟩=⟨Qjφn,Pjφn⟩−anbn; hence Im⁡⟨Qjφn,Pjφn⟩=Im⁡⟨xn,yn⟩. By [F3], ⟨[Qj,Pj]φn,φn⟩=iℏ; hence −2iIm⁡⟨xn,yn⟩=iℏ and Im⁡⟨xn,yn⟩=−ℏ/2. By [F4], xn→x and yn→y in Hs (each is the sum of a convergent term and a scalar multiple of a convergent term), so the inner product is continuous and Im⁡⟨x,y⟩=lim⁡nIm⁡⟨xn,yn⟩=−ℏ/2. This is the first display of (c).

4.1step 2.1step 3.1F6algebra

[Equality characterization] For a unit ψ∈D(Qj)∩D(Pj) put ΔQ:=ΔψQj, ΔP:=ΔψPj. By step 3.1, Im⁡⟨x,y⟩=−ℏ/2, and by [F6] ℏ/2≤ΔQΔP=∥x∥ ∥y∥≥∣⟨x,y⟩∣≥∣Im⁡⟨x,y⟩∣=ℏ/2. Equality ΔQΔP=ℏ/2 holds exactly when both inequalities are equalities, that is (by the equality case of [F6] and the identity ∣⟨x,y⟩∣2=(Re⁡⟨x,y⟩)2+(Im⁡⟨x,y⟩)2) when x,y are linearly dependent and Re⁡⟨x,y⟩=0. This completes (c).

5.1step 1.1step 2.1step 3.1step 4.1∎

[Scope] Clauses (a)-(c) were obtained from the model's operators, the product-rule identity, the approximation lemma and the Robertson relation; no joint outcome law, apparatus, disturbance, dynamics or empirical input enters. This is (d).

Depends on

Dependency tree · 2 levels

Sources