The typed answer-reduced decider

Piece AR-3e of planning/answer-reduction.md, concluded: the decider of the typed answer-reduced verifier as a total CL.TypedDecider over the types Role × PcpTy, whose acceptance law is the typed predicate typedPred of MIPRE/Background/AnswerReduction/TypedGame with the game check gameCheck (accepts_iff).

The decider is hardcode core (S̄, D̄, λ, μ, σ), one fixed program with the input programs and the parameters as data. On a typed input (n, u, x, v, y, a, b) it runs eight stages, each keeping its input as context:

1. the PCP parameters pd n, by the parameter routine of the sampler (ParRoutine.core);
2. Q = (λn + 1)^μ and T = 2^{(Q + 5)(μ + 1)} (ParRoutine.budCore);
3. to 6. the input sampler's full marginals L^𝖠 x_O, L^𝖡 x_O, L^𝖠 y_O, L^𝖡 y_O of the oracle halves of the two questions, through the universal machine;
4. and 8. the PCP verifier of PD on each question's game-check view;

and decides by the program verdictP of MIPRE/Background/AnswerReduction/DecideProg on what it read. Unlike the oracularized decider it never runs the input decider, whose program only enters the PCP verifier's input as data, and every stage halts on every input: the parsing stages are total, the input sampler halts on every input (Sampler.halts), and the PCP verifier runs on the encoding of a genuine input. So no clock is needed (total).

Stages

noncomputable def MIPRE.AnswerReduction.stg (arg : Cost.PolyTimeFun Cost.Data Cost.Data) (p : Cost.Prog) : Cost.Prog

A stage: run p on an argument read off the context, and keep the context.

Equations

• MIPRE.AnswerReduction.stg arg p = MIPRE.Pipeline.stageProg (MIPRE.Cost.PolyTimeFun.treePair.ap₂ arg (MIPRE.Cost.PolyTimeFun.id MIPRE.Cost.Data)) p MIPRE.AnswerReduction.ParRoutine.postKeep

theorem MIPRE.AnswerReduction.stg_closed (arg : Cost.PolyTimeFun Cost.Data Cost.Data) {p : Cost.Prog} (hp : Cost.Prog.WellScoped 1 p) : Cost.Prog.WellScoped 1 (stg arg p)

theorem MIPRE.AnswerReduction.stg_runs (arg : Cost.PolyTimeFun Cost.Data Cost.Data) {p : Cost.Prog} (hp : Cost.Prog.WellScoped 1 p) (X r : Cost.Data) (h : ∃ (t : ℕ), p.Runs (arg.toFun X) r t) : ∃ (t : ℕ), (stg arg p).Runs X (r.cons X) t

Reading the context

def MIPRE.AnswerReduction.tails : ℕ → Cost.PolyTimeFun Cost.Data Cost.Data

The context k stages back.

Equations

• MIPRE.AnswerReduction.tails 0 = MIPRE.Cost.PolyTimeFun.id MIPRE.Cost.Data
• MIPRE.AnswerReduction.tails k.succ = (MIPRE.AnswerReduction.tails k).comp MIPRE.Cost.PolyTimeFun.treeTail

@[simp]

theorem MIPRE.AnswerReduction.tails_zero (d : Cost.Data) : (tails 0).toFun d = d

@[simp]

theorem MIPRE.AnswerReduction.tails_cons (k : ℕ) (a d : Cost.Data) : (tails (k + 1)).toFun (a.cons d) = (tails k).toFun d

noncomputable def MIPRE.AnswerReduction.res (k : ℕ) : Cost.PolyTimeFun Cost.Data Cost.Data

The result of the stage k stages back.

Equations

• MIPRE.AnswerReduction.res k = MIPRE.Cost.PolyTimeFun.treeHead.comp (MIPRE.AnswerReduction.tails k)

noncomputable def MIPRE.AnswerReduction.hdat (j : ℕ) : Cost.PolyTimeFun Cost.Data Cost.Data

The input tuple and the hardcoded data, after j stages.

Equations

• MIPRE.AnswerReduction.hdat j = MIPRE.Cost.PolyTimeFun.treeHead.comp (MIPRE.AnswerReduction.tails j)

noncomputable def MIPRE.AnswerReduction.inp (j i : ℕ) : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

• MIPRE.AnswerReduction.inp j i = MIPRE.Cost.PolyTimeFun.treeHead.comp ((MIPRE.AnswerReduction.tails i).comp (MIPRE.Cost.PolyTimeFun.treeTail.comp (MIPRE.AnswerReduction.tails j)))

