Empirical/CSD: the einselection commutation criterion ([P, H_int] = 0)

Category: 6-Local (the open-system / decoherence stratum of D1 — the Hamiltonian-level einselection criterion on the LF6-B machinery).

Build 15a (Empirical/CSD/Einselection.lean) proved decoherence is basis-selective: the de-isolation channel's output is diagonal in exactly one basis (up to degeneracy). What it deliberately did not model — its honest-scope note says so — is the Hamiltonian-level account of which observable an interaction leaves intact. That is Zurek's einselection criterion: the pointer observable is the one the interaction Hamiltonian commutes with, hence does not disturb. This module proves the criterion.

The criterion

For an interaction H_int (Hermitian) with unitary flow U(t) = exp (t • (−i • H_int)) (intFlow), commutation [P, H_int] = 0 makes P a constant of the interaction motion:

• ★ pointer_invariant_of_commute — Heisenberg invariance U(t)ᴴ P U(t) = P;
• pointer_population_conserved — tr (P · U ρ Uᴴ) = tr (P · ρ) for every state ρ and every time: pointer records do not degrade under the interaction;
• compress_conj_comm / sector_state_invariant — compressing to the P-sector commutes with the flow, so a state in a pointer sector stays in it;
• ★★ pointer_basis_of_commuting — the packaged criterion, for a family P : ι → Matrix _ _ ℂ with ∀ i, Commute (P i) H_int: all three conclusions, every member, every time. Commutation alone is load-bearing — no projection or positivity hypothesis is needed for any of the three (stronger than the textbook phrasing, which states the criterion for projection-valued pointer observables).

The class of interactions, and coherence survival under the flow

• single_commute_diagonal — every computational projection |eᵢ⟩⟨eᵢ| = Matrix.single i i 1 (outerProduct_single, LF5/DilationFromFlow.lean) commutes with every pointer-diagonal interaction: the criterion holds for the whole class H_int = diagonal (real spectrum), not one instance (pointer_basis_of_diagonal).
• intFlow_diagonal — the flow of a diagonal interaction is the diagonal-phase unitary, computed via Matrix.exp_diagonal.
• ★ coherence_modulus_preserved — under that flow every coherence modulus is exactly preserved: ‖(U ρ Uᴴ) i j‖ = ‖ρ i j‖. The interaction flow alone never dephases the pointer basis; the dephasing of LF6/Decoherence.lean is the unmonitored-environment trace, not the flow. Flow preserves, trace selects — the two halves of einselection, now both theorems.

The contrast: a non-commuting observable is disturbed

Reusing Build 15a's rotated-basis contrast (the Hadamard qmH): rotatedProj = qmH · |e₀⟩⟨e₀| · qmH is a genuine projection (rotatedProj_mul_self) that fails the criterion (rotatedProj_not_commute, against contrastH = diagonal (0, π)), and the flow punishes it maximally: its population in its own eigenstate falls 1 → 0 in one stroke (noncommuting_population_disturbed). ★★ einselection_commutation_contrast bundles the two sides: commuting ⟹ conserved, non-commuting ⟹ disturbed. The pointer basis is the one the interaction does not disturb — computed, not narrated.

Honest scope and residue

