An almost optimal action is near one passing Checks 1–3

Paper I, the soundness of Theorem I:2126 up to Proposition I:2279: Propositions I:2267 (perturbation) and I:2283 (significance), combined through the robustness claim I:1480. If a finite action σ has value at least 1 - ε in the associated test assocTest g, some finite action σ' passes Checks 1–3 at every point and has value at least 1 - 300 (Λ + 1)⁴ 2^{4(Λ + 1)} ε, Λ = g.ansLen (exists_checks_of_value).

The proof: σ' is the perturbation (MIPRE/Tailored/Sofic/Perturb.lean) of the doubled action τ = σ ⊕ σ, which has the same value. Writing Lose = Σ_{x,y} w(x, y) · #{points failing the challenge at (x, y)}, the value bound says Lose ≤ ε |τ| W. J₀ fixes, and J₀² moves, no more points than fail any challenge, so d(J₂, J₀) ≤ 3 Lose / W. At the vertex x, every relation of Checks 1–3 fails at no more points than fail the challenge at (x, y) or at (y, x), so weighting by m(x) = Σ_y (w(x, y) + w(y, x)) gives m(x) · #bad(x) ≤ (Λ² + 3Λ) D_x + 3Λ m(x) d(J₂, J₀) with Σ_x D_x = 2 Lose. The significance of X(x, i) carries the factor m(x) / W (sig_genX_le), which turns these per-vertex bounds into a bound in terms of Lose, and so of ε. These are the paper's per-vertex losing probabilities ε_x, with m(x) ε_x = D_x / |τ|.

Reindexing the generators

theorem MIPRE.Tailored.Sofic.sum_gens {g : TailoredGameValue.TailoredGameData} (F : ℕ → ℝ) : ∑ k : Fin (nGen g), F ↑k = F genJ + ∑ x ∈ Finset.range (g.nV + 1), ∑ i ∈ Finset.range g.ansLen, F (genX g x i)

The generators are J and the X(x, i), x ≤ nV, i < Λ.

The losing mass

def MIPRE.Tailored.Sofic.lose (g : TailoredGameValue.TailoredGameData) (τ : SubgroupTestValue.FiniteAction (nGen g)) : ℕ

The weighted number of (challenge, point) pairs failing: Lose = Σ_{x,y} w(x, y) · #fail.

Equations

• MIPRE.Tailored.Sofic.lose g τ = ∑ x ∈ Finset.range (g.nV + 1), ∑ y ∈ Finset.range (g.nV + 1), MIPRE.Tailored.Sofic.qw g x y * MIPRE.Tailored.Sofic.npass τ g x y

theorem MIPRE.Tailored.Sofic.one_sub_value {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) : 1 - (assocTest g).value τ = ↑(lose g τ) / (↑τ.N * ↑(qwTot g))

theorem MIPRE.Tailored.Sofic.lose_le {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) {ε : ℝ} (h : 1 - ε ≤ (assocTest g).value τ) : ↑(lose g τ) ≤ ε * ↑τ.N * ↑(qwTot g)

theorem MIPRE.Tailored.Sofic.mul_qwTot_le_lose {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) {c : ℕ} (h : ∀ (x y : ℕ), c ≤ npass τ g x y) : c * qwTot g ≤ lose g τ

A count bounded by every challenge's failures is bounded by Lose / W.

theorem MIPRE.Tailored.Sofic.diffCard_J₂_mul_le {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) (S : SwapData τ) : diffCard (J₂ τ S) (J₀ τ) * qwTot g ≤ 3 * lose g τ

def MIPRE.Tailored.Sofic.loseAt (g : TailoredGameValue.TailoredGameData) (τ : SubgroupTestValue.FiniteAction (nGen g)) (x : ℕ) : ℕ

The weighted failures at the vertex x.

Equations

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

theorem MIPRE.Tailored.Sofic.sum_loseAt {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) : ∑ x ∈ Finset.range (g.nV + 1), loseAt g τ x = 2 * lose g τ

theorem MIPRE.Tailored.Sofic.mdeg_mul_bad_le {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) (S : SwapData τ) {x : ℕ} (hx : x < g.nV + 1) : mdeg g x * badX τ S x ≤ (g.ansLen ^ 2 + 3 * g.ansLen) * loseAt g τ x + 3 * g.ansLen * diffCard (J₂ τ S) (J₀ τ) * mdeg g x

The weighted distance

theorem MIPRE.Tailored.Sofic.weighted_dist_le {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) (S : SwapData τ) : ∑ k : Fin (nGen g), sig (assocTest g) ↑k * dH (τ.σ k) (ρPert τ S k) ≤ ↑(sigBound g) * ↑(diffCard (J₂ τ S) (J₀ τ)) / ↑τ.N + ↑g.ansLen * (↑(sigBound g) * 2 ^ (g.ansLen + 1) / (↑(qwTot g) * ↑τ.N)) * ∑ x ∈ Finset.range (g.nV + 1), ↑(mdeg g x) * ↑(badX τ S x)

The significance-weighted distance from τ to its perturbation, generator by generator: J contributes sig(J) d(J₂, J₀), the variables at x at most Λ times sig(X(x, ·)) · 2^{Λ+1} #bad(x) / |τ|.

theorem MIPRE.Tailored.Sofic.value_perturbed_ge {g : TailoredGameValue.TailoredGameData} (τ : SubgroupTestValue.FiniteAction (nGen g)) (S : SwapData τ) {ε : ℝ} (h : 1 - ε ≤ (assocTest g).value τ) : 1 - (1 + ↑(sigBound g) * (3 + 2 ^ (g.ansLen + 1) * (2 * ↑g.ansLen ^ 3 + 24 * ↑g.ansLen ^ 2))) * ε ≤ (assocTest g).value (perturbed τ S)

Perturbation and robustness combined: if τ has value at least 1 - ε, its perturbation has value at least 1 - sigBound · ε (3 + 2^{Λ+1}(2Λ³ + 24Λ²)).

theorem MIPRE.Tailored.Sofic.numeric_bound (L : ℕ) : 1 + ↑((2 * L + 4) * (3 + 8 * L + 2 * L ^ 2 + 2 * 4 ^ L)) * (3 + 2 ^ (L + 1) * (2 * ↑L ^ 3 + 24 * ↑L ^ 2)) ≤ 300 * (↑L + 1) ^ 4 * 2 ^ (4 * (L + 1))

1 + sigBound · (3 + 2^{Λ+1}(2Λ³ + 24Λ²)) ≤ 300 (Λ + 1)⁴ 2^{4(Λ + 1)}.

def MIPRE.Tailored.Sofic.Cp : ℝ

The constant of exists_checks_of_value.

Equations

• MIPRE.Tailored.Sofic.Cp = 300

theorem MIPRE.Tailored.Sofic.exists_checks_of_value (g : TailoredGameValue.TailoredGameData) (σ : SubgroupTestValue.FiniteAction (nGen g)) (ε : ℝ) (h : 1 - ε ≤ (assocTest g).value σ) : ∃ (σ' : SubgroupTestValue.FiniteAction (nGen g)), Checks g σ' ∧ 1 - Cp * (↑g.ansLen + 1) ^ 4 * 2 ^ (4 * (g.ansLen + 1)) * ε ≤ (assocTest g).value σ'

An action of value ≥ 1 - ε in the associated test is near one passing Checks 1–3 (Propositions I:2267 and I:2283 with Claim I:1480): some finite action passes Checks 1–3 at every point and has value at least 1 - Cp (Λ + 1)⁴ 2^{4(Λ + 1)} ε, Λ = g.ansLen, Cp = 300.