Empirical/QM: Ozawa's universally valid error–disturbance relation

Category: 3-Local (promotion-ready to 2-Framework on demand). QM-generic: no CSD ontology, pure operator geometry on one inner-product space.

Glossary: https://glossary.constraintsurfacedynamics.com/ozawa-error-disturbance/ — the entry names this module as its Lean anchor. Kept symmetric by scripts/check-glossary.sh.

Robertson (Uncertainty.lean) bounds the preparation spread of two observables in one state. It says nothing about a measurement's error or the disturbance it inflicts. The Heisenberg-microscope reading

ε(A)·η(B) ≥ ½ |⟪ψ, [A,B] ψ⟫|

is quoted constantly and is not universally valid: it holds under restrictive extra hypotheses (unbiased measurements) and fails in general, as Erhart et al. 2012 and Rozema et al. 2012 measured. Ozawa 2003's universally valid replacement is what this module proves:

★★ ozawa_error_disturbance: ε(A)·η(B) + ε(A)·σ(B) + σ(A)·η(B) ≥ ½ |⟪Ψ, [A_in,B_in] Ψ⟫|

with σ the standard deviations (Uncertainty.stdDev), not variances.

The shape: four operators on one space, two of which commute

Ozawa's ε and η are usually introduced through a measurement model (K, σ_probe, U, M) on a tensor product, with A_in = A ⊗ 1, A_out = U†(1 ⊗ M)U, B_in = B ⊗ 1, B_out = U†(B ⊗ 1)U. But the tensor structure plays no part in the inequality. What the proof uses is:

• four symmetric operators A_in, B_in, A_out, B_out on one space, and
• Commute A_out B_out — which in the measurement model holds because A_out and B_out are conjugates by the same U of 1 ⊗ M and B ⊗ 1, and those commute.

