Soundness of the answer-reduced game: the per-role low-degree games #
The first step of the soundness of 𝔄𝔫𝔰ℜ𝔢𝔡 (prop:completeness_soundness_combi_ans_red, II:10487),
for a projective strategy T in a bipartite model for the answer-reduced typed game arGame on
the CL functions of an answer-reduced sampler (ArSampler).
A typed question carries the oracularized input question of its role and a question of the seeded
low-degree test (ArSampler): at the seed (z, w) of the input sampler and the test's registers,
the question of type (r, τ) is arQr r (oq r z) (ldq τ w), the typed question presenting the
role's oracularized question and the test's question of type τ of the sample w carries
(eval_seed). So:
- the typed failure is the average over the
81type pairs and the seeds(z, w)ofT's failure at those questions (one_sub_value_eq_sum), and any set of type pairs weighs at most81times the typed failure (sum_edges_le); Tplayed at one role and one oracularized question, througharQrand the readingdecAnsof the role's codewords, is a strategy for the seeded low-degree test with one codeword per slot of the role (roleStrat): the typed data's low-degree check is the test's predicate (arDt_role), so it loses no acceptance;- its failures average, over the seeds of the input sampler, to at most
9times the typed failure (sum_one_sub_value_roleStrat_le): a role's nine type pairs are1/9of the81, and the registers of a uniform vector carry a uniform sample (Regs.sum_sampleOf_retype, with multiplicity1, the test's registers being all ofF_q^{D}).
The paper runs the test inside its first perturbation (II:10623); its type graph has the
low-degree test's own (ALine – Point – DLine), here the complete graph with loops, which changes
the constant only.
Vectors and typed questions #
The bits of a low-degree vector, as an equivalence.
Equations
Instances For
The typed question of a question of the low-degree test, at role r and oracularized
question y: the low-degree half presents the test's question, the role half is y.
Equations
- MIPRE.Tailored.AnsRed.Typed.arQr sel rV r y q = ((r, q.ty), Fin.append y (MIPRE.Tailored.AnsRed.Typed.ldBits t ht j ((MIPRE.Tailored.AnsRed.Typed.regs j).embedQ sel q)))
Instances For
The question of type τ of the sample the registers of the low-degree vector w carry.
Equations
- MIPRE.Tailored.AnsRed.Typed.ldq sel τ w = MIPRE.LIDT.CL.Sample.question hM ((MIPRE.Tailored.AnsRed.Typed.regs j).sampleOf sel τ w) τ
Instances For
The questions of an answer-reduced sampler #
The oracularized question of role r at the seed z of the input sampler.
Equations
- MIPRE.Tailored.AnsRed.Typed.oq V n r z = ((MIPRE.Tailored.AnsRed.Typed.inSeeded V n).oquestion r z).2
Instances For
The typed question at a seed: at the seed (z, w), the question of type (r, τ) of an
answer-reduced sampler is the typed question presenting the oracularized question of role r at
z and the low-degree test's question of type τ of the sample w carries.
The per-role low-degree strategies #
The low-degree check of the typed data is the test's predicate: at two typed questions of one role presenting questions of the test, an answer pair the typed data accepts reads, through the role's codewords, as an answer pair the seeded test accepts.
The per-role low-degree strategy at role r and oracularized question y: T played
through arQr and the reading decAns of the role's codewords, both players at role r. At the
seed z of the input sampler the oracularized question is oq r z: the seed itself for the
oracle, the original player's question for an isolated player.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The per-role failure is at most the average of T's failures at the typed questions of
the test's samples.
The typed failure, by type pair and seed #
T's failure at the typed questions of the type pair uv at the seed (z, w).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The typed failure is the average over the type pairs and the seeds (z, w) of T's
failure at the typed questions they determine.
Any set of type pairs inside the typed failure: the failures at an injective family of
type pairs, summed over the seeds, add up to at most 81 times the number of seeds times the
typed failure.
A single type pair inside the typed failure.
The per-role failures average to the typed failure #
The per-role failures average to at most 9 times the typed failure: a role's nine type
pairs are 1/9 of the 81, and on them the registers of a uniform vector carry a uniform
sample.