The semidecider of the halting reduction (obligation O3)

Obligation O3 of the halting reduction (Halting/Reduction.lean) asks for a closed program halting on encode (x, n) exactly when the string x lies outside the class B at level n. By Verifier.not_inClassB_iff that is a disjunction of three Σ₁ statements — the verifier x denotes is not n-bounded, or its decider accepts some answer longer than the answer bound, or its n-th game has value more than 1/2 — and the obligation is an equivalence, so all three have to be recognized exactly.

The second disjunct is the tabulation's, and is O2's to supply: with a computable game description whose value is that of 𝒱_n, lem:value-lower-approx (MIPRE.ValueApprox.rePred_lt_quantumValue) enumerates the strategies. The first is proved here, and it is the part of O3 that O2 does not contain:

• Verifier.BoundViolation is a witness that λ-boundedness fails: an index and one input of the sampler or the decider at that index. The index is carried as a datum, not a number, so that the encoding encode m under which Decider.TimeBoundAt reads its input is primitive recursive in the witness (Data.encode_natOf); every index arises this way (Data.natOf_encode), so nothing is lost.
• Verifier.not_isBounded_iff_exists is the characterization: λ-boundedness fails exactly when some witness works. Each clause of def:lambda-bounded is a ∀, over indices and over inputs, so its negation is a search — and what makes the search effective is that Prog.HaltsWithin is decidable (Halting/CostBudget.lean), which needs the cost of a run and not only its length.
• Verifier.rePred_not_isBounded: hence, for a computably presented family of verifiers (Verifier.ComputablyPresented), the boundedness violation is recursively enumerable.
• Verifier.rePred_not_rejectsLong: the acceptance of a long answer is recursively enumerable too, by the same pattern with a simpler witness — the tuple and a step budget — and one budgeted run of the decider (Machine.runForD).
• Halting.exists_sem_of_tab merges the three disjuncts (REPred.or, by Partrec.merge') and hands the result to Cost.exists_semidecider_prod_nat, which is Cost.exists_semidecider on pair-encoded inputs. Out comes sem, sem_closed and sem_spec.

What was assumed, and what discharged it

exists_sem_of_tab takes the tabulation and the presentation of the family as hypotheses. Both are O2's: a GameData for 𝒱_n cannot be computed without the sampler's dimension and the two programs. Stating them rather than proving them keeps the mathematical content here — that the violation of a ∀-clause over an infinite index set is enumerable — independent of how the tabulation is built. Both are now supplied: Halting.computablyPresented_Vof at the end of this file, and Halting.tab_value in Halting/Instantiation.lean, so that Halting.exists_sem takes no hypotheses; halting_reduction (Halting/Reduction.lean, below this file in the import order) applies it directly, and Obligations has no O3 field.

Two things found in the writing, both recorded in planning/h4-assembly.md, and both since discharged — by different repairs. The findings are kept because they say where the seams were:

1. O3 is not "O2 plus a disjunction", as the plan and Obligations' docstring said. The hypothesis hval below asks the tabulation to have the value of 𝒱_n for every n-bounded verifier, and the match as it then stood gave that only for a verifier synchronous at n — because a GameData describes a synchronous game by construction (MIPRE.Verifier.isSynchronousAt_of_game_matches). Membership in B does not carry synchronicity, so the equivalence sem_spec demands was not available. Three ways out were on the record; the one taken is the doubled question set of Foundations/GameDouble.lean. MIPRE.Halting.tab_match now matches (Vof G U x).doubledGame, whose distribution puts no weight on the diagonal a GameData vetoes, and MIPRE.Halting.tab_value is hval on the nose — the equality, in both directions, at every n-bounded string.
2. Primrec fun n : ℕ => (encode n : Data) — natural numbers encode in binary (Nat.bits) — was missing and is a prerequisite of ComputablyPresented for the verifier a string denotes, hence of O2's tabulation too. It is now MIPRE.Cost.Data.primrec_encode_nat. The witness trick above is what kept this file from needing it in the first place.

Two closure properties of recursively enumerable predicates

theorem MIPRE.REPred.or {α : Type u_1} [Primcodable α] {p q : α → Prop} (hp : REPred p) (hq : REPred q) : REPred fun (a : α) => p a ∨ q a

A union of two r.e. predicates is r.e., by dovetailing (Partrec.merge'). Mathlib has the dovetailing but not this corollary of it.

theorem MIPRE.REPred.of_computable_exists {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] [Inhabited β] {test : α → β → Bool} (h : Computable fun (q : α × β) => test q.1 q.2) : REPred fun (a : α) => ∃ (b : β), test a b = true

A Σ₁ predicate is r.e.: an unbounded search for a witness passing a computable test. MIPRE.ValueApprox.REPred.of_primrecRel_exists is the same statement for a primitive recursive test; the tests here are only computable, the dimension of a compressed sampler being read off a run of its program.

The boundedness violation

theorem MIPRE.Cost.primrec_natLeB : Primrec fun (p : ℕ × ℕ) => decide (p.1 ≤ p.2)

≤ on naturals as a primitive recursive Bool-valued function. Primrec.nat_le is a PrimrecRel, which hides the Decidable instance behind an existential and so does not compose with Computable arguments; this is the same fact in usable form.

theorem MIPRE.Cost.primrec_optionDataEqB : Primrec fun (p : Option Data × Option Data) => decide (p.1 = p.2)

Equality on Option Data as a primitive recursive Bool-valued function, extracted from Primrec.eq the way primrec_natLeB extracts Primrec.nat_le.

structure MIPRE.Verifier.ComputablyPresented {α : Type u_1} [Primcodable α] {ℓ : ℕ} (V : α → Verifier ℓ) : Prop

A family of verifiers is computably presented when the two programs of V a and the dimension of its sampler are computable in a — the programs as the data that encode them, which is the form every computability statement of the ambient model takes.

This is what a computable tabulation of the games of the family needs anyway (MIPRE.Halting.tab_computable): the question weights come from running the sampler over 𝔽₂^{s(n)}, so s(n) has to be computed before anything else can be.

• samplerProg : Computable fun (a : α) => Cost.encode (V a).sampler.prog

  The sampler's program, as data.

• deciderProg : Computable fun (a : α) => Cost.encode (V a).decider.prog

  The decider's program, as data.

• dim : Computable fun (q : α × ℕ) => (V q.1).sampler.dim q.2

  The dimension s(n) of the sampler's ambient space, uniformly in a and n.

def MIPRE.Verifier.boundBudget (lam m : ℕ) (d : Cost.Data) : ℕ

The budget the time bounds of def:lambda-bounded allow at index m on the input d: m ^ λ · (|d| + 1) ^ λ, read off the shape of Decider.TimeBoundAt.

Equations

• MIPRE.Verifier.boundBudget lam m d = m ^ lam * (d.size + 1) ^ lam

def MIPRE.Verifier.BoundViolation {ℓ : ℕ} (V : Verifier ℓ) (lam : ℕ) (w : Cost.Data × Cost.Data) : Prop

A witness that λ-boundedness fails. The index at which a clause of def:lambda-bounded breaks is carried as a datum w.1 — read as the number Data.natOf w.1, so that the encoding encode (Data.natOf w.1) the two time bounds prepend to their input is Data.normBin w.1, primitive recursive in the witness — and w.2 is an input of the sampler or of the decider at that index on which the time bound fails.

Equations

• One or more equations did not get rendered due to their size.

def MIPRE.Verifier.boundViolationB {ℓ : ℕ} (V : Verifier ℓ) (lam : ℕ) (w : Cost.Data × Cost.Data) : Bool

The witness test, as a Bool: every clause of BoundViolation is decidable, the two time bounds by Machine.haltsWithinB (Halting/CostBudget.lean).

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Verifier.boundViolationB_iff {ℓ : ℕ} (V : Verifier ℓ) (lam : ℕ) (w : Cost.Data × Cost.Data) : V.boundViolationB lam w = true ↔ V.BoundViolation lam w

theorem MIPRE.Verifier.not_isBounded_iff_exists {ℓ : ℕ} (V : Verifier ℓ) (lam : ℕ) : ¬V.IsBounded lam ↔ ∃ (w : Cost.Data × Cost.Data), V.BoundViolation lam w

λ-boundedness fails exactly when some witness works. Each clause of def:lambda-bounded is a universal statement — over indices, and over the inputs of the two programs — so its negation is a search, and BoundViolation is what the search looks for.

The rejection of long answers, violated

def MIPRE.Verifier.LongAcceptance {ℓ : ℕ} (V : Verifier ℓ) (n T : ℕ) (w : (Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) × ℕ) : Prop

A witness that the decider accepts a long answer at index n: a tuple of two questions and two answers, one of the answers longer than T, and a step budget within which the decider's run on the tuple returns true. The budget is what makes the acceptance, a Σ₁ statement, testable.

Equations

• One or more equations did not get rendered due to their size.

def MIPRE.Verifier.longAcceptanceB {ℓ : ℕ} (V : Verifier ℓ) (n T : ℕ) (w : (Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) × ℕ) : Bool

The witness test, as a Bool.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Verifier.longAcceptanceB_iff {ℓ : ℕ} (V : Verifier ℓ) (n T : ℕ) (w : (Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) × ℕ) : V.longAcceptanceB n T w = true ↔ V.LongAcceptance n T w

theorem MIPRE.Verifier.not_rejectsLong_iff_exists {ℓ : ℕ} (V : Verifier ℓ) (n T : ℕ) : ¬V.RejectsLong n T ↔ ∃ (w : (Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) × ℕ), V.LongAcceptance n T w

Rejection of long answers fails exactly when some witness works: RejectsLong is a universal statement over tuples, so its negation is a search for a tuple, and acceptance on the tuple is a search for a budget, Machine.runForD returning the result of a run within its budget (Machine.runForD_eq_some_iff).

@[reducible, inline]

abbrev MIPRE.Verifier.LongZ (α : Type u_2) : Type u_2

The search space of rePred_not_rejectsLong: a witness paired with the parameters.

Equations

• MIPRE.Verifier.LongZ α = ((α × ℕ) × (MIPRE.Cost.BitStr × MIPRE.Cost.BitStr × MIPRE.Cost.BitStr × MIPRE.Cost.BitStr) × ℕ)

theorem MIPRE.Verifier.computable_longInput {α : Type u_1} [Primcodable α] : Computable fun (z : LongZ α) => Cost.encode (z.1.2, z.2.1.1, z.2.1.2.1, z.2.1.2.2.1, z.2.1.2.2.2)

theorem MIPRE.Verifier.computable_longRun {α : Type u_1} [Primcodable α] {ℓ : ℕ} {V : α → Verifier ℓ} (hV : ComputablyPresented V) : Computable fun (z : LongZ α) => Cost.Machine.runForD (Cost.encode (V z.1.1).decider.prog) (Cost.encode (z.1.2, z.2.1.1, z.2.1.2.1, z.2.1.2.2.1, z.2.1.2.2.2)) z.2.2

theorem MIPRE.Verifier.computable_longRunB {α : Type u_1} [Primcodable α] {ℓ : ℕ} {V : α → Verifier ℓ} (hV : ComputablyPresented V) : Computable fun (z : LongZ α) => decide (Cost.Machine.runForD (Cost.encode (V z.1.1).decider.prog) (Cost.encode (z.1.2, z.2.1.1, z.2.1.2.1, z.2.1.2.2.1, z.2.1.2.2.2)) z.2.2 = some (Cost.encode true))

theorem MIPRE.Verifier.computable_longLen {α : Type u_1} [Primcodable α] {T : α → ℕ → ℕ} (hT : Computable fun (q : α × ℕ) => T q.1 q.2) : Computable fun (z : LongZ α) => decide (T z.1.1 z.1.2 + 1 ≤ List.length z.2.1.2.2.1) || decide (T z.1.1 z.1.2 + 1 ≤ List.length z.2.1.2.2.2)

theorem MIPRE.Verifier.computable_longAcceptanceB {α : Type u_1} [Primcodable α] {ℓ : ℕ} {V : α → Verifier ℓ} (hV : ComputablyPresented V) {T : α → ℕ → ℕ} (hT : Computable fun (q : α × ℕ) => T q.1 q.2) : Computable fun (z : LongZ α) => (V z.1.1).longAcceptanceB z.1.2 (T z.1.1 z.1.2) z.2

theorem MIPRE.Verifier.rePred_not_rejectsLong {α : Type u_1} [Primcodable α] {ℓ : ℕ} {V : α → Verifier ℓ} (hV : ComputablyPresented V) {T : α → ℕ → ℕ} (hT : Computable fun (q : α × ℕ) => T q.1 q.2) : REPred fun (q : α × ℕ) => ¬(V q.1).RejectsLong q.2 (T q.1 q.2)

The acceptance of a long answer is recursively enumerable for a computably presented family and a computable answer bound: Verifier.not_rejectsLong_iff_exists turns the failure of RejectsLong into a search, longAcceptanceB runs the test — the length comparison and one budgeted run of the decider — and REPred.of_computable_exists does the searching. This is the third disjunct of Verifier.not_inClassB_iff.

theorem MIPRE.Verifier.rePred_not_isBounded {α : Type u_1} [Primcodable α] {ℓ : ℕ} {V : α → Verifier ℓ} (hV : ComputablyPresented V) : REPred fun (q : α × ℕ) => ¬(V q.1).IsBounded q.2

The boundedness violation is recursively enumerable for a computably presented family: Verifier.not_isBounded_iff_exists turns it into a search, Verifier.boundViolationB runs the test, and REPred.of_computable_exists does the searching.

The semidecider

theorem MIPRE.Halting.exists_sem_of_tab {G : GapCompression} {U : Cost.UniversalMachine} (ω : ValueModel) (hlow : ω.LowerRE) (hV : Verifier.ComputablyPresented (Vof G U)) (tab : Cost.BitStr → ℕ → HaltingGameValue.GameData) (htab : Computable fun (q : Cost.BitStr × ℕ) => tab q.1 q.2) (hval : ∀ (x : Cost.BitStr) (n : ℕ), (Vof G U x).IsBounded n → ω.val (tab x n).game = (Vof G U x).val ω n (ansBound G x n)) : ∃ (S : Cost.Prog), Cost.Prog.WellScoped 1 S ∧ ∀ (x : Cost.BitStr) (n : ℕ), Cost.Halts S (Cost.encode (x, n)) ↔ x ∉ classB G U ω n

Obligation O3 from the tabulation of O2, in a value model r.e. from below. For a computably presented family of verifiers, a computable tabulation whose game has the value of 𝒱_n in the model at every n-bounded string, and a lower semidecider for the value, a closed program halts on encode (x, n) exactly off the class B of the model at level n — obligation O3 of the halting reduction, applied by halting_reduction_lower through exists_sem_lower.

The three disjuncts of Verifier.not_inClassB_iff are enumerated separately — the boundedness violation by Verifier.rePred_not_isBounded, the acceptance of a long answer by Verifier.rePred_not_rejectsLong, the value by the lower semidecider on the tabulation (lem:value-lower-approx at ValueModel.tensor) — and merged by dovetailing (REPred.or).

theorem MIPRE.Halting.computablyPresented_Vof (G : GapCompression) (U : Cost.UniversalMachine) : Verifier.ComputablyPresented (Vof G U)

The family Vof is computably presented. All three fields, and all three are O2's: the two programs by computable_sampData/sampData_eq and computable_decProgData/decProgData_eq, and the third — the sampler's dimension, unconditionally in the string and the level — by the re-budgeted dimOf read back by dimOf_eq. That dimOf_eq carries no hypothesis is the whole point: ComputablyPresented asks for the true dimension at every string and every level, including n = 0 and n = 1, and the budget IsBounded n supplies cannot reach those. What supplies it instead is GapCompression.sampler_time, which holds for every parameter and every index.

theorem MIPRE.Halting.exists_sem_lower (G : GapCompression) (U : Cost.UniversalMachine) (ω : ValueModel) (hlow : ω.LowerRE) : ∃ (S : Cost.Prog), Cost.Prog.WellScoped 1 S ∧ ∀ (x : Cost.BitStr) (n : ℕ), Cost.Halts S (Cost.encode (x, n)) ↔ x ∉ classB G U ω n

Obligation O3, with no hypotheses left but the lower semidecider. Both arguments of exists_sem_of_tab are discharged by O2: the computable presentation by the re-budgeted sampler runs, and hval — the value equality at every n-bounded string, in both directions and with no synchronicity — by the doubled question set of Foundations/GameDouble.lean (tab_val).

This is the repair blueprint lem:halting-semidecider records as the first of three, and the only one that changes nothing outside the tabulation: the two alternatives were to make Decider.wrap reject unequal answers at equal questions, which changes what a string denotes and so reopens accOf_iff, the classes and thm:compression; or to put synchronicity into classB, which moves the cost into compr_spec, a field of the one obligation still open.

theorem MIPRE.Halting.exists_sem (G : GapCompression) (U : Cost.UniversalMachine) : ∃ (S : Cost.Prog), Cost.Prog.WellScoped 1 S ∧ ∀ (x : Cost.BitStr) (n : ℕ), Cost.Halts S (Cost.encode (x, n)) ↔ x ∉ classB G U ValueModel.tensor n

Obligation O3 for the tensor-product value, with no hypotheses.

theorem MIPRE.Halting.exists_sem_upper (G : GapCompression) (U : Cost.UniversalMachine) (ω : ValueModel) (hup : ω.UpperRE) : ∃ (S : Cost.Prog), Cost.Prog.WellScoped 1 S ∧ ∀ (x : Cost.BitStr) (n : ℕ), Cost.Halts S (Cost.encode (x, n)) ↔ x ∉ classOne G U ω n

Obligation O3 for the coRE direction, in a value model r.e. from above: a closed program halting on encode (x, n) exactly off classOne ω n, that is, when the tabulated game at level n has value below 1 — the upper semidecider at the threshold 1/1, composed with the computable tabulation. At ValueModel.commuting this is the role Lin's proof gives to the NPA hierarchy (Lin25). No boundedness is involved: classOne is read on the tabulation.