Empirical/CSD: the three-qubit bit-flip code (CSD-side reading) #

Category: 3-Local (CSD-side companion to Empirical/QM/QEC/ThreeQubit.lean).

Pairs with the QM-validity bit-flip code (Shor 1995). The QM file proves error correction as pure matrix algebra: stabilisers fix the codespace, the discretised Pauli errors give distinct syndromes, and each X is self-inverse (recovery). This file states the CSD reading and, since 2026-09-11, proves its two ontic halves (the error channel from a Σ-flow; the code and error regions of Σ). The ontic content is subtler than "a flow off the codespace", and getting it right is what makes QEC the corpus's sharpest pointer at the dynamics layer.

The codespace is a sub-surface of Σ. The +1 joint eigenspace of the stabilisers is a 2-dimensional subspace of ℂ⁸, i.e. a ℂℙ¹ ⊂ ℂℙ⁷ inside the ontic Σ = ℂℙ⁷ of the three-qubit register — a constraint surface within the constraint surface.
The physical error is decoherence, which is volume flow — not a volume-preserving flow on the system alone. A coherent (stray-unitary) error would be a symplectomorphism of Σ_sys (volume-preserving, no information lost). But the dominant error is the system entangling with the environment, |ψ_L⟩|e₀⟩ ↦ Σ_E (E|ψ_L⟩)|e_E⟩: the joint flow on Σ_sys × Σ_env is volume-preserving (Liouville — the hΦ_pres field), while the system marginal spreads as its coherence leaks into system–environment correlation. That is the "volume loss": lost from the system to the environment, conserved jointly. The Pauli errors {I, X₁, X₂, X₃} formalised on the QM side are the discretised representation of this channel (the QEC discretisation theorem), not coherent rotations.
The syndrome measurement is the entropy-extraction step — the part that actually undoes decoherence. Measuring the stabilisers reads the environment's "which-error" record, re-concentrating the system's spread reduced state back to a pure state in one branch; the unitary recovery afterwards is the easy, volume-preserving return to the codespace. The four syndrome weights are the decoherence probabilities, and each is a sum of two computational-basis Fubini–Study volumes (a coarse-graining of the general-N Born-from-volume result at N = 8): "syndrome statistics as Kähler volumes."

So the honest ontic statement of QEC needs the environment Σ_env, the joint flow, and partial trace. Since 2026-09-11 (W6, W11) that is what this module has, in two pieces:

The error channel is produced by a Σ-flow. bitFlipChannel_traceRight_barycenter_flow: on a joint sector (system qubit ⊗ environment qubit), for a preparation that is a product with the environment ready and an ontic flow lifting the bit-flip joint unitary U_p (QM/QEC/BitFlipDilation.lean), the reduced density operator of the flowed preparation is the bit-flip channel applied to the system's density operator. The "volume loss" is the partial trace over the environment of a flow that is unitary on the joint space, exactly as described above. And bitFlipFlow_traceRight_barycenter is the concrete instance: on the corpus's own sector cpSectorData over ℂℙ³ (Σ = P = ℂℙ³, π = id), the projective action bitFlipFlow of U_p is a Φ ≠ id flow, it lifts U_p with no hypothesis (isUnitaryLift_bitFlipFlow, via the canonical measurable unit section), and its environment marginal is the bit-flip channel.
The code space is a region of Σ, and the syndrome is a partition. codeRegion is the set of rays of the codespace, the sub-surface ℂℙ¹ ⊂ ℂℙ⁷; errorRegion k is its image under the error Eₖ. ★★ errorRegion_disjoint: the four error regions are pairwise disjoint — two errored codewords on one ray would share their stabiliser eigenvalues, hence their syndromes, hence their error — so the syndrome measurement is the ontic selection of which of four disjoint regions the trajectory occupies. recovery_mem_codeRegion: re-applying the identified error returns every point of its error region to the code region.
The syndrome measurement is a projective measurement whose outcomes are the regions (2026-09-12). QM/QEC/SyndromeRecovery.lean builds the syndrome projectors Pₖ (pairwise orthogonal, summing to 1) and ★ syndromeProj_fixes_errorRegion here says every point of the k-th error region is fixed by Pₖ and annihilated by every other Pⱼ: the projectors are the indicator of the partition. The syndrome-conditioned recovery R (Kraus Eₖ Pₖ: "if in region k, apply Eₖ") is then one channel that returns every code state from the mixed post-error state — Empirical/CSD/QECDecoherence.lean, syndrome_recovery_corrects_mixed, the conjunct csd_qec_decoherence_corrected gained on 2026-09-12.

The joint flow on the three-qubit register ⊗ environment, and QEC on Σ end to end, are Empirical/CSD/QEC/RegisterFlow.lean (2026-09-12): registerFlow on ℂℙ³¹ produces the register's single-error channel as its environment marginal, and the syndrome-conditioned recovery returns every code-region preparation's density operator from it (registerFlow_recovery). The independent-noise channel (bit-flip_p)^{⊗3} itself, with its 3p² − 2p³ residual failure, is Empirical/CSD/QEC/IndependentNoiseFlow.lean (indepFlow_recovery, 2026-09-21). The LF5/SyndromeFlow.lean tranche carries the coherent-error syndrome flow.

Source #

Shor 1995, Phys. Rev. A 52, R2493 (the bit-flip half of the 9-qubit code).

Empirical/CSD: the three-qubit bit-flip code (CSD-side reading) #

Source #

The bit-flip channel produced by a Σ-flow #

The concrete flow: the bit-flip unitary acting on ℂℙ³ #

The code space as a region of Σ, and the error regions #

The bit-flip channel produced by a `Σ`-flow #

The concrete flow: the bit-flip unitary acting on `ℂℙ³` #

The code space as a region of `Σ`, and the error regions #