Empirical/CSD: the three-qubit register ⊗ environment as one Σ-flow, and QEC on Σ

Category: 3-Local (CSD-side companion to Empirical/QM/QEC/RegisterDilation.lean; closes the register ⊗ environment residue of Empirical/CSD/QEC/ThreeQubit.lean).

QEC/ThreeQubit.lean produced the one-qubit bit-flip channel from a Σ-flow on qubit ⊗ qubit (bitFlipFlow_traceRight_barycenter) and read the code and the syndrome as regions of Σ. QM/QEC/SyndromeRecovery.lean then made the syndrome-conditioned recovery one channel on the mixed state. This file puts the pieces on the whole register:

• registerFlow q — the projective action of the register's joint unitary U_q (QM/QEC/RegisterDilation.lean) on ℂℙ³¹, the joint projective space of the three-qubit register ⊗ the four-level "which-error" environment; a flow of the corpus's cpSectorData over ℂℙ³¹, lifting U_q with no hypothesis (isUnitaryLift_registerFlow, through the canonical measurable unit section);
• ★★ registerFlow_traceRight_barycenter — the register's single-error channel is the environment marginal of the joint Σ-flow: for a preparation that is a product with the environment ready, the reduced density operator of the flowed preparation is singleFlipChannel q applied to the register's density operator;
• ★★★ registerFlow_recovery — QEC on Σ, end to end: if the register preparation lives in the code region (P₀ (rep x) = rep x a.e.), then the syndrome-conditioned recovery channel applied to the environment marginal of the flowed preparation returns the register's density operator. The error is the Σ-flow's leak into the environment; the syndrome measurement is the projective measurement whose outcomes are the four disjoint error regions of Σ (syndromeProj_fixes_errorRegion); the recovery undoes the leak exactly.

The independent-noise channel (bit-flip_p)^{⊗3} — whose double- and triple-flip branches the code mis-corrects into the logical flip — is Empirical/CSD/QEC/IndependentNoiseFlow.lean (indepFlow_recovery: the 3p² − 2p³ residual); singleFlipChannel is its correctable part with free weights. What is not here: a Hamiltonian generating U_q (the flow is the time-one map of the projective action, as for bitFlipFlow).

Source

Shor 1995, Phys. Rev. A 52, R2493; Knill–Laflamme 1997, Phys. Rev. A 55, 900.

The joint index as Fin 32, and the flow on ℂℙ³¹

def CSD.Empirical.CSDBridge.QEC.registerEquiv : (Fin 2 × Fin 2 × Fin 2) × Fin 4 ≃ Fin 32

The joint index (register) × (environment) = (Fin 2 × Fin 2 × Fin 2) × Fin 4 as Fin 32.

Equations

• CSD.Empirical.CSDBridge.QEC.registerEquiv = ((((Equiv.refl (Fin 2)).prodCongr finProdFinEquiv).trans finProdFinEquiv).prodCongr (Equiv.refl (Fin 4))).trans finProdFinEquiv

noncomputable def CSD.Empirical.CSDBridge.QEC.registerU32 (q : Fin 4 → ℝ) (hq0 : ∀ (k : Fin 4), 0 ≤ q k) (hq1 : ∑ k : Fin 4, q k = 1) : ↥(Matrix.unitaryGroup (Fin 32) ℂ)

The register's joint unitary as an element of U(32), reindexed to Fin 32.

Equations

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

theorem CSD.Empirical.CSDBridge.QEC.registerU32_val (q : Fin 4 → ℝ) (hq0 : ∀ (k : Fin 4), 0 ≤ q k) (hq1 : ∑ k : Fin 4, q k = 1) : ↑(registerU32 q hq0 hq1) = (Matrix.reindex registerEquiv registerEquiv) (QM.QEC.registerUnitary q hq0 hq1)

noncomputable def CSD.Empirical.CSDBridge.QEC.registerFlow (q : Fin 4 → ℝ) (hq0 : ∀ (k : Fin 4), 0 ≤ q k) (hq1 : ∑ k : Fin 4, q k = 1) : LF4.CPN 32 → LF4.CPN 32

The register's de-isolation flow on ℂℙ³¹: the projective action of U_q. A flow of the corpus's cpSectorData (Σ = P = ℂℙ³¹, π = id).

Equations

• CSD.Empirical.CSDBridge.QEC.registerFlow q hq0 hq1 x = CSD.Empirical.CSDBridge.QEC.registerU32 q hq0 hq1 • x

theorem CSD.Empirical.CSDBridge.QEC.measurable_registerFlow (q : Fin 4 → ℝ) (hq0 : ∀ (k : Fin 4), 0 ≤ q k) (hq1 : ∑ k : Fin 4, q k = 1) : Measurable (registerFlow q hq0 hq1)

