LF5: syndrome statistics from a coarse-grained de-isolation flow (QEC, projective tier)

Category: 3-Local (LF5 measurement-dynamics layer, QEC tranche).

The three-qubit bit-flip code's syndrome statistics for (Z₁Z₂, Z₂Z₃) are realised as a coarse-graining of the LF5 von Neumann computational-basis (Z-basis) de-isolation flow at N = 8 (the 3-qubit register). The apparatus retains the full computational-basis label: grouping its outcomes by syndrome does not erase the information distinguishing the two basis states in each syndrome subspace. This construction establishes the syndrome probabilities; it does not implement nondestructive syndrome extraction for an unknown logical superposition. The recovery identities below are separate matrix facts.

The key structural fact

The stabilisers Z₁Z₂, Z₂Z₃ (CSD.Empirical.QM.QEC.Z1Z2 / Z2Z3) are diagonal in the computational basis: on |x₁x₂x₃⟩ they act by (-1)^{x₁⊕x₂}, (-1)^{x₂⊕x₃}. So the syndrome is a function of the computational bitstring, and the syndrome outcome distribution is a coarse-graining of the Z-basis distribution: the 8 computational outcomes Fin 2 × Fin 2 × Fin 2 ≃ Fin 8 partition into 4 syndrome classes of 2 each (synClass, matched to CSD.Empirical.QM.QEC.errorSyndrome: I → 0 (+,+), X₁ → 1 (−,+), X₂ → 2 (−,−), X₃ → 3 (+,−)).

Therefore this module builds no new dilation. It reuses the LF5 N = 8 computational-basis machinery (basisPOVM, vnNaimark, measurementFlow, vnDilation_pointer_volume) and the unconditional FS-volume = Born engine (LF4/BornRegionUncond.lean), and only coarse-grains the pointer index by synClass.

What is delivered

Stratum 1 — syndrome statistics as Kähler volumes, read by a deterministic flow.

• synClass : Fin 8 → Fin 4 — the parity classifier; synClass_class_nonempty, synClass_fiber_card (each class has exactly 2 preimages — the partition is genuine and the classes are nonempty).
• syndromeWeight ψ s = ∑_{i : synClass i = s} ‖ψᵢ‖² (syndromeWeight), and syndromeWeight_eq_pointer_sum / syndromeWeight_eq_fs_volume_sum: the syndrome weight is the block sum over the syndrome class of the computational-basis Born weights, hence (via vnDilation_pointer_volume at N = 8 + finite additivity of the FS measure over the disjoint pointer-block cells) a sum of Fubini–Study volumes.
• The syndrome-s region syndromeRegion ψ' hψ'0 e s is the union of the pointer-i blocks over i ∈ class s (the partition into syndrome blocks is synClass, a fixed ψ-INDEPENDENT function — pre-registered tripwire), and syndromeRegion_fs_volume proves its FS volume = syndromeWeight ψ s.
• The flow Φ_syn is measurementFlow N=8 e itself — already Φ ≠ id and FS-measure-preserving, inherited directly.

Stratum 2 — codeword specialisation + separate recovery identities.

• The Z-basis support of logical a b is {000, 111} ⊆ class 0, and of Xⱼ · logical is ⊆ class j. (Established inline inside the weight computation below; there is no standalone support lemma. This bullet previously named synClass_logicalSupport / synClass_erroredSupport, neither of which was ever written — corrected 2026-08-19, see scripts/check-doc-promises.sh.)
• syndromeWeight_Xⱼ_logical: syndromeWeight (Xⱼ·logical) s = (if s = j then ‖a‖²+‖b‖² else 0) — the deterministic syndrome (indicator on block j for a unit codeword).
• Recovery is the matrix transport of bitflip_recovers / three_qubit_corrects_single_bitflip (CSD.Empirical.QM.QEC): re-applying the error operator Xⱼ restores the input logical vector, with no intervening measurement or syndromeFlow in the theorem. It does not prove recovery after this module's computational-basis coupling. The codeword's syndrome-block FS volume reading is NOT bundled into the headline; it follows by instantiating syndromeRegion_fs_volume at the (unit-normalised) errored codeword. What conjunct (4) proves is the codeword's deterministic syndrome weight statistic plus the matrix recovery equalities, on a state distinct from conjunct (3)'s free ψ (no shared preparation, no normalisation hypothesis on a, b).

