LF3 Singlet / Leakage: finite-leakage stability of kernel, correlation, marginals

Category: 3-Local (LF3 finite-leakage bounds on all four kernel quantities, parameterised by εA, εB).

Paper §7.

Each finite-leakage bound is a triangle inequality on the appropriate finite sum over Sign × Sign or Sign, with the per-sector deviation supplied by sectorVolume_finite_leakage and LeakageCompat. Composes sectorVolume_finite_leakage from Projectors/SectorVolume.lean with the cst_squared_eq algebraic core.

theorem CSD.LF3.singlet_pointer_probability_finite_leakage {K_A : Type u_1} {K_B : Type u_2} {H_SA : Type u_3} [NormedAddCommGroup K_A] [InnerProductSpace ℂ K_A] [FiniteDimensional ℂ K_A] [NormedAddCommGroup K_B] [InnerProductSpace ℂ K_B] [FiniteDimensional ℂ K_B] [NormedAddCommGroup H_SA] [InnerProductSpace ℂ H_SA] [FiniteDimensional ℂ H_SA] {S : SystemApparatusSetup K_A K_B H_SA} (P : ProjectorAlgebra S) (M : MeasurementUnitary S) (φA0 : K_A) (φB0 : K_B) (a b : DetectorSetting) (L : LeakageCompat P M φA0 φB0) (s t : Sign) : |sectorVolume P (finalState M (cAmp a b) φA0 φB0) s t - P_st a b s t| ≤ L.εA + L.εB + L.εA * L.εB

Singlet pointer-probability finite-leakage bound (paper §7.5). The measured pointer-sector frequency deviates from P_{st}(a, b) by at most εA + εB + εA · εB. Composes sectorVolume_finite_leakage (operator layer) with cst_squared_eq (algebraic-core identity).

theorem CSD.LF3.correlation_finite_leakage_bound {K_A : Type u_1} {K_B : Type u_2} {H_SA : Type u_3} [NormedAddCommGroup K_A] [InnerProductSpace ℂ K_A] [FiniteDimensional ℂ K_A] [NormedAddCommGroup K_B] [InnerProductSpace ℂ K_B] [FiniteDimensional ℂ K_B] [NormedAddCommGroup H_SA] [InnerProductSpace ℂ H_SA] [FiniteDimensional ℂ H_SA] {S : SystemApparatusSetup K_A K_B H_SA} (P : ProjectorAlgebra S) (M : MeasurementUnitary S) (φA0 : K_A) (φB0 : K_B) (a b : DetectorSetting) (L : LeakageCompat P M φA0 φB0) : |∑ st : Sign × Sign, st.1.val * st.2.val * sectorVolume P (finalState M (cAmp a b) φA0 φB0) st.1 st.2 - -dotR a b| ≤ 4 * (L.εA + L.εB + L.εA * L.εB)

Singlet correlation finite-leakage bound (paper §7.6). The measured correlation deviates from −a·b by at most 4(εA + εB + εA · εB). Triangle inequality on the four-term Sign × Sign sum, each term bounded by the per-sector leakage.

theorem CSD.LF3.marginal_a_finite_leakage_bound {K_A : Type u_1} {K_B : Type u_2} {H_SA : Type u_3} [NormedAddCommGroup K_A] [InnerProductSpace ℂ K_A] [FiniteDimensional ℂ K_A] [NormedAddCommGroup K_B] [InnerProductSpace ℂ K_B] [FiniteDimensional ℂ K_B] [NormedAddCommGroup H_SA] [InnerProductSpace ℂ H_SA] [FiniteDimensional ℂ H_SA] {S : SystemApparatusSetup K_A K_B H_SA} (P : ProjectorAlgebra S) (M : MeasurementUnitary S) (φA0 : K_A) (φB0 : K_B) (a b : DetectorSetting) (L : LeakageCompat P M φA0 φB0) (s : Sign) : |∑ t : Sign, sectorVolume P (finalState M (cAmp a b) φA0 φB0) s t - 1 / 2| ≤ 2 * (L.εA + L.εB + L.εA * L.εB)

Singlet A-side marginal finite-leakage bound (paper §7.7).

theorem CSD.LF3.marginal_b_finite_leakage_bound {K_A : Type u_1} {K_B : Type u_2} {H_SA : Type u_3} [NormedAddCommGroup K_A] [InnerProductSpace ℂ K_A] [FiniteDimensional ℂ K_A] [NormedAddCommGroup K_B] [InnerProductSpace ℂ K_B] [FiniteDimensional ℂ K_B] [NormedAddCommGroup H_SA] [InnerProductSpace ℂ H_SA] [FiniteDimensional ℂ H_SA] {S : SystemApparatusSetup K_A K_B H_SA} (P : ProjectorAlgebra S) (M : MeasurementUnitary S) (φA0 : K_A) (φB0 : K_B) (a b : DetectorSetting) (L : LeakageCompat P M φA0 φB0) (t : Sign) : |∑ s : Sign, sectorVolume P (finalState M (cAmp a b) φA0 φB0) s t - 1 / 2| ≤ 2 * (L.εA + L.εB + L.εA * L.εB)

Singlet B-side marginal finite-leakage bound (paper §7.7).