Soundness of answer reduction

Piece AR-5f of planning/answer-reduction.md, concluded (lem:ar-soundness, lem:ar-error-assembly): the soundness clause of the AnswerReduction contract for arVerifier (arVerifier_soundness), under a new hypothesis on the PCP decider, FieldLarge: for every exponent e, its field eventually has at least (8 (Q + 1) m')^e elements.

The chain: a projective strategy of value at least 1 - ε for the answer-reduced verifier at the answer cut, in a bipartite model where the seeded CL test is sound, gives a typed strategy of failure θ ≤ 16^{54} ε (typedStrategy_value_ge), which gives ω(𝒱_n) ≥ 1 - 24 √(7 errE(θ)) (val_ge_of_typedGame) in every value model ω where oracularization is sound and which dominates the model. The combined error is bounded over the large field by errE_le, the size of the parameters by ParamsBound (z_le), and the result compared with δ(ε, n) by sqrt_le_delta, past a threshold on n (exists_threshold_clB): val_ge_of_arStrategy, at the explicit constants soundA, clB / 2, soundC.

The clause then holds, at the same constants, in every value model where oracularization is sound and which is approached by projective strategies of models it dominates where the seeded test is sound (LIDT.Simul.ApproxSoundIn, arVerifier_soundness_of_approx). So it holds in val* (arVerifier_soundness_tensor), a tensor-product strategy being a projective strategy in its tensor-product model, where the seeded test is sound; and in ω_co (arVerifier_soundness_commuting) given the seeded test's soundness in the commuting-operator model, ω_co being approached by projective strategies in the models of commuting-operator strategies. The output verifier rejects answers longer than the cut, so its value at any larger bound is the same; at μ = 0 or ε ≥ 1 the loss is at least 1 and there is nothing to prove.

def MIPRE.AnswerReduction.FieldLarge (PD : SAT.PcpDecider) : Prop

The PCP's field is eventually large: for every exponent e, past a threshold on Q, at least (8 (Q + 1) m')^e elements. At e = fieldExp the low-degree test's field term q^{-clB} then kills its prefactor, a polynomial of degree about 2 simA in m'. thm:pcp-decider does not carry the paper's lower bound on q (eq:pcp-q-choice); this is it, as a hypothesis on the decider, like ParamsBound and ShoupField. It asks for no particular constant, so a field of 2^{O(log² (Q m'))} elements satisfies it.

Equations