Module headline

syndrome_flow_born_volume bundles: Φ_syn ≠ id ∧ FS-measure-preserving ∧ (∀ unit ψ, ∀ s, syndrome-block FS volume = syndromeWeight ψ s = block sum of computational-basis FS volumes) ∧ (codeword corollary: deterministic syndrome weights + the separate identities Xⱼ (Xⱼ ψ_L) = ψ_L).

Honest scope

Statistics versus the post-measurement state. The coupling sends |i⟩|0⟩_A to |i⟩|i⟩_A (vnDilationV_mulVec). Thus even two basis states in the same syndrome class leave distinguishable apparatus records. Discarding the apparatus removes their relative coherence in the register; coarse-graining the reported label by synClass does not undo that effect. The theorem syndrome_recovery applies a second bit flip directly to the errored input, without this coupling, apparatus readout, or partial trace. The headline bundles these separate facts and makes no claim that this measurement followed by correction restores the logical state.

Operational recovery elsewhere in the corpus. CsdLean4/Empirical/QM/QEC/SyndromeRecovery.lean defines recoveryChannel using the two-dimensional syndrome projectors and proves CSD.Empirical.QM.QEC.recoveryChannel_apply_singleFlipChannel_apply: syndrome measurement followed by correction restores every code density matrix after a mixture of the four correctable errors. In CsdLean4/Empirical/CSD/QEC/RegisterFlow.lean, CSD.Empirical.CSDBridge.QEC.registerFlow_recovery applies that recovery channel to the reduced register state produced by a concrete register–environment error flow, under its code-support and ready-environment preparation hypotheses. That result composes an error flow with a recovery channel; it does not identify the recovery channel with this module's syndromeFlow.

The Born = FS-volume identity is derived one layer down (the moment-map / Duistermaat–Heckman cluster, fs_born_volume_ratio_N / born_frequency_convergence_N: the FS volume of a pure-geometry region equals ‖⟨eᵢ,ψ⟩‖², Gleason-free, no Born put in) and imported here via vnDilation_pointer_volume / bornRegion_fs_measure_uncond; this module re-proves nothing about the number and takes Born as no primitive. Its increment is the syndrome-readout dynamics. What is posited is not Born but the CSD sector (SO-1) — that the sector's typicality law is the Fubini–Study measure; Born = volume is a theorem, FS-as-typicality is the sector posit (reducing to D1). The syndrome partition into blocks is synClass, a fixed ψ-independent function; only the underlying cell shapes (bornRegion ψ') are ψ'-dependent (engine realisation mechanism, measures forced by Kähler geometry). The decoherence / partial-trace origin of the error channel is treated in the register–environment construction cited above. The recovery-correctness half is a transport of the matrix fact (bitflip_recovers); the genuinely-new content is the volume / flow realisation of the syndrome statistics (Stratum 1).

Mirrors the register-Σ honesty conventions of the other LF5 module docstrings.

Reference: specs/lf5-plan.md; specs/carve-out-plan.md §6.

The 3-qubit register index and the syndrome classifier

def CSD.LF5.q3 : Fin 2 × Fin 2 × Fin 2 ≃ Fin 8

The fixed reindex Fin 2 × Fin 2 × Fin 2 ≃ Fin 8 of the 3-qubit register onto the Fin N-indexed LF5 engine (N = 8). Composes the right-nested finProdFinEquivs.

Equations

• CSD.LF5.q3 = ((Equiv.refl (Fin 2)).prodCongr finProdFinEquiv).trans finProdFinEquiv

def CSD.LF5.synClass3 : Fin 2 × Fin 2 × Fin 2 → Fin 4

The syndrome classifier on the triple index. Maps the computational bitstring (x₁, x₂, x₃) to its syndrome class in Fin 4, matched to CSD.Empirical.QM.QEC.errorSyndrome (machine-checked: errorSyndrome_synClass3): the eigenvalue pair ((-1)^{x₁⊕x₂}, (-1)^{x₂⊕x₃}) reads (+,+) → 0, (−,+) → 1, (−,−) → 2, (+,−) → 3.

Equations

