A content, and a product of two independent line-point pairs #
lem:qld-pairs-of-lines is proved on the Pauli basis test's own question distribution: one
Content, carrying both sides' points but a single seed and a single raw direction, so the
X line and the Z line it presents are not independent. lem:qld-padded-lines needs the same
conclusion on a product of two independent line-point laws, which is what lem:qld-sublines
delivers.
The transfer is available, and the reason is worth stating before the machinery: no hypothesis of the pasting lemma involves both lines. Each marginal consistency involves one line and the two points; the fine self-consistency and the collision term involve one line only. So the only laws that have to agree are
- one side's line-point data on its own,
- one side's line-point data together with the other side's point,
- the two points.
and each of those has the same law under a content as under a product, because a content's two
points and its seed and raw direction are independent and uniform. This file says that three times,
and each proof is one line on top of MIPRE.avg_comp_equiv_fst: exhibit the splitting of each
sample space that isolates the part the quantity depends on, and the marginals match.
What the file does not claim is that the two laws agree on anything involving both lines --- they do not, and that is the content of the paper's restriction to product distributions.
In a bipartite model #
Stated in a bipartite model (Phase 5 of planning/mipco-track.md). The laws and splittings are
unchanged; the operator statements read the strategies as families of projective measurements
PA, PB in the players' algebras and the expanded state as the model M.reg (Anc F m), as
MIPRE/Background/QLD/Lines.lean does. The joint point measurement indexed by the pair of points is
combined_points_pts_dilated, built with BipartiteModel.exists_projective_joint on the model of
the dilation (extHat); combined_points_pts is its agreement form in the expanded model, and the
product form of the pairs-of-lines lemma from the game (pairs_of_lines_prod_of_items) is an
agreement bound of the sandwich there, the dilation being kept inside its proof. Every constant is
the matrix statement's.
Reading a content as line-point data, and back #
The Z-side line-point data a content carries: the same seed and raw direction, with the
Z point. That sharing is exactly why a content is not a product of two independent line-point
pairs.
Instances For
A content assembled from X-side line-point data and a Z point. The probe registers are
irrelevant to every line quantity, so they are set to zero.
Instances For
A content assembled from Z-side line-point data and an X point.
Instances For
The three splittings, on each of the two sample spaces #
Each pair of equivalences isolates the same part of the sample --- the part a hypothesis of the
pasting lemma can depend on --- on the content side and on the product side. avg_comp_equiv_fst
then says both uniform averages equal the uniform average over that part.
A pair of line-point data splits as (the X one, the Z one's point) and the Z one's line.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The mirror of contentSplitX.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The mirror of pairSplitX.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A content splits as its two points and everything else.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A pair of line-point data splits as its two points and the two lines.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The three laws that agree #
One side's data together with the other side's point has the same law under a content as
under a product. The X version: every marginal consistency and every collision term of the
pasting lemma at the X line is a quantity of this shape.
The Z version.
The two points have the same law under a content as under a product. This is what carries the combined point measurement's consistency across.
One side's data on its own, as the special case that ignores the other side's point.
The change of variables, at the product #
MIPRE.QLD.sum_shift_gen (in Lines.lean, where the content instance of it lives) needs only a
finite sample space, a shift action on it, and a direction the shift does not move. So it applies to a
pair of line-point data with the shift acting on the X side only, which is what the product form
of the pasting lemma's collision term needs; all that is required here is the action and its three
properties.
The shift on a pair, and what it leaves alone #
The shift on a pair of line-point data: move the X side's point, leave the Z side alone.
Instances For
The X line's direction, read off a pair through the content the X side presents.
Equations
- MIPRE.QLD.pairDirX PX p = PX.dir (MIPRE.QLD.ofLPX p.1 p.2.pt)
Instances For
Shifting the pair shifts the X side's content, which is what the LinePres invariances are
stated about.
The same shift moves the Z side's content only in its other point, which the _other
invariances say changes nothing on the Z line.
The change of variables at the product: averaging over pairs is averaging over
(pair, shift), the shift moving the X point along the X line.
lem:qld-pairs-of-lines, at a product of two independent line-point pairs #
pairs_of_lines_gen asks for a content per side and a shift both sides see as a shift of the X
point. A pair of line-point data supplies exactly that: each side's content is its own point, seed
and raw direction, with the other side's point filled in as the content's other point --- which no
quantity of that side's line depends on --- and pairShift moves the X point. So the product form
is an instance, with nothing to prove beyond the two rfls below.
The X-side content a pair of line-point data presents: the X side's own line-point data, with
the Z side's point as the content's other point.
Equations
- MIPRE.QLD.pairCX p = MIPRE.QLD.ofLPX p.1 p.2.pt
Instances For
The Z-side content. Its seed and raw direction are the Z side's own, independent of the X
side's --- which is the whole difference from a single content.
Equations
- MIPRE.QLD.pairCZ p = MIPRE.QLD.ofLPZ p.2 p.1.pt
Instances For
The combined point measurement, indexed by the pair of points #
lem:qld-combined-points is stated over the Pauli basis test's own contents, and the measurement it
produces is indexed by them. Every quantity it is bounded against depends on the content only through
its two points, so the same construction runs at the pair of points and gives a measurement that
any sample space carrying two points can use --- in particular a pair of line-point data, where the
content-indexed version would have to be fed contents with zeroed probes and the averages would not
match.
A quantity of the two points has the same law under a content as under a uniform pair of points.
lem:qld-combined-points, the dilated measurement, indexed by the pair of points. Verbatim
combined_points_dilated with the content replaced by the two points it contributes, which is all
four inputs of the joint-measurement construction (BipartiteModel.exists_projective_joint) see:
for each pair of points a projective measurement on the model of the dilation (extHat),
compressing to the sandwich at |inl (0, 0)⟩, self-consistent and consistent with both ordered
products, at the constants of the content-indexed statement.
lem:qld-combined-points, indexed by the pair of points, as agreement bounds of the
sandwiches in the expanded model: combined_points with the content replaced by the two points it
contributes, every quantity there depending on the content only through them
(avg_content_eq_pts). The dilated measurement indexed by the pair of points is
combined_points_pts_dilated.
lem:qld-pairs-of-lines, on a product of two independent line-point laws. The instance of
pairs_of_lines_gen at kX = pairCX, kZ = pairCZ, sh = pairShift: this is the form
lem:qld-padded-lines needs, where the X line and the Z line are drawn independently.
The line data of one side factors through that side's line-point data #
Every quantity of the X line --- the measurement, the parameter, the collision probability ---
reads the content only through its X point, its seed and its raw direction, which is exactly
Content.lpX. Saying so once is what lets a content-level bound be read as a bound on the product,
through avg_content_eq_pair_X: the two laws agree on quantities of (lpX, uZ), and this is the
proof that the quantities in question are of that shape.
The hypothesis is the three data a LinePres carries. Both line presentations satisfy it by rfl:
dirOf and ddirOf read the seed and the raw direction, the base point is the canonical
representative of the side's own point, and Content.question at a line type reads nothing else.
PX reads the content only through its X line-point data.
Equations
- One or more equations did not get rendered due to their size.
Instances For
PZ reads the content only through its Z line-point data.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The four bounds, read on the product #
Each is the content-level bound with avg_content_eq_pair_X or avg_content_eq_pair_Z applied and
the factoring lemmas used to put the summand in the shape those identities need.
The fine self-consistency of the X line measurement involves no point at all, so the transfer
is the point-free form of the same identity.
The collision probability reads only the direction, so it transfers the same way.
lem:qld-pairs-of-lines on the product, from the game #
The product form of the pasting conclusion, with only game-level hypotheses on the X and Z line
presentations. Every input is the content-level one of pairs_of_lines_of_items, read on the product
through the four transfer identities above; the combined point measurement is the dilated one
indexed by the pair of points (combined_points_pts_dilated), which is what makes the reading
possible. As in pairs_of_lines_of_items, the dilation stays inside the proof: the conclusion is an
agreement bound of the sandwich in the expanded model.