The model chain, part 3: the seeded test at one codeword, by reduction

The model counterpart of the repository's MIPRE/Background/LIDT/Adapter/Reduction.lean (not a vendored file: its matrix statements serve the tensor instance and stay), in the port of planning/c6b-plan.md (milestone M14, unit M14-4). It is the ldc = 1 case of thm:lidt-cl-soundness in any bipartite model M : MIPRE.BipartiteModel 𝒞 𝒜 ℬ with the instance set of MIPRE.LIDT.Simul.SoundIn, from the canonical-line theorem in M, MIPRE.LIDT.Co.Chain.SoundLidtIn M (Co/Chain/Defs.lean), taken as a hypothesis.

The argument is the matrix one:

• a projective strategy S for clGame with ldc = 1 is played as one for lidtGame (adapted), through MIPRE.BipartiteModel.ProjStrat.adapt, reindexing the questions along the classical qmapS and coarse-graining the answers along amap;
• the classical hD_qmap and pushforward_le make the averaging lemma MIPRE.BipartiteModel.exists_one_sub_povmValue_adapt_le produce a seed whose adapted strategy fails at most 3m times as often;
• SoundLidtIn M applies to it, at hd : 1 ≤ d, and returns two projective measurements of polynomials;
• the three conclusions are carried back through the coordinate reversal: on the questions by revPoint, which preserves the uniform distribution (inconsistency_uniform_comp), on the polynomials by revPolyEquiv (revMeas, MIPRE.BipartiteModel.inconsistency_map_equiv).

clSoundness_ldc_one states the conclusion with the canonical-line error, and clSoundness_ldc_one_deltaCL with the blueprint's δ_CL, through the classical lidtError_le_deltaCL and the choice k = clK m d.

The conclusions are read with CL.pointPOVMAIn S and CL.pointPOVMBIn S, the model forms of MIPRE.LIDT.CL.pointPOVMA, pointPOVMB: the point measurements with outcomes in F (the tuple readings MIPRE.LIDT.Simul.tuplePOVMAIn at r = 1 have outcomes in Fin 1 → F, and do not serve).

