The product of a typed sampler and a directly answered one: the presentations

The answer-reduced sampler (sec:ar-verifier, ld_compiler.tex) is the direct sum of the oracularized sampler, whose queries are answered by a program, and the downsized PCP sampler, whose queries a polynomial-time function answers outright. This file is the CL half of that construction, for any two families of presentations on 𝔽₂^a and 𝔽₂^b:

• prodCL L P Q pads both to L levels and puts them side by side on 𝔽₂^{a + b}, the first a coordinates for P;
• its three queries, in bits, are the two halves' queries concatenated (toBits_eval_truncate_prodCL, toBits_mapOfPrefix_prodCL, indicatorBits_factorOfPrefix_prodCL);
• beyond a presentation's own level its marginal is its full evaluation, its stage map zero and its factor space empty (eval_truncate_of_le, mapOfPrefix_of_le, factorOfPrefix_of_le).

Beyond the level

theorem MIPRE.CL.CLFun.eval_truncate_of_le {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] {ℓ : ℕ} (P : CLFun F ι ℓ) {j : ℕ} (h : ℓ ≤ j) (x : ι → F) : (truncate j P).eval x = P.eval x

theorem MIPRE.CL.CLFun.mapOfPrefix_of_le {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] {ℓ : ℕ} (P : CLFun F ι ℓ) {k : ℕ} (h : ℓ ≤ k) (u : ι → F) : P.mapOfPrefix k u = 0

theorem MIPRE.CL.CLFun.factorOfPrefix_of_le {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] {ℓ : ℕ} (P : CLFun F ι ℓ) {k : ℕ} (h : ℓ ≤ k) (u : ι → F) : P.factorOfPrefix k u = ∅

Splitting vectors of 𝔽₂^{a + b}

def MIPRE.CL.leftPart {a b : ℕ} (x : Fin (a + b) → 𝔽₂) : Fin a → 𝔽₂

The first a coordinates.

Equations

• MIPRE.CL.leftPart x i = x (Fin.castAdd b i)

def MIPRE.CL.rightPart {a b : ℕ} (x : Fin (a + b) → 𝔽₂) : Fin b → 𝔽₂

The last b coordinates.

Equations

• MIPRE.CL.rightPart x i = x (Fin.natAdd a i)

@[simp]

theorem MIPRE.CL.leftPart_append {a b : ℕ} (v : Fin a → 𝔽₂) (w : Fin b → 𝔽₂) : leftPart (Fin.append v w) = v

@[simp]

theorem MIPRE.CL.rightPart_append {a b : ℕ} (v : Fin a → 𝔽₂) (w : Fin b → 𝔽₂) : rightPart (Fin.append v w) = w

theorem MIPRE.CL.toBits_append {a b : ℕ} (v : Fin a → 𝔽₂) (w : Fin b → 𝔽₂) : toBits (Fin.append v w) = toBits v ++ toBits w

theorem MIPRE.CL.toBits_eq_append {a b : ℕ} (x : Fin (a + b) → 𝔽₂) : toBits x = toBits (leftPart x) ++ toBits (rightPart x)

theorem MIPRE.CL.indicatorBits_eq_append {a b : ℕ} (S : Finset (Fin (a + b))) : indicatorBits S = indicatorBits (S.preimage (Fin.castAdd b) ⋯) ++ indicatorBits (S.preimage (Fin.natAdd a) ⋯)

theorem MIPRE.CL.leftPart_ofBits {a b : ℕ} (l : Cost.BitStr) : leftPart (ofBits (a + b) l) = ofBits a (List.take a l)

theorem MIPRE.CL.rightPart_ofBits {a b : ℕ} (l : Cost.BitStr) : rightPart (ofBits (a + b) l) = ofBits b (List.drop a l)

theorem MIPRE.CL.take_toBits {a b : ℕ} (x : Fin (a + b) → 𝔽₂) : List.take a (toBits x) = toBits (leftPart x)

theorem MIPRE.CL.drop_toBits {a b : ℕ} (x : Fin (a + b) → 𝔽₂) : List.drop a (toBits x) = toBits (rightPart x)

The product presentation

noncomputable def MIPRE.CL.CLFun.prodCL {a b ℓa ℓb : ℕ} (L : ℕ) (P : CLFun 𝔽₂ (Fin a) ℓa) (Q : CLFun 𝔽₂ (Fin b) ℓb) (ha : ℓa ≤ L) (hb : ℓb ≤ L) : CLFun 𝔽₂ (Fin (a + b)) L

P and Q padded to L levels, side by side on 𝔽₂^{a + b}: P on the first a coordinates.

Equations

• MIPRE.CL.CLFun.prodCL L P Q ha hb = MIPRE.CL.CLFun.reindex finSumFinEquiv ((MIPRE.CL.CLFun.liftTo Finset.univ L ha P).prod (MIPRE.CL.CLFun.liftTo Finset.univ L hb Q))

theorem MIPRE.CL.CLFun.ExactlyOn.prodCL {a b ℓa ℓb : ℕ} (L : ℕ) {P : CLFun 𝔽₂ (Fin a) ℓa} {Q : CLFun 𝔽₂ (Fin b) ℓb} (hP : P.ExactlyOn Finset.univ) (hQ : Q.ExactlyOn Finset.univ) (ha : ℓa ≤ L) (hb : ℓb ≤ L) : (CLFun.prodCL L P Q ha hb).ExactlyOn Finset.univ

