The quantum value is approximable from below: the val* half of lem:value-lower-approx

MIPRE.ValueApprox.rePred_lt_quantumValue: the set of pairs (g, p / q) of a game description and a nonnegative rational threshold with val*(G_g) > p / q is recursively enumerable, in Mathlib's sense (REPred, the domain of a partial computable function).

The procedure is the one of statement (S) in the paper's proof of cor:mip-re, with exact candidates: dovetail over the raw candidates r (RawStrategy, a Primcodable type) and halt on the first that passes the primitive recursive check Check g p q r. Some candidate passes iff p / q < val*(G_g) (exists_check_iff), so the search halts exactly on the members of the set; the boundary case val* = p / q is correctly non-halting.

Thresholds are nonnegative rationals given as fractions p / q of naturals, as in the paper's (S) (t ∈ [0, 1]); a negative threshold is trivial, since val* ≥ 0. For q = 0 the real number p / q is 0, and the check tests 0 < val* accordingly.

theorem MIPRE.ValueApprox.REPred.of_primrecRel_exists {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : α → β → Prop} (hp : PrimrecRel p) : REPred fun (a : α) => ∃ (b : β), p a b

A predicate of the form ∃ b, p a b with p primitive recursive is recursively enumerable: search over the codes of b.

theorem MIPRE.ValueApprox.rePred_lt_quantumValue : REPred fun (x : HaltingGameValue.GameData × ℕ × ℕ) => ↑x.2.1 / ↑x.2.2 < quantumValue x.1.game

The quantum value from below (the val* half of lem:value-lower-approx): the pairs (g, (p, q)) with p / q < val*(G_g) form a recursively enumerable set.