Legalizing a strategy for the Pauli basis test #
The paper's strategies answer each question in the format its type prescribes: a strategy's
measurement for a (Point, W) question has outcomes in F_q, for an axis-parallel line question
outcomes of degree at most d, and so on. The Lean strategies of MIPRE.QLD are more permissive:
one answer type Answer F m d serves every question, so a measurement may have an element on an
answer of the wrong format. The decider rejects such an answer before running any rule
(Question.fmtOk), so the mass on them is controlled by the failure probability --- but "controlled
by O(ε)" is not "zero", and one place needs zero. lem:qld-axis-degree asks that the expanded
axis-parallel line measurement be supported on polynomials of degree at most d, which the
paper takes from the format and which a dpoly answer to an axis question breaks.
This file makes the paper's convention available at no cost. legalize q a keeps an answer of the
right format and replaces any other by a fixed legal default (Question.defaultAns); the
legalized strategy legalizeStrat P relabels every measurement along it. Four things hold, and
they are all one needs to pass to the legalized strategy without loss of generality:
- it is projective when the original is (
isPVM_legalizeStrat); - it has no element on an answer of the wrong format (
legalizeStrat_mats_eq_zero, packaged asLegalSupport); - its value in the game is at least the original's (
povmValue_le_legalizeStrat): the decider rejected the answers that were changed, so no accepted pair is lost; - every reading the rules and the conclusions use is unchanged (
rdVal_legalize_pointand its siblings, lifted to the measurements bylegalizeStrat_map): the defaults read as0, which is what every reading already assigns to an ill-formatted answer. In particular the point-probe measurements and the hatted point measurements of the two strategies coincide (ptPOVM_legalizeStrat,hatPtPOVM_legalizeStrat), so a conclusion about the legalized strategy's point or Pauli measurements is a conclusion about the original's.
So every hypothesis of the appendix's chain holds for legalizeStrat PA, legalizeStrat PB when it
holds for PA, PB, and the extra property --- legal support --- is what
MIPRE/Background/QLD/PaddedLines.lean turns into the exact degree bound of lem:qld-axis-degree.
The campaign record had costed that lemma as "coarse-grain and pay the format-failure probability,
which changes the constants"; legalizing the strategy first costs nothing and changes no constant.
In a bipartite model #
Stated in a bipartite model (Phase 5 of planning/mipco-track.md). A strategy is a family of POVMs
P : Question F m → POVMIn (Answer F m d) R in a player's ordered ⋆-algebra R, legalizing is
the coarse-graining POVMIn.map along legalize q, and projectivity is IsPVMIn, which a
coarse-graining keeps (POVMIn.isPVMIn_map). The value comparison is the model's
(BipartiteModel.povmValue), by the same data processing on the Born distribution
(BipartiteModel.sum_weight_bornProb_map). The coarse (Pauli, W) measurement is unchanged by
legalizeStrat_map at the reading rdPauliVec (rdPauliVec_legalize_pauli,
MIPRE/Background/QLD/Soundness.lean). For a projective strategy S : M.ProjStrat (qldGame hm)
the legalized strategy is S.adapt (qldGame hm) id id legalize legalize, whose measurements are
legalizeStrat S.PA and legalizeStrat S.PB by definition.
The default legal answer, and the legalization of an answer #
A legal answer to each question, reading as 0 under every rule's reading.
Equations
- (MIPRE.QLD.Question.point W y).defaultAns = MIPRE.QLD.Answer.val 0
- (MIPRE.QLD.Question.aline W u₀ s).defaultAns = MIPRE.QLD.Answer.apoly 0
- (MIPRE.QLD.Question.dline W u₀ s v).defaultAns = MIPRE.QLD.Answer.dpoly 0
- (MIPRE.QLD.Question.pauli W).defaultAns = MIPRE.QLD.Answer.pauliAns 0
- (MIPRE.QLD.Question.pairB W ω).defaultAns = MIPRE.QLD.Answer.bit 0
- (MIPRE.QLD.Question.pair ω).defaultAns = MIPRE.QLD.Answer.bitPair 0
- (MIPRE.QLD.Question.con i ω).defaultAns = MIPRE.QLD.Answer.bitTriple 0
- (MIPRE.QLD.Question.var j ω).defaultAns = MIPRE.QLD.Answer.bit 0
Instances For
The readings are unchanged #
Each rule of fig:decider_pauli reads an answer through one of the maps of
MIPRE/Background/QLD/Win.lean, all of which send an answer of the wrong format to 0; the
defaults read as 0 too, so legalizing commutes with every reading at the question type it is
made for.
The legalized strategy #
A strategy is legally supported when it has no measurement element on an answer of the wrong format for the question. This is the paper's standing convention on strategies.
Equations
- MIPRE.QLD.LegalSupport P = ∀ (q : MIPRE.QLD.Question F m) (a : MIPRE.QLD.Answer F m d), q.fmtOk a = false → (P q).op a = 0
Instances For
The legalized strategy: each measurement relabelled along legalize.
Equations
- MIPRE.QLD.legalizeStrat P q = MIPRE.POVMIn.map (MIPRE.QLD.legalize q) (P q)
Instances For
An answer of the wrong format has no element in the legalized strategy.
A reading that legalization does not change reads the same measurement.
The point-probe measurements of the legalized strategy are the original's.
The point observables of the legalized strategy are the original's.
The hatted point measurements of the legalized strategy are the original's.
The value can only go up #
Legalizing both strategies does not decrease the value. The decider rejects an answer of the wrong format before any rule runs, so an accepted pair consists of legal answers, which legalization leaves alone; the accepted mass can only grow.
The failure probability of the legalized strategies is at most the original's: the form the appendix's hypotheses take.