thomasvidick

Solved 50

• RE is contained in the paper's class $\mathrm{MIP}^*_{1,1/2}(2,1)$, given an answer reduction stageProved

  Oct 2026

• The quantum game value is uncomputable, given an answer reduction stageProved

  Oct 2026

• The synchronous game value is uncomputable, given an answer reduction stageProved

  Oct 2026

• RE is contained in the computable class MIP*: a computable family of games with value 1 on an r.e. language and at most 1/2 off itProved

  Oct 2026

• $\mathrm{MIP}^*_{1,1/2}(2,1) = \mathrm{RE}$ for the paper's class, given an answer reduction stageProved

  Oct 2026

• RE is contained in the computable class MIP*, given an answer reduction stageProved

  Oct 2026

• MIP*_{1,1/2}(2,1) = RE: the title theorem of MIP* = RE, for the paper's classProved

  Oct 2026

• Halting reduces to the synchronous game value (MIP* = RE, Theorem 12.2)Proved

  Oct 2026

• MIP* = RE for the computable class, given an answer reduction stageProved

  Oct 2026

• MIP* = RE for the computable class: a language has a computable family of games with gap 1 versus 1/2 if and only if it is recursively enumerableProved

  Oct 2026

• An introspection stage exists for seven-level normal form verifiersProved

  Oct 2026

• Uncomputability of the synchronous game value: no algorithm separates value 1 from value at most 1/2Proved

  Oct 2026

• Halting reduces to the quantum (entangled) value of a game descriptionProved

  Oct 2026

• Halting reduces to the quantum game value, given an answer reduction stageProved

  Oct 2026

• Halting reduces to the synchronous game value, given an answer reduction stageProved

  Oct 2026

• RE is contained in MIP*_{1,1/2}(2,1): a polynomial-time verifier for every recursively enumerable languageProved

  Oct 2026

• Uncomputability of the quantum game value: no algorithm separates value 1 from value at most 1/2Proved

  Oct 2026

• Soundness in exactly the ambient verifier-value form used by the pipelineProved

  Oct 2026

• An answer reduction stage exists for five-level normal form verifiersProved

  Oct 2026

• A raw typed strategy already gives the original verifier's source valueProved

  Oct 2026

• Lemma coefficient_one_le of the MIP* = RE formalizationProved

  Oct 2026

• Lemma exponent_le_one of the MIP* = RE formalizationProved

  Oct 2026

• Soundness of answer reduction (lem:ar-soundness, the soundness clause of the AnswerReduction contract, at any answer bound above the answer cut): val* of the…Proved

  Oct 2026

• Lemma exponent_pos of the MIP* = RE formalizationProved

  Oct 2026

• Uniform soundness for the actual canonical field and register parameters, on the source's original coordinate typeProved

  Oct 2026

• The decoded strategy fails the typed oracularized game with probability at most 6 times the combined error, given the PCP's soundness in the form hgcProved

  Oct 2026

• Bob's oracles' game checks, summed over the oracle halvesProved

  Oct 2026

• Lemma qldExponent_pos of the MIP* = RE formalizationProved

  Oct 2026

• Alice's oracles' game checks, summed over the oracle halvesProved

  Oct 2026

• The decoded strategy's failure at a seed, over the nine ordered pairs of rolesProved

  Oct 2026

• Summed over the oracle halves, Alice's placed G against Bob's JProved

  Oct 2026

• The parameters are polynomial: Z = 8 (Q + 1) m' ≤ zC (Q σ)^{zE}Proved

  Oct 2026

• Summed over the oracle halves, Alice's J against Bob's placed GProved

  Oct 2026

• The oracle's game check under Bob's J, the mirror imageProved

  Oct 2026

• Alice's Point_6 against Bob's extracted j-th polynomial of the sixth copyProved

  Oct 2026

