The sofic value is not approximable, from a halting reduction to tailored games

The argument of Corollary I:2144 without the measure side. Suppose a computable f approximates the sofic value of every test to within 1/(k+1), and let g be a computable reduction from the halting problem to tailored games (TailoredGameValue.TailoredHaltingReduction). Main Theorem II separates the associated tests of the two kinds of games:

• a halting machine gives a game with a perfect ZPC strategy, whose test has sofic value 1;
• a non-halting machine gives a game of value at most 1/2, whose test has sofic value at most 1 − 1/(2K), with K = K(Λ) a computable function of the answer length.

Approximating to within 1/(4K + 1) tells the two apart, which decides the halting problem. not_sofValueApproximable_of takes the two clauses of Main Theorem II as hypotheses, in the form MainTheoremII K.

structure MIPRE.Tailored.Sofic.MainTheoremII (K : ℕ → ℕ) : Prop

The two clauses of Main Theorem II (Theorem I:2126) in the form the corollary uses, for a gap function K of the answer length: perfect ZPC games have tests of sofic value 1, and games of synchronous value at most 1/2 have tests of sofic value at most 1 − 1/(2K(Λ)).

• one_le (Λ : ℕ) : 1 ≤ K Λ
• complete (g : TailoredGameValue.TailoredGameData) : g.HasPerfectZPC → (assocTest g).valSof = 1
• sound (g : TailoredGameValue.TailoredGameData) : HaltingGameValue.gameValue g.toGame ≤ 1 / 2 → (assocTest g).valSof ≤ 1 - 1 / (2 * ↑(K g.ansLen))

theorem MIPRE.Tailored.Sofic.le_iff_of_gap {v : ℝ} {K F : ℕ} (hK : 1 ≤ K) (happ : |v - ↑F / (↑(4 * K) + 1)| ≤ 1 / (↑(4 * K) + 1)) : (v = 1 → 4 * K ≤ F) ∧ (v ≤ 1 - 1 / (2 * ↑K) → F < 4 * K)

The decision: approximating at k = 4K lands at or above k/(k+1) exactly for the tests of sofic value 1.

theorem MIPRE.Tailored.Sofic.not_sofValueApproximable_of {K : ℕ → ℕ} (hK : Primrec K) (hMT : MainTheoremII K) (hred : TailoredGameValue.TailoredHaltingReduction) : ¬SubgroupTestValue.SofValueApproximable

The sofic value is not approximable (the measure-free part of Corollary I:2144): from a halting reduction to tailored games and Main Theorem II with a primitive recursive gap function, no computable function approximates the sofic value of every subgroup test.