The tabulation of a string's verifier under its own parameter

Halting.tab G U x n (Halting/Instantiation.lean) tabulates the n-th game of the verifier a string denotes with the decider budget that n-boundedness supplies, n ^ n · (|d| + 1) ^ n, and is correct on n-bounded strings. The halting reduction along the paper's route (planning/polytime-halting.md) runs its verifier at the fixed level C₀ with a parameter λ = poly(|M|) that is far larger than C₀; that verifier is λ-bounded and not C₀-bounded, and its size clause alone rules the old budget out. So the decider is re-budgeted from the string's own parameter: n ^ λ · (|d| + 1) ^ λ at index n with λ = descLam x, which is exactly what Verifier.IsBounded λ supplies at every n ≥ 2.

Everything else — the sampler runs under the compressed sampler's own bound, the doubled question set, the weight list — is Instantiation.lean's, and the correctness proof is its tab_match with the one budget lemma swapped (accOfL_iff). The semidecider for "val* at level C₀ exceeds 1/2" on this tabulation (exists_semL) is what the search branch of the paper-route decider tests.

Acceptance under the λ-budget

def MIPRE.Halting.accOfL (pd : Cost.Data) (n lam : ℕ) (x y a b : Cost.BitStr) : Bool

Acceptance from the encoded decider program, under the budget n ^ λ · (|d| + 1) ^ λ.

Equations

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

theorem MIPRE.Halting.primrec_accOfL {α : Type u_1} [Primcodable α] {pd : α → Cost.Data} {lvl lam : α → ℕ} (hpd : Primrec pd) (hlvl : Primrec lvl) (hlam : Primrec lam) : Primrec fun (q : α × Cost.BitStr × Cost.BitStr × Cost.BitStr × Cost.BitStr) => accOfL (pd q.1) (lvl q.1) (lam q.1) q.2.1 q.2.2.1 q.2.2.2.1 q.2.2.2.2

def MIPRE.Halting.tabOfL (sd pd : Cost.Data) (s T B k n lam : ℕ) : HaltingGameValue.GameData

The doubled tabulation with the decider under the λ-budget; the sampler side is tabOf's.

Equations

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

theorem MIPRE.Halting.primrec_tabOfL {α : Type u_1} [Primcodable α] {sd pd : α → Cost.Data} {s T B lvl lam : α → ℕ} (k : ℕ) (hsd : Primrec sd) (hpd : Primrec pd) (hs : Primrec s) (hT : Primrec T) (hB : Primrec B) (hlvl : Primrec lvl) (hlam : Primrec lam) : Primrec fun (a : α) => tabOfL (sd a) (pd a) (s a) (T a) (B a) k (lvl a) (lam a)

theorem MIPRE.Halting.primrec_tabOfL_tuple (k : ℕ) : Primrec fun (q : (Cost.Data × Cost.Data) × (ℕ × ℕ) × ℕ × ℕ × ℕ) => tabOfL q.1.1 q.1.2 q.2.1.1 q.2.2.1 q.2.1.2 k q.2.2.2.1 q.2.2.2.2

noncomputable def MIPRE.Halting.tabL (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) : HaltingGameValue.GameData

The tabulation of (Vof G U x)'s n-th game under the string's own parameter.

Equations

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

theorem MIPRE.Halting.computable_tabArgsL (G : GapCompression) (U : Cost.UniversalMachine) : Computable fun (p : Cost.BitStr × ℕ) => ((sampData G p.1, decProgData G U p.1), (dimOf (sampData G p.1) (ansBound G p.1 p.2) G.deg p.2, ansBound G p.1 p.2), ansBound G p.1 p.2, p.2, descLam p.1)

theorem MIPRE.Halting.tabL_computable (G : GapCompression) (U : Cost.UniversalMachine) : Computable fun (p : Cost.BitStr × ℕ) => tabL G U p.1 p.2

theorem MIPRE.Halting.accOfL_iff (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) (hb : (Vof G U x).IsBounded (descLam x)) (hn : 2 ≤ n) (x' y' a b : Cost.BitStr) : accOfL (decProgData G U x) n (descLam x) x' y' a b = true ↔ (Vof G U x).decider.Accepts n x' y' a b

The tabulated acceptance test is the verifier's acceptance, on a string whose verifier is bounded by the string's own parameter.

The tabulation matches the verifier, doubled

Verbatim Instantiation.lean's tab_nX … tab_value, at tabL and with accOfL_iff in place of accOf_iff.

theorem MIPRE.Halting.tabL_nX (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) : (tabL G U x n).nX + 1 = 2 ^ ((Vof G U x).sampler.dim n + 1)

theorem MIPRE.Halting.tabL_nA (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) : (tabL G U x n).nA + 1 = (Verifier.answerList (ansBound G x n)).length

noncomputable def MIPRE.Halting.eXofL (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) : Fin ((tabL G U x n).nX + 1) ≃ Bool × (Vof G U x).Questions n

The question relabeling.

Equations

