The class verifiers' sampler, for a polynomial-time family of samplers

The sampler of the class verifiers: the PolyVerifier that puts an r.e. language in MIP*_{1,1/2}(2,1) (Paper/ClassVerifier.lean), and the polynomial-time tailored verifier that puts it in TMIP* (MIPRE/Tailored/ClassVerifier.lean). It is stated for any family of samplers λ ↦ S^λ of a level ℓ whose programs are computed from λ in polynomial time and which run within a polynomial in n + λ (SamplerFamily). A GapCompression supplies one at level 7 (GapCompression.samplerFamily), a tailored gap compression one at its own level.

On (z, r), for a polynomial-time reduction R to halting and the parameter λ(z) = Λ₀ + 4|R z| of lem:lambda (lamz), the sampler sampProg computes M = R z, λ(z) and the program of S^{λ(z)} (A1); asks it its dimension s at the fixed index n₀ through the universal machine (runUK); converts s to unary (unaryStage); takes the first s bits r' of the seed and asks S^{λ(z)} the two marginals at r' (A2, A3, runUK). sampProg_runs: at a level ℓ ≥ 1 it halts with the question pair of S^{λ(z)} at the point r' within sampB (|z| + |r|), a polynomially bounded function (polyBounded_sampB). At level 0 the marginal queries say nothing, but there the questions are empty (CL.Sampler.dim_eq_zero_of_level_zero): classSampler outputs the empty pair at level 0 and is sampProg above it.

The question distribution. A PolyVerifier whose sampler does this on the seeds of length B z (Samples) pushes the uniform seed forward to the distribution of S^{λ(z)} at n₀, on the questions embedded as bit strings (game_μ_qEmb), and its game has no weight elsewhere (game_support): the seeds producing a question pair are the extensions of the points of 𝔽₂^s producing it, each in 2^{B - s} ways (seedCount_eq).

theorem MIPRE.CL.Sampler.dim_eq_zero_of_level_zero (S : Sampler 0) (n : ℕ) : S.dim n = 0

At level 0 the questions are empty: the CL function of level 0 is the zero map, which is exactly on the empty set only.

The parameter

def MIPRE.Halting.lamz (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z : Cost.BitStr) : ℕ

The parameter of the input z: Λ₀ + 4|R z|.

Equations

• MIPRE.Halting.lamz Λ₀ R z = Λ₀ + 4 * MIPRE.Cost.esize (R.toFun z)

