Two-Space Projective Strategies: Role-Register Measurements

This module contains the direct-sum measurement constructors and the role-register symmetric strategy associated to a heterogeneous projective strategy.

Complete block-measurement constructors

noncomputable def MIPStarRE.LDT.ProjStrat.localDirectSumMeasurement {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype Outcome] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (MA : Measurement Outcome ιA) (MB : Measurement Outcome ιB) : Measurement Outcome (LocalCarrierSum ιA ιB)

Direct-sum measurement obtained by placing Alice's and Bob's complete measurements on the Sum.inl and Sum.inr sectors respectively.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPStarRE.LDT.ProjStrat.localDirectSumMeasurement_outcome {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype Outcome] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (MA : Measurement Outcome ιA) (MB : Measurement Outcome ιB) (a : Outcome) : (localDirectSumMeasurement MA MB).outcome a = localDirectSumBlock (MA.outcome a) (MB.outcome a)

@[simp]

theorem MIPStarRE.LDT.ProjStrat.localDirectSumMeasurement_total {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype Outcome] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (MA : Measurement Outcome ιA) (MB : Measurement Outcome ιB) : (localDirectSumMeasurement MA MB).total = 1

noncomputable def MIPStarRE.LDT.ProjStrat.localDirectSumProjMeas {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype Outcome] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (MA : ProjMeas Outcome ιA) (MB : ProjMeas Outcome ιB) : ProjMeas Outcome (LocalCarrierSum ιA ιB)

Direct-sum projective measurement obtained by block-diagonalizing two projective measurements with the same outcome type.

Equations

• MIPStarRE.LDT.ProjStrat.localDirectSumProjMeas MA MB = { toMeasurement := MIPStarRE.LDT.ProjStrat.localDirectSumMeasurement MA.toMeasurement MB.toMeasurement, proj := ⋯ }

@[simp]

theorem MIPStarRE.LDT.ProjStrat.localDirectSumProjMeas_outcome {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype Outcome] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (MA : ProjMeas Outcome ιA) (MB : ProjMeas Outcome ιB) (a : Outcome) : (localDirectSumProjMeas MA MB).outcome a = localDirectSumBlock (MA.outcome a) (MB.outcome a)

noncomputable def MIPStarRE.LDT.ProjStrat.roleBlockMeasurement {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype Outcome] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (MA MB : Measurement Outcome (LocalCarrierSum ιA ιB)) : Measurement Outcome (RoleRegisterLocal ιA ιB)

Role-register measurement obtained by placing two complete direct-sum measurements in the Role.A and Role.B sectors.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPStarRE.LDT.ProjStrat.roleBlockMeasurement_outcome {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype Outcome] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (MA MB : Measurement Outcome (LocalCarrierSum ιA ιB)) (a : Outcome) : (roleBlockMeasurement MA MB).outcome a = roleBlock (MA.outcome a) (MB.outcome a)

@[simp]

theorem MIPStarRE.LDT.ProjStrat.roleBlockMeasurement_total {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype Outcome] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (MA MB : Measurement Outcome (LocalCarrierSum ιA ιB)) : (roleBlockMeasurement MA MB).total = 1

noncomputable def MIPStarRE.LDT.ProjStrat.roleBlockProjMeas {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype Outcome] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (MA MB : ProjMeas Outcome (LocalCarrierSum ιA ιB)) : ProjMeas Outcome (RoleRegisterLocal ιA ιB)

Role-register projective measurement obtained by block-diagonalizing two complete direct-sum projective measurements.

Equations

• MIPStarRE.LDT.ProjStrat.roleBlockProjMeas MA MB = { toMeasurement := MIPStarRE.LDT.ProjStrat.roleBlockMeasurement MA.toMeasurement MB.toMeasurement, proj := ⋯ }

@[simp]

