Soundness of the answer-reduced game: the polynomial measurements #
The soundness of the seeded low-degree test in the model (LIDT.Simul.SoundIn), applied to each
per-role strategy of SoundSetup (II:10623, the first perturbation): at each role r and
oracularized question y, projective measurements GA r y, GB r y of tuples of polynomials of
individual degree at most d in M = 2^j variables, one per codeword of the role, whose
evaluations at a uniform point are consistent with the role's point answers, and which are
consistent with each other, up to δ_sim of the per-role failure (extR_spec).
Averaged over the seeds of the input sampler, the error is at most δ_sim of 9 times the typed
failure (sum_deltaSimR_le), by Jensen's inequality (LIDT.Simul.sum_deltaSim_le).
@[reducible, inline]
The outcomes of a role's polynomial measurement: a polynomial of individual degree at most
d in 2^j variables for each of the role's codewords.
Equations
- MIPRE.Tailored.AnsRed.Typed.PolyR t ht j d L r = (Fin (MIPRE.Tailored.AnsRed.slotsOf L r).length → MIPRE.LIDT.LowIndDegPoly)
Instances For
@[reducible, inline]
noncomputable abbrev
MIPRE.Tailored.AnsRed.Typed.dS
(t : ℕ)
(ht : 1 ≤ t)
(j d : ℕ)
(L : PcpDims)
(r : Role)
(ε : ℝ)
:
The error of the seeded test's soundness at a role, as a function of its failure.
Equations
- MIPRE.Tailored.AnsRed.Typed.dS t ht j d L r ε = MIPRE.LIDT.Simul.deltaSim (Fintype.card (MIPRE.Tailored.AnsRed.Typed.Fq t ht)) (2 ^ j) d (MIPRE.Tailored.AnsRed.slotsOf L r).length ε
Instances For
noncomputable def
MIPRE.Tailored.AnsRed.Typed.epsR
{𝒞 : 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))
(r : Role)
(y : V.Questions n)
:
The failure of the per-role strategy at role r and oracularized question y.
Equations
- MIPRE.Tailored.AnsRed.Typed.epsR T r y = 1 - (MIPRE.Tailored.AnsRed.Typed.roleStrat T r y).value
Instances For
theorem
MIPRE.Tailored.AnsRed.Typed.epsR_nonneg
{𝒞 : 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))
(r : Role)
(y : V.Questions n)
:
theorem
MIPRE.Tailored.AnsRed.Typed.exists_extR
{𝒞 : 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)
(r : Role)
(y : V.Questions n)
:
∃ (GA : POVMIn (PolyR t ht j d L r) 𝒜) (GB : POVMIn (PolyR t ht j d L r) ℬ),
IsPVMIn GA.op ∧ IsPVMIn GB.op ∧ M.inconsistency (uniform (Fin (2 ^ j) → Fq t ht)) (LIDT.Simul.tuplePOVMAIn hM (roleStrat T r y))
(LIDT.Simul.evalTuplePOVMIn GB) ≤ dS t ht j d L r (epsR T r y) ∧ M.inconsistency (uniform (Fin (2 ^ j) → Fq t ht)) (LIDT.Simul.evalTuplePOVMIn GA)
(LIDT.Simul.tuplePOVMBIn hM (roleStrat T r y)) ≤ dS t ht j d L r (epsR T r y) ∧ (M.inconsistency (uniform Unit) (fun (x : Unit) => GA) fun (x : Unit) => GB) ≤ dS t ht j d L r (epsR T r y)
noncomputable def
MIPRE.Tailored.AnsRed.Typed.GA
{𝒞 : 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)
(r : Role)
(y : V.Questions n)
:
Alice's polynomial measurement at role r and oracularized question y.
Equations
- MIPRE.Tailored.AnsRed.Typed.GA T hL hd r y = ⋯.choose
Instances For
noncomputable def
MIPRE.Tailored.AnsRed.Typed.GB
{𝒞 : 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)
(r : Role)
(y : V.Questions n)
:
Bob's polynomial measurement at role r and oracularized question y.
Equations
- MIPRE.Tailored.AnsRed.Typed.GB T hL hd r y = ⋯.choose
Instances For
theorem
MIPRE.Tailored.AnsRed.Typed.extR_proj
{𝒞 : 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)
(r : Role)
(y : V.Questions n)
:
The polynomial measurements are projective.
theorem
MIPRE.Tailored.AnsRed.Typed.extR_spec
{𝒞 : 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)
(r : Role)
(y : V.Questions n)
:
M.inconsistency (uniform (Fin (2 ^ j) → Fq t ht)) (LIDT.Simul.tuplePOVMAIn hM (roleStrat T r y))
(LIDT.Simul.evalTuplePOVMIn (GB T ⋯ hd r y)) ≤ dS t ht j d L r (epsR T r y) ∧ M.inconsistency (uniform (Fin (2 ^ j) → Fq t ht)) (LIDT.Simul.evalTuplePOVMIn (GA T ⋯ hd r y))
(LIDT.Simul.tuplePOVMBIn hM (roleStrat T r y)) ≤ dS t ht j d L r (epsR T r y) ∧ (M.inconsistency (uniform Unit) (fun (x : Unit) => GA T ⋯ hd r y) fun (x : Unit) => GB T ⋯ hd r y) ≤ dS t ht j d L r (epsR T r y)
The three conclusions of the seeded test's soundness at role r and question y.
theorem
MIPRE.Tailored.AnsRed.Typed.sum_deltaSimR_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))
(hP : ArSampler hM sel V n P)
(r : Role)
:
The averaged error of the seeded test's soundness at a role: at most δ_sim of 9 times
the typed failure.