The criterion einselects the basis given the interaction: H_int is the measurement context and remains an input, exactly as it is for Bohm and for Everett — no interpretation derives the apparatus Hamiltonian from first principles, and this module does not either. What is discharged is the Hamiltonian-level criterion (parity with the field's accepted einselection answer, machine-checked); what remains is the D1 obligation, untouched here (RecordLayer/MomentMapRace.lean, specs/q12-fibre-mechanism-scoping.md). This supersedes in part the Build 15a honest-scope note ("the basis is the de-isolation's by construction"): given H_int, the basis is now the commutation-selected one, a theorem; the interaction itself is still posited.

References

specs/future-work.md; Empirical/CSD/Einselection.lean (Build 15a — the channel-level basis selectivity this completes); LF6/Decoherence.lean (decohereReduced, the trace half); Mathlib/Analysis/Matrix/StoneC1.lean (Matrix.StoneC1.exp_smul_unitary); LF5/DilationFromFlow.lean (outerProduct_single). All exports are foundational-triple-only.

The interaction flow

noncomputable def CSD.Empirical.CSDBridge.Einselection.intFlow {N : ℕ} (Hint : Matrix (Fin N) (Fin N) ℂ) (t : ℝ) : Matrix (Fin N) (Fin N) ℂ

The interaction flow of a (Hermitian) interaction Hint: U(t) = exp (t • (−i • Hint)), the one-parameter unitary group Hint generates.

Equations

• CSD.Empirical.CSDBridge.Einselection.intFlow Hint t = NormedSpace.exp (t • -Complex.I • Hint)

theorem CSD.Empirical.CSDBridge.Einselection.intFlow_def {N : ℕ} (Hint : Matrix (Fin N) (Fin N) ℂ) (t : ℝ) : intFlow Hint t = NormedSpace.exp (t • -Complex.I • Hint)

theorem CSD.Empirical.CSDBridge.Einselection.neg_I_smul_skew {N : ℕ} {Hint : Matrix (Fin N) (Fin N) ℂ} (hH : Hint.IsHermitian) : star (-Complex.I • Hint) = -(-Complex.I • Hint)

For Hermitian Hint the generator −i • Hint is skew-Hermitian.

theorem CSD.Empirical.CSDBridge.Einselection.smul_neg_I_skew {N : ℕ} {Hint : Matrix (Fin N) (Fin N) ℂ} (hH : Hint.IsHermitian) (t : ℝ) : (t • -Complex.I • Hint).conjTranspose = -(t • -Complex.I • Hint)

For Hermitian Hint the full generator t • (−i • Hint) is skew-Hermitian.

theorem CSD.Empirical.CSDBridge.Einselection.intFlow_zero {N : ℕ} (Hint : Matrix (Fin N) (Fin N) ℂ) : intFlow Hint 0 = 1

The flow at time zero is the identity.

theorem CSD.Empirical.CSDBridge.Einselection.intFlow_conjTranspose_mul {N : ℕ} {Hint : Matrix (Fin N) (Fin N) ℂ} (hH : Hint.IsHermitian) (t : ℝ) : (intFlow Hint t).conjTranspose * intFlow Hint t = 1

The interaction flow is unitary (left inverse): U(t)ᴴ U(t) = 1. Via Matrix.StoneC1.exp_smul_unitary on the skew generator.

theorem CSD.Empirical.CSDBridge.Einselection.intFlow_mul_conjTranspose {N : ℕ} {Hint : Matrix (Fin N) (Fin N) ℂ} (hH : Hint.IsHermitian) (t : ℝ) : intFlow Hint t * (intFlow Hint t).conjTranspose = 1

The interaction flow is unitary (right inverse): U(t) U(t)ᴴ = 1.

theorem CSD.Empirical.CSDBridge.Einselection.commute_intFlow {N : ℕ} {P Hint : Matrix (Fin N) (Fin N) ℂ} (hcomm : Commute P Hint) (t : ℝ) : Commute P (intFlow Hint t)

Commutation with the generator transfers to the flow: [P, Hint] = 0 ⟹ [P, U(t)] = 0 (via Commute.exp_right).

theorem CSD.Empirical.CSDBridge.Einselection.commute_intFlow_conjTranspose {N : ℕ} {P Hint : Matrix (Fin N) (Fin N) ℂ} (hH : Hint.IsHermitian) (hcomm : Commute P Hint) (t : ℝ) : Commute P (intFlow Hint t).conjTranspose

Commutation with the generator also transfers to the adjoint flow: [P, Hint] = 0 ⟹ [P, U(t)ᴴ] = 0 (the adjoint is the reversed flow).

The criterion: commuting pointer observables are constants of the motion

theorem CSD.Empirical.CSDBridge.Einselection.pointer_invariant_of_commute {N : ℕ} {P Hint : Matrix (Fin N) (Fin N) ℂ} (hH : Hint.IsHermitian) (hcomm : Commute P Hint) (t : ℝ) : (intFlow Hint t).conjTranspose * P * intFlow Hint t = P

★ Heisenberg invariance (the einselection criterion). A pointer observable commuting with the interaction is a constant of the interaction motion: U(t)ᴴ P U(t) = P at every time. The interaction does not disturb P — Zurek's criterion for the preferred (pointer) observable, as a theorem.

theorem CSD.Empirical.CSDBridge.Einselection.trace_conj_of_heisenberg_fixed {N : ℕ} {U P ρ : Matrix (Fin N) (Fin N) ℂ} (hfix : U.conjTranspose * P * U = P) : (P * (U * ρ * U.conjTranspose)).trace = (P * ρ).trace

Trace bookkeeping: a Heisenberg-fixed observable has conserved expectation under the corresponding Schrödinger conjugation, by trace cyclicity alone.

theorem CSD.Empirical.CSDBridge.Einselection.pointer_population_conserved {N : ℕ} {P Hint : Matrix (Fin N) (Fin N) ℂ} (hH : Hint.IsHermitian) (hcomm : Commute P Hint) (ρ : Matrix (Fin N) (Fin N) ℂ) (t : ℝ) : (P * (intFlow Hint t * ρ * (intFlow Hint t).conjTranspose)).trace = (P * ρ).trace

Pointer populations are exactly conserved. For every state ρ and every time, tr (P · U(t) ρ U(t)ᴴ) = tr (P · ρ): the record weight in a commuting pointer observable does not degrade under the interaction flow.

theorem CSD.Empirical.CSDBridge.Einselection.compress_conj_comm {N : ℕ} {P Hint : Matrix (Fin N) (Fin N) ℂ} (hH : Hint.IsHermitian) (hcomm : Commute P Hint) (ρ : Matrix (Fin N) (Fin N) ℂ) (t : ℝ) : P * (intFlow Hint t * ρ * (intFlow Hint t).conjTranspose) * P = intFlow Hint t * (P * ρ * P) * (intFlow Hint t).conjTranspose

Sector compression commutes with the interaction flow: P (U ρ Uᴴ) P = U (P ρ P) Uᴴ. Compressing to the pointer sector before or after the interaction is the same operation.

theorem CSD.Empirical.CSDBridge.Einselection.sector_state_invariant {N : ℕ} {P Hint ρ : Matrix (Fin N) (Fin N) ℂ} (hH : Hint.IsHermitian) (hcomm : Commute P Hint) (t : ℝ) (hρ : P * ρ * P = ρ) : P * (intFlow Hint t * ρ * (intFlow Hint t).conjTranspose) * P = intFlow Hint t * ρ * (intFlow Hint t).conjTranspose

Pointer-sector states stay in their sector. If ρ is supported in the P-sector (P ρ P = ρ), so is its image under the interaction flow.

theorem CSD.Empirical.CSDBridge.Einselection.pointer_basis_of_commuting {N : ℕ} {ι : Type u_1} (Hint : Matrix (Fin N) (Fin N) ℂ) (hH : Hint.IsHermitian) (P : ι → Matrix (Fin N) (Fin N) ℂ) (hcomm : ∀ (i : ι), Commute (P i) Hint) : (∀ (i : ι) (t : ℝ), (intFlow Hint t).conjTranspose * P i * intFlow Hint t = P i) ∧ (∀ (i : ι) (t : ℝ) (ρ : Matrix (Fin N) (Fin N) ℂ), (P i * (intFlow Hint t * ρ * (intFlow Hint t).conjTranspose)).trace = (P i * ρ).trace) ∧ ∀ (i : ι) (t : ℝ) (ρ : Matrix (Fin N) (Fin N) ℂ), P i * ρ * P i = ρ → P i * (intFlow Hint t * ρ * (intFlow Hint t).conjTranspose) * P i = intFlow Hint t * ρ * (intFlow Hint t).conjTranspose

★★ The einselection commutation criterion, packaged. For an interaction Hint (Hermitian) and a family of pointer observables P i each commuting with Hint ([P i, H_int] = 0):

1. every P i is a constant of the interaction motion, U(t)ᴴ (P i) U(t) = P i (pointer_invariant_of_commute);
2. every pointer population is exactly conserved in every state, tr (P i · U ρ Uᴴ) = tr (P i · ρ) (pointer_population_conserved);
3. every pointer-sector state stays in its sector (sector_state_invariant).

Coherences in the P-basis survive the H_int flow; a non-commuting observable does not enjoy this (see einselection_commutation_contrast). Commutation alone is load-bearing: no projection hypothesis is required. Residue: the criterion selects the basis given the interaction — H_int is the measurement context and remains an input.

The converse: invariance forces commutation — the criterion is a characterisation

theorem CSD.Empirical.CSDBridge.Einselection.commute_intFlow_of_invariant {N : ℕ} {P Hint : Matrix (Fin N) (Fin N) ℂ} (hH : Hint.IsHermitian) {t : ℝ} (hinv : (intFlow Hint t).conjTranspose * P * intFlow Hint t = P) : P * intFlow Hint t = intFlow Hint t * P

Heisenberg invariance at a time transfers to plain commutation with the flow at that time: U(t)ᴴ P U(t) = P ⟹ P U(t) = U(t) P (left-multiply by U(t) and cancel U Uᴴ = 1).

theorem CSD.Empirical.CSDBridge.Einselection.hasDerivAt_intFlow_zero {N : ℕ} (Hint : Matrix (Fin N) (Fin N) ℂ) : HasDerivAt (fun (t : ℝ) => intFlow Hint t) (-Complex.I • Hint) 0

The derivative of the interaction flow at time zero is its generator −i • Hint.

theorem CSD.Empirical.CSDBridge.Einselection.commute_of_pointer_invariant {N : ℕ} {P Hint : Matrix (Fin N) (Fin N) ℂ} (hH : Hint.IsHermitian) (hinv : ∀ (t : ℝ), (intFlow Hint t).conjTranspose * P * intFlow Hint t = P) : Commute P Hint

★ The converse of the criterion. An observable that is a constant of the interaction motion at every time commutes with the interaction: differentiate P · U(t) = U(t) · P at t = 0 to recover [P, H_int] = 0.

theorem CSD.Empirical.CSDBridge.Einselection.pointer_invariant_iff_commute {N : ℕ} {P Hint : Matrix (Fin N) (Fin N) ℂ} (hH : Hint.IsHermitian) : (∀ (t : ℝ), (intFlow Hint t).conjTranspose * P * intFlow Hint t = P) ↔ Commute P Hint

★★ The einselection criterion is a characterisation. A pointer observable is a constant of the interaction motion at every time iff it commutes with the interaction: the pointer observables of H_int are exactly the commuting ones. Forward: differentiate at t = 0 (commute_of_pointer_invariant); backward: pointer_invariant_of_commute. This upgrades the criterion from sufficient to characterising, which is the form the einselection literature intends.

theorem CSD.Empirical.CSDBridge.Einselection.exists_trace_mul_ne {N : ℕ} {X Y : Matrix (Fin N) (Fin N) ℂ} (hXY : X ≠ Y) : ∃ (ρ : Matrix (Fin N) (Fin N) ℂ), (X * ρ).trace ≠ (Y * ρ).trace

Trace separation: distinct matrices are told apart by some trace pairing (the matrix witness ρ = single j i 1 reads entry (i, j); ρ is a matrix, not necessarily a state — the state-level witness is the N = 2 contrast below).

theorem CSD.Empirical.CSDBridge.Einselection.exists_population_ne_of_not_commute {N : ℕ} {P Hint : Matrix (Fin N) (Fin N) ℂ} (hH : Hint.IsHermitian) (hnc : ¬Commute P Hint) : ∃ (t : ℝ) (ρ : Matrix (Fin N) (Fin N) ℂ), (P * (intFlow Hint t * ρ * (intFlow Hint t).conjTranspose)).trace ≠ (P * ρ).trace

★ A non-commuting observable is disturbed. If [P, H_int] ≠ 0 then at some time some trace-functional detects the change: tr (P · U ρ Uᴴ) ≠ tr (P · ρ). (The witness ρ is a matrix; the concrete state-level disturbance is noncommuting_population_disturbed.) With pointer_population_conserved this separates the commuting from the non-commuting observables at the population level.

The class: pointer-diagonal interactions

theorem CSD.Empirical.CSDBridge.Einselection.single_commute_diagonal {N : ℕ} (i : Fin N) (d : Fin N → ℂ) : Commute (Matrix.single i i 1) (Matrix.diagonal d)

Every computational pointer projection |eᵢ⟩⟨eᵢ| = Matrix.single i i 1 commutes with every diagonal interaction.

theorem CSD.Empirical.CSDBridge.Einselection.single_mul_self {N : ℕ} (i : Fin N) : Matrix.single i i 1 * Matrix.single i i 1 = Matrix.single i i 1

The computational pointer projections are idempotent.

theorem CSD.Empirical.CSDBridge.Einselection.diagonal_ofReal_isHermitian {N : ℕ} (d : Fin N → ℝ) : (Matrix.diagonal fun (i : Fin N) => ↑(d i)).IsHermitian

A real-spectrum diagonal is Hermitian.

theorem CSD.Empirical.CSDBridge.Einselection.pointer_basis_of_diagonal {N : ℕ} (d : Fin N → ℝ) (i : Fin N) : Commute (Matrix.single i i 1) (Matrix.diagonal fun (j : Fin N) => ↑(d j)) ∧ ∀ (t : ℝ), (intFlow (Matrix.diagonal fun (j : Fin N) => ↑(d j)) t).conjTranspose * Matrix.single i i 1 * intFlow (Matrix.diagonal fun (j : Fin N) => ↑(d j)) t = Matrix.single i i 1

★ The criterion holds for the whole class of pointer-diagonal interactions. For every real spectrum d, every computational projection commutes with H_int = diagonal d and is a constant of its flow — the class-level statement of einselection for the computational pointer basis.

theorem CSD.Empirical.CSDBridge.Einselection.intFlow_diagonal {N : ℕ} (d : Fin N → ℝ) (t : ℝ) : intFlow (Matrix.diagonal fun (j : Fin N) => ↑(d j)) t = Matrix.diagonal fun (j : Fin N) => Complex.exp (-(Complex.I * ↑(t * d j)))

The flow of a diagonal interaction is the diagonal-phase unitary diag (e^{−i t d(j)}) (via Matrix.exp_diagonal).

theorem CSD.Empirical.CSDBridge.Einselection.norm_diagonal_phase (r : ℝ) : ‖Complex.exp (-(Complex.I * ↑r))‖ = 1

Each diagonal phase has unit modulus.

theorem CSD.Empirical.CSDBridge.Einselection.coherence_modulus_preserved {N : ℕ} (d : Fin N → ℝ) (t : ℝ) (ρ : Matrix (Fin N) (Fin N) ℂ) (i j : Fin N) : ‖(intFlow (Matrix.diagonal fun (k : Fin N) => ↑(d k)) t * ρ * (intFlow (Matrix.diagonal fun (k : Fin N) => ↑(d k)) t).conjTranspose) i j‖ = ‖ρ i j‖

★ Every coherence modulus survives the interaction flow. Under the flow of any pointer-diagonal interaction, ‖(U ρ Uᴴ) i j‖ = ‖ρ i j‖ for every entry: the flow rotates coherences by phases and destroys none of them. The dephasing of LF6/Decoherence.lean is the unmonitored-environment trace, not the flow — flow preserves, trace selects.

The contrast: a non-commuting observable is disturbed

The other half of einselection, concrete at N = 2, reusing Build 15a's rotated-basis contrast. The interaction contrastH = diag (0, π) is pointer-diagonal; the Hadamard-rotated projection rotatedProj = qmH |e₀⟩⟨e₀| qmH (the |+⟩⟨+| projector) does not commute with it, and its population in its own eigenstate is driven 1 → 0 by the time-one flow — maximal disturbance, against exact conservation for the commuting pointer projections.

noncomputable def CSD.Empirical.CSDBridge.Einselection.contrastH : Matrix (Fin 2) (Fin 2) ℂ

The contrast interaction diag (0, π): pointer-diagonal, Hermitian, generating the time-one flow diag (1, −1) (the Pauli-Z stroke).

Equations

• CSD.Empirical.CSDBridge.Einselection.contrastH = Matrix.diagonal fun (j : Fin 2) => ↑(![0, Real.pi] j)

theorem CSD.Empirical.CSDBridge.Einselection.contrastH_isHermitian : contrastH.IsHermitian

noncomputable def CSD.Empirical.CSDBridge.Einselection.rotatedProj : Matrix (Fin 2) (Fin 2) ℂ

The Hadamard-rotated pointer projection qmH |e₀⟩⟨e₀| qmH — the |+⟩⟨+| projector, Build 15a's rotated basis.

Equations

• CSD.Empirical.CSDBridge.Einselection.rotatedProj = CSD.Empirical.QM.Gates.qmH * Matrix.single 0 0 1 * CSD.Empirical.QM.Gates.qmH

theorem CSD.Empirical.CSDBridge.Einselection.rotatedProj_eq : rotatedProj = (1 / 2) • !![1, 1; 1, 1]

The rotated projection, computed: |+⟩⟨+| = (1/2) !![1,1;1,1].

theorem CSD.Empirical.CSDBridge.Einselection.rotatedProj_mul_self : rotatedProj * rotatedProj = rotatedProj

The rotated observable is a genuine projection (idempotent): non-vacuity that the disturbed observable is a legitimate pointer candidate.

theorem CSD.Empirical.CSDBridge.Einselection.rotatedProj_not_commute : ¬Commute rotatedProj contrastH

The rotated projection fails the commutation criterion: [rotatedProj, contrastH] ≠ 0. The failing entry is (0,1), where the products differ by π/2 ≠ 0.

theorem CSD.Empirical.CSDBridge.Einselection.intFlow_contrastH_one : intFlow contrastH 1 = Matrix.diagonal ![1, -1]

The time-one flow of the contrast interaction is the Pauli-Z stroke diag (1, −1) (via intFlow_diagonal, Complex.exp_pi_mul_I).

theorem CSD.Empirical.CSDBridge.Einselection.noncommuting_population_disturbed : (rotatedProj * rotatedProj).trace = 1 ∧ (rotatedProj * (intFlow contrastH 1 * rotatedProj * (intFlow contrastH 1).conjTranspose)).trace = 0

The non-commuting observable is maximally disturbed. In its own eigenstate (ρ = rotatedProj, population 1), one stroke of the contrast flow drives the rotatedProj-population to 0: tr (Q · U Q Uᴴ) = 0 while tr (Q · Q) = 1. Compare pointer_population_conserved: a commuting observable is conserved in every state, at every time.

theorem CSD.Empirical.CSDBridge.Einselection.einselection_commutation_contrast : (∀ (i : Fin 2) (t : ℝ), (intFlow contrastH t).conjTranspose * Matrix.single i i 1 * intFlow contrastH t = Matrix.single i i 1) ∧ ¬Commute rotatedProj contrastH ∧ rotatedProj * rotatedProj = rotatedProj ∧ (rotatedProj * rotatedProj).trace = 1 ∧ (rotatedProj * (intFlow contrastH 1 * rotatedProj * (intFlow contrastH 1).conjTranspose)).trace = 0

★★ The einselection commutation contrast: the criterion separates. For the pointer-diagonal contrast interaction contrastH = diag (0, π):

1. commuting ⟹ conserved — every computational pointer projection is a constant of the flow, U(t)ᴴ |eᵢ⟩⟨eᵢ| U(t) = |eᵢ⟩⟨eᵢ| (pointer_basis_of_diagonal);
2. the rotated observable fails the criterion — [rotatedProj, contrastH] ≠ 0 (rotatedProj_not_commute), though it is a genuine projection (rotatedProj_mul_self);
3. and is maximally disturbed — its population in its own eigenstate is driven 1 → 0 by one stroke (noncommuting_population_disturbed).

The pointer basis is the one the interaction does not disturb — the field's einselection answer to "why this basis", machine-checked. Residue: the interaction H_int is the measurement context and remains an input.