theorem MIPStarRE.LDT.ProjStrat.roleBlockProjMeas_outcome {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype Outcome] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (MA MB : ProjMeas Outcome (LocalCarrierSum ιA ιB)) (a : Outcome) : (roleBlockProjMeas MA MB).outcome a = roleBlock (MA.outcome a) (MB.outcome a)

noncomputable def MIPStarRE.LDT.ProjStrat.roleRegisterProjMeas {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Inhabited Outcome] [Fintype Outcome] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (MA : ProjMeas Outcome ιA) (MB : ProjMeas Outcome ιB) : ProjMeas Outcome (RoleRegisterLocal ιA ιB)

Heterogeneous role-register projective measurement for a two-space strategy.

The Role.A sector acts on Alice's original summand and the Role.B sector acts on Bob's original summand, as in the role-register symmetrization in references/ldt-paper/inductive_step.tex:40-59. The complementary direct-sum sectors are filled by the canonical distinguished-outcome projective measurement. Those sectors are auxiliary: in the eventual heterogeneous symmetrized state, the occupied sectors are (Role.A, Sum.inl _) on the left and (Role.B, Sum.inr _) on the right, together with their swapped copy.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPStarRE.LDT.ProjStrat.roleRegisterProjMeas_A_inl_inl {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Inhabited Outcome] [Fintype Outcome] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (MA : ProjMeas Outcome ιA) (MB : ProjMeas Outcome ιB) (a : Outcome) (i j : ιA) : (roleRegisterProjMeas MA MB).outcome a (Role.A, Sum.inl i) (Role.A, Sum.inl j) = MA.outcome a i j

@[simp]

theorem MIPStarRE.LDT.ProjStrat.roleRegisterProjMeas_B_inr_inr {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Inhabited Outcome] [Fintype Outcome] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (MA : ProjMeas Outcome ιA) (MB : ProjMeas Outcome ιB) (a : Outcome) (i j : ιB) : (roleRegisterProjMeas MA MB).outcome a (Role.B, Sum.inr i) (Role.B, Sum.inr j) = MB.outcome a i j

@[simp]

theorem MIPStarRE.LDT.ProjStrat.roleRegisterProjMeas_A_B {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Inhabited Outcome] [Fintype Outcome] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (MA : ProjMeas Outcome ιA) (MB : ProjMeas Outcome ιB) (a : Outcome) (i j : LocalCarrierSum ιA ιB) : (roleRegisterProjMeas MA MB).outcome a (Role.A, i) (Role.B, j) = 0

@[simp]

theorem MIPStarRE.LDT.ProjStrat.roleRegisterProjMeas_B_A {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Inhabited Outcome] [Fintype Outcome] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (MA : ProjMeas Outcome ιA) (MB : ProjMeas Outcome ιB) (a : Outcome) (i j : LocalCarrierSum ιA ιB) : (roleRegisterProjMeas MA MB).outcome a (Role.B, i) (Role.A, j) = 0

Heterogeneous role-register measurement families

noncomputable def MIPStarRE.LDT.ProjStrat.roleRegisterPointMeasurement {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) : IdxProjMeas (Point params) (Fq params) (RoleRegisterLocal ιA ιB)

Point measurements of the heterogeneous role-register strategy associated to a two-space projective strategy.

Equations

• strategy.roleRegisterPointMeasurement u = MIPStarRE.LDT.ProjStrat.roleRegisterProjMeas (strategy.pointMeasurementA u) (strategy.pointMeasurementB u)

noncomputable def MIPStarRE.LDT.ProjStrat.roleRegisterAxisParallelMeasurement {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) : IdxProjMeas (AxisParallelLine params) (AxisLinePolynomial params) (RoleRegisterLocal ιA ιB)

Axis-parallel-line measurements of the heterogeneous role-register strategy associated to a two-space projective strategy.

Equations

• strategy.roleRegisterAxisParallelMeasurement ℓ = MIPStarRE.LDT.ProjStrat.roleRegisterProjMeas (strategy.axisParallelMeasurementA ℓ) (strategy.axisParallelMeasurementB ℓ)

