LF6-3/LF6-4: Bloch-volume contraction — the open-system drift, measured

Category: LF6 (open-system / de-isolation dynamics).

The geometric signature that separates open from closed dynamics, on the two proved qubit dissipators. Closed (unitary) dynamics preserves state-space volume — the corpus carries that side as schrodinger_flow_kahler_symplectomorphism and fubiniStudyMeasure_smul_invariant. This module proves the open side: both canonical dissipators contract Bloch volume, at exactly the same rate e^{-2γt}, and the drift rate is the measurable decoherence rate.

• blochX/Y/Z — Bloch coordinates of a 2×2 matrix (no positivity or normalisation assumed; for a density matrix they are the standard Bloch vector).
• The channel actions in Bloch form: dephasing shrinks the equatorial plane and fixes the axis (blochX/Y/Z_dephasing); damping shrinks the equator at half rate and drifts the axis toward the ground pole (blochX/Y/Z_damping — the z-action is affine, with offset weighted by the trace).
• blochLinearDephasing / blochLinearDamping — the linear parts, with blochVec_dephasing / blochVec_damping proving they ARE the actions (damping up to the trace-weighted pole offset).
• ★★ det_blochLinearDephasing / det_blochLinearDamping — the volume-drift law: both determinants equal e^{-2γt}. T2 dephasing (equator² × 1) and T1 damping (equator × axis, e^{-γt/2}·e^{-γt/2}·e^{-γt}) contract the Bloch ball's volume by the SAME factor — the marginal volume drift is a dissipation invariant, blind to how the contraction is distributed over axes (LF6-3).
• ★ Metrology A4 (LF6-4): bloch_volume_closed (γ·t = 0 ⟹ volume factor 1 — the closed case is drift-free), bloch_volume_lt_one (any γt > 0 is detected), bloch_volume_decay_rate (the initial drift rate is exactly -2γ), and volume_drift_determines_rate (one drift sample at any t > 0 identifies γ). Decoherence is not merely modelled: its rate is an observable of the volume drift.

Honest scope: the two exhibited dissipators only — the general-generator form of the volume-drift law waits on LF6-9's exponential-CP residual (Mathlib-scale, recorded there); the closed-side volume preservation is cited from the pure-state Kähler results, not re-proved at the density level. Cross-references: LF6/LindbladGenerator.lean (both channels are GKSL), LF5/ (the reduced-state framing), specs/future-work.md rows LF6-3/LF6-4.

Bloch coordinates

noncomputable def CSD.LF6.blochX (ρ : Matrix (Fin 2) (Fin 2) ℂ) : ℝ

Bloch x: the real part of the coherence sum.

Equations

• CSD.LF6.blochX ρ = (ρ 0 1 + ρ 1 0).re

noncomputable def CSD.LF6.blochY (ρ : Matrix (Fin 2) (Fin 2) ℂ) : ℝ

Bloch y: the rotated coherence difference.

Equations

• CSD.LF6.blochY ρ = (Complex.I * (ρ 0 1 - ρ 1 0)).re

noncomputable def CSD.LF6.blochZ (ρ : Matrix (Fin 2) (Fin 2) ℂ) : ℝ

Bloch z: the population difference.

Equations

• CSD.LF6.blochZ ρ = (ρ 0 0 - ρ 1 1).re

noncomputable def CSD.LF6.blochVec (ρ : Matrix (Fin 2) (Fin 2) ℂ) : Fin 3 → ℝ

The Bloch vector.

Equations

• CSD.LF6.blochVec ρ = ![CSD.LF6.blochX ρ, CSD.LF6.blochY ρ, CSD.LF6.blochZ ρ]

The channel actions in Bloch form

theorem CSD.LF6.blochX_dephasing (γ t : ℝ) (ρ : Matrix (Fin 2) (Fin 2) ℂ) : blochX (dephasingChannel γ t ρ) = Real.exp (-(γ * t)) * blochX ρ

theorem CSD.LF6.blochY_dephasing (γ t : ℝ) (ρ : Matrix (Fin 2) (Fin 2) ℂ) : blochY (dephasingChannel γ t ρ) = Real.exp (-(γ * t)) * blochY ρ

theorem CSD.LF6.blochZ_dephasing (γ t : ℝ) (ρ : Matrix (Fin 2) (Fin 2) ℂ) : blochZ (dephasingChannel γ t ρ) = blochZ ρ

