The PCP parameters of answer reduction, and the routine computing them

Pieces AR-3d and AR-3f of planning/answer-reduction.md. At index n, with the parameters (λ, μ, σ), answer reduction runs the PCP of a PcpDecider at pcpparams(n, T, Q, σ) with Q = (λn + 1)^μ the input sampler's budget and T = 2^{(Q + 5)(μ + 1)} (tPcp): an input decider within its budget 2^Q (|d| + 1)^μ accepts honest answers, of length at most 2^Q, within T steps, which is what the PCP's completeness asks. m and m' are powers of two, so this is a PcpFamily (family).

The routine parProg computes the family's parameters pd n from n, with (λ, μ, σ) hardcoded. Its budgets' routine budCore computes (Q, T): λ and n in unary (λ replaced by 0 at the index 0, where it is not needed, so that no step is longer than Q), Q by a power loop, μ in unary and T from both. Then the PCP's parameter program gives (k, m, s), and k, m, s are written in unary. parProg_runs is its correctness.

@[reducible, inline]

abbrev MIPRE.AnswerReduction.arQ (lam mu n : ℕ) : ℕ

The input sampler's budget Q = (λn + 1)^μ.

Equations

• MIPRE.AnswerReduction.arQ lam mu n = (lam * n + 1) ^ mu

@[reducible, inline]

abbrev MIPRE.AnswerReduction.tPcp (lam mu n : ℕ) : ℕ

The PCP's time bound T = 2^{(Q + 5)(μ + 1)}: an input decider running within 2^Q (|d| + 1)^μ on inputs of answers at most 2^Q long accepts within T.

Equations

• MIPRE.AnswerReduction.tPcp lam mu n = 2 ^ ((MIPRE.AnswerReduction.arQ lam mu n + 5) * (mu + 1))

def MIPRE.AnswerReduction.arPar (PD : SAT.PcpDecider) (lam mu sigma n : ℕ) : SAT.PcpParams

The PCP parameters at index n: pcpparams(n, T, Q, σ).

Equations

• MIPRE.AnswerReduction.arPar PD lam mu sigma n = PD.params n (MIPRE.AnswerReduction.tPcp lam mu n) (MIPRE.AnswerReduction.arQ lam mu n) sigma

theorem MIPRE.AnswerReduction.arPar_hk (PD : SAT.PcpDecider) (lam mu sigma n : ℕ) : 1 ≤ (arPar PD lam mu sigma n).k

theorem MIPRE.AnswerReduction.pow_size_sub_one {m : ℕ} (h : ∃ (j : ℕ), m = 2 ^ j) : m = 2 ^ (m.size - 1)

theorem MIPRE.AnswerReduction.size_sub_one_le {m k : ℕ} (h : ∃ (j : ℕ), m = 2 ^ j) (hd : m ∣ 2 ^ k) : m.size - 1 ≤ k

def MIPRE.AnswerReduction.family (PD : SAT.PcpDecider) (lam mu sigma : ℕ) : PcpFamily

The family of PCP parameters of answer reduction.

Equations

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

The routine

noncomputable def MIPRE.AnswerReduction.ParRoutine.hD : Cost.PolyTimeFun Cost.Data Cost.Data

The hardcoded (λ, μ, σ).

Equations

• MIPRE.AnswerReduction.ParRoutine.hD = MIPRE.Cost.PolyTimeFun.treeHead

noncomputable def MIPRE.AnswerReduction.ParRoutine.pre1 : Cost.PolyTimeFun Cost.Data Cost.Data

Stage 1: λ in unary, or 0 at the index 0, where λ is not needed and may be arbitrarily large. The input is X₀ = (λ, μ, σ), n.

Equations

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

noncomputable def MIPRE.AnswerReduction.ParRoutine.post1 : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data

Equations

• MIPRE.AnswerReduction.ParRoutine.post1 = MIPRE.Cost.PolyTimeFun.treePair.ap₂ MIPRE.Cost.PolyTimeFun.snd MIPRE.Cost.PolyTimeFun.fst