• CSD.LF5.synClass3 x = match (x.1 + x.2.1, x.2.1 + x.2.2) with | (0, 0) => 0 | (1, 0) => 1 | (1, 1) => 2 | (0, 1) => 3

def CSD.LF5.synClass : Fin 8 → Fin 4

The syndrome classifier on the Fin 8 register index (synClass3 transported along q3). The 8 computational outcomes partition into 4 syndrome classes; this is the coarse-graining of the Z-basis pointer index.

Equations

• CSD.LF5.synClass = CSD.LF5.synClass3 ∘ ⇑CSD.LF5.q3.symm

theorem CSD.LF5.synClass3_eq (x : Fin 2 × Fin 2 × Fin 2) : synClass3 x = if x.1 + x.2.1 = 0 then if x.2.1 + x.2.2 = 0 then 0 else 3 else if x.2.1 + x.2.2 = 0 then 1 else 2

The four computational basis triples whose syndrome class is s. By the diagonal-stabiliser parity, each class has exactly two: class 0 {000, 111}, class 1 {100, 011}, class 2 {010, 101}, class 3 {001, 110}.

theorem CSD.LF5.errorSyndrome_synClass3 (x : Fin 2 × Fin 2 × Fin 2) : Empirical.QM.QEC.errorSyndrome (synClass3 x) = (if x.1 + x.2.1 = 0 then 1 else -1, if x.2.1 + x.2.2 = 0 then 1 else -1)

The classifier IS the errorSyndrome index (machine-checked anchor). synClass3 x is exactly the Fin 4 index whose CSD.Empirical.QM.QEC.errorSyndrome sign-pair equals the stabiliser eigenvalue pair ((-1)^{x₁⊕x₂}, (-1)^{x₂⊕x₃}) of the computational basis state x. This upgrades the "matched to errorSyndrome" docstring claim of synClass3 into a theorem: the labels 0,1,2,3 are not an arbitrary convention but the genuine errorSyndrome indices. (The complementary load-bearing fact — the support of Xⱼ·logical lands in class j — is syndromeWeight_Xⱼ_logical below.)

Each syndrome class has exactly two basis states (genuine partition)

theorem CSD.LF5.synClass3_fiber_card (s : Fin 4) : {x : Fin 2 × Fin 2 × Fin 2 | synClass3 x = s}.card = 2

The syndrome partition is genuine: each class has exactly two computational basis states. Hence the four classes are nonempty and partition the 8 outcomes. The parity map (x₁⊕x₂, x₂⊕x₃) is a bijection Fin 2 × Fin 2 × Fin 2 ≃ Fin 2 × Fin 2 × Fin 2 onto (parity₁, parity₂, x₃), so each (parity₁, parity₂) has exactly two preimages (the two values of x₃).

theorem CSD.LF5.synClass_fiber_card (s : Fin 4) : {i : Fin 8 | synClass i = s}.card = 2

The Fin 8 syndrome classes also have exactly two elements each (transport of synClass3_fiber_card along the bijection q3).

theorem CSD.LF5.synClass_class_nonempty (s : Fin 4) : {i : Fin 8 | synClass i = s}.Nonempty

Every syndrome class is nonempty (it has two elements).

Syndrome weights as block sums of computational-basis Born weights

noncomputable def CSD.LF5.syndromeWeight (ψ : EuclideanSpace ℂ (Fin 8)) (s : Fin 4) : ℝ

The syndrome weight. For a preparation ψ on the 3-qubit register (Fin 8), the weight of syndrome class s is the block sum, over the computational outcomes i in class s, of the computational-basis Born weights ‖ψᵢ‖².

Equations

• CSD.LF5.syndromeWeight ψ s = ∑ i : Fin 8 with CSD.LF5.synClass i = s, ‖ψ.ofLp i‖ ^ 2

theorem CSD.LF5.syndromeWeight_eq_pointer_sum (ψ : EuclideanSpace ℂ (Fin 8)) (s : Fin 4) : syndromeWeight ψ s = ∑ i : Fin 8 with synClass i = s, ‖inner ℂ (EuclideanSpace.single i 1) ψ‖ ^ 2

Syndrome weight = block sum of computational-basis Born weights (the definitional unfolding stated against the Born quadratic form).

The syndrome region: the union of the pointer blocks over the class