• MIPRE.Halting.eXofL G U x n = (finCongr ⋯).trans (MIPRE.Verifier.tagEquiv ((MIPRE.Halting.Vof G U x).sampler.dim n)).symm

noncomputable def MIPRE.Halting.eAofL (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) : Fin ((tabL G U x n).nA + 1) ≃ Verifier.Answers (ansBound G x n)

The answer relabeling.

Equations

• MIPRE.Halting.eAofL G U x n = (finCongr ⋯).trans (MIPRE.Verifier.answerEquiv (MIPRE.Halting.ansBound G x n))

theorem MIPRE.Halting.eXofL_apply (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) (i : Fin ((tabL G U x n).nX + 1)) : Verifier.bitsToIdx (((eXofL G U x n) i).1 :: CL.toBits ((eXofL G U x n) i).2) = ↑i

theorem MIPRE.Halting.eAofL_apply (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) (k : Fin ((tabL G U x n).nA + 1)) : List.idxOf (↑((eAofL G U x n) k)) (Cost.Data.bitStrsLE (ansBound G x n)) = ↑k

theorem MIPRE.Halting.margL_idx_eq (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) (w : Player) (tg : Bool) (z : Cost.BitStr) (hz : List.length z = (Vof G U x).sampler.dim n) (i : Fin ((tabL G U x n).nX + 1)) : Verifier.bitsToIdx (tg :: margOf (sampData G x) (ansBound G x n) G.deg n w z) = ↑i ↔ tg = ((eXofL G U x n) i).1 ∧ ((Vof G U x).sampler.cl n w).eval (CL.ofBits ((Vof G U x).sampler.dim n) z) = ((eXofL G U x n) i).2

theorem MIPRE.Halting.mu_clauseL (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) (i j : Fin ((tabL G U x n).nX + 1)) : (tabL G U x n).game.μ i j = ((Vof G U x).doubledGame n (ansBound G x n)).μ ((eXofL G U x n) i) ((eXofL G U x n) j)

The μ clause, doubled.

theorem MIPRE.Halting.accL_mem_iff (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) (hb : (Vof G U x).IsBounded (descLam x)) (hn : 2 ≤ n) (i j : Fin ((tabL G U x n).nX + 1)) (k l : Fin ((tabL G U x n).nA + 1)) : (↑i, ↑j, ↑k, ↑l) ∈ (tabL G U x n).acc ↔ ((eXofL G U x n) i).1 = false ∧ ((eXofL G U x n) j).1 = true ∧ (Vof G U x).decider.Accepts n (CL.toBits ((eXofL G U x n) i).2) (CL.toBits ((eXofL G U x n) j).2) ↑((eAofL G U x n) k) ↑((eAofL G U x n) l)

The acceptance table read back, doubled.

theorem MIPRE.Halting.tabL_match (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) (hb : (Vof G U x).IsBounded (descLam x)) (hn : 2 ≤ n) : ∃ (eX : Fin ((tabL G U x n).nX + 1) ≃ Bool × (Vof G U x).Questions n) (eA : Fin ((tabL G U x n).nA + 1) ≃ Verifier.Answers (ansBound G x n)), (∀ (i j : Fin ((tabL G U x n).nX + 1)), (tabL G U x n).game.μ i j = ((Vof G U x).doubledGame n (ansBound G x n)).μ (eX i) (eX j)) ∧ ∀ (i j : Fin ((tabL G U x n).nX + 1)) (k l : Fin ((tabL G U x n).nA + 1)), (tabL G U x n).game.D i j k l = ((Vof G U x).doubledGame n (ansBound G x n)).D (eX i) (eX j) (eA k) (eA l)

The match, doubled.

theorem MIPRE.Halting.tabL_value (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) (hb : (Vof G U x).IsBounded (descLam x)) (hn : 2 ≤ n) : quantumValue (tabL G U x n).game = (Vof G U x).valStar n (ansBound G x n)

The value of the tabulation is the verifier's, on a string whose verifier is bounded by the string's own parameter, at every index n ≥ 2.

The semidecider of the search branch

theorem MIPRE.Halting.exists_semL (G : GapCompression) (U : Cost.UniversalMachine) (n₀ : ℕ) : ∃ (S : Cost.Prog), Cost.Prog.WellScoped 1 S ∧ ∀ (x : Cost.BitStr), Cost.Halts S (Cost.encode x) ↔ 1 / 2 < quantumValue (tabL G U x n₀).game

The search branch's semidecider: a closed program halting on encode x exactly when the tabulation of x's verifier at the level n₀ has quantum value above 1/2. On the strings this tabulation is correct for (tabL_value), that is val*(𝒱_{n₀}) > 1/2.

theorem MIPRE.Halting.Vof_descOf (G : GapCompression) (U : Cost.UniversalMachine) (lam : ℕ) (e : Cost.Prog) : Vof G U (descOf lam e) = Verifier.ofSamplerDecider U (G.sampler lam) e

The verifier the string descOf lam e denotes.