Reused by import. The classical content of Adapter/* is named through explicit open lists: revPoint, revPolyEquiv, eval_revPoly, Seed, qmapS, qmapS_point, amap, toValue_amap_point, hD_qmap, pushforward_le, nonempty_seed (namespace MIPRE.LIDT.Adapter); lidtError_le_deltaCL, deltaCL, clK, le_clK and clK_pos are in MIPRE.LIDT and need no open.

Not ported

The model forms of adapted, revMeas, clSoundness_ldc_one and clSoundness_ldc_one_deltaCL are declared here under their names. clSoundness_ldc_one takes SoundLidtIn M and 1 ≤ d (the hypothesis of SoundLidtIn) in addition to the matrix hypotheses, and its measurements are POVMIns with IsPVMIn carried beside them. Of the rest:

• revExp, revPoly, eval_revPoly, revPolyEquiv, toValue_amap_point: classical, imported.
• val_mats_map: the operators of a matrix coarse-graining; for POVMIn it is MIPRE.POVMIn.map_op.
• sum_filter_comp: composing two matrix coarse-grainings; for POVMIn it is MIPRE.POVMIn.map_map.
• val_mats_pointPOVMA_adapted, val_mats_pointPOVMB_adapted: replaced by pointPOVMAIn_adapted, pointPOVMBIn_adapted, equalities of POVMs rather than of their operators.
• val_mats_evalPOVM_revMeas: replaced by evalPOVMIn_revMeas, likewise.

New here

• CL.pointPOVMAIn, CL.pointPOVMBIn: above.
• pointPOVMAIn_adapted, pointPOVMBIn_adapted, evalPOVMIn_revMeas: above.
• revMeas_isPVMIn: the reversal of a projective measurement is projective.
• inconsistency_uniform_comp: relabelling the questions along a bijection keeps the inconsistency on the uniform distribution (the question half of the matrix MIPRE.inconsistency_congr).

The readings of the conclusions

def MIPRE.LIDT.Co.Chain.CL.pointPOVMAIn {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {F : Type u_4} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {hm : m ∣ Fintype.card F} (S : M.ProjStrat (CL.clGame hm)) (u : Point F m) : POVMIn F 𝒜

The first player's point measurements of a projective strategy for the seeded test with one codeword, as POVMs with outcomes in F (the model form of MIPRE.LIDT.CL.pointPOVMA).

Equations

• MIPRE.LIDT.Co.Chain.CL.pointPOVMAIn S u = MIPRE.POVMIn.map MIPRE.LIDT.CL.Answer.toValue (S.PA (MIPRE.LIDT.CL.Question.point u))

def MIPRE.LIDT.Co.Chain.CL.pointPOVMBIn {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {F : Type u_4} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {hm : m ∣ Fintype.card F} (S : M.ProjStrat (CL.clGame hm)) (u : Point F m) : POVMIn F ℬ

The second player's point measurements, as for pointPOVMAIn (the model form of MIPRE.LIDT.CL.pointPOVMB).

Equations

• MIPRE.LIDT.Co.Chain.CL.pointPOVMBIn S u = MIPRE.POVMIn.map MIPRE.LIDT.CL.Answer.toValue (S.PB (MIPRE.LIDT.CL.Question.point u))

The adapted strategy and its point measurements

noncomputable def MIPRE.LIDT.Co.Chain.adapted {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {F : Type u_4} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {hm : m ∣ Fintype.card F} (σc : Adapter.Seed F m) (S : M.ProjStrat (CL.clGame hm)) : M.ProjStrat (lidtGame F m d)

The strategy the adapter builds, for one member σc of the averaging family: S played on the canonical-line test through qmapS and amap.

Equations

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

theorem MIPRE.LIDT.Co.Chain.pointPOVMAIn_adapted {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {F : Type u_4} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {hm : m ∣ Fintype.card F} (σc : Adapter.Seed F m) (S : M.ProjStrat (CL.clGame hm)) (u : Point F m) : CL.pointPOVMAIn S u = pointPOVMAIn (adapted σc S) (Adapter.revPoint u)

A's point measurement of the adapted strategy is A's point measurement of the seeded strategy at the reversed point.

theorem MIPRE.LIDT.Co.Chain.pointPOVMBIn_adapted {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {F : Type u_4} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {hm : m ∣ Fintype.card F} (σc : Adapter.Seed F m) (S : M.ProjStrat (CL.clGame hm)) (u : Point F m) : CL.pointPOVMBIn S u = pointPOVMBIn (adapted σc S) (Adapter.revPoint u)

B's point measurement, likewise.

Reversing the low-degree measurements

def MIPRE.LIDT.Co.Chain.revMeas {F : Type u_4} [Fintype F] [DecidableEq F] {m d : ℕ} {R : Type u_5} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (G : POVMIn LowIndDegPoly R) : POVMIn LowIndDegPoly R

The reversal of a measurement with polynomial outcomes: its outcomes relabelled along revPolyEquiv.

Equations

• MIPRE.LIDT.Co.Chain.revMeas G = MIPRE.POVMIn.map (⇑MIPRE.LIDT.Adapter.revPolyEquiv) G

theorem MIPRE.LIDT.Co.Chain.revMeas_isPVMIn {F : Type u_4} [Fintype F] [DecidableEq F] {m d : ℕ} {R : Type u_5} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {G : POVMIn LowIndDegPoly R} (hG : IsPVMIn G.op) : IsPVMIn (revMeas G).op

The reversal of a projective measurement is projective.

theorem MIPRE.LIDT.Co.Chain.evalPOVMIn_revMeas {F : Type u_4} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} {R : Type u_5} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (G : POVMIn LowIndDegPoly R) (u : Point F m) : evalPOVMIn (revMeas G) u = evalPOVMIn G (Adapter.revPoint u)

Evaluating the reversal is evaluating at the reversed point.

theorem MIPRE.LIDT.Co.Chain.inconsistency_uniform_comp {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {X : Type u_4} {Λ : Type u_5} [Fintype X] [Fintype Λ] [DecidableEq Λ] (e : X ≃ X) (P : X → POVMIn Λ 𝒜) (Q : X → POVMIn Λ ℬ) : (M.inconsistency (uniform X) (fun (x : X) => P (e x)) fun (x : X) => Q (e x)) = M.inconsistency (uniform X) P Q

Relabelling the questions along a bijection keeps the inconsistency on the uniform distribution.

The reduction

theorem MIPRE.LIDT.Co.Chain.clSoundness_ldc_one {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {F : Type} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {hm : m ∣ Fintype.card F} (h : SoundLidtIn M) (S : M.ProjStrat (CL.clGame hm)) (ε : ℝ) (hS : 1 - ε ≤ S.value) (hd : 1 ≤ d) (k : ℕ) (hk : 400 * m * d ≤ k) (hk0 : 0 < k) : ∃ (GA : POVMIn LowIndDegPoly 𝒜) (GB : POVMIn LowIndDegPoly ℬ), IsPVMIn GA.op ∧ IsPVMIn GB.op ∧ M.inconsistency (uniform (Point F m)) (CL.pointPOVMAIn S) (evalPOVMIn GB) ≤ lidtError m d (Fintype.card F) k (3 * ↑m * ε) ∧ M.inconsistency (uniform (Point F m)) (evalPOVMIn GA) (CL.pointPOVMBIn S) ≤ lidtError m d (Fintype.card F) k (3 * ↑m * ε) ∧ (M.inconsistency (uniform Unit) (fun (x : Unit) => GA) fun (x : Unit) => GB) ≤ lidtError m d (Fintype.card F) k (3 * ↑m * ε)

Soundness of the seeded CL test at ldc = 1 in the model M, by reduction to the canonical-line test (the model form of MIPRE.LIDT.Adapter.clSoundness_ldc_one). If the canonical-line theorem holds in M, a projective strategy for clGame passing with probability at least 1 - ε has point measurements consistent, up to lidtError m d q k (3m ε), with the evaluations of a projective measurement of polynomials of individual degree d held by the other player, the two measurements consistent with each other; k ≥ 400 m d is free.

theorem MIPRE.LIDT.Co.Chain.clSoundness_ldc_one_deltaCL {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {F : Type} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {hm : m ∣ Fintype.card F} (h : SoundLidtIn M) (S : M.ProjStrat (CL.clGame hm)) (ε : ℝ) (hε : 0 ≤ ε) (hS : 1 - ε ≤ S.value) (hm1 : 1 ≤ m) (hd : 1 ≤ d) : ∃ (GA : POVMIn LowIndDegPoly 𝒜) (GB : POVMIn LowIndDegPoly ℬ), IsPVMIn GA.op ∧ IsPVMIn GB.op ∧ M.inconsistency (uniform (Point F m)) (CL.pointPOVMAIn S) (evalPOVMIn GB) ≤ deltaCL (Fintype.card F) m d ε ∧ M.inconsistency (uniform (Point F m)) (evalPOVMIn GA) (CL.pointPOVMBIn S) ≤ deltaCL (Fintype.card F) m d ε ∧ (M.inconsistency (uniform Unit) (fun (x : Unit) => GA) fun (x : Unit) => GB) ≤ deltaCL (Fintype.card F) m d ε

The ldc = 1 case of thm:lidt-cl-soundness in the model M (the model form of MIPRE.LIDT.Adapter.clSoundness_ldc_one_deltaCL): the conclusion of clSoundness_ldc_one with the blueprint's error δ_CL in place of the canonical-line one, at the sampling parameter clK m d (lidtError_le_deltaCL).