The answer reduction's contract, from its routine

Slice P4i of planning/aldous-lyons-track.md: the output verifier of the routine arRoutine inhabits TailoredAnswerReduction 5 (tailoredAnswerReductionOf), given the two facts about the field the soundness clause needs: the field-size conditions of valStar_sound_output and the bound of its error 24 √(errAR (16⁹ ε)) by the contract's loss AnswerReduction.delta. Every other clause is proved here:

• the programs and the output are the routine's (arSamplerProg, lenPF, lpPF, output);
• the complexity clause is output_within at the routine's ParTime, the calculator's totality lenD_total;
• completeness is hasPerfectZPC_output at the honest PCPs' hypotheses (honestHyp_arRoutine), for λ, μ ≥ 1;
• soundness is valStar_sound_output and the error bound for μ ≥ 1; for μ = 0 the loss is at least 1 and there is nothing to prove.

theorem MIPRE.Tailored.AnsRed.Typed.one_le_delta_mu_zero {a b : ℝ} (ha : 0 ≤ a) {lam sigma n : ℕ} (hs : 1 ≤ sigma) {ε : ℝ} (hε : 0 < ε) : 1 ≤ AnswerReduction.delta a b lam 0 sigma n ε

At μ = 0 the loss is at least 1.

theorem MIPRE.Tailored.AnsRed.Typed.one_le_size {ℓ : ℕ} (V : TailoredVerifier ℓ) : 1 ≤ V.size

A verifier's description length is at least 1.

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.arOut (κ : Params.ArConsts) (hE : 1 ≤ κ.E₂) (V : TailoredVerifier 5) (lam mu sigma : ℕ) : TailoredVerifier 7

The output verifier of the routine, for a 5-level input.

Equations

• MIPRE.Tailored.AnsRed.Typed.arOut κ hE V lam mu sigma = (MIPRE.Tailored.AnsRed.Typed.arRoutine κ hE).output V lam mu sigma

noncomputable def MIPRE.Tailored.AnsRed.Typed.tailoredAnswerReductionOf (κ : Params.ArConsts) (hE : 1 ≤ κ.E₂) (hE₁ : 2 * lstarE ≤ κ.E₁) (hc₀ : κ.c₀ = lstarProgSize₀) (a b : ℝ) (C : ℕ) (ha : 1 ≤ a) (hb0 : 0 < b) (hb1 : b ≤ 1) (hq : ∀ (lam mu sigma n : ℕ), 2 * ((2 ^ Params.pJ κ lam mu sigma n + 1) * Params.pD) ≤ Fintype.card (Fq (Params.pTw κ lam mu sigma n) ⋯)) (hτ : ∀ (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) ⋯)) (herr : ∀ (lam mu sigma n : ℕ) (ε : ℝ), C ≤ n → 2 ≤ n → 1 ≤ lam → 1 ≤ sigma → 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 a b lam mu sigma n ε ∨ 1 ≤ AnswerReduction.delta a b lam mu sigma n ε) : TailoredAnswerReduction 5

The answer reduction's contract, from the routine, given the field-size conditions and the bound of the soundness error by the contract's loss, or the loss at least 1.

Equations

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

The constants

noncomputable def MIPRE.Tailored.AnsRed.Typed.arConsts : Params.ArConsts

The constants of the answer reduction: E₁ = 2E for the running time of L*, E₂ the field width's threshold of the soundness error, c₀ the size of L*'s program.

Equations

• MIPRE.Tailored.AnsRed.Typed.arConsts = { E₁ := 2 * MIPRE.Tailored.AnsRed.Typed.lstarE, E₂ := MIPRE.Tailored.AnsRed.Typed.e2Min, c₀ := MIPRE.Tailored.AnsRed.lstarProgSize₀ }

theorem MIPRE.Tailored.AnsRed.Typed.one_le_arConsts_E₂ : 1 ≤ arConsts.E₂

noncomputable def MIPRE.Tailored.AnsRed.Typed.tailoredAnswerReduction : TailoredAnswerReduction 5

Answer reduction for tailored verifiers (thm:tailored-ar, II:6883): the contract TailoredAnswerReduction 5 is inhabited.

Equations

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