Self-consistency: data processing

prop:self-consistency-implies-data-processing: self-consistency implies that postprocessing a measurement cannot substantially decrease consistency. This is the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Preliminaries/SelfConsistency/DataProcessing.lean in the port of planning/c6b-plan.md (milestone M3, section "Port conventions").

Both statements take a symmetric model S : SymModel 𝔓 K in place of the state ψ : QuantumState (ι × ι), as an explicit first argument, with the local families A and P in 𝔓 lifted by IdxSubMeas.liftLeft S and IdxSubMeas.liftRight S. The vendored hypotheses hperm : PermInvState ψ and hψ : ψ.IsNormalized are dropped: swap symmetry is the model's S.ev_L_eq_ev_R (which replaces the vendored hperm.swap_ev) and enters also through twoNotionsOfSelfConsistencyAfterEvaluation; normalization is not used. The subprobability hypothesis h𝒟 stays.

The proof of wrongSideEstimate is the vendored one, organised question by question: the squared distance between P_[f_q] ⊗ I and I ⊗ A_[f_q] expands, outcome by outcome, as ev(L p²) + ev(R a²) - 2 ev(L p R a) (ev_star_L_sub_R_mul_self, in SwitchSandwichMain/RightTransfer.lean), the diagonal terms are at most the masses (subMeas_diagMass_le_mass) and the cross term at least that of the unprocessed families (qMatchMass_leftRight_postprocess_ge). The average is then bounded through avgOver_sub, avgOver_add and avgOver_const_mul, in place of the vendored unfolding of avgOver into finite sums.

Not ported

Every declaration of the vendored file has a counterpart here.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

• references/ldt-paper/preliminaries.tex

theorem MIPRE.LIDT.Co.Preliminaries.wrongSideEstimate {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {α : Type u_4} {β : Type u_5} [Fintype α] [Fintype β] (S : SymModel 𝔓 K) (𝒟 : MIPStarRE.LDT.Distribution Question) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A : IdxSubMeas Question α 𝔓) (P : IdxProjSubMeas Question α 𝔓) (δ ε : ℝ) (f : Question → α → β) : S.BipartiteSSCRel 𝒟 A δ → S.SDDRel 𝒟 (IdxSubMeas.liftLeft S P.toIdxSubMeas) (IdxSubMeas.liftLeft S A) ε → S.SDDRel 𝒟 (IdxSubMeas.liftLeft S fun (q : Question) => postprocess (P q).toSubMeas (f q)) (IdxSubMeas.liftRight S fun (q : Question) => postprocess (A q) (f q)) (2 * δ + 4 * √ε)

prop:self-consistency-implies-data-processing, the wrong-side estimate P_[f_q] ⊗ I ≈_{2δ + 4√ε} I ⊗ A_[f_q].

Proof:

1. expand the qSDD square, outcome by outcome, and bound the diagonal terms by the masses;
2. bound the mass of P by completenessTransferProjectiveP;
3. bound the postprocessed cross term below by the unprocessed one (qMatchMass_leftRight_postprocess_ge), and compare that with the diagonal overlap of A (easyApproxFromApproxDelta);
4. bound the gap between the mass of A and its diagonal overlap by bipartite SSC.

The vendored lemma asks for a permutation-invariant, normalized state.

theorem MIPRE.LIDT.Co.Preliminaries.selfConsistencyImpliesDataProcessing {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {α : Type u_4} {β : Type u_5} [Fintype α] [Fintype β] (S : SymModel 𝔓 K) (𝒟 : MIPStarRE.LDT.Distribution Question) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A : IdxSubMeas Question α 𝔓) (P : IdxProjSubMeas Question α 𝔓) (δ ε : ℝ) (f : Question → α → β) : S.BipartiteSSCRel 𝒟 A δ → S.SDDRel 𝒟 (IdxSubMeas.liftLeft S P.toIdxSubMeas) (IdxSubMeas.liftLeft S A) ε → S.SDDRel 𝒟 (IdxSubMeas.liftLeft S fun (q : Question) => postprocess (P q).toSubMeas (f q)) (IdxSubMeas.liftLeft S fun (q : Question) => postprocess (A q) (f q)) (8 * δ + 8 * √ε)

prop:self-consistency-implies-data-processing.

A projective approximation to a strongly self-consistent family remains close after postprocessing on the left register. The proof combines the wrong-side estimate, self-consistency after evaluation, and the SDDRel triangle inequality. The vendored lemma asks for a permutation-invariant, normalized state.