The answer-reduced verifier

Piece AR-3f of planning/answer-reduction.md, concluded: the output of answer reduction as a normal form verifier (arVerifier), the typed answer-reduced verifier through the detyping compiler at the answer cut cutVal (arCut); its programs as polynomial-time functions of the input programs and (λ, μ, σ) (arSamplerProg, arCompute), the sampler's of the input sampler's alone; and its complexity clause (arVerifier_within), the within field of the AnswerReduction contract.

The answer cut 32 (k + 1)(m' + 7)^2 is above the length 4 (k + 1) cnt + 1 of the encoding of every well-formed answer, cnt ≤ (m' + 6)(7 m' + 1) field elements of k bits (MIPRE/Background/AnswerReduction/AnswerFormat), which completeness (AR-4) needs; and it is polynomial in the PCP's parameters, which the complexity clause needs.

The answer cut

def MIPRE.AnswerReduction.cutVal (P : SAT.PcpParams) : ℕ

The answer cut, 32 (k + 1)(m' + 7)^2.

Equations

• MIPRE.AnswerReduction.cutVal P = 32 * ((P.k + 1) * (P.m' + 7) * (P.m' + 7))

noncomputable def MIPRE.AnswerReduction.cutP : Cost.PolyTimeFun Cost.Data (ℕ × ℕ)

The answer cut, from the parameters pd n, twice.

Equations

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

theorem MIPRE.AnswerReduction.cutP_pd (PD : SAT.PcpDecider) (lam mu sigma n : ℕ) : cutP.toFun ((family PD lam mu sigma).pd n) = (cutVal (arPar PD lam mu sigma n), cutVal (arPar PD lam mu sigma n))

noncomputable def MIPRE.AnswerReduction.cutProg (PD : SAT.PcpDecider) (lam mu sigma : ℕ) : Cost.Prog

The cutoff program: the parameter routine, then cutP.

Equations

• MIPRE.AnswerReduction.cutProg PD lam mu sigma = MIPRE.Cost.seqProg (MIPRE.AnswerReduction.parProg PD lam mu sigma) MIPRE.AnswerReduction.cutP.code

noncomputable def MIPRE.AnswerReduction.arCut (PD : SAT.PcpDecider) (lam mu sigma : ℕ) : CL.Detyping.CutoffProgram

The cutoff program of answer reduction: both cuts cutVal.

Equations

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

The verifier

noncomputable def MIPRE.AnswerReduction.arVerifier (PD : SAT.PcpDecider) (lam mu sigma : ℕ) {ℓ : ℕ} (V : Verifier (ℓ + 1)) : Verifier (level ℓ + 2)

The answer-reduced verifier of V at (λ, μ, σ): the typed answer-reduced verifier through the detyping compiler, at the cutoff arCut.

Equations

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

The programs, in polynomial time

noncomputable def MIPRE.AnswerReduction.parPF (PD : SAT.PcpDecider) : Cost.PolyTimeFun (ℕ × ℕ × ℕ) Cost.Prog

The parameter routine's program, from (λ, μ, σ).

Equations

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

noncomputable def MIPRE.AnswerReduction.typedPF (PD : SAT.PcpDecider) (ℓ : ℕ) : Cost.PolyTimeFun (Cost.Prog × ℕ × ℕ × ℕ) Cost.Prog

The typed sampler's program, from the input sampler's and (λ, μ, σ).

Equations

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

noncomputable def MIPRE.AnswerReduction.arSamplerProg (PD : SAT.PcpDecider) (ℓ : ℕ) : Cost.PolyTimeFun (Cost.Prog × ℕ × ℕ × ℕ) Cost.Prog

The answer-reduced sampler's program, from the input sampler's and (λ, μ, σ).

Equations

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

theorem MIPRE.AnswerReduction.arSamplerProg_eq (PD : SAT.PcpDecider) (lam mu sigma : ℕ) {ℓ : ℕ} (V : Verifier (ℓ + 1)) : (arSamplerProg PD ℓ).toFun (V.sampler.prog, lam, mu, sigma) = (arVerifier PD lam mu sigma V).sampler.prog

noncomputable def MIPRE.AnswerReduction.typedDPF (PD : SAT.PcpDecider) (ℓ : ℕ) : Cost.PolyTimeFun ((Cost.Prog × Cost.Prog) × ℕ × ℕ × ℕ) Cost.Prog

The typed decider's program, from the input programs and (λ, μ, σ).

Equations

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

noncomputable def MIPRE.AnswerReduction.cutPF (PD : SAT.PcpDecider) : Cost.PolyTimeFun (ℕ × ℕ × ℕ) Cost.Prog

The cutoff program, from (λ, μ, σ).

Equations

• MIPRE.AnswerReduction.cutPF PD = MIPRE.CL.ProgBuild.letF.comp ((MIPRE.AnswerReduction.parPF PD).pair (MIPRE.Cost.PolyTimeFun.const MIPRE.AnswerReduction.cutP.code))

noncomputable def MIPRE.AnswerReduction.arCompute (PD : SAT.PcpDecider) (ℓ : ℕ) : Cost.PolyTimeFun ((Cost.Prog × Cost.Prog) × ℕ × ℕ × ℕ) Cost.Prog

The answer-reduced decider's program (ComputeAnsVerifier), from the input programs and (λ, μ, σ).

Equations

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

theorem MIPRE.AnswerReduction.arCompute_eq (PD : SAT.PcpDecider) (lam mu sigma : ℕ) {ℓ : ℕ} (V : Verifier (ℓ + 1)) : (arCompute PD ℓ).toFun ((V.sampler.prog, V.decider.prog), lam, mu, sigma) = (arVerifier PD lam mu sigma V).decider.prog

theorem MIPRE.AnswerReduction.arVerifier_sampler (PD : SAT.PcpDecider) (lam mu sigma : ℕ) {ℓ : ℕ} (V V' : Verifier (ℓ + 1)) (h : V.sampler = V'.sampler) : (arVerifier PD lam mu sigma V).sampler = (arVerifier PD lam mu sigma V').sampler

The sampler depends only on the input sampler and (λ, μ, σ) (lem:ar-sampler-independence).

The complexity clause

theorem MIPRE.AnswerReduction.arCut_time (PD : SAT.PcpDecider) (R : Polynomial ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {W X : ℕ}, ParamsBound PD R → ∀ (lam mu sigma n : ℕ), 1 ≤ X → arQ lam mu n ≤ W → lam ≤ W → sigma ≤ W → n ≤ W → Pipeline.PRuns W X mu c m e (arCut PD lam mu sigma).prog (Cost.encode n) (Cost.encode ((arCut PD lam mu sigma).inner n, (arCut PD lam mu sigma).outer n))

The cutoff program's time.

theorem MIPRE.AnswerReduction.parA_pdom (PD : SAT.PcpDecider) (R : Polynomial ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {W X : ℕ}, ParamsBound PD R → ∀ (lam mu sigma n : ℕ), 1 ≤ X → arQ lam mu n ≤ W → sigma ≤ W → n ≤ W → Pipeline.PDom W X mu c m e (20 * ((arPar PD lam mu sigma n).k + (arPar PD lam mu sigma n).m + (arPar PD lam mu sigma n).s) + 20)

The PCP's parameters, in the form the cut and the dimension use.

theorem MIPRE.AnswerReduction.cutVal_pdom (PD : SAT.PcpDecider) (R : Polynomial ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {W X : ℕ}, ParamsBound PD R → ∀ (lam mu sigma n : ℕ), 1 ≤ X → arQ lam mu n ≤ W → sigma ≤ W → n ≤ W → Pipeline.PDom W X mu c m e (cutVal (arPar PD lam mu sigma n))

The answer cut is dominated.

theorem MIPRE.AnswerReduction.pcpWidth_pdom (PD : SAT.PcpDecider) (R : Polynomial ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {W X : ℕ}, ParamsBound PD R → ∀ (lam mu sigma n : ℕ), 1 ≤ X → arQ lam mu n ≤ W → sigma ≤ W → n ≤ W → Pipeline.PDom W X mu c m e (Pcp.pcpDim (arPar PD lam mu sigma n) * (arPar PD lam mu sigma n).k)

The PCP half's width is dominated.

theorem MIPRE.AnswerReduction.exists_esize_arTy_le : ∃ (c : ℕ), ∀ (u : ArTy), Cost.esize u ≤ c

A bound on the size of the answer-reduced types' encodings.

theorem MIPRE.AnswerReduction.typedArg_pdom (PD : SAT.PcpDecider) (R : Polynomial ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {W X : ℕ}, ParamsBound PD R → ∀ (lam mu sigma n s : ℕ), 1 ≤ X → arQ lam mu n ≤ W → sigma ≤ W → n ≤ W → s ≤ W + Pcp.pcpDim (arPar PD lam mu sigma n) * (arPar PD lam mu sigma n).k → ∀ (u v : ArTy) (x y a b : Cost.BitStr), List.length x = s → List.length y = s → List.length a ≤ cutVal (arPar PD lam mu sigma n) → List.length b ≤ cutVal (arPar PD lam mu sigma n) → Pipeline.PDom W X mu c m e (Cost.encode (u, x, v, y, a, b)).size

The typed inputs the router hands the typed decider are dominated.

theorem MIPRE.AnswerReduction.dim_pdom (PD : SAT.PcpDecider) (R : Polynomial ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {W X : ℕ}, ParamsBound PD R → ∀ (lam mu sigma n d : ℕ), 1 ≤ X → arQ lam mu n ≤ W → sigma ≤ W → n ≤ W → d ≤ W → Pipeline.PDom W X mu c m e (CL.Detyping.graphDim ArTy + (d + Pcp.pcpDim (arPar PD lam mu sigma n) * (arPar PD lam mu sigma n).k))

The detyped sampler's dimension is dominated.

theorem MIPRE.AnswerReduction.pow_le_pow_of_le {W K c m C M : ℕ} (hc : c ≤ C) (hm : m ≤ M) : (c * (W + 1) ^ m) ^ (K + 1) ≤ (C * (W + 1) ^ M) ^ (K + 1)

A monomial bound below the output bound.

theorem MIPRE.AnswerReduction.arVerifier_bounds (PD : SAT.PcpDecider) (R : Polynomial ℕ) (ℓ : ℕ) (hR : ParamsBound PD R) : ∃ (bound : Polynomial ℕ) (deg : ℕ), (∀ (V : Verifier (ℓ + 1)) (lam mu sigma n : ℕ), V.Within n (inBudget lam mu n) → V.size ≤ sigma → (arVerifier PD lam mu sigma V).Within n (Budget.uniform (outBound bound lam mu sigma n) (outDegree deg mu))) ∧ ∀ (lam mu sigma n : ℕ), cutVal (arPar PD lam mu sigma n) ≤ outBound bound lam mu sigma n

The output bounds of answer reduction: the complexity clause (arVerifier_within), and the answer cut below the same output bound, which completeness needs.

theorem MIPRE.AnswerReduction.arVerifier_within (PD : SAT.PcpDecider) (R : Polynomial ℕ) (ℓ : ℕ) (hR : ParamsBound PD R) : ∃ (bound : Polynomial ℕ) (deg : ℕ), ∀ (V : Verifier (ℓ + 1)) (lam mu sigma n : ℕ), V.Within n (inBudget lam mu n) → V.size ≤ sigma → (arVerifier PD lam mu sigma V).Within n (Budget.uniform (outBound bound lam mu sigma n) (outDegree deg mu))

The complexity clause of answer reduction (within of the AnswerReduction contract): an input within inBudget λ μ n with |𝒮|, |𝒟| ≤ σ gives an output within outBound bound λ μ σ n at degree outDegree deg μ, rejecting longer answers, for a polynomial bound and a degree deg depending only on the PCP.