lean qubit_t_m6_stabRankP_le_six in LeanProofs.QubitTM6StabRank, machine-checked by Lean
Implied per-copy exponent γ ≤ 0.4308 against a published 0.3962, no improvement.
This bound is backed by a machine-checked theorem: qubit_t_m6_stabRankP_le_six in LeanProofs.QubitTM6StabRank. The recorded lake build confirms it compiles.
rank 5 plateaus at √(5/6) sin(π/12) Witness: the products of the three m=4 terms with the two m=2 terms, verified here in exact arithmetic on all 64 amplitudes. Now at the lean tier: qubit_t_m6_stabRankP_le_six in LeanProofs.QubitTM6StabRank proves stabRankP 2 |qubitT⟩⊗6 ≤ 6 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).
Labib and Russo · arXiv:2605.28586 · literature
{
"schema_version": "0.1",
"orbit": "qubit_T",
"m": 6,
"direction": "upper",
"rank": 6,
"provenance": {
"author": "Labib and Russo",
"reference": "arXiv:2605.28586",
"method": "literature",
"date": "2026-05-27",
"github": [
"FarLab",
"vprusso"
]
},
"notes": "rank 5 plateaus at sqrt(5/6) sin(pi/12) Witness: the products of the three m=4 terms with the two m=2 terms, verified here in exact arithmetic on all 64 amplitudes. Now at the lean tier: qubit_t_m6_stabRankP_le_six in LeanProofs.QubitTM6StabRank proves stabRankP 2 |qubit_T>^6 <= 6 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.QubitTM6StabRank",
"theorem": "qubit_t_m6_stabRankP_le_six"
},
"witness": {
"terms": [
{
"k": 4,
"x0": [
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
1,
0,
0,
0
],
[
0,
1,
0,
0,
0,
0
],
[
0,
0,
0,
1,
0,
0
],
[
0,
0,
0,
0,
1,
1
]
],
"Q": [
[
0,
0,
0,
0
],
[
0,
0,
1,
0
],
[
0,
0,
0,
0
],
[
0,
0,
0,
0
]
],
"l": [
1,
0,
0,
1
]
},
{
"k": 5,
"x0": [
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
1,
0,
0,
0
],
[
0,
1,
0,
0,
0,
0
],
[
0,
0,
0,
1,
0,
0
],
[
0,
0,
0,
0,
1,
0
],
[
0,
0,
0,
0,
0,
1
]
],
"Q": [
[
0,
0,
0,
0,
0
],
[
0,
0,
1,
0,
0
],
[
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0
]
],
"l": [
1,
0,
0,
0,
0
]
},
{
"k": 5,
"x0": [
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0,
0
],
[
0,
0,
1,
0,
0,
0
],
[
0,
0,
0,
1,
0,
0
],
[
0,
0,
0,
0,
1,
1
]
],
"Q": [
[
0,
0,
1,
0,
0
],
[
0,
0,
0,
1,
0
],
[
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0
]
],
"l": [
0,
1,
0,
1,
1
]
},
{
"k": 6,
"x0": [
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0,
0
],
[
0,
0,
1,
0,
0,
0
],
[
0,
0,
0,
1,
0,
0
],
[
0,
0,
0,
0,
1,
0
],
[
0,
0,
0,
0,
0,
1
]
],
"Q": [
[
0,
0,
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,
1
],
[
0,
0,
0,
0,
0,
0
]
],
"l": [
0,
1,
0,
1,
0,
0
]
},
{
"k": 4,
"x0": [
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
0,
0
],
[
0,
1,
0,
1,
0,
0
],
[
0,
0,
1,
0,
0,
0
],
[
0,
0,
0,
0,
1,
1
]
],
"Q": [
[
0,
0,
1,
0
],
[
0,
0,
0,
0
],
[
0,
0,
0,
0
],
[
0,
0,
0,
0
]
],
"l": [
1,
1,
1,
1
]
},
{
"k": 5,
"x0": [
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
0,
0
],
[
0,
1,
0,
1,
0,
0
],
[
0,
0,
1,
0,
0,
0
],
[
0,
0,
0,
0,
1,
0
],
[
0,
0,
0,
0,
0,
1
]
],
"Q": [
[
0,
0,
1,
0,
0
],
[
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0
]
],
"l": [
1,
1,
1,
0,
0
]
}
],
"coeffs": [
"sqrt(3)/9 + 1/3 + I*(-1/3 + sqrt(3)/9)",
"sqrt(6)/9 + sqrt(2)*I/3",
"sqrt(2)/3 - sqrt(6)*I/9",
"2*sqrt(3)/9 + 2*sqrt(3)*I/9",
"2*sqrt(3)/9 - 2*sqrt(3)*I/9",
"sqrt(2)/3 + sqrt(6)*I/9"
]
}
}