The symmetric strategy of a two-space strategy

Theorem D of reports/c6b-paper-proofs.md, §4 (Lemma 12; symmetrization placed after the bridge), for the doubled model Doubling.model hM hψ of Co/Doubling/Model.lean. A two-space projective strategy strategy : ProjStrat params 𝒞 𝒜 ℬ (Co/Test/StrategyCore.lean) whose state M is a finite pair doubles to a symmetric strategy Doubling.symmStrat strategy hM of the doubled model, whose every measurement family is the componentwise pairing of the first and the second player's, and the failure probabilities of the doubled strategy are the role averages of the two-space surrogate of Co/Test/StrategyBiProj/Measurements.lean:

• symmStrat_axisParallel_eq_roleAverage: axis(S_D) = axisParallelRoleAverage(S);
• symmStrat_selfConsistency_eq_pointAgreement: selfCons(S_D) = pointAgreement(S);
• symmStrat_diagonal_eq_roleAverage: diag(S_D) = diagonalRoleAverage(S);
• symmStrat_isGood_three_mul: a strategy passing the test with error ε doubles to a (3ε, 3ε, 3ε)-good symmetric strategy, the constants of the vendored roleRegisterSymmStrategy_is_good_three_mul (LDT/Test/StrategyBiProjRoleAverage/Final.lean), which this replaces.

The pairing. SubMeas.prod, Measurement.prod and ProjMeas.prod pair two families with the same outcomes into the product algebra, componentwise; Doubling.pairProjMeas hM P Q translates the pairing of P in 𝒜 and Q in ℬ to the doubled local algebra Loc M along Doubling.equiv (Co/Doubling/FinitePair.lean). Its components are P and Q again (subMeasA_pairProjMeas, subMeasB_pairProjMeas). Covariance holds componentwise (pairAxisParallel_reparamInvariant, pairDiagonal_reparamInvariant).

The halving (bipartiteConsError_model): the port's symmetric-model defect of two families of the doubled model is the average of the two two-space defects of M at their components, the max 0 of the definitions being inactive on both sides (qBipartiteConsDefect_model of Co/Doubling/Halving.lean). So a doubled defect at most σ bounds each role assignment by 2σ (bipartiteConsError_components_le_two_mul), the arithmetic of Theorem E (unsymmetrization at the vendored cut), whose input, the point consistency of the ported mainInduction's measurement, is milestone M13's. For measurements the two-space defect is the inconsistency of M (bipartiteConsError_eq_inconsistency), the form MIPRE.LIDT.Simul.SoundIn concludes with.

Componentwise pairing

def MIPRE.LIDT.Co.SubMeas.prod {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] {T : Type u_3} [Ring T] [StarRing T] [PartialOrder T] (A : SubMeas α R) (B : SubMeas α T) : SubMeas α (R × T)

The componentwise pairing (A ⊠ B)_a = (A_a, B_a) of two submeasurements with the same outcomes, a submeasurement of the product algebra.

Equations

• A.prod B = { outcome := fun (a : α) => (A.outcome a, B.outcome a), total := (A.total, B.total), outcome_pos := ⋯, sum_eq_total := ⋯, total_le_one := ⋯ }

def MIPRE.LIDT.Co.Measurement.prod {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] {T : Type u_3} [Ring T] [StarRing T] [PartialOrder T] (A : Measurement α R) (B : Measurement α T) : Measurement α (R × T)

The componentwise pairing of two measurements, a measurement of the product algebra.

Equations

• A.prod B = { toSubMeas := A.prod B.toSubMeas, total_eq_one := ⋯ }

def MIPRE.LIDT.Co.ProjMeas.prod {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] {T : Type u_3} [Ring T] [StarRing T] [PartialOrder T] (A : ProjMeas α R) (B : ProjMeas α T) : ProjMeas α (R × T)

The componentwise pairing of two projective measurements, a projective measurement of the product algebra.