noncomputable def MIPRE.AnswerReduction.ParRoutine.pre2 : Cost.PolyTimeFun Cost.Data Cost.Data

Stage 2: n in unary; then the base λn + 1 and the exponent μ.

Equations

• MIPRE.AnswerReduction.ParRoutine.pre2 = MIPRE.Cost.PolyTimeFun.treePair.ap₂ (MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.Cost.PolyTimeFun.treeTail) (MIPRE.Cost.PolyTimeFun.id MIPRE.Cost.Data)

noncomputable def MIPRE.AnswerReduction.ParRoutine.post2 : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data

Equations

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

noncomputable def MIPRE.AnswerReduction.ParRoutine.pre3 : Cost.PolyTimeFun Cost.Data Cost.Data

Stage 3: Q = (λn + 1)^μ in unary, kept in front of the input.

Equations

• MIPRE.AnswerReduction.ParRoutine.pre3 = MIPRE.Cost.PolyTimeFun.id MIPRE.Cost.Data

noncomputable def MIPRE.AnswerReduction.ParRoutine.preMu : Cost.PolyTimeFun Cost.Data Cost.Data

Stage 4: μ in unary; then (Q, T) in binary, T = 2^{(Q + 5)(μ + 1)}.

Equations

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

noncomputable def MIPRE.AnswerReduction.ParRoutine.postBud : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data

Equations

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

noncomputable def MIPRE.AnswerReduction.ParRoutine.pre4 : Cost.PolyTimeFun Cost.Data Cost.Data

Stages 4, 5, 6: k, m, s in unary.

Equations

• MIPRE.AnswerReduction.ParRoutine.pre4 = MIPRE.Cost.PolyTimeFun.treePair.ap₂ MIPRE.Cost.PolyTimeFun.treeHead (MIPRE.Cost.PolyTimeFun.id MIPRE.Cost.Data)

noncomputable def MIPRE.AnswerReduction.ParRoutine.pre5 : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

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

noncomputable def MIPRE.AnswerReduction.ParRoutine.pre6 : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

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

noncomputable def MIPRE.AnswerReduction.ParRoutine.postKeep : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data

Equations

• MIPRE.AnswerReduction.ParRoutine.postKeep = MIPRE.Cost.PolyTimeFun.treePair.ap₂ MIPRE.Cost.PolyTimeFun.snd MIPRE.Cost.PolyTimeFun.fst

noncomputable def MIPRE.AnswerReduction.ParRoutine.budCore : Cost.Prog

The budgets' routine, on ((λ, μ, σ), n): (Q, T) in binary.

Equations

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

theorem MIPRE.AnswerReduction.ParRoutine.budCore_closed : Cost.Prog.WellScoped 1 budCore

noncomputable def MIPRE.AnswerReduction.ParRoutine.paramsP (PD : SAT.PcpDecider) : Cost.PolyTimeFun Cost.Data Cost.Data

The PCP's parameters (k, m, s), from ((Q, T), (λ, μ, σ), n).

Equations

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

noncomputable def MIPRE.AnswerReduction.ParRoutine.logU : Cost.PolyTimeFun ℕ Cost.Unary

log₂ of a power of two, from its binary encoding, in unary.

Equations

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

theorem MIPRE.AnswerReduction.ParRoutine.logU_apply (m : ℕ) : logU.toFun m = Cost.unary (m.size - 1)

def MIPRE.AnswerReduction.ParRoutine.timesU : ℕ → Cost.PolyTimeFun Cost.Unary Cost.Unary

c copies of a unary numeral.

Equations

• MIPRE.AnswerReduction.ParRoutine.timesU 0 = MIPRE.Cost.PolyTimeFun.const []
• MIPRE.AnswerReduction.ParRoutine.timesU c.succ = MIPRE.Cost.PolyTimeFun.append.ap₂ (MIPRE.AnswerReduction.ParRoutine.timesU c) (MIPRE.Cost.PolyTimeFun.id MIPRE.Cost.Unary)

