The seeded-CL adapter, part 5: both tests' distributions, as counts #
The reduction's remaining obligation is a push-forward bound between the two tests' question
distributions, and both are defined as sums over a Sample type against an indicator. So the
first thing to do is to turn each into a count, after which the bound is arithmetic on
cardinalities rather than on sums.
clGame's distribution is uniform over its samples, so it is the number of samples producing the question pair, over the total (clGame_μ_eq).lidtGame's is not uniform — its three subtests are weighted1/3each and its diagonal directions carry a factorq^{-(j+1)}— so the best that can be said in general is that it is the sum of the weights of the samples producing the pair (lidtGame_μ_eq). That sum is a singleton for the point and axis-parallel shapes and a geometric series over the admissiblejfor the diagonal one, which is where theq^{χ s}againstq^{j+1}matching ofplanning/lidt-cl-adapter.mdlives.
The seeded test's distribution, as a count. It is uniform over its samples, so the weight of a question pair is the number of samples producing it over the total.
The canonical-line test, shape by shape #
Each shape needs the set of samples producing a given question pair. For the point and axis-parallel shapes it is a singleton and the weight is read off directly; the diagonal shape is the one where several samples contribute.
The diagonal shape #
Here several samples contribute, so the weight is a sum. It does not have to be evaluated:
in the push-forward bound the canonical-line weight appears only on the larger side, so an upper
bound suffices, and bounding the sum by count × largest term costs only a factor m in the
constant --- which δ_CL absorbs, being allowed a prefactor polynomial in m and d. What it
may not absorb is a factor growing with q, so the q-exponent has to be right, and that is
what le_rev_diagIdx_of_questions pins down.
A sample producing a given diagonal line against a given point is a diag sample at that
point whose direction is a nonzero multiple of the line's.
The direction pins the q-exponent. A sample producing the line has j at least the
reversal of diagIdx ℓ: its direction vanishes above j, hence so does the line's, hence the
reversed direction vanishes below rev j, so its first nonzero coordinate is at least
rev j.
The key (j, c) of a diagonal sample, read at a coordinate p. Two samples producing the
same line with the same key are equal, which is what bounds the count.
Equations
- MIPRE.LIDT.Adapter.diagKey p (MIPRE.LIDT.Sample.diag swap u j v) = (j, MIPRE.LIDT.Sample.extend v p)
- MIPRE.LIDT.Adapter.diagKey p x✝ = (MIPRE.LIDT.Adapter.idx0, 0)
Instances For
At most m q samples produce a given diagonal line against a given point. A sample is
pinned by its j together with the scalar relating its direction to the line's, and there are
m values of the first and q of the second.
Every sample producing a given diagonal line against a point has weight at most
1/(6 m q^m q^{rev (diagIdx ℓ) + 1}). This is where the q-exponent of the bound is fixed:
le_rev_diagIdx_of_questions says a contributing sample's j is at least rev (diagIdx ℓ).
The seeded test, shape by shape #
Only lower bounds are needed here, since the seeded weight sits on the smaller side of the push-forward bound, and a lower bound on a count is an injection into the set of contributing samples. That is much cheaper than an exact count, and it is why this section is short.
The samples of the seeded test that ask the same point twice include one for every seed and
every raw direction, so there are at least q · q^m of them.
Likewise for an axis-parallel line against a point: one sample for every raw direction.
And for a diagonal line against a point, provided the direction really does vanish below the
seed's block --- which it must, for the question to be in the seeded test's support. There is one
sample for every completion of the direction below that block, hence at least q^{χ s}.
From fibres of the question map to samples #
The push-forward bound is stated over fibres of the question map, but the canonical-line test's weight lives on samples, and only five shapes of question pair carry any weight at all. This lemma moves the whole thing onto samples, where the case analysis is a case analysis on a constructor.
Counting the seed choices #
With the push-forward on samples, the average over the family becomes a weight times a count of family members, and that is what the shapes differ in: a point question's image does not depend on the family member at all, while a line question's pins the seed at one index (and, for a diagonal, the scale).
Averaging over a family, as a weight times a count of family members.
The averaging family: a fibre position for each direction index, and one global nonzero
direction scale. The scale is there because of the second correction in
planning/lidt-cl-adapter.md.
Instances For
The seeded question a canonical-line question is played through, for a family member.
Equations
- MIPRE.LIDT.Adapter.qmapS hm σc = MIPRE.LIDT.Adapter.qmap hm σc.1 ↑σc.2
Instances For
The point shape #
Only the self-consistency sample can contribute, and its image does not depend on the family
member, so averaging neither helps nor hurts here: the requirement is the unaveraged
1/(3 q^m) ≤ C · 1/(9 q^m), i.e. C ≥ 3.
The samples whose images are a pair of point questions: at most the self-consistency sample at the reversed point.
And if the two points differ, nothing contributes: the one candidate fails the second condition.
Cardinalities #
Three counts enter the arithmetic: the point space, the seeded test's sample space and the
averaging family. Only the first has to be known as a power of q; the other two enter as
symbols that cancel.
The seeded test's sample space: nine ordered type pairs against (u, s, v).
The averaging family: a fibre position per direction index, and one nonzero scale.
The shape of every one of the bounds #
All four nonzero shapes are bounded the same way: the contributing samples lie in one finite set
T that does not depend on the family member, each of them has weight at most B, and each is
picked out by at most M family members.
Count times weight times count.
The mirrored shapes come for free #
Both tests are symmetric under exchanging the two players --- lidtGame's swap bit and
clGame's ordered type pair --- so a bound for (x, y) is a bound for (y, x), and only the
shapes with the line on the left have to be done by hand.
Flipping a sample's swap bit.
Equations
Instances For
The swap as an equivalence of samples.
Equations
- MIPRE.LIDT.Adapter.swapEquiv = { toFun := MIPRE.LIDT.Adapter.swapSample, invFun := MIPRE.LIDT.Adapter.swapSample, left_inv := ⋯, right_inv := ⋯ }
Instances For
The canonical-line side is symmetric.
The type exchange as an equivalence of seeded samples.
Equations
- MIPRE.LIDT.Adapter.clSwapEquiv = { toFun := MIPRE.LIDT.Adapter.clSwap, invFun := MIPRE.LIDT.Adapter.clSwap, left_inv := ⋯, right_inv := ⋯ }
Instances For
The seeded side is symmetric too, the nine ordered type pairs being equally likely.
The seed counts #
A line question's image pins the family's fibre position at exactly one index --- and, for a
diagonal, the scale as well. That is the whole content of the averaging: the family has
(q/m)^m (q-1) members and only (q/m)^{m-1} (q-1) or (q/m)^{m-1} of them can contribute.
A pinned seed index costs a factor q/m.
The axis-parallel shape #
The seed determines the direction index, so the contributing sample is unique and the constraint on the family is at one index.
At most one sample maps to an axis-parallel question against a point.
The adapter's axis-parallel base point, unreversed: exactly the seeded test's own.
The base point the contributing sample forces. If anything contributes to an
axis-parallel question against a point, the question is the one the seeded test itself would
have asked at that point and seed: revPoint_rep_single unreverses the adapter's base point.
The family members that can contribute to an axis-parallel question: the seed index is
pinned, so there are at most (q/m)^{m-1} (q-1) of them.
The arithmetic facts #
Each shape ends in an inequality between two explicit rationals in q, m and q/m. These are
the casts and positivity facts they all need.
The block size, as a real.
Equations
- MIPRE.LIDT.Adapter.blk F m = ↑(Fintype.card F / m)
Instances For
The averaging family's size, as a real.
The seeded test's sample space, as a real.
The axis-parallel bound #
The axis-parallel shape of the push-forward bound. The one contributing sample has weight
1/(6 m q^m), the family pins one seed index, and the seeded test puts at least 1/(9 q^{m+1})
on the pair; the three combine with room to spare at C = 3m (3/2 would do).
The point bound #
Here the averaging is neutral: the image of a point question does not depend on the family
member, so both sides carry the same factor |Seed| and the requirement is the unaveraged
1/(3 q^m) ≤ C/(9 q^m).
The point shape of the push-forward bound.
The diagonal shape #
Two cases, and they are genuinely different. A nondegenerate diagonal question determines the
line, the scale and the seed index, so the family is pinned twice over and only (q/m)^{m-1} of
its members contribute. A singleton question (direction zero) pins the seed index but not the
scale --- scaling the zero direction does nothing --- and is paid for instead by diagIdx
sending singleton lines to χ = m - 1, where the seeded test has q^{m-1} samples rather
than one.
Only a diagonal sample with the line on the left maps to a DLine question against a
point, and the point pins its point.
A singleton DLine question comes only from a sample with zero direction.
The adapter's image of a singleton diagonal line.
What a contributing sample forces, for a singleton DLine question.
The singleton diagonal shape of the push-forward bound. The m contributing samples have
weight at most 1/(6 m q^m q), the family pins the seed index but not the scale, and the seeded
test has q^{m-1} samples for this question --- which is why diagIdx sends singleton lines to
the last block. The three combine at C = 3m with a factor 2 to spare.
The nondegenerate diagonal shape #
Here the question determines the line, the scale and the seed index, so the family is pinned
twice and only (q/m)^{m-1} of its members contribute. That second pinning is what the scale
averaging bought.
A set of family members agreeing at one seed index and on the scale has at most
(q/m)^{m-1} elements.
Rescaling a reversed direction does not move the adapter's base point off the seeded
test's. This is the diagonal analogue of revPoint_through_single_eq_rep: the seeded question
carries c · ρℓ₂ as its direction and rep of that is the adapter's ρℓ₁ - sh · ρℓ₂.
A seeded direction vanishes below its own χ-index, which is what puts the question in
the seeded test's support.
A canonical presentation has a nonzero direction as soon as its input direction is nonzero.
Rescaling the reversed direction identifies the two canonical presentations.
The data a contributing sample carries, read off the question.
A sample mapping to a nondegenerate DLine question asks the reversed line at the
reversed point.
What a contributing sample forces, for a nondegenerate DLine question.
The nondegenerate diagonal shape of the push-forward bound. At most m q samples
contribute, each of weight at most 1/(6 m q^m q^{J+1}), and the family is pinned both at the
seed index and on the scale, so only (q/m)^{m-1} of its members can contribute. Against the
seeded test's q^{χ} samples, with J + 1 + χ = m, the constant comes out 3q/(2(q-1)), which
C = 3m covers for every q ≥ 2.
The pairs of lines, and the assembly #
lidtGame's only same-type subtest is point self-consistency, so no sample asks two lines and
the four remaining shapes carry no weight at all. That is the piece of luck this route runs on:
it needs no line-synchronicity transfer, hence no Schwartz--Zippel and no d/q term.
No sample of the canonical-line test asks two lines.
The shapes with a line on both sides carry no weight.
The bound for (x, y) is the bound for (y, x), both tests being symmetric under
exchanging the players.
The push-forward bound, assembled. The average over the family of the canonical-line
test's mass on the fibre of a seeded question pair is at most 3m times the seeded test's mass
on it. This is the hypothesis exists_one_sub_value_adapt_le asks for, and 3m is the constant
thm:lidt-cl-soundness multiplies its ε by --- polynomial in m, as δ_CL allows, and free
of q, which it does not.