Section 3 — Strategy core

Base state-invariance and strategy structures for the low individual degree test: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Test/StrategyCore.lean in the port of planning/c6b-plan.md (milestone M0, section "Port conventions").

The vendored file assumes the swap symmetry of a symmetric strategy: its SymStrat carries, beside the state ψ : QuantumState (ι × ι), a proof permInvState that the density matrix is fixed by the swap swapDensity of the two tensor factors, the same fact again as densityFixed, and the normalization isNormalized. Here the state is a symmetric model state : SymModel 𝔓 K (Co/Basic/QuantumState.lean), and all three are theorems of it: the swap of the two factors is the flip S.flip, which fixes the expectation (S.ev_flip), carries S.L to S.R (S.ev_L_eq_ev_R, the vendored PermInvState.swap_ev), and S.ev 1 = 1 holds by S.Ψ_norm. So the ported SymStrat has the field state (the vendored text strategy.state is unchanged) and the three measurement families, over the local C*-algebra 𝔓; the symmetry lemmas of the vendored file lose their hypothesis hfix.

The covariance predicates and the answer families are generic over the ordered ⋆-ring R of Co/Basic/SubMeasurementCore.lean (the vendored Op ι), with [StarOrderedRing R] where they postprocess. The two-space ProjStrat keeps its two local algebras 𝒜, ℬ, star-ordered as in MIPRE.LIDT.Simul.SoundIn; its state is a bipartite model of the repository, MIPRE.BipartiteModel 𝒞 𝒜 ℬ (MIPRE/Foundations/BipartiteModel.lean), and its field isNormalized is ‖state.ψ‖ = 1, since a bipartite model carries no normalization (reports/c6b-paper-proofs.md, §4.1).

The consistency of a ProjStrat is not stated by the ported defects. The bipartite defects of the port (qBipartiteMatchMass, qBipartiteConsDefect, bipartiteConsError, ConsRel and their lemmas, Co/Test/Defs.lean and Co/Preliminaries/ComparisonCore.lean) are SymModel declarations, so they do not apply to strategy.state : MIPRE.BipartiteModel 𝒞 𝒜 ℬ, whereas the vendored ones hold for any state on ιA × ιB and the vendored Test/MainTheorem/MainFormal.lean states ConsRel strategy.state … of a ProjStrat. In the port that two-space route goes through the doubling (planning/c6b-plan.md, M2 and M13): a ProjStrat on M becomes a symmetric strategy on the doubled model D(M), where the ported ConsRel applies, and the consistency it yields on M itself is the repository's MIPRE.BipartiteModel.inconsistency, the form MIPRE.LIDT.Simul.SoundIn asks for (for measurements, bipartiteConsError is that inconsistency, SymModel.bipartiteConsError_eq_inconsistency). So the vendored ConsRel strategy.state statements of MainFormal are replaced, not ported, by M13 and M14.

The classical declarations of the vendored file (the test samples, extendRestrictedDirection, lastDirectionLine, the Fintype Role instance) are not ported: this file imports the vendored file and names them through an explicit open MIPStarRE.LDT (…) list.

Not ported

• swapDensity: the swap of the two factors of ι × ι; replaced by the model's flip S.flip (Co/Basic/QuantumState.lean). Its algebraic lemmas are ported below with S.flip in place of swapDensity.
• swapDensity_eq_reindex: an entrywise matrix identity; S.flip is a ⋆-algebra equivalence by construction.
• normalizedTrace_swapDensity: the model has no trace; its role is played by S.ev_flip.
• PermInvState: a hypothesis on the vendored state; both of its fields are theorems of every symmetric model, S.ev_flip (density_swap) and S.ev_L_eq_ev_R (swap_ev).
• AxisParallelTestSample: classical, imported.
• extendRestrictedDirection: classical, imported.
• RestrictedDiagonalSample: classical, imported.
• restrictedDiagonalSampleNonempty: classical, imported.
• lastDirectionLine: classical, imported.
• SymStrat.permInvState: not a field; the vendored PermInvState strategy.state is a theorem of every symmetric model, strategy.state.ev_flip and strategy.state.ev_L_eq_ev_R.
• SymStrat.densityFixed: not a field; the fixed density is strategy.state.ev_flip, and its bipartite form strategy.state.ev_opTensor_swap_of_density_fixed.
• AnswerSymStrat.permInvState: as SymStrat.permInvState.
• AnswerSymStrat.densityFixed: as SymStrat.densityFixed.

Ported elsewhere

