Soundness of answer reduction: the per-seed low-degree games #
Piece AR-5b of planning/answer-reduction.md (claim:ar-3, claim:ar-4, def:ar-seed-index).
A strategy for the typed answer-reduced game, restricted to one copy of the low-degree test at a
role pair where that copy is tested and to one seed of the input sampler, is a strategy for the
seeded CL test of the copy's parameters (copyStrategy): its question maps a CL question to the
typed question whose PCP half the copy's presentation computes (Regs.embedQ) and whose oracle
half the seed's role family gives, and its answers are parsed and read as answers of the copy's
test. The seeds are indexed by the full seed of the input sampler, as the blueprint's
def:ar-seed-index asks.
The per-seed failures average to at most a constant times the typed failure
(sum_one_sub_value_copyStrategy_le): the copy's nine type pairs are a fixed fraction of the
typed game's, and the copy's registers of a uniform PCP vector carry a uniform sample
(Regs.sum_sampleOf).
The strategies are projective strategies in a bipartite model (BipartiteModel.ProjStrat), as in
every file of the soundness chain, so that the analysis holds in the tensor-product and in the
commuting-operator model alike (Phase 3 of planning/mipco-track.md); a per-seed strategy is the
typed strategy played through maps (BipartiteModel.ProjStrat.adapt), and so is projective in
the same model.
The seeded test's distribution is the push-forward of the uniform sample.
The seeded test's failure is the average failure over samples.
The bits of a vector of V^pcp, in the numbering of a question's PCP half.
Equations
- MIPRE.AnswerReduction.pcpBits P hk w = (MIPRE.CL.reindexEquiv (MIPRE.AnswerReduction.Pcp.bitIndex P P.k)) ((MIPRE.CL.downsizeEquiv (MIPRE.AnswerReduction.basis P hk)) w)
Instances For
The typed question of a CL question of copy i ≤ 5, at role r and oracle half x.
Equations
- MIPRE.AnswerReduction.arQ1 V n P hk S r i x q = ((r, i.castSucc, q.ty), Fin.append x (MIPRE.AnswerReduction.pcpBits P hk ((MIPRE.AnswerReduction.Pcp.regs P i).embedQ S q)))
Instances For
An answer read as an answer of copy i's test: parsed at the question's type, then read by
ans1; a failed parse reads as the zero point answer.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The per-seed low-degree strategy of copy i ≤ 5 at role r and oracle half y: the
typed strategy played through arQ1 and readAns1, both players at role r. At the seed x₀ of
the input sampler the oracle half is (roleFamily L r).eval x₀: the seed itself for an oracle,
the original player's question for an isolated player, whose measurements see nothing else.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The per-seed strategy loses no acceptance: on the question pair of a sample of the copy's test, an answer pair the typed predicate accepts at the corresponding typed questions is read as one the copy's test accepts, at a role pair where the copy is tested.
T's failure at the typed question pair of sample sm at oracle half y.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The per-seed failure is at most the average of T's failures at the typed questions of
the copy's samples.
The bits of a vector of V^pcp, as an equivalence.
Equations
Instances For
The typed question of copy i at type τ, on the vector whose oracle half is x and whose
PCP half is w: the typed question arQ1 of the sample copy i's registers carry.
T's failure at the typed question pair of the type pair uv, on the vector whose oracle half
is x and whose PCP half is w.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Any set of type pairs inside the typed failure: the failures at an injective family of type pairs, summed over the oracle halves and the PCP vectors, add up to at most the number of type pairs times the number of vectors times the typed game's failure.
The copy's edges inside the typed failure: the nine type pairs of copy i at role r,
summed over the seeds and the samples, weigh at most the typed game's failure.
The per-seed failures average to at most 324 times the typed failure, at a role pair
where copy i is tested: the copy's nine type pairs are 9 / 54^2 = 1 / 324 of the typed game's
edges, and on them the copy's registers of a uniform vector carry a uniform sample.
The sixth copy #
The typed question of a CL question of the sixth copy, at role r and oracle half x.
Equations
- MIPRE.AnswerReduction.arQ6 V n P hk S' r x q = ((r, 5, q.ty), Fin.append x (MIPRE.AnswerReduction.pcpBits P hk ((MIPRE.AnswerReduction.Pcp.regs6 P).embedQ S' q)))
Instances For
An answer read as an answer of the sixth copy's test: parsed at the question's type, then
read by ans6.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The per-seed simultaneous low-degree strategy of the sixth copy at oracle half y: the
typed strategy played through arQ6 and readAns6, both players oracles.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The sixth copy's per-seed strategy loses no acceptance.
T's failure at the typed question pair of sample sm of the sixth copy at oracle half y.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The sixth copy's per-seed failure is at most the average of T's failures at the typed
questions of the copy's samples.
The typed question of the sixth copy at type τ, on the vector whose oracle half is x and
whose PCP half is w.
The sixth copy's edges inside the typed failure.
The sixth copy's per-seed failures average to at most 324 times the typed failure.