noncomputable def MIPRE.AnswerReduction.inpLast (j : ℕ) : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

• MIPRE.AnswerReduction.inpLast j = (MIPRE.AnswerReduction.tails 6).comp (MIPRE.Cost.PolyTimeFun.treeTail.comp (MIPRE.AnswerReduction.tails j))

noncomputable def MIPRE.AnswerReduction.spD (j : ℕ) : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

• MIPRE.AnswerReduction.spD j = MIPRE.Cost.PolyTimeFun.treeHead.comp (MIPRE.AnswerReduction.hdat j)

noncomputable def MIPRE.AnswerReduction.dpD (j : ℕ) : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

• MIPRE.AnswerReduction.dpD j = MIPRE.Cost.PolyTimeFun.treeHead.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp (MIPRE.AnswerReduction.hdat j))

noncomputable def MIPRE.AnswerReduction.lmsD (j : ℕ) : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

• MIPRE.AnswerReduction.lmsD j = MIPRE.Cost.PolyTimeFun.treeTail.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp (MIPRE.AnswerReduction.hdat j))

noncomputable def MIPRE.AnswerReduction.leftBP : Cost.PolyTimeFun (Cost.BitStr × Cost.Unary) Cost.BitStr

The first |x| - d bits: the oracle half.

Equations

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

noncomputable def MIPRE.AnswerReduction.rightBP : Cost.PolyTimeFun (Cost.BitStr × Cost.Unary) Cost.BitStr

The last d bits: the PCP half.

Equations

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

theorem MIPRE.AnswerReduction.leftBP_apply (l : Cost.BitStr) (d : Cost.Unary) : leftBP.toFun (l, d) = List.take (List.length l - List.length d) l

theorem MIPRE.AnswerReduction.rightBP_apply (l : Cost.BitStr) (d : Cost.Unary) : rightBP.toFun (l, d) = List.drop (List.length l - List.length d) l

noncomputable def MIPRE.AnswerReduction.blocksOfP : Cost.PolyTimeFun (Cost.Unary × Cost.Unary × Cost.BitStr) StageProg.Blocks

