Role-Register Averaging: Branch Equalities

This module proves the role-register branch equalities for heterogeneous projective strategies.

theorem MIPStarRE.LDT.ProjStrat.ev_roleRegisterSymmState_rolePairDirectSumCond_AA {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Nonempty ιA] [Fintype ιB] [DecidableEq ιB] [Nonempty ιB] (ψ : QuantumState (ιA × ιB)) (X : Quantum.Op (LocalCarrierSum ιA ιB × LocalCarrierSum ιA ιB)) : ev (roleRegisterSymmState ψ) (rolePairDirectSumCond Role.A Role.A X) = 0

theorem MIPStarRE.LDT.ProjStrat.ev_roleRegisterSymmState_rolePairDirectSumCond_BB {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Nonempty ιA] [Fintype ιB] [DecidableEq ιB] [Nonempty ιB] (ψ : QuantumState (ιA × ιB)) (X : Quantum.Op (LocalCarrierSum ιA ιB × LocalCarrierSum ιA ιB)) : ev (roleRegisterSymmState ψ) (rolePairDirectSumCond Role.B Role.B X) = 0

theorem MIPStarRE.LDT.ProjStrat.roleRegisterSymmStrategy_selfConsistency_eq_pointAgreement {params : Parameters} [FieldModel params.q] {ιA : Type u_1} [Fintype ιA] [DecidableEq ιA] {ιB : Type u_2} [Fintype ιB] [DecidableEq ιB] (strategy : ProjStrat params ιA ιB) : strategy.roleRegisterSymmStrategy.selfConsistencyFailureProbability = strategy.pointAgreementFailureProbability

The point self-consistency branch of the heterogeneous role-register symmetrization is exactly the original cross-prover point-agreement branch.

theorem MIPStarRE.LDT.ProjStrat.roleRegisterSymmStrategy_axisParallel_eq_roleAverage {params : Parameters} [FieldModel params.q] {ιA : Type u_1} [Fintype ιA] [DecidableEq ιA] {ιB : Type u_2} [Fintype ιB] [DecidableEq ιB] (strategy : ProjStrat params ιA ιB) : strategy.roleRegisterSymmStrategy.axisParallelFailureProbability = strategy.axisParallelRoleAverage

The axis-parallel branch of the heterogeneous role-register symmetrization is exactly the axis-parallel role average of the original two-space strategy.

theorem MIPStarRE.LDT.ProjStrat.roleRegisterSymmStrategy_diagonal_eq_roleAverage {params : Parameters} [FieldModel params.q] {ιA : Type u_1} [Fintype ιA] [DecidableEq ιA] {ιB : Type u_2} [Fintype ιB] [DecidableEq ιB] (strategy : ProjStrat params ιA ιB) : strategy.roleRegisterSymmStrategy.diagonalFailureProbability = strategy.diagonalRoleAverage

The diagonal branch of the heterogeneous role-register symmetrization is exactly the diagonal role average of the original two-space strategy.