LF5: syndrome-granularity frequency + outcome map (QEC, projective tier)

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

This module completes the QEC syndrome tranche by mirroring the pointer-level LF5-D (vnDilation_pointer_frequency) and LF5-F (vnPointerOutcome / measurement_flow_outcome_frequency) results at syndrome granularity for the three-qubit bit-flip code (N = 8). It is a pure mechanical coarse-graining of the existing engines by the parity classifier synClass : Fin 8 → Fin 4 (LF5/SyndromeFlow.lean): no new dilation, no new flow, no new physics. The module only imports and assembles.

What is delivered

• syndrome_flow_born_frequency (+ _canonical): a.s., for every syndrome s : Fin 4, the syndrome-class block frequency — the double sum over the pointers i ∈ class s and the apparatus index n : Fin 8 of the per-cell empirical frequencies — converges to syndromeWeight ψ s (the block sum of the computational-basis Born weights, SyndromeFlow.lean). Proof: a finite class sum (tendsto_finsetSum) of the per-pointer vnDilation_pointer_frequency limits, landing on syndromeWeight via syndromeWeight_eq_pointer_sum.
• synOutcome + synOutcome_preimage_some: the per-microstate syndrome outcome map CPN (M+1) → Option (Fin 4), vnPointerOutcome post-composed with the ψ-INDEPENDENT parity classifier synClass; its some s fibre is the syndrome-class block union ⋃_{i ∈ class s} ⋃_n bornRegion ψ' (e (n,i)).
• syndrome_flow_outcome_frequency (+ _canonical): a.s., for every syndrome s, the frequency of trials whose microstate's syndrome outcome is s — a single event per syndrome, (X k) ⁻¹' (synOutcome ⁻¹' {some s}), not a sum — converges to syndromeWeight ψ s. Mirrors measurement_flow_outcome_frequency: union-indicator split over the genuinely disjoint class cells (bornRegion_pairwiseDisjoint + e injectivity), landing on the block-sum limit of syndrome_flow_born_frequency.

Honest scope

Unchanged from SyndromeFlow.lean. Projective / coherent-error tier only. 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, Gleason-free, no Born put in) and imported here via vnDilation_pointer_volume / vnDilation_pointer_frequency; this module re-proves nothing about the number — it just coarse-grains the pointer index by the fixed synClass. Born is taken as no primitive. What is posited is 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 (the pre-registered tripwire: ψ/ψ' enter only the cell shapes bornRegion ψ', never the index sets). The decoherence / partial-trace origin of incoherent errors is NOT here — gated entangled tier (specs/lf5-plan.md §0; Bell forces non-locality).

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

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

Syndrome weight as an inner-product block sum (helper)

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

Syndrome weight = the block sum of computational-basis Born weights, in inner-product form. This is literally syndromeWeight_eq_pointer_sum (SyndromeFlow.lean), surfaced here under the name used by the part-(A) limit identity: the limit of the syndrome-class block frequency is ∑_{i ∈ class s} ‖⟨eᵢ, ψ⟩‖², which this identifies with syndromeWeight ψ s.

(A) Syndrome-class block frequencies converge to the syndrome weight

