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. Since
2026-09-11 the ontic origin of the bit-flip channel is a theorem
(Empirical/CSD/QEC/ThreeQubit.lean, bitFlipFlow_traceRight_barycenter: the channel is the
environment marginal of a Σ-flow), so csd_qec_decoherence_corrected carries no bundle.
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ⱼ.
The code projector fixes the logical states, as a mulVec identity.
The encoded density is supported on the code: P₀ |ψ_L⟩⟨ψ_L| P₀ = |ψ_L⟩⟨ψ_L|.
★★ Syndrome-conditioned recovery corrects the mixed post-error state, as one channel. For
every single-error mixture N_q = ∑ₖ qₖ Eₖ · Eₖ on the register (qₖ ≥ 0, ∑ qₖ = 1), the
recovery channel R — project onto the syndrome subspace, apply the correction it names — returns
the encoded density: R (N_q |ψ_L⟩⟨ψ_L|) = |ψ_L⟩⟨ψ_L|. This is the end-to-end statement the
branch-by-branch recover_channel_compose_error_on_code lacked: one CPTP map, the whole mixed
error, exact.
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).syndrome-conditioned recovery as one channel on the mixed state (2026-09-12) — for every single-error mixture
N_q = ∑ₖ qₖ Eₖ · Eₖon the register, the recovery channelR = ∑ₖ Eₖ Pₖ · Pₖ Eₖ(QM/QEC/SyndromeRecovery.lean) returns the encoded density from the mixed post-error state:R (N_q |ψ_L⟩⟨ψ_L|) = |ψ_L⟩⟨ψ_L|(syndrome_recovery_corrects_mixed).
Honest scope. Items 3–4 are the correction of the discretised X Kraus branch, one branch at
a time; item 5 is the end-to-end statement for the whole single-error CPTP map, with the recovery
as a sum of syndrome-projector-conditioned corrections. The independent-noise channel
(bit-flip_p)^{⊗3} itself (its double- and triple-flip branches are mis-corrected, so the code
corrects it only to first order: 3p² − 2p³ residual) is
QM/QEC/IndependentNoise.lean (recoveryChannel_apply_indepFlipChannel_apply) and its Σ-flow
CSD/QEC/IndependentNoiseFlow.lean. 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, branch by branch and (2026-09-12) as one channel
on the whole mixed single-error state (syndrome_recovery_corrects_mixed, the last conjunct;
see qec_corrects_decoherence). The ontic origin of the error channel — the bit-flip channel as
the environment marginal of a Σ-flow — is bitFlipFlow_traceRight_barycenter
(Empirical/CSD/QEC/ThreeQubit.lean, 2026-09-11); the former CSDThreeQubitBundle binder is
gone.