noncomputable def MIPRE.Halting.lamB (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : ℕ

The parameter, in the total input length m.

Equations

• MIPRE.Halting.lamB Λ₀ R m = Λ₀ + 4 * Polynomial.eval (4 * m + 1) R.timeBound

theorem MIPRE.Halting.lamz_le (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z : Cost.BitStr) (m : ℕ) (hm : List.length z ≤ m) : lamz Λ₀ R z ≤ lamB Λ₀ R m

theorem MIPRE.Halting.polyBounded_lamB (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyBounded (lamB Λ₀ R)

The parameter's bound lamB is polynomial.

def MIPRE.Halting.unB (D : ℕ) : ℕ

The cost of the binary-to-unary conversion, monotone in the number.

Equations

• MIPRE.Halting.unB D = (D + 2) * ((D + 1) * (4 * D + 14) + 7 * (4 * D + 1) + 8 * D + 90)

theorem MIPRE.Halting.unCost_le {d D : ℕ} (hd : d ≤ D) : (d.size + 2) * ((d + 1) * (4 * d + 14) + 7 * Cost.esize d + 8 * d + 90) ≤ unB D

Families of samplers

structure MIPRE.Halting.SamplerFamily (ℓ : ℕ) : Type

A polynomial-time family of samplers: samplers S^λ of level ℓ, their programs computed from λ in polynomial time, running within poly(n + λ) at degree deg, of dimension at most poly(n + λ).

• sampler : ℕ → CL.Sampler ℓ
• samplerProg : Cost.PolyTimeFun ℕ Cost.Prog
• samplerProg_eq (lam : ℕ) : self.samplerProg.toFun lam = (self.sampler lam).prog
• bound : Polynomial ℕ
• deg : ℕ
• sampler_time (lam n : ℕ) : (self.sampler lam).TimeBoundAt n (Polynomial.eval (n + lam) self.bound) self.deg
• sampler_dim (lam n : ℕ) : (self.sampler lam).dim n ≤ Polynomial.eval (n + lam) self.bound

noncomputable def MIPRE.Halting.SamplerFamily.queryF (ℓ n₀ : ℕ) (w : Player) : Cost.PolyTimeFun Cost.BitStr Cost.Data

The marginal query of player w at the level ℓ and the index n₀, as data.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.Halting.SamplerFamily.queryF_apply (ℓ n₀ : ℕ) (w : Player) (z : Cost.BitStr) : (queryF ℓ n₀ w).toFun z = Cost.encode (n₀, CL.Sampler.Query.marginal w ℓ z)

def MIPRE.Halting.SamplerFamily.qdim (n₀ : ℕ) : Cost.Data

The dimension query at the index n₀, as data.

Equations

• MIPRE.Halting.SamplerFamily.qdim n₀ = MIPRE.Cost.encode (n₀, MIPRE.CL.Sampler.Query.dimension)

theorem MIPRE.Halting.SamplerFamily.sampler_run_bounded {ℓ : ℕ} (S : CL.Sampler ℓ) {n T k : ℕ} (hb : S.TimeBoundAt n T k) (q : CL.Sampler.Query) {r : Cost.Data} {t : ℕ} (h : S.prog.Runs (Cost.encode (n, q)) r t) : ∃ t' ≤ T * ((Cost.encode q).size + 1) ^ k, S.prog.Runs (Cost.encode (n, q)) r t'

A run of a sampler on a query is within its time bound.

The sampler and its pieces

@[reducible, inline]

noncomputable abbrev MIPRE.Halting.SamplerFamily.Sz {ℓ : ℕ} (F : SamplerFamily ℓ) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z : Cost.BitStr) : CL.Sampler ℓ

The sampler of the input z: S^{λ(z)}.

Equations

• F.Sz Λ₀ R z = F.sampler (MIPRE.Halting.lamz Λ₀ R z)

noncomputable def MIPRE.Halting.SamplerFamily.dimz {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z : Cost.BitStr) : ℕ

The dimension of its questions at the index n₀.

Equations

• F.dimz n₀ Λ₀ R z = (F.Sz Λ₀ R z).dim n₀

noncomputable def MIPRE.Halting.SamplerFamily.qOf {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (w : Player) (z r : Cost.BitStr) : Cost.BitStr

Player w's question on the seed r, on the input z: the marginal of S^{λ(z)} at the first dimz z bits of r.

Equations

• F.qOf n₀ Λ₀ R w z r = MIPRE.CL.toBits (((F.Sz Λ₀ R z).cl n₀ w).eval (MIPRE.CL.ofBits (F.dimz n₀ Λ₀ R z) (List.take (F.dimz n₀ Λ₀ R z) r)))

theorem MIPRE.Halting.SamplerFamily.qOf_length {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (w : Player) (z r : Cost.BitStr) : List.length (F.qOf n₀ Λ₀ R w z r) = F.dimz n₀ Λ₀ R z

noncomputable def MIPRE.Halting.SamplerFamily.spF {ℓ : ℕ} (F : SamplerFamily ℓ) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr) Cost.Prog

(z, r) ↦ ComputeSampler(λ(z)).

Equations

• F.spF Λ₀ R = F.samplerProg.comp ((MIPRE.Halting.lamF Λ₀).comp (R.comp MIPRE.Cost.PolyTimeFun.fst))

theorem MIPRE.Halting.SamplerFamily.spF_apply {ℓ : ℕ} (F : SamplerFamily ℓ) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z r : Cost.BitStr) : (F.spF Λ₀ R).toFun (z, r) = (F.Sz Λ₀ R z).prog

noncomputable def MIPRE.Halting.SamplerFamily.A1 {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr) ((Cost.Prog × Cost.Data) × Cost.Prog × Cost.BitStr)

Stage 1: from (z, r), the pair (S, dimension) to run and the state (S, r).

Equations

• F.A1 n₀ Λ₀ R = ((F.spF Λ₀ R).pair (MIPRE.Cost.PolyTimeFun.const (MIPRE.Halting.SamplerFamily.qdim n₀))).pair ((F.spF Λ₀ R).pair MIPRE.Cost.PolyTimeFun.snd)

theorem MIPRE.Halting.SamplerFamily.A1_apply {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z r : Cost.BitStr) : (F.A1 n₀ Λ₀ R).toFun (z, r) = (((F.Sz Λ₀ R z).prog, qdim n₀), (F.Sz Λ₀ R z).prog, r)

noncomputable def MIPRE.Halting.SamplerFamily.A2 {ℓ : ℕ} (n₀ : ℕ) : Cost.PolyTimeFun ((Cost.Prog × Cost.BitStr) × Cost.Unary) ((Cost.Prog × Cost.Data) × Cost.Prog × Cost.BitStr)

Stage 2: from ((S, r), s) with s in unary, the pair (S, marginal A (r.take s)) to run and the state (S, r.take s).

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Halting.SamplerFamily.A2_apply {ℓ : ℕ} (n₀ : ℕ) (sp : Cost.Prog) (r : Cost.BitStr) (u : Cost.Unary) : (A2 n₀).toFun ((sp, r), u) = ((sp, Cost.encode (n₀, CL.Sampler.Query.marginal Player.alice ℓ (List.take (List.length u) r))), sp, List.take (List.length u) r)

noncomputable def MIPRE.Halting.SamplerFamily.A3 {ℓ : ℕ} (n₀ : ℕ) : Cost.PolyTimeFun ((Cost.Prog × Cost.BitStr) × Cost.BitStr) ((Cost.Prog × Cost.Data) × Cost.BitStr)

Stage 3: from ((S, r'), x), the pair (S, marginal B r') to run and the state x.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Halting.SamplerFamily.A3_apply {ℓ : ℕ} (n₀ : ℕ) (sp : Cost.Prog) (z' x : Cost.BitStr) : (A3 n₀).toFun ((sp, z'), x) = ((sp, Cost.encode (n₀, CL.Sampler.Query.marginal Player.bob ℓ z')), x)

noncomputable def MIPRE.Halting.SamplerFamily.sampProg {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ : ℕ) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.Prog

The sampler of the class verifier.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Halting.SamplerFamily.sampProg_wellScoped {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ : ℕ) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.Prog.WellScoped 1 (F.sampProg n₀ U Λ₀ R)

The costs

noncomputable def MIPRE.Halting.SamplerFamily.dimB {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : ℕ

The family's bound poly(n₀, λ), in the total input length m: bounds the dimension and the times.

Equations

• F.dimB n₀ Λ₀ R m = Polynomial.eval (n₀ + MIPRE.Halting.lamB Λ₀ R m) F.bound

noncomputable def MIPRE.Halting.SamplerFamily.T1B {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : ℕ

Stage 1's cost.

Equations

• F.T1B n₀ Λ₀ R m = Polynomial.eval (4 * m + 3) (F.A1 n₀ Λ₀ R).timeBound

noncomputable def MIPRE.Halting.SamplerFamily.R1B {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ : ℕ) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : ℕ

The first universal call's cost.

Equations

• F.R1B n₀ U Λ₀ R m = 2 * F.T1B n₀ Λ₀ R m + (4 * F.dimB n₀ Λ₀ R m + 1) + Polynomial.eval (2 * F.T1B n₀ Λ₀ R m + F.dimB n₀ Λ₀ R m * (F.T1B n₀ Λ₀ R m + 1) ^ F.deg) U.bound + 8

noncomputable def MIPRE.Halting.SamplerFamily.UnB {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ : ℕ) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : ℕ

The conversion's cost.

Equations

• F.UnB n₀ U Λ₀ R m = F.R1B n₀ U Λ₀ R m + (4 * F.dimB n₀ Λ₀ R m + 1) + MIPRE.Halting.unB (F.dimB n₀ Λ₀ R m) + 5

noncomputable def MIPRE.Halting.SamplerFamily.T2B {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ : ℕ) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : ℕ

Stage 2's cost.

Equations

• F.T2B n₀ U Λ₀ R m = Polynomial.eval (F.UnB n₀ U Λ₀ R m) (MIPRE.Halting.SamplerFamily.A2 n₀).timeBound

noncomputable def MIPRE.Halting.SamplerFamily.R2B {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ : ℕ) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : ℕ

The second universal call's cost.

Equations

• F.R2B n₀ U Λ₀ R m = 2 * F.T2B n₀ U Λ₀ R m + (4 * F.dimB n₀ Λ₀ R m + 1) + Polynomial.eval (2 * F.T2B n₀ U Λ₀ R m + F.dimB n₀ Λ₀ R m * (F.T2B n₀ U Λ₀ R m + 1) ^ F.deg) U.bound + 8

noncomputable def MIPRE.Halting.SamplerFamily.T3B {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ : ℕ) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : ℕ

Stage 3's cost.

Equations

• F.T3B n₀ U Λ₀ R m = Polynomial.eval (F.R2B n₀ U Λ₀ R m) (MIPRE.Halting.SamplerFamily.A3 n₀).timeBound

noncomputable def MIPRE.Halting.SamplerFamily.R3B {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ : ℕ) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : ℕ

The third universal call's cost.

Equations

• F.R3B n₀ U Λ₀ R m = 2 * F.T3B n₀ U Λ₀ R m + (4 * F.dimB n₀ Λ₀ R m + 1) + Polynomial.eval (2 * F.T3B n₀ U Λ₀ R m + F.dimB n₀ Λ₀ R m * (F.T3B n₀ U Λ₀ R m + 1) ^ F.deg) U.bound + 8

noncomputable def MIPRE.Halting.SamplerFamily.sampB {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ : ℕ) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : ℕ

The sampler's cost, in the total input length.

Equations

• F.sampB n₀ U Λ₀ R m = 2 * (F.T1B n₀ Λ₀ R m + F.R1B n₀ U Λ₀ R m + F.UnB n₀ U Λ₀ R m + F.T2B n₀ U Λ₀ R m + F.R2B n₀ U Λ₀ R m + F.T3B n₀ U Λ₀ R m) + F.R3B n₀ U Λ₀ R m + 18

theorem MIPRE.Halting.SamplerFamily.dimz_le {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z : Cost.BitStr) (m : ℕ) (hm : List.length z ≤ m) : F.dimz n₀ Λ₀ R z ≤ F.dimB n₀ Λ₀ R m

theorem MIPRE.Halting.SamplerFamily.sampProg_runs {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ : ℕ) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (hℓ : 1 ≤ ℓ) (z r : Cost.BitStr) (hd : F.dimz n₀ Λ₀ R z ≤ List.length r) : ∃ t ≤ F.sampB n₀ U Λ₀ R (List.length z + List.length r), (F.sampProg n₀ U Λ₀ R).Runs (Cost.encode (z, r)) (Cost.encode (F.qOf n₀ Λ₀ R Player.alice z r, F.qOf n₀ Λ₀ R Player.bob z r)) t

The sampler's run: on (z, r) with r at least dimz z long, it halts with the question pair of the seed within sampB (|z| + |r|).

The bounds are polynomial

theorem MIPRE.Halting.SamplerFamily.polyBounded_dimB {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyBounded (F.dimB n₀ Λ₀ R)

theorem MIPRE.Halting.SamplerFamily.polyBounded_T1B {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyBounded (F.T1B n₀ Λ₀ R)

theorem MIPRE.Halting.SamplerFamily.polyBounded_call {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ : ℕ) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) {T : ℕ → ℕ} (hT : Cost.PolyBounded T) : Cost.PolyBounded fun (m : ℕ) => 2 * T m + (4 * F.dimB n₀ Λ₀ R m + 1) + Polynomial.eval (2 * T m + F.dimB n₀ Λ₀ R m * (T m + 1) ^ F.deg) U.bound + 8

The shape of the three universal calls' bounds.

theorem MIPRE.Halting.SamplerFamily.polyBounded_R1B {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ : ℕ) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyBounded (F.R1B n₀ U Λ₀ R)

theorem MIPRE.Halting.SamplerFamily.polyBounded_unB_dimB {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyBounded fun (m : ℕ) => unB (F.dimB n₀ Λ₀ R m)

theorem MIPRE.Halting.SamplerFamily.polyBounded_UnB {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ : ℕ) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyBounded (F.UnB n₀ U Λ₀ R)

theorem MIPRE.Halting.SamplerFamily.polyBounded_T2B {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ : ℕ) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyBounded (F.T2B n₀ U Λ₀ R)

theorem MIPRE.Halting.SamplerFamily.polyBounded_R2B {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ : ℕ) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyBounded (F.R2B n₀ U Λ₀ R)

theorem MIPRE.Halting.SamplerFamily.polyBounded_T3B {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ : ℕ) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyBounded (F.T3B n₀ U Λ₀ R)

theorem MIPRE.Halting.SamplerFamily.polyBounded_R3B {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ : ℕ) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyBounded (F.R3B n₀ U Λ₀ R)

theorem MIPRE.Halting.SamplerFamily.polyBounded_sampB {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ : ℕ) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyBounded (F.sampB n₀ U Λ₀ R)

At every level

noncomputable def MIPRE.Halting.SamplerFamily.classSampler {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ : ℕ) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.Prog

The class sampler, at every level: sampProg at the levels ℓ ≥ 1, and at level 0, where the questions are empty, the program outputting the empty pair.

Equations

• F.classSampler n₀ U Λ₀ R = if 1 ≤ ℓ then F.sampProg n₀ U Λ₀ R else MIPRE.Cost.Prog.const (MIPRE.Cost.encode ([], []))

theorem MIPRE.Halting.SamplerFamily.classSampler_wellScoped {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ : ℕ) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.Prog.WellScoped 1 (F.classSampler n₀ U Λ₀ R)

noncomputable def MIPRE.Halting.SamplerFamily.classB {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ : ℕ) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (m : ℕ) : ℕ

The class sampler's cost, in the total input length.

Equations

• F.classB n₀ U Λ₀ R m = F.sampB n₀ U Λ₀ R m + (MIPRE.Cost.encode ([], [])).size

theorem MIPRE.Halting.SamplerFamily.classSampler_runs {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ : ℕ) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z r : Cost.BitStr) (hd : F.dimz n₀ Λ₀ R z ≤ List.length r) : ∃ t ≤ F.classB n₀ U Λ₀ R (List.length z + List.length r), (F.classSampler n₀ U Λ₀ R).Runs (Cost.encode (z, r)) (Cost.encode (F.qOf n₀ Λ₀ R Player.alice z r, F.qOf n₀ Λ₀ R Player.bob z r)) t

The class sampler's run, at every level: on (z, r) with r at least dimz z long, it halts with the question pair of the seed within classB (|z| + |r|).

theorem MIPRE.Halting.SamplerFamily.polyBounded_classB {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ : ℕ) (U : Cost.UniversalMachine) (Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) : Cost.PolyBounded (F.classB n₀ U Λ₀ R)

The question distribution

@[reducible, inline]

abbrev MIPRE.Halting.SamplerFamily.Qz {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (z : Cost.BitStr) : Type

The questions of S^{λ(z)} at the index n₀.

Equations

• F.Qz n₀ Λ₀ R z = (Fin ((F.Sz Λ₀ R z).dim n₀) → MIPRE.CL.𝔽₂)

def MIPRE.Halting.SamplerFamily.Samples {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) (V : PolyVerifier) : Prop

V samples S^{λ(z)} at n₀: on every input z and every seed r of length B z, its sampler halts within P(|z| + |r|) with the question pair of the seed.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Halting.SamplerFamily.dimz_le_B {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) {V : PolyVerifier} (hdim : ∀ (m : ℕ), F.dimB n₀ Λ₀ R m ≤ Polynomial.eval m V.bound) (z : Cost.BitStr) : F.dimz n₀ Λ₀ R z ≤ V.B z

theorem MIPRE.Halting.SamplerFamily.samples_of_runs {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) {V : PolyVerifier} (hdim : ∀ (m : ℕ), F.dimB n₀ Λ₀ R m ≤ Polynomial.eval m V.bound) {p : Cost.Prog} {T : ℕ → ℕ} (hp : ∀ (z r : Cost.BitStr), F.dimz n₀ Λ₀ R z ≤ List.length r → ∃ t ≤ T (List.length z + List.length r), p.Runs (Cost.encode (z, r)) (Cost.encode (F.qOf n₀ Λ₀ R Player.alice z r, F.qOf n₀ Λ₀ R Player.bob z r)) t) (hS : V.sampler = p) (hT : ∀ (m : ℕ), T m ≤ Polynomial.eval m V.bound) : F.Samples n₀ Λ₀ R V

A sampler running as the class sampler does, within a bound below P, samples.

theorem MIPRE.Halting.SamplerFamily.Samples.samplerRuns {ℓ : ℕ} {F : SamplerFamily ℓ} {n₀ Λ₀ : ℕ} {R : Cost.PolyTimeFun Cost.BitStr Cost.Prog} {V : PolyVerifier} (hS : F.Samples n₀ Λ₀ R V) (hdim : ∀ (m : ℕ), F.dimB n₀ Λ₀ R m ≤ Polynomial.eval m V.bound) (z : Cost.BitStr) : V.SamplerRuns z

A sampler that samples meets the sampler's clause of efficiency.

theorem MIPRE.Halting.SamplerFamily.questions_eq {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) {V : PolyVerifier} (hS : F.Samples n₀ Λ₀ R V) (hdim : ∀ (m : ℕ), F.dimB n₀ Λ₀ R m ≤ Polynomial.eval m V.bound) (z r : Cost.BitStr) (hr : List.length r = V.B z) : V.questions z r = (⟨F.qOf n₀ Λ₀ R Player.alice z r, ⋯⟩, ⟨F.qOf n₀ Λ₀ R Player.bob z r, ⋯⟩)

The question pair of a seed of the right length.

noncomputable def MIPRE.Halting.SamplerFamily.qEmb {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) {V : PolyVerifier} (hdim : ∀ (m : ℕ), F.dimB n₀ Λ₀ R m ≤ Polynomial.eval m V.bound) (z : Cost.BitStr) : F.Qz n₀ Λ₀ R z ↪ Verifier.Answers (V.B z)

The embedding of the questions of S^{λ(z)} into the strings of length at most B z.

Equations

• F.qEmb n₀ Λ₀ R hdim z = { toFun := fun (v : F.Qz n₀ Λ₀ R z) => ⟨MIPRE.CL.toBits v, ⋯⟩, inj' := ⋯ }

@[simp]

theorem MIPRE.Halting.SamplerFamily.qEmb_apply {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) {V : PolyVerifier} (hdim : ∀ (m : ℕ), F.dimB n₀ Λ₀ R m ≤ Polynomial.eval m V.bound) (z : Cost.BitStr) (v : F.Qz n₀ Λ₀ R z) : ↑((F.qEmb n₀ Λ₀ R hdim z) v) = CL.toBits v

theorem MIPRE.Halting.SamplerFamily.seedCount_eq {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) {V : PolyVerifier} (hS : F.Samples n₀ Λ₀ R V) (hdim : ∀ (m : ℕ), F.dimB n₀ Λ₀ R m ≤ Polynomial.eval m V.bound) (z : Cost.BitStr) (x y : F.Qz n₀ Λ₀ R z) : V.seedCount z ((F.qEmb n₀ Λ₀ R hdim z) x) ((F.qEmb n₀ Λ₀ R hdim z) y) = {v : F.Qz n₀ Λ₀ R z | ((F.Sz Λ₀ R z).cl n₀ Player.alice).eval v = x ∧ ((F.Sz Λ₀ R z).cl n₀ Player.bob).eval v = y}.card * 2 ^ (V.B z - F.dimz n₀ Λ₀ R z)

The number of seeds producing a given question pair: a count over 𝔽₂^{s} times 2 ^ (B - s).

theorem MIPRE.Halting.SamplerFamily.game_μ_qEmb {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) {V : PolyVerifier} (hS : F.Samples n₀ Λ₀ R V) (hdim : ∀ (m : ℕ), F.dimB n₀ Λ₀ R m ≤ Polynomial.eval m V.bound) (z : Cost.BitStr) (x y : F.Qz n₀ Λ₀ R z) : (V.game z).μ ((F.qEmb n₀ Λ₀ R hdim z) x) ((F.qEmb n₀ Λ₀ R hdim z) y) = (F.Sz Λ₀ R z).dist n₀ x y

The distribution of the game, on the embedded questions, is the sampler's.

theorem MIPRE.Halting.SamplerFamily.game_support {ℓ : ℕ} (F : SamplerFamily ℓ) (n₀ Λ₀ : ℕ) (R : Cost.PolyTimeFun Cost.BitStr Cost.Prog) {V : PolyVerifier} (hS : F.Samples n₀ Λ₀ R V) (hdim : ∀ (m : ℕ), F.dimB n₀ Λ₀ R m ≤ Polynomial.eval m V.bound) (z : Cost.BitStr) (x' y' : Verifier.Answers (V.B z)) (h : (V.game z).μ x' y' ≠ 0) : (∃ (x : F.Qz n₀ Λ₀ R z), (F.qEmb n₀ Λ₀ R hdim z) x = x') ∧ ∃ (y : F.Qz n₀ Λ₀ R z), (F.qEmb n₀ Λ₀ R hdim z) y = y'

The distribution of the game is supported on the embedded questions.

def MIPRE.GapCompression.samplerFamily (G : GapCompression) : Halting.SamplerFamily 7

The compressed samplers of a gap compression.

Equations

• G.samplerFamily = { sampler := G.sampler, samplerProg := G.samplerProg, samplerProg_eq := ⋯, bound := G.bound, deg := G.deg, sampler_time := ⋯, sampler_dim := ⋯ }