The self-consistency of the exact Pauli observables (lem:qld-pauli-selfcons) #
MIPRE/Background/QLD/ChainAssembly.lean takes Alice's exact Pauli measurement at an arbitrary
probe to the endpoint of the pulling chain, on the physical state. This file closes the lemma:
Bob's exact Pauli measurement reaches the same endpoint (the same chain at the mirror, carried back
by the exchange of the blocks of registers), so the two measurements agree across the physical cut
(sum_selfConsGap_le); and the observables, the signed sums of the measurements' elements, agree
at a factor two (snorm_sq_wTilde_le), the family being coarse-grained along the character first.
Stated in a bipartite model #
Stated in a bipartite model (Phase 5 of planning/mipco-track.md). The two exact Pauli
observables are operators of the two players of the physical model phys (Anc F m) F m d M Mi.K,
the first cut's and the second cut's wTildeAt flattened onto the players' physical registers by
compHom. The matrix route moved Bob's half of the chain to the physical state through the
exchange of the parties on the vector (swapVec, snorm_swapVec_aOp_sub_kron_sum); here the
mirror's physical model is the physical model of the exchanged players, and Bob's half is carried
over by the exchange of the blocks of registers (MirrorSimul.snorm_sub_endOpMirror, through
blockSwapIso). The passage from the measurements to the observables is the state-model form of
lem:qld-povm-to-obs (StateModel.snorm_sq_obs_sub_le). The constants are the matrix ones.
Regrouping a weighted sum by the fibres of a relabelling.
Alice's exact Pauli observable, the signed sum of her measurement's elements, on her
physical registers (A'', (Ea, A')).
Equations
- Mi.aliceWTilde W e v = MIPRE.compHom (MIPRE.QLD.SimulPair.wTildeAt Mi.first W e v)
Instances For
Bob's, on his, (B'', (Eb, B')): the second cut's.
Equations
- Mi.bobWTilde W e v = MIPRE.compHom (MIPRE.QLD.SimulPair.wTildeAt Mi.second W e v)
Instances For
At the mirror, Alice's exact Pauli observable is Bob's.
Each observable is the signed sum of its measurement's elements, flattened onto the physical registers.
Display eq:qld-pulling-cons for Alice, with the average over the sampled point dropped:
neither side depends on it.
The same at the mirror, read on the physical state. The mirror of a MirrorSimul is a
MirrorSimul, its physical model is the physical model of the exchanged players, and its endpoint
is this one read from the other side: the exchange of the blocks of registers carries the one to
the other (snorm_sub_endOpMirror).
Display eq:qld-pulling-cons for Bob.
Lemma lem:qld-pauli-selfcons at the level of the two exact Pauli measurements: they
agree on the physical state, at four times what each costs to reach the chain's endpoint.
Lemma lem:qld-pauli-selfcons: the two parties' exact Pauli observables agree.
The passage from the measurements to the observable is the paper's, and it is not
Lemma lem:qld-povm-to-obs applied to the whole outcome set --- that would cost a factor the
size of the field. The family is coarse-grained first, along the character the observable reads
(sum_xSqNorm_fibre_le, which is free for projective families), and only the resulting
two-outcome family is turned into an observable. The factor is therefore two.