• MIPRE.AnswerReduction.FieldLarge PD = ∀ (e : ℕ), ∃ (Q₀ : ℕ), ∀ (n T Q σ : ℕ), Q₀ ≤ Q → (8 * ((Q + 1) * (PD.params n T Q σ).m')) ^ e ≤ (PD.params n T Q σ).q

The size of the parameters

def MIPRE.AnswerReduction.coeffSum (R : Polynomial ℕ) : ℕ

The coefficient sum of R.

Equations

• MIPRE.AnswerReduction.coeffSum R = ∑ i ∈ Finset.range (R.natDegree + 1), R.coeff i

def MIPRE.AnswerReduction.zC (R : Polynomial ℕ) : ℕ

The constant of the bound on Z = 8 (Q + 1) m'.

Equations

• MIPRE.AnswerReduction.zC R = 160 * (MIPRE.AnswerReduction.coeffSum R + 1) * 10 ^ R.natDegree

def MIPRE.AnswerReduction.zE (R : Polynomial ℕ) : ℕ

The exponent of the bound on Z.

Equations

• MIPRE.AnswerReduction.zE R = 2 * R.natDegree + 1

theorem MIPRE.AnswerReduction.one_le_arQ {lam mu n : ℕ} : 1 ≤ arQ lam mu n

theorem MIPRE.AnswerReduction.z_le (PD : SAT.PcpDecider) (R : Polynomial ℕ) (hR : ParamsBound PD R) {lam mu sigma n : ℕ} (hlam : 1 ≤ lam) (hmu : 1 ≤ mu) (hs : 1 ≤ sigma) (hn : 1 ≤ n) : 8 * ((arQ lam mu n + 1) * (arPar PD lam mu sigma n).m') ≤ zC R * (arQ lam mu n * sigma) ^ zE R

The parameters are polynomial: Z = 8 (Q + 1) m' ≤ zC (Q σ)^{zE}.

The soundness clause

@[reducible, inline]

abbrev MIPRE.AnswerReduction.kDet : ℕ

The detyping factor 16^{54}, as a natural number.

Equations

• MIPRE.AnswerReduction.kDet = 16 ^ Fintype.card MIPRE.AnswerReduction.ArTy

noncomputable def MIPRE.AnswerReduction.soundA (R : Polynomial ℕ) : ℕ

The exponent a of the soundness loss, which depends only on the parameter polynomial R.

Equations

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

theorem MIPRE.AnswerReduction.one_le_soundA (R : Polynomial ℕ) : 1 ≤ soundA R

noncomputable def MIPRE.AnswerReduction.soundC (PD : SAT.PcpDecider) (R : Polynomial ℕ) (hL : FieldLarge PD) : ℕ

The threshold C of the soundness clause: past the threshold of the error comparison (exists_threshold_clB) and past the one from which the PCP's field is large enough (FieldLarge at fieldExp). Explicit, so that the clause holds in each value model at the same constants (arVerifier_soundness_of_approx).

Equations

• MIPRE.AnswerReduction.soundC PD R hL = max ⋯.choose ⋯.choose

theorem MIPRE.AnswerReduction.sub_delta_le_of_one_le {ℓ : ℕ} (ω : ValueModel) {V : Verifier (ℓ + 1)} {n B : ℕ} {δ : ℝ} (h : 1 ≤ δ) : 1 - δ ≤ V.val ω n B

The loss is trivial at least 1: then there is nothing to prove, in any value model.

theorem MIPRE.AnswerReduction.one_le_delta_of_trivial {a : ℕ} (ha : 1 ≤ a) {lam mu sigma n : ℕ} {ε : ℝ} (hs1 : 1 ≤ sigma) (hN1 : 1 ≤ ↑lam * ↑n) (hε : 0 < ε) (h : mu = 0 ∨ 1 ≤ ε) : 1 ≤ delta (↑a) (LIDT.clB / 2) lam mu sigma n ε

The loss is at least 1 when μ = 0 or ε ≥ 1.

theorem MIPRE.AnswerReduction.val_ge_of_arStrategy (PD : SAT.PcpDecider) {ℓ : ℕ} (R : Polynomial ℕ) (hF : ShoupField PD) (hR : ParamsBound PD R) (hL : FieldLarge PD) {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hLD : LIDT.Simul.SoundIn M) {ω : ValueModel} (hω : ω.OracularSound) (hdom : ω.Dominates M) {V : Verifier (ℓ + 1)} {lam mu sigma n : ℕ} {ε : ℝ} (hC : soundC PD R hL ≤ n) (hn2 : 2 ≤ n) (hlam : 1 ≤ lam) (hV : V.Within n (inBudget lam mu n)) (hsz : V.decider.size ≤ sigma) (hε : 0 < ε) (hmu : 1 ≤ mu) (hε1 : ε < 1) (Rs : M.ProjStrat ((arVerifier PD lam mu sigma V).game n (cutVal (arPar PD lam mu sigma n)))) (hRs : 1 - ε ≤ Rs.value) : 1 - delta (↑(soundA R)) (LIDT.clB / 2) lam mu sigma n ε ≤ V.val ω n (inAns lam mu n)

Soundness of answer reduction, for a projective strategy in a bipartite model (lem:ar-error-assembly): in a model in which the low-individual-degree test is sound, a projective strategy of value at least 1 - ε for the answer-reduced verifier's game at the answer cut puts ω(𝒱_n) at least 1 - δ(ε, n), past the threshold, for every value model ω in which oracularization is sound and which dominates the model. The typed strategy fails with probability θ ≤ 16^{54} ε (typedStrategy_value_ge), which gives ω(𝒱_n) ≥ 1 - 24 √(7 errE(θ)) (val_ge_of_typedGame); the rest compares that with δ(ε, n), and is the same in every model.

theorem MIPRE.AnswerReduction.arVerifier_soundness_of_approx (PD : SAT.PcpDecider) {ℓ : ℕ} (R : Polynomial ℕ) (hF : ShoupField PD) (hR : ParamsBound PD R) (hL : FieldLarge PD) {ω : ValueModel} (hA : LIDT.Simul.ApproxSoundIn ω) (hω : ω.OracularSound) (V : Verifier (ℓ + 1)) (lam mu sigma n : ℕ) (ε : ℝ) (B : ℕ) (hC : soundC PD R hL ≤ n) (hn2 : 2 ≤ n) (hlam : 1 ≤ lam) (hV : V.Within n (inBudget lam mu n)) (hsz : V.decider.size ≤ sigma) (hε : 0 < ε) (hcut : cutVal (arPar PD lam mu sigma n) ≤ B) (hval : 1 - ε < (arVerifier PD lam mu sigma V).val ω n B) : 1 - delta (↑(soundA R)) (LIDT.clB / 2) lam mu sigma n ε ≤ V.val ω n (inAns lam mu n)

Soundness of answer reduction in a value model approached in sound models (lem:ar-soundness, at any answer bound above the answer cut), at the explicit constants soundA, clB / 2, soundC: 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), ω of the answer-reduced verifier above 1 - ε gives ω(𝒱_n) ≥ 1 - δ(ε, n), for n past the threshold. A projective strategy above 1 - ε in such a model carries the analysis (val_ge_of_arStrategy).

theorem MIPRE.AnswerReduction.arVerifier_soundness_tensor (PD : SAT.PcpDecider) {ℓ : ℕ} (R : Polynomial ℕ) (hF : ShoupField PD) (hR : ParamsBound PD R) (hL : FieldLarge PD) (V : Verifier (ℓ + 1)) (lam mu sigma n : ℕ) (ε : ℝ) (B : ℕ) (hC : soundC PD R hL ≤ n) (hn2 : 2 ≤ n) (hlam : 1 ≤ lam) (hV : V.Within n (inBudget lam mu n)) (hsz : V.decider.size ≤ sigma) (hε : 0 < ε) (hcut : cutVal (arPar PD lam mu sigma n) ≤ B) (hval : 1 - ε < (arVerifier PD lam mu sigma V).valStar n B) : 1 - delta (↑(soundA R)) (LIDT.clB / 2) lam mu sigma n ε ≤ V.valStar n (inAns lam mu n)

Soundness of answer reduction in the tensor-product value (lem:ar-soundness, the soundness clause of the AnswerReduction contract, at any answer bound above the answer cut), at the explicit constants soundA, clB / 2, soundC: val* of the answer-reduced verifier above 1 - ε gives val*(𝒱_n) ≥ 1 - δ(ε, n), for n past the threshold. A tensor-product strategy is a projective strategy in its tensor-product model, where the low-individual-degree test is sound (LIDT.Simul.approxSoundIn_tensor).

theorem MIPRE.AnswerReduction.arVerifier_soundness_commuting (PD : SAT.PcpDecider) {ℓ : ℕ} (R : Polynomial ℕ) (hF : ShoupField PD) (hR : ParamsBound PD R) (hL : FieldLarge PD) (hLD : LIDT.Simul.SoundCo) (V : Verifier (ℓ + 1)) (lam mu sigma n : ℕ) (ε : ℝ) (B : ℕ) (hC : soundC PD R hL ≤ n) (hn2 : 2 ≤ n) (hlam : 1 ≤ lam) (hV : V.Within n (inBudget lam mu n)) (hsz : V.decider.size ≤ sigma) (hε : 0 < ε) (hcut : cutVal (arPar PD lam mu sigma n) ≤ B) (hval : 1 - ε < (arVerifier PD lam mu sigma V).val ValueModel.commuting n B) : 1 - delta (↑(soundA R)) (LIDT.clB / 2) lam mu sigma n ε ≤ V.val ValueModel.commuting n (inAns lam mu n)

Soundness of answer reduction in the commuting-operator value (thm:ar-sound-co), at the same constants as in the tensor-product value, given the soundness of the low-individual-degree test in the commuting-operator model (LIDT.Simul.SoundCo, Phase 6 of planning/mipco-track.md): ω_co of the answer-reduced verifier above 1 - ε gives ω_co(𝒱_n) ≥ 1 - δ(ε, n), for n past the threshold. ω_co is approached by projective strategies in the models of commuting-operator strategies (LIDT.Simul.approxSoundIn_commuting).

theorem MIPRE.AnswerReduction.arVerifier_soundness (PD : SAT.PcpDecider) {ℓ : ℕ} (R : Polynomial ℕ) (hF : ShoupField PD) (hR : ParamsBound PD R) (hL : FieldLarge PD) : ∃ (a : ℝ) (b : ℝ) (C : ℕ), 1 ≤ a ∧ 0 < b ∧ b ≤ 1 ∧ ∀ (V : Verifier (ℓ + 1)) (lam mu sigma n : ℕ) (ε : ℝ) (B : ℕ), C ≤ n → 2 ≤ n → 1 ≤ lam → V.Within n (inBudget lam mu n) → V.decider.size ≤ sigma → 0 < ε → cutVal (arPar PD lam mu sigma n) ≤ B → 1 - ε < (arVerifier PD lam mu sigma V).valStar n B → 1 - delta a b lam mu sigma n ε ≤ V.valStar n (inAns lam mu n)

Soundness of answer reduction (lem:ar-soundness, the soundness clause of the AnswerReduction contract, at any answer bound above the answer cut): val* of the answer-reduced verifier above 1 - ε gives val*(𝒱_n) ≥ 1 - δ(ε, n), for n past a threshold, with a depending only on R and b = clB / 2 (arVerifier_soundness_tensor, at its explicit constants).