def CSD.LF5.synCellIndex (s : Fin 4) : Finset (Fin 8 × Fin 8)

The cell index of the syndrome-s region: the pairs (n, i) with the pointer i in syndrome class s. The cell shapes are the dilated Born cells; this index set — the partition into syndrome blocks — is synClass, ψ-independent and context-fixed (the pre-registered tripwire: ψ must not leak into the block partition).

Equations

• CSD.LF5.synCellIndex s = {p : Fin 8 × Fin 8 | CSD.LF5.synClass p.2 = s}

noncomputable def CSD.LF5.syndromeRegion {M : ℕ} (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'0 : ψ' ≠ 0) (e : Fin 8 × Fin 8 ≃ Fin (M + 1)) (s : Fin 4) : Set (LF4.CPN (M + 1))

The syndrome-s region on the dilated ontic ℂℙ^{63}: the union of the pointer-i blocks {(n, i) : n} over the computational outcomes i ∈ class s. The dilated Born cells bornRegion ψ' provide the shapes; the partition into syndrome blocks is the fixed synClass.

Equations

• CSD.LF5.syndromeRegion ψ' hψ'0 e s = ⋃ p ∈ CSD.LF5.synCellIndex s, CSD.LF4.bornRegion ψ' hψ'0 (e p)

theorem CSD.LF5.bornRegion_e_pairwiseDisjoint {M : ℕ} (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'0 : ψ' ≠ 0) (e : Fin 8 × Fin 8 ≃ Fin (M + 1)) (t : Finset (Fin 8 × Fin 8)) : (↑t).PairwiseDisjoint fun (p : Fin 8 × Fin 8) => LF4.bornRegion ψ' hψ'0 (e p)

The cells bornRegion ψ' (e p) indexed by distinct p are disjoint (bornRegion_pairwiseDisjoint + e injective).

theorem CSD.LF5.syndromeRegion_fs_volume {M : ℕ} (ψ : EuclideanSpace ℂ (Fin 8)) (hψ : ‖ψ‖ = 1) (e : Fin 8 × Fin 8 ≃ Fin (M + 1)) (p₀ : LF4.CPN (M + 1)) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (vnDilationV 8)) ψ)) (hψ'0 : ψ' ≠ 0) (s : Fin 4) : ((Matrix.UnitaryGroup.fsMeasure p₀) (syndromeRegion ψ' hψ'0 e s)).toReal = syndromeWeight ψ s

The syndrome-block FS volume equals the syndrome weight (Stratum 1, step 3). The Fubini–Study typicality volume of the syndrome-s region equals syndromeWeight ψ s = the block sum of the computational-basis Born weights, for every unit preparation ψ. Finite additivity of the FS measure over the disjoint cells (measure_biUnion_finset) reduces it to the per-pointer vnDilation_pointer_volume identities summed over the class.

theorem CSD.LF5.syndromeWeight_eq_fs_volume_sum {M : ℕ} (ψ : EuclideanSpace ℂ (Fin 8)) (hψ : ‖ψ‖ = 1) (e : Fin 8 × Fin 8 ≃ Fin (M + 1)) (p₀ : LF4.CPN (M + 1)) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (vnDilationV 8)) ψ)) (hψ'0 : ψ' ≠ 0) (s : Fin 4) : syndromeWeight ψ s = ∑ i : Fin 8 with synClass i = s, ∑ n : Fin 8, ((Matrix.UnitaryGroup.fsMeasure p₀) (LF4.bornRegion ψ' hψ'0 (e (n, i)))).toReal

Syndrome weight = a sum of Fubini–Study volumes (Stratum 1, step 2, headline form). Reads each pointer-block weight in syndromeWeight as its constituent sum of dilated-cell FS volumes (vnDilation_pointer_volume), giving the syndrome weight as an explicit double sum of FS volumes over the syndrome class.

Stratum 2: codeword specialisation

noncomputable def CSD.LF5.regOfH3 (v : Empirical.QM.QEC.H3) : EuclideanSpace ℂ (Fin 8)

The reindex of the 3-qubit register state v : H3 onto EuclideanSpace ℂ (Fin 8) along q3. The Z-basis amplitudes are permuted, not changed: (regOfH3 v).ofLp (q3 x) = v.ofLp x.

Equations

• CSD.LF5.regOfH3 v = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ CSD.LF5.q3) v

