Main Theorem II, and the sofic value is not approximable from a halting reduction #

Theorem I:2126 for the tailored games of MIPRE/TailoredGameValue.lean, assembled from its two halves:

completeness (valSof_eq_one_of_hasPerfectZPC): a perfect ZPC strategy lifts to an action of value 1 (exists_value_one_of_hasPerfectZPC), and no action has value above 1;
soundness (gameValue_ge_of_valSof): an action of value 1 − ε is perturbed into one passing Checks 1–3 (exists_checks_of_value), whose quotient by J is a strategy for the game (gameValue_ge_of_checks), so the game's synchronous value is at least 1 − 600 (Λ+1)^4 2^{6(Λ+1)} ε, Λ the answer length.

So MainTheoremII holds with the gap function gapK Λ = 600 (Λ+1)^4 2^{6(Λ+1)}, which is primitive recursive, and not_sofValueApproximable_of gives not_sofValueApproximable: a halting reduction to tailored games makes the sofic value not approximable.

Values lie in `[0, 1]` #

source

theorem MIPRE.Tailored.Sofic.sum_mul_le_sum {l : List (ℕ × List SubgroupTestValue.Word × List (List (ℕ × Bool)))} (p : ℕ × List SubgroupTestValue.Word × List (List (ℕ × Bool)) → ℝ) (hp : ∀ (c : ℕ × List SubgroupTestValue.Word × List (List (ℕ × Bool))), p c ≤ 1) :

(List.map (fun (c : ℕ × List SubgroupTestValue.Word × List (List (ℕ × Bool))) => ↑c.1 * p c) l).sum ≤ (List.map (fun (x : ℕ × List SubgroupTestValue.Word × List (List (ℕ × Bool))) => ↑x.1) l).sum

source

theorem MIPRE.Tailored.Sofic.value_le_one (T : SubgroupTestValue.SubgroupTestData) (σ : SubgroupTestValue.FiniteAction T.nGen) :

T.value σ ≤ 1

No action has value above 1.

source

def MIPRE.Tailored.Sofic.trivialAction (n : ℕ) :

SubgroupTestValue.FiniteAction n

The trivial action, on one point.

Equations

MIPRE.Tailored.Sofic.trivialAction n = { N := 1, N_pos := Nat.one_pos, σ := fun (x : Fin n) => 1 }

Instances For

source

instance MIPRE.Tailored.Sofic.instNonemptyFiniteAction (n : ℕ) :

Nonempty (SubgroupTestValue.FiniteAction n)

source

theorem MIPRE.Tailored.Sofic.bddAbove_value (T : SubgroupTestValue.SubgroupTestData) :

BddAbove (Set.range T.value)

source

theorem MIPRE.Tailored.Sofic.valSof_le_one (T : SubgroupTestValue.SubgroupTestData) :

T.valSof ≤ 1

Main Theorem II #

source

theorem MIPRE.Tailored.Sofic.valSof_eq_one_of_hasPerfectZPC (g : TailoredGameValue.TailoredGameData) (h : g.HasPerfectZPC) :

(assocTest g).valSof = 1

Completeness of Main Theorem II (Theorem I:2126 (1)).

source

def MIPRE.Tailored.Sofic.CII :

ℝ

The constant of Main Theorem II's soundness.

Equations

MIPRE.Tailored.Sofic.CII = 600

Instances For

source

theorem MIPRE.Tailored.Sofic.gameValue_ge_of_valSof (g : TailoredGameValue.TailoredGameData) (ε : ℝ) (h : 1 - ε ≤ (assocTest g).valSof) :

1 - CII * (↑g.ansLen + 1) ^ 4 * 2 ^ (6 * (g.ansLen + 1)) * ε ≤ HaltingGameValue.gameValue g.toGame

Soundness of Main Theorem II (Theorem I:2126 (2)): a sofic value of at least 1 − ε gives a synchronous value of at least 1 − 600 (Λ+1)^4 2^{6(Λ+1)} ε.