The parameters of the answer reduction

Slice P4i of planning/aldous-lyons-track.md: the parameters at which the output verifier of the answer reduction runs at an index n, from (λ, μ, σ) (II:10846–11074, in the form the formalization needs). With Q = (λn + 1)^μ the input's budget:

• the PCP's window width ℓ = Q: the input's answers have length at most 2^Q;
• its copy width ◇ = (μ + 2)(Q + 4): the input's processor runs within 2^Q (|d| + 1)^μ, so it outputs fewer than 2^{◇ - Q - 2} constraints on the answers the PCP reads;
• the output indicator's description time T = 2^K, K = E₁ (μ + 1)(oW + Q + 4), with oW = 2ℓ + 3◇ + 6 the width of the table O: L* accepts the honest strings within T;
• the size bound σ' = c₀ + 5σ + 4(ℓ + ◇) + 8 of the description of L*;
• the witness index width r = r₀(T, σ') and the gate count s = s₀(n, T, Q, σ') of the window describer (MIPRE.SAT.windowDescriber);
• the selector width j = size m, m = nIn + s the number of the PCP's variables, so m < 2^j;
• the degree d = 17;
• the field width t = E₂ (j + r + Q + 1), large enough for the soundness error.

The constants E₁, E₂ and c₀ are arguments (ArConsts); the bounds that fix them come later (the running time of L*, the error of the soundness, the size of L*'s program).

structure MIPRE.Tailored.AnsRed.Params.ArConsts : Type

The constants of the parameters: E₁ scales the description time's exponent, E₂ the field width, c₀ is the fixed part of the size of the output indicator's program.

• E₁ : ℕ
• E₂ : ℕ
• c₀ : ℕ

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Params.pQ (lam mu n : ℕ) : ℕ

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

Equations

• MIPRE.Tailored.AnsRed.Params.pQ lam mu n = (lam * n + 1) ^ mu

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Params.pEll (lam mu n : ℕ) : ℕ

The window width ℓ = Q.

Equations

• MIPRE.Tailored.AnsRed.Params.pEll lam mu n = MIPRE.Tailored.AnsRed.Params.pQ lam mu n

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Params.pDm (lam mu n : ℕ) : ℕ

The copy width ◇ = (μ + 2)(Q + 4).

Equations

• MIPRE.Tailored.AnsRed.Params.pDm lam mu n = (mu + 2) * (MIPRE.Tailored.AnsRed.Params.pQ lam mu n + 4)

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Params.pOW (lam mu n : ℕ) : ℕ

The width oW = 2ℓ + 3◇ + 6 of an index of the table O.

Equations

• MIPRE.Tailored.AnsRed.Params.pOW lam mu n = MIPRE.Tailored.AnsRed.Params.pEll lam mu n + MIPRE.Tailored.AnsRed.Params.pEll lam mu n + 3 * MIPRE.Tailored.AnsRed.Params.pDm lam mu n + 6

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Params.pK (κ : ArConsts) (lam mu n : ℕ) : ℕ

The exponent K = E₁ (μ + 1)(oW + Q + 4) of the description time.

Equations

• MIPRE.Tailored.AnsRed.Params.pK κ lam mu n = κ.E₁ * (mu + 1) * (MIPRE.Tailored.AnsRed.Params.pOW lam mu n + MIPRE.Tailored.AnsRed.Params.pQ lam mu n + 4)

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Params.pT (κ : ArConsts) (lam mu n : ℕ) : ℕ

The description time T = 2^K of the output indicator.

Equations

• MIPRE.Tailored.AnsRed.Params.pT κ lam mu n = 2 ^ MIPRE.Tailored.AnsRed.Params.pK κ lam mu n

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Params.pSig (κ : ArConsts) (lam mu sigma n : ℕ) : ℕ

The size bound σ' = c₀ + 5σ + 4(ℓ + ◇) + 8 of the output indicator's program.

Equations

• MIPRE.Tailored.AnsRed.Params.pSig κ lam mu sigma n = κ.c₀ + 5 * sigma + 4 * (MIPRE.Tailored.AnsRed.Params.pEll lam mu n + MIPRE.Tailored.AnsRed.Params.pDm lam mu n) + 8

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Params.pR (κ : ArConsts) (lam mu sigma n : ℕ) : ℕ

The witness index width r = r₀(T, σ').

Equations

• MIPRE.Tailored.AnsRed.Params.pR κ lam mu sigma n = MIPRE.SAT.windowDescriber.r₀ (MIPRE.Tailored.AnsRed.Params.pT κ lam mu n) (MIPRE.Tailored.AnsRed.Params.pSig κ lam mu sigma n)

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Params.pS (κ : ArConsts) (lam mu sigma n : ℕ) : ℕ

The gate count s = s₀(n, T, Q, σ').

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Params.pL (κ : ArConsts) (lam mu sigma n : ℕ) : PcpDims

The dimensions of the PCP.

Equations

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

@[simp]

theorem MIPRE.Tailored.AnsRed.Params.pL_ℓ (κ : ArConsts) (lam mu sigma n : ℕ) : (pL κ lam mu sigma n).ℓ = pEll lam mu n

@[simp]

theorem MIPRE.Tailored.AnsRed.Params.pL_dm (κ : ArConsts) (lam mu sigma n : ℕ) : (pL κ lam mu sigma n).dm = pDm lam mu n

@[simp]

theorem MIPRE.Tailored.AnsRed.Params.pL_r (κ : ArConsts) (lam mu sigma n : ℕ) : (pL κ lam mu sigma n).r = pR κ lam mu sigma n

@[simp]

theorem MIPRE.Tailored.AnsRed.Params.pL_s (κ : ArConsts) (lam mu sigma n : ℕ) : (pL κ lam mu sigma n).s = pS κ lam mu sigma n

theorem MIPRE.Tailored.AnsRed.Params.pL_oW (κ : ArConsts) (lam mu sigma n : ℕ) : (pL κ lam mu sigma n).oW = pOW lam mu n

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Params.pJ (κ : ArConsts) (lam mu sigma n : ℕ) : ℕ

The selector width j = size m.

Equations

• MIPRE.Tailored.AnsRed.Params.pJ κ lam mu sigma n = (MIPRE.Tailored.AnsRed.Params.pL κ lam mu sigma n).m.size

@[reducible, inline]

abbrev MIPRE.Tailored.AnsRed.Params.pD : ℕ

The degree d = 17.

Equations

• MIPRE.Tailored.AnsRed.Params.pD = 17

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Params.pTw (κ : ArConsts) (lam mu sigma n : ℕ) : ℕ

The field width t = E₂ (j + r + Q + 1).

Equations

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

def MIPRE.Tailored.AnsRed.Params.pExtra (κ : ArConsts) (lam mu sigma n : ℕ) : Cost.Data

The data of the circuit function: K and σ', in unary.

Equations

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

Basic facts

theorem MIPRE.Tailored.AnsRed.Params.one_le_pQ (lam mu n : ℕ) : 1 ≤ pQ lam mu n

theorem MIPRE.Tailored.AnsRed.Params.pL_m_lt (κ : ArConsts) (lam mu sigma n : ℕ) : (pL κ lam mu sigma n).m < 2 ^ pJ κ lam mu sigma n

m < 2^j.

theorem MIPRE.Tailored.AnsRed.Params.pL_m_le (κ : ArConsts) (lam mu sigma n : ℕ) : (pL κ lam mu sigma n).m ≤ 2 ^ pJ κ lam mu sigma n

m ≤ 2^j.

theorem MIPRE.Tailored.AnsRed.Params.pJ_le_pTw (κ : ArConsts) (lam mu sigma n : ℕ) (h : 1 ≤ κ.E₂) : pJ κ lam mu sigma n ≤ pTw κ lam mu sigma n

j ≤ t once E₂ ≥ 1.

theorem MIPRE.Tailored.AnsRed.Params.one_le_pTw (κ : ArConsts) (lam mu sigma n : ℕ) (h : 1 ≤ κ.E₂) : 1 ≤ pTw κ lam mu sigma n

1 ≤ t once E₂ ≥ 1.

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

Q ≤ K once E₁ ≥ 1.

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

oW ≤ K once E₁ ≥ 1.