theorem CSD.LF5.regOfH3_apply (v : Empirical.QM.QEC.H3) (x : Fin 2 × Fin 2 × Fin 2) : (regOfH3 v).ofLp (q3 x) = v.ofLp x

Coordinate transport: (regOfH3 v).ofLp (q3 x) = v.ofLp x.

theorem CSD.LF5.regOfH3_norm (v : Empirical.QM.QEC.H3) : ‖regOfH3 v‖ = ‖v‖

regOfH3 preserves norm (it is a linear isometry).

theorem CSD.LF5.syndromeWeight_eq_triple_sum (v : Empirical.QM.QEC.H3) (s : Fin 4) : syndromeWeight (regOfH3 v) s = ∑ x : Fin 2 × Fin 2 × Fin 2 with synClass3 x = s, ‖v.ofLp x‖ ^ 2

The syndrome weight, with the class sum pulled back along q3 to a sum over the triple index of the squared register amplitudes.

theorem CSD.LF5.syndromeWeight_logical (a b : ℂ) (s : Fin 4) : syndromeWeight (regOfH3 (Empirical.QM.QEC.logical a b)) s = if s = 0 then ‖a‖ ^ 2 + ‖b‖ ^ 2 else 0

The logical codeword's Z-basis support lies in syndrome class 0. The only nonzero amplitudes of logical a b are at 000 and 111, both with syndrome class 0 ((+,+)). Hence the syndrome weight vanishes off class 0, and equals ‖a‖² + ‖b‖² on class 0.

Errored codewords: deterministic syndrome

noncomputable def CSD.LF5.erroredLogical (Xⱼ : Matrix (Fin 2 × Fin 2 × Fin 2) (Fin 2 × Fin 2 × Fin 2) ℂ) (a b : ℂ) : Empirical.QM.QEC.H3

The errored codeword Xⱼ · (logical a b), for j ∈ {1, 2, 3} (here indexed by the matrices X1, X2, X3).

Equations

• CSD.LF5.erroredLogical Xⱼ a b = (Matrix.toEuclideanLin Xⱼ) (CSD.Empirical.QM.QEC.logical a b)

theorem CSD.LF5.erroredLogical_syndromeWeight {Xⱼ : Matrix (Fin 2 × Fin 2 × Fin 2) (Fin 2 × Fin 2 × Fin 2) ℂ} {a b : ℂ} {p₀ p₁ : Fin 2 × Fin 2 × Fin 2} {cj : Fin 4} (hc0 : synClass3 p₀ = cj) (hc1 : synClass3 p₁ = cj) (hamp : ∀ (x : Fin 2 × Fin 2 × Fin 2), ‖(erroredLogical Xⱼ a b).ofLp x‖ ^ 2 = (if x = p₀ then ‖a‖ ^ 2 else 0) + if x = p₁ then ‖b‖ ^ 2 else 0) (s : Fin 4) : syndromeWeight (regOfH3 (erroredLogical Xⱼ a b)) s = if s = cj then ‖a‖ ^ 2 + ‖b‖ ^ 2 else 0

A bit-flip permutes the {000, 111} support of the codeword to a two-element support whose two outcomes share a single syndrome class cj. The squared amplitudes are ‖a‖² and ‖b‖² on the two flipped basis states. Stated as: for each x, the squared amplitude is (if x = p₀ then ‖a‖² else 0) + (if x = p₁ then ‖b‖² else 0), with synClass3 p₀ = synClass3 p₁ = cj.

theorem CSD.LF5.X1_logical_amp (a b : ℂ) (x : Fin 2 × Fin 2 × Fin 2) : ‖(erroredLogical Empirical.QM.QEC.X1 a b).ofLp x‖ ^ 2 = (if x = (1, 0, 0) then ‖a‖ ^ 2 else 0) + if x = (0, 1, 1) then ‖b‖ ^ 2 else 0

Squared register amplitudes of X1 · logical = a|100⟩ + b|011⟩.

theorem CSD.LF5.X2_logical_amp (a b : ℂ) (x : Fin 2 × Fin 2 × Fin 2) : ‖(erroredLogical Empirical.QM.QEC.X2 a b).ofLp x‖ ^ 2 = (if x = (0, 1, 0) then ‖a‖ ^ 2 else 0) + if x = (1, 0, 1) then ‖b‖ ^ 2 else 0

