The honest PCPs' hypotheses at the parameters of the answer reduction

Slice P4i of planning/aldous-lyons-track.md. At the parameters of ArParams.lean, the circuit of a seed is the window describer's description of the output indicator L* through its three windows, padded to the gate count s (arCirc); L* reads the parameters (ℓ, ◇) from the constant function arPrm. For an input verifier within the answer reduction's input budget inBudget λ μ n, with |𝒱| ≤ σ and λ, μ ≥ 1, these circuits satisfy the hypotheses of the honest PCPs (HonestHyp), at the description time T = 2^K (honestHyp_ar):

• the window and copy widths fit the input's lengths (at most 2^Q) and the constraints its processor outputs on readable answers (fewer than 2^{◇ - Q - 2}, from its running time);
• each circuit is well formed with the PCP's inputs, and describes L* within T: the describer's validity holds since Q, 2 log n ≤ T, L*'s program is at most σ' long, and the questions have at most Q bits; the windows fit T and the witness width r ≥ K + 2;
• L* accepts the honest strings within T.

Two facts about L* at constant parameters are hypotheses here, discharged where they are proved: its running time on accepted inputs (hTime, at a universal constant E with 2E ≤ E₁) and the size of its program (hSize, at the constant c₀ of σ').

Lengths of outputs

theorem MIPRE.Tailored.AnsRed.Params.length_spineList_le (d : Cost.Data) : d.spineList.length ≤ d.size

theorem MIPRE.Tailored.AnsRed.Params.length_bitsListD_le (d : Cost.Data) : d.bitsListD.length ≤ d.size

theorem MIPRE.Tailored.AnsRed.Params.lenOf_le {ℓ : ℕ} {V : TailoredVerifier ℓ} {n B : ℕ} (hB : LenBound V.len n B) (x : Cost.BitStr) (κ : Bool) : V.lenOf n x κ ≤ B

The length a calculator outputs is at most its bound.

theorem MIPRE.Tailored.AnsRed.Params.consOf_length_le {ℓ : ℕ} {V : TailoredVerifier ℓ} {n T k : ℕ} (hP : V.lp.TimeBoundAt n T k) (x y aR bR : Cost.BitStr) : (V.consOf n x y aR bR).length ≤ max 1 (T * ((Cost.encode (x, y, aR, bR)).size + 1) ^ k)

The constraints a processor outputs are at most its running time.

Arithmetic

theorem MIPRE.Tailored.AnsRed.Params.two_mul_le_two_pow {K : ℕ} (h : 1 ≤ K) : 2 * K ≤ 2 ^ K

theorem MIPRE.Tailored.AnsRed.Params.pOW_add_le_pK (κ : ArConsts) (lam mu n : ℕ) (h : 1 ≤ κ.E₁) : pOW lam mu n + pQ lam mu n + 4 ≤ pK κ lam mu n

theorem MIPRE.Tailored.AnsRed.Params.le_pQ (lam mu n : ℕ) (hlam : 1 ≤ lam) (hmu : 1 ≤ mu) : n + 1 ≤ pQ lam mu n

theorem MIPRE.Tailored.AnsRed.Params.pQ_lt_two_pow (lam mu n : ℕ) : pQ lam mu n < 2 ^ pQ lam mu n

theorem MIPRE.Tailored.AnsRed.Params.two_pow_ell_add_le (κ : ArConsts) (lam mu n : ℕ) (h : 1 ≤ κ.E₁) : 2 ^ (pEll lam mu n + 1) + 2 ^ (pOW lam mu n + 1) ≤ 2 * pT κ lam mu n

The windows fit the description time: 2^ℓ + 2^oW ≤ 2^K.

theorem MIPRE.Tailored.AnsRed.Params.pK_add_two_le_pR (κ : ArConsts) (lam mu sigma n : ℕ) : pK κ lam mu n + 2 ≤ pR κ lam mu sigma n

The witness width: K + 2 ≤ r.

The parameter function and the circuits

noncomputable def MIPRE.Tailored.AnsRed.Params.arPrm (lam mu n : ℕ) : Cost.PolyTimeFun ℕ (Cost.Unary × Cost.Unary)

The parameters of L* at the index: (ℓ, ◇), as a constant function.

Equations

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

@[simp]

theorem MIPRE.Tailored.AnsRed.Params.arPrm_apply (lam mu n m : ℕ) : (arPrm lam mu n).toFun m = (Cost.unary (pEll lam mu n), Cost.unary (pDm lam mu n))

noncomputable def MIPRE.Tailored.AnsRed.Params.arDescIn (κ : ArConsts) (lam mu sigma n : ℕ) (L P : Cost.Prog) (x y : Cost.BitStr) : SAT.Desc6Input

The input of the window describer at a seed: the three windows ℓ + 1, ℓ + 1, oW + 1, the program of L*, the index, T, Q, σ', and the two questions.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Params.arCirc (κ : ArConsts) (lam mu sigma n : ℕ) (L P : Cost.Prog) (x y : Cost.BitStr) : SAT.Circuit

The circuit of a seed: the description of L* through its windows, padded to s gates.

Equations

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

theorem MIPRE.Tailored.AnsRed.Params.one_le_pS (κ : ArConsts) (lam mu sigma n : ℕ) : 1 ≤ pS κ lam mu sigma n

theorem MIPRE.Tailored.AnsRed.Params.arCirc_wf (κ : ArConsts) (lam mu sigma n : ℕ) (L P : Cost.Prog) (x y : Cost.BitStr) : (arCirc κ lam mu sigma n L P x y).WellFormed

theorem MIPRE.Tailored.AnsRed.Params.arCirc_inputs (κ : ArConsts) (lam mu sigma n : ℕ) (L P : Cost.Prog) (x y : Cost.BitStr) : (arCirc κ lam mu sigma n L P x y).inputs = (pL κ lam mu sigma n).nIn

theorem MIPRE.Tailored.AnsRed.Params.arCirc_size (κ : ArConsts) (lam mu sigma n : ℕ) (L P : Cost.Prog) (x y : Cost.BitStr) : (arCirc κ lam mu sigma n L P x y).size = (pL κ lam mu sigma n).s

The honest PCPs' hypotheses

noncomputable def MIPRE.Tailored.AnsRed.Params.arCc {κ : ArConsts} {lam mu sigma n ℓV : ℕ} (V : TailoredVerifier ℓV) (z : V.Questions n) : SAT.Circuit

The circuits at the seeds of an input verifier.

Equations

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

theorem MIPRE.Tailored.AnsRed.Params.tableSize_pow {lam mu n : ℕ} : tableSize (2 ^ pEll lam mu n) (2 ^ pDm lam mu n) = 2 ^ pOW lam mu n

tableSize (2^ℓ) (2^◇) = 2^oW.

theorem MIPRE.Tailored.AnsRed.Params.esize_bitStr_le_pow {x : Cost.BitStr} {w : ℕ} (h : List.length x ≤ 2 ^ w) : Cost.esize x + 1 ≤ 4 * 2 ^ w + 2

An encoded bit string is at most 4 · 2^w once its length is at most 2^w.

theorem MIPRE.Tailored.AnsRed.Params.cons_le_ar {lam mu n ℓV : ℕ} {V : TailoredVerifier ℓV} (hV : V.Within n (AnswerReduction.inBudget lam mu n)) (x y : V.Questions n) (aR bR : Cost.BitStr) (haR : List.length aR ≤ (V.tgame n).lenR x) (hbR : List.length bR ≤ (V.tgame n).lenR y) : ((V.tgame n).cons x y aR bR).length * (2 ^ pEll lam mu n + 2 ^ pEll lam mu n) + (2 ^ pEll lam mu n + 2 ^ pEll lam mu n) ≤ 2 ^ pDm lam mu n

The constraint bound of the honest PCPs.

def MIPRE.Tailored.AnsRed.Params.LstarTime (E : ℕ) : Prop

L*'s running time on accepted inputs at constant parameters, at a constant E: the form in which the honest PCPs' time hypothesis is discharged.

Equations

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

def MIPRE.Tailored.AnsRed.Params.LstarSize (c₀ : ℕ) : Prop

The size of L*'s program at constant parameters, at the constant c₀.

Equations

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

theorem MIPRE.Tailored.AnsRed.Params.exists_lstarTime : ∃ (E : ℕ), 1 ≤ E ∧ LstarTime E

L*'s running time at constant parameters, at a universal constant (lstar_const_acceptsWithin_pow).

theorem MIPRE.Tailored.AnsRed.Params.lstarSize_lstarProgSize₀ : LstarSize lstarProgSize₀

The size of L*'s program at constant parameters (esize_lstarProg_const).

theorem MIPRE.Tailored.AnsRed.Params.acceptsWithin_mono {D : Decider} {m : ℕ} {x y a b : Cost.BitStr} {T T' : ℕ} (h : D.AcceptsWithin m x y a b T) (hT : T ≤ T') : D.AcceptsWithin m x y a b T'

theorem MIPRE.Tailored.AnsRed.Params.esize_arPrm_pair {lam mu n : ℕ} : Cost.esize (Cost.unary (pEll lam mu n), Cost.unary (pDm lam mu n)) = 2 * pEll lam mu n + 1 + (2 * pDm lam mu n + 1) + 1

theorem MIPRE.Tailored.AnsRed.Params.honestHyp_ar {κ : ArConsts} {lam mu sigma n E : ℕ} (hE₁ : 2 * E ≤ κ.E₁) (hE : 1 ≤ E) (hTime : LstarTime E) (hSize : LstarSize κ.c₀) {ℓV : ℕ} (V : TailoredVerifier ℓV) (hlam : 1 ≤ lam) (hmu : 1 ≤ mu) (hV : V.Within n (AnswerReduction.inBudget lam mu n)) (hsz : V.size ≤ sigma) : HonestHyp (pL κ lam mu sigma n) V n (arPrm lam mu n) (arCc V) (pT κ lam mu n)

The honest PCPs' hypotheses hold at the parameters of the answer reduction, for an input within the input budget with |𝒱| ≤ σ and λ, μ ≥ 1.