noncomputable def MIPStarRE.LDT.ProjStrat.roleRegisterDiagonalMeasurement {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) : IdxProjMeas (DiagonalLine params) (DiagonalLinePolynomial params) (RoleRegisterLocal ιA ιB)

Diagonal-line measurements of the heterogeneous role-register strategy associated to a two-space projective strategy.

Equations

• strategy.roleRegisterDiagonalMeasurement ℓ = MIPStarRE.LDT.ProjStrat.roleRegisterProjMeas (strategy.diagonalMeasurementA ℓ) (strategy.diagonalMeasurementB ℓ)

theorem MIPStarRE.LDT.ProjStrat.roleRegisterAxisParallelTransportInvariant {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) : AxisParallelMeasurementTransportInvariant params strategy.roleRegisterAxisParallelMeasurement

theorem MIPStarRE.LDT.ProjStrat.roleRegisterDiagonalTransportInvariant {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) : DiagonalMeasurementTransportInvariant params strategy.roleRegisterDiagonalMeasurement

noncomputable def MIPStarRE.LDT.ProjStrat.roleRegisterSymmStrategy {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) : SymStrat params (RoleRegisterLocal ιA ιB)

The heterogeneous role-register symmetrization of a two-space projective strategy as a symmetric strategy on the common local space Role × (ιA ⊕ ιB).

This construction proves the structural part of the paper's symmetrization step: the state is exchange-invariant, normalized, and equipped with the role-blocked point, axis-parallel, and diagonal projective measurements. The branch-probability comparison giving (3ε,3ε,3ε) goodness is a separate theorem.

Equations

• One or more equations did not get rendered due to their size.

Paper test branches for two-space strategies

noncomputable def MIPStarRE.LDT.ProjStrat.axisParallelPointAnswerFamilyA {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) : IdxSubMeas (AxisParallelTestSample params) (Fq params) ιA

Alice's point answers in the axis-parallel branch: Alice receives u, the base point of the sampled line, and answers with A^{A,u}.

Equations

• strategy.axisParallelPointAnswerFamilyA s = (strategy.pointMeasurementA s.1).toSubMeas

noncomputable def MIPStarRE.LDT.ProjStrat.axisParallelPointAnswerFamilyB {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) : IdxSubMeas (AxisParallelTestSample params) (Fq params) ιB

Bob's point answers in the axis-parallel branch: Bob receives u, the base point of the sampled line, and answers with A^{B,u}.

Equations

• strategy.axisParallelPointAnswerFamilyB s = (strategy.pointMeasurementB s.1).toSubMeas

noncomputable def MIPStarRE.LDT.ProjStrat.axisParallelLineAnswerFamilyA {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) : IdxSubMeas (AxisParallelTestSample params) (Fq params) ιA

Alice's axis-parallel-line answers: Alice receives ℓ, answers with B^{A,ℓ}, and the verifier postprocesses to the value at the sampled base point.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.ProjStrat.axisParallelLineAnswerFamilyB {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) : IdxSubMeas (AxisParallelTestSample params) (Fq params) ιB

Bob's axis-parallel-line answers: Bob receives ℓ, answers with B^{B,ℓ}, and the verifier postprocesses to the value at the sampled base point.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.ProjStrat.diagonalPointAnswerFamilyA {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) (j : Fin params.m) : IdxSubMeas (RestrictedDiagonalSample params j) (Fq params) ιA

Alice's point answers in the restricted diagonal branch: Alice receives the sampled base point u and answers with A^{A,u}.

Equations

• strategy.diagonalPointAnswerFamilyA j s = (strategy.pointMeasurementA s.1).toSubMeas

noncomputable def MIPStarRE.LDT.ProjStrat.diagonalPointAnswerFamilyB {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) (j : Fin params.m) : IdxSubMeas (RestrictedDiagonalSample params j) (Fq params) ιB