Squared register amplitudes of X2 · logical = a|010⟩ + b|101⟩.

theorem CSD.LF5.X3_logical_amp (a b : ℂ) (x : Fin 2 × Fin 2 × Fin 2) : ‖(erroredLogical Empirical.QM.QEC.X3 a b).ofLp x‖ ^ 2 = (if x = (0, 0, 1) then ‖a‖ ^ 2 else 0) + if x = (1, 1, 0) then ‖b‖ ^ 2 else 0

Squared register amplitudes of X3 · logical = a|001⟩ + b|110⟩.

theorem CSD.LF5.syndromeWeight_X1_logical (a b : ℂ) (s : Fin 4) : syndromeWeight (regOfH3 (erroredLogical Empirical.QM.QEC.X1 a b)) s = if s = 1 then ‖a‖ ^ 2 + ‖b‖ ^ 2 else 0

Deterministic syndrome for the error X₁. X₁ · logical is supported on {100, 011} ⊆ class 1, so its syndrome weight is the indicator on block 1.

theorem CSD.LF5.syndromeWeight_X2_logical (a b : ℂ) (s : Fin 4) : syndromeWeight (regOfH3 (erroredLogical Empirical.QM.QEC.X2 a b)) s = if s = 2 then ‖a‖ ^ 2 + ‖b‖ ^ 2 else 0

Deterministic syndrome for the error X₂. X₂ · logical is supported on {010, 101} ⊆ class 2.

theorem CSD.LF5.syndromeWeight_X3_logical (a b : ℂ) (s : Fin 4) : syndromeWeight (regOfH3 (erroredLogical Empirical.QM.QEC.X3 a b)) s = if s = 3 then ‖a‖ ^ 2 + ‖b‖ ^ 2 else 0

Deterministic syndrome for the error X₃. X₃ · logical is supported on {001, 110} ⊆ class 3.

Recovery (transport of the matrix fact)

theorem CSD.LF5.syndrome_recovery (a b : ℂ) : (Matrix.toEuclideanLin Empirical.QM.QEC.X1) (erroredLogical Empirical.QM.QEC.X1 a b) = Empirical.QM.QEC.logical a b ∧ (Matrix.toEuclideanLin Empirical.QM.QEC.X2) (erroredLogical Empirical.QM.QEC.X2 a b) = Empirical.QM.QEC.logical a b ∧ (Matrix.toEuclideanLin Empirical.QM.QEC.X3) (erroredLogical Empirical.QM.QEC.X3 a b) = Empirical.QM.QEC.logical a b

A second application of the same bit flip restores the logical vector (transport of CSD.Empirical.QM.QEC.bitflip_recovers). These are the identities Xⱼ (Xⱼ ψ_L) = ψ_L: no measurement, syndromeFlow, or partial trace intervenes. They do not establish recovery after this module's computational-basis coupling. For syndrome measurement followed by correction on a density matrix, see CSD.Empirical.QM.QEC.recoveryChannel_apply_singleFlipChannel_apply in CsdLean4/Empirical/QM/QEC/SyndromeRecovery.lean.

The syndrome de-isolation flow Φ_syn

@[reducible, inline]

noncomputable abbrev CSD.LF5.syndromeFlow {M : ℕ} (e : Fin 8 × Fin 8 ≃ Fin (M + 1)) : Projectivization ℂ (EuclideanSpace ℂ (Fin (M + 1))) → Projectivization ℂ (EuclideanSpace ℂ (Fin (M + 1)))

The computational-basis flow used for syndrome statistics. Φ_syn is the LF5 von Neumann measurement flow at N = 8. Only its reported pointer label is coarse-grained by synClass; the apparatus retains the full basis label. This is not a nondestructive syndrome-extraction coupling. It inherits Φ_syn ≠ id and FS-measure-preservation directly.

Equations

• CSD.LF5.syndromeFlow e = CSD.LF5.measurementFlow 8 e

theorem CSD.LF5.syndromeFlow_ne_id {M : ℕ} (e : Fin 8 × Fin 8 ≃ Fin (M + 1)) : syndromeFlow e ≠ id

Φ_syn ≠ id: the syndrome de-isolation flow is genuine measurement dynamics (inherited from measurementFlow_ne_id at N = 8 > 1).

theorem CSD.LF5.syndromeFlow_measurePreserving {M : ℕ} (e : Fin 8 × Fin 8 ≃ Fin (M + 1)) (p₀ : Projectivization ℂ (EuclideanSpace ℂ (Fin (M + 1)))) : MeasureTheory.MeasurePreserving (syndromeFlow e) (Matrix.UnitaryGroup.fsMeasure p₀) (Matrix.UnitaryGroup.fsMeasure p₀)

Φ_syn is FS-measure-preserving (the Liouville / hΦ_pres content, inherited from measurementFlow_measurePreserving).

The module headline

theorem CSD.LF5.syndrome_flow_born_volume {M : ℕ} (e : Fin 8 × Fin 8 ≃ Fin (M + 1)) (p₀ : LF4.CPN (M + 1)) (ψ : EuclideanSpace ℂ (Fin 8)) (hψ : ‖ψ‖ = 1) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (vnDilationV 8)) ψ)) (hψ'0 : ψ' ≠ 0) : syndromeFlow e ≠ id ∧ MeasureTheory.MeasurePreserving (syndromeFlow e) (Matrix.UnitaryGroup.fsMeasure p₀) (Matrix.UnitaryGroup.fsMeasure p₀) ∧ (∀ (s : Fin 4), ((Matrix.UnitaryGroup.fsMeasure p₀) (syndromeRegion ψ' hψ'0 e s)).toReal = syndromeWeight ψ s ∧ syndromeWeight ψ s = ∑ i : Fin 8 with synClass i = s, ∑ n : Fin 8, ((Matrix.UnitaryGroup.fsMeasure p₀) (LF4.bornRegion ψ' hψ'0 (e (n, i)))).toReal) ∧ (∀ (a b : ℂ) (s : Fin 4), syndromeWeight (regOfH3 (erroredLogical Empirical.QM.QEC.X1 a b)) s = if s = 1 then ‖a‖ ^ 2 + ‖b‖ ^ 2 else 0) ∧ ∀ (a b : ℂ), (Matrix.toEuclideanLin Empirical.QM.QEC.X1) (erroredLogical Empirical.QM.QEC.X1 a b) = Empirical.QM.QEC.logical a b ∧ (Matrix.toEuclideanLin Empirical.QM.QEC.X2) (erroredLogical Empirical.QM.QEC.X2 a b) = Empirical.QM.QEC.logical a b ∧ (Matrix.toEuclideanLin Empirical.QM.QEC.X3) (erroredLogical Empirical.QM.QEC.X3 a b) = Empirical.QM.QEC.logical a b

Syndrome statistics as Born volumes, with separate bit-flip identities. For the context-fixed von Neumann coupling e at N = 8 and every unit preparation ψ on the 3-qubit register:

1. the syndrome de-isolation dynamics is genuine, Φ_syn ≠ id (syndromeFlow_ne_id);
2. it is physically admissible: FS-measure-preserving — the Liouville / hΦ_pres content (syndromeFlow_measurePreserving);
3. for every syndrome class s, the syndrome-block FS volume equals syndromeWeight ψ s, the block sum (over the syndrome class) of the computational-basis Born weights — itself a sum of Fubini–Study volumes of the disjoint dilated cells (syndromeRegion_fs_volume, syndromeWeight_eq_fs_volume_sum);
4. codeword corollary: the error X₁ on logical a b gives a deterministic syndrome weight concentrated on block 1 (syndromeWeight_X1_logical), and a second bit flip (syndrome_recovery) restores the logical vector with no intervening measurement. This does not assert recovery after syndromeFlow. NB conjunct (4) concerns a state distinct from conjunct (3)'s free ψ and is not normalised; the codeword's FS-volume reading (not bundled here) follows by instantiating syndromeRegion_fs_volume at the unit-normalised errored codeword.

Pure assembly of the Stratum-1 / Stratum-2 results. The module docstring explains the distinction between syndrome probabilities and preservation of the logical state, and points to recoveryChannel_apply_singleFlipChannel_apply and registerFlow_recovery for operational recovery in their respective models. Born = volume is derived one layer down and imported; FS-as-typicality is the sector posit.