Equations

• A.prod B = { toMeasurement := A.prod B.toMeasurement, proj := ⋯ }

@[simp]

theorem MIPRE.LIDT.Co.ProjMeas.prod_outcome {α : Type u_1} [Fintype α] {R : Type u_2} [Ring R] [StarRing R] [PartialOrder R] {T : Type u_3} [Ring T] [StarRing T] [PartialOrder T] (A : ProjMeas α R) (B : ProjMeas α T) (a : α) : (A.prod B).outcome a = (A.outcome a, B.outcome a)

The outcomes of a paired projective measurement are the pairs of outcomes.

theorem MIPRE.LIDT.Co.SubMeas.map_postprocess {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {R : Type u_3} [Ring R] [StarRing R] [Algebra ℂ R] [PartialOrder R] [StarOrderedRing R] {T : Type u_4} [Ring T] [StarRing T] [Algebra ℂ T] [PartialOrder T] [StarOrderedRing T] (g : R →⋆ₐ[ℂ] T) (A : SubMeas α R) (f : α → β) : map g (postprocess A f) = postprocess (map g A) f

Postprocessing commutes with the image under a ⋆-homomorphism.

The two-space defect of measurements is the inconsistency

theorem MIPRE.LIDT.Co.bipartiteConsError_eq_inconsistency {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {Question : Type u_4} {Outcome : Type u_5} [Fintype Question] [Fintype Outcome] [DecidableEq Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (A : IdxMeas Question Outcome 𝒜) (B : IdxMeas Question Outcome ℬ) : bipartiteConsError M 𝒟 A.toIdxSubMeas B.toIdxSubMeas = M.inconsistency 𝒟.weight (fun (q : Question) => (A q).toPOVMIn) fun (q : Question) => (B q).toPOVMIn

The two-space consistency error of two measurement families is the inconsistency of M (MIPRE.BipartiteModel.inconsistency), weighted by the question distribution: the form of the consistency conclusions of MIPRE.LIDT.Simul.SoundIn.

The components of a submeasurement

noncomputable def MIPRE.LIDT.Co.Doubling.subMeasA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) {Outcome : Type u_4} [Fintype Outcome] (X : SubMeas Outcome (Loc M)) : SubMeas Outcome 𝒜

The first components of a submeasurement of the doubled local algebra, a submeasurement of 𝒜 (the image under compA).

Equations

• MIPRE.LIDT.Co.Doubling.subMeasA hM X = MIPRE.LIDT.Co.SubMeas.map (MIPRE.LIDT.Co.Doubling.compA hM) X

noncomputable def MIPRE.LIDT.Co.Doubling.subMeasB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) {Outcome : Type u_4} [Fintype Outcome] (X : SubMeas Outcome (Loc M)) : SubMeas Outcome ℬ

The second components of a submeasurement of the doubled local algebra, a submeasurement of ℬ (the image under compB).

Equations

• MIPRE.LIDT.Co.Doubling.subMeasB hM X = MIPRE.LIDT.Co.SubMeas.map (MIPRE.LIDT.Co.Doubling.compB hM) X

theorem MIPRE.LIDT.Co.Doubling.subMeasA_postprocess {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) {α : Type u_4} {β : Type u_5} [Fintype α] [Fintype β] (X : SubMeas α (Loc M)) (f : α → β) : subMeasA hM (postprocess X f) = postprocess (subMeasA hM X) f

Taking first components commutes with postprocessing.

theorem MIPRE.LIDT.Co.Doubling.subMeasB_postprocess {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) {α : Type u_4} {β : Type u_5} [Fintype α] [Fintype β] (X : SubMeas α (Loc M)) (f : α → β) : subMeasB hM (postprocess X f) = postprocess (subMeasB hM X) f

Taking second components commutes with postprocessing.

The halving of the bipartite defect

theorem MIPRE.LIDT.Co.Doubling.qBipartiteConsDefect_model_eq {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hψ : ‖M.ψ‖ = 1) {Outcome : Type u_4} [Fintype Outcome] [DecidableEq Outcome] (X Y : SubMeas Outcome (Loc M)) : (model hM hψ).qBipartiteConsDefect X Y = 2⁻¹ * (qBipartiteConsDefect M (subMeasA hM X) (subMeasB hM Y) + qBipartiteConsDefect M (subMeasA hM Y) (subMeasB hM X))

The bipartite defect halves (Theorem C of reports/c6b-paper-proofs.md, §4), in the vocabulary of the two-space defect: the symmetric-model defect of two submeasurements of the doubled model is the average of the two-space defects of M at the components X¹, Y² and Y¹, X².

theorem MIPRE.LIDT.Co.Doubling.bipartiteConsError_model {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hψ : ‖M.ψ‖ = 1) {Question : Type u_4} {Outcome : Type u_5} [Fintype Outcome] [DecidableEq Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (X Y : IdxSubMeas Question Outcome (Loc M)) : (model hM hψ).bipartiteConsError 𝒟 X Y = 2⁻¹ * ((bipartiteConsError M 𝒟 (fun (q : Question) => subMeasA hM (X q)) fun (q : Question) => subMeasB hM (Y q)) + bipartiteConsError M 𝒟 (fun (q : Question) => subMeasA hM (Y q)) fun (q : Question) => subMeasB hM (X q))

The averaged bipartite defect halves: the symmetric-model consistency error of two families of the doubled model is the average of the two-space consistency errors of M at their components.

theorem MIPRE.LIDT.Co.Doubling.bipartiteConsError_components_le_two_mul {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) (hψ : ‖M.ψ‖ = 1) {Question : Type u_4} {Outcome : Type u_5} [Fintype Outcome] [DecidableEq Outcome] (𝒟 : MIPStarRE.LDT.Distribution Question) (X Y : IdxSubMeas Question Outcome (Loc M)) {σ : ℝ} (h : (model hM hψ).bipartiteConsError 𝒟 X Y ≤ σ) : (bipartiteConsError M 𝒟 (fun (q : Question) => subMeasA hM (X q)) fun (q : Question) => subMeasB hM (Y q)) ≤ 2 * σ ∧ (bipartiteConsError M 𝒟 (fun (q : Question) => subMeasA hM (Y q)) fun (q : Question) => subMeasB hM (X q)) ≤ 2 * σ

Each role assignment costs at most twice the doubled defect (the arithmetic of Theorem E of reports/c6b-paper-proofs.md, §4, Lemma 13): if the doubled defect of two families is at most σ, each of the two two-space defects of M at their components is at most 2σ.

The paired measurements

noncomputable def MIPRE.LIDT.Co.Doubling.pairProjMeas {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) {α : Type u_4} [Fintype α] (P : ProjMeas α 𝒜) (Q : ProjMeas α ℬ) : ProjMeas α (Loc M)

The paired projective measurement in the doubled model: the componentwise pairing of a projective measurement P of 𝒜 and Q of ℬ, translated to the doubled local algebra Loc M along Doubling.equiv.

Equations

• MIPRE.LIDT.Co.Doubling.pairProjMeas hM P Q = MIPRE.LIDT.Co.ProjMeas.map (MIPRE.LIDT.Co.Doubling.equiv hM).toStarAlgHom (P.prod Q)

theorem MIPRE.LIDT.Co.Doubling.pairProjMeas_outcome {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) {α : Type u_4} [Fintype α] (P : ProjMeas α 𝒜) (Q : ProjMeas α ℬ) (a : α) : (pairProjMeas hM P Q).outcome a = (equiv hM) (P.outcome a, Q.outcome a)

The outcomes of a paired projective measurement are the translated pairs of outcomes.

@[simp]

theorem MIPRE.LIDT.Co.Doubling.subMeasA_pairProjMeas {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) {α : Type u_4} [Fintype α] (P : ProjMeas α 𝒜) (Q : ProjMeas α ℬ) : subMeasA hM (pairProjMeas hM P Q).toSubMeas = P.toSubMeas

The first components of a paired projective measurement are the first measurement.

@[simp]

theorem MIPRE.LIDT.Co.Doubling.subMeasB_pairProjMeas {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) {α : Type u_4} [Fintype α] (P : ProjMeas α 𝒜) (Q : ProjMeas α ℬ) : subMeasB hM (pairProjMeas hM P Q).toSubMeas = Q.toSubMeas

The second components of a paired projective measurement are the second measurement.

Covariance, componentwise

theorem MIPRE.LIDT.Co.Doubling.pairAxisParallel_reparamInvariant {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {A : IdxProjMeas (MIPStarRE.LDT.AxisParallelLine params) (MIPStarRE.LDT.AxisLinePolynomial params) 𝒜} {B : IdxProjMeas (MIPStarRE.LDT.AxisParallelLine params) (MIPStarRE.LDT.AxisLinePolynomial params) ℬ} (hA : AxisParallelMeasurementReparamInvariant params A) (hB : AxisParallelMeasurementReparamInvariant params B) : AxisParallelMeasurementReparamInvariant params fun (ℓ : MIPStarRE.LDT.AxisParallelLine params) => pairProjMeas hM (A ℓ) (B ℓ)

Covariance of the paired axis-parallel measurements: if both players' axis-parallel families are covariant under rebasing, so is their pairing.

theorem MIPRE.LIDT.Co.Doubling.pairDiagonal_reparamInvariant {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {A : IdxProjMeas (MIPStarRE.LDT.DiagonalLine params) (MIPStarRE.LDT.DiagonalLinePolynomial params) 𝒜} {B : IdxProjMeas (MIPStarRE.LDT.DiagonalLine params) (MIPStarRE.LDT.DiagonalLinePolynomial params) ℬ} (hA : DiagonalMeasurementReparamInvariant params A) (hB : DiagonalMeasurementReparamInvariant params B) : DiagonalMeasurementReparamInvariant params fun (ℓ : MIPStarRE.LDT.DiagonalLine params) => pairProjMeas hM (A ℓ) (B ℓ)

Covariance of the paired diagonal measurements: if both players' diagonal families are covariant under rebasing, so is their pairing.

The symmetric strategy

noncomputable def MIPRE.LIDT.Co.Doubling.symmStrat {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 ℬ] (strategy : ProjStrat params 𝒞 𝒜 ℬ) (hM : strategy.state.IsFinitePair) : SymStrat params (Loc strategy.state) (OperatorMatrix.Ampl (Fin 2) strategy.state.H)

The symmetric strategy of a two-space strategy (Theorem D of reports/c6b-paper-proofs.md, §4): on the doubled model of the strategy's state, every family is the componentwise pairing of the first and the second player's, and the line families are covariant componentwise. This replaces the vendored role-register symmetrization ProjStrat.roleRegisterSymmStrategy.

Equations

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

@[simp]

theorem MIPRE.LIDT.Co.Doubling.symmStrat_state {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 ℬ] (strategy : ProjStrat params 𝒞 𝒜 ℬ) (hM : strategy.state.IsFinitePair) : (symmStrat strategy hM).state = model hM ⋯

The state of the symmetric strategy is the doubled model.

theorem MIPRE.LIDT.Co.Doubling.symmStrat_pointMeasurement {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 ℬ] (strategy : ProjStrat params 𝒞 𝒜 ℬ) (hM : strategy.state.IsFinitePair) (u : MIPStarRE.LDT.Point params) : (symmStrat strategy hM).pointMeasurement u = pairProjMeas hM (strategy.pointMeasurementA u) (strategy.pointMeasurementB u)

The point measurements of the symmetric strategy are the paired point measurements.

theorem MIPRE.LIDT.Co.Doubling.symmStrat_axisParallelMeasurement {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 ℬ] (strategy : ProjStrat params 𝒞 𝒜 ℬ) (hM : strategy.state.IsFinitePair) (ℓ : MIPStarRE.LDT.AxisParallelLine params) : (symmStrat strategy hM).axisParallelMeasurement.toIdxProjMeas ℓ = pairProjMeas hM (strategy.axisParallelMeasurementA ℓ) (strategy.axisParallelMeasurementB ℓ)

The axis-parallel measurements of the symmetric strategy are the paired axis-parallel measurements.

theorem MIPRE.LIDT.Co.Doubling.symmStrat_diagonalMeasurement {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 ℬ] (strategy : ProjStrat params 𝒞 𝒜 ℬ) (hM : strategy.state.IsFinitePair) (ℓ : MIPStarRE.LDT.DiagonalLine params) : (symmStrat strategy hM).diagonalMeasurement.toIdxProjMeas ℓ = pairProjMeas hM (strategy.diagonalMeasurementA ℓ) (strategy.diagonalMeasurementB ℓ)

The diagonal measurements of the symmetric strategy are the paired diagonal measurements.

The failure probabilities are the role averages

theorem MIPRE.LIDT.Co.Doubling.symmStrat_axisParallel_eq_roleAverage {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 ℬ] (strategy : ProjStrat params 𝒞 𝒜 ℬ) (hM : strategy.state.IsFinitePair) : (symmStrat strategy hM).axisParallelFailureProbability = strategy.axisParallelRoleAverage

The axis-parallel branch (Theorem D): the axis-parallel failure probability of the symmetric strategy is the two-space role average axisParallelRoleAverage.

theorem MIPRE.LIDT.Co.SymModel.qBipartiteSSCDefect_eq_qBipartiteConsDefect {𝔓 : Type u_4} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_5} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {Outcome : Type u_6} [Fintype Outcome] (X : SubMeas Outcome 𝔓) (hX : X.total = 1) : S.qBipartiteSSCDefect X = S.qBipartiteConsDefect X X

For a measurement (total 1), the bipartite strong self-consistency defect of a symmetric model is its bipartite consistency defect with itself.

theorem MIPRE.LIDT.Co.Doubling.symmStrat_selfConsistency_eq_pointAgreement {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 ℬ] (strategy : ProjStrat params 𝒞 𝒜 ℬ) (hM : strategy.state.IsFinitePair) : (symmStrat strategy hM).selfConsistencyFailureProbability = strategy.pointAgreementFailureProbability

The self-consistency branch (Theorem D): the self-consistency failure probability of the symmetric strategy is the two-space point agreement pointAgreementFailureProbability.

theorem MIPRE.LIDT.Co.Doubling.symmStrat_diagonal_eq_roleAverage {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 ℬ] (strategy : ProjStrat params 𝒞 𝒜 ℬ) (hM : strategy.state.IsFinitePair) : (symmStrat strategy hM).diagonalFailureProbability = strategy.diagonalRoleAverage

The diagonal branch (Theorem D): the diagonal failure probability of the symmetric strategy is the two-space role average diagonalRoleAverage.

theorem MIPRE.LIDT.Co.Doubling.symmStrat_isGood_three_mul {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 ℬ] (strategy : ProjStrat params 𝒞 𝒜 ℬ) (hM : strategy.state.IsFinitePair) {eps : ℝ} (hpass : strategy.PassesLowIndividualDegreeTest eps) : (symmStrat strategy hM).IsGood (3 * eps) (3 * eps) (3 * eps)

Symmetrization after the bridge (Theorem D of reports/c6b-paper-proofs.md, §4): a two-space strategy on a finite pair passing the low-individual-degree test with error ε doubles to a (3ε, 3ε, 3ε)-good symmetric strategy, the constants of the vendored roleRegisterSymmStrategy_is_good_three_mul.