1
Overview
2
The low individual degree test
▶
2.1
The game and its strategies
2.2
Formal soundness target
3
Preliminaries
▶
3.1
Polynomials and measurements
3.2
Consistency and state-dependent distance
3.3
Consistency from state-dependent distance
3.4
Strong self-consistency
4
Making measurements projective
▶
4.0.1
Naimark dilation
4.0.2
Orthogonalization lemma
5
Expansion in the hypercube graph
▶
5.1
The graph and its spectrum
5.2
Local and global variance
6
Global variance of the points measurements
7
Self-improvement
▶
7.1
Non-projective Output
▶
7.1.1
A Semidefinite Program
7.2
Projective Output
8
Commutativity
▶
8.1
Commutativity of the point measurements
8.2
Commutativity of \(G\) after evaluation
8.3
Commutativity of \(G\)
9
Pasting
▶
9.0.1
From Measurements to Submeasurements
9.0.2
The Pasted Submeasurement
▶
The First Construction
The Second Construction
9.0.3
Strong Self-Consistency and Commutation of \(\widehat G\)
▶
Commutativity of \(G_{\bot }\)
Putting Everything Together
9.0.4
Sandwiching Lemmas
9.0.5
Consistency of \(H\) with \(A\)
9.0.6
Completeness of \(H\)
10
The main induction step
▶
10.1
Restricting to one slice
10.2
The inductive construction
▶
Checked status of the corrected induction interface.
10.3
Proof of the main formal theorem
▶
Removed successor restricted-recursion targets.
Lean successor-dependent Step 6 targets.
11
Bibliography
Dependency graph
Blueprint for arXiv:2009.12982
Quantum Soundness of the Classical Low Individual Degree Test
MIPStarRE Project
Last updated: October 25, 2026
1
Overview
2
The low individual degree test
2.1
The game and its strategies
2.2
Formal soundness target
3
Preliminaries
3.1
Polynomials and measurements
3.2
Consistency and state-dependent distance
3.3
Consistency from state-dependent distance
3.4
Strong self-consistency
4
Making measurements projective
4.0.1
Naimark dilation
4.0.2
Orthogonalization lemma
5
Expansion in the hypercube graph
5.1
The graph and its spectrum
5.2
Local and global variance
6
Global variance of the points measurements
7
Self-improvement
7.1
Non-projective Output
7.1.1
A Semidefinite Program
7.2
Projective Output
8
Commutativity
8.1
Commutativity of the point measurements
8.2
Commutativity of \(G\) after evaluation
8.3
Commutativity of \(G\)
9
Pasting
9.0.1
From Measurements to Submeasurements
9.0.2
The Pasted Submeasurement
The First Construction
The Second Construction
9.0.3
Strong Self-Consistency and Commutation of \(\widehat G\)
Commutativity of \(G_{\bot }\)
Putting Everything Together
9.0.4
Sandwiching Lemmas
9.0.5
Consistency of \(H\) with \(A\)
9.0.6
Completeness of \(H\)
10
The main induction step
10.1
Restricting to one slice
10.2
The inductive construction
Checked status of the corrected induction interface.
10.3
Proof of the main formal theorem
Removed successor restricted-recursion targets.
Lean successor-dependent Step 6 targets.
11
Bibliography