Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck 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 two-level Zeeman toy model: sector energies, level splitting and spin precession

Physical scope

A worked example inside the massive spin-half model with the adopted effective magnetic-moment coupling in a uniform static field: the exact sector identities for the Zeeman operator on product states, the energy offsets, and an explicitly labeled two-level truncation in which the internal levels differ by gamma hbar B_z and the spin precesses with angular frequency gamma B_z. The truncation is a toy model assumption, not derived from the full operator; no spectroscopy, no radiation, no measured gyromagnetic parameter and no apparatus is asserted.

Example

Adopt the state and composition postulate P1, the observable and probability postulate P2, the autonomous-dynamics postulate P4, the kinematics and massive-particle model postulate P5 and the internal-factor assignment of the spin postulate P6, read for the massive spin-12 model of The massive spin-s particle model of the framework: state space, operators, units and frame readings with mass parameter m>0, together with the effective magnetic-moment coupling of Effective magnetic-moment coupling of the finite-spin model: gyromagnetic parameter, magnetic moment and Zeeman energy operator with parameter γ:=γ1/2∈R, and assume the Axiom of Countable Choice and the Axiom of Choice (The Axiom of Countable Choice (ACω), The Axiom of Choice). Fix Bz∈R and the uniform field B=(0,0,Bz), let HZ=H0−γBzS3 on D(HZ)=W2,2(R3;C2) be the model's Zeeman operator with flow UZ(t)=e−itHZ/ℏ and put ω:=γBz. Then:

(i) for every unit f∈L2(R3;C) and each sign, the product flow satisfies UZ(t)(f⊗e±)=e±iγBzt/2(e−itH0/ℏf)⊗e±(t∈R), and the transverse spin means of such a product state precess as in Spin precession and the Zeeman splitting in a uniform magnetic field: Larmor angular frequency and the conservation of one component. If in addition f∈D(H0)=W2,2(R3;C), then HZ(f⊗e±)=(H0f)⊗e±∓γℏBz2 f⊗e±,⟨HZ⟩f⊗e±:=⟨HZ(f⊗e±),f⊗e±⟩=⟨H0f,f⟩∓γℏBz2; the displayed expectation is defined only for these domain vectors.

(ii) toy truncation. Fix a real energy parameter E0∈R in joules. Suppose in addition that, on a declared two-dimensional internal subspace, the free part is replaced by the scalar E0I (a truncation assumption of the toy model, not a theorem of the full model): then the truncated operator is HZ(2)=E0I−γBzS3=(E0−γℏBz2)e+e+∗+(E0+γℏBz2)e−e−∗ in the basis (e+,e−), with energy levels E0∓γℏBz2 and signed level difference ΔE:=γℏBz=ℏω; its evolution is e−itHZ(2)/ℏ=e−itE0/ℏ(eiωt/200e−iωt/2), so the relative phase of the two amplitudes accumulates at the angular frequency ω (equivalently at the ordinary frequency ∣ω∣/(2π));

(iii) in the truncation the conjugation identities of the precession theorem reduce to explicit matrix identities, V(t)∗σ1V(t)=cos⁡(ωt)σ1+sin⁡(ωt)σ2,V(t)∗σ2V(t)=cos⁡(ωt)σ2−sin⁡(ωt)σ1, with V(t)=e−itHZ(2)/ℏeitE0/ℏ;

(iv) the toy model contains no driving field: its diagonal evolution preserves the two sector weights, hence there is no spin flip between e+ and e− under HZ(2) alone. Statements about spin-flip transitions, resonance or spectroscopy require a separately adopted drive or coupling, belong to the driven-dynamics and light-matter pages, and are not derived here. No apparatus, calibration, measured frequency or measured value of γ is asserted.

Facts & Assumptions

Given: The postulates P1, P2, P4, P5 and P6 and the magnetic-moment postulate in the stated readings; the two choice principles; the parameters m>0, s=12, γ∈R, Bz∈R and ω=γBz; the operator HZ and its flow; a unit f∈L2(R3;C); the basis (e+,e−); the scalar E0.

[F1]

