Documentation

MIPRE.Background.Tailored.AnswerReduction.ArInstance

The routine of the answer reduction, fixed #

Slice P4i of planning/aldous-lyons-track.md: the parameter routine of the answer-reduced verifier (ArRoutine) at the parameters of MIPRE/Tailored/AnsRed/ArParams.lean, for constants κ with E₂ ≥ 1 (arRoutine): the field and selector widths t, j, the degree 17, the PCP's dimensions, the parameter program arParCore and the circuit function arCircF at the builder lstarProgF of the output indicator's program. Its parameter program runs in polynomial time (arRoutine_parTime), and its circuits are those of the honest PCPs' hypotheses (arRoutine_circ), which hold for every input within the input budget (honestHyp_arRoutine).

source
noncomputable def MIPRE.Tailored.AnsRed.Typed.arFam (κ : Params.ArConsts) (hE : 1 ≤ κ.E₂) (lam mu sigma : ℕ) :
LdFamily

The field and selector widths at (λ, μ, σ).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def MIPRE.Tailored.AnsRed.Typed.arRoutine (κ : Params.ArConsts) (hE : 1 ≤ κ.E₂) :
    ArRoutine

    The routine of the answer reduction.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MIPRE.Tailored.AnsRed.Typed.arRoutine_params (κ : Params.ArConsts) (hE : 1 ≤ κ.E₂) (lam mu sigma n : ℕ) :
      (arRoutine κ hE).params lam mu sigma n = arParams (Params.pTw κ lam mu sigma n) (Params.pJ κ lam mu sigma n) Params.pD (Params.pL κ lam mu sigma n) (Params.pExtra κ lam mu sigma n)
      source
      theorem MIPRE.Tailored.AnsRed.Typed.arRoutine_parTime (κ : Params.ArConsts) (hE : 1 ≤ κ.E₂) :
      (arRoutine κ hE).ParTime

      The routine's parameter program runs in polynomial time.

      source
      theorem MIPRE.Tailored.AnsRed.Typed.arRoutine_circ (κ : Params.ArConsts) (hE : 1 ≤ κ.E₂) {ℓ : ℕ} (V : TailoredVerifier ℓ) (lam mu sigma n : ℕ) :
      (arRoutine κ hE).circ lam mu sigma n V = Params.arCc V

      The routine's circuits are those of the honest PCPs' hypotheses.

      source
      noncomputable def MIPRE.Tailored.AnsRed.Typed.lstarE :
      ℕ

      The constant of L*'s running time.

      Equations
      Instances For
        source
        theorem MIPRE.Tailored.AnsRed.Typed.one_le_lstarE :
        1 ≤ lstarE
        source
        theorem MIPRE.Tailored.AnsRed.Typed.lstarTime_lstarE :
        Params.LstarTime lstarE
        source
        theorem MIPRE.Tailored.AnsRed.Typed.honestHyp_arRoutine (κ : Params.ArConsts) (hE : 1 ≤ κ.E₂) (hE₁ : 2 * lstarE ≤ κ.E₁) (hc₀ : κ.c₀ = lstarProgSize₀) {ℓ : ℕ} (V : TailoredVerifier ℓ) {lam mu sigma n : ℕ} (hlam : 1 ≤ lam) (hmu : 1 ≤ mu) (hV : V.Within n (AnswerReduction.inBudget lam mu n)) (hsz : V.size ≤ sigma) :
        HonestHyp ((arRoutine κ hE).L lam mu sigma n) V n (Params.arPrm lam mu n) ((arRoutine κ hE).circ lam mu sigma n V) (Params.pT κ lam mu n)

        The honest PCPs' hypotheses hold for the routine's circuits, for an input within the input budget with |𝒱| ≤ σ and λ, μ ≥ 1, once E₁ ≥ 2E and c₀ is the size of L*'s program.