So the theorem is stated at that level (OzawaData), and a measurement model is one way to produce the data. This is deliberate: Empirical/QM/WignerArakiYanase.lean states its theorems over an abstract tensor (arakiYanase_identity takes tensor with h_tensor_inner as a hypothesis rather than using Mathlib's ⊗[ℂ]), and specs/way-theorem-scoping.md records that WAY brick 2 shares these definitions. Fixing a concrete tensor here would strand that brick.

Why the commutation is the whole content

Expanding [A_out, B_out] = [A_in + N, B_in + D] with N = A_out − A_in, D = B_out − B_in gives four summands, and the left-hand side is zero. Hence

[A_in, B_in] = −[A_in, D] − [N, B_in] − [N, D] (ozawa_commutator_identity)

and the three remaining terms are bounded by 2σ(A)η(B), 2ε(A)σ(B), 2ε(A)η(B) through one application each of Uncertainty.commutator_le_two_mul_norm — the unsquared Cauchy–Schwarz core, which exists in that file precisely because Robertson's squared form cannot be summed across three products. Centring A_in and B_in does not move the commutator (commutator_shift).

⚠️ Honest scope

• ε and η are defined here as norms ‖(A_out − A_in) Ψ‖, ‖(B_out − B_in) Ψ‖. For symmetric operators this is Ozawa's ⟪Ψ, (A_out − A_in)² Ψ⟫^{1/2} (error_sq_eq), so the definitions agree; the norm form is what the proof consumes.
• The naive Heisenberg form is not proved false here, and no Lean claim is made about it. That needs ε and η computed inside a measurement model. ozawa_two_term_false refutes only the two-term variant ε·η + ε·σ(B) ≥ ½|⟪[A,B]⟫|, i.e. it shows the third term is load-bearing.
• The witness inhabits OzawaData; a measurement model deriving A_out = U†(1 ⊗ M)U from a probe is not built here (specs/ozawa-scoping.md §3a).
• Nothing here is a CSD result. The record-layer stroke is not a measurement model in this sense — see Empirical/CSD/Ozawa.lean, which states that as a theorem rather than leaving it implied.

References

specs/ozawa-scoping.md (the scoping note, csd-foundations-checked; §3a is the vocabulary decision above, §5 the CSD side); specs/BACKLOG.md row B; Empirical/QM/Uncertainty.lean (commutator_le_two_mul_norm, commutator_shift, stdDev, expectation, robertson_uncertainty); Empirical/QM/WignerArakiYanase.lean (the abstract-tensor interface WAY brick 2 shares, and way_hypotheses_satisfiable, the non-vacuity pattern followed here); specs/future-work.md (MT-1); specs/qm-empirical-tests.md (the twins board). Sources: Ozawa 2003, Phys. Rev. A 67, 042105; Erhart et al. 2012, Nature Physics 8, 185; Rozema et al. 2012, Phys. Rev. Lett. 109, 100404; Branciard 2013, PNAS 110, 6742 (the tight form, not proved here).

The data the inequality needs

structure CSD.Empirical.Ozawa.OzawaData (H : Type u_2) [NormedAddCommGroup H] [InnerProductSpace ℂ H] : Type u_2

The data of an error–disturbance situation: the two observables as they enter (aIn, bIn) and as the interaction leaves them (aOut the meter read-back, bOut the disturbed observable), all symmetric, with aOut and bOut commuting.

In a measurement model (K, σ_probe, U, M) this is A ⊗ 1, B ⊗ 1, U†(1 ⊗ M)U, U†(B ⊗ 1)U, and commute_out holds because conjugation by one U preserves the commutation of 1 ⊗ M with B ⊗ 1. The tensor structure is not needed anywhere else, so it is not assumed here.

• aIn : Module.End ℂ H

  The measured observable as it enters.

• bIn : Module.End ℂ H

  The second observable as it enters.

• aOut : Module.End ℂ H

  The meter read-back: what the apparatus reports for aIn.

• bOut : Module.End ℂ H

  The second observable after the interaction.

• aIn_symm : LinearMap.IsSymmetric self.aIn

  Observables are symmetric.

• bIn_symm : LinearMap.IsSymmetric self.bIn

  Observables are symmetric.

• aOut_symm : LinearMap.IsSymmetric self.aOut

  The read-back is symmetric.

• bOut_symm : LinearMap.IsSymmetric self.bOut

  The disturbed observable is symmetric.

• commute_out : self.aOut * self.bOut = self.bOut * self.aOut

  ★ The load-bearing hypothesis. The read-back and the disturbed observable commute — in a measurement model, because they are conjugates by the same unitary of the commuting 1 ⊗ M and B ⊗ 1. Everything else in this file is formal; this is where the physics is.

noncomputable def CSD.Empirical.Ozawa.OzawaData.noiseOp {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (d : OzawaData H) : Module.End ℂ H

The noise operator N = A_out − A_in.

Equations

• d.noiseOp = d.aOut - d.aIn

noncomputable def CSD.Empirical.Ozawa.OzawaData.disturbOp {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (d : OzawaData H) : Module.End ℂ H

The disturbance operator D = B_out − B_in.

Equations

• d.disturbOp = d.bOut - d.bIn

noncomputable def CSD.Empirical.Ozawa.OzawaData.error {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (d : OzawaData H) (Ψ : H) : ℝ

Ozawa's error ε(A) = ‖(A_out − A_in) Ψ‖.

Equations

• d.error Ψ = ‖d.noiseOp Ψ‖

noncomputable def CSD.Empirical.Ozawa.OzawaData.disturbance {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (d : OzawaData H) (Ψ : H) : ℝ

Ozawa's disturbance η(B) = ‖(B_out − B_in) Ψ‖.

Equations

• d.disturbance Ψ = ‖d.disturbOp Ψ‖

theorem CSD.Empirical.Ozawa.OzawaData.error_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (d : OzawaData H) (Ψ : H) : 0 ≤ d.error Ψ

theorem CSD.Empirical.Ozawa.OzawaData.disturbance_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (d : OzawaData H) (Ψ : H) : 0 ≤ d.disturbance Ψ

theorem CSD.Empirical.Ozawa.OzawaData.noiseOp_symm {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (d : OzawaData H) : LinearMap.IsSymmetric d.noiseOp

theorem CSD.Empirical.Ozawa.OzawaData.disturbOp_symm {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (d : OzawaData H) : LinearMap.IsSymmetric d.disturbOp

theorem CSD.Empirical.Ozawa.OzawaData.error_sq_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (d : OzawaData H) (Ψ : H) : d.error Ψ ^ 2 = (inner ℂ Ψ ((d.noiseOp * d.noiseOp) Ψ)).re

The norm definition agrees with Ozawa's quadratic one: ε(A)² = ⟪Ψ, (A_out − A_in)² Ψ⟫. (Real part taken because the inner product is ℂ-valued; symmetry makes it real.)

theorem CSD.Empirical.Ozawa.OzawaData.disturbance_sq_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (d : OzawaData H) (Ψ : H) : d.disturbance Ψ ^ 2 = (inner ℂ Ψ ((d.disturbOp * d.disturbOp) Ψ)).re

Likewise for the disturbance: η(B)² = ⟪Ψ, (B_out − B_in)² Ψ⟫.

The algebraic identity: the fourth term vanishes

theorem CSD.Empirical.Ozawa.ozawa_commutator_identity {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (d : OzawaData H) : d.aIn * d.bIn - d.bIn * d.aIn = -(d.aIn * d.disturbOp - d.disturbOp * d.aIn) - (d.noiseOp * d.bIn - d.bIn * d.noiseOp) - (d.noiseOp * d.disturbOp - d.disturbOp * d.noiseOp)

★ The identity the theorem rests on. With N = A_out − A_in and D = B_out − B_in, expanding [A_out, B_out] gives four summands — and the left-hand side is zero by commute_out, so

[A_in, B_in] = −[A_in, D] − [N, B_in] − [N, D].

Each remaining commutator pairs a measurement quantity with a preparation quantity, which is exactly the shape of Ozawa's three terms. Without the commutation the residue is [A_out, B_out], a term containing neither ε nor η, and no bound in those quantities can follow.

The relation

theorem CSD.Empirical.Ozawa.ozawa_error_disturbance {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (d : OzawaData H) (Ψ : H) : d.error Ψ * d.disturbance Ψ + d.error Ψ * Uncertainty.stdDev d.bIn Ψ + Uncertainty.stdDev d.aIn Ψ * d.disturbance Ψ ≥ 1 / 2 * ‖inner ℂ Ψ ((d.aIn * d.bIn - d.bIn * d.aIn) Ψ)‖

★★ Ozawa's universally valid error–disturbance relation (Ozawa 2003).

ε(A)·η(B) + ε(A)·σ(B) + σ(A)·η(B) ≥ ½ |⟪Ψ, [A_in, B_in] Ψ⟫|

Three Cauchy–Schwarz bounds on the three terms of ozawa_commutator_identity, after centring A_in and B_in (which does not move the commutator). Each term pairs a measurement quantity with a preparation quantity; the pure-preparation product σ(A)·σ(B) appears in none of them, which is why this neither implies nor follows from Robertson.

Non-vacuity, and the two-term variant

way_hypotheses_satisfiable is the pattern followed here: exhibit the data, and exhibit it where the statement has content. What would make the relation vacuous is a vanishing right-hand side — ⟪Ψ,[A_in,B_in]Ψ⟫ = 0 leaves 0 ≤ (nonneg). It is NOT ε = 0: that is the sharpest case, an exact measurement forcing disturbance, and it is exactly the case exhibited below.

⚠️ This inhabits OzawaData, which is what the theorem quantifies over. A full measurement-model instantiation — probe space, U, and A_out = U†(1 ⊗ M)U derived rather than posited — is not built here; specs/ozawa-scoping.md §3a records why the module is stated at the OzawaData level in the first place.

noncomputable def CSD.Empirical.Ozawa.yPlus : EuclideanSpace ℂ (Fin 2)

The +1 eigenvector of σ_y, unnormalised: (1, i).

Equations

• CSD.Empirical.Ozawa.yPlus = !₂[1, Complex.I]

theorem CSD.Empirical.Ozawa.sigmaZ_isHermitian : MerminPeres.sigmaZ.IsHermitian

theorem CSD.Empirical.Ozawa.sigmaX_isHermitian : MerminPeres.sigmaX.IsHermitian

noncomputable def CSD.Empirical.Ozawa.zxWitness : OzawaData (EuclideanSpace ℂ (Fin 2))

The witness: A_in = σ_z measured exactly (A_out = σ_z, so ε = 0), with B_in = σ_x disturbed to B_out = σ_z. commute_out is immediate because A_out and B_out are the same operator.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CSD.Empirical.Ozawa.zxWitness_error (Ψ : EuclideanSpace ℂ (Fin 2)) : zxWitness.error Ψ = 0

The measurement is exact: ε(σ_z) = 0.

theorem CSD.Empirical.Ozawa.zxWitness_commutator_ne_zero : inner ℂ yPlus ((zxWitness.aIn * zxWitness.bIn - zxWitness.bIn * zxWitness.aIn) yPlus) = 4 * Complex.I

★ Non-vacuity: the right-hand side is nonzero. ⟪y₊, [σ_z, σ_x] y₊⟫ = 4i, so the bound ozawa_error_disturbance asserts at this datum is a strictly positive lower bound, not 0 ≤ 0.

theorem CSD.Empirical.Ozawa.ozawa_two_term_false : ¬∀ (H : Type) (x : NormedAddCommGroup H) (x_1 : InnerProductSpace ℂ H) (d : OzawaData H) (Ψ : H), d.error Ψ * d.disturbance Ψ + d.error Ψ * Uncertainty.stdDev d.bIn Ψ ≥ 1 / 2 * ‖inner ℂ Ψ ((d.aIn * d.bIn - d.bIn * d.aIn) Ψ)‖

★ The two-term variant is false. Dropping σ(A)·η(B) from Ozawa's relation leaves ε(A)·η(B) + ε(A)·σ(B) ≥ ½|⟪Ψ,[A_in,B_in]Ψ⟫|, which the witness refutes: its left-hand side is 0 (the measurement is exact) while the right-hand side is 2.

This is not a refutation of the naive Heisenberg form ε·η ≥ ½|⟪[A,B]⟫| — that needs ε and η computed inside a measurement model, and is deliberately out of scope (specs/ozawa-scoping.md §2). It does show that the third term is load-bearing.