Uniform-field Zeeman operator. H0 has domain D(H0)=W2,2(R3;C), and HZ=H0−γBzS3 is self-adjoint on D(HZ)=W2,2(R3;C2) with flow UZ(t)=e−itH0/ℏeitγBzS3/ℏ, S3 commutes with the flow, and for every unit vector the transverse means satisfy the precession identities of Spin precession and the Zeeman splitting in a uniform magnetic field: Larmor angular frequency and the conservation of one component clauses (a),(b),(c) (Effective magnetic-moment coupling of the finite-spin model: gyromagnetic parameter, magnetic moment and Zeeman energy operator clauses (i),(ii), Assigned energy observable, unitary flow and the two pictures of autonomous evolution, The state space of the framework: preparations, pure rays and density operators).

[F2]

Spin-half matrices. S3=ℏ2σ3 with σ3e±=±e±, S1=ℏ2σ1, S2=ℏ2σ2, and the Pauli matrices satisfy σ12=σ22=I, σ1σ2=iσ3, σ2σ1=−iσ3 (Finite spin matrices clause (e), Orbital, spin and total angular momentum of the massive spin-s model: assigned sharp observables, units and readings clause (c)).

[F3]

Bounded exponentials. For a bounded self-adjoint matrix A the map t↦e−itA/ℏ=∑n(−itA/ℏ)n/n! is a norm-continuous unitary group with (e−itA/ℏ)∗=eitA/ℏ (The exponential series of a bounded operator, The operator norm as the least bound and as the unit-sphere or unit-ball supremum, The state space: density operators, pure and mixed states, and purity).

Verification

technique · direct; evaluate the Zeeman operator on the product basis of sectors, read the eigenvalues of the truncated internal matrix, and compute the conjugated Pauli matrices explicitly

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

1.1F1F2algebra

[Sector identities] By [F2] one has S3(f⊗e±)=±ℏ2f⊗e± and H0 acts on the spatial factor only; hence, for f∈D(H0), HZ(f⊗e±)=(H0f)⊗e±∓γℏBz2f⊗e±, and taking the inner product with the unit vector f⊗e± gives the displayed expectation. For every f∈L2, not necessarily in D(H0), [F1] gives the product-flow identity, with eitγBzS3/ℏe±=e±iγBzt/2e± by [F2]; the transverse means then precess as in the cited theorem, proving (i).

2.1step 1.1F2F3algebra

[Toy levels and evolution] In the two-dimensional internal model with free part E0I, the operator HZ(2)=E0I−γBzS3 is diagonal in (e+,e−) with entries E0∓γℏBz2 by [F2], so its eigenvalues are those entries and the signed difference is γℏBz=ℏω; by [F3] the exponential is the displayed diagonal unitary, and the relative phase accumulates at the angular frequency ω, which is (ii).

3.1step 2.1F2algebra

[Conjugation identities] With V(t)=e−itHZ(2)/ℏeitE0/ℏ=diag⁡(eiωt/2,e−iωt/2) from step 2.1, direct matrix multiplication using [F2] gives V(t)∗σ1V(t)=(0e−iωteiωt0)=cos⁡(ωt)σ1+sin⁡(ωt)σ2 and V(t)∗σ2V(t)=(0−ie−iωtieiωt0)=cos⁡(ωt)σ2−sin⁡(ωt)σ1, which is (iii) and agrees with the general conjugation of Spin precession and the Zeeman splitting in a uniform magnetic field: Larmor angular frequency and the conservation of one component clause (c).

4.1step 2.1step 3.1F2algebra∎

[Scope] Since HZ(2) is diagonal in (e+,e−), its evolution multiplies the two amplitudes by phases and preserves the sector weights ∣c±∣2: no spin flip occurs without a driving term, and the truncation was an explicit toy assumption, which is (iv).

Remarks

  • What the truncation discards. Replacing H0 by E0I discards the kinetic and any potential structure of the spatial factor; the truncated model is a toy description of the internal degree of freedom, and no spatial dynamics or position-space measurement model follows from it.
  • Frequency conventions. ω=γBz is an angular frequency in s−1; the ordinary frequency is ∣ω∣/(2π) in hertz, with the radian dimensionless, in the conventions of Dimensions, SI unit conventions and quantity types of the framework.

Depends on

Dependency tree · 2 levels

Sources