Soundness of the answer reduction: the error chain

Slice P4i of planning/aldous-lyons-track.md: the soundness error 24 √(errAR (16⁹ ε)) of the answer-reduced verifier (valStar_sound_output), at the parameters of ArParams, is below the contract's loss δ(ε, n) = σ^a ((λn)^{μa} ε^b + (λn)^{-μb}) (exists_errAR_le_delta), and the field-size hypotheses of valStar_sound_output hold (field_hyps).

The chain, with j the selector width, t the field width and m the PCP's variable count:

1. every role's number of codewords is at most 11 m + 11 (length_slotsOf_le), and m < 2^j;

2. errAR(θ) ≤ 2^j (250 D + 25920 θ + 4 d / q) for D above the three roles' δ_sim (errAR_le_of_dS), and each δ_sim is at most P (9 · 16⁹ ε^{clB} + q^{-clB} + 2^{-clB Q}) with P = 2^{3A (j + 5)}, A = ⌈simA⌉ (dS_le_of), since Q ≤ m < 2^j;

3. when t ≥ e2Min (j + Q + 1), e2Min = 400000 (3A + 2), the field terms 2^j P q^{-clB} and 2^j / q are at most 2^{-(2Q + 9)} (field_term_le), so (errAR_le_shape)

   errAR(16⁹ ε) ≤ 7 (39204 · 16⁹ G ε^{clB} + (Q + 1)^{-2} + 22 G 2^{-clB Q}), G = 2 · 2^j P,

   which is the shape MIPRE.AnswerReduction.sqrt_le_delta compares with the loss;

4. at the parameters, m ≤ errCM (Q σ)^{errPM} (pL_m_le), from the window describer's bounds on r₀ and s₀, so G ≤ (96 m)^{3A + 1} ≤ errCc (Q σ)^{errPp} (gN_le_poly), and the threshold of exists_threshold_clB gives C.