The runs of blocks of a PCP half: (k, m', z) ↦ blocksOf k m' z.

Equations

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

@[simp]

theorem MIPRE.AnswerReduction.blocksOfP_apply (k m' : Cost.Unary) (z : Cost.BitStr) : blocksOfP.toFun (k, m', z) = StageProg.blocksOf k m' z

The stages

@[instance_reducible]

instance MIPRE.AnswerReduction.instInhabitedTy : Inhabited LIDT.CL.Ty

Equations

• MIPRE.AnswerReduction.instInhabitedTy = { default := MIPRE.LIDT.CL.Ty.point }

noncomputable def MIPRE.AnswerReduction.pdD (j : ℕ) : Cost.PolyTimeFun Cost.Data Cost.Data

The PCP parameters pd, the width k and m', after j stages (j ≥ 1).

Equations

• MIPRE.AnswerReduction.pdD j = MIPRE.AnswerReduction.res (j - 1)

noncomputable def MIPRE.AnswerReduction.kD (j : ℕ) : Cost.PolyTimeFun Cost.Data Cost.Unary

Equations

• MIPRE.AnswerReduction.kD j = MIPRE.AnswerReduction.readU.comp (MIPRE.Cost.PolyTimeFun.treeHead.comp (MIPRE.AnswerReduction.pdD j))

noncomputable def MIPRE.AnswerReduction.m'D (j : ℕ) : Cost.PolyTimeFun Cost.Data Cost.Unary

Equations

• MIPRE.AnswerReduction.m'D j = MIPRE.AnswerReduction.readU.comp (MIPRE.Cost.PolyTimeFun.treeHead.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp (MIPRE.AnswerReduction.pdD j)))

noncomputable def MIPRE.AnswerReduction.qBits (j i : ℕ) : Cost.PolyTimeFun Cost.Data Cost.BitStr

The bits of the question in the input's field i (2 or 4), after j stages.

Equations

• MIPRE.AnswerReduction.qBits j i = MIPRE.CL.Detyping.Program.readBits.comp (MIPRE.AnswerReduction.inp j i)

noncomputable def MIPRE.AnswerReduction.oBits (j i : ℕ) : Cost.PolyTimeFun Cost.Data Cost.BitStr

Its oracle half.

Equations

• MIPRE.AnswerReduction.oBits j i = MIPRE.AnswerReduction.leftBP.comp ((MIPRE.AnswerReduction.qBits j i).pair (MIPRE.AnswerReduction.dimProg.comp (MIPRE.AnswerReduction.pdD j)))

noncomputable def MIPRE.AnswerReduction.pBlocks (j i : ℕ) : Cost.PolyTimeFun Cost.Data StageProg.Blocks

Its PCP half, in runs of blocks.

Equations

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

noncomputable def MIPRE.AnswerReduction.argPar (j : ℕ) : Cost.PolyTimeFun Cost.Data Cost.Data

Stage 1's argument: ((λ, μ, σ), n).

Equations

• MIPRE.AnswerReduction.argPar j = MIPRE.Cost.PolyTimeFun.treePair.ap₂ (MIPRE.AnswerReduction.lmsD j) (MIPRE.AnswerReduction.inp j 0)

noncomputable def MIPRE.AnswerReduction.argMarg (ℓ j i : ℕ) (w : Player) : Cost.PolyTimeFun Cost.Data Cost.Data

A marginal call's argument, after j stages: the input sampler's program and the query (n, marginal w (ℓ + 1) z) at the oracle half z of the question in field i.

Equations

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

noncomputable def MIPRE.AnswerReduction.aBlocks (j it ia : ℕ) : Cost.PolyTimeFun Cost.Data (List Cost.BitStr)

The answer blocks of the answer in field ia, parsed at the type in field it.

Equations

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

noncomputable def MIPRE.AnswerReduction.argVer (j i it ia rA rB : ℕ) : Cost.PolyTimeFun Cost.Data Cost.Data

A game check's argument, after j stages (j = 6, 7): the PCP verifier's input on the question in field i, the answer in field ia and the marginals rA, rB stages back.

Equations

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

noncomputable def MIPRE.AnswerReduction.readV : Cost.PolyTimeFun Cost.Data VerdictIn

The verdict's reader, after the eight stages.

Equations

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

noncomputable def MIPRE.AnswerReduction.core (PD : SAT.PcpDecider) (ℓ : ℕ) : Cost.Prog

The core of the answer-reduced decider, on ((S̄, D̄, λ, μ, σ), (n, u, x, v, y, a, b)).

Equations

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

theorem MIPRE.AnswerReduction.core_closed (PD : SAT.PcpDecider) (ℓ : ℕ) : Cost.Prog.WellScoped 1 (core PD ℓ)

The run

def MIPRE.AnswerReduction.ctx0 (sp dp : Cost.Prog) (lam mu sigma n : ℕ) (u v : ArTy) (x y a b : Cost.BitStr) : Cost.Data

The core's input.

Equations

• MIPRE.AnswerReduction.ctx0 sp dp lam mu sigma n u v x y a b = (MIPRE.Cost.encode (sp, dp, lam, mu, sigma)).cons (MIPRE.Cost.encode (n, u, x, v, y, a, b))

@[reducible, inline]

abbrev MIPRE.AnswerReduction.dB (PD : SAT.PcpDecider) (lam mu sigma n : ℕ) : Cost.Unary

The width of the PCP half at index n.

Equations

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

theorem MIPRE.AnswerReduction.dimProg_pd' (PD : SAT.PcpDecider) (lam mu sigma n : ℕ) : dimProg.toFun ((family PD lam mu sigma).pd n) = dB PD lam mu sigma n

noncomputable def MIPRE.AnswerReduction.margQ (PD : SAT.PcpDecider) (ℓ : ℕ) (sp : Cost.Prog) (lam mu sigma n : ℕ) (w : Player) (z : Cost.BitStr) : Cost.Data

A marginal query at the oracle half of z.

Equations

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

noncomputable def MIPRE.AnswerReduction.pBl (PD : SAT.PcpDecider) (lam mu sigma n : ℕ) (z : Cost.BitStr) : StageProg.Blocks

The PCP half of a question, in runs of blocks.

Equations

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

noncomputable def MIPRE.AnswerReduction.aBl (PD : SAT.PcpDecider) (lam mu sigma n : ℕ) (t : ArTy) (s : Cost.BitStr) : List Cost.BitStr

The parse of an answer into blocks, at a type.

Equations

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

noncomputable def MIPRE.AnswerReduction.chkV (PD : SAT.PcpDecider) (dp : Cost.Prog) (lam mu sigma n : ℕ) (rA rB : Cost.Data) (z : Cost.BitStr) (t : ArTy) (s : Cost.BitStr) : Bool

A game check's verdict.

Equations

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

def MIPRE.AnswerReduction.ctx1 (PD : SAT.PcpDecider) (sp dp : Cost.Prog) (lam mu sigma n : ℕ) (u v : ArTy) (x y a b : Cost.BitStr) : Cost.Data

The contexts after each stage.

Equations

• MIPRE.AnswerReduction.ctx1 PD sp dp lam mu sigma n u v x y a b = ((MIPRE.AnswerReduction.family PD lam mu sigma).pd n).cons (MIPRE.AnswerReduction.ctx0 sp dp lam mu sigma n u v x y a b)

def MIPRE.AnswerReduction.ctx2 (PD : SAT.PcpDecider) (sp dp : Cost.Prog) (lam mu sigma n : ℕ) (u v : ArTy) (x y a b : Cost.BitStr) : Cost.Data

Equations

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

def MIPRE.AnswerReduction.ctx6 (PD : SAT.PcpDecider) (sp dp : Cost.Prog) (lam mu sigma n : ℕ) (u v : ArTy) (x y a b : Cost.BitStr) (rxA rxB ryA ryB : Cost.Data) : Cost.Data

Equations

• MIPRE.AnswerReduction.ctx6 PD sp dp lam mu sigma n u v x y a b rxA rxB ryA ryB = ryB.cons (ryA.cons (rxB.cons (rxA.cons (MIPRE.AnswerReduction.ctx2 PD sp dp lam mu sigma n u v x y a b))))

noncomputable def MIPRE.AnswerReduction.ctx7 (PD : SAT.PcpDecider) (sp dp : Cost.Prog) (lam mu sigma n : ℕ) (u v : ArTy) (x y a b : Cost.BitStr) (rxA rxB ryA ryB : Cost.Data) : Cost.Data

Equations

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

noncomputable def MIPRE.AnswerReduction.ctx8 (PD : SAT.PcpDecider) (sp dp : Cost.Prog) (lam mu sigma n : ℕ) (u v : ArTy) (x y a b : Cost.BitStr) (rxA rxB ryA ryB : Cost.Data) : Cost.Data

Equations

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

theorem MIPRE.AnswerReduction.pd_heads (PD : SAT.PcpDecider) (lam mu sigma n : ℕ) : readU.toFun (Cost.PolyTimeFun.treeHead.toFun ((family PD lam mu sigma).pd n)) = Cost.unary (arPar PD lam mu sigma n).k ∧ readU.toFun (Cost.PolyTimeFun.treeHead.toFun (Cost.PolyTimeFun.treeTail.toFun ((family PD lam mu sigma).pd n))) = Cost.unary (arPar PD lam mu sigma n).m' ∧ List.map readDesc.toFun (rawListP.toFun (Cost.PolyTimeFun.treeTail.toFun (Cost.PolyTimeFun.treeTail.toFun ((family PD lam mu sigma).pd n)))) = List.ofFn ((family PD lam mu sigma).desc n)

theorem MIPRE.AnswerReduction.descs_m (PD : SAT.PcpDecider) (lam mu sigma n : ℕ) : ((List.ofFn ((family PD lam mu sigma).desc n)).getD 0 default).2.1 = Cost.unary (arPar PD lam mu sigma n).m

theorem MIPRE.AnswerReduction.argPar_zero (sp dp : Cost.Prog) (lam mu sigma n : ℕ) (u v : ArTy) (x y a b : Cost.BitStr) : (argPar 0).toFun (ctx0 sp dp lam mu sigma n u v x y a b) = (Cost.encode (lam, mu, sigma)).cons (Cost.encode n)

theorem MIPRE.AnswerReduction.argPar_one (PD : SAT.PcpDecider) (sp dp : Cost.Prog) (lam mu sigma n : ℕ) (u v : ArTy) (x y a b : Cost.BitStr) : (argPar 1).toFun (ctx1 PD sp dp lam mu sigma n u v x y a b) = (Cost.encode (lam, mu, sigma)).cons (Cost.encode n)

theorem MIPRE.AnswerReduction.pdD_eq (PD : SAT.PcpDecider) (lam mu sigma n : ℕ) {j : ℕ} (d : Cost.Data) (h : (pdD j).toFun d = (family PD lam mu sigma).pd n) : (kD j).toFun d = Cost.unary (arPar PD lam mu sigma n).k ∧ (m'D j).toFun d = Cost.unary (arPar PD lam mu sigma n).m' ∧ dimProg.toFun ((pdD j).toFun d) = dB PD lam mu sigma n

theorem MIPRE.AnswerReduction.margArg_eq (PD : SAT.PcpDecider) (ℓ : ℕ) (sp : Cost.Prog) (lam mu sigma n j i : ℕ) (w : Player) (d : Cost.Data) (z : Cost.BitStr) (hpd : (pdD j).toFun d = (family PD lam mu sigma).pd n) (hsp : (spD j).toFun d = Cost.encode sp) (hn : (inp j 0).toFun d = Cost.encode n) (hz : (inp j i).toFun d = Cost.encode z) : (argMarg ℓ j i w).toFun d = margQ PD ℓ sp lam mu sigma n w z

theorem MIPRE.AnswerReduction.aBlocks_eq (PD : SAT.PcpDecider) (lam mu sigma n j it ia : ℕ) (d : Cost.Data) (t : ArTy) (s : Cost.BitStr) (hpd : (pdD j).toFun d = (family PD lam mu sigma).pd n) (ht : (inp j it).toFun d = Cost.encode t) (hs : (if ia = 5 then inp j ia else inpLast j).toFun d = Cost.encode s) : (aBlocks j it ia).toFun d = aBl PD lam mu sigma n t s

theorem MIPRE.AnswerReduction.pBlocks_eq (PD : SAT.PcpDecider) (lam mu sigma n j i : ℕ) (d : Cost.Data) (z : Cost.BitStr) (hpd : (pdD j).toFun d = (family PD lam mu sigma).pd n) (hz : (inp j i).toFun d = Cost.encode z) : (pBlocks j i).toFun d = pBl PD lam mu sigma n z

theorem MIPRE.AnswerReduction.argVer_eq (PD : SAT.PcpDecider) (dp : Cost.Prog) (lam mu sigma n j i it ia rA rB : ℕ) (d RA RB : Cost.Data) (z : Cost.BitStr) (t : ArTy) (s : Cost.BitStr) (hpd : (pdD j).toFun d = (family PD lam mu sigma).pd n) (hdp : (dpD j).toFun d = Cost.encode dp) (hn : (inp j 0).toFun d = Cost.encode n) (hqt : (res (j - 2)).toFun d = Cost.encode (arQ lam mu n, tPcp lam mu n)) (hσ : Cost.PolyTimeFun.treeTail.toFun (Cost.PolyTimeFun.treeTail.toFun ((lmsD j).toFun d)) = Cost.encode sigma) (hA : (res rA).toFun d = RA) (hB : (res rB).toFun d = RB) (hz : (inp j i).toFun d = Cost.encode z) (ht : (inp j it).toFun d = Cost.encode t) (hs : (if ia = 5 then inp j ia else inpLast j).toFun d = Cost.encode s) : (argVer j i it ia rA rB).toFun d = Cost.encode (SAT.pcpInput dp n (tPcp lam mu n) (arQ lam mu n) sigma (CL.Detyping.Program.readBits.toFun RA) (CL.Detyping.Program.readBits.toFun RB) (pBl PD lam mu sigma n z).1 (aBl PD lam mu sigma n t s))

theorem MIPRE.AnswerReduction.ctx6_reads (PD : SAT.PcpDecider) (sp dp : Cost.Prog) (lam mu sigma n : ℕ) (u v : ArTy) (x y a b : Cost.BitStr) (rxA rxB ryA ryB : Cost.Data) : (pdD 6).toFun (ctx6 PD sp dp lam mu sigma n u v x y a b rxA rxB ryA ryB) = (family PD lam mu sigma).pd n ∧ (dpD 6).toFun (ctx6 PD sp dp lam mu sigma n u v x y a b rxA rxB ryA ryB) = Cost.encode dp ∧ (inp 6 0).toFun (ctx6 PD sp dp lam mu sigma n u v x y a b rxA rxB ryA ryB) = Cost.encode n ∧ (res 4).toFun (ctx6 PD sp dp lam mu sigma n u v x y a b rxA rxB ryA ryB) = Cost.encode (arQ lam mu n, tPcp lam mu n) ∧ Cost.PolyTimeFun.treeTail.toFun (Cost.PolyTimeFun.treeTail.toFun ((lmsD 6).toFun (ctx6 PD sp dp lam mu sigma n u v x y a b rxA rxB ryA ryB))) = Cost.encode sigma ∧ (res 3).toFun (ctx6 PD sp dp lam mu sigma n u v x y a b rxA rxB ryA ryB) = rxA ∧ (res 2).toFun (ctx6 PD sp dp lam mu sigma n u v x y a b rxA rxB ryA ryB) = rxB ∧ (inp 6 2).toFun (ctx6 PD sp dp lam mu sigma n u v x y a b rxA rxB ryA ryB) = Cost.encode x ∧ (inp 6 1).toFun (ctx6 PD sp dp lam mu sigma n u v x y a b rxA rxB ryA ryB) = Cost.encode u ∧ (if 5 = 5 then inp 6 5 else inpLast 6).toFun (ctx6 PD sp dp lam mu sigma n u v x y a b rxA rxB ryA ryB) = Cost.encode a

theorem MIPRE.AnswerReduction.ctx7_reads (PD : SAT.PcpDecider) (sp dp : Cost.Prog) (lam mu sigma n : ℕ) (u v : ArTy) (x y a b : Cost.BitStr) (rxA rxB ryA ryB : Cost.Data) : (pdD 7).toFun (ctx7 PD sp dp lam mu sigma n u v x y a b rxA rxB ryA ryB) = (family PD lam mu sigma).pd n ∧ (dpD 7).toFun (ctx7 PD sp dp lam mu sigma n u v x y a b rxA rxB ryA ryB) = Cost.encode dp ∧ (inp 7 0).toFun (ctx7 PD sp dp lam mu sigma n u v x y a b rxA rxB ryA ryB) = Cost.encode n ∧ (res 5).toFun (ctx7 PD sp dp lam mu sigma n u v x y a b rxA rxB ryA ryB) = Cost.encode (arQ lam mu n, tPcp lam mu n) ∧ Cost.PolyTimeFun.treeTail.toFun (Cost.PolyTimeFun.treeTail.toFun ((lmsD 7).toFun (ctx7 PD sp dp lam mu sigma n u v x y a b rxA rxB ryA ryB))) = Cost.encode sigma ∧ (res 2).toFun (ctx7 PD sp dp lam mu sigma n u v x y a b rxA rxB ryA ryB) = ryA ∧ (res 1).toFun (ctx7 PD sp dp lam mu sigma n u v x y a b rxA rxB ryA ryB) = ryB ∧ (inp 7 4).toFun (ctx7 PD sp dp lam mu sigma n u v x y a b rxA rxB ryA ryB) = Cost.encode y ∧ (inp 7 3).toFun (ctx7 PD sp dp lam mu sigma n u v x y a b rxA rxB ryA ryB) = Cost.encode v ∧ (if 6 = 5 then inp 7 6 else inpLast 7).toFun (ctx7 PD sp dp lam mu sigma n u v x y a b rxA rxB ryA ryB) = Cost.encode b

theorem MIPRE.AnswerReduction.readV_ctx8 (PD : SAT.PcpDecider) (sp dp : Cost.Prog) (lam mu sigma n : ℕ) (u v : ArTy) (x y a b : Cost.BitStr) (rxA rxB ryA ryB : Cost.Data) : readV.toFun (ctx8 PD sp dp lam mu sigma n u v x y a b rxA rxB ryA ryB) = ((Cost.unary (arPar PD lam mu sigma n).k, Cost.unary (arPar PD lam mu sigma n).m', List.ofFn ((family PD lam mu sigma).desc n)), (chkV PD dp lam mu sigma n rxA rxB x u a, chkV PD dp lam mu sigma n ryA ryB y v b), (u, v), (pBl PD lam mu sigma n x, pBl PD lam mu sigma n y), a, b)

theorem MIPRE.AnswerReduction.core_runs (PD : SAT.PcpDecider) (ℓ : ℕ) (sp dp : Cost.Prog) (lam mu sigma n : ℕ) (u v : ArTy) (x y a b : Cost.BitStr) (rxA rxB ryA ryB : Cost.Data) (hxA : ∃ (t : ℕ), Cost.selfUniversal.univ.Runs (margQ PD ℓ sp lam mu sigma n Player.alice x) rxA t) (hxB : ∃ (t : ℕ), Cost.selfUniversal.univ.Runs (margQ PD ℓ sp lam mu sigma n Player.bob x) rxB t) (hyA : ∃ (t : ℕ), Cost.selfUniversal.univ.Runs (margQ PD ℓ sp lam mu sigma n Player.alice y) ryA t) (hyB : ∃ (t : ℕ), Cost.selfUniversal.univ.Runs (margQ PD ℓ sp lam mu sigma n Player.bob y) ryB t) : ∃ (t : ℕ), (core PD ℓ).Runs (ctx0 sp dp lam mu sigma n u v x y a b) (Cost.encode (verdictP.toFun (readV.toFun (ctx8 PD sp dp lam mu sigma n u v x y a b rxA rxB ryA ryB)))) t

The core's run, given the input sampler's four runs.

The typed decider and its acceptance law

noncomputable def MIPRE.AnswerReduction.typedDecider (PD : SAT.PcpDecider) {ℓ : ℕ} (V : Verifier (ℓ + 1)) (lam mu sigma : ℕ) : CL.Detyping.TypedDecider ArTy

The typed answer-reduced decider of V at the parameters (λ, μ, σ).

Equations

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

theorem MIPRE.AnswerReduction.leftBP_toBits (PD : SAT.PcpDecider) {ℓ : ℕ} (V : Verifier (ℓ + 1)) (lam mu sigma n : ℕ) (z : Fin (dim V n ((family PD lam mu sigma).par n)) → CL.𝔽₂) : leftBP.toFun (CL.toBits z, dB PD lam mu sigma n) = CL.toBits (oraclePart V n ((family PD lam mu sigma).par n) z)

theorem MIPRE.AnswerReduction.rightBP_toBits (PD : SAT.PcpDecider) {ℓ : ℕ} (V : Verifier (ℓ + 1)) (lam mu sigma n : ℕ) (z : Fin (dim V n ((family PD lam mu sigma).par n)) → CL.𝔽₂) : rightBP.toFun (CL.toBits z, dB PD lam mu sigma n) = Pcp.flatBits ((family PD lam mu sigma).par n) ⋯ (pcpPart V n ((family PD lam mu sigma).par n) ⋯ z)

theorem MIPRE.AnswerReduction.pBl_toBits (PD : SAT.PcpDecider) {ℓ : ℕ} (V : Verifier (ℓ + 1)) (lam mu sigma n : ℕ) (z : Fin (dim V n ((family PD lam mu sigma).par n)) → CL.𝔽₂) : pBl PD lam mu sigma n (CL.toBits z) = blocksV ⋯ ((family PD lam mu sigma).par n) (pcpPart V n ((family PD lam mu sigma).par n) ⋯ z)

theorem MIPRE.AnswerReduction.margBits_oracle (PD : SAT.PcpDecider) {ℓ : ℕ} (V : Verifier (ℓ + 1)) (lam mu sigma n : ℕ) (w : Player) (z : Fin (dim V n ((family PD lam mu sigma).par n)) → CL.𝔽₂) : OracleDecider.margBits V.sampler n (ℓ + 1) w (CL.toBits (oraclePart V n ((family PD lam mu sigma).par n) z)) = CL.toBits ((V.sampler.cl n w).eval (oraclePart V n ((family PD lam mu sigma).par n) z))

The input sampler's full marginal at the oracle half, in bits.

theorem MIPRE.AnswerReduction.margQ_runs (PD : SAT.PcpDecider) {ℓ : ℕ} (V : Verifier (ℓ + 1)) (lam mu sigma n : ℕ) (w : Player) (z : Fin (dim V n ((family PD lam mu sigma).par n)) → CL.𝔽₂) : ∃ (t : ℕ), Cost.selfUniversal.univ.Runs (margQ PD ℓ V.sampler.prog lam mu sigma n w (CL.toBits z)) (Cost.encode (CL.toBits ((V.sampler.cl n w).eval (oraclePart V n ((family PD lam mu sigma).par n) z)))) t

The input sampler's runs on the marginal queries at a question's oracle half.

@[reducible, inline]

noncomputable abbrev MIPRE.AnswerReduction.chk (PD : SAT.PcpDecider) {ℓ : ℕ} (V : Verifier (ℓ + 1)) (lam mu sigma n : ℕ) : (Fin (V.sampler.dim n) → CL.𝔽₂) → (Fin ((family PD lam mu sigma).par n).m' → Fq ((family PD lam mu sigma).par n) ⋯) → (Fin (((family PD lam mu sigma).par n).m' + 6) → Fq ((family PD lam mu sigma).par n) ⋯) → Bool

The game check of the typed game at index n.

Equations

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

theorem MIPRE.AnswerReduction.chkV_eq (PD : SAT.PcpDecider) {ℓ : ℕ} (V : Verifier (ℓ + 1)) (lam mu sigma n : ℕ) (t : ArTy) (z : Fin (dim V n ((family PD lam mu sigma).par n)) → CL.𝔽₂) (s : Cost.BitStr) (u' : Ans ((family PD lam mu sigma).par n) (Fq ((family PD lam mu sigma).par n) ⋯)) (hs : parse (fld ((family PD lam mu sigma).par n) ⋯) t.2 s = some u') (ht : chkPlan t = true) : chkV PD V.decider.prog lam mu sigma n (Cost.encode (CL.toBits ((V.sampler.cl n Player.alice).eval (oraclePart V n ((family PD lam mu sigma).par n) z)))) (Cost.encode (CL.toBits ((V.sampler.cl n Player.bob).eval (oraclePart V n ((family PD lam mu sigma).par n) z)))) (CL.toBits z) t s = chk PD V lam mu sigma n (oraclePart V n ((family PD lam mu sigma).par n) z) ((Pcp.regs6 ((family PD lam mu sigma).par n)).ptOf (pcpPart V n ((family PD lam mu sigma).par n) ⋯ z)) (vals6 u')

The game check's verdict is the game check, on a parsed Point_6 answer.

theorem MIPRE.AnswerReduction.accepts_iff (PD : SAT.PcpDecider) {ℓ : ℕ} (V : Verifier (ℓ + 1)) (lam mu sigma n : ℕ) (u v : ArTy) (x y : Fin (dim V n ((family PD lam mu sigma).par n)) → CL.𝔽₂) {B : ℕ} (a b : Verifier.Answers B) : (typedDecider PD V lam mu sigma).Accepts n u (CL.toBits x) v (CL.toBits y) ↑a ↑b ↔ typedPred V n ((family PD lam mu sigma).par n) ⋯ ((family PD lam mu sigma).sel n) ((family PD lam mu sigma).sel' n) (chk PD V lam mu sigma n) B (u, x) (v, y) a b = true

The acceptance law: on questions of the typed game and any answers, the typed answer-reduced decider accepts exactly when the typed predicate does.

Totality

theorem MIPRE.AnswerReduction.argMarg_general {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n j i : ℕ) (w : Player) (d : Cost.Data) (hsp : (spD j).toFun d = Cost.encode V.sampler.prog) (hn : (inp j 0).toFun d = Cost.encode n) : (argMarg ℓ j i w).toFun d = (Cost.encode V.sampler.prog).cons ((Cost.encode n).cons (Cost.encode (1, w, ℓ + 1, (oBits j i).toFun d, [])))

theorem MIPRE.AnswerReduction.argVer_general {ℓ : ℕ} (V : Verifier (ℓ + 1)) (j i it ia rA rB : ℕ) (d : Cost.Data) (hdp : (dpD j).toFun d = Cost.encode V.decider.prog) : (argVer j i it ia rA rB).toFun d = Cost.encode (SAT.pcpInput V.decider.prog (CL.Detyping.Program.readNat.toFun ((inp j 0).toFun d)) (CL.Detyping.Program.readNat.toFun (Cost.PolyTimeFun.treeTail.toFun ((res (j - 2)).toFun d))) (CL.Detyping.Program.readNat.toFun (Cost.PolyTimeFun.treeHead.toFun ((res (j - 2)).toFun d))) (CL.Detyping.Program.readNat.toFun (Cost.PolyTimeFun.treeTail.toFun (Cost.PolyTimeFun.treeTail.toFun ((lmsD j).toFun d)))) (CL.Detyping.Program.readBits.toFun ((res rA).toFun d)) (CL.Detyping.Program.readBits.toFun ((res rB).toFun d)) ((pBlocks j i).toFun d).1 ((aBlocks j it ia).toFun d))

theorem MIPRE.AnswerReduction.univ_marg_halts {ℓ : ℕ} (V : Verifier (ℓ + 1)) (n : ℕ) (q : Cost.Data) : ∃ (r : Cost.Data) (t : ℕ), Cost.selfUniversal.univ.Runs ((Cost.encode V.sampler.prog).cons ((Cost.encode n).cons q)) r t

A marginal call halts, whatever its query.

theorem MIPRE.AnswerReduction.total (PD : SAT.PcpDecider) {ℓ : ℕ} (V : Verifier (ℓ + 1)) (lam mu sigma : ℕ) : (typedDecider PD V lam mu sigma).Total

The typed answer-reduced decider halts on every input (n, …).