Every Gaussian-rational exact strategy is a raw candidate

MIPRE.ValueApprox.exists_rawStrategy_interp_eq: an exact strategy whose entries lie in ℚ(i) is interp r for some raw candidate r — clear a common denominator k of the finitely many entries (exists_common_den) and list the numerators. With the correctness of the check (check_iff_interp) and the density and soundness of exact strategies (lt_quantumValue_iff), this gives exists_check_iff: some raw candidate passes Check g p q iff p / q < val*(G_g).

A common denominator

theorem MIPRE.ValueApprox.natCast_mul_ratCast_den (a : ℚ) : ↑a.den * ↑a = ↑a.num

theorem MIPRE.ValueApprox.exists_common_den (s : Finset ℂ) (hs : ∀ z ∈ s, z ∈ GaussianRat) : ∃ (k : ℕ), 0 < k ∧ ∀ z ∈ s, ∃ (w : GInt), ↑k * z = w.toC

Finitely many Gaussian rationals have a common denominator: some k ≥ 1 with k z ∈ ℤ[i] for all of them.

Reading off numerators

theorem MIPRE.ValueApprox.getD_ofFn {α : Type u_1} {n : ℕ} (f : Fin n → α) (i : Fin n) (d : α) : (List.ofFn f).getD (↑i) d = f i

(List.ofFn f).getD i d = f i for i : Fin n.

theorem MIPRE.ValueApprox.exists_rawStrategy_interp_eq {nX nA : ℕ} (c : ExactStrategy (Fin (nX + 1)) (Fin (nX + 1)) (Fin (nA + 1)) (Fin (nA + 1))) (hc : c.EntriesIn GaussianRat) : ∃ (r : RawStrategy), RawStrategy.interp nX nA r = c

Every exact strategy with Gaussian-rational entries is denoted by a raw candidate.

The semidecision procedure is correct

theorem MIPRE.ValueApprox.exists_check_iff (g : HaltingGameValue.GameData) (p q : ℕ) : (∃ (r : RawStrategy), Check g p q r) ↔ ↑p / ↑q < quantumValue g.game

Some raw candidate passes the check iff the quantum value of the described game exceeds p / q.