Empirical/CSD: the Steane register ⊗ environment as one Σ-flow, and QEC on Σ #
Category: 3-Local (CSD-side companion to Empirical/QM/QEC/SteaneRecovery.lean). BACKLOG #53,
the Σ-twin of the Steane recovery — the twin the cell promised for link 12's seven-qubit code.
QM/QEC/SteaneRecovery.lean built the recovery on the QM side: one channel undoes every
single-qubit Pauli on a code state. This file gives the same physics as one flow on Σ, on the
pattern of RegisterFlow.lean (three qubits) and IndependentNoiseFlow.lean:
steaneJointMat q— the joint unitary of register ⊗ environment, the controlled-error dilation of #52 (ControlledDilation.lean) instantiated at the Steane code's own error family: the seven-qubit register (128rays) times the22single-error labels,Option (Fin 7 × Fin 3);steaneFlow q— its projective action onℂℙ²⁸¹⁵, the joint projective space, a flow of the corpus'scpSectorData, lifting the joint unitary with no hypothesis (★isUnitaryLift_steaneFlow, through the canonical measurable unit section);- ★★
steaneFlow_traceRight_barycenter— the single-qubit Pauli 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 the mixed-unitary Pauli channel applied to the register's density operator; exists_steane_recovery_mixedUnitary— one recovery undoes the whole channel, not only each error separately, because the channel is a convex combination of the errors and a channel is linear;- ★★★
exists_steaneFlow_recovery— QEC onΣ, end to end: one recovery channel, the code's own and independent of both the preparation and the noise weights, applied to the environment marginal of the flowed preparation, returns the register's density operator.
The CSD reading. The error is not a separate axiom: it is the Σ-flow's leak into the
environment factor, which is what de-isolation means here. The codespace is a region of Σ (the
hypothesis P₀ (repS x) = repS x, every prepared ray in ℂℙ¹ ⊂ ℂℙ¹²⁷); the regions are epistemic
and the measure weighting them is ontic, so the preparation is a probability measure over rays and
the register's state is its barycentre. The recovery then undoes the leak exactly.
Honest scope #
⚠️ No Hamiltonian generates the joint unitary here: the flow is the time-one map of the projective
action, as for bitFlipFlow, registerFlow and indepFlow.
⚠️ Single-qubit Pauli errors with free weights. Two qubits in error are outside the Steane code at
this level, exactly as on the QM side; the arbitrary (non-Pauli) single-qubit error is
QM/QEC/SteaneArbitrary.lean (#61) and is not fed through the flow here.
⚠️ The code region is a hypothesis on the preparation, not a derivation: nothing here says why a
preparation would live in the codespace.
Source #
A. Steane, Error correcting codes in quantum theory, PRL 77 (1996); E. Knill, R. Laflamme,
Phys. Rev. A 55 (1997) 900; Empirical/QM/QEC/ControlledDilation.lean (#52);
Empirical/CSD/QEC/RegisterFlow.lean; specs/BACKLOG.md #53; specs/steane-plan.md.
The joint index of register ⊗ environment #
The joint index (seven-qubit register) × (the 22 single-error labels) as Fin 2816.
Equations
Instances For
The single-qubit Pauli errors of the Steane code are unitary.
The joint unitary of the Steane register and its environment: the controlled-error dilation of
the single-qubit Pauli channel with weights q.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The joint unitary as an element of U(2816).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The flow on ℂℙ²⁸¹⁵ #
The Steane register's de-isolation flow: the projective action of the joint unitary on
ℂℙ²⁸¹⁵, a flow of the corpus's cpSectorData.
Equations
- CSD.Empirical.CSDBridge.QEC.steaneFlow q hq0 hq1 x = CSD.Empirical.CSDBridge.QEC.steaneU2816 q hq0 hq1 • x
Instances For
The joint representative: the canonical unit section, transported to the joint index.
Equations
Instances For
★ The Steane flow lifts the joint unitary, with no hypotheses.
The Pauli channel as the environment marginal #
★★ The Steane register's single-qubit Pauli 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 the mixed-unitary Pauli channel applied to the register's
density operator.
The recovery undoes the leak #
The Steane recovery undoes the whole Pauli channel, not only each error separately: the channel is a convex combination of the errors and a recovery is linear. One channel serves every weight vector.
★★★ QEC on Σ for the Steane code, end to end. One recovery channel — the code's own,
independent of the preparation and of the noise weights — serves every case: 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 steaneFlow q. Then
the recovery applied to the environment marginal of the flowed preparation returns the register's
density operator: the flow's leak into the 22-level environment is undone exactly.