Enumerating the questions and the answers of 𝒱_n

The tabulation of 𝒱_n as a game description (blueprint def:game-description, rem:compression-abstract) indexes the questions and the answers by Fin (nX + 1) and Fin (nA + 1). This file provides the two indexings, explicitly and computably, together with the agreement of the tabulated value with val*.

• Data.bitStrsOfLen k and Data.bitStrsLE T: the bit strings of length exactly k, and of length at most T, without repetition (nodup_bitStrsLE, mem_bitStrsLE); the second has 2 ^ (T + 1) - 1 entries.
• Verifier.answerList T and Verifier.answerEquiv T : Fin (answerList T).length ≃ Answers T: the answer alphabet, enumerated.
• Verifier.questionEquiv s : Fin (2 ^ s) ≃ (Fin s → CL.𝔽₂): the question alphabet, from Mathlib's finFunctionFinEquiv (𝔽₂ = ZMod 2 is Fin 2).
• Verifier.quantumValue_toGame_eq_valStar: a game description whose distribution and decision predicate match 𝒱_n along these indexings has val*(G) = val*(𝒱_n). This is the bridge rem:compression-abstract needs between the criterion's semidecision procedure, which runs on game descriptions (lem:value-lower-approx), and the verifiers of the pipeline.

What is still owed is the computation of such a description from an n-bounded verifier — running the sampler on every point of 𝔽₂^{s(n)} to count the question weights, and the decider under its budget to fill in the acceptance table (planning/formalization-plan.md, H4).

def MIPRE.Cost.Data.bitStrsOfLen : ℕ → List BitStr

The bit strings of length exactly k.

Equations

• MIPRE.Cost.Data.bitStrsOfLen 0 = [[]]
• MIPRE.Cost.Data.bitStrsOfLen k.succ = List.flatMap (fun (l : List Bool) => [false :: l, true :: l]) (MIPRE.Cost.Data.bitStrsOfLen k)

@[simp]

theorem MIPRE.Cost.Data.mem_bitStrsOfLen (k : ℕ) (l : BitStr) : l ∈ bitStrsOfLen k ↔ List.length l = k

theorem MIPRE.Cost.Data.nodup_bitStrsOfLen (k : ℕ) : (bitStrsOfLen k).Nodup

@[simp]

theorem MIPRE.Cost.Data.length_bitStrsOfLen (k : ℕ) : (bitStrsOfLen k).length = 2 ^ k

def MIPRE.Cost.Data.bitStrsLE (T : ℕ) : List BitStr

The bit strings of length at most T.

Equations

• MIPRE.Cost.Data.bitStrsLE T = List.flatMap MIPRE.Cost.Data.bitStrsOfLen (List.range (T + 1))

@[simp]

theorem MIPRE.Cost.Data.mem_bitStrsLE (T : ℕ) (l : BitStr) : l ∈ bitStrsLE T ↔ List.length l ≤ T

theorem MIPRE.Cost.Data.nodup_bitStrsLE (T : ℕ) : (bitStrsLE T).Nodup

The two enumerations are primitive recursive: the tabulation of MIPRE.Halting walks both of them, so both are on the critical path of MIPRE.Halting.tab_computable.

theorem MIPRE.Cost.Data.primrec_bitStrsOfLen : Primrec bitStrsOfLen

theorem MIPRE.Cost.Data.primrec_bitStrsLE : Primrec bitStrsLE

theorem MIPRE.Cost.Data.length_bitStrsLE_pos (T : ℕ) : 0 < (bitStrsLE T).length

The answer alphabet

def MIPRE.Verifier.toAnswer (T : ℕ) (l : Cost.BitStr) : Answers T

A bit string as an answer of length at most T, by truncation (the identity on the strings that already fit).

Equations

• MIPRE.Verifier.toAnswer T l = ⟨List.take T l, ⋯⟩

@[simp]

theorem MIPRE.Verifier.toAnswer_val (T : ℕ) (a : Answers T) : toAnswer T ↑a = a

def MIPRE.Verifier.answerList (T : ℕ) : List (Answers T)

The answers of length at most T, enumerated.

Equations

• MIPRE.Verifier.answerList T = List.map (MIPRE.Verifier.toAnswer T) (MIPRE.Cost.Data.bitStrsLE T)

@[simp]

theorem MIPRE.Verifier.mem_answerList (T : ℕ) (a : Answers T) : a ∈ answerList T

theorem MIPRE.Verifier.nodup_answerList (T : ℕ) : (answerList T).Nodup

noncomputable def MIPRE.Verifier.answerEquiv (T : ℕ) : Fin (answerList T).length ≃ Answers T