• thm:qld: soundness of the Pauli basis test (the paper's thm:pauli-appendix)Proved

  Oct 2026

• The oracle's game check under Alice's J: the outcomes not placed on their blocks, which disagree with Bob's placed G, plus twice the weight of the rejected evaluationsProved

  Oct 2026

• Alice's extracted polynomial of copy i against Bob's point, from the extractionProved

  Oct 2026

• Alice's extracted j-th polynomial of the sixth copy against Bob's Point_6Proved

  Oct 2026

• Bob and Bob: the disagreement of the two extracted polynomial measurementsProved

  Oct 2026

• The combined error at a typed failure θ ≤ Kε, over a large fieldProved

  Oct 2026

• Bob's J against the check, the mirror imageProved

  Oct 2026

• The PCP's soundness, as the decoded strategy needs it, for the answer-reduced verifier's game check and the decoder decAnsProved

  Oct 2026

• Alice's point of copy i against Bob's extracted polynomial, from the extractionProved

  Oct 2026

• Bob and an oracleProved

  Oct 2026

• The failure of a strategy for a typed oracularized game is the average, over the ordered pairs of roles and the seed, of its failure at the questions they determineProved

  Oct 2026

• From evaluations to polynomials, Alice's J: at each oracle half, the outcome-level disagreement is at most the evaluated one, averaged over the PCP vectors, plus m' d / qProved

  Oct 2026

• Alice's J against the check: summed over the oracle halves, at most the sixth copy's extraction error plus 54² times the typed failure, per oracle halfProved

  Oct 2026

• thm:qld with its error named: both items at most qldErr ε m d q, for a POVM strategy of failure probability at most εProved

  Oct 2026

• Bob and Alice never fail: only the formats are checkedProved

  Oct 2026

Posted 50

• Definitions of Compiler: Supplying the ambient introspection contract The sampler, executable decision kernel, universal clock, all-index…Definition

  Oct 2026

• Definitions of Instance: Answer reduction, supplied Piece AR-6 of `planning/answer-reduction.md` (`thm:answer-reduction`): the `AnswerReduction…Definition

  Oct 2026

• Lemma coefficient_one_le of the MIP* = RE formalizationProved

  Oct 2026

• Lemma exponent_pos of the MIP* = RE formalizationProved

  Oct 2026

• Soundness in exactly the ambient verifier-value form used by the pipelineProved

  Oct 2026

• A raw typed strategy already gives the original verifier's source valueProved

  Oct 2026

• Lemma exponent_le_one of the MIP* = RE formalizationProved

  Oct 2026

• Definitions of CompiledSoundness: Soundness of the actual compiled introspection verifier The compiled strategy is restricted through finite detyping,…Definition

  Oct 2026

• Uniform soundness for the actual canonical field and register parameters, on the source's original coordinate typeProved

  Oct 2026

• Definitions of NumberedSoundness: Source soundness with the actual finite register numbering Coordinate relabeling is performed on the intrinsic quotient…Definition

  Oct 2026

• Lemma qldExponent_pos of the MIP* = RE formalizationProved

  Oct 2026

• Definitions of QLDExtractionAdapter: Actual QLD soundness witnesses in the introspection interface QLD reads all wrongly formatted Pauli answers as zeroDefinition

  Oct 2026

• The parameters are polynomial: Z = 8 (Q + 1) m' ≤ zC (Q σ)^{zE}Proved

  Oct 2026

• The decoded strategy fails the typed oracularized game with probability at most 6 times the combined error, given the PCP's soundness in the form hgcProved

  Oct 2026

• Soundness of answer reduction (lem:ar-soundness, the soundness clause of the AnswerReduction contract, at any answer bound above the answer cut): val* of the…Proved

  Oct 2026

• The oracle's game check under Bob's J, the mirror imageProved

  Oct 2026

• Definitions of SoundFinal: Soundness of answer reduction Piece AR-5f of `planning/answer-reduction.md`, concluded (`lem:ar-soundness`,…Definition

  Oct 2026

• The decoded strategy's failure at a seed, over the nine ordered pairs of rolesProved

  Oct 2026

• The PCP's soundness, as the decoded strategy needs it, for the answer-reduced verifier's game check and the decoder decAnsProved

  Oct 2026

• Alice's oracles' game checks, summed over the oracle halvesProved

  Oct 2026

• The failure of a strategy for a typed oracularized game is the average, over the ordered pairs of roles and the seed, of its failure at the questions they determineProved

  Oct 2026

• Bob's oracles' game checks, summed over the oracle halvesProved

  Oct 2026

• The oracle's game check under Alice's J: the outcomes not placed on their blocks, which disagree with Bob's placed G, plus twice the weight of the rejected evaluationsProved

  Oct 2026

• Alice and an oracleProved

  Oct 2026

• Bob and Alice never fail: only the formats are checkedProved

  Oct 2026

• Alice and Alice: the disagreement of the two extracted polynomial measurementsProved

  Oct 2026

• An oracle and BobProved

  Oct 2026

• Bob and an oracleProved

  Oct 2026

• Bob and Bob: the disagreement of the two extracted polynomial measurementsProved

  Oct 2026

• Definitions of SoundPcp: Soundness of answer reduction: the PCP's soundness Piece AR-5e of `planning/answer-reduction.md`, concluded…Definition

  Oct 2026

• Alice and Bob never fail: only the formats are checkedProved

  Oct 2026

• Two oracles: the two game checks and the disagreement of the two JProved

  Oct 2026

• An oracle and Alice: the oracle's game check and the disagreement of its first answer polynomial with Alice'sProved

  Oct 2026

• A placed outcome whose decoded pair fails the game check is rejected at at least half the pointsProved

  Oct 2026

• Bob's J against the check, the mirror imageProved

  Oct 2026

• Definitions of SoundDecoded: Soundness of answer reduction: the decoded strategy Piece AR-5e of `planning/answer-reduction.md` (`lem:ar-ora`): a…Definition

  Oct 2026

• Alice's J against the check: summed over the oracle halves, at most the sixth copy's extraction error plus 54² times the typed failure, per oracle halfProved

  Oct 2026

• Step 5 at two Point_6 questions: acceptance forces the PCP check to pass on both answersProved

  Oct 2026

• Summed over the oracle halves, Alice's placed G against Bob's JProved

  Oct 2026

• Summed over the oracle halves, Alice's J against Bob's placed GProved

  Oct 2026

• From evaluations to polynomials, Alice's J: at each oracle half, the outcome-level disagreement is at most the evaluated one, averaged over the PCP vectors, plus m' d / qProved

  Oct 2026

• From evaluations to polynomials, Bob's JProved

  Oct 2026

• Definitions of SoundGameCheck: Soundness of answer reduction: the game check under the extracted measurement Piece AR-5e of…Definition

  Oct 2026

• The error is below the soundness loss: with N = λn, Q between N^μ and N^{2μ} and past the threshold, the bound of errE_le gives 24 √(7 e) ≤ σ^a (N^{μa} ε^{clB/2} +…Proved

  Oct 2026

• The prefactor of δ_sim is at most Z^{3A} when its argument is at most Z²Proved

  Oct 2026

• One extraction's error, term by termProved

  Oct 2026

• Alice's point of copy i against Bob's extracted polynomial, from the extractionProved

  Oct 2026

• The combined error at a typed failure θ ≤ Kε, over a large fieldProved

  Oct 2026

• Definitions of SoundPoly: Soundness of answer reduction: from evaluations to polynomials Piece AR-5d of `planning/answer-reduction.md`, the…Definition

  Oct 2026

• Past a threshold, 2^{clB Q} beats every polynomial in Q, and Q ≥ 8064Proved

  Oct 2026