The model chain, part 4: the padded strategy

The model counterpart of the strategy section of the repository's MIPRE/Background/LIDT/Padding.lean (blueprint lem:lidt-ldc-adapter; 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). A projective strategy S, in any bipartite model M : MIPRE.BipartiteModel 𝒞 𝒜 ℬ with the instance set of MIPRE.LIDT.Simul.SoundIn, for the seeded test with r codewords in m variables is played as one for the seeded test with one codeword in K + m variables (padded), through MIPRE.BipartiteModel.ProjStrat.adapt along the classical question map qmap and answer map rmap, for a seed offset σ.

• exists_padded_value: some offset makes the padded strategy fail at most 9 (K + 1) times as often as S, by the averaging lemma MIPRE.BipartiteModel.exists_one_sub_povmValue_adapt_le with the classical acceptance transfer clGame_D_rmap and push-forward bound sum_mu_qmap_le.
• pointPOVMA_padded, pointPOVMB_padded: the padded strategy's point measurements (CL.pointPOVMAIn, CL.pointPOVMBIn of Co/Chain/Reduction.lean) are the combined ones, combPOVM of Co/Chain/Extraction.lean applied to the tuple readings MIPRE.LIDT.Simul.tuplePOVMAIn, tuplePOVMBIn of S.

The parameter hd : 1 ≤ d is passed straight through: d is the same on both sides of the padding.

Reused by import. Everything before the strategy section of Padding.lean is classical: the decider on a sample, the geometry of lines and blocks, the question and answer maps, the acceptance transfer and the count. It is named through an explicit open MIPRE.LIDT.Simul (…) list: qmap, rmap, clGame_D_rmap, sum_mu_qmap_le, eval_linPoly_padB, and the model readings tuplePOVMAIn, tuplePOVMBIn of ModelSoundness.lean.

Not ported

padded, exists_padded_value, pointPOVMA_padded and pointPOVMB_padded are declared here under their names. Of the rest of Padding.lean:

• tuplePOVMA, tuplePOVMB: replaced by the existing model readings MIPRE.LIDT.Simul.tuplePOVMAIn, tuplePOVMBIn (ModelSoundness.lean).
• toPOVM_mergeAt: the matrix adapted strategy is built with ProjectiveMeasurement.mergeAt; the model's ProjStrat.adapt is the coarse-graining POVMIn.map by definition, so there is nothing to convert.
• the declarations of the sections Interface, Lines, Blocks, Maps, Answers, Transfer, Accept and Count: classical, imported.

New here

Nothing: every declaration here is the model form of a matrix one.

noncomputable def MIPRE.LIDT.Co.Chain.padded {𝒞 : 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] {K m d r : ℕ} [NeZero m] [NeZero (K + m)] (hm : m ∣ Fintype.card F) (hM : K + m ∣ Fintype.card F) (hr : r ≤ K) (S : M.ProjStrat (CL.clGame hm)) (σ : Fin (Fintype.card F / m)) : M.ProjStrat (CL.clGame hM)

The padded strategy for the seeded test with one codeword in K + m variables: S played through the question map qmap at the seed offset σ and the answer map rmap.

Equations

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

theorem MIPRE.LIDT.Co.Chain.exists_padded_value {𝒞 : 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] {K m d r : ℕ} [NeZero m] [NeZero (K + m)] (hm : m ∣ Fintype.card F) (hM : K + m ∣ Fintype.card F) (hr : r ≤ K) (hd : 1 ≤ d) (hK : 1 ≤ K) (S : M.ProjStrat (CL.clGame hm)) : ∃ (σ : Fin (Fintype.card F / m)), 1 - (padded hm hM hr S σ).value ≤ 9 * (↑K + 1) * (1 - S.value)

The padded adapter loses a factor 9 (K + 1) (blueprint lem:lidt-ldc-adapter): some seed offset makes the padded strategy fail at most 9 (K + 1) times as often as S.

theorem MIPRE.LIDT.Co.Chain.pointPOVMA_padded {𝒞 : 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] {K m d r : ℕ} [NeZero m] [NeZero (K + m)] (hm : m ∣ Fintype.card F) (hM : K + m ∣ Fintype.card F) (hr : r ≤ K) (hd : 1 ≤ d) (S : M.ProjStrat (CL.clGame hm)) (σ : Fin (Fintype.card F / m)) (u : Point F (K + m)) : CL.pointPOVMAIn (padded hm hM hr S σ) u = combPOVM hd (Simul.tuplePOVMAIn hm S) u

The padded strategy's point measurements are the combined ones: at the padded point (x, y), measure the original point measurement at y and answer ∑_{k<r} x_k b_k.

theorem MIPRE.LIDT.Co.Chain.pointPOVMB_padded {𝒞 : 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] {K m d r : ℕ} [NeZero m] [NeZero (K + m)] (hm : m ∣ Fintype.card F) (hM : K + m ∣ Fintype.card F) (hr : r ≤ K) (hd : 1 ≤ d) (S : M.ProjStrat (CL.clGame hm)) (σ : Fin (Fintype.card F / m)) (u : Point F (K + m)) : CL.pointPOVMBIn (padded hm hM hr S σ) u = combPOVM hd (Simul.tuplePOVMBIn hm S) u

The same for player B.