Answer reduction, supplied

Piece AR-6 of planning/answer-reduction.md (thm:answer-reduction): the AnswerReduction 5 contract, inhabited by arVerifier over the classical PCP decider (TM.CookLevin.Pad.classicalPcpDecider). The three hypotheses the construction and its analysis ask of the PCP decider hold for it:

• its field is the Shoup field (shoupField_classical), by definition;
• its parameters are polynomial in (log n, log T, Q, σ) (exists_paramsBound_classical): the padded dimension is, and the field degree is polylogarithmic in Q m';
• its field is eventually larger than every fixed power of 8 (Q + 1) m' (fieldLarge_classical), from the field degree's square term.

The contract's clauses are then arVerifier_bounds (the complexity clause and the answer cut below the output bound), arVerifier_hasPerfectPCC (completeness at the cut, hence at the bound) and arVerifier_soundness_tensor (at the output bound), at the explicit soundness constants soundA, clB / 2, soundC. At the same constants, the clause holds in every value model approached in models where the low-individual-degree test is sound (answerReduction_soundIn_of_approx), so in the commuting-operator value once the test is sound in the commuting-operator model (answerReduction_soundIn_commuting, Phase 3 of planning/mipco-track.md), or in every dyadic pair (answerReduction_soundIn_commuting_fin, Phase 6).

The classical PCP decider's hypotheses

theorem MIPRE.AnswerReduction.shoupField_classical : ShoupField TM.CookLevin.Pad.classicalPcpDecider

The classical PCP decider uses the Shoup field.

theorem MIPRE.AnswerReduction.exists_paramsBound_classical : ∃ (R : Polynomial ℕ), ParamsBound TM.CookLevin.Pad.classicalPcpDecider R

The classical PCP decider's parameters are polynomial.

theorem MIPRE.AnswerReduction.fieldLarge_classical : FieldLarge TM.CookLevin.Pad.classicalPcpDecider

The classical PCP decider's field is eventually large.

The constants

noncomputable def MIPRE.AnswerReduction.classicalR : Polynomial ℕ

The parameter polynomial of the classical PCP decider.

Equations

• MIPRE.AnswerReduction.classicalR = MIPRE.AnswerReduction.exists_paramsBound_classical.choose

theorem MIPRE.AnswerReduction.classicalR_spec : ParamsBound TM.CookLevin.Pad.classicalPcpDecider classicalR

theorem MIPRE.AnswerReduction.exists_bounds : ∃ (bound : Polynomial ℕ) (deg : ℕ), (∀ (V : Verifier (4 + 1)) (lam mu sigma n : ℕ), V.Within n (inBudget lam mu n) → V.size ≤ sigma → (arVerifier TM.CookLevin.Pad.classicalPcpDecider lam mu sigma V).Within n (Budget.uniform (outBound bound lam mu sigma n) (outDegree deg mu))) ∧ ∀ (lam mu sigma n : ℕ), cutVal (arPar TM.CookLevin.Pad.classicalPcpDecider lam mu sigma n) ≤ outBound bound lam mu sigma n

noncomputable def MIPRE.AnswerReduction.arBound : Polynomial ℕ

The output bound's polynomial.

Equations

• MIPRE.AnswerReduction.arBound = MIPRE.AnswerReduction.exists_bounds.choose

noncomputable def MIPRE.AnswerReduction.arDeg : ℕ

The output bound's degree.

Equations

• MIPRE.AnswerReduction.arDeg = MIPRE.AnswerReduction.arDeg._proof_1.choose

theorem MIPRE.AnswerReduction.arBounds_spec : (∀ (V : Verifier (4 + 1)) (lam mu sigma n : ℕ), V.Within n (inBudget lam mu n) → V.size ≤ sigma → (arVerifier TM.CookLevin.Pad.classicalPcpDecider lam mu sigma V).Within n (Budget.uniform (outBound arBound lam mu sigma n) (outDegree arDeg mu))) ∧ ∀ (lam mu sigma n : ℕ), cutVal (arPar TM.CookLevin.Pad.classicalPcpDecider lam mu sigma n) ≤ outBound arBound lam mu sigma n

noncomputable def MIPRE.AnswerReduction.arA : ℝ

The constant a of the soundness loss.

Equations

• MIPRE.AnswerReduction.arA = ↑(MIPRE.AnswerReduction.soundA MIPRE.AnswerReduction.classicalR)

noncomputable def MIPRE.AnswerReduction.arB : ℝ

The exponent b of the soundness loss.

Equations

• MIPRE.AnswerReduction.arB = MIPRE.LIDT.clB / 2

noncomputable def MIPRE.AnswerReduction.arC : ℕ

The threshold.

Equations

• MIPRE.AnswerReduction.arC = MIPRE.AnswerReduction.soundC MIPRE.TM.CookLevin.Pad.classicalPcpDecider MIPRE.AnswerReduction.classicalR MIPRE.AnswerReduction.fieldLarge_classical

theorem MIPRE.AnswerReduction.arSound_spec : 1 ≤ arA ∧ 0 < arB ∧ arB ≤ 1 ∧ ∀ (V : Verifier (4 + 1)) (lam mu sigma n : ℕ) (ε : ℝ) (B : ℕ), arC ≤ n → 2 ≤ n → 1 ≤ lam → V.Within n (inBudget lam mu n) → V.decider.size ≤ sigma → 0 < ε → cutVal (arPar TM.CookLevin.Pad.classicalPcpDecider lam mu sigma n) ≤ B → 1 - ε < (arVerifier TM.CookLevin.Pad.classicalPcpDecider lam mu sigma V).valStar n B → 1 - delta arA arB lam mu sigma n ε ≤ V.valStar n (inAns lam mu n)

The instance

noncomputable def MIPRE.AnswerReduction.answerReduction : AnswerReduction 5

Answer reduction (thm:answer-reduction), for 5-level inputs: arVerifier over the classical PCP decider.

Equations

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

Soundness in the commuting-operator value

theorem MIPRE.AnswerReduction.answerReduction_soundIn_of_approx {ω : ValueModel} (hA : LIDT.Simul.ApproxSoundIn ω) (hω : ω.OracularSound) : answerReduction.SoundIn ω

Answer reduction is sound in a value model approached in sound models, at the constants of answerReduction: in a value model where oracularization is sound and which is approached by projective strategies of models it dominates where the low-individual-degree test is sound (LIDT.Simul.ApproxSoundIn), arVerifier_soundness_of_approx at the output bound, which is above the answer cut.

theorem MIPRE.AnswerReduction.answerReduction_soundIn_commuting (hLD : LIDT.Simul.SoundCo) : answerReduction.SoundIn ValueModel.commuting

Answer reduction is sound in the commuting-operator value (thm:ar-sound-co), at the constants of answerReduction, given the soundness of the low-individual-degree test in the commuting-operator model: ω_co is approached in the models of commuting-operator strategies (LIDT.Simul.approxSoundIn_commuting).

theorem MIPRE.AnswerReduction.answerReduction_soundIn_commuting_fin (hV : CommutingFinitePairApprox) (h : LIDT.Simul.SoundFin) : answerReduction.SoundIn ValueModel.commuting

Answer reduction is sound in the commuting-operator value, from dyadic pairs (thm:ar-sound-co-fin), at the constants of answerReduction, given the soundness of the low-individual-degree test in every dyadic pair (LIDT.Simul.SoundFin) and the approximation of ω_co by projective strategies in dyadic pairs (CommutingFinitePairApprox): ω_co is then approached in dyadic pairs (LIDT.Simul.approxSoundIn_commuting_of_fin).