Empirical/QM: the Wigner–Araki–Yanase theorem #
Category: 3-Local (promotion-ready to 2-Framework on demand, exactly as
no_cloning_two_state is). QM-generic: no CSD ontology, pure inner-product
geometry, plus Fin 2 × Fin 2 matrix computations for the witnesses.
Glossary: https://glossary.constraintsurfacedynamics.com/way-theorem/
Plain-language, CSD-role and formal statements of the Wigner-Araki-Yanase theorem, with
this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.
The Wigner–Araki–Yanase (WAY) theorem: an observable A of a system S that
fails to commute with the system part L_S of an additively conserved
quantity L = L_S ⊗ 1 + 1 ⊗ L_A admits no exact measurement by an isometric
interaction U on HS ⊗ HA conserving L — provided the pointer states are
insensitive to L_A (the Yanase condition ⟨ξ_i, L_A ξ_j⟩ = 0, Yanase 1961)
or the measurement is repeatable (⟨φ_i, φ_j⟩ = 0). Contrapositively: exact,
Yanase-compliant (or repeatable) conserving measurements exist only for
observables commuting with L_S.
The master identity #
Everything follows from one line. For exact records U (a ⊗ ξ) = φ ⊗ ξ₁,
U (a' ⊗ ξ) = φ' ⊗ ξ₂ of orthogonal system vectors a ⊥ a' from a unit ready
state ξ, conservation L ∘ U = U ∘ L and inner-product preservation give
(arakiYanase_identity)
⟨a, L_S a'⟩ = ⟨φ, L_S φ'⟩ · ⟨ξ₁, ξ₂⟩ + ⟨φ, φ'⟩ · ⟨ξ₁, L_A ξ₂⟩.
Distinct pointer states ξ₁ ⊥ ξ₂ kill the first term; the Yanase condition
or repeatability kills the second (arakiYanase_offDiag_eq_zero). Summing
over an eigenbasis of A then makes L_S block-diagonal in the eigenspaces of
A, i.e. Commute A L_S (wigner_araki_yanase); the no-go form
no_exact_record_of_not_commute is its contrapositive. Neither a nor a'
need be normalised, so the σ_x instance below runs on the raw vectors
(1, 1), (1, −1).
Abstraction over the tensor structure #
As in no_cloning_two_state, the tensor product enters only through a map
tensor : HS → HA → HT with the inner-product factorisation
⟨tensor a b, tensor c d⟩ = ⟨a, c⟩ · ⟨b, d⟩, and additivity of L only on
product vectors, L (tensor a b) = tensor (L_S a) b + tensor a (L_A b). U
enters as an inner-product-preserving map commuting with L; no linearity of
U, no Matrix.exp, no unitary group, no Star synthesis. The witnesses
instantiate the idiom on EuclideanSpace ℂ (Fin 2 × Fin 2) with
tensorEuc/swapMap from Empirical/QM/Algorithms/HadamardTest.lean (both
factors are Fin 2, so the same-index product is the right one), sigmaX/sigmaZ
from Empirical/QM/Contextuality/MerminPeres.lean, the isometry of a unitary
matrix from Projectivization.inner_toEuclideanLin_unitary, and the measurement
unitary LF5.vnUnitary 2, which is CNOT ((j, k) ↦ (j, j + k) mod 2).
Witnesses #
- The side condition is load-bearing (
swap_exact_record_not_commute): SWAP conservesσ_z ⊗ 1 + 1 ⊗ σ_z(chargeZZ_swapMap), recordsσ_xexactly from the ready state|0⟩with orthogonal pointers(1, ±1), yet⟨(1, 1), σ_z (1, −1)⟩ = 2 ≠ 0(inner_xPlus_sigmaZ_xMinus). Both escape routes are closed there — the pointer fails Yanase and the record is not repeatable (φ_± = |0⟩) — so the theorem fails once both extra hypotheses are dropped. A reader cannot believe the side condition removable. - Non-vacuity (
way_hypotheses_satisfiable): CNOT conservesσ_z ⊗ 1 + 1 ⊗ σ_x(chargeZX_mul_cnot), recordsσ_zexactly and repeatably (cnot_record) with orthogonal pointers (inner_ket) — every hypothesis ofwigner_araki_yanaseis met, through the repeatability disjunct: the pointer fails Yanase againstL_A = σ_x(cnot_pointer_not_yanase). - The no-go in use (
sigmaX_no_exact_conserving_record): no isometry conservingσ_z ⊗ 1 + 1 ⊗ L_A, for anyL_A, recordsσ_xexactly with orthogonal pointers unless the pointer fails Yanase and the record is non-repeatable.σ_xhas the eigenvectors of the corpus'srotatedProj(Empirical/CSD/PointerCommutation.lean,rotatedProj_not_commute), which this module does not import (layer hygiene: Empirical/QM sits below Empirical/CSD).
Neighbours in the corpus #
pointer_basis_of_commuting / pointer_invariant_iff_commute
(Empirical/CSD/PointerCommutation.lean) are the einselection direction: a
pointer P commuting with H_int on one space. WAY is about an additive
conserved quantity on a tensor product and the exactly recorded observable —
neighbours, not the same theorem; nothing is re-proved here.
csd_robertson_uncertainty (Empirical/CSD/Uncertainty.lean) is the other
uncertainty-type theorem of the Empirical layer. Quantitative WAY (Ozawa 2002:
the measurement error is bounded below by the inverse apparatus variance of
L_A) is not formalised.
Where this sits relative to CSD #
WAY constrains nothing in CSD, for different reasons at the two measurement
tiers. In the LF5 von Neumann tier its hypotheses can be met — vnUnitary
(LF5/VonNeumannUnitary.lean) is a tensor-product isometry, and the CNOT witness
below exhibits an additive L it conserves — and its conclusion then holds
trivially: the recorded computational basis is L_S = σ_z-diagonal. In the
record layer (RecordLayer/), the stroke pointerEvolve / jointLift is a skew
product on the arena ℂℙ^{N−1} × T² × ℂℙ^N, not a linear isometry on
HS ⊗ HA, and no additive L_S ⊗ 1 + 1 ⊗ L_A is modelled, so the hypotheses
are not met at all. In neither tier is a physical apparatus charge modelled —
a consequence of the R-015 boundary in specs/residues.tsv (the coupling is
an engineered witness; which physical H_int, hence which conserved L_A, an
apparatus realises is a modelling input). This module is a QM-side theorem, not
a CSD result; the record-layer scope statement is its twin
Empirical/CSD/WignerArakiYanase.lean (no_joint_hilbert_map: no map on a joint
Hilbert space reproduces any joint lift's pointer image — the fibre register
selects the outcome; brick 1 of specs/way-theorem-scoping.md §3), and §2 W5–W7
there record what WAY does not say about the record layer.
specs/qm-empirical-tests.md (ER1, the twins board) and specs/future-work.md
(MT-1, the measurement-theoretic pillar row) index it.
Experimental verification #
WAY is a structural theorem, not a measured inequality. Its laboratory face is
Ozawa's conservative-quantum-computing bound (Ozawa 2002b): under an additive
conservation law a gate that fails to commute with the conserved charge — a
σ_x rotation under σ_z conservation — cannot be realised with unit fidelity
by a finite control system; the infidelity floor scales inversely with the
control's charge variance, which is the quantitative WAY theorem in gate form.
Source #
Wigner 1952, Z. Phys. 133, 101; Araki–Yanase 1960, Phys. Rev. 120, 622; Yanase 1961, Phys. Rev. 123, 666; Ozawa 2002, Phys. Rev. Lett. 88, 050402 (quantitative form) and Phys. Rev. Lett. 89, 057902 (conservative quantum computing); neither quantitative form is formalised here.
The abstract theorem #
The Araki–Yanase master identity. For an inner-product-preserving U commuting
with an additive L (L (a ⊗ b) = L_S a ⊗ b + a ⊗ L_A b), a unit ready state ξ, orthogonal
system vectors a ⊥ a', and exact records U (a ⊗ ξ) = φ ⊗ ξ₁, U (a' ⊗ ξ) = φ' ⊗ ξ₂,
⟨a, L_S a'⟩ = ⟨φ, L_S φ'⟩ · ⟨ξ₁, ξ₂⟩ + ⟨φ, φ'⟩ · ⟨ξ₁, L_A ξ₂⟩.
Only inner_add_right, the factorisation, isometry and pointwise conservation are used:
no linearity of U, no additivity of tensor, and a, a' need not be normalised.
Off-diagonal vanishing. With distinct (orthogonal) pointer states and either the
Yanase condition ⟨ξ₁, L_A ξ₂⟩ = 0 or repeatability ⟨φ, φ'⟩ = 0, the master identity
forces ⟨a, L_S a'⟩ = 0. The disjunction is the whole theorem: swap_exact_record_not_commute
shows the conclusion fails when both disjuncts fail.
★★ Wigner–Araki–Yanase. Let A be diagonal in an orthonormal basis b with
eigenvalues α, and let U be an inner-product-preserving interaction conserving the
additive L = L_S ⊗ 1 + 1 ⊗ L_A that records every b i exactly from the unit ready state
ξ (U (b i ⊗ ξ) = φ i ⊗ ξ' i) with pointers orthogonal across distinct eigenvalues. If, across
distinct eigenvalues, the pointers satisfy the Yanase condition or the record is repeatable,
then Commute A L_S. The hypotheses on the record are asked only across distinct
eigenvalues, so a degenerate A is covered.
★ The no-go form, which is how the theorem is used: if A does not commute with
L_S, no ready state and no exact record with pointers orthogonal across distinct eigenvalues
and Yanase-compliant (or repeatable) across distinct eigenvalues exists for any conserving
isometry U. Contrapositive of wigner_araki_yanase.
Two-qubit infrastructure #
Kronecker matrices act factorwise on tensorEuc; the computational kets and the unnormalised
σ_x eigenvectors, with their σ_z/σ_x actions and inner products.
A Kronecker product acts factorwise on a product vector:
(A ⊗ₖ B) (a ⊗ c) = (A a) ⊗ (B c). This is the additivity input for L = L_S ⊗ₖ 1 + 1 ⊗ₖ L_A.
Placed here rather than beside tensorEuc to keep Kronecker out of the Hadamard-test
import chain (SigmaLayer/Interference.lean sits downstream of it).
σ_z |j⟩ = (−1)^j |j⟩: the computational basis is the σ_z eigenbasis.
The computational basis as the orthonormal basis EuclideanSpace.basisFun, in ket form.
|j⟩ ⊗ |k⟩ is the standard basis vector at (j, k).
The unnormalised σ_x eigenvector (1, 1).
Equations
Instances For
xPlus ≠ 0 (its 0-th coordinate is 1); the hypothesis Projectivization.mk needs to
form the ray [xPlus] in the CSD twin.
The unnormalised σ_x eigenvector (1, −1).
Equations
Instances For
σ_x (1, 1) = (1, 1).
σ_x (1, −1) = −(1, −1).
⟨(1, 1), σ_z (1, −1)⟩ = 2: the σ_x eigenvectors are coupled by σ_z. This is the
⟨a, L_S a'⟩ ≠ 0 that WAY forbids for an exact conserving record.
Witnesses: CNOT (non-vacuity) and SWAP (sharpness) #
chargeZX is additive on product vectors: L (a ⊗ c) = σ_z a ⊗ c + a ⊗ σ_x c.
chargeZZ is additive on product vectors: L (a ⊗ c) = σ_z a ⊗ c + a ⊗ σ_z c.
CNOT (vnUnitary 2) commutes with σ_z ⊗ 1 + 1 ⊗ σ_x: entrywise on Fin 2 × Fin 2.
CNOT conserves chargeZX pointwise: L (U x) = U (L x).
CNOT is an isometry of EuclideanSpace ℂ (Fin 2 × Fin 2).
CNOT records σ_z exactly and repeatably: U (|j⟩ ⊗ |0⟩) = |j⟩ ⊗ |j⟩
(φ j = ξ' j = |j⟩; vnUnitary_mulVec_ground).
The CNOT pointer fails the Yanase condition against L_A = σ_x: ⟨0| σ_x |1⟩ = 1 ≠ 0.
CNOT therefore satisfies wigner_araki_yanase through the repeatability disjunct only.
Non-vacuity of wigner_araki_yanase. With A = L_S = σ_z on the computational basis
(α = (1, −1)), there are a tensor map, an additive conserved L with apparatus part L_A, an
isometry U conserving L, a unit ready state and exact records satisfying every hypothesis of
wigner_araki_yanase — and the pointers fail the Yanase condition, so it is the repeatability
disjunct that carries the instance. Witness: tensorEuc, chargeZX, σ_x, CNOT, |0⟩,
φ j = ξ' j = |j⟩.
SWAP conserves chargeZZ pointwise: L (swap x) = swap (L x).
Sharpness: the side condition cannot be dropped. There are data satisfying every
hypothesis of arakiYanase_offDiag_eq_zero except hside — an isometry conserving an additive
σ_z ⊗ 1 + 1 ⊗ L_A, a unit ready state, orthogonal system vectors recorded exactly with
orthogonal pointers — for which ⟨a, L_S a'⟩ ≠ 0; and there both disjuncts of hside fail
(the pointer violates Yanase and the record is not repeatable). Witness: SWAP with
L_A = σ_z, ready state |0⟩, a = (1, 1), a' = (1, −1), records |0⟩ ⊗ (1, ±1)
(swapMap_tensorEuc), so φ_± = |0⟩ and ξ_± = (1, ±1).
The no-go in use: no exact conserving record of σ_x with a well-behaved pointer.
For any apparatus part L_A, any isometry U conserving the additive σ_z ⊗ 1 + 1 ⊗ L_A
that records the σ_x eigenvectors (1, ±1) exactly from a unit ready state with orthogonal
pointers must have a pointer violating the Yanase condition and a non-repeatable record.
(σ_x has the eigenvectors of rotatedProj, Empirical/CSD/PointerCommutation.lean;
sigmaX_xPlus, sigmaX_xMinus.) The 2 ≠ 0 of inner_xPlus_sigmaZ_xMinus against
arakiYanase_offDiag_eq_zero.