theorem MIPRE.CL.CLFun.sumElim_reindex {a b : ℕ} (v : Fin a → 𝔽₂) (w : Fin b → 𝔽₂) : (reindexEquiv finSumFinEquiv) (Sum.elim v w) = Fin.append v w

theorem MIPRE.CL.CLFun.split_symm {a b : ℕ} (x : Fin (a + b) → 𝔽₂) : (reindexEquiv finSumFinEquiv).symm x = Sum.elim (leftPart x) (rightPart x)

theorem MIPRE.CL.CLFun.eval_truncate_prodCL {a b ℓa ℓb : ℕ} (L : ℕ) {P : CLFun 𝔽₂ (Fin a) ℓa} {Q : CLFun 𝔽₂ (Fin b) ℓb} (hP : P.ExactlyOn Finset.univ) (hQ : Q.ExactlyOn Finset.univ) (ha : ℓa ≤ L) (hb : ℓb ≤ L) (j : ℕ) (x : Fin (a + b) → 𝔽₂) : (truncate j (prodCL L P Q ha hb)).eval x = Fin.append ((truncate j P).eval (leftPart x)) ((truncate j Q).eval (rightPart x))

theorem MIPRE.CL.CLFun.toBits_eval_truncate_prodCL {a b ℓa ℓb : ℕ} (L : ℕ) {P : CLFun 𝔽₂ (Fin a) ℓa} {Q : CLFun 𝔽₂ (Fin b) ℓb} (hP : P.ExactlyOn Finset.univ) (hQ : Q.ExactlyOn Finset.univ) (ha : ℓa ≤ L) (hb : ℓb ≤ L) (j : ℕ) (x : Fin (a + b) → 𝔽₂) : toBits ((truncate j (prodCL L P Q ha hb)).eval x) = toBits ((truncate j P).eval (leftPart x)) ++ toBits ((truncate j Q).eval (rightPart x))

theorem MIPRE.CL.CLFun.mapOfPrefix_prodCL {a b ℓa ℓb : ℕ} (L : ℕ) {P : CLFun 𝔽₂ (Fin a) ℓa} {Q : CLFun 𝔽₂ (Fin b) ℓb} (hP : P.ExactlyOn Finset.univ) (hQ : Q.ExactlyOn Finset.univ) (ha : ℓa ≤ L) (hb : ℓb ≤ L) (k : ℕ) (u y : Fin (a + b) → 𝔽₂) : ((prodCL L P Q ha hb).mapOfPrefix k u) y = Fin.append ((P.mapOfPrefix k (leftPart u)) (leftPart y)) ((Q.mapOfPrefix k (rightPart u)) (rightPart y))

theorem MIPRE.CL.CLFun.toBits_mapOfPrefix_prodCL {a b ℓa ℓb : ℕ} (L : ℕ) {P : CLFun 𝔽₂ (Fin a) ℓa} {Q : CLFun 𝔽₂ (Fin b) ℓb} (hP : P.ExactlyOn Finset.univ) (hQ : Q.ExactlyOn Finset.univ) (ha : ℓa ≤ L) (hb : ℓb ≤ L) (k : ℕ) (u y : Fin (a + b) → 𝔽₂) : toBits (((prodCL L P Q ha hb).mapOfPrefix k u) y) = toBits ((P.mapOfPrefix k (leftPart u)) (leftPart y)) ++ toBits ((Q.mapOfPrefix k (rightPart u)) (rightPart y))

theorem MIPRE.CL.CLFun.factorOfPrefix_prodCL {a b ℓa ℓb : ℕ} (L : ℕ) {P : CLFun 𝔽₂ (Fin a) ℓa} {Q : CLFun 𝔽₂ (Fin b) ℓb} (hP : P.ExactlyOn Finset.univ) (hQ : Q.ExactlyOn Finset.univ) (ha : ℓa ≤ L) (hb : ℓb ≤ L) (k : ℕ) (u : Fin (a + b) → 𝔽₂) : (prodCL L P Q ha hb).factorOfPrefix k u = Finset.map finSumFinEquiv.toEmbedding (Finset.map Function.Embedding.inl (P.factorOfPrefix k (leftPart u)) ∪ Finset.map Function.Embedding.inr (Q.factorOfPrefix k (rightPart u)))

theorem MIPRE.CL.CLFun.indicatorBits_factorOfPrefix_prodCL {a b ℓa ℓb : ℕ} (L : ℕ) {P : CLFun 𝔽₂ (Fin a) ℓa} {Q : CLFun 𝔽₂ (Fin b) ℓb} (hP : P.ExactlyOn Finset.univ) (hQ : Q.ExactlyOn Finset.univ) (ha : ℓa ≤ L) (hb : ℓb ≤ L) (k : ℕ) (u : Fin (a + b) → 𝔽₂) : indicatorBits ((prodCL L P Q ha hb).factorOfPrefix k u) = indicatorBits (P.factorOfPrefix k (leftPart u)) ++ indicatorBits (Q.factorOfPrefix k (rightPart u))