theorem MIPRE.AnswerReduction.ParRoutine.timesU_apply (c : ℕ) (u : Cost.Unary) : (timesU c).toFun u = Cost.unary (c * List.length u)

noncomputable def MIPRE.AnswerReduction.ParRoutine.post6 : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data

Stage 6's post-processing: the parameters pd n. The context is (m, k, (k, m, s)) in unary and binary, the answer s in unary.

Equations

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

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

The routine's core, on ((λ, μ, σ), n): the budgets, the PCP's parameters, then k, m, s in unary.

Equations

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

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

theorem MIPRE.AnswerReduction.ParRoutine.seq_runs {p q : Cost.Prog} (hq : Cost.Prog.WellScoped 1 q) {x y r : Cost.Data} (hp : ∃ (t : ℕ), p.Runs x y t) (hq' : ∃ (t : ℕ), q.Runs y r t) : ∃ (t : ℕ), (Cost.seqProg p q).Runs x r t

theorem MIPRE.AnswerReduction.ParRoutine.bitsVal_pow (Q : ℕ) : Cost.bitsVal (List.replicate Q false ++ [true]) = 2 ^ Q

theorem MIPRE.AnswerReduction.ParRoutine.map_const_toFun {α : Type u_1} {β : Type u_2} [Cost.SizedEncoding α] [Cost.SizedEncoding β] (b : β) (l : List α) : List.map (Cost.PolyTimeFun.const b).toFun l = List.replicate l.length b

theorem MIPRE.AnswerReduction.ParRoutine.unary_mul_succ (a b : ℕ) : () :: Cost.unary (a * b) = Cost.unary (a * b + 1)

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

The parameter routine of answer reduction, with (λ, μ, σ) hardcoded.

Equations

• MIPRE.AnswerReduction.parProg PD lam mu sigma = MIPRE.Cost.hardcode (MIPRE.AnswerReduction.ParRoutine.core PD) (MIPRE.Cost.encode (lam, mu, sigma))

theorem MIPRE.AnswerReduction.parProg_closed (PD : SAT.PcpDecider) (lam mu sigma : ℕ) : Cost.Prog.WellScoped 1 (parProg PD lam mu sigma)

theorem MIPRE.AnswerReduction.post6_apply (PD : SAT.PcpDecider) (lam mu sigma n : ℕ) : ParRoutine.post6.toFun ((Cost.encode (Cost.unary (arPar PD lam mu sigma n).m)).cons ((Cost.encode (Cost.unary (arPar PD lam mu sigma n).k)).cons (Cost.encode ((arPar PD lam mu sigma n).k, (arPar PD lam mu sigma n).m, (arPar PD lam mu sigma n).s))), Cost.encode (Cost.unary (arPar PD lam mu sigma n).s)) = (family PD lam mu sigma).pd n

theorem MIPRE.AnswerReduction.budCore_runs (lam mu sigma n : ℕ) : ∃ (t : ℕ), ParRoutine.budCore.Runs ((Cost.encode (lam, mu, sigma)).cons (Cost.encode n)) (Cost.encode (arQ lam mu n, tPcp lam mu n)) t

The budgets' routine computes (Q, T).

theorem MIPRE.AnswerReduction.parCore_runs (PD : SAT.PcpDecider) (lam mu sigma n : ℕ) : ∃ (t : ℕ), (ParRoutine.core PD).Runs ((Cost.encode (lam, mu, sigma)).cons (Cost.encode n)) ((family PD lam mu sigma).pd n) t

The routine's core computes the parameters of the family, from ((λ, μ, σ), n).

theorem MIPRE.AnswerReduction.parProg_runs (PD : SAT.PcpDecider) (lam mu sigma n : ℕ) : ∃ (t : ℕ), (parProg PD lam mu sigma).Runs (Cost.encode n) ((family PD lam mu sigma).pd n) t

The routine computes the parameters of the family.