lean qubit_h_m8_stabRankP_le_twelve in LeanProofs.QubitHM8StabRank, machine-checked by Lean
Implied per-copy exponent γ ≤ 0.4481 against a published 0.3962, no improvement.
This bound is backed by a machine-checked theorem: qubit_h_m8_stabRankP_le_twelve in LeanProofs.QubitHM8StabRank. The recorded lake build confirms it compiles.
1 run; 0.01 CPU-hours; 0.01 h wall-clock; on Apple silicon laptop, one core; direct construction, no search.
χ(|H⟩⊗8) ≤ 12 from the partial decomposition of Kissinger, van de Wetering, and Vilmart (arXiv:2202.09202, Section 4.2), χ(T^t) ≤ 3 χ(T^{t-4}), with χ(T^4) = 4: the leftover |T⟩ of each of the three terms joins the remaining |T⟩⊗3, and |T⟩⊗4 has rank 4. Same value as the product 6 x 2 of the m=6 and m=2 cells and as QPG's table. Witness built here by research/constructions/kvv_cat.py from the three cat_6 terms and the board's m=4 witness, and verified in exact arithmetic; exponent log_2(12)/8 = 0.4481. Now at the lean tier: qubit_h_m8_stabRankP_le_twelve in LeanProofs.QubitHM8StabRank proves stabRankP 2 |qubitH⟩⊗8 ≤ 12 against IsStabP 2 from this witness, the pointwise identity being decided by the kernel on integer coordinate vectors (see lean_proofs/LeanProofs/Stabilizer/Reflect.lean).
Kissinger, van de Wetering, and Vilmart · arXiv:2202.09202 · literature
{
"schema_version": "0.1",
"orbit": "qubit_H",
"m": 8,
"direction": "upper",
"rank": 12,
"provenance": {
"author": "Kissinger, van de Wetering, and Vilmart",
"reference": "arXiv:2202.09202",
"method": "literature",
"date": "2022-02-18",
"github": [],
"compute": {
"cpu_hours": 0.01,
"wall_clock_hours": 0.01,
"runs": 1,
"hardware": "Apple silicon laptop, one core; direct construction, no search"
}
},
"notes": "chi(|H>^8) <= 12 from the partial decomposition of Kissinger, van de Wetering, and Vilmart (arXiv:2202.09202, Section 4.2), chi(T^t) <= 3 chi(T^{t-4}), with chi(T^4) = 4: the leftover |T> of each of the three terms joins the remaining |T>^3, and |T>^4 has rank 4. Same value as the product 6 x 2 of the m=6 and m=2 cells and as QPG's table. Witness built here by research/constructions/kvv_cat.py from the three cat_6 terms and the board's m=4 witness, and verified in exact arithmetic; exponent log_2(12)/8 = 0.4481. Now at the lean tier: qubit_h_m8_stabRankP_le_twelve in LeanProofs.QubitHM8StabRank proves stabRankP 2 |qubit_H>^8 <= 12 against IsStabP 2 from this witness, the pointwise identity being decided by the kernel on integer coordinate vectors (see lean_proofs/LeanProofs/Stabilizer/Reflect.lean).",
"lean": {
"module": "LeanProofs.QubitHM8StabRank",
"theorem": "qubit_h_m8_stabRankP_le_twelve"
},
"witness": {
"terms": [
{
"k": 7,
"x0": [
0,
0,
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
0,
0,
0,
1
],
[
0,
1,
0,
0,
0,
0,
0,
1
],
[
0,
0,
1,
0,
0,
0,
0,
1
],
[
0,
0,
0,
1,
0,
0,
0,
1
],
[
0,
0,
0,
0,
1,
0,
0,
1
],
[
0,
0,
0,
0,
0,
1,
0,
1
],
[
0,
0,
0,
0,
0,
0,
1,
1
]
],
"Q": [
[
0,
1,
1,
1,
1,
0,
0
],
[
0,
0,
1,
1,
1,
0,
0
],
[
0,
0,
0,
1,
1,
0,
0
],
[
0,
0,
0,
0,
1,
0,
0
],
[
0,
0,
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0,
0,
0
]
],
"l": [
2,
2,
2,
2,
2,
0,
0
]
},
{
"k": 8,
"x0": [
0,
0,
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0,
0,
0,
0
],
[
0,
0,
1,
0,
0,
0,
0,
0
],
[
0,
0,
0,
1,
0,
0,
0,
0
],
[
0,
0,
0,
0,
1,
0,
0,
0
],
[
0,
0,
0,
0,
0,
1,
0,
0
],
[
0,
0,
0,
0,
0,
0,
1,
0
],
[
0,
0,
0,
0,
0,
0,
0,
1
]
],
"Q": [
[
0,
1,
1,
1,
1,
1,
1,
1
],
[
0,
0,
1,
1,
1,
1,
1,
1
],
[
0,
0,
0,
1,
1,
1,
1,
1
],
[
0,
0,
0,
0,
1,
1,
1,
1
],
[
0,
0,
0,
0,
0,
1,
1,
1
],
[
0,
0,
0,
0,
0,
0,
1,
1
],
[
0,
0,
0,
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
0,
0,
0
]
],
"l": [
0,
0,
0,
0,
0,
0,
0,
0
]
},
{
"k": 5,
"x0": [
0,
0,
0,
0,
0,
1,
1,
1
],
"W": [
[
1,
0,
0,
0,
0,
1,
1,
1
],
[
0,
1,
0,
0,
0,
1,
1,
1
],
[
0,
0,
1,
0,
0,
1,
1,
1
],
[
0,
0,
0,
1,
0,
1,
1,
1
],
[
0,
0,
0,
0,
1,
1,
1,
1
]
],
"Q": [
[
0,
1,
1,
1,
1
],
[
0,
0,
1,
1,
1
],
[
0,
0,
0,
1,
1
],
[
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0
]
],
"l": [
0,
0,
0,
0,
0
]
},
{
"k": 5,
"x0": [
0,
0,
0,
0,
0,
1,
1,
1
],
"W": [
[
1,
0,
0,
0,
0,
1,
1,
1
],
[
0,
1,
0,
0,
0,
1,
1,
1
],
[
0,
0,
1,
0,
0,
1,
1,
1
],
[
0,
0,
0,
1,
0,
1,
1,
1
],
[
0,
0,
0,
0,
1,
1,
1,
1
]
],
"Q": [
[
0,
1,
1,
1,
1
],
[
0,
0,
1,
1,
1
],
[
0,
0,
0,
1,
1
],
[
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0
]
],
"l": [
2,
2,
2,
2,
2
]
},
{
"k": 8,
"x0": [
0,
0,
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0,
0,
0,
0
],
[
0,
0,
1,
0,
0,
0,
0,
0
],
[
0,
0,
0,
1,
0,
0,
0,
0
],
[
0,
0,
0,
0,
1,
0,
0,
0
],
[
0,
0,
0,
0,
0,
1,
0,
0
],
[
0,
0,
0,
0,
0,
0,
1,
0
],
[
0,
0,
0,
0,
0,
0,
0,
1
]
],
"Q": [
[
0,
0,
0,
0,
0,
1,
1,
1
],
[
0,
0,
0,
0,
0,
1,
1,
1
],
[
0,
0,
0,
0,
0,
1,
1,
1
],
[
0,
0,
0,
0,
0,
1,
1,
1
],
[
0,
0,
0,
0,
0,
1,
1,
1
],
[
0,
0,
0,
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0,
0,
0,
0
]
],
"l": [
2,
2,
2,
2,
2,
2,
2,
2
]
},
{
"k": 7,
"x0": [
0,
0,
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
0,
0,
0,
1
],
[
0,
1,
0,
0,
0,
0,
0,
1
],
[
0,
0,
1,
0,
0,
0,
0,
1
],
[
0,
0,
0,
1,
0,
0,
0,
1
],
[
0,
0,
0,
0,
1,
0,
0,
1
],
[
0,
0,
0,
0,
0,
1,
0,
1
],
[
0,
0,
0,
0,
0,
0,
1,
1
]
],
"Q": [
[
0,
0,
0,
0,
0,
1,
1
],
[
0,
0,
0,
0,
0,
1,
1
],
[
0,
0,
0,
0,
0,
1,
1
],
[
0,
0,
0,
0,
0,
1,
1
],
[
0,
0,
0,
0,
0,
1,
1
],
[
0,
0,
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
0,
0
]
],
"l": [
2,
2,
2,
2,
2,
2,
2
]
},
{
"k": 6,
"x0": [
0,
0,
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0,
0,
0,
0
],
[
0,
0,
1,
0,
0,
0,
0,
0
],
[
0,
0,
0,
1,
0,
0,
0,
0
],
[
0,
0,
0,
0,
1,
0,
0,
0
],
[
0,
0,
0,
0,
0,
1,
1,
1
]
],
"Q": [
[
0,
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
0
]
],
"l": [
0,
0,
0,
0,
0,
0
]
},
{
"k": 6,
"x0": [
0,
0,
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0,
0,
0,
0
],
[
0,
0,
1,
0,
0,
0,
0,
0
],
[
0,
0,
0,
1,
0,
0,
0,
0
],
[
0,
0,
0,
0,
1,
0,
0,
0
],
[
0,
0,
0,
0,
0,
1,
1,
1
]
],
"Q": [
[
0,
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
0
]
],
"l": [
0,
0,
0,
0,
0,
2
]
},
{
"k": 4,
"x0": [
0,
0,
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
1,
1,
1,
1,
0,
0,
0
],
[
0,
0,
0,
0,
0,
1,
0,
0
],
[
0,
0,
0,
0,
0,
0,
1,
0
],
[
0,
0,
0,
0,
0,
0,
0,
1
]
],
"Q": [
[
0,
1,
1,
1
],
[
0,
0,
0,
0
],
[
0,
0,
0,
0
],
[
0,
0,
0,
0
]
],
"l": [
0,
0,
0,
0
]
},
{
"k": 3,
"x0": [
0,
0,
0,
0,
0,
0,
0,
1
],
"W": [
[
1,
1,
1,
1,
1,
0,
0,
1
],
[
0,
0,
0,
0,
0,
1,
0,
1
],
[
0,
0,
0,
0,
0,
0,
1,
1
]
],
"Q": [
[
0,
1,
1
],
[
0,
0,
1
],
[
0,
0,
0
]
],
"l": [
0,
0,
0
]
},
{
"k": 2,
"x0": [
0,
0,
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
1,
1,
1,
1,
0,
0,
0
],
[
0,
0,
0,
0,
0,
1,
1,
1
]
],
"Q": [
[
0,
1
],
[
0,
0
]
],
"l": [
2,
2
]
},
{
"k": 2,
"x0": [
0,
0,
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
1,
1,
1,
1,
0,
0,
0
],
[
0,
0,
0,
0,
0,
1,
1,
1
]
],
"Q": [
[
0,
1
],
[
0,
0
]
],
"l": [
2,
0
]
}
],
"coeffs": [
"-1/4",
"-1/4",
"1/4",
"-sqrt(2)/4",
"-sqrt(2)/4",
"-sqrt(2)/4",
"sqrt(2)/4",
"1/2",
"sqrt(2)/4",
"sqrt(2)/4",
"sqrt(2)/4",
"1/2"
]
}
}