The combining map and the padded line measurement #

Blueprint lem:qld-padded-lines, the definitional half. The pairs-of-lines stage measures a pair of line polynomials, one per basis; the low-degree test over the padded space F_q^{4m} wants a single polynomial on a single padded line. The bridge is the paper's combining map: on the padded point u = (x, z, alpha, beta, w) the combined polynomial takes the value

alpha * f_X(x) + beta * f_Z(z).

Three things have to be said about it, and this file says them.

It is a polynomial of degree at most md + 1 on the padded line. Restricted to the padded line the two evaluations become evaluations of f_X and f_Z at affine functions of the padded parameter --- which is exactly Property 2 of lem:qld-sublines, made quantitative --- and the factors alpha and beta are affine in it too. So the whole thing is a product of an affine polynomial with a degree-md one, and combine is that polynomial, built through Mathlib's Polynomial and truncated back to a coefficient vector.
On an axis-parallel padded line the degree drops to d. The padded direction is a single coordinate, and the case distinction is the one padCase already makes: in the X and Z blocks alpha and beta are constant along the line, so the degree is that of f_X and f_Z; at alpha, beta or a dummy coordinate both blocks are constant along the line, so the combined polynomial is affine. The first case needs f_X and f_Z to have degree d, which is lem:qld-axis-degree; the second needs only d >= 1.
The measurement. padLineMats is the paper's Q-hat^l: the conditional average, over the fresh randomness the subline construction draws, of the pasted line measurement T^{l_X,l_Z}, coarse-grained by the combining map. It is a POVM in a player's algebra of the expanded model.

What is not here is the consistency bound delta_combine; see the blueprint.

In a bipartite model #

Stated in a bipartite model (Phase 5 of planning/mipco-track.md). Only the measurement changes: the pasted line measurement (MIPRE/Background/QLD/Lines.lean) is a family of elements of Matrix (Anc F m) (Anc F m) R over a player's ordered ⋆-algebra R, with no combining register F × F (it was inert in every padded measurement), so padLineMats is an average of pasted sandwiches there. Completeness is IsPVMIn.sum_conj' and nonnegativity is the Gram form IsPVMIn.conj_eq_gram of a sandwich, averaged with nonnegative real weights (real_smul_nonneg); the name posSemidef_* is kept for these nonnegativity statements. The combinatorics of the combining map is unchanged.

The affine data, and why the whole geometry is in `xBlk_dir_sub` #

The one calculation behind the affine substitutions is this. Moving along the padded line moves the X block by tau * xBlk(dir), and xBlk_dir_sub says that block is either the X subline's own direction or zero. In the first case the parameter on the subline moves by exactly tau, in the second it does not move at all --- so in both cases it is p0 + c * tau with c one or zero, and subAff is that pair. Nothing else about the construction is used.

The combining map and the padded line measurement #

In a bipartite model #

The affine data, and why the whole geometry is in xBlk_dir_sub #

Affine maps of the line parameter #

Coefficient vectors and polynomials, the other way #

The combining map #

The affine substitution a subline induces #

The affine data of a padded line and its sublines #

The four affine maps #

The parameter identity #

The padded combining map #

The degree bound on an axis-parallel padded line #

The padded line measurement #

The affine data, and why the whole geometry is in `xBlk_dir_sub` #