Soundness of the answer-reduced game #
Slice P4e of planning/aldous-lyons-track.md: the soundness clause of
prop:completeness_soundness_combi_ans_red (II:10487), at one index of the input. If the
answer-reduced game presented by the typed data tdata, on any answer-reduced sampler, has
val* > 1 - ε, then val*(𝒱_n) ≥ 1 - 24 √(errAR (16⁹ ε)) (valStar_ar_sound).
The chain:
- the presented game's
val*is at most the detyped game's (valStar_presented_le), whose typed game hasval*above1 - 16⁹ ε(CL.Detyping.quantumValue_typedGame_ge); - a projective strategy
Tof a tensor-product model near that value, in which the seeded low-degree test is sound (LIDT.Simul.approxSoundIn_tensor); - the decoded strategy of
SoundDecoded, which fails the typed oracularized game of the input at mosterrARofT's failure (one_sub_value_decoded_le): the nine pairs of roles at a seed (sum_roles_condFail_le), summed over the seeds; - oracularization's soundness (
ValueModel.OracularSound), the typed oracularized game being at most the oracularization (SeededGame.val_typedGame_le), and the oracularized input's game being the input's (inCL_toGame).
errAR is explicit in the errors of the seeded test's soundness (dS) and the field size; P4i
bounds it by the contract's AnswerReduction.delta.
The error #
noncomputable def
MIPRE.Tailored.AnsRed.Typed.errAR
(t : ℕ)
(ht : 1 ≤ t)
(j d : ℕ)
(L : PcpDims)
(θ : ℝ)
:
The error of the answer-reduced game's soundness, at typed failure θ: the outcomes of the
oracle that are not block-local or pass the proof check sparsely, the two polynomial
measurements' disagreements at each role, and the agreement of the isolated roles' polynomials
with the oracle's.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MIPRE.Tailored.AnsRed.Typed.deltaSim_mono
{q m d r : ℕ}
{x y : ℝ}
(hx : 0 ≤ x)
(hxy : x ≤ y)
:
The oracularized input #
theorem
MIPRE.Tailored.AnsRed.Typed.roleFamily_liftedCl_eval
{ℓV : ℕ}
(V : TailoredVerifier ℓV)
(n : ℕ)
(r : Role)
(z : V.Questions n)
:
The oracularized input's game is the input's.
The decoded strategy's failure #
theorem
MIPRE.Tailored.AnsRed.Typed.sum_roles_condFail_le
{𝒞 : Type u_1}
{𝒜 : Type u_2}
{ℬ : Type u_3}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
{M : BipartiteModel 𝒞 𝒜 ℬ}
{t : ℕ}
{ht : 1 ≤ t}
{j d : ℕ}
{hM : 2 ^ j ∣ Fintype.card (Fq t ht)}
{sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM}
{L : PcpDims}
{hLM : L.m ≤ 2 ^ j}
{ℓV : ℕ}
{V : TailoredVerifier ℓV}
{n : ℕ}
{Cc : V.Questions n → SAT.Circuit}
{hm : ∀ (z : V.Questions n), (Cc z).inputs + (Cc z).size = L.m}
{ℓ : ℕ}
{P : Bool → Role × LIDT.CL.Ty → CL.CLFun (ZMod 2) (Fin (V.sampler.dim n + D j * t)) ℓ}
{B : ℕ}
(T : M.ProjStrat (arGame d hM sel L hLM V n Cc hm P B))
(hL : LIDT.Simul.SoundIn M)
(hd : 1 ≤ d)
(z : V.Questions n)
:
∑ u : Role, ∑ v : Role, M.condFail (oGameT V n) (MAd T ⋯ hd) (MBd T ⋯ hd) (u, oq V n u z) (v, oq V n v z) ≤ 3 * gcA T ⋯ hd z + 3 * gcB T ⋯ hd z + M.dis (GA T ⋯ hd Role.oracle z) (GB T ⋯ hd Role.oracle z) + M.dis (GA T ⋯ hd Role.alice (oq V n Role.alice z)) (GB T ⋯ hd Role.alice (oq V n Role.alice z)) + M.dis (GA T ⋯ hd Role.bob (oq V n Role.bob z)) (GB T ⋯ hd Role.bob (oq V n Role.bob z)) + (M.dis (POVMIn.map (restr L Role.alice) (GA T ⋯ hd Role.oracle z)) (GB T ⋯ hd Role.alice (oq V n Role.alice z)) + M.dis (POVMIn.map (restr L Role.bob) (GA T ⋯ hd Role.oracle z)) (GB T ⋯ hd Role.bob (oq V n Role.bob z)) + M.dis (GA T ⋯ hd Role.alice (oq V n Role.alice z)) (POVMIn.map (restr L Role.alice) (GB T ⋯ hd Role.oracle z)) + M.dis (GA T ⋯ hd Role.bob (oq V n Role.bob z)) (POVMIn.map (restr L Role.bob) (GB T ⋯ hd Role.oracle z)))
The decoded strategy's failure at a seed, over the nine ordered pairs of roles.
theorem
MIPRE.Tailored.AnsRed.Typed.one_sub_value_decoded_le
{𝒞 : Type u_1}
{𝒜 : Type u_2}
{ℬ : Type u_3}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
{M : BipartiteModel 𝒞 𝒜 ℬ}
{t : ℕ}
{ht : 1 ≤ t}
{j d : ℕ}
{hM : 2 ^ j ∣ Fintype.card (Fq t ht)}
{sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM}
{L : PcpDims}
{hLM : L.m ≤ 2 ^ j}
{ℓV : ℕ}
{V : TailoredVerifier ℓV}
{n : ℕ}
{Cc : V.Questions n → SAT.Circuit}
{hm : ∀ (z : V.Questions n), (Cc z).inputs + (Cc z).size = L.m}
{ℓ : ℕ}
{P : Bool → Role × LIDT.CL.Ty → CL.CLFun (ZMod 2) (Fin (V.sampler.dim n + D j * t)) ℓ}
{B : ℕ}
(T : M.ProjStrat (arGame d hM sel L hLM V n Cc hm P B))
(hL : LIDT.Simul.SoundIn M)
(hd : 1 ≤ d)
{prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)}
{Tt : ℕ}
(H : HonestHyp L V n prm Cc Tt)
(hP : ArSampler hM sel V n P)
(hq : 2 * ((2 ^ j + 1) * d) ≤ Fintype.card (Fq t ht))
(hτ : 2 * (L.m * chkDeg 5 d) ≤ Fintype.card (Fq t ht))
:
The decoded strategy fails the typed oracularized game at most errAR of the typed
failure, once the field has 2 (M + 1) d and 2 m (5 + 6(d + 1)) elements.
The soundness of the answer-reduced game #
An answer as one of the bounded answers, when its length allows.
Equations
- MIPRE.Tailored.AnsRed.Typed.decB B a = if h : List.length a ≤ B then ⟨a, h⟩ else ⟨[], ⋯⟩
Instances For
theorem
MIPRE.Tailored.AnsRed.Typed.valStar_presented_ar_le
{t : ℕ}
{ht : 1 ≤ t}
{j d : ℕ}
{hM : 2 ^ j ∣ Fintype.card (Fq t ht)}
{sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM}
{L : PcpDims}
{hLM : L.m ≤ 2 ^ j}
{ℓV : ℕ}
{V : TailoredVerifier ℓV}
{n : ℕ}
{Cc : V.Questions n → SAT.Circuit}
{hm : ∀ (z : V.Questions n), (Cc z).inputs + (Cc z).size = L.m}
{ℓ : ℕ}
{P : Bool → Role × LIDT.CL.Ty → CL.CLFun (ZMod 2) (Fin (V.sampler.dim n + D j * t)) ℓ}
{B : ℕ}
(hB : ∀ (u : Role × LIDT.CL.Ty), len t j d L u ≤ B)
:
(presented arGraph (CL.Detyping.game arGraph P (arDt d hM sel L hLM V n Cc hm B))
(tdata t ht j d L (V.sampler.dim n) sel hLM (circOf L V n Cc hm))).valStar ≤ quantumValue (CL.Detyping.game arGraph P (arDt d hM sel L hLM V n Cc hm B))
The presented game's value is at most the detyped game's.
theorem
MIPRE.Tailored.AnsRed.Typed.valStar_ar_sound
{t : ℕ}
{ht : 1 ≤ t}
{j d : ℕ}
{hM : 2 ^ j ∣ Fintype.card (Fq t ht)}
{sel : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM}
{L : PcpDims}
{hLM : L.m ≤ 2 ^ j}
{ℓV : ℕ}
{V : TailoredVerifier ℓV}
{n : ℕ}
{Cc : V.Questions n → SAT.Circuit}
{hm : ∀ (z : V.Questions n), (Cc z).inputs + (Cc z).size = L.m}
{ℓ : ℕ}
{P : Bool → Role × LIDT.CL.Ty → CL.CLFun (ZMod 2) (Fin (V.sampler.dim n + D j * t)) ℓ}
{B : ℕ}
{prm : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)}
{Tt : ℕ}
(H : HonestHyp L V n prm Cc Tt)
(hd : 1 ≤ d)
(hP : ArSampler hM sel V n P)
(hℓ : 0 < ℓ)
(hB : ∀ (u : Role × LIDT.CL.Ty), len t j d L u ≤ B)
(hq : 2 * ((2 ^ j + 1) * d) ≤ Fintype.card (Fq t ht))
(hτ : 2 * (L.m * chkDeg 5 d) ≤ Fintype.card (Fq t ht))
{ε : ℝ}
(hε : 0 < ε)
(h :
1 - ε < (presented arGraph (CL.Detyping.game arGraph P (arDt d hM sel L hLM V n Cc hm B))
(tdata t ht j d L (V.sampler.dim n) sel hLM (circOf L V n Cc hm))).valStar)
:
The soundness of the answer-reduced game (prop:completeness_soundness_combi_ans_red,
item 2): if the game presented by the typed data on an answer-reduced sampler has
val* > 1 - ε, then val*(𝒱_n) ≥ 1 - 24 √(errAR (16⁹ ε)), once the field has 2 (M + 1) d and
2 m (5 + 6(d + 1)) elements.