noncomputable def CSD.Empirical.CSDBridge.QEC.registerRep : LF4.CPN 32 → EuclideanSpace ℂ ((Fin 2 × Fin 2 × Fin 2) × Fin 4)

The joint representative: the canonical unit section of ℂℙ³¹, transported to the joint index.

Equations

• CSD.Empirical.CSDBridge.QEC.registerRep x = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ CSD.Empirical.CSDBridge.QEC.registerEquiv).symm (Projectivization.unitSection x)

theorem CSD.Empirical.CSDBridge.QEC.registerRep_norm (x : LF4.CPN 32) : ‖registerRep x‖ = 1

theorem CSD.Empirical.CSDBridge.QEC.measurable_registerRep : Measurable registerRep

theorem CSD.Empirical.CSDBridge.QEC.isUnitaryLift_registerFlow (p₀ : LF4.CPN 32) (q : Fin 4 → ℝ) (hq0 : ∀ (k : Fin 4), 0 ≤ q k) (hq1 : ∑ k : Fin 4, q k = 1) : LF2.IsUnitaryLift (LF4.cpSectorData p₀) (registerFlow q hq0 hq1) registerRep (QM.QEC.registerUnitary q hq0 hq1)

★ The register flow lifts U_q, with no hypotheses.

The single-error channel as the environment marginal of the flow, and QEC on Σ

theorem CSD.Empirical.CSDBridge.QEC.registerFlow_traceRight_barycenter (p₀ : LF4.CPN 32) (μprep : MeasureTheory.Measure (LF4.CPN 32)) [MeasureTheory.IsProbabilityMeasure μprep] (repS : LF4.CPN 32 → EuclideanSpace ℂ (Fin 2 × Fin 2 × Fin 2)) (hrepS_meas : Measurable repS) (q : Fin 4 → ℝ) (hq0 : ∀ (k : Fin 4), 0 ≤ q k) (hq1 : ∑ k : Fin 4, q k = 1) (hprod : ∀ᵐ (x : LF4.CPN 32) ∂μprep, LF2.outerProduct (registerRep x) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (LF2.outerProduct (repS x)) (LF2.outerProduct (EuclideanSpace.single 0 1))) : (LF2.barycenterMatrix registerRep (MeasureTheory.Measure.map (LF4.cpSectorData p₀).π (MeasureTheory.Measure.map (registerFlow q hq0 hq1) μprep))).traceRight = (QM.QEC.singleFlipChannel q hq0 hq1).apply (LF2.barycenterMatrix repS (MeasureTheory.Measure.map (LF4.cpSectorData p₀).π μprep))

★★ The register's single-error channel is the environment marginal of the joint Σ-flow. For a preparation on ℂℙ³¹ that is a product with the environment ready (a.e., in the canonical representative, with register representative repS), the reduced density operator of the flowed preparation is singleFlipChannel q applied to the register's density operator.

theorem CSD.Empirical.CSDBridge.QEC.registerFlow_recovery (p₀ : LF4.CPN 32) (μprep : MeasureTheory.Measure (LF4.CPN 32)) [MeasureTheory.IsProbabilityMeasure μprep] (repS : LF4.CPN 32 → EuclideanSpace ℂ (Fin 2 × Fin 2 × Fin 2)) (hrepS_unit : ∀ (x : LF4.CPN 32), ‖repS x‖ = 1) (hrepS_meas : Measurable repS) (q : Fin 4 → ℝ) (hq0 : ∀ (k : Fin 4), 0 ≤ q k) (hq1 : ∑ k : Fin 4, q k = 1) (hprod : ∀ᵐ (x : LF4.CPN 32) ∂μprep, LF2.outerProduct (registerRep x) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (LF2.outerProduct (repS x)) (LF2.outerProduct (EuclideanSpace.single 0 1))) (hcode : ∀ᵐ (x : LF4.CPN 32) ∂μprep, (Matrix.toEuclideanLin QM.QEC.codeProj) (repS x) = repS x) : QM.QEC.recoveryChannel.apply (LF2.barycenterMatrix registerRep (MeasureTheory.Measure.map (LF4.cpSectorData p₀).π (MeasureTheory.Measure.map (registerFlow q hq0 hq1) μprep))).traceRight = LF2.barycenterMatrix repS (MeasureTheory.Measure.map (LF4.cpSectorData p₀).π μprep)

★★★ QEC on Σ, end to end. Let the register preparation live in the code region (P₀ (repS x) = repS x a.e.: every prepared ray lies in the codespace ℂℙ¹ ⊂ ℂℙ⁷), the environment be ready, and the joint Σ-flow be registerFlow q. Then the syndrome-conditioned recovery channel, applied to the environment marginal of the flowed preparation, returns the register's density operator: the flow's leak into the environment is undone exactly.