The padded space, and the sublines of a padded line #
Blueprint lem:qld-sublines. The combining stage compares a measurement of pairs of
m-variable polynomials with a low-degree test, and a low-degree test wants a single polynomial
in a number of variables dividing q. The paper's device is to pad: work over F_q^{4m}, whose
coordinates split as u = (x, z, alpha, beta, w) with x, z in F_q^m, alpha, beta in F_q
and w in F_q^{2m-2} the dummy coordinates, and to combine the pair (f_X, f_Z) into the
single polynomial alpha f_X(x) + beta f_Z(z). Admissibility makes m a power of two, so
2m + 2 never divides q = 2^k, while 4m does as soon as 4m <= q; that is the whole reason
the dummy block is there.
This file is the geometry of that padding, and it is deliberately free of operators.
The two pieces #
- The seed's block and offset. The seeded test reads an axis index off a seed through
chi, which is "which of themequal blocks ofFdoessfall into".seedEquivnames the corresponding bijectionF ~ Fin m x Fin (q/m), withchias its first component. Two things follow that the subline construction needs: a seed can be retargeted to a prescribed block keeping its offset (seedIn), and a uniform seed retargeted to a fixed block is uniform on that block's fibre (sum_seedIn). The paper's "chooses_Xuniformly at random subject tochi(s_X) = i" is exactly this. - The blocks of
F_q^{4m}.xIdx,zIdx,aIdx,bIdxare the coordinate positions andxBlk,zBlk,alph,betthe projections.padCaseclassifies a coordinate position into the four blocks, which is the case distinction the construction oflem:qld-sublinesbranches on: whether the padded line's direction moves anXcoordinate, aZcoordinate, or onlyalpha,betaand the dummy coordinates.
Why 4m and not 2m + 2 #
aIdx and bIdx sit at positions 2m and 2m + 1, so the dummy block is positions
2m + 2, ..., 4m - 1, of size 2m - 2. Every index bound below needs only 1 <= m.
In a bipartite model #
Stated in a bipartite model (Phase 5 of planning/mipco-track.md), which changes nothing here:
no statement of this file mentions a state, a strategy or an operator, so the geometry is the
matrix route's verbatim, compiled against the model form of MIPRE/Background/QLD/Lines.lean.
The seed's block and offset #
A seed's block and offset: the bijection F ~ Fin m x Fin (q/m) whose first component is
chi, available because m divides q.
Equations
- MIPRE.QLD.seedEquiv hm = (Fintype.equivFin F).trans ((finCongr ⋯).trans finProdFinEquiv.symm)
Instances For
The first component of seedEquiv is chi: both are "divide the index by the block size".
The seed in block i with the same offset as s. For a fixed i this turns a uniform seed
into a uniform seed of axis index i, which is the paper's "s_X uniformly at random subject to
chi(s_X) = i".
Equations
- MIPRE.QLD.seedIn hm i s = (MIPRE.QLD.seedEquiv hm).symm (i, ((MIPRE.QLD.seedEquiv hm) s).2)
Instances For
Retargeting a seed to its own block does nothing.
A uniform seed retargeted to a fixed block is uniform on that block. Summing over all
seeds counts each seed of block i exactly m times, once per block the offset could have come
from. This is the only property of seedIn the mixture-of-products statement of
lem:qld-sublines uses.
The blocks of the padded space #
The alpha coordinate of a padded point.
Equations
- MIPRE.QLD.alph u = u (MIPRE.QLD.aIdx m)
Instances For
Moving along the padded line moves the X block along the X block of the direction. This
is the identity that makes the combining map of lem:qld-padded-lines well defined.
Which block a coordinate position lies in #
Where a coordinate position of the padded space lies: in the X block, in the Z block, at
alpha or beta, or among the dummy coordinates. The construction of lem:qld-sublines
branches on this.
- xc {m : ℕ} [NeZero m] (i : Fin m) : PadCase m
- zc {m : ℕ} [NeZero m] (i : Fin m) : PadCase m
- ab {m : ℕ} [NeZero m] : PadCase m
- dum {m : ℕ} [NeZero m] : PadCase m
Instances For
The blocks of a single coordinate and of a truncated direction #
These are the only geometric facts the subline construction needs: they say which block of the padded direction is nonzero, and what it is.
The sublines of a padded line #
Blueprint lem:qld-sublines. The paper's D is a sampling procedure, and this is that procedure:
subX and subZ read the two m-dimensional line-point pairs off a padded one together with a
pair of fresh seeds and raw directions.
The shape of the construction is forced by what Property 2 demands. Moving along the padded line
moves the X block along the X block of the padded direction, so if that block is nonzero the
X subline has no choice: its direction must be exactly that block, and the only freedom left is
which seed presents it, which is where seedIn comes in. If the block vanishes the X block is
constant along the padded line, the containment is free, and the subline is sampled fresh.
The four cases of padCase say which blocks vanish, and they do not say the same thing for the
two line types. For an axis-parallel padded line the direction is a single coordinate, so at most
one of the two blocks is nonzero. For a diagonal padded line the direction is v truncated below
the axis index, so an index in the X block leaves the whole Z block untouched: both blocks are
then nonzero, and the Z subline is forced too --- at axis index 0, since nothing of its
direction is truncated. That asymmetry is the only place subZ looks at the line type.
The data a line-point pair of the seeded test is generated from: the point, the seed, and the
raw diagonal direction. This is the part of MIPRE.LIDT.CL.Sample that the line questions read,
and it has the same shape in the padded dimension 4m and the unpadded dimension m.
- pt : LIDT.Point F m
The sampled point.
- s : F
The seed, which selects the axis index through
chi. - raw : LIDT.Point F m
The raw diagonal direction, truncated by
zeroBelowbefore use.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- MIPRE.QLD.instFintypeLPData = Fintype.ofEquiv ((_ : MIPRE.LIDT.Point F✝ m✝) × (_ : F✝) × MIPRE.LIDT.Point F✝ m✝) (MIPRE.QLD.LPData.proxyTypeEquiv F✝ m✝)
Truncating below the first coordinate truncates nothing.
The sample whose questions this data generates. Both players are given the same type, which is all that the line questions read.
Instances For
The question of type t this data presents, as the seeded test computes it.
Equations
- MIPRE.QLD.LPData.question hm t c = MIPRE.LIDT.CL.Sample.question hm (MIPRE.QLD.LPData.toSample t c) t
Instances For
The direction of the line this data presents.
Equations
- MIPRE.QLD.LPData.dir hm t c = MIPRE.LIDT.CL.Question.dir hm (MIPRE.QLD.LPData.question hm t c)
Instances For
On a line type the base point of the question is the canonical representative of the point in the direction, which is what puts the point on its own line.
The X-side subline data, as a function of the block the padded axis index lies in. Splitting
the case distinction out of subX is what lets a proof rewrite the block and then reduce.
Equations
- MIPRE.QLD.subXof hm (MIPRE.QLD.PadCase.xc i) P e = { pt := MIPRE.QLD.xBlk P.pt, s := MIPRE.QLD.seedIn hm i e.1, raw := MIPRE.QLD.xBlk P.raw }
- MIPRE.QLD.subXof hm k P e = { pt := MIPRE.QLD.xBlk P.pt, s := e.1, raw := e.2 }
Instances For
The X-side subline data of a padded line-point pair. The point is the X block of the padded
point; the direction is forced to the X block of the padded direction when that block is nonzero,
with the fresh seed e.1 supplying only the offset inside the forced block, and is sampled from e
when it vanishes. No case distinction on the line type is needed here: an axis index in the X
block forces the X block of the direction for both types at once.
Equations
- MIPRE.QLD.subX hm4 hm P e = MIPRE.QLD.subXof hm (MIPRE.QLD.padCase (MIPRE.LIDT.CL.chi hm4 P.s)) P e
Instances For
The Z-side subline data, as a function of the line type and of the block the padded axis index
lies in.
Equations
- MIPRE.QLD.subZof hm MIPRE.LIDT.CL.Ty.dline (MIPRE.QLD.PadCase.xc i) P e = { pt := MIPRE.QLD.zBlk P.pt, s := MIPRE.QLD.seedIn hm 0 e.1, raw := MIPRE.QLD.zBlk P.raw }
- MIPRE.QLD.subZof hm t (MIPRE.QLD.PadCase.zc i) P e = { pt := MIPRE.QLD.zBlk P.pt, s := MIPRE.QLD.seedIn hm i e.1, raw := MIPRE.QLD.zBlk P.raw }
- MIPRE.QLD.subZof hm t k P e = { pt := MIPRE.QLD.zBlk P.pt, s := e.1, raw := e.2 }
Instances For
The Z-side subline data. A diagonal padded line whose axis index lies in the X block leaves
the whole Z block of its direction intact, so the Z subline is forced, at axis index 0 since
nothing of its direction is truncated; an axis-parallel one leaves that block zero, so the Z
subline is free. That is the one asymmetry between the two sides.
Equations
- MIPRE.QLD.subZ hm4 hm t P e = MIPRE.QLD.subZof hm t (MIPRE.QLD.padCase (MIPRE.LIDT.CL.chi hm4 P.s)) P e
Instances For
Property 2 of lem:qld-sublines: the blocks of the padded direction #
The X block of the padded direction is the X subline's direction, or it vanishes. This
is the whole geometric content of the construction: in the first case the X block of a point moves
along the subline as the point moves along the padded line, in the second it does not move at all,
and either way it stays on the subline.
The Z block of the padded direction is the Z subline's direction, or it vanishes.
Property 2 of lem:qld-sublines, the containment #
Whether the shift direction is the candidate direction or zero, the shifted point lies on the line the candidate direction presents through the unshifted point. This is the one-line calculation behind the containment, and it is where the point's own parameter enters.
Property 2 of lem:qld-sublines, the X side: the X block of every point of the padded
line lies on the X subline.
Property 2 of lem:qld-sublines, the Z side.
The containment in the paper's own terms for an axis-parallel padded line: the X block of a
point of the padded line is a point of the X subline as the seeded test presents it, base point
and direction.
Property 3 of lem:qld-sublines #
The paper's Property 3 --- an axis-parallel padded line has axis-parallel sublines --- is
definitional here, because the line type is a parameter handed to both sides rather than something
the construction chooses. What is not definitional, and is the reason the paper needs the
property, is that the two directions then agree in the way xBlk_dir_sub and zBlk_dir_sub state;
those are the lemmas a consumer should cite.
The padded space as a product of its blocks #
lem:qld-sublines' second property is distributional: under a uniform point of a padded line the
two sublines are drawn from a mixture of products of restricted laws, with each side's point
conditionally uniform on its line. What makes that true is that the X and Z blocks of a uniform
padded point are uniform and independent, and that is a statement about the index type: Fin (4m)
is the disjoint union of the X block, the Z block, and the 2m positions above them. padEquiv
names that decomposition and sum_point_pad is the resulting product identity.
The block decomposition of the padded index type. The X block lands on positions
0, ..., m-1 and the Z block on m, ..., 2m-1, which is exactly xIdx and zIdx.
Equations
- MIPRE.QLD.padEquiv m = ((finSumFinEquiv.sumCongr (Equiv.refl (Fin (2 * m)))).trans finSumFinEquiv).trans (finCongr ⋯)
Instances For
The X and Z blocks of a uniform padded point are uniform and independent. The remaining
2m coordinates -- alpha, beta and the dummy block -- contribute the multiplicity.
Only the X block of the padded point is read.
Only the Z block of the padded point is read.
The law of the sublines #
lem:qld-sublines' second property is that under a uniform point of a padded line the pair of
sublines is drawn from a mixture of products of restricted line-point laws, each side's point
conditionally uniform on its own line. sumRestr and sumAll are the two laws, unnormalized, and
sumSub is the sum over the sampling space; the four branch identities below say which product each
branch of the construction gives, and with what multiplicity.
The sum of h over the data of a line-point pair whose axis index is i: the restricted law
D_{ty,i} of def:ith-restricted-line, unnormalized. The seed ranges over the fibre of chi above
i, written through seedEquiv as an offset.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The sum of h over all the data of a line-point pair: the unrestricted seeded law,
unnormalized.
Equations
- MIPRE.QLD.sumAll h = ∑ pt : MIPRE.LIDT.Point F m, ∑ s : F, ∑ raw : MIPRE.LIDT.Point F m, h { pt := pt, s := s, raw := raw }
Instances For
The unrestricted law is the sum of the m restricted ones. This is the "mixture" of
lem:qld-sublines' second property: a branch that leaves a side free gives that side the
unrestricted law, which is the uniform mixture of the D_{ty,i}.
The sum over the subline sampling space at a fixed padded seed: the padded point and the padded raw direction, and a fresh seed and raw direction for each side.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Neither side is forced: the axis index of the padded line lies in the alpha/beta block
or among the dummy coordinates, so the padded direction moves neither the X nor the Z block and
both sublines are sampled fresh. Both sides get the unrestricted law.
The Z side is forced: the padded axis index lies in the Z block, so the Z subline's
direction is the Z block of the padded direction and its axis index is i, while the X block of
the padded direction vanishes and the X subline is sampled fresh. The Z side gets the restricted
law D_{ty,i}, the X side the unrestricted one.
The X side is forced and the Z side is not: the padded axis index lies in the X block
and the padded line is axis-parallel (or the question is a point), so the Z block of its direction
vanishes. The X side gets the restricted law D_{ty,i}, the Z side the unrestricted one.
Both sides are forced: the padded axis index lies in the X block and the padded line is
diagonal, so its direction truncates nothing of the Z block and the Z subline is forced as well,
at axis index 0. Both sides get restricted laws. This is the branch whose repair the paper's
round-12 note on lem:qld-sublines records.
From sums to averages #
The four branch identities are sum identities with an explicit multiplicity: the assignments to the
coordinates and to the fresh randomness that the construction does not read. Dividing by the number
of terms turns them into the statement lem:qld-sublines makes --- an identity of laws, with no
constant left over. The average over the subline sampling space is exactly the average over a
product of two line-point laws, restricted on a side exactly when the padded direction forces that
side's subline.
The average of h over all the data of a line-point pair: q^m points, q seeds, q^m raw
directions.
Equations
- MIPRE.QLD.avgAll h = (↑(Fintype.card F) ^ (2 * m + 1))⁻¹ * MIPRE.QLD.sumAll h
Instances For
The average of h over the data of a line-point pair with axis index i: the restricted law
D_{ty,i}, whose seed ranges over one block of q/m elements.
Equations
- MIPRE.QLD.avgRestr hm i h = (↑(Fintype.card F) ^ (2 * m) * ↑(Fintype.card F / m))⁻¹ * MIPRE.QLD.sumRestr hm i h
Instances For
The average of g over the subline sampling space at a fixed padded seed: two padded points and
two fresh seed-and-direction pairs.
Equations
- MIPRE.QLD.avgSub hm4 hm t s g = (↑(Fintype.card F) ^ (10 * m + 2))⁻¹ * MIPRE.QLD.sumSub hm4 hm t s g
Instances For
The block size as a real division, which is what clearing the denominators needs.
Neither side forced: the padded average is the product of the two unrestricted averages.
The Z side forced: the padded average is the product of the unrestricted X average and
the restricted Z average at index i.
The X side forced, the Z side free.
Both sides forced, the Z side at index 0.
The restricted law is the unrestricted one up to a factor of m #
The paper's def:ith-restricted-line splits the line-point distribution by axis index and observes
that an approximation holding at error delta on average holds on each restricted law at
2m * delta --- the 2 being the mixture over the two line types, which here is a parameter rather
than something mixed over, so the factor is m. This is where every factor of m in
delta_combine = m * poly(eps, md/q) comes from, and it is one line on top of
sumAll_eq_sum_sumRestr: the m restricted laws are nonnegative and average to the unrestricted
one, so each of them is at most m times it.
A bound on the unrestricted law bounds each restricted one, at m times the error.
The product form, at m^2 times the error: the shape the pasting lemma's hypotheses are in,
each side's line drawn from its own restricted law.
The unrestricted law is the uniform average over the data #
pairs_of_lines_prod is stated as a uniform average over LPData F m x LPData F m; avgAll is the
same average written as nested sums. One equiv identifies them.
The data of a line-point pair, as a triple.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The product form.
Linearity and monotonicity of the averages #
The padded law is dominated by the product law #
This is the distributional content of the paper's Claims 17-1 to 17-3, and it is stronger than what
those claims extract. The paper's \cnote on the conclusion of lem:qld-4-13 says the joint law of
the two sublines-with-points is not a product, because "for diagonal lines both coordinates share
the line parameter", and the three claims are written to use only the marginals. That is right about
conditioning on the padded line: given it, the two blocks of a uniform point on it move with one
parameter. But the quantity to be bounded conditions only on the two sublines, which know each
block's coset in its own space and not the relative offset --- and avgSub_free and its three
companions say that at a fixed padded seed the joint law is exactly a product of the two marginals,
each of them restricted or not according to padCase. Combining that with the restricted-law
transfer bounds the padded law by m^2 times the product of the two unrestricted laws, uniformly in
the padded seed and the line type.
The Z side restricted, the X side free.
The X side restricted, the Z side free.
The padded line-point law is at most m^2 times the product of the two unrestricted subline
laws, whatever the padded seed and the line type.
The alpha and beta coordinates of the padded point #
The measurement of lem:qld-padded-lines reads alpha and beta at the sampled padded point, which
avgSub does not carry. They are coordinates of the padded point outside the X and Z blocks, so
translating the point in those two coordinates alone leaves both sublines untouched --- which makes
the (alpha, beta) average uniform and independent of everything else, and a bound that holds for
every fixed (alpha, beta) therefore holds for the joint law. No refinement of the block
decomposition is needed.
Translating the padded point in its alpha and beta coordinates only.
Equations
- MIPRE.QLD.shiftAB c d u = u + (Pi.single (MIPRE.QLD.aIdx m) c + Pi.single (MIPRE.QLD.bIdx m) d)
Instances For
The inner average of the subline sampling space, at a fixed padded point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The padded average with alpha and beta carried.
Equations
- MIPRE.QLD.sumSubAB hm4 hm t s g = ∑ pt : MIPRE.LIDT.Point F (4 * m), MIPRE.QLD.sumSubAt hm4 hm t s pt (g (MIPRE.QLD.alph pt) (MIPRE.QLD.bet pt))
Instances For
The normalized version.
Equations
- MIPRE.QLD.avgSubAB hm4 hm t s g = (↑(Fintype.card F) ^ (10 * m + 2))⁻¹ * MIPRE.QLD.sumSubAB hm4 hm t s g
Instances For
(alpha, beta) is uniform and independent of the two sublines, because translating the
padded point in those two coordinates alone is a bijection that leaves both sublines fixed.
A bound that holds for every fixed (alpha, beta) holds for the padded law.