The field-width constant e2Min depends only on simA, while a and C depend on E₁ and c₀ through errCM. The case ε ≥ 1 or μ = 0 is the trivial one: the loss is then at least 1 (one_le_delta_of_trivial'); errAR_le_delta_or packages both.

The number of codewords

theorem MIPRE.Tailored.AnsRed.Typed.length_slotsOf_le (L : PcpDims) (r : Role) : (slotsOf L r).length ≤ 11 * L.m + 11

Every role has at most 11 m + 11 codewords.

The error, in terms of the extractions' errors

theorem MIPRE.Tailored.AnsRed.Typed.errAR_le_of_dS {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {L : PcpDims} {θ D : ℝ} (hθ : 0 ≤ θ) (hD : ∀ (r : Role), dS t ht j d L r (9 * θ) ≤ D) : errAR t ht j d L θ ≤ 2 ^ j * (250 * D + 25920 * θ + 4 * (↑d / ↑(Fintype.card (Fq t ht))))

The error is 2^j times the extractions' errors, up to constants.

One extraction's error

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.pwR (j : ℕ) : ℝ

The prefactor bound P = 2^{3A (j + 5)}, as a real number.

Equations

• MIPRE.Tailored.AnsRed.Typed.pwR j = ↑(2 ^ (j + 5)) ^ (3 * MIPRE.AnswerReduction.simAN)

theorem MIPRE.Tailored.AnsRed.Typed.one_le_pwR (j : ℕ) : 1 ≤ pwR j

theorem MIPRE.Tailored.AnsRed.Typed.dS_le_of {t : ℕ} {ht : 1 ≤ t} {j : ℕ} {L : PcpDims} (r : Role) {Q : ℕ} (hQ : Q ≤ 2 ^ j) (hm : L.m < 2 ^ j) {ε : ℝ} (hε : 0 ≤ ε) : dS t ht j 17 L r (9 * (16 ^ 9 * ε)) ≤ pwR j * (9 * 16 ^ 9 * ε ^ LIDT.clB) + pwR j * ↑(Fintype.card (Fq t ht)) ^ (-LIDT.clB) + pwR j * 2 ^ (-(LIDT.clB * ↑Q))

One extraction's error, at the typed failure 16⁹ ε and degree 17, when the PCP's variables fit the selector (m < 2^j) and Q ≤ 2^j.

The field terms

@[irreducible]

noncomputable def MIPRE.Tailored.AnsRed.Typed.e2Min : ℕ

The field-width constant: t ≥ e2Min (j + Q + 1) makes the field terms negligible. It depends only on simA.

Equations

• MIPRE.Tailored.AnsRed.Typed.e2Min = 400000 * (3 * MIPRE.AnswerReduction.simAN + 2)

theorem MIPRE.Tailored.AnsRed.Typed.e2Min_def : e2Min = 400000 * (3 * AnswerReduction.simAN + 2)

theorem MIPRE.Tailored.AnsRed.Typed.seven_le_e2Min : 7 ≤ e2Min

theorem MIPRE.Tailored.AnsRed.Typed.field_term_le {t j Q : ℕ} (hT : e2Min * (j + Q + 1) ≤ t) : 2 ^ j * pwR j * ↑(2 ^ t) ^ (-LIDT.clB) ≤ 1 / 2 ^ (2 * Q + 9) ∧ 2 ^ j * (1 / ↑(2 ^ t)) ≤ 1 / 2 ^ (2 * Q + 9)

The field terms: when t ≥ e2Min (j + Q + 1), 2^j P q^{-clB} ≤ 2^{-(2Q + 9)} and 2^j / q ≤ 2^{-(2Q + 9)}, at q = 2^t.

The shape of the error

noncomputable def MIPRE.Tailored.AnsRed.Typed.gN (j : ℕ) : ℕ

G = 2 · 2^j · 2^{3A (j + 5)}, the factor of the error's shape.

Equations

• MIPRE.Tailored.AnsRed.Typed.gN j = 2 * 2 ^ j * (2 ^ (j + 5)) ^ (3 * MIPRE.AnswerReduction.simAN)

theorem MIPRE.Tailored.AnsRed.Typed.shape_Q (Q : ℕ) : 318 * (1 / 2 ^ (2 * Q + 9)) ≤ 7 * (1 / (↑Q + 1) ^ 2)

318 · 2^{-(2Q + 9)} ≤ 7 / (Q + 1)².

theorem MIPRE.Tailored.AnsRed.Typed.shape_arith {X J P w E F ε qc q R : ℝ} (hX : X ≤ J * (250 * (P * (9 * 16 ^ 9 * w) + P * qc + P * E) + 25920 * (16 ^ 9 * ε) + 4 * (17 / q))) (hJ1 : 1 ≤ J) (hP1 : 1 ≤ P) (hw0 : 0 ≤ w) (hεw : ε ≤ w) (hE0 : 0 ≤ E) (hqc : J * P * qc ≤ F) (hqi : J * (1 / q) ≤ F) (hF : 318 * F ≤ 7 * R) : X ≤ 7 * (39204 * 16 ^ 9 * (2 * J * P) * w + R + 22 * (2 * J * P) * E)

The arithmetic of the error's shape.

theorem MIPRE.Tailored.AnsRed.Typed.errAR_le_shape {t : ℕ} {ht : 1 ≤ t} {j : ℕ} {L : PcpDims} {Q : ℕ} (hm : L.m < 2 ^ j) (hQ : Q ≤ L.m) (hT : e2Min * (j + Q + 1) ≤ t) {ε : ℝ} (hε : 0 ≤ ε) (hε1 : ε ≤ 1) : errAR t ht j 17 L (16 ^ 9 * ε) ≤ 7 * (39204 * ↑(16 ^ 9) * ↑(gN j) * ε ^ LIDT.clB + 1 / (↑Q + 1) ^ 2 + 22 * ↑(gN j) * 2 ^ (-(LIDT.clB * ↑Q)))

The shape of the error: at degree 17, when the PCP's variables fit the selector, Q ≤ m, and the field is wide (t ≥ e2Min (j + Q + 1)), errAR(16⁹ ε) has the shape MIPRE.AnswerReduction.sqrt_le_delta compares with the loss, with K = 16⁹ and G = gN j.

The field-size hypotheses

theorem MIPRE.Tailored.AnsRed.Typed.field_hyps (κ : Params.ArConsts) (hE : 7 ≤ κ.E₂) (lam mu sigma n : ℕ) : 2 * ((2 ^ Params.pJ κ lam mu sigma n + 1) * Params.pD) ≤ Fintype.card (Fq (Params.pTw κ lam mu sigma n) ⋯) ∧ 2 * ((Params.pL κ lam mu sigma n).m * chkDeg 5 Params.pD) ≤ Fintype.card (Fq (Params.pTw κ lam mu sigma n) ⋯)

The field-size hypotheses of valStar_sound_output hold at the parameters once E₂ ≥ 7: both sides are at most 2^{j + 8}, and t ≥ 7 (j + 2).

The size of the parameters

noncomputable def MIPRE.Tailored.AnsRed.Typed.wdC : ℕ

The constant of the window describer's bound on r₀.

Equations

• MIPRE.Tailored.AnsRed.Typed.wdC = ⋯.choose

noncomputable def MIPRE.Tailored.AnsRed.Typed.wdP : Polynomial ℕ

The polynomial of the window describer's bound on s₀.

Equations

• MIPRE.Tailored.AnsRed.Typed.wdP = ⋯.choose

theorem MIPRE.Tailored.AnsRed.Typed.r₀_le_wdC (T σ : ℕ) : SAT.windowDescriber.r₀ T σ ≤ wdC * (T.size + σ.size + 1)

theorem MIPRE.Tailored.AnsRed.Typed.s₀_le_wdP (n T Q σ : ℕ) : SAT.windowDescriber.s₀ n T Q σ ≤ Polynomial.eval (n.size + T.size + Q + σ) wdP

def MIPRE.Tailored.AnsRed.Typed.cW (κ : Params.ArConsts) : ℕ

The constant of the bound on the window describer's arguments.

Equations

• MIPRE.Tailored.AnsRed.Typed.cW κ = 43 * κ.E₁ + κ.c₀ + 60

noncomputable def MIPRE.Tailored.AnsRed.Typed.errCM (κ : Params.ArConsts) : ℕ

The constant of the bound on m.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.errPM : ℕ

The exponent of the bound on m.

Equations

• MIPRE.Tailored.AnsRed.Typed.errPM = 3 * MIPRE.Tailored.AnsRed.Typed.wdP.natDegree + 3

theorem MIPRE.Tailored.AnsRed.Typed.pQ_facts {lam mu n : ℕ} (hlam : 1 ≤ lam) (hmu : 1 ≤ mu) (hn : 1 ≤ n) : n + 1 ≤ Params.pQ lam mu n ∧ mu + 1 ≤ Params.pQ lam mu n

n < Q and μ < Q.

theorem MIPRE.Tailored.AnsRed.Typed.size_le_self (x : ℕ) : x.size ≤ x

theorem MIPRE.Tailored.AnsRed.Typed.pL_m_eq (κ : Params.ArConsts) (lam mu sigma n : ℕ) : (Params.pL κ lam mu sigma n).m = Params.pQ lam mu n + 1 + (Params.pQ lam mu n + 1) + (Params.pOW lam mu n + 1) + 3 * Params.pR κ lam mu sigma n + 6 + Params.pS κ lam mu sigma n

The PCP's variable count, unfolded.

theorem MIPRE.Tailored.AnsRed.Typed.pL_m_le (κ : Params.ArConsts) {lam mu sigma n : ℕ} (hlam : 1 ≤ lam) (hmu : 1 ≤ mu) (hs : 1 ≤ sigma) (hn : 1 ≤ n) : (Params.pL κ lam mu sigma n).m ≤ errCM κ * (Params.pQ lam mu n * sigma) ^ errPM

The PCP's variable count is polynomial: m ≤ errCM (Q σ)^{errPM}.

theorem MIPRE.Tailored.AnsRed.Typed.two_pow_pJ_le (κ : Params.ArConsts) (lam mu sigma n : ℕ) : 2 ^ Params.pJ κ lam mu sigma n ≤ 2 * (Params.pL κ lam mu sigma n).m + 1

2^j ≤ 2 m + 1.

theorem MIPRE.Tailored.AnsRed.Typed.gN_le {j m : ℕ} (hm1 : 1 ≤ m) (hj : 2 ^ j ≤ 2 * m + 1) : gN j ≤ (96 * m) ^ (3 * AnswerReduction.simAN + 1)

The factor of the error's shape is polynomial in m.

The constants of the loss

noncomputable def MIPRE.Tailored.AnsRed.Typed.errCc (κ : Params.ArConsts) : ℕ

The constant c of the polynomial bound G ≤ c Q^p σ^p.

Equations

• MIPRE.Tailored.AnsRed.Typed.errCc κ = (96 * MIPRE.Tailored.AnsRed.Typed.errCM κ) ^ (3 * MIPRE.AnswerReduction.simAN + 1)

noncomputable def MIPRE.Tailored.AnsRed.Typed.errPp : ℕ

The exponent p of the polynomial bound G ≤ c Q^p σ^p.

Equations

• MIPRE.Tailored.AnsRed.Typed.errPp = MIPRE.Tailored.AnsRed.Typed.errPM * (3 * MIPRE.AnswerReduction.simAN + 1)

noncomputable def MIPRE.Tailored.AnsRed.Typed.errA (κ : Params.ArConsts) : ℕ

The exponent a of the soundness loss. It depends on E₁ and c₀, not on E₂.

Equations

• MIPRE.Tailored.AnsRed.Typed.errA κ = MIPRE.AnswerReduction.aOf (MIPRE.Tailored.AnsRed.Typed.errCc κ) MIPRE.Tailored.AnsRed.Typed.errPp (16 ^ 9)

theorem MIPRE.Tailored.AnsRed.Typed.one_le_errA (κ : Params.ArConsts) : 1 ≤ errA κ

noncomputable def MIPRE.Tailored.AnsRed.Typed.errC (κ : Params.ArConsts) : ℕ

The threshold C of the soundness loss: past it, 2^{clB Q} beats the polynomial.

Equations

• MIPRE.Tailored.AnsRed.Typed.errC κ = ⋯.choose

theorem MIPRE.Tailored.AnsRed.Typed.gN_le_poly (κ : Params.ArConsts) {lam mu sigma n : ℕ} (hlam : 1 ≤ lam) (hmu : 1 ≤ mu) (hs : 1 ≤ sigma) (hn : 1 ≤ n) : ↑(gN (Params.pJ κ lam mu sigma n)) ≤ ↑(errCc κ) * ↑(Params.pQ lam mu n) ^ errPp * ↑sigma ^ errPp

The error below the loss

theorem MIPRE.Tailored.AnsRed.Typed.errAR_le_delta (κ : Params.ArConsts) (hE : e2Min ≤ κ.E₂) {lam mu sigma n : ℕ} {ε : ℝ} (hC : errC κ ≤ n) (hn2 : 2 ≤ n) (hlam : 1 ≤ lam) (hmu : 1 ≤ mu) (hs : 1 ≤ sigma) (hε : 0 < ε) (hε1 : ε ≤ 1) : 24 * √(errAR (Params.pTw κ lam mu sigma n) ⋯ (Params.pJ κ lam mu sigma n) Params.pD (Params.pL κ lam mu sigma n) (16 ^ 9 * ε)) ≤ AnswerReduction.delta (↑(errA κ)) (LIDT.clB / 2) lam mu sigma n ε

The soundness error is below the loss (ε ≤ 1, μ ≥ 1), past the threshold errC κ, with a = errA κ and b = clB / 2, when E₂ ≥ e2Min.

theorem MIPRE.Tailored.AnsRed.Typed.one_le_delta_of_trivial' (κ : Params.ArConsts) {lam mu sigma n : ℕ} {ε : ℝ} (hlam : 1 ≤ lam) (hn : 1 ≤ n) (hs : 1 ≤ sigma) (hε : 0 < ε) (h : mu = 0 ∨ 1 ≤ ε) : 1 ≤ AnswerReduction.delta (↑(errA κ)) (LIDT.clB / 2) lam mu sigma n ε

The loss is at least 1 when μ = 0 or ε ≥ 1, at a = errA κ, b = clB / 2.

theorem MIPRE.Tailored.AnsRed.Typed.errAR_le_delta_or (κ : Params.ArConsts) (hE : e2Min ≤ κ.E₂) {lam mu sigma n : ℕ} {ε : ℝ} (hC : errC κ ≤ n) (hn2 : 2 ≤ n) (hlam : 1 ≤ lam) (hs : 1 ≤ sigma) (hε : 0 < ε) : 24 * √(errAR (Params.pTw κ lam mu sigma n) ⋯ (Params.pJ κ lam mu sigma n) Params.pD (Params.pL κ lam mu sigma n) (16 ^ 9 * ε)) ≤ AnswerReduction.delta (↑(errA κ)) (LIDT.clB / 2) lam mu sigma n ε ∨ 1 ≤ AnswerReduction.delta (↑(errA κ)) (LIDT.clB / 2) lam mu sigma n ε

The soundness error against the loss, for every ε > 0 and μ: either the error is below the loss, or the loss is at least 1 (and the contract's conclusion is trivial).

theorem MIPRE.Tailored.AnsRed.Typed.exists_errAR_le_delta : ∃ (E₂₀ : ℕ), 7 ≤ E₂₀ ∧ ∀ (κ : Params.ArConsts) (hE1 : 1 ≤ κ.E₂), E₂₀ ≤ κ.E₂ → ∃ (a : ℝ) (b : ℝ) (C : ℕ), 1 ≤ a ∧ 0 < b ∧ b ≤ 1 ∧ (∀ (lam mu sigma n : ℕ) (ε : ℝ), C ≤ n → 2 ≤ n → 1 ≤ lam → 1 ≤ mu → 1 ≤ sigma → 0 < ε → ε ≤ 1 → 24 * √(errAR (Params.pTw κ lam mu sigma n) ⋯ (Params.pJ κ lam mu sigma n) Params.pD (Params.pL κ lam mu sigma n) (16 ^ 9 * ε)) ≤ AnswerReduction.delta a b lam mu sigma n ε) ∧ ∀ (lam mu sigma n : ℕ) (ε : ℝ), 1 ≤ n → 1 ≤ lam → 1 ≤ sigma → 0 < ε → mu = 0 ∨ 1 ≤ ε → 1 ≤ AnswerReduction.delta a b lam mu sigma n ε

The soundness error chain (P4i): a field-width threshold E₂₀ independent of κ, and for every κ past it, constants a ≥ 1, 0 < b ≤ 1 and a threshold C such that the error of valStar_sound_output is below the contract's loss δ(ε, n) for ε ≤ 1 and μ ≥ 1, and the loss is at least 1 otherwise.