theorem CSD.LF6.blochX_damping (γ t : ℝ) (ρ : Matrix (Fin 2) (Fin 2) ℂ) : blochX (dampingChannel γ t ρ) = Real.exp (-(γ * t) / 2) * blochX ρ

theorem CSD.LF6.blochY_damping (γ t : ℝ) (ρ : Matrix (Fin 2) (Fin 2) ℂ) : blochY (dampingChannel γ t ρ) = Real.exp (-(γ * t) / 2) * blochY ρ

theorem CSD.LF6.blochZ_damping (γ t : ℝ) (ρ : Matrix (Fin 2) (Fin 2) ℂ) : blochZ (dampingChannel γ t ρ) = Real.exp (-(γ * t)) * blochZ ρ + (1 - Real.exp (-(γ * t))) * ρ.trace.re

The damping z-action is affine: contraction toward the ground pole, with the offset weighted by the trace.

The linear parts and the volume-drift law

noncomputable def CSD.LF6.blochLinearDephasing (γ t : ℝ) : Matrix (Fin 3) (Fin 3) ℝ

The dephasing Bloch superoperator: equatorial contraction, axis fixed.

Equations

• CSD.LF6.blochLinearDephasing γ t = Matrix.diagonal ![Real.exp (-(γ * t)), Real.exp (-(γ * t)), 1]

noncomputable def CSD.LF6.blochLinearDamping (γ t : ℝ) : Matrix (Fin 3) (Fin 3) ℝ

The damping Bloch superoperator (linear part): equatorial contraction at half rate, axis contraction at full rate.

Equations

• CSD.LF6.blochLinearDamping γ t = Matrix.diagonal ![Real.exp (-(γ * t) / 2), Real.exp (-(γ * t) / 2), Real.exp (-(γ * t))]

theorem CSD.LF6.blochVec_dephasing (γ t : ℝ) (ρ : Matrix (Fin 2) (Fin 2) ℂ) : blochVec (dephasingChannel γ t ρ) = (blochLinearDephasing γ t).mulVec (blochVec ρ)

The dephasing Bloch action IS the linear map.

theorem CSD.LF6.blochVec_damping (γ t : ℝ) (ρ : Matrix (Fin 2) (Fin 2) ℂ) : blochVec (dampingChannel γ t ρ) = (blochLinearDamping γ t).mulVec (blochVec ρ) + ((1 - Real.exp (-(γ * t))) * ρ.trace.re) • ![0, 0, 1]

The damping Bloch action is the linear map plus the trace-weighted pole offset.

theorem CSD.LF6.det_blochLinearDephasing (γ t : ℝ) : (blochLinearDephasing γ t).det = Real.exp (-(2 * γ * t))

★★ The dephasing volume-drift law: T2 contracts Bloch volume by exactly e^{-2γt} (equator² × fixed axis).

theorem CSD.LF6.det_blochLinearDamping (γ t : ℝ) : (blochLinearDamping γ t).det = Real.exp (-(2 * γ * t))

★★ The damping volume-drift law: T1 contracts Bloch volume by exactly the SAME e^{-2γt} (half-rate equator × full-rate axis) — the volume drift is a dissipation invariant, blind to how the contraction is distributed over axes.

Metrology A4: the drift is the observable (LF6-4)

theorem CSD.LF6.bloch_volume_closed {γ t : ℝ} (h : γ * t = 0) : (blochLinearDephasing γ t).det = 1

The closed case is drift-free: at γ·t = 0 the volume factor is 1.

theorem CSD.LF6.bloch_volume_lt_one {γ t : ℝ} (h : 0 < γ * t) : (blochLinearDephasing γ t).det < 1

★ Openness is detected: any γ·t > 0 strictly contracts the volume.

theorem CSD.LF6.bloch_volume_decay_rate (γ : ℝ) : HasDerivAt (fun (t : ℝ) => (blochLinearDephasing γ t).det) (-(2 * γ)) 0

★ The initial drift rate is the decoherence rate: the volume factor's derivative at t = 0 is exactly -2γ — measuring the drift measures γ.

theorem CSD.LF6.volume_drift_determines_rate {γ₁ γ₂ t : ℝ} (ht : 0 < t) (h : (blochLinearDephasing γ₁ t).det = (blochLinearDephasing γ₂ t).det) : γ₁ = γ₂

★ One drift sample identifies the rate: equal volume factors at any single t > 0 force equal γ — the drift is a faithful observable of the decoherence rate.