The pulling chain's index algebra, and its first displays #
lem:qld-pauli-selfcons is proved by a chain of eleven displays that ends at
sum_{g,h,g',h' : g - g_h = g' - g_h', (cd(g) - h) . u-tilde = a}
((S-hat^W_g)_{A A'} (x) (tau^W_h)_{A''}) . ((S-hat^W_g')_{B B'} (x) (tau^W_h')_{B''})
and concludes by the observation that this expression is symmetric between (g, h) and
(g', h'), so that the analogous derivation starting from Bob's exact Pauli measurement reaches
the same place, and the two are therefore close to each other. That observation is the whole reason
the lemma holds, and the reason it is not obvious is that the two conditions cutting out the index
set look asymmetric: the second mentions both pairs, but the first mentions only g and h.
The paper's sentence is that the conditions (cd(g) - h) . u-tilde = a and g - g_h = g' - g_h'
are together equivalent to (cd(g') - h') . u-tilde = a and g - g_h = g' - g_h'. This file is
that sentence, together with the rewriting of the exact Pauli measurement over the same index set
(eq:qld-pulling-2 and eq:qld-pulling-2b), the chain's Schwartz--Zippel step, and the chain's
first displays, eq:qld-pulling-0 to eq:qld-pulling-3b, each of which concerns one simultaneous
pair measurement. The displays that compare the two players' pair measurements on the physical
state, from eq:qld-pulling-4 on, are in MIPRE/Background/QLD/ChainPhysical.lean.
Subtraction is written as addition throughout, the field having characteristic two.
Stated in a bipartite model #
Stated in a bipartite model (Phase 5 of planning/mipco-track.md). The index algebra is unchanged.
The chain's summand chainOp is, as mTildeAnc is, a matrix over the first algebra of the model
of a SimulPair on the register Anc F m (register outer, smulKron). The displays
eq:qld-pulling-0 to -3b are stated for a pair measurement on the first cut of the physical state
(CutSimul N S K δ) and read in the physical model phys (Anc F m) F m d N K itself. The matrix
route ran them on a regrouping mVec of the first cut's state that gives A'' to Alice --- whose
model is the physical model --- and then carried them to the physical cut by an explicit lift
(physLift, which regrouped the registers and appended Bob's pair); the first cut and the physical
model share one state model, so here the chain's terms are elements of its algebra from the start,
and nothing is lifted. The helper's near-identity nearId is the first cut's agreement operator,
written physically by the reading lemmas cut1_πA, cut1_πB; the strategy's point measurements
are read with the registers inert (physInert); the EPR switching of eq:qld-pulling-3a is the
mirror identity of Alice's own pair in the physical state (physE_mirror_A); and the estimates
about one state are stated in a state model (sum_snorm_sq_sub_mul,
sum_snorm_sq_fiber_sandwich_subset_le).
The label a pair of outcomes carries #
The chain's label. cd(g) - h is the paper's difference of the pair outcome's cube data
and the Weyl outcome; the chain's index set asks its pairing with the probe to be the measurement
outcome.
Equations
- MIPRE.QLD.chainLabel g h = MIPRE.QLD.cubeData g + h
Instances For
The chain's coupling condition. The paper's g - g_h = g' - g_{h'}, with g_h the
low-degree encoding of h.
Equations
- MIPRE.QLD.ChainCoupled g g' h h' = (g.toMv + MIPRE.LowDegree.ldEnc h = g'.toMv + MIPRE.LowDegree.ldEnc h')
Instances For
Equations
- MIPRE.QLD.decidableChainCoupled g g' h h' = MIPRE.QLD.decidableChainCoupled._aux_1 g g' h h'
The coupling is symmetric on its face, which is half of the display's symmetry.
Coupled pairs carry the same label, which is the other half. Evaluating the coupling at a cube point reads off the two labels there, the encoding of a cube datum being that datum on the cube.
So the chain's last display is symmetric between the two pairs. Its index set is cut out by
the coupling, symmetric on its face, and by a pairing condition read off one pair --- and the two
readings agree, so it may be read off either. That is what lets the derivation starting from Bob's
exact Pauli measurement reach the same expression as Alice's, and hence what makes
lem:qld-pauli-selfcons conclude.
The index set, and the exact Pauli measurement written over it #
The chain's index set at the probe v and the outcome a: the pairs whose label pairs
with the probe to give a.
Equations
- MIPRE.QLD.chainIdx v a = {p : MIPRE.LIDT.LowIndDegPoly × MIPRE.QLD.Anc F m | MIPRE.Weyl.dotF (MIPRE.QLD.chainLabel p.1 p.2) v = a}
Instances For
In characteristic two the syndrome's condition and the label's are one condition.
A reindexing, and the label filters #
The chain's label filters are products, the label reading only the first pair. The reindexing
fact before them is not the chain's: it is about matrices, a regrouping of the matrix route
(SwapItemTwo.lean) still uses it, and it is kept here unchanged.
A reindexing carries mulVec the way it carries the quadratic form.
The chain's three- and four-index label filters are products, the label reading only the first pair.
The chain's endpoint index set, and its symmetry #
Display eq:qld-pulling-12 is a sum over pairs of index pairs, one per party, coupled by
g - g_h = g' - g_{h'} and cut out by the pairing condition on the first. Both parties' derivations
end there, and that is only because the expression does not in fact depend on which party's pair
the condition is read off.
The index set of eq:qld-pulling-12: coupled pairs, with the label read off the first.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The index set does not care which pair the label is read off. This is the paper's sentence:
the conditions (cd(g) - h) . u-tilde = a and g - g_h = g' - g_{h'} are together equivalent to
(cd(g') - h') . u-tilde = a and the same coupling.
The outcome the chain's four-index pair carries, the paper's (g - g_h + g_h')(u).
Equations
- MIPRE.QLD.chainQShift u q = q.1.1.eval u + MIPRE.Weyl.dotF q.1.2 (MIPRE.LowDegree.indVec u) + MIPRE.Weyl.dotF q.2.2 (MIPRE.LowDegree.indVec u)
Instances For
eq:qld-pulling-12, Schwartz--Zippel #
The chain's last display, and its only step that is not about operators: the constraint the chain carries is an equality of polynomial values at the sampled point, and passing to equality of the polynomials themselves discards only the tuples where distinct polynomials happen to agree there.
Schwartz--Zippel for the chain's coupling. Two index pairs that are not coupled carry
distinct polynomials, and distinct polynomials of individual degree at most d agree at a uniform
point with probability at most md/q. The encoding of a Weyl outcome is multilinear, so adding it
keeps the degree bound as long as d is at least one.
The chain's agreement condition, in the form Schwartz--Zippel reads. In characteristic two the shift the chain carries may be moved to the other side.
A version of Finset.filter bookkeeping the display needs: restricting a weighted sum to a
subset of the index is the same as zeroing the weights outside it.
Display eq:qld-pulling-12, as a bound on a weighted sum. The chain's constraint is an
equality of polynomial values at the sampled point; passing to equality of the polynomials
themselves discards only the tuples where distinct polynomials happen to agree there, and those
carry at most md/q of the weight.
Estimates about one state #
Two facts about a single state that the chain's displays share, stated in a state model
(MIPRE/Foundations/StateModel.lean): right-multiplying a projective measurement costs exactly the
operator's deviation from the identity, and the chain's terms, grouped by the measurement outcome,
have as summed squared norm a sum of sandwiches.
Right-multiplying a projective measurement costs exactly the operator's deviation from the
identity. Summed over the outcomes there is no cross term, so no factor of the outcome count
appears --- which is what makes display eq:qld-pulling-1 free rather than lossy.
The outer shape both remaining displays share. Each is a bound on the summed squared norm
of the chain's terms, grouped by the measurement outcome. Projectivity turns each group into a sum
of sandwiches (snorm_sq_sum_proj_sandwich), the groups are the fibres of the outcome map, so the
double sum is the single one over the index --- and what is left to bound is a sum of sandwiches
with no outcome in it. The index may be a subset, which is what eq:qld-pulling-10 needs: it sums
over the pairs whose outcomes disagree.
The case the first of the two displays uses, where the whole index is summed over.
Two projective families of the two players, and fact:add-a-proj #
A product of projective measurements of the two players is projective, indexed by the pairs of outcomes: the two families commute.
A second-player sandwich of a product of the two players' operators: the first player's factor is untouched.
Dropping the far party's sub-identity factor. Each of the chain's sandwiches carries, on
the far party, a projector times a Weyl outcome; summed over the outcome those are at most the
identity, so the whole sum is bounded by the near party's sandwiches alone. This is
fact:add-a-proj in the form eq:qld-pulling-7 and eq:qld-pulling-11 consume it, for a second
player whose algebra is the matrices over R on the register.
The same, for a second player whose registers are a pair: the second player's algebra is
the matrices over R on anc × α, the far party's factor a projection of α times a projective
measurement of anc flattened onto the pair (compHom). The flattening is monotone, being a
⋆-homomorphism of star-ordered rings.
The physical registers' operators #
A player's physical registers are (A'', (Ea, A')) (PhysReg). Three kinds of operators of them
occur in the chain: an operator X of (Ea, A') with the far half A'' inert,
compHom (diagonal fun _ => X) --- the first player's operators of the first cut, read physically
(cut1_πA); a matrix Q of scalars on the far half, compHom (smulKron 1 Q); and their products,
compHom (smulKron X Q). These are the identities between them, over any ⋆-algebra.
X ⊗ 1 is the block-diagonal matrix of X.
An operator of the inner register, with the outer one inert, is its right lift, a unital
⋆-homomorphism.
The identity minus an operator of the inner register is one of the inner register.
The adjoint of an operator of the inner register is one of the inner register.
Operators of the inner register multiply as they do there.
An element on the diagonal of the pair of registers is one on the diagonal of each.
An operator of the near half, read on the three registers: X ⊗ Q on the innermost
register α, with the two outer ones inert.
The Weyl spectral projectors, and the hatted point measurement against one #
A Weyl family's spectral projectors are a projective measurement. The three facts are in Foundations one by one; this is them bundled.
The point measurement read off a strategy is projective when the strategy's own is: it is a coarse-graining of it along the answer's value.
A syndrome projector meets a single spectral projector in that projector or in nothing. The syndrome is the fibre of the spectral family over the pairing, so the product keeps the one outcome exactly when it lies in the fibre.
Display eq:qld-pulling-3b. The chain's factor (M^{Point}_r)_A (x) (tau_h)_{A'} is the
hatted point measurement itself, cut down by the Weyl outcome: M-hat^{u}_{c} times the projector
at h keeps exactly the point outcome c - g_h(u), the syndrome factor selecting the one term of
the convolution whose shift matches h. Over any ⋆-algebra, with the register outer.
A single Weyl projector across the expanded state #
A single Weyl spectral projector transports across the expanded state, exactly. The
syndrome version is stateVec_hatVec_syn; the chain's display eq:qld-pulling-3a moves one
projector, not a fibre of them.
The same, as the vanishing of a cross-party deviation.
The chain's summand, on one pair measurement #
The chain's summand on one party: the pair measurement's W-marginal at g, tensored with
the Weyl spectral projector at h on the register.
Equations
- P.chainOp W p = MIPRE.smulKron ((MIPRE.QLD.polyMarg P.SA W).op p.1) (MIPRE.Weyl.proj (MIPRE.QLD.weylOf W) p.2)
Instances For
Displays eq:qld-pulling-2 and eq:qld-pulling-2b: the exact Pauli measurement, indexed the
chain's way. eq:tilde_M sums over the pair measurement's outcomes g with a syndrome projector
attached; the chain sums over pairs (g, h) cut out by the pairing condition. The two are the same
sum, because the syndrome projector is by definition the fibre of the spectral family over that
pairing, and in characteristic two the shift the definition carries is the sum the chain's label is
written with.
The chain's summands are a projective measurement in the pair (g, h): a marginal of a
projective pair measurement, tensored with a Weyl spectral projector.
Summing the pair outcome out of the summand leaves the Weyl projector alone, the pair
measurement's outcomes being complete. This is what eq:qld-pulling-9a inserts.
The exact Pauli measurement, expanded over the pair outcomes.
Multiplying it by one of the near-identity's terms. The pair measurement's outcomes are
orthogonal, so only the matching one survives, and syn_mul_syn collapses the two syndrome
projectors onto the Weyl outcomes satisfying both conditions.
The chain's summand splits into the pair measurement's marginal and the Weyl outcome.
The outcome the chain's index pair carries, the paper's (g - g_h)(u): the pair outcome's
value at the sampled point, shifted by the Weyl outcome's own encoding there.
Equations
- MIPRE.QLD.SimulPair.chainShift u p = p.1.eval u + MIPRE.Weyl.dotF p.2 (MIPRE.LowDegree.indVec u)
Instances For
The Weyl projector across the pair measurement's model #
Display eq:qld-pulling-3a: the Weyl projector transports across the model of the pair
measurement. The two halves of the register model's pair are maximally entangled and the
projectors are symmetric (stateVec_hatVec_proj), and the embedding ι intertwines each player's
operators and carries the state to the state.
Display eq:qld-pulling-4: the matched pairs of Weyl projectors leave the state alone. By
the transport each matched pair acts as the projector on one side alone, and those sum to the
identity.
eq:qld-pulling-13, the chain's only Cauchy--Schwarz #
The swap that completes eq:qld-pulling-10. It is stated on a SimulPair, in the model that
pair's measurements live in, because that is where both placements of the point measurement are
local: the one that sandwiches is the first party's own, the one that replaces it is the second
party's. The mirror then makes it Bob's.
Display eq:qld-pulling-13: moving the sandwiching point measurement from the party that
carries the pair measurement to the other one. The cost is twice the square root of the two
placements' summed squared state distance, and no more: the pair measurement's outcomes are
orthogonal, so summing the deviation over them leaves one copy rather than one per outcome.
The swapped side, read as a Born probability. Summing the other party's point measurement over the outcomes its own value excludes leaves the complement of that value.
Display eq:qld-pulling-10, complete: the whole cost of moving the point measurement
across and then dropping it is the helper's own delta_S plus twice the square root of the point
measurements' cross-party deviation. The average over the sampled point goes inside the square
root by Cauchy--Schwarz against the constant one.
The chain's first displays, on the physical model #
Displays eq:qld-pulling-0 to -3b concern one simultaneous pair measurement on the first cut of
the physical state, and run in the physical model, which has the first cut's state: the exact Pauli
measurement there is the first player's compHom (P.mTildeAnc …), on (A'', (Ea, A')).
The helper's near-identity, an element of the physical model's algebra: the agreement
operator of the first cut, of Alice's pair-measurement marginals against Bob's expanded point
measurements carried along ι₁, which is what lem:qld-helper bounds. The first cut and the
physical model share their state model, so no regrouping is needed to read it physically.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Display eq:qld-pulling-1, as an identity. Inserting the near-identity costs exactly its
own deficit on the state, with no loss at all.
And its cost, which is item 1 of lem:qld-helper.
Alice's copy of the strategy's point measurement, on her physical registers, which it does not see.
Equations
- MIPRE.QLD.SimulPair.ptA _P W u k = (MIPRE.QLD.physInert (MIPRE.QLD.Anc F m) F m d N K).ΦA ((MIPRE.QLD.ptAtPOVM S.PA W u).op k)
Instances For
Bob's, on his.
Equations
- MIPRE.QLD.SimulPair.ptB _P W u k = (MIPRE.QLD.physInert (MIPRE.QLD.Anc F m) F m d N K).ΦB ((MIPRE.QLD.ptAtPOVM S.PB W u).op k)
Instances For
The near-identity, expanded: on the physical model it is a sum of products of Alice's pair
measurement and the syndrome on A'' against Bob's point measurement.
Display eq:qld-pulling-2b at the interface. Expanding both factors, the pair
measurement's orthogonality picks out one outcome, syn_mul_syn fuses the two syndrome projectors,
and the sum over Bob's point outcome collapses --- for each Weyl outcome h exactly one of them
survives, namely (g - g_h)(u). What is left is a sum over the chain's own index set.
Display eq:qld-pulling-3. Inserting Alice's copy of the point measurement beside each
term of the chain costs the point measurements' own cross-consistency and nothing else. Two things
hold the bound down: the chain's terms are a projective family in the pair (g, h), so the
outcomes do not interfere (StateModel.snorm_sq_sum_orthogonal') and the fibres of the outcome map
are seen only once (sum_snorm_sq_proj_comp_le, inside sum_snorm_sq_insert_le).
The chain's first four terms, and the three steps between them #
chainS names the terms displays eq:qld-pulling-0 to -3 run through, as elements of the
physical model's algebra, and the three lemmas below are those displays read as bounds on
consecutive deviations --- which is the form StateModel.sum_snorm_sq_chain_le consumes.
The chain's first four terms, on the physical model. eq:qld-pulling-0 through
eq:qld-pulling-3: the exact Pauli measurement, that measurement times the near-identity, the
same written over the chain's index, and the same with Alice's copy of the point measurement
inserted.
Equations
- One or more equations did not get rendered due to their size.
- MIPRE.QLD.SimulPair.chainS P W v u 0 = fun (a : F) => (MIPRE.QLD.phys (MIPRE.QLD.Anc F m) F m d N K).πA (MIPRE.compHom (MIPRE.QLD.SimulPair.mTildeAnc P W v a))
Instances For
Displays eq:qld-pulling-2 and -2b say the second and third terms are one.
And the third and fourth differ by what eq:qld-pulling-3 bounds.
Step 0 to 1 is eq:qld-pulling-1, at item 1 of lem:qld-helper's own constant.
Step 1 to 2 is free, being displays eq:qld-pulling-2 and -2b, which are identities.
Step 2 to 3 is eq:qld-pulling-3, the insertion.
Displays eq:qld-pulling-3a and -3b: Alice's own pair #
The physical model gives Alice both halves of her pair (A'', A'); on the physical state a Weyl
projector on the near half acts as the same projector on the far half (physE_mirror_A), and once
it is there Alice's copy of the point measurement and her hatted point measurement agree.
Alice's Weyl spectral projector on the near half A' of her own pair.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The same projector on the far half A'', which the physical model also gives her.
Equations
- MIPRE.QLD.SimulPair.ancB _P W h = MIPRE.compHom (MIPRE.smulKron 1 (MIPRE.Weyl.proj (MIPRE.QLD.weylOf W) h))
Instances For
Display eq:qld-pulling-3a on the physical state: the two halves of Alice's pair are
maximally entangled and the projectors are symmetric.
Alice's hatted point measurement, on her physical registers: on (A, A'), with the padding
and the far half inert.
Equations
- MIPRE.QLD.SimulPair.hatA _P W u c = MIPRE.compHom (Matrix.diagonal fun (x : MIPRE.QLD.Anc F m) => (MIPRE.QLD.ι₁ (MIPRE.QLD.Anc F m) F m d N K).ΦA (MIPRE.QLD.hatMats S.PA W u c))
Instances For
Display eq:qld-pulling-3b on Alice's physical registers.
Displays eq:qld-pulling-3a and -3b together. Inserting Alice's own near half beside the
far half the chain already carries changes nothing on the state, and once it is there the point
measurement and the hatted point measurement agree.
Display eq:qld-pulling-3b's term: the chain's third term with Alice's own hatted point
measurement in place of her copy of the point measurement.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Displays eq:qld-pulling-3a and -3b, on the chain's third term.