Bob's point answers in the restricted diagonal branch: Bob receives the sampled base point u and answers with A^{B,u}.

Equations

• strategy.diagonalPointAnswerFamilyB j s = (strategy.pointMeasurementB s.1).toSubMeas

noncomputable def MIPStarRE.LDT.ProjStrat.diagonalLineAnswerFamilyA {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) (j : Fin params.m) : IdxSubMeas (RestrictedDiagonalSample params j) (Fq params) ιA

Alice's restricted diagonal-line answers: Alice receives ℓ, answers with L^{A,ℓ}, and the verifier postprocesses to the value at the sampled base point.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.ProjStrat.diagonalLineAnswerFamilyB {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) (j : Fin params.m) : IdxSubMeas (RestrictedDiagonalSample params j) (Fq params) ιB

Bob's restricted diagonal-line answers: Bob receives ℓ, answers with L^{B,ℓ}, and the verifier postprocesses to the value at the sampled base point.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.ProjStrat.axisParallelLineLeftPointRightFailureProbability {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) : Error

Axis-parallel branch component where Alice receives the sampled line and Bob receives its base point.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.ProjStrat.axisParallelPointLeftLineRightFailureProbability {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) : Error

Axis-parallel branch component where Alice receives the sampled base point and Bob receives the sampled line.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.ProjStrat.axisParallelRoleAverage {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) : Error

The paper's axis-parallel branch for a two-space general strategy, averaged over the two role choices.

Equations

• strategy.axisParallelRoleAverage = (strategy.axisParallelLineLeftPointRightFailureProbability + strategy.axisParallelPointLeftLineRightFailureProbability) / 2

noncomputable def MIPStarRE.LDT.ProjStrat.pointAgreementFailureProbability {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) : Error

Point-agreement branch: both provers receive the same point and the verifier checks equality of their field answers.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.ProjStrat.diagonalLineLeftPointRightFailureProbability {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) : Error

Diagonal branch component where Alice receives the sampled diagonal line and Bob receives its base point.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.ProjStrat.diagonalPointLeftLineRightFailureProbability {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) : Error

Diagonal branch component where Alice receives the sampled base point and Bob receives the sampled diagonal line.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.ProjStrat.diagonalRoleAverage {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) : Error

The paper's diagonal branch for a two-space general strategy, averaged over the two role choices and the restricted diagonal samples.

Equations

• strategy.diagonalRoleAverage = (strategy.diagonalLineLeftPointRightFailureProbability + strategy.diagonalPointLeftLineRightFailureProbability) / 2

noncomputable def MIPStarRE.LDT.ProjStrat.lowIndividualDegreeFailureProbability {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) : Error

Trace-based failure surrogate for the full low-individual-degree test for a paper-faithful two-space projective strategy.

The three outer summands are respectively axis-parallel consistency, point agreement, and restricted-diagonal consistency, with outer weight 1 / 3. Each line branch averages the two prover-role orderings with weight 1 / 2, and the restricted-diagonal branch also averages its restriction index with weight 1 / m. Line answers are evaluated at zeroCoord, the parameter value of the sampled base point.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPStarRE.LDT.ProjStrat.lowIndividualDegreeFailureProbability_eq_role_averages {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.lowIndividualDegreeFailureProbability = (strategy.axisParallelRoleAverage + strategy.pointAgreementFailureProbability + strategy.diagonalRoleAverage) / 3

The direct low-individual-degree score agrees with its decomposition into axis-parallel, point-agreement, and restricted-diagonal role averages.

structure MIPStarRE.LDT.ProjStrat.PassesLowIndividualDegreeTest {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) (eps : Error) : Prop

Passing the full low-individual-degree test with error ε, for the paper-faithful two-space strategy container.

• soundnessHypothesis : strategy.lowIndividualDegreeFailureProbability ≤ eps