lean qubit_h_m10_stabRankP_le_eighteen in LeanProofs.QubitHM10StabRank, machine-checked by Lean
Implied per-copy exponent γ ≤ 0.4170 against a published 0.3962, no improvement.
This bound is backed by a machine-checked theorem: qubit_h_m10_stabRankP_le_eighteen in LeanProofs.QubitHM10StabRank. 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⟩⊗10) ≤ 18 from the cat_{4k+2} gluing of Qassim, Pashayan, and Gosset as restated by Kissinger, van de Wetering, and Vilmart (arXiv:2202.09202, Section 4.2) at k = 2: |cat10⟩ is proportional to (I ⊗ ⟨cat_2| ⊗ I)(|cat6⟩ ⊗ |cat6⟩), so it has at most 3 x 3 = 9 stabilizer terms and |T⟩⊗10 = (|cat10⟩ + |cat_10^→)/√ 2 has 18. Exponent log_2(18)/10 = 0.4170, the best finite-m value on the board for this orbit. QPG's own nine-term |cat10⟩ gives the same rank. Witness built here by research/constructions/kvv_cat.py and verified in exact arithmetic. Now at the lean tier: qubit_h_m10_stabRankP_le_eighteen in LeanProofs.QubitHM10StabRank proves stabRankP 2 |qubitH⟩⊗10 ≤ 18 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": 10,
"direction": "upper",
"rank": 18,
"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>^10) <= 18 from the cat_{4k+2} gluing of Qassim, Pashayan, and Gosset as restated by Kissinger, van de Wetering, and Vilmart (arXiv:2202.09202, Section 4.2) at k = 2: |cat_10> is proportional to (I (x) <cat_2| (x) I)(|cat_6> (x) |cat_6>), so it has at most 3 x 3 = 9 stabilizer terms and |T>^10 = (|cat_10> + |cat_10^->)/sqrt 2 has 18. Exponent log_2(18)/10 = 0.4170, the best finite-m value on the board for this orbit. QPG's own nine-term |cat_10> gives the same rank. Witness built here by research/constructions/kvv_cat.py and verified in exact arithmetic. Now at the lean tier: qubit_h_m10_stabRankP_le_eighteen in LeanProofs.QubitHM10StabRank proves stabRankP 2 |qubit_H>^10 <= 18 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.QubitHM10StabRank",
"theorem": "qubit_h_m10_stabRankP_le_eighteen"
},
"witness": {
"terms": [
{
"k": 10,
"x0": [
0,
0,
0,
0,
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
0,
0,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0,
0,
0,
0,
0,
0
],
[
0,
0,
1,
0,
0,
0,
0,
0,
0,
0
],
[
0,
0,
0,
1,
0,
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
1,
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0,
1,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0,
0,
1,
0,
0,
0
],
[
0,
0,
0,
0,
0,
0,
0,
1,
0,
0
],
[
0,
0,
0,
0,
0,
0,
0,
0,
1,
0
],
[
0,
0,
0,
0,
0,
0,
0,
0,
0,
1
]
],
"Q": [
[
0,
1,
1,
1,
1,
1,
1,
1,
1,
1
],
[
0,
0,
1,
1,
1,
1,
1,
1,
1,
1
],
[
0,
0,
0,
1,
1,
1,
1,
1,
1,
1
],
[
0,
0,
0,
0,
1,
1,
1,
1,
1,
1
],
[
0,
0,
0,
0,
0,
1,
1,
1,
1,
1
],
[
0,
0,
0,
0,
0,
0,
1,
1,
1,
1
],
[
0,
0,
0,
0,
0,
0,
0,
1,
1,
1
],
[
0,
0,
0,
0,
0,
0,
0,
0,
1,
1
],
[
0,
0,
0,
0,
0,
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
0,
0,
0,
0,
0
]
],
"l": [
0,
0,
0,
0,
0,
0,
0,
0,
0,
0
]
},
{
"k": 9,
"x0": [
0,
0,
0,
0,
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
0,
0,
0,
0,
0,
1
],
[
0,
1,
0,
0,
0,
0,
0,
0,
0,
1
],
[
0,
0,
1,
0,
0,
0,
0,
0,
0,
1
],
[
0,
0,
0,
1,
0,
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
1,
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
1,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
0,
1,
0,
0,
1
],
[
0,
0,
0,
0,
0,
0,
0,
1,
0,
1
],
[
0,
0,
0,
0,
0,
0,
0,
0,
1,
1
]
],
"Q": [
[
0,
1,
1,
1,
1,
0,
0,
0,
0
],
[
0,
0,
1,
1,
1,
0,
0,
0,
0
],
[
0,
0,
0,
1,
1,
0,
0,
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,
0,
0,
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,
0,
0,
0,
0
]
},
{
"k": 5,
"x0": [
0,
0,
0,
0,
0,
1,
1,
1,
1,
1
],
"W": [
[
1,
0,
0,
0,
0,
1,
1,
1,
1,
1
],
[
0,
1,
0,
0,
0,
1,
1,
1,
1,
1
],
[
0,
0,
1,
0,
0,
1,
1,
1,
1,
1
],
[
0,
0,
0,
1,
0,
1,
1,
1,
1,
1
],
[
0,
0,
0,
0,
1,
1,
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": 9,
"x0": [
0,
0,
0,
0,
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
0,
0,
0,
0,
0,
1
],
[
0,
1,
0,
0,
0,
0,
0,
0,
0,
1
],
[
0,
0,
1,
0,
0,
0,
0,
0,
0,
1
],
[
0,
0,
0,
1,
0,
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
1,
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
1,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
0,
1,
0,
0,
1
],
[
0,
0,
0,
0,
0,
0,
0,
1,
0,
1
],
[
0,
0,
0,
0,
0,
0,
0,
0,
1,
1
]
],
"Q": [
[
0,
0,
0,
0,
0,
1,
1,
1,
1
],
[
0,
0,
0,
0,
0,
1,
1,
1,
1
],
[
0,
0,
0,
0,
0,
1,
1,
1,
1
],
[
0,
0,
0,
0,
0,
1,
1,
1,
1
],
[
0,
0,
0,
0,
0,
1,
1,
1,
1
],
[
0,
0,
0,
0,
0,
0,
1,
1,
1
],
[
0,
0,
0,
0,
0,
0,
0,
1,
1
],
[
0,
0,
0,
0,
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
0,
0,
0,
0
]
],
"l": [
2,
2,
2,
2,
2,
2,
2,
2,
2
]
},
{
"k": 10,
"x0": [
0,
0,
0,
0,
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
0,
0,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0,
0,
0,
0,
0,
0
],
[
0,
0,
1,
0,
0,
0,
0,
0,
0,
0
],
[
0,
0,
0,
1,
0,
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
1,
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0,
1,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0,
0,
1,
0,
0,
0
],
[
0,
0,
0,
0,
0,
0,
0,
1,
0,
0
],
[
0,
0,
0,
0,
0,
0,
0,
0,
1,
0
],
[
0,
0,
0,
0,
0,
0,
0,
0,
0,
1
]
],
"Q": [
[
0,
0,
0,
0,
0,
1,
1,
1,
1,
1
],
[
0,
0,
0,
0,
0,
1,
1,
1,
1,
1
],
[
0,
0,
0,
0,
0,
1,
1,
1,
1,
1
],
[
0,
0,
0,
0,
0,
1,
1,
1,
1,
1
],
[
0,
0,
0,
0,
0,
1,
1,
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,
0,
0,
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,
2,
2
]
},
{
"k": 6,
"x0": [
0,
0,
0,
0,
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
0,
0,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0,
0,
0,
0,
0,
0
],
[
0,
0,
1,
0,
0,
0,
0,
0,
0,
0
],
[
0,
0,
0,
1,
0,
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
1,
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0,
1,
1,
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": 5,
"x0": [
0,
0,
0,
0,
0,
0,
0,
0,
0,
1
],
"W": [
[
1,
1,
1,
1,
1,
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
1,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
0,
1,
0,
0,
1
],
[
0,
0,
0,
0,
0,
0,
0,
1,
0,
1
],
[
0,
0,
0,
0,
0,
0,
0,
0,
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": 6,
"x0": [
0,
0,
0,
0,
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
1,
1,
1,
1,
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0,
1,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0,
0,
1,
0,
0,
0
],
[
0,
0,
0,
0,
0,
0,
0,
1,
0,
0
],
[
0,
0,
0,
0,
0,
0,
0,
0,
1,
0
],
[
0,
0,
0,
0,
0,
0,
0,
0,
0,
1
]
],
"Q": [
[
0,
1,
1,
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
],
[
0,
0,
0,
0,
0,
0
]
],
"l": [
0,
0,
0,
0,
0,
0
]
},
{
"k": 2,
"x0": [
0,
0,
0,
0,
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
1,
1,
1,
1,
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0,
1,
1,
1,
1,
1
]
],
"Q": [
[
0,
1
],
[
0,
0
]
],
"l": [
2,
2
]
},
{
"k": 9,
"x0": [
0,
0,
0,
0,
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
0,
0,
0,
0,
0,
1
],
[
0,
1,
0,
0,
0,
0,
0,
0,
0,
1
],
[
0,
0,
1,
0,
0,
0,
0,
0,
0,
1
],
[
0,
0,
0,
1,
0,
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
1,
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
1,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
0,
1,
0,
0,
1
],
[
0,
0,
0,
0,
0,
0,
0,
1,
0,
1
],
[
0,
0,
0,
0,
0,
0,
0,
0,
1,
1
]
],
"Q": [
[
0,
1,
1,
1,
1,
1,
1,
1,
1
],
[
0,
0,
1,
1,
1,
1,
1,
1,
1
],
[
0,
0,
0,
1,
1,
1,
1,
1,
1
],
[
0,
0,
0,
0,
1,
1,
1,
1,
1
],
[
0,
0,
0,
0,
0,
1,
1,
1,
1
],
[
0,
0,
0,
0,
0,
0,
1,
1,
1
],
[
0,
0,
0,
0,
0,
0,
0,
1,
1
],
[
0,
0,
0,
0,
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
0,
0,
0,
0
]
],
"l": [
0,
2,
2,
2,
2,
2,
2,
2,
2
]
},
{
"k": 10,
"x0": [
0,
0,
0,
0,
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
0,
0,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0,
0,
0,
0,
0,
0
],
[
0,
0,
1,
0,
0,
0,
0,
0,
0,
0
],
[
0,
0,
0,
1,
0,
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
1,
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0,
1,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0,
0,
1,
0,
0,
0
],
[
0,
0,
0,
0,
0,
0,
0,
1,
0,
0
],
[
0,
0,
0,
0,
0,
0,
0,
0,
1,
0
],
[
0,
0,
0,
0,
0,
0,
0,
0,
0,
1
]
],
"Q": [
[
0,
1,
1,
1,
1,
1,
1,
1,
1,
1
],
[
0,
0,
1,
1,
1,
1,
1,
1,
1,
1
],
[
0,
0,
0,
1,
1,
1,
1,
1,
1,
1
],
[
0,
0,
0,
0,
1,
1,
1,
1,
1,
1
],
[
0,
0,
0,
0,
0,
1,
1,
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,
0,
0,
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": [
0,
2,
2,
2,
2,
2,
2,
2,
2,
2
]
},
{
"k": 6,
"x0": [
0,
0,
0,
0,
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
0,
0,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0,
0,
0,
0,
0,
0
],
[
0,
0,
1,
0,
0,
0,
0,
0,
0,
0
],
[
0,
0,
0,
1,
0,
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
1,
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0,
1,
1,
1,
1,
1
]
],
"Q": [
[
0,
1,
1,
1,
1,
1
],
[
0,
0,
1,
1,
1,
1
],
[
0,
0,
0,
1,
1,
1
],
[
0,
0,
0,
0,
1,
1
],
[
0,
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
0
]
],
"l": [
2,
0,
0,
0,
0,
0
]
},
{
"k": 10,
"x0": [
0,
0,
0,
0,
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
0,
0,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0,
0,
0,
0,
0,
0
],
[
0,
0,
1,
0,
0,
0,
0,
0,
0,
0
],
[
0,
0,
0,
1,
0,
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
1,
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0,
1,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0,
0,
1,
0,
0,
0
],
[
0,
0,
0,
0,
0,
0,
0,
1,
0,
0
],
[
0,
0,
0,
0,
0,
0,
0,
0,
1,
0
],
[
0,
0,
0,
0,
0,
0,
0,
0,
0,
1
]
],
"Q": [
[
0,
1,
1,
1,
1,
1,
1,
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,
0,
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0,
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0,
0,
1,
1,
1,
1
],
[
0,
0,
0,
0,
0,
0,
0,
1,
1,
1
],
[
0,
0,
0,
0,
0,
0,
0,
0,
1,
1
],
[
0,
0,
0,
0,
0,
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
0,
0,
0,
0,
0
]
],
"l": [
0,
0,
0,
0,
0,
2,
2,
2,
2,
2
]
},
{
"k": 9,
"x0": [
0,
0,
0,
0,
0,
0,
0,
0,
0,
1
],
"W": [
[
1,
0,
0,
0,
0,
0,
0,
0,
0,
1
],
[
0,
1,
0,
0,
0,
0,
0,
0,
0,
0
],
[
0,
0,
1,
0,
0,
0,
0,
0,
0,
0
],
[
0,
0,
0,
1,
0,
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
1,
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0,
1,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
0,
1,
0,
0,
1
],
[
0,
0,
0,
0,
0,
0,
0,
1,
0,
1
],
[
0,
0,
0,
0,
0,
0,
0,
0,
1,
1
]
],
"Q": [
[
0,
1,
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,
0,
0,
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0,
0,
0,
0,
0
],
[
0,
0,
0,
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,
0,
0,
0,
0,
0,
0,
0,
0
]
},
{
"k": 5,
"x0": [
0,
0,
0,
0,
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
0,
1,
1,
1,
1,
1
],
[
0,
1,
0,
0,
0,
0,
0,
0,
0,
0
],
[
0,
0,
1,
0,
0,
0,
0,
0,
0,
0
],
[
0,
0,
0,
1,
0,
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
1,
0,
0,
0,
0,
0
]
],
"Q": [
[
0,
1,
1,
1,
1
],
[
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0
]
],
"l": [
0,
0,
0,
0,
0
]
},
{
"k": 6,
"x0": [
0,
0,
0,
0,
0,
0,
0,
0,
0,
1
],
"W": [
[
1,
0,
0,
0,
0,
0,
0,
0,
0,
0
],
[
0,
1,
1,
1,
1,
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
1,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
0,
1,
0,
0,
1
],
[
0,
0,
0,
0,
0,
0,
0,
1,
0,
1
],
[
0,
0,
0,
0,
0,
0,
0,
0,
1,
1
]
],
"Q": [
[
0,
1,
0,
0,
0,
0
],
[
0,
0,
1,
1,
1,
1
],
[
0,
0,
0,
1,
1,
1
],
[
0,
0,
0,
0,
1,
1
],
[
0,
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
0
]
],
"l": [
0,
0,
0,
0,
0,
0
]
},
{
"k": 7,
"x0": [
0,
0,
0,
0,
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
0,
0,
0,
0,
0,
0
],
[
0,
1,
1,
1,
1,
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0,
1,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0,
0,
1,
0,
0,
0
],
[
0,
0,
0,
0,
0,
0,
0,
1,
0,
0
],
[
0,
0,
0,
0,
0,
0,
0,
0,
1,
0
],
[
0,
0,
0,
0,
0,
0,
0,
0,
0,
1
]
],
"Q": [
[
0,
1,
0,
0,
0,
0,
0
],
[
0,
0,
1,
1,
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,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0,
0,
0
]
],
"l": [
0,
0,
0,
0,
0,
0,
0
]
},
{
"k": 3,
"x0": [
0,
0,
0,
0,
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
0,
0,
0,
0,
0,
0
],
[
0,
1,
1,
1,
1,
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0,
1,
1,
1,
1,
1
]
],
"Q": [
[
0,
1,
0
],
[
0,
0,
1
],
[
0,
0,
0
]
],
"l": [
0,
2,
2
]
}
],
"coeffs": [
"-sqrt(2)/8",
"-1/4",
"1/4",
"-1/4",
"-sqrt(2)/4",
"sqrt(2)/4",
"1/4",
"sqrt(2)/4",
"sqrt(2)/4",
"-sqrt(2)/8",
"-1/4",
"1/4",
"-1/4",
"sqrt(2)/4",
"sqrt(2)/4",
"1/4",
"sqrt(2)/4",
"sqrt(2)/4"
]
}
}