thm:qld: soundness of the Pauli basis test, in a bipartite model #
Phase 5 of planning/mipco-track.md. This file proves thm:qld for the projective strategies of
a bipartite model, in the form QLD.SoundIn ω M in which introspection takes it
(MIPRE/Background/QLD/ModelSoundness.lean), from two hypotheses on the model:
- the seeded low individual degree test is sound (
LIDT.Simul.SoundIn) in every extensionM.expand eof the model by a unit vector: stage 4 runs the seeded test on the padded strategy, which lives in such an extension (exists_globalPair); - the value model dominates the POVM strategies of every model obtained from such an extension by replacing its state with a unit vector: the ancilla model the theorem produces is one, the extension by the padding registers in the auxiliary state of the swap isometry lemma.
The headline is soundIn_of_lidt. Its two instances are the two models the project needs.
soundIn_tensor: in the tensor-product model of every state, withval*. An extension of a tensor-product model is the tensor-product model of the expanded vector (BipartiteModel.tensorExpandIso), in which the seeded test is sound (LIDT.Simul.soundIn_expand_tensor) and whichval*dominates (ValueModel.tensor_dominatesPOVM). The main theorem uses it, through introspection (approxSoundIn_tensor).soundCo_of_lidt: in the model of every commuting-operator strategy, withω_co, as soon as the seeded test is sound in the commuting-operator model (LIDT.Simul.SoundCo): an extension of a commuting-operator model is again one (LIDT.Simul.SoundCo.expand), andω_codominates every model in a unit state (ValueModel.commuting_dominatesPOVM). So the Pauli basis test adds no hypothesis toMIP^co = coRE(MIPRE.mipco_eq_core_of_lidt).
The route #
Inside the regime --- 48 m d ≤ q, where the chain runs, and qldHlt < 1, where the swap
isometry lemma applies --- three steps (exists_extraction_of_regime).
- Legalize (
legalStrat). Sending each answer of the wrong format to the question's default makes the strategy legally supported, which stage 4 needs. It keeps the strategy projective, does not raise its failure probability (one_sub_povmValue_legalizeStrat_le), and does not change the cube data a Pauli answer carries (rdPauliVec_legalize_pauli), which is all the conclusion is about (legalStrat_pauli_A,legalStrat_pauli_B). - Both cuts on one state (
exists_mirrorSimul):lem:qld-global-pvmat the strategy and at the strategy with the players exchanged, at one padding size. - The swap isometry (
MirrorSimul.swap_isometry): a local isometryswapPhi auxof the model into the register model over the padded extension in an auxiliary unit stateaux, with item 1 on the squared distance and item 2 for both players.
The extraction is that local isometry, with the padded extension in the state aux as its ancilla
model. Item 1 of thm:qld is the distance itself, at most √qldEta, and item 2 is the swap
lemma's: both are at most qldBound, and both are at most the trivial bound 4
(sum_stateSqNorm_alice_le_four, sum_stateSqNorm_bob_le_four), so at most qldErr
(le_qldErr). Outside the regime qldErr = 4, and the model itself with the EPR register adjoined
inertly is an extraction at the trivial bound (Extraction.trivial).
What changed from the matrix statement #
The matrix thm:qld this replaces (qld_soundness, removed in Phase 5) was about an arbitrary
POVM strategy on finite-dimensional spaces. It dilated the strategy to a projective one, ran the
chain on the dilation, and carried item 2 back down to the original POVM through the agreement
with τ^W on the other half of the pair, at a cost of 8 √η. Introspection, its one consumer,
applies it to projective strategies only, so the descent is gone, and with it the explicit
embedding of the original space and the register-first reading of the isometries. The error is
the same function qldErr, of the closed form a (md)^a (ε^b + q^{-b} + 2^{-bmd})
(exists_qldErr_le).
What differs from the paper's statement #
- The strategy is projective, in a bipartite model satisfying the two hypotheses, rather than a POVM strategy on a tensor product of finite-dimensional spaces.
- The regime is
48 m d ≤ q, not16 m d ≤ q:48is wherelem:qld-global-separateis formalized. The error absorbs the difference, as the paper's owna ≥ 64does. m ≥ 1is the instance[NeZero m], whichqldGameneeds to be stated at all.- The
(Pauli, W)measurement is read as cube data throughrdPauliVec, which reads an answer of the wrong format ash = 0. The paper assumes well-formatted answers; this is a relabelling of outcomes, not a restriction.
A local isometry between the two models with their states replaced: the same isometry and
homomorphisms, the states playing no part in a local isometry (toWithState replaces the target's
alone).
Equations
Instances For
Legalizing the strategy #
The legalized strategy: each measurement relabelled along legalize, which sends an
answer of the wrong format for the question to the question's default (legalizeStrat). A
coarse-graining of a projective strategy is projective.
Equations
Instances For
Legalizing does not raise the failure probability (one_sub_povmValue_legalizeStrat_le).
The first player's coarse (Pauli, W) measurement is unchanged by legalizing.
The second player's coarse (Pauli, W) measurement is unchanged by legalizing.
The trivial bound #
The first player's error of an extraction is at most 4, for a local isometry into the
register model of an ancilla model whose first homomorphism preserves the unit: the transported
Pauli measurement and the honest one are projective, on a unit vector
(BipartiteModel.sum_stateSqNorm_sub_le_four).
The second player's error of an extraction is at most 4.
The inert EPR register carries the state exactly to the state of the register model.
The trivial extraction, at the trivial bound 4: the model itself is the ancilla model,
and the local isometry adjoins the EPR register inertly, carrying the state exactly to the
register model's.
Equations
- MIPRE.QLD.Extraction.trivial S = { N := MIPRE.QLD.AncillaModel.of M ⋯, Φ := M.inert (MIPRE.Introspection.registerEPR (MIPRE.QLD.Anc F m)) ⋯, state_error := ⋯, alice_error := ⋯, bob_error := ⋯ }
Instances For
A value model dominating the extensions of a model in unit states dominates the model, in a unit state: the model reduces to its extension by one-point registers, which is itself in its own state.
Inside the regime #
The swap isometry preserves the first player's unit.
The swap isometry preserves the second player's unit.
thm:qld inside the regime. For a projective strategy failing with probability at most
ε, when 48 m d ≤ q and qldHlt < 1: the swap isometry of the legalized strategy
(MirrorSimul.swap_isometry, at the MirrorSimul of exists_mirrorSimul), with the extension by
the padding registers in the swap lemma's auxiliary state as the ancilla model, is an extraction at
error qldErr. Item 1 is the swap lemma's at the cost of a square root, and item 2 is the swap
lemma's on the nose, the legalized strategy having the strategy's Pauli measurements.
thm:qld #
thm:qld: the Pauli basis test is sound in a bipartite model (the paper's
thm:pauli-appendix), with the value model ω, when the seeded low individual degree test is
sound in every extension of the model by a unit vector and ω dominates every such extension in
every unit state. For every admissible (q, m, d) and every projective strategy in the model that
fails with probability at most ε, there are an ancilla model, which ω dominates, and a local
isometry of the model into it with the EPR register |EPR_q>^{⊗M} adjoined, such that
- the transported state is within
qldErr ε m d qof|EPR_q>^{⊗M} ⊗ |aux>, the state of the register model; and - for each basis
W ∈ {X, Z}, each player's own(Pauli, W)measurement, read as cube data and transported, is withinqldErr ε m d qof the honest Pauli basis measurementτ^W_hon that player's register, in summed squared state norm on that state.
qldErr is of the closed form a (md)^a (ε^b + q^{-b} + 2^{-bmd}) (exists_qldErr_le). Inside
the regime this is exists_extraction_of_regime; outside it, Extraction.trivial.
The tensor-product instance #
The Pauli basis test is sound in the tensor-product model of every state, with val*.
An extension of a tensor-product model by a unit vector is the tensor-product model of the
expanded vector (BipartiteModel.tensorExpandIso), in which the seeded test is sound
(LIDT.Simul.soundIn_expand_tensor), and which val* dominates in every unit state
(ValueModel.tensor_dominatesPOVM).
val* is approached in tensor-product models, where the test is sound
(soundIn_tensor): a tensor-product strategy near the supremum is a projective strategy of its
model, of the same value.
The commuting-operator instance #
The Pauli basis test is sound in the commuting-operator model as soon as the seeded low
individual degree test is: an extension of the model of a commuting-operator strategy by a unit
vector is the model of a commuting-operator strategy (LIDT.Simul.SoundCo.expand), and ω_co
dominates every model in a unit state (ValueModel.commuting_dominatesPOVM).