swapDensity_opTensor, ev_swapDensity_of_density_fixed and ev_opTensor_swap_of_density_fixed are SymModel theorems of Co/Basic/QuantumState.lean, without the hypothesis hfix. The fields isNormalized of SymStrat and AnswerSymStrat are the theorems SymStrat.isNormalized and AnswerSymStrat.isNormalized below.

The swap of the two factors

theorem MIPRE.LIDT.Co.SymModel.swapDensity_swapDensity {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (X : K →L[ℂ] K) : S.flip (S.flip X) = X

The flip is an involution (the vendored swapDensity_swapDensity).

theorem MIPRE.LIDT.Co.SymModel.swapDensity_add {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (X Y : K →L[ℂ] K) : S.flip (X + Y) = S.flip X + S.flip Y

The flip is additive (the vendored swapDensity_add).

theorem MIPRE.LIDT.Co.SymModel.swapDensity_smul {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (c : ℂ) (X : K →L[ℂ] K) : S.flip (c • X) = c • S.flip X

The flip is complex-linear (the vendored swapDensity_smul).

theorem MIPRE.LIDT.Co.SymModel.swapDensity_mul {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (X Y : K →L[ℂ] K) : S.flip (X * Y) = S.flip X * S.flip Y

The flip preserves multiplication (the vendored swapDensity_mul).

theorem MIPRE.LIDT.Co.SymModel.qBipartiteMatchMass_symm_of_density_fixed {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Outcome : Type u_3} [Fintype Outcome] (A B : SubMeas Outcome 𝔓) : S.qBipartiteMatchMass A B = S.qBipartiteMatchMass B A

The bipartite matching mass is symmetric.

theorem MIPRE.LIDT.Co.SymModel.qBipartiteConsDefect_symm_of_density_fixed {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Outcome : Type u_3} [Fintype Outcome] (A B : SubMeas Outcome 𝔓) : S.qBipartiteConsDefect A B = S.qBipartiteConsDefect B A

The bipartite consistency defect is symmetric.

theorem MIPRE.LIDT.Co.SymModel.consRel_symm_of_density_fixed {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (A B : IdxSubMeas Question Outcome 𝔓) (δ : ℝ) : S.ConsRel 𝒟 A B δ → S.ConsRel 𝒟 B A δ

The bipartite consistency relation is symmetric.

Covariance of the line measurements

def MIPRE.LIDT.Co.AxisParallelMeasurementReparamInvariant {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (M : IdxProjMeas (MIPStarRE.LDT.AxisParallelLine params) (MIPStarRE.LDT.AxisLinePolynomial params) R) : Prop

Direct outcome-level covariance for axis-parallel-line measurements.

Rebasing a line question by t and reparametrizing an outcome polynomial by the same translation leaves the corresponding projector unchanged.

Equations

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

def MIPRE.LIDT.Co.DiagonalMeasurementReparamInvariant {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (M : IdxProjMeas (MIPStarRE.LDT.DiagonalLine params) (MIPStarRE.LDT.DiagonalLinePolynomial params) R) : Prop

Direct outcome-level covariance for diagonal-line measurements.

Rebasing a line question by t and reparametrizing an outcome polynomial by the same translation leaves the corresponding projector unchanged.

Equations

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

def MIPRE.LIDT.Co.DiagonalEvaluationReparamInvariant {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (M : IdxProjMeas (MIPStarRE.LDT.DiagonalLine params) (MIPStarRE.LDT.DiagonalLinePolynomial params) R) : Prop

Reparametrization invariance for diagonal-line measurements: evaluating a rebased line at zeroCoord agrees outcome-wise with evaluating the original line at the rebasing parameter.

At the answer level, the geometric identity is DiagonalLinePolynomial.reparamAt_apply_zero. This predicate is stronger: it asserts that the measurement family itself is covariant under rebasing the question index.

Equations

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

def MIPRE.LIDT.Co.AxisParallelEvaluationReparamInvariant {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (M : IdxProjMeas (MIPStarRE.LDT.AxisParallelLine params) (MIPStarRE.LDT.AxisLinePolynomial params) R) : Prop

Reparametrization invariance for axis-parallel-line measurements: evaluating a rebased line at zeroCoord agrees outcome-wise with evaluating the original line at the rebasing parameter.

Equations

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

noncomputable def MIPRE.LIDT.Co.AxisParallelLine.transportMeasurement {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] (M : ProjMeas (MIPStarRE.LDT.AxisLinePolynomial params) R) (t : MIPStarRE.LDT.Fq params) : ProjMeas (MIPStarRE.LDT.AxisLinePolynomial params) R

Transport an axis-parallel-line measurement along rebasing of the line question by translating its polynomial outcomes.

Equations

• MIPRE.LIDT.Co.AxisParallelLine.transportMeasurement M t = MIPRE.LIDT.Co.ProjMeas.transport (MIPStarRE.LDT.AxisLinePolynomial.reparamAtEquiv t) M

theorem MIPRE.LIDT.Co.AxisParallelLine.transportMeasurement_postprocess_zero {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] (M : ProjMeas (MIPStarRE.LDT.AxisLinePolynomial params) R) (t a : MIPStarRE.LDT.Fq params) : (postprocess (transportMeasurement M t).toSubMeas fun (x : MIPStarRE.LDT.AxisLinePolynomial params) => x.toFun MIPStarRE.LDT.zeroCoord).outcome a = (postprocess M.toSubMeas fun (f : MIPStarRE.LDT.AxisLinePolynomial params) => f.toFun t).outcome a

Evaluating a transported axis-line measurement at zeroCoord agrees with reading the original measurement at the rebasing parameter.

noncomputable def MIPRE.LIDT.Co.DiagonalLine.transportMeasurement {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] (M : ProjMeas (MIPStarRE.LDT.DiagonalLinePolynomial params) R) (t : MIPStarRE.LDT.Fq params) : ProjMeas (MIPStarRE.LDT.DiagonalLinePolynomial params) R

Transport a diagonal-line measurement along rebasing of the line question by translating its polynomial outcomes.

Equations

• MIPRE.LIDT.Co.DiagonalLine.transportMeasurement M t = MIPRE.LIDT.Co.ProjMeas.transport (MIPStarRE.LDT.DiagonalLinePolynomial.reparamAtEquiv t) M

theorem MIPRE.LIDT.Co.DiagonalLine.transportMeasurement_postprocess_zero {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] (M : ProjMeas (MIPStarRE.LDT.DiagonalLinePolynomial params) R) (t a : MIPStarRE.LDT.Fq params) : (postprocess (transportMeasurement M t).toSubMeas fun (x : MIPStarRE.LDT.DiagonalLinePolynomial params) => x.toFun MIPStarRE.LDT.zeroCoord).outcome a = (postprocess M.toSubMeas fun (f : MIPStarRE.LDT.DiagonalLinePolynomial params) => f.toFun t).outcome a

Evaluating a transported diagonal-line measurement at zeroCoord agrees with reading the original measurement at the rebasing parameter.

def MIPRE.LIDT.Co.AxisParallelMeasurementTransportInvariant {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (M : IdxProjMeas (MIPStarRE.LDT.AxisParallelLine params) (MIPStarRE.LDT.AxisLinePolynomial params) R) : Prop

Stronger rebasing compatibility for axis-parallel-line measurements: the measurement indexed by the rebased line is equal to the transport of the original measurement along the answer reparametrization equivalence.

Equations

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

def MIPRE.LIDT.Co.DiagonalMeasurementTransportInvariant {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (M : IdxProjMeas (MIPStarRE.LDT.DiagonalLine params) (MIPStarRE.LDT.DiagonalLinePolynomial params) R) : Prop

Stronger rebasing compatibility for diagonal-line measurements: the measurement indexed by the rebased line is equal to the transport of the original measurement along the answer reparametrization equivalence.

Equations

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

theorem MIPRE.LIDT.Co.AxisParallelMeasurementTransportInvariant.toMeasurementReparamInvariant {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {M : IdxProjMeas (MIPStarRE.LDT.AxisParallelLine params) (MIPStarRE.LDT.AxisLinePolynomial params) R} (hM : AxisParallelMeasurementTransportInvariant params M) : AxisParallelMeasurementReparamInvariant params M

Transport-level axis-parallel covariance implies direct outcome covariance.

theorem MIPRE.LIDT.Co.DiagonalMeasurementTransportInvariant.toMeasurementReparamInvariant {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {M : IdxProjMeas (MIPStarRE.LDT.DiagonalLine params) (MIPStarRE.LDT.DiagonalLinePolynomial params) R} (hM : DiagonalMeasurementTransportInvariant params M) : DiagonalMeasurementReparamInvariant params M

Transport-level diagonal covariance implies direct outcome covariance.

theorem MIPRE.LIDT.Co.AxisParallelMeasurementReparamInvariant.toTransportInvariant {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {M : IdxProjMeas (MIPStarRE.LDT.AxisParallelLine params) (MIPStarRE.LDT.AxisLinePolynomial params) R} (hM : AxisParallelMeasurementReparamInvariant params M) : AxisParallelMeasurementTransportInvariant params M

Direct axis-parallel outcome covariance implies transport-level covariance.

theorem MIPRE.LIDT.Co.DiagonalMeasurementReparamInvariant.toTransportInvariant {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {M : IdxProjMeas (MIPStarRE.LDT.DiagonalLine params) (MIPStarRE.LDT.DiagonalLinePolynomial params) R} (hM : DiagonalMeasurementReparamInvariant params M) : DiagonalMeasurementTransportInvariant params M

Direct diagonal outcome covariance implies transport-level covariance.

theorem MIPRE.LIDT.Co.axisParallelMeasurementReparamInvariant_iff_transportInvariant {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {M : IdxProjMeas (MIPStarRE.LDT.AxisParallelLine params) (MIPStarRE.LDT.AxisLinePolynomial params) R} : AxisParallelMeasurementReparamInvariant params M ↔ AxisParallelMeasurementTransportInvariant params M

Direct outcome covariance and transport-level covariance are equivalent for axis-parallel-line projective measurements.

theorem MIPRE.LIDT.Co.diagonalMeasurementReparamInvariant_iff_transportInvariant {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {M : IdxProjMeas (MIPStarRE.LDT.DiagonalLine params) (MIPStarRE.LDT.DiagonalLinePolynomial params) R} : DiagonalMeasurementReparamInvariant params M ↔ DiagonalMeasurementTransportInvariant params M

Direct outcome covariance and transport-level covariance are equivalent for diagonal-line projective measurements.

theorem MIPRE.LIDT.Co.AxisParallelMeasurementTransportInvariant.toEvaluationReparamInvariant {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {M : IdxProjMeas (MIPStarRE.LDT.AxisParallelLine params) (MIPStarRE.LDT.AxisLinePolynomial params) R} (hM : AxisParallelMeasurementTransportInvariant params M) : AxisParallelEvaluationReparamInvariant params M

The stronger transport-level axis-parallel compatibility implies the older outcome-level reparametrization invariant predicate.

theorem MIPRE.LIDT.Co.DiagonalMeasurementTransportInvariant.toEvaluationReparamInvariant {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {M : IdxProjMeas (MIPStarRE.LDT.DiagonalLine params) (MIPStarRE.LDT.DiagonalLinePolynomial params) R} (hM : DiagonalMeasurementTransportInvariant params M) : DiagonalEvaluationReparamInvariant params M

The stronger transport-level diagonal compatibility implies the older outcome-level reparametrization invariant predicate.

Covariant measurement families

structure MIPRE.LIDT.Co.AxisParallelCovariantMeasurement (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (R : Type u_1) [Ring R] [StarRing R] [PartialOrder R] : Type (max u_1 u_2)

Axis-parallel line measurements bundled with the stronger transport-level rebasing covariance.

• toIdxProjMeas : IdxProjMeas (MIPStarRE.LDT.AxisParallelLine params) (MIPStarRE.LDT.AxisLinePolynomial params) R
• transportInvariant : AxisParallelMeasurementTransportInvariant params self.toIdxProjMeas

@[instance_reducible]

instance MIPRE.LIDT.Co.instCoeFunAxisParallelCovariantMeasurementForallAxisParallelLineProjMeasAxisLinePolynomial {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] : CoeFun (AxisParallelCovariantMeasurement params R) fun (x : AxisParallelCovariantMeasurement params R) => MIPStarRE.LDT.AxisParallelLine params → ProjMeas (MIPStarRE.LDT.AxisLinePolynomial params) R

A covariant measurement is applied as its measurement family.

Equations

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

theorem MIPRE.LIDT.Co.AxisParallelCovariantMeasurement.reparamInvariant {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (M : AxisParallelCovariantMeasurement params R) : AxisParallelEvaluationReparamInvariant params M.toIdxProjMeas

A covariant wrapper automatically satisfies the older evaluation-level rebasing invariant.

structure MIPRE.LIDT.Co.DiagonalCovariantMeasurement (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (R : Type u_1) [Ring R] [StarRing R] [PartialOrder R] : Type (max u_1 u_2)

Diagonal line measurements bundled with the stronger transport-level rebasing covariance.

• toIdxProjMeas : IdxProjMeas (MIPStarRE.LDT.DiagonalLine params) (MIPStarRE.LDT.DiagonalLinePolynomial params) R
• transportInvariant : DiagonalMeasurementTransportInvariant params self.toIdxProjMeas

@[instance_reducible]

instance MIPRE.LIDT.Co.instCoeFunDiagonalCovariantMeasurementForallDiagonalLineProjMeasDiagonalLinePolynomial {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] : CoeFun (DiagonalCovariantMeasurement params R) fun (x : DiagonalCovariantMeasurement params R) => MIPStarRE.LDT.DiagonalLine params → ProjMeas (MIPStarRE.LDT.DiagonalLinePolynomial params) R

A covariant measurement is applied as its measurement family.

Equations

• MIPRE.LIDT.Co.instCoeFunDiagonalCovariantMeasurementForallDiagonalLineProjMeasDiagonalLinePolynomial = { coe := fun (M : MIPRE.LIDT.Co.DiagonalCovariantMeasurement params R) => M.toIdxProjMeas }

theorem MIPRE.LIDT.Co.DiagonalCovariantMeasurement.reparamInvariant {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (M : DiagonalCovariantMeasurement params R) : DiagonalEvaluationReparamInvariant params M.toIdxProjMeas

A covariant wrapper automatically satisfies the older evaluation-level rebasing invariant.

def MIPRE.LIDT.Co.DiagonalAnswerMeasurementTransportInvariant (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] (M : IdxProjMeas (MIPStarRE.LDT.DiagonalLine params) (MIPStarRE.LDT.DiagonalLineAnswer params) R) : Prop

Transport covariance for diagonal-line measurements whose answers are the paper-level line functions.

Equations

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

structure MIPRE.LIDT.Co.DiagonalAnswerCovariantMeasurement (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (R : Type u_1) [Ring R] [StarRing R] [PartialOrder R] : Type u_1

Diagonal-line measurements with paper-level function answers, bundled with transport-level rebasing covariance.

This parallel API is intended for the paper-faithful restriction redesign: unlike DiagonalLinePolynomial, the function-answer alphabet admits a total slice append/restrict equivalence.

• toIdxProjMeas : IdxProjMeas (MIPStarRE.LDT.DiagonalLine params) (MIPStarRE.LDT.DiagonalLineAnswer params) R
• transportInvariant : DiagonalAnswerMeasurementTransportInvariant params self.toIdxProjMeas

@[instance_reducible]

instance MIPRE.LIDT.Co.instCoeFunDiagonalAnswerCovariantMeasurementForallDiagonalLineProjMeasDiagonalLineAnswer {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] : CoeFun (DiagonalAnswerCovariantMeasurement params R) fun (x : DiagonalAnswerCovariantMeasurement params R) => MIPStarRE.LDT.DiagonalLine params → ProjMeas (MIPStarRE.LDT.DiagonalLineAnswer params) R

A covariant measurement is applied as its measurement family.

Equations

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

Symmetric strategies

structure MIPRE.LIDT.Co.AnswerSymStrat (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (𝔓 : Type u_1) [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (K : Type u_2) [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] : Type (max (max u_1 u_2) u_3)

Paper-level symmetric strategy data whose diagonal-line answers are functions.

This parallel structure is the target shape for the restriction redesign in Section 6: restricting an ambient diagonal line to a slice is total for function answers, unlike the current degree-bounded DiagonalLinePolynomial alphabet.

The vendored fields permInvState, densityFixed and isNormalized are theorems of the symmetric model state (see the module docstring).

• state : SymModel 𝔓 K
• pointMeasurement : IdxProjMeas (MIPStarRE.LDT.Point params) (MIPStarRE.LDT.Fq params) 𝔓
• axisParallelMeasurement : AxisParallelCovariantMeasurement params 𝔓
• diagonalMeasurement : DiagonalAnswerCovariantMeasurement params 𝔓

structure MIPRE.LIDT.Co.SymStrat (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (𝔓 : Type u_1) [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (K : Type u_2) [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] : Type (max (max u_1 u_2) u_3)

Paper-local symmetric strategy data.

The line-measurement fields are bundled as transport-covariant wrappers: rebasing the question index is required to agree with transporting the projective measurement along the corresponding answer reparametrization equivalence. This is stronger than the older evaluation-level formulas at zeroCoord, but those formulas remain available as derived lemmas via AxisParallelCovariantMeasurement.reparamInvariant and DiagonalCovariantMeasurement.reparamInvariant.

The state is a symmetric model (Co/Basic/QuantumState.lean): a unit vector Ψ in a Hilbert space K, with the local algebra 𝔓 placed on the two factors by state.L and state.R and exchanged by the flip state.flip, which fixes the state. So the swap symmetry and the normalization that the vendored structure carries as the fields permInvState, densityFixed and isNormalized are theorems here: strategy.state.ev_L_eq_ev_R, strategy.state.ev_flip and strategy.isNormalized.

• state : SymModel 𝔓 K
• pointMeasurement : IdxProjMeas (MIPStarRE.LDT.Point params) (MIPStarRE.LDT.Fq params) 𝔓
• axisParallelMeasurement : AxisParallelCovariantMeasurement params 𝔓
• diagonalMeasurement : DiagonalCovariantMeasurement params 𝔓

theorem MIPRE.LIDT.Co.SymStrat.isNormalized {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) : strategy.state.IsNormalized

The state of a symmetric strategy is normalized (the vendored field SymStrat.isNormalized, a theorem of the model).

theorem MIPRE.LIDT.Co.AnswerSymStrat.isNormalized {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] (strategy : AnswerSymStrat params 𝔓 K) : strategy.state.IsNormalized

The state of an answer-valued symmetric strategy is normalized (the vendored field AnswerSymStrat.isNormalized, a theorem of the model).

@[reducible, inline]

noncomputable abbrev MIPRE.LIDT.Co.axisParallelPointAnswerFamilyOf {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {R : Type u_3} [Ring R] [StarRing R] [PartialOrder R] (pointMeasurement : IdxProjMeas (MIPStarRE.LDT.Point params) (MIPStarRE.LDT.Fq params) R) : IdxSubMeas (MIPStarRE.LDT.AxisParallelTestSample params) (MIPStarRE.LDT.Fq params) R

Sampled point answers in the axis-parallel lines test, obtained from a point measurement.

Equations

• MIPRE.LIDT.Co.axisParallelPointAnswerFamilyOf pointMeasurement s = (pointMeasurement s.1).toSubMeas

@[reducible, inline]

noncomputable abbrev MIPRE.LIDT.Co.axisParallelLineAnswerFamilyOf {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {R : Type u_3} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (axisParallelMeasurement : MIPStarRE.LDT.AxisParallelLine params → ProjMeas (MIPStarRE.LDT.AxisLinePolynomial params) R) : IdxSubMeas (MIPStarRE.LDT.AxisParallelTestSample params) (MIPStarRE.LDT.Fq params) R

Sampled line answers in the axis-parallel lines test, obtained from an axis-parallel measurement and evaluated at the base point.

Equations

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

@[reducible, inline]

noncomputable abbrev MIPRE.LIDT.Co.diagonalPointAnswerFamilyOf {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {R : Type u_3} [Ring R] [StarRing R] [PartialOrder R] (pointMeasurement : IdxProjMeas (MIPStarRE.LDT.Point params) (MIPStarRE.LDT.Fq params) R) (j : Fin params.m) : IdxSubMeas (MIPStarRE.LDT.RestrictedDiagonalSample params j) (MIPStarRE.LDT.Fq params) R

Sampled point answers in the restricted diagonal test, obtained from a point measurement.

Equations

• MIPRE.LIDT.Co.diagonalPointAnswerFamilyOf pointMeasurement j s = (pointMeasurement s.1).toSubMeas

@[reducible, inline]

noncomputable abbrev MIPRE.LIDT.Co.diagonalLineAnswerFamilyOf {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {R : Type u_3} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {Answer : Type u_4} [Fintype Answer] (diagonalMeasurement : MIPStarRE.LDT.DiagonalLine params → ProjMeas Answer R) (evalAtBase : Answer → MIPStarRE.LDT.Fq params) (j : Fin params.m) : IdxSubMeas (MIPStarRE.LDT.RestrictedDiagonalSample params j) (MIPStarRE.LDT.Fq params) R

Sampled diagonal-line answers in the restricted diagonal test, obtained from a diagonal-line measurement and evaluated at the base point.

Equations

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

noncomputable def MIPRE.LIDT.Co.axisParallelPointAnswerFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) : IdxSubMeas (MIPStarRE.LDT.AxisParallelTestSample params) (MIPStarRE.LDT.Fq params) 𝔓

Sampled point answers in the axis-parallel lines test. The point player receives u (the base point) and answers with their measurement at u.

Equations

• MIPRE.LIDT.Co.axisParallelPointAnswerFamily strategy = MIPRE.LIDT.Co.axisParallelPointAnswerFamilyOf strategy.pointMeasurement

noncomputable def MIPRE.LIDT.Co.axisParallelLineAnswerFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) : IdxSubMeas (MIPStarRE.LDT.AxisParallelTestSample params) (MIPStarRE.LDT.Fq params) 𝔓

Sampled line answers in the axis-parallel lines test, evaluated at the base point u. The line player receives ℓ and returns a polynomial f. The verifier checks f(u) = a; since u = ℓ.pointAt zeroCoord, we evaluate f at zeroCoord.

Equations

• MIPRE.LIDT.Co.axisParallelLineAnswerFamily strategy = MIPRE.LIDT.Co.axisParallelLineAnswerFamilyOf strategy.axisParallelMeasurement.toIdxProjMeas

noncomputable def MIPRE.LIDT.Co.lastDirectionMeasurementFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) : IdxProjMeas (MIPStarRE.LDT.Point params) (MIPStarRE.LDT.AxisLinePolynomial params.next) 𝔓

The axis-parallel line measurement family restricted to the paper's last-direction notation u ↦ B^u.

Equations

• MIPRE.LIDT.Co.lastDirectionMeasurementFamily strategy u = strategy.axisParallelMeasurement.toIdxProjMeas (MIPStarRE.LDT.lastDirectionLine params u)

noncomputable def MIPRE.LIDT.Co.diagonalPointAnswerFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (j : Fin params.m) : IdxSubMeas (MIPStarRE.LDT.RestrictedDiagonalSample params j) (MIPStarRE.LDT.Fq params) 𝔓

Sampled point answers in the j-restricted diagonal test. The point player receives u and answers at u.

Equations

• MIPRE.LIDT.Co.diagonalPointAnswerFamily strategy j = MIPRE.LIDT.Co.diagonalPointAnswerFamilyOf strategy.pointMeasurement j

noncomputable def MIPRE.LIDT.Co.diagonalLineAnswerFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (j : Fin params.m) : IdxSubMeas (MIPStarRE.LDT.RestrictedDiagonalSample params j) (MIPStarRE.LDT.Fq params) 𝔓

Sampled diagonal-line answers in the j-restricted diagonal test, evaluated at the base point u. Since u = ℓ.pointAt zeroCoord, we evaluate f at zeroCoord.

Equations

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

noncomputable def MIPRE.LIDT.Co.AnswerSymStrat.axisParallelPointAnswerFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] (strategy : AnswerSymStrat params 𝔓 K) : IdxSubMeas (MIPStarRE.LDT.AxisParallelTestSample params) (MIPStarRE.LDT.Fq params) 𝔓

Sampled point answers in the axis-parallel lines test for an answer-valued symmetric strategy.

Equations

• strategy.axisParallelPointAnswerFamily = MIPRE.LIDT.Co.axisParallelPointAnswerFamilyOf strategy.pointMeasurement

noncomputable def MIPRE.LIDT.Co.AnswerSymStrat.axisParallelLineAnswerFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] (strategy : AnswerSymStrat params 𝔓 K) : IdxSubMeas (MIPStarRE.LDT.AxisParallelTestSample params) (MIPStarRE.LDT.Fq params) 𝔓

Sampled line answers in the axis-parallel lines test for an answer-valued symmetric strategy, evaluated at the base point.

Equations

• strategy.axisParallelLineAnswerFamily = MIPRE.LIDT.Co.axisParallelLineAnswerFamilyOf strategy.axisParallelMeasurement.toIdxProjMeas

noncomputable def MIPRE.LIDT.Co.AnswerSymStrat.diagonalPointAnswerFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] (strategy : AnswerSymStrat params 𝔓 K) (j : Fin params.m) : IdxSubMeas (MIPStarRE.LDT.RestrictedDiagonalSample params j) (MIPStarRE.LDT.Fq params) 𝔓

Sampled point answers in the restricted diagonal test for an answer-valued symmetric strategy.

Equations

• strategy.diagonalPointAnswerFamily j = MIPRE.LIDT.Co.diagonalPointAnswerFamilyOf strategy.pointMeasurement j

noncomputable def MIPRE.LIDT.Co.AnswerSymStrat.diagonalLineAnswerFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] (strategy : AnswerSymStrat params 𝔓 K) (j : Fin params.m) : IdxSubMeas (MIPStarRE.LDT.RestrictedDiagonalSample params j) (MIPStarRE.LDT.Fq params) 𝔓

Sampled diagonal-line answers in the restricted diagonal test for an answer-valued symmetric strategy, evaluated at the base point.

Equations

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

noncomputable def MIPRE.LIDT.Co.AnswerSymStrat.axisParallelFailureProbability {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] (strategy : AnswerSymStrat params 𝔓 K) : ℝ

Axis-parallel failure surrogate for an answer-valued symmetric strategy.

Equations

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

noncomputable def MIPRE.LIDT.Co.AnswerSymStrat.selfConsistencyFailureProbability {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] (strategy : AnswerSymStrat params 𝔓 K) : ℝ

Self-consistency failure surrogate for an answer-valued symmetric strategy.

Equations

• strategy.selfConsistencyFailureProbability = strategy.state.bipartiteSSCError (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas

noncomputable def MIPRE.LIDT.Co.AnswerSymStrat.diagonalFailureProbability {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] (strategy : AnswerSymStrat params 𝔓 K) : ℝ

Diagonal-line failure surrogate for an answer-valued symmetric strategy.

Equations

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

structure MIPRE.LIDT.Co.AnswerSymStrat.IsGood {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] (strategy : AnswerSymStrat params 𝔓 K) (eps delta gamma : ℝ) : Prop

Goodness data for an answer-valued symmetric strategy.

• axisParallelTest : strategy.axisParallelFailureProbability ≤ eps

  The axis-parallel test fails with probability at most eps.

• selfConsistencyTest : strategy.selfConsistencyFailureProbability ≤ delta

  The self-consistency test fails with probability at most delta.

• diagonalLineTest : strategy.diagonalFailureProbability ≤ gamma

  The diagonal-line test fails with probability at most gamma.

Two-space projective strategies

structure MIPRE.LIDT.Co.ProjStrat (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (𝒞 : Type u_1) [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (𝒜 : Type u_2) [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] (ℬ : Type u_3) [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] : Type (max (max (max (max (u + 1) u_1) u_2) u_3) u_4)

Paper-faithful two-space projective strategy data.

This matches the paper's def:general-projective-strategy (test_definition.tex, lines 98--115): Alice's and Bob's measurements act on separate local algebras 𝒜 and ℬ, and the state is a bipartite model of the repository (MIPRE.BipartiteModel 𝒞 𝒜 ℬ, MIPRE/Foundations/BipartiteModel.lean), a vector state on a Hilbert space on which 𝒜 and ℬ act by commuting representations, without a built-in swap symmetry. This replaces the vendored state on the tensor product ιA × ιB of two matrix carriers.

The isNormalized field records that the state is a unit vector (a bipartite model carries no normalization).

The four covariance conditions express that the line-indexed projectors descend from chosen affine parametrizations to geometric lines; transport and zero-coordinate evaluation are equivalent consequences.

• state : BipartiteModel 𝒞 𝒜 ℬ

  The bipartite state: a vector state with commuting representations of 𝒜 and ℬ.

• isNormalized : ‖self.state.ψ‖ = 1

  The state is a unit vector.

• pointMeasurementA : IdxProjMeas (MIPStarRE.LDT.Point params) (MIPStarRE.LDT.Fq params) 𝒜

  Alice's point-measurement family, in 𝒜.

• axisParallelMeasurementA : IdxProjMeas (MIPStarRE.LDT.AxisParallelLine params) (MIPStarRE.LDT.AxisLinePolynomial params) 𝒜

  Alice's axis-parallel-line measurement family, in 𝒜.

• axisParallelReparamInvariantA : AxisParallelMeasurementReparamInvariant params self.axisParallelMeasurementA

  Alice's axis-parallel measurement is covariant under line rebasing.

• diagonalMeasurementA : IdxProjMeas (MIPStarRE.LDT.DiagonalLine params) (MIPStarRE.LDT.DiagonalLinePolynomial params) 𝒜

  Alice's diagonal-line measurement family, in 𝒜.

• diagonalReparamInvariantA : DiagonalMeasurementReparamInvariant params self.diagonalMeasurementA

  Alice's diagonal measurement is covariant under line rebasing.

• pointMeasurementB : IdxProjMeas (MIPStarRE.LDT.Point params) (MIPStarRE.LDT.Fq params) ℬ

  Bob's point-measurement family, in ℬ.

• axisParallelMeasurementB : IdxProjMeas (MIPStarRE.LDT.AxisParallelLine params) (MIPStarRE.LDT.AxisLinePolynomial params) ℬ

  Bob's axis-parallel-line measurement family, in ℬ.

• axisParallelReparamInvariantB : AxisParallelMeasurementReparamInvariant params self.axisParallelMeasurementB

  Bob's axis-parallel measurement is covariant under line rebasing.

• diagonalMeasurementB : IdxProjMeas (MIPStarRE.LDT.DiagonalLine params) (MIPStarRE.LDT.DiagonalLinePolynomial params) ℬ

  Bob's diagonal-line measurement family, in ℬ.

• diagonalReparamInvariantB : DiagonalMeasurementReparamInvariant params self.diagonalMeasurementB

  Bob's diagonal measurement is covariant under line rebasing.