The padded line measurement's consistency #
Blueprint lem:qld-padded-lines, the analytic half. Combine.lean built the measurement; this file
proves it consistent with the padded point measurement on the padded line-point law.
The paper chains three Cauchy--Schwarz claims here. They are not needed for this construction, and
reports/padded-lines-product-law.md says why: the joint law of the two sublines-with-points is
exactly a product of the two marginals at a fixed padded seed, so the product form of the
pairs-of-lines lemma applies directly. What is left is a single coarse-graining step, and that is
what this file adds.
- Coarse-graining both sides the same way can only increase agreement.
sum_bornProb_le_fibre, for bare nonnegative families rather thanPOVMInstructures --- which is what the pasted line measurement is. - The two coarse-grained families.
ptCombis the combined point measurement read along the linear form(a, b), the paper'sQ-hat^{x,z,alpha,beta};lineCombis the pasted line measurement coarse-grained by the combining map.lineComb_eq_sum_pasteFibidentifies the second as a coarse-graining of the first coarse-graining, which is what makes them comparable. - The bound.
padded_lines_consistency: the two disagree by at mostm^2 * delta_Pon the padded line-point law, at every padded seed and line type.
The m^2 and the functional form are discussed in the report: it is poly(m) * poly(eps, md/q)
rather than the m * poly(eps, md/q) the blueprint statement advertises, which
lem:qld-simultaneous's a(md)^a prefactor absorbs.
In a bipartite model #
Stated in a bipartite model (Phase 5 of planning/mipco-track.md). The pasted line measurement and
its coarse-grainings (pasteFib, lineComb) are families of elements of
Matrix (Anc F m) (Anc F m) R over a player's ordered โ-algebra, and the consistency bound is an
agreement bound in the expanded model M.reg (Anc F m): the combined point measurement is the
first player's sandwich M-hat^Z_b M-hat^X_a M-hat^Z_b itself, read along (alpha, beta)
(ptComb), not a dilation of it. That is the form pairs_of_lines_prod_of_items now returns, and
it is also what the padded strategy measures, so no compression is needed downstream. The
exchanged player is the same statement for M.swap, read back through hatVec_swapVec_xSqNorm
and hatVec_swapVec_bornProb. Positivity is the model's order: the two coarse-graining lemmas
take nonnegative families, and the name posSemidef_pasteFib is kept for a nonnegativity
statement.
Coarse-graining a Born sum #
Coarse-graining both sides the same way can only increase agreement. The POVMIn version
is BipartiteModel.sum_bornProb_le_map; here the families are bare nonnegative families, which is
the shape the pasted line measurement comes in.
A Born sum on the diagonal of two POVMs is at most one.
The two coarse-grained families #
The pasted line measurement's own outcome map: each side's polynomial read at the parameter of its own subline.
Instances For
The combined point measurement along the linear form (a, b): the paper's
Q-hat^{x,z,alpha,beta}, as the coarse-graining of a family indexed by pairs, in any additive
monoid.
Instances For
The pasted line measurement coarse-grained by that map --- the family the product form of
lem:qld-pairs-of-lines bounds.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Each element of the coarse-grained pasted family is nonnegative.
The pasted line measurement coarse-grained by the combining map at (a, b). Averaged over
the fresh randomness this is padLineMats read at the sampled point; see
sum_filter_padLineMats.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The line side is a coarse-graining of the fibre family, along the same linear form. This is
what lets the two be compared by sum_bornProb_le_fibre.
The axis-parallel degree bound #
The degree computation of lem:qld-axis-degree: on an axis-parallel line the expansion adds a
polynomial of degree at most one, because the restriction of a multilinear polynomial to
u_0 + t e_j is affine in t (natDegree_lineRestrict_single_le), so an outcome built from a legal
axis answer has degree at most d as soon as d >= 1.
What this does not give is the support claim of lem:qld-axis-degree. The strategy's line
measurement is indexed by all answers, and a dpoly answer to an axis-parallel question --- which
the decider rejects, but for which the measurement still has an element --- produces an outcome of
degree up to md. Turning the computation below into the lemma means modifying the measurement to
send those answers to a default outcome and paying the format-failure probability, which is not done
here; that is why lem:qld-padded-lines states its degree-d clause conditionally on
lem:qld-axis-degree.
A line outcome read off an answer that is not a diagonal-line answer has degree at most d.
The expansion adds degree at most one on an axis-parallel line.
The degree computation of lem:qld-axis-degree: a legal axis answer convolved with the
expansion's line outcome has degree at most d, for d >= 1.
The support half of lem:qld-axis-degree #
The degree computation above says what an outcome built from a legal axis answer looks like. The
support claim is that the expanded axis-line measurement has no element anywhere else, and that is
false for an arbitrary strategy: a dpoly answer to an axis question is rejected by the decider but
still has a measurement element, whose outcome has degree up to m d. For a strategy with
LegalSupport --- which legalizeStrat provides at no cost --- it is true and exact: every element
of the strategy's factor sits on a legal apoly answer, of degree at most d, and every element of
the ancilla's factor sits on a restriction of the multilinear encoding, of degree at most 1. The
padded line measurement inherits it through degLE_padCombine_aline.
The strategy's axis-line reading of a legally supported strategy is supported on degree at
most d.
The support half of lem:qld-axis-degree, at the expanded measurement: for d โฅ 1 and a
legally supported strategy, the expanded axis-parallel line measurement has no element off the
polynomials of degree at most d.
The same, for the axis-parallel presentation's line measurement.
The support half of lem:qld-axis-degree, at the padded line measurement: on an
axis-parallel padded line, the padded line measurement of a legally supported strategy has no
element off the polynomials of degree at most d. This is what makes its outcome a legal answer to
an axis-parallel line question of the seeded test at (q, 4m, d, 1).
The consistency bound #
lem:qld-padded-lines, the consistency bound. On the padded line-point law, at every padded
seed and line type, the first player's combined point measurement --- the sandwich of the expanded
point measurements, read along (alpha, beta) at the sampled point --- agrees in the expanded
model M.reg (Anc F m) with the second player's pasted line measurement coarse-grained by the
combining map, up to m^2 * delta_P.
The proof is the coarse-graining step and then the two domination lemmas: agreement only increases
under a common coarse-graining, the padded law is at most m^2 times the product law
(avgSub_le_mul_avgAll), and (alpha, beta) is uniform and independent of both sublines
(avgSubAB_le_of_forall). The paper's Claims 17-1 to 17-3 are not used; see
reports/padded-lines-product-law.md.
The other register version #
The paper's lem:qld-4-13 asserts the relation in both orientations. The second is the first
applied to the exchanged model M.swap, with the two strategies exchanged, read back through
hatVec_swapVec_xSqNorm and hatVec_swapVec_bornProb --- the route Swap.lean takes for the
expansion stage's point items. The two mirrored inputs are lem:qld-expanded-lines' second item
with the players exchanged.
lem:qld-padded-lines, the consistency bound in the other register version: the first
player's pasted line measurement against the second player's combined point measurement, in the
expanded model.