The pulling chain on the physical state #
MIPRE/Background/QLD/Chain.lean proves the index algebra of lem:qld-pauli-selfcons's chain and
its first displays, eq:qld-pulling-0 to eq:qld-pulling-3b, each of which concerns one
simultaneous pair measurement. From eq:qld-pulling-4 on the chain compares both players' pair
measurements, Alice's on (A'', (Ea, A')) and Bob's on (B'', (Eb, B')), on the physical state,
and runs over the four-index family chainQ, whose restriction to the coupled index set is the
chain's endpoint endOp. This file is that part:
eq:qld-pulling-4and-5(chainS3b_mulVec): resolving the identity on Bob's own pair brings its outcome into the chain, and each matched pair of Weyl projectors cuts Bob's point measurement down to the hatted one at the shifted outcome --- exactly;eq:qld-pulling-5to-9(sum_snorm_sq_chainP_le), costing item 2 oflem:qld-helper;eq:qld-pulling-9a(sum_poly_chainQ), free;eq:qld-pulling-10down to its Cauchy--Schwarz step (sum_snorm_sq_chainQ_disagree_le,sum_qform_bobTail_eq), finished bySimulPair.sum_uniform_qform_ne_leat the second cut;eq:qld-pulling-11(sum_snorm_sq_chainQ_agree_le), costing item 2 oflem:qld-helperat the second cut;eq:qld-pulling-12(sum_uniform_snorm_sq_chainQ_notCoupled_le), Schwartz--Zippel;- the endpoint's symmetry between the two players (
endOpMirror_eq,snorm_sub_endOpMirror) and the chain's conclusion (sum_xSqNorm_le_of_endOp).
Stated in a bipartite model #
Stated in a bipartite model (Phase 5 of planning/mipco-track.md). Everything here lives in the
physical model phys (Anc F m) F m d M Mi.K of a MirrorSimul: Alice's operators are matrices over
𝒜 on her physical registers, built from the first cut's pair measurement by compHom, and Bob's
are matrices over ℬ on his, built from the second cut's. The matrix route read the first cut's
estimates on the physical state through an explicit lift (physLift, physLiftEquiv) that
regrouped the registers and appended Bob's pair, and read Bob's on the second cut through
mirrorVec; here the first cut is a reading of the physical model's state model, so its estimates
need no lift (bornProb_physVec_aOp), and the second cut is the first cut of the physical model of
the exchanged players, so Bob's estimates are carried over by the exchange of the blocks of
registers (blockSwapIso, through phys_swap_bornProb; bornProb_physVec_bOp,
endOpMirror_eq). The EPR switching on Bob's own pair, which the matrix route did on the regrouped
vector, is the mirror identity of the physical state (physE_mirror_B), and many of Bob's objects
are Alice's objects of the second cut on the nose (bobWeyl, bobAnc, bobPt, bobHat).
A sandwich on the first cut, read physically #
A sandwich of a projection by an operator, on the first cut, is the squared state norm of half of it.
Two facts about models, used by instantiation #
An isomorphism of bipartite models keeps the state norm of a difference of two operators that its unitary intertwines with two operators of the other model.
The representation of a product, applied to a vector, is the composite. Stated for a state model, so that it is used by instantiation rather than by a rewrite that would compare large operators by unfolding them.
The chain's endpoint, 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 (swap_mem_coupledIdx).
The chain's endpoint, an element of the physical model's algebra: Alice's pair against Bob's, over the coupled index set.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The same endpoint reached from Bob's side: the endpoint of the mirror, an element of the algebra of the physical model of the exchanged players, which writes the two parties in the other order and reads the label off Bob's pair.
Equations
- Mi.endOpMirror W v a = Mi.mirror.endOp W v a
Instances For
Read with the parties' operators exchanged, the endpoint is the sum over the coupled index set with the label read off Bob's pair.
The endpoint is symmetric between the two parties, which is the whole reason
lem:qld-pauli-selfcons concludes: the exchange of the blocks of registers (blockSwapIso)
carries the endpoint reached from Bob's side to the endpoint reached from Alice's, so the two
exact Pauli measurements are close to each other rather than merely each close to something.
The same, on a state norm: an operator of Bob's against the endpoint reached from his side, on the physical model of the exchanged players, has the state norm it has against the endpoint on the physical model.
Each party's chain summand, on its physical registers #
Alice's chain summand, on her physical registers (A'', (Ea, A')): her pair measurement's
W-marginal at g on (Ea, A'), tensored with the Weyl spectral projector at h on A''.
Equations
- Mi.aliceChainOp W p = MIPRE.compHom (MIPRE.QLD.SimulPair.chainOp Mi.first W p)
Instances For
It is a projective family in the pair (g, h).
Bob's, on (B'', (Eb, B')) --- the mirror image, and the second cut's.
Equations
- Mi.bobChainOp W p = MIPRE.compHom (MIPRE.QLD.SimulPair.chainOp Mi.second W p)
Instances For
It is a projective family too.
Bob's Weyl projector, on the far half B'' of his own pair --- the outermost of his
physical registers. It is the second cut's ancB.
Equations
- Mi.bobWeyl W h = MIPRE.QLD.SimulPair.ancB Mi.second W h
Instances For
Bob's Weyl projectors are a projective measurement.
The chain's projective family on the physical cut: Alice's pair outcome and Weyl outcome
together, against Bob's Weyl outcome. Displays eq:qld-pulling-5 onward sum over this triple.
Equations
- Mi.chainP W t = (MIPRE.QLD.phys (MIPRE.QLD.Anc F m) F m d M Mi.K).πA (Mi.aliceChainOp W t.1) * (MIPRE.QLD.phys (MIPRE.QLD.Anc F m) F m d M Mi.K).πB (Mi.bobWeyl W t.2)
Instances For
It is projective, each party's family being so.
Alice's hatted point measurement, on her physical registers: on (A, A'), with Ea and
A'' inert.
Equations
- Mi.aliceHat W u c = MIPRE.QLD.SimulPair.hatA Mi.first W u c
Instances For
Bob's, on his: the second cut's.
Equations
- Mi.bobHat W u c = MIPRE.QLD.SimulPair.hatA Mi.second W u c
Instances For
The tail the chain carries at eq:qld-pulling-5: Alice's gap from her own point
measurement, against Bob's point measurement at the shifted outcome (g - g_h + g_h')(u).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The sandwich splits across the parties, each factor being local.
Summing the Weyl outcome out of Alice's summand leaves her pair measurement's marginal
alone, extended by the identity on A''.
So the Weyl index collapses out of her sandwich, the gap operator not depending on it.
The far party's factor of the chain's sandwich: a projector on (Eb, B') times a Weyl
outcome on B''.
Alice's sandwich is nonnegative, being a projection conjugated.
Display eq:qld-pulling-8: dropping the far party. Summed over Bob's Weyl outcome, his
factor is a projector times a projective measurement, so at most the identity.
The bridge from the physical state back to the first cut. An operator that is Alice's alone, and the identity on the far half of her pair, sees the state the first cut already describes: the two share their state model.
Displays eq:qld-pulling-5 to -8. The chain's terms on the physical cut, grouped by the
measurement outcome: projectivity turns each group into a sum of sandwiches, Bob's factor is a
projector times a Weyl outcome and so sums away, and Alice's Weyl outcome sums out of hers,
leaving the pair-measurement marginal against the complement of her own point measurement, on the
first cut.
Display eq:qld-pulling-9: the chain's step from eq:qld-pulling-5 to
eq:qld-pulling-7 costs item 2 of lem:qld-helper and nothing more.
The four-index family, and Bob's half of the chain for free #
eq:qld-pulling-9a left-multiplies by Bob's own pair measurement, which is the identity, and from
there to eq:qld-pulling-12 the chain runs over both parties' pairs. chainQ is that family,
and endOp --- the chain's endpoint --- is its restriction to the coupled index set. What the
mirror buys is the rest: Bob's derivation is Alice's, instantiated.
The chain's four-index family on the physical cut: each party's pair outcome and Weyl outcome together.
Equations
- Mi.chainQ W q = (MIPRE.QLD.phys (MIPRE.QLD.Anc F m) F m d M Mi.K).πA (Mi.aliceChainOp W q.1) * (MIPRE.QLD.phys (MIPRE.QLD.Anc F m) F m d M Mi.K).πB (Mi.bobChainOp W q.2)
Instances For
It is projective, each party's family being so.
endOp is that family, restricted to the coupled index set --- so display
eq:qld-pulling-12 and the displays leading to it speak about one and the same projective
measurement.
Display eq:qld-pulling-9a: left-multiplying by Bob's own pair measurement, which is the
identity, refines the chain's three-index family into the four-index one.
Bob's eq:qld-pulling-5 to -8, for free. The same lemma at the mirror: what it asks of
Bob there it asks of Alice here, and the physical model of the mirror has the physical model's
state model, with the two players' algebras exchanged. The paper's ``an entirely analogous
derivation'' for the second party is discharged this way, once for the whole chain.
eq:qld-pulling-10, down to its Cauchy--Schwarz step #
The second of the chain's two remaining estimates. It runs over the four-index family and over the pairs whose outcomes disagree at the sampled point, and the reduction below is everything before the swap: projectivity, one relaxation, and two completeness sums.
Bob's tail at eq:qld-pulling-9a, at an arbitrary outcome: his hatted point measurement,
and nothing on Alice.
Equations
- Mi.bobTail W u c = (MIPRE.QLD.phys (MIPRE.QLD.Anc F m) F m d M Mi.K).πB (Mi.bobHat W u c)
Instances For
The sandwich splits across the parties, Alice's factor untouched.
Bob's sandwiched pair-measurement marginal, on (Eb, B'): an operator of the second cut's
first player.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Bob's factor of that sandwich: his point measurement conjugating his pair measurement's marginal, tensored with his Weyl outcome.
The sandwich, fully split.
The tail at the chain's own outcome, the paper's (g - g_h + g_h')(u).
Equations
- Mi.chainV W u q = Mi.bobTail W u (MIPRE.QLD.chainQShift u q)
Instances For
The first two steps of eq:qld-pulling-10's justification. Projectivity turns the grouped
squared norm into a sum of sandwiches over the disagreeing pairs; each of those is one term of a
sum over all outcomes the pair's own value excludes, and the rest of that sum is nonnegative; and
then the constraint tying the outcome to the index may be dropped.
Display eq:qld-pulling-13a: Alice's family and Bob's Weyl outcome both sum to the
identity, so what is left of the bound carries neither.
eq:qld-pulling-11, and the second cut's bridge #
The last of the chain's estimates before Schwartz--Zippel. Everything here is Bob's, and everything Bob's is Alice's at the mirror.
The bridge from the physical state to the second cut. The mirror image of
bornProb_physVec_aOp: an operator that is Bob's alone, and the identity on the far half of his
pair, sees the state the second cut already describes, by the exchange of the blocks of
registers.
Bob's lift: an operator of his on (Eb, B'), extended by the identity on B'' and read on
the physical model. Both remaining displays sandwich the four-index family with one of these; only
which one differs.
Equations
- Mi.bobLift T = (MIPRE.QLD.phys (MIPRE.QLD.Anc F m) F m d M Mi.K).πB (MIPRE.compHom (Matrix.diagonal fun (x : MIPRE.QLD.Anc F m) => T))
Instances For
The sandwich splits across the parties, Alice's factor untouched.
Bob's factor of it: his operator conjugating his pair measurement's marginal, tensored with his Weyl outcome.
The sandwich, fully split.
Alice's family and Bob's Weyl outcome sum away, leaving a statement about the second cut
alone. This is the shape both eq:qld-pulling-10 and eq:qld-pulling-11 end at.
Display eq:qld-pulling-11: dropping Bob's point measurement from his side of the
chain's endpoint costs item 2 of lem:qld-helper, read on the second cut. The index set carries
the agreement constraint, which the bound simply drops --- every sandwich is nonnegative.
And its cost, which is item 2 of lem:qld-helper at the second cut --- available, with no
new proof, because the second cut is a simultaneous pair measurement in its own right.
eq:qld-pulling-12, Schwartz--Zippel, on the physical state #
The chain's four-index family has total weight one on the physical state.
Display eq:qld-pulling-12: 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 Schwartz--Zippel bounds that by md/q.
eq:qld-pulling-4 and -5 on the physical state #
The step that brings Bob's pair's outcome into the chain. Both halves of Bob's own pair are his in
the physical grouping, so the matched Weyl projectors are one operator of his, and the pair being
maximally entangled they act on the state as the projector on the far half alone
(physE_mirror_B).
The half of Bob's pair beside his own space, B': the second cut's ancA.
Equations
- Mi.bobAnc W h = MIPRE.QLD.SimulPair.ancA Mi.second W h
Instances For
Bob's matched Weyl projectors, on the two halves of his own pair.
Equations
- Mi.bobPairProj W h = Mi.bobAnc W h * Mi.bobWeyl W h
Instances For
The matched pair of projectors is the one on B' and Bob's Weyl outcome.
It is a single scalar matrix on Bob's registers, the projector on both halves of his pair.
Bob's two halves commute, living on different registers.
Bob's Weyl projector, as a scalar matrix on his registers: the projector on B'', the
identity on (Eb, B').
One matched pair of Weyl projectors acts as Bob's Weyl outcome alone. The pair the physical grouping gives him entirely is maximally entangled, so the projector on its near half is redundant beside the one on its far half.
Display eq:qld-pulling-4: Bob's matched Weyl projectors leave the physical state alone.
Each acts as the projector on the far half alone, and those sum to the identity.
Bob's point measurement, on his physical registers: the second cut's ptA, which is the
first cut's ptB.
Equations
- Mi.bobPt W u k = MIPRE.QLD.SimulPair.ptA Mi.second W u k
Instances For
Display eq:qld-pulling-5's algebra on Bob's register. The projector on the pair's near
half cuts the point measurement down to the hatted point measurement: the second cut's
ptA_mul_ancA.
The same against the matched pair, which is the form eq:qld-pulling-5 uses.
Bob's Weyl outcome and his hatted point measurement commute, living on different registers.
Displays eq:qld-pulling-4 and -5. Resolving the identity on Bob's pair brings its
outcome into the chain, and each matched pair cuts Bob's point measurement down to the hatted point
measurement at the shifted outcome. The step costs nothing: with the first cut's
chainS_three_mulVec it carries the chain's fourth term to its fifth on the physical state.
Closing the chain #
Both parties' derivations end at the endpoint, and what remains is arithmetic: the triangle
inequality for a family of deviations (StateModel.sum_snorm_sq_triangle). The two hypotheses
below are exactly the two chains --- Alice's eq:qld-pulling-0 through eq:qld-pulling-12, and
Bob's symmetric equivalent --- and nothing else stands between them and lem:qld-pauli-selfcons.
The chain's conclusion. Given that each party's exact Pauli measurement is close to the
endpoint, the two are close to each other, which is eq:qld-pulling-cons. The factor two is the
triangle inequality's, and the paper absorbs it into delta_S.