The answer alphabet, indexed.

Equations

• MIPRE.Verifier.answerEquiv T = List.Nodup.getEquivOfForallMemList (MIPRE.Verifier.answerList T) ⋯ ⋯

The question alphabet

def MIPRE.Verifier.questionEquiv (s : ℕ) : Fin (2 ^ s) ≃ (Fin s → CL.𝔽₂)

The question alphabet 𝔽₂^s, indexed: 𝔽₂ is ZMod 2, which is Fin 2.

Equations

• MIPRE.Verifier.questionEquiv s = finFunctionFinEquiv.symm

The agreement of the tabulated value with val*

theorem MIPRE.Verifier.isSynchronousAt_of_game_matches {ℓ : ℕ} (V : Verifier ℓ) (n T : ℕ) (g : HaltingGameValue.GameData) (eX : Fin (g.nX + 1) ≃ V.Questions n) (eA : Fin (g.nA + 1) ≃ Answers T) (hD : ∀ (i j : Fin (g.nX + 1)) (k l : Fin (g.nA + 1)), g.game.D i j k l = (V.game n T).D (eX i) (eX j) (eA k) (eA l)) (q : V.Questions n) (a b : Answers T) (hab : a ≠ b) : ¬V.decider.Accepts n (CL.toBits q) (CL.toBits q) ↑a ↑b

A game description can match 𝒱_n only if 𝒱_n is synchronous. GameData.game rejects unequal answers at equal questions by construction (GameData.game_D), whatever the acceptance table holds, while Verifier.game accepts exactly what the decider accepts. So the hD of quantumValue_toGame_eq_valStar below forces the decider to reject those tuples --- for every question and every pair of in-range answers.

This is what rules the un-doubled bridges out of the halting reduction. Every statement whose hD matches a description against V.game n T --- quantumValue_toGame_eq_valStar below, and gameValue_toGame_le_of_valStar_le of Foundations/SyncTransport.lean --- is satisfiable only at a verifier synchronous at n, while their hypotheses mention no synchronicity, so it is forced on them anyway. (Three un-doubled completeness bridges once sat beside them; they went when HasPerfectPCC moved to the doubled game, issue #77.) IsBounded n does not supply it (the wrapper of Decider.wrap enforces accepts_length and nothing else), and neither does MIPRE.Halting.classB, which is the class the soundness branch of the halting reduction runs in. That is why Foundations/GameDouble.lean and the _doubled bridges beside them exist: MIPRE.Halting.tab_match matches (Vof G U x).doubledGame, whose distribution puts no weight on the diagonal, and asks the verifier for no synchronicity at all.

Nothing consumes this lemma, and that is deliberate: it is the machine-checked form of the obstruction, so that a match stated against V.game n T again --- the shape an earlier tab_match had, with the IsSynchronousAt n hypothesis it needed --- can be met with it rather than with a commit message.

theorem MIPRE.Verifier.quantumValue_toGame_eq_valStar {ℓ : ℕ} (V : Verifier ℓ) (n T : ℕ) (g : HaltingGameValue.GameData) (eX : Fin (g.nX + 1) ≃ V.Questions n) (eA : Fin (g.nA + 1) ≃ Answers T) (hμ : ∀ (i j : Fin (g.nX + 1)), g.game.μ i j = V.sampler.dist n (eX i) (eX j)) (hD : ∀ (i j : Fin (g.nX + 1)) (k l : Fin (g.nA + 1)), g.game.D i j k l = (V.game n T).D (eX i) (eX j) (eA k) (eA l)) : quantumValue g.game = V.valStar n T

The bridge to game descriptions. A game description whose question distribution and decision predicate match those of 𝒱_n along the two indexings has the same quantum value. The semidecision procedure of lem:value-lower-approx runs on game descriptions, and this is what carries its verdict back to the verifier.

The shape of the semidecision procedure

theorem MIPRE.Verifier.not_inClassB_iff {ℓ : ℕ} (V : Verifier ℓ) (ω : ValueModel) (n T : ℕ) : ¬V.InClassB ω n T ↔ ¬V.IsBounded n ∨ ¬V.RejectsLong n T ∨ 1 / 2 < V.val ω n T

The complement of the class B, as the criterion's semidecider has to see it: either the verifier is not n-bounded — witnessed by a single input whose run exceeds the budget, so a search — or its value at index n exceeds 1/2, which is the val* half of lem:value-lower-approx on the tabulation. Neither disjunct decides n-boundedness, which is Π₁; the point of the disjunction is that it does not have to.