Empirical/CSD: QEC corrects a decoherence error (Build 15b) #
Category: 3-Local (QM-operational) with a 6-Local (open-system / D1) gating note. The
open-system/decoherence companion to Build 15a (Empirical/CSD/Einselection.lean).
A single-qubit error is not a coherent rotation but a decoherence channel: a CPTP map arising as the partial trace of a system-environment unitary (Stinespring). The three-qubit bit-flip code corrects the correctable (single-qubit) branch of that error. This file states the decoherence content + the correction + the unprotected-qubit contrast, and the honest CSD reading with the ontic-volume gating.
What is QM-operational (discharged here) #
- The error is a decoherence channel. The K2 bit-flip channel
Φ(ρ) = (1−p)·ρ + p·X ρ X(Empirical.QM.QEC.bitFlipChannel) is aChannel(CPTP:bitflip_error_cptpreusesChannel.apply_trace/Channel.apply_posSemidef). Its Stinespring / partial-trace origin isbitflip_error_is_decoherence:Φ(ρ) = traceRight (V ρ Vᴴ)withVᴴ V = 1(Channel.apply_eq_traceRight_stinespring+Channel.stinespringIsom_isom). The error is environmental entanglement traced away. - The correction is exact on the code (closed form, weight 1).
- density / channel level (deterministic branch):
recover ∘ error = idon a bare qubit for theXKraus branch (qubit_recover_compose_bitflip), and on the code (three_qubit_recover_density:Xⱼ (Xⱼ ρ Xⱼᴴ) Xⱼᴴ = ρ). - vector level: re-applying the syndrome-identified
Xⱼrestores the codeword, routed throughEmpirical.QM.QEC.bitflip_recovers(the headlineqec_corrects_decoherence).
- density / channel level (deterministic branch):
- The unprotected qubit decoheres (non-vacuity). The SAME channel genuinely corrupts a
bare qubit:
bitFlipChannel_corrupts_bare_qubitshowsΦ(|0⟩⟨0|) ≠ |0⟩⟨0|for0 < p(the(1,1)entry moves top). Decoherence damages the unprotected qubit; the code reverses it on the codespace. Cf. 15a's purity-drop witnessdecohere_purity_lt_one_*.
What is ontic Σ-volume (GATED, not discharged here) #
The CSD-ontic reading is: decoherence = system→environment Σ-volume leakage (the partial
trace), and QEC restores the lost volume for correctable errors. The full ontic
Σ-volume / partial-trace-volume-loss ORIGIN needs Σ_env, the entangled joint Liouville
flow on Σ_sys × Σ_env, and partial trace on Σ. That is the entangled-tier debt (LF6 /
D1), gated and NOT discharged here (see LF5/SyndromeFlow.lean's identical gating and
Empirical/CSD/QEC/ThreeQubit.lean). What is dischargeable now is the channel/operational
decoherence (the CPTP map + its Stinespring dilation) + the syndrome recovery. The
csd_qec_decoherence_corrected transport carries a CSDThreeQubitBundle whose ontic
realisability is load-bearing, externally supplied, undischarged.
All exports are foundational-triple-only (off busch_effect_gleason): concrete Matrix
algebra over the K2 Channel / Stinespring machinery.
(1) The error as a decoherence channel: CPTP + Stinespring / partial-trace origin #
The bit-flip error is CPTP (a genuine quantum channel): trace-preserving and
positivity-preserving, reusing the K2 Channel properties. So the error maps density
operators to density operators.
The error is decoherence (Stinespring / partial-trace origin). The bit-flip channel
is the environment-trace of an isometric system-environment dilation:
Φ(ρ) = traceRight (V ρ Vᴴ) with V = stinespringIsom Φ an isometry (Vᴴ V = 1). This is
the "error = trace away the environment of a joint unitary" content: decoherence as
environmental entanglement averaged out. Reuses Channel.apply_eq_traceRight_stinespring
and Channel.stinespringIsom_isom (K2).
(2) The correction: recover ∘ error = identity (closed form) #
Conjugation by a self-inverse matrix is undone by a second conjugation:
X (X ρ X) X = ρ when X X = 1. The algebraic core of "re-apply the identified error".
Deterministic-branch recovery on a bare qubit: recover ∘ error = id. The
nontrivial Kraus branch of the bit-flip error is the unitary conjugation ρ ↦ X ρ Xᴴ
(unitaryChannel pX); applying it twice is the identity, since X is self-inverse. So the
deterministic single-qubit bit-flip is perfectly reversed by re-applying X.
Self-adjointness of the three-qubit error operators #
X₁ = X ⊗ I ⊗ I is self-adjoint.
X₂ = I ⊗ X ⊗ I is self-adjoint.
X₃ = I ⊗ I ⊗ X is self-adjoint.
Generic self-inverse-conjugation-undone identity for Xⱼ (NOT code-specific): for any
operator ρ on the three-qubit space, Xⱼ (Xⱼ ρ Xⱼᴴ) Xⱼᴴ = ρ. This is the algebraic fact
conj_self_inv instantiated at the self-inverse Xⱼ; it is universally quantified over ρ
(true even for Xⱼ := I), so it carries NO code-specific content by itself. The code-specific
correction lives in recover_channel_compose_error_on_code (channel level, on the encoded
density, one Hilbert space) + error_moves_codeword (the error genuinely acts) and
bitflip_recovers (the syndrome-identified vector recovery).
The in-code channel-correction bridge (one Hilbert space) #
X₁ is unitary: X₁ᴴ X₁ = 1.
X₂ is unitary: X₂ᴴ X₂ = 1.
X₃ is unitary: X₃ᴴ X₃ = 1.
The in-code channel-correction bridge: recoverⱼ ∘ errorⱼ = id on the ENCODED density,
in ONE Hilbert space. The correctable single-qubit branch of the bit-flip error is lifted to
qubit j of the code as the unitary CHANNEL unitaryChannel Xⱼ (the same K2 channel formalism
as the decoherence-origin conjunct, not a bare matrix identity). Composing the error channel
with the syndrome-identified recovery channel unitaryChannel Xⱼ (Xⱼ self-inverse) returns
the encoded density encodeDensity a b = |ψ_L⟩⟨ψ_L| exactly. This is the genuine "the channel
acting on the encoded state is corrected" statement: channel level, on the actual codeword
density, one space, specialised to the real Xⱼ. Non-vacuity (the error genuinely displaces
the encoded state) is error_moves_codeword. Routed through conj_self_inv / Xⱼ_mul_Xⱼ.
Non-vacuity: the error genuinely acts on the encoded state. The X₁ error moves the
codeword |000⟩ (logical 1 0): X₁ · |000⟩ = |100⟩ ≠ |000⟩ (they differ at coordinate
(0,0,0), value 0 vs 1). So recover_channel_compose_error_on_code is not vacuous: it
reverses an error that actually displaces the encoded state, not the trivial Xⱼ := I.
Density-level non-vacuity, co-located with the bridge. The X₁ error channel genuinely
moves the encoded density: (unitaryChannel X₁).apply (encodeDensity 1 0) ≠ encodeDensity 1 0
(they differ at the (0,0,0),(0,0,0) diagonal entry, 0 vs 1). This puts the "error acts /
recovery undoes" pair at the same channel/density level as
recover_channel_compose_error_on_code, so the on-code correction reverses an error that
actually displaces the encoded density, not the trivial Xⱼ := I.
(3) Contrast: the unprotected (bare) qubit genuinely decoheres #
The bare qubit density |0⟩⟨0|.
Equations
- CSD.Empirical.CSDBridge.QECDecoherence.qubitZero = !![1, 0; 0, 0]
Instances For
The bit-flip channel moves the |1⟩ population of a bare qubit. The (1,1) entry of
Φ(|0⟩⟨0|) is p (it was 0): Φ(|0⟩⟨0|) = diag(1−p, p). Computed via bitFlipChannel_apply
and X |0⟩⟨0| X = |1⟩⟨1|.
The unprotected qubit decoheres (non-vacuity). For 0 < p the bit-flip channel is NOT
the identity on the bare qubit |0⟩⟨0|: Φ(|0⟩⟨0|) ≠ |0⟩⟨0| (the (1,1) entry moves from
0 to p). So the error genuinely acts; the correction theorems above are non-trivial. The
same channel that damages the unprotected qubit is exactly reversed on the codespace.
Concrete non-vacuity witness at p = 1/2: the bit-flip channel is not the identity on the
bare qubit |0⟩⟨0|.
(2'+) The QEC headline: decoherence error, identifiable, corrected #
QEC corrects the (correctable branch of the) decoherence error on the encoded state (the
headline). For the three-qubit bit-flip code on ψ_L = a|000⟩ + b|111⟩, any 1-qubit density
ρ, the four conjuncts:
- decoherence origin — the single-qubit error is the Stinespring partial trace of a
system-environment isometry:
Φ(ρ) = traceRight (V ρ Vᴴ)withVᴴ V = 1(bitflip_error_is_decoherence); - identifiability — the four errors
{I, X₁, X₂, X₃}give the distinct syndromes(+,+),(−,+),(−,−),(+,−)(three_qubit_syndromes_distinct), so the syndrome measurement pins down which qubit flipped; - in-code channel correction (the conjunct that earns the name) — the correctable
single-qubit error lifted to qubit
jof the code as the CHANNELunitaryChannel Xⱼ, composed with the recovery channel, is the IDENTITY on the ENCODED densityencodeDensity a b = |ψ_L⟩⟨ψ_L|, in ONE Hilbert space (recover_channel_compose_error_on_code). This is the genuine "channel acting on the encoded state is corrected" statement; it is non-vacuous (error_moves_codeword: the error genuinely displaces|000⟩); - vector recovery (syndrome-identified) —
Xⱼ (Xⱼ ψ_L) = ψ_L(bitflip_recovers).
Honest scope (correctable / discrete branch). What is formalised is the correction of the
discretised X Kraus branch (the standard QEC error-discretisation): the deterministic
single-qubit bit-flip, perfectly reversed (weight 1). The FULL mixed channel
Φ = (1−p)·I + p·X corrected END-TO-END via syndrome-conditioned recovery — i.e. the recovery
channel as a sum of syndrome-projector-conditioned corrections, R(ρ) = ∑_s Pₛ-conditioned Xₛ,
giving recover ∘ Φ ∘ encode = encode for the whole CPTP map — is the deeper statement and is
NOT formalised here. QM-operational; the ontic Σ-volume-loss origin of the partial trace is
gated to LF6 (see the module docstring and csd_qec_decoherence_corrected).
(4) The CSD reading + entangled-tier gating #
TRANSPORT + GATING: QEC corrects the decoherence error, in the CSD reading. For any
CSD three-qubit-code bundle on a SectorData D, the operational headline
qec_corrects_decoherence holds: the single-qubit error is a decoherence channel (Stinespring
partial trace of a joint isometry), the four errors are syndrome-distinct, and recovery is
exact on the codeword.
CSD reading. Decoherence = system→environment Σ-volume leakage (the partial trace V ↦ traceRight (V · Vᴴ)); QEC restores the lost volume for the correctable single-qubit branch.
The conservative joint flow is Liouville (hΦ_pres); the loss is on the system marginal only.
Status: load-bearing, externally supplied, undischarged. The ontic Σ-volume / partial-
trace-volume-loss ORIGIN needs Σ_env, the entangled joint Liouville flow on Σ_sys × Σ_env,
and partial trace on Σ — the entangled-tier / D1 debt (LF6), gated and NOT discharged
here (Φ = id in every concrete SectorData). What is discharged is the channel/operational
decoherence + the in-code channel correction of the correctable branch (the full mixed-channel
syndrome-conditioned recovery is the deeper unformalised statement; see
qec_corrects_decoherence). The CSDThreeQubitBundle carries the ontic realisability as an
externally-supplied obligation (see Empirical/CSD/QEC/ThreeQubit.lean,
BRIDGE-OBLIGATIONS.md).