The commuting-operator instances: MIP^co ⊆ coRE, and MIP^co = coRE from co-soundness

The value model ValueModel.commuting (ω_co, Foundations/ValueModel.lean) is r.e. from above (ValueModel.commuting_upperRE, blueprint lem:valco-upper-re, through the Positivstellensatz certificates of Tsirelson/UpperRE.lean), which is the one fact about it the generic development needs. This module instantiates that development (planning/mipco-track.md, Phase 0):

• MIPCo.isCoRE: MIP^co ⊆ coRE (blueprint lem:mipco-sub-core), with no hypothesis — MIPClass.isCoRE at the upper semidecider, the role Lin's proof gives to the NPA hierarchy (Lin25, lem:MIPcoincoRE);
• Halting.halting_reduction_commuting_of: the halting reduction to ω_co (blueprint thm:halting-co) from a gap compression sound in the commuting-operator model (GapCompression.Sound ValueModel.commuting), which is halting_reduction_upper_of;
• Halting.core_subset_mipco_of, Halting.mipco_eq_core_of: MIP^co = coRE (blueprint thm:mipco-eq-core) from the same hypothesis. MIPRE/MIPCo.lean proves the hypothesis for gapCompressionCo, the main theorem's pipeline with the commuting-operator repetition constant, and so states them without it.

theorem MIPRE.MIPCo.isCoRE {L : Set Cost.BitStr} (h : MIPCo L) : IsCoRE L

MIP^co ⊆ coRE (blueprint lem:mipco-sub-core): the complement of a language in MIP^co is the preimage, under its computable map, of the set of descriptions with ω_co < 1, which the upper semidecider enumerates.

theorem MIPRE.MIPCo.exists_cosemidecider {L : Set Cost.BitStr} (h : MIPCo L) : ∃ (S : Cost.Prog), Cost.Prog.WellScoped 1 S ∧ ∀ (x : Cost.BitStr), Cost.Halts S (Cost.encode x) ↔ x ∉ L

The complement of a language in MIP^co is the halting set of a program of the ambient model.

theorem MIPRE.Halting.halting_reduction_commuting_of (G : GapCompression) (U : Cost.UniversalMachine) (hco : G.Sound ValueModel.commuting) : ValueModel.commuting.HaltingReductionCoRE

The halting reduction to the commuting-operator value (blueprint thm:halting-co), from a gap compression sound in the commuting-operator model: ω_co ≤ 1/2 on machines that halt on the empty input, ω_co = 1 on the others.

theorem MIPRE.Halting.core_subset_mipco_of (G : GapCompression) (U : Cost.UniversalMachine) (hco : G.Sound ValueModel.commuting) {L : Set Cost.BitStr} (h : IsCoRE L) : MIPCo L

coRE ⊆ MIP^co, from a gap compression sound in the commuting-operator model.

theorem MIPRE.Halting.mipco_eq_core_of (G : GapCompression) (U : Cost.UniversalMachine) (hco : G.Sound ValueModel.commuting) : MIPCo = IsCoRE

MIP^co = coRE (blueprint thm:mipco-eq-core), from a gap compression sound in the commuting-operator model.