Empirical/CSD: independent bit-flip noise as one Σ-flow, and the residual failure on Σ

Category: 3-Local (CSD-side companion to Empirical/QM/QEC/IndependentNoise.lean; BACKLOG #52, the Σ half — the independent-noise channel RegisterFlow.lean left out).

RegisterFlow.lean read the register's single-error channel as the environment marginal of a Σ-flow on ℂℙ³¹ and showed the syndrome recovery undoes that leak exactly. The physical noise is independent: each qubit flips on its own with probability p, so the environment is the eight-level register of flip patterns and the leak has a part the code cannot undo. This file:

• indepFlow p — the projective action of the joint unitary controlledUnitary flipOp (indepWeight p) (ControlledDilation.lean) on ℂℙ⁶³, the joint projective space of the register ⊗ the pattern environment; a flow of the corpus's cpSectorData over ℂℙ⁶³, lifting the unitary with no hypothesis (isUnitaryLift_indepFlow);
• ★★ indepFlow_traceRight_barycenter — the independent bit-flip channel is the environment marginal of the joint Σ-flow: for a preparation that is a product with the environment ready (no flip), the reduced density operator of the flowed preparation is indepFlipChannel p applied to the register's density operator;
• ★★★ indepFlow_recovery — QEC on Σ under independent noise, with its residual failure: if the register preparation lives in the code region, the syndrome-conditioned recovery applied to the environment marginal of the flowed preparation returns (1 − p_fail) σ + p_fail X̄ σ X̄, p_fail = 3p² − 2p³. The leak into the one-flip regions is undone; the leak into the two- and three-flip regions — weight 3p² − 2p³ — is mis-read by the syndrome as its complementary single flip and corrected into the logical flip X̄. Below p = 1/2 this is less than the bare flip probability (failProb_lt_of_lt_half).

What is not here: a Hamiltonian generating the joint unitary (the flow is its time-one projective action, as for bitFlipFlow), and concatenation or a threshold (BACKLOG #51).

Source

Nielsen–Chuang §10.1.1; Shor 1995, Phys. Rev. A 52, R2493.

The joint index as Fin 64, and the flow on ℂℙ⁶³

def CSD.Empirical.CSDBridge.QEC.patternEquiv : Fin 2 × Fin 2 × Fin 2 ≃ Fin 8

A flip pattern Fin 2 × Fin 2 × Fin 2 as Fin 8.

Equations

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

def CSD.Empirical.CSDBridge.QEC.indepEquiv : (Fin 2 × Fin 2 × Fin 2) × QM.QEC.FlipPattern ≃ Fin 64

The joint index (register) × (pattern environment) as Fin 64.

Equations

• CSD.Empirical.CSDBridge.QEC.indepEquiv = (CSD.Empirical.CSDBridge.QEC.patternEquiv.prodCongr CSD.Empirical.CSDBridge.QEC.patternEquiv).trans finProdFinEquiv

@[reducible, inline]

abbrev CSD.Empirical.CSDBridge.QEC.readyPattern : QM.QEC.FlipPattern

The ready pattern: no qubit flipped.

Equations

• CSD.Empirical.CSDBridge.QEC.readyPattern = (0, 0, 0)

noncomputable def CSD.Empirical.CSDBridge.QEC.indepUnitary (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : Matrix ((Fin 2 × Fin 2 × Fin 2) × QM.QEC.FlipPattern) ((Fin 2 × Fin 2 × Fin 2) × QM.QEC.FlipPattern) ℂ

The joint unitary of independent noise: the controlled error of the pattern family with the independent weights, on register ⊗ pattern environment.

Equations

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

theorem CSD.Empirical.CSDBridge.QEC.indepUnitary_conjTranspose_mul (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : (indepUnitary p hp0 hp1).conjTranspose * indepUnitary p hp0 hp1 = 1

theorem CSD.Empirical.CSDBridge.QEC.stinespringChannel_indepUnitary (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : LF2.stinespringChannel (indepUnitary p hp0 hp1) ⋯ (EuclideanSpace.single readyPattern 1) stinespringChannel_indepUnitary._proof_1 = QM.QEC.indepFlipChannel p hp0 hp1

★ The independent bit-flip channel is the Stinespring channel of the joint unitary with the environment ready, as channels.

noncomputable def CSD.Empirical.CSDBridge.QEC.indepU64 (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : ↥(Matrix.unitaryGroup (Fin 64) ℂ)

The joint unitary as an element of U(64), reindexed to Fin 64.

Equations

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

theorem CSD.Empirical.CSDBridge.QEC.indepU64_val (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : ↑(indepU64 p hp0 hp1) = (Matrix.reindex indepEquiv indepEquiv) (indepUnitary p hp0 hp1)

noncomputable def CSD.Empirical.CSDBridge.QEC.indepFlow (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : LF4.CPN 64 → LF4.CPN 64

The independent-noise de-isolation flow on ℂℙ⁶³: the projective action of the joint unitary. A flow of the corpus's cpSectorData (Σ = P = ℂℙ⁶³, π = id).

Equations

• CSD.Empirical.CSDBridge.QEC.indepFlow p hp0 hp1 x = CSD.Empirical.CSDBridge.QEC.indepU64 p hp0 hp1 • x

theorem CSD.Empirical.CSDBridge.QEC.measurable_indepFlow (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : Measurable (indepFlow p hp0 hp1)

noncomputable def CSD.Empirical.CSDBridge.QEC.indepRep : LF4.CPN 64 → EuclideanSpace ℂ ((Fin 2 × Fin 2 × Fin 2) × QM.QEC.FlipPattern)

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

Equations

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

theorem CSD.Empirical.CSDBridge.QEC.indepRep_norm (x : LF4.CPN 64) : ‖indepRep x‖ = 1

theorem CSD.Empirical.CSDBridge.QEC.measurable_indepRep : Measurable indepRep

theorem CSD.Empirical.CSDBridge.QEC.isUnitaryLift_indepFlow (p₀ : LF4.CPN 64) (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : LF2.IsUnitaryLift (LF4.cpSectorData p₀) (indepFlow p hp0 hp1) indepRep (indepUnitary p hp0 hp1)

★ The independent-noise flow lifts the joint unitary, with no hypotheses.

The independent bit-flip channel as the environment marginal of the flow, and QEC on Σ

theorem CSD.Empirical.CSDBridge.QEC.indepFlow_traceRight_barycenter (p₀ : LF4.CPN 64) (μprep : MeasureTheory.Measure (LF4.CPN 64)) [MeasureTheory.IsProbabilityMeasure μprep] (repS : LF4.CPN 64 → EuclideanSpace ℂ (Fin 2 × Fin 2 × Fin 2)) (hrepS_meas : Measurable repS) (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hprod : ∀ᵐ (x : LF4.CPN 64) ∂μprep, LF2.outerProduct (indepRep x) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (LF2.outerProduct (repS x)) (LF2.outerProduct (EuclideanSpace.single readyPattern 1))) : (LF2.barycenterMatrix indepRep (MeasureTheory.Measure.map (LF4.cpSectorData p₀).π (MeasureTheory.Measure.map (indepFlow p hp0 hp1) μprep))).traceRight = (QM.QEC.indepFlipChannel p hp0 hp1).apply (LF2.barycenterMatrix repS (MeasureTheory.Measure.map (LF4.cpSectorData p₀).π μprep))

★★ The independent bit-flip channel is the environment marginal of the joint Σ-flow. For a preparation on ℂℙ⁶³ that is a product with the environment ready — no qubit flipped — (a.e., in the canonical representative, with register representative repS), the reduced density operator of the flowed preparation is indepFlipChannel p applied to the register's density operator.

theorem CSD.Empirical.CSDBridge.QEC.indepFlow_recovery (p₀ : LF4.CPN 64) (μprep : MeasureTheory.Measure (LF4.CPN 64)) [MeasureTheory.IsProbabilityMeasure μprep] (repS : LF4.CPN 64 → EuclideanSpace ℂ (Fin 2 × Fin 2 × Fin 2)) (hrepS_unit : ∀ (x : LF4.CPN 64), ‖repS x‖ = 1) (hrepS_meas : Measurable repS) (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hprod : ∀ᵐ (x : LF4.CPN 64) ∂μprep, LF2.outerProduct (indepRep x) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (LF2.outerProduct (repS x)) (LF2.outerProduct (EuclideanSpace.single readyPattern 1))) (hcode : ∀ᵐ (x : LF4.CPN 64) ∂μprep, (Matrix.toEuclideanLin QM.QEC.codeProj) (repS x) = repS x) : QM.QEC.recoveryChannel.apply (LF2.barycenterMatrix indepRep (MeasureTheory.Measure.map (LF4.cpSectorData p₀).π (MeasureTheory.Measure.map (indepFlow p hp0 hp1) μprep))).traceRight = ↑(1 - QM.QEC.failProb p) • LF2.barycenterMatrix repS (MeasureTheory.Measure.map (LF4.cpSectorData p₀).π μprep) + ↑(QM.QEC.failProb p) • (QM.QEC.logicalX * LF2.barycenterMatrix repS (MeasureTheory.Measure.map (LF4.cpSectorData p₀).π μprep) * QM.QEC.logicalX)

★★★ QEC on Σ under independent noise, with its residual failure. 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 indepFlow p. Then the syndrome-conditioned recovery channel, applied to the environment marginal of the flowed preparation, returns (1 − p_fail) σ + p_fail X̄ σ X̄ with σ the register's density operator and p_fail = 3p² − 2p³: the flow's leak into the one-flip regions is undone, its leak into the two- and three-flip regions is corrected into the logical flip.