theorem CSD.LF5.syndrome_flow_born_frequency {M : ℕ} (ψ : EuclideanSpace ℂ (Fin 8)) (hψ : ‖ψ‖ = 1) (e : Fin 8 × Fin 8 ≃ Fin (M + 1)) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (vnDilationV 8)) ψ)) (hψ'0 : ψ' ≠ 0) (p₀ : LF4.CPN (M + 1)) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (X : ℕ → Ω → LF4.CPN (M + 1)) (hX : ∀ (n : ℕ), Measurable (X n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (X n) Pr = Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (hindep : ∀ (j : Fin (M + 1)), Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (X n ⁻¹' LF4.bornRegion ψ' hψ'0 j).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂Pr, ∀ (s : Fin 4), Filter.Tendsto (fun (m : ℕ) => ∑ i : Fin 8 with synClass i = s, ∑ n : Fin 8, (∑ k ∈ Finset.range m, (X k ⁻¹' LF4.bornRegion ψ' hψ'0 (e (n, i))).indicator (fun (x : Ω) => 1) ω) / ↑m) Filter.atTop (nhds (syndromeWeight ψ s))

Syndrome-class block frequencies → syndrome weight, every unit ψ. For i.i.d. FS-typical trials on the dilated ℂℙ^{63} (the posited CSD sector (SO-1) on the enlarged N = 8 sector), almost surely every syndrome s : Fin 4 has its syndrome-class block frequency — the double sum, over the pointers i ∈ class s and the apparatus index n : Fin 8, of the per-cell empirical frequencies (∑_{k<m} indicator((X k)⁻¹' bornRegion ψ' (e (n, i))) ω) / m — converging to syndromeWeight ψ s.

Proof: filter_upwards on vnDilation_pointer_frequency; the a.s. ω gives, for each pointer i, convergence of the pointer-i block frequency to ‖⟨eᵢ,ψ⟩‖². Sum over the class Finset.univ.filter (synClass · = s) by tendsto_finsetSum (continuity of finite addition); the limit ∑_{i ∈ class s} ‖⟨eᵢ,ψ⟩‖² is syndromeWeight ψ s (syndromeWeight_eq_inner_sum). The syndrome-block frequency function is presented as a finite class sum of the per-pointer block frequency functions, so tendsto_finsetSum applies termwise.

theorem CSD.LF5.syndrome_flow_born_frequency_canonical {M : ℕ} (ψ : EuclideanSpace ℂ (Fin 8)) (hψ : ‖ψ‖ = 1) (e : Fin 8 × Fin 8 ≃ Fin (M + 1)) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (vnDilationV 8)) ψ)) (hψ'0 : ψ' ≠ 0) (p₀ : LF4.CPN (M + 1)) : ∀ᵐ (ω : LF4.fsTrialSpace (M + 1)) ∂LF4.fsTrialMeasure p₀, ∀ (s : Fin 4), Filter.Tendsto (fun (m : ℕ) => ∑ i : Fin 8 with synClass i = s, ∑ n : Fin 8, (∑ k ∈ Finset.range m, (LF4.fsTrial (M + 1) k ⁻¹' LF4.bornRegion ψ' hψ'0 (e (n, i))).indicator (fun (x : LF4.fsTrialSpace (M + 1)) => 1) ω) / ↑m) Filter.atTop (nhds (syndromeWeight ψ s))

Syndrome-class block frequencies → syndrome weight, on the canonical i.i.d. FS trial process. syndrome_flow_born_frequency with the trial bundle discharged by the canonical coordinate process (fsTrialMeasure / fsTrial), mirroring measurement_flow_born_frequency_canonical.

(B) The per-microstate syndrome outcome map

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

The per-microstate syndrome outcome map. The syndrome class of the microstate's cell: vnPointerOutcome post-composed with the parity classifier synClass. Equivalently (bornOutcome ψ' hψ'0 ·).map (synClass ∘ (e.symm ·).2). The pointer→syndrome coarse-graining synClass and the block assignment c ↦ (e.symm c).2 are both ψ-independent and context-fixed — only the measurement context e enters, never the preparation. Deterministic and total off an FS-null set (inherited from bornOutcome).

Equations

• CSD.LF5.synOutcome ψ' hψ'0 e p = Option.map CSD.LF5.synClass (CSD.LF5.vnPointerOutcome ψ' hψ'0 e p)

theorem CSD.LF5.synOutcome_preimage_some {M : ℕ} (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'0 : ψ' ≠ 0) (e : Fin 8 × Fin 8 ≃ Fin (M + 1)) (s : Fin 4) : synOutcome ψ' hψ'0 e ⁻¹' {some s} = ⋃ i ∈ {i : Fin 8 | synClass i = s}, ⋃ (n : Fin 8), LF4.bornRegion ψ' hψ'0 (e (n, i))

The syndrome-s fibre is the syndrome-class block union. The set of microstates whose syndrome outcome is s is the union over the pointers i ∈ class s and the apparatus index n of the dilated Born cells bornRegion ψ' hψ'0 (e (n, i)). Via vnPointerOutcome_preimage_some and the Option.map fibre algebra over the (ψ-independent) classifier synClass.

(C) Syndrome outcome frequencies converge to the syndrome weight

theorem CSD.LF5.syndrome_flow_outcome_frequency {M : ℕ} (e : Fin 8 × Fin 8 ≃ Fin (M + 1)) (ψ : EuclideanSpace ℂ (Fin 8)) (hψ : ‖ψ‖ = 1) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (vnDilationV 8)) ψ)) (hψ'0 : ψ' ≠ 0) (p₀ : LF4.CPN (M + 1)) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (X : ℕ → Ω → LF4.CPN (M + 1)) (hX : ∀ (n : ℕ), Measurable (X n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (X n) Pr = Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (hindep : ∀ (j : Fin (M + 1)), Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (X n ⁻¹' LF4.bornRegion ψ' hψ'0 j).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂Pr, ∀ (s : Fin 4), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (X k ⁻¹' synOutcome ψ' hψ'0 e ⁻¹' {some s}).indicator (fun (x : Ω) => 1) ω) / ↑m) Filter.atTop (nhds (syndromeWeight ψ s))

LF5-F (syndrome) outcome-frequency capstone: per-microstate syndrome outcomes commit the syndrome-class frequencies. With the LF5-D/E set-up (unit ψ, dilated state ψ' = piLpCongrLeft e (Vψ)) at N = 8, for i.i.d. FS-typical trials on the dilated ℂℙ^{63}, almost surely every syndrome s : Fin 4 has the frequency of trials whose microstate's syndrome outcome is s — a single event per syndrome, (X k) ⁻¹' (synOutcome ⁻¹' {some s}), not a sum of per-cell frequencies — converging to syndromeWeight ψ s.

This is the syndrome-granularity analogue of measurement_flow_outcome_frequency. Proof: rewrite the outcome event into the syndrome-class block union (synOutcome_preimage_some + Set.preimage_iUnion), turn the union indicator into the sum over the genuinely disjoint cells indexed by {(i, n) : i ∈ class s} via indicator_iUnion_disjoint + bornRegion_pairwiseDisjoint (disjointness across BOTH i and n: (n, i) ↦ e (n, i) is injective), then land on part (A)'s block-sum limit syndrome_flow_born_frequency.

theorem CSD.LF5.syndrome_flow_outcome_frequency_canonical {M : ℕ} (e : Fin 8 × Fin 8 ≃ Fin (M + 1)) (ψ : EuclideanSpace ℂ (Fin 8)) (hψ : ‖ψ‖ = 1) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (vnDilationV 8)) ψ)) (hψ'0 : ψ' ≠ 0) (p₀ : LF4.CPN (M + 1)) : ∀ᵐ (ω : LF4.fsTrialSpace (M + 1)) ∂LF4.fsTrialMeasure p₀, ∀ (s : Fin 4), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (LF4.fsTrial (M + 1) k ⁻¹' synOutcome ψ' hψ'0 e ⁻¹' {some s}).indicator (fun (x : LF4.fsTrialSpace (M + 1)) => 1) ω) / ↑m) Filter.atTop (nhds (syndromeWeight ψ s))

LF5-F (syndrome) outcome-frequency capstone on the canonical i.i.d. FS trial process. syndrome_flow_outcome_frequency with the trial bundle discharged by the canonical coordinate process (fsTrialMeasure / fsTrial), mirroring measurement_flow_outcome_frequency_canonical.