lean t3_m4_stabRankP_le_nine in LeanProofs.T3M4StabRank, machine-checked by Lean
Implied per-copy exponent γ ≤ 0.5000 against a published 0.5000, no improvement.
This bound is backed by a machine-checked theorem: t3_m4_stabRankP_le_nine in LeanProofs.T3M4StabRank. The recorded lake build confirms it compiles.
nine-term product witness from the m=2 carry decomposition Witness: the nine products vs ⊗ vt of the m=2 carry blocks, verified here in exact arithmetic. Now at the lean tier: t3_m4_stabRankP_le_nine in LeanProofs.T3M4StabRank proves stabRankP 3 |T3⟩⊗4 ≤ 9 against IsStabP 3 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": "T3",
"m": 4,
"direction": "upper",
"rank": 9,
"provenance": {
"author": "Labib and Russo",
"reference": "arXiv:2605.28586",
"method": "literature",
"date": "2026-05-27",
"github": [
"FarLab",
"vprusso"
]
},
"notes": "nine-term product witness from the m=2 carry decomposition Witness: the nine products v_s (x) v_t of the m=2 carry blocks, verified here in exact arithmetic. Now at the lean tier: t3_m4_stabRankP_le_nine in LeanProofs.T3M4StabRank proves stabRankP 3 |T3>^4 <= 9 against IsStabP 3 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.T3M4StabRank",
"theorem": "t3_m4_stabRankP_le_nine"
},
"witness": {
"terms": [
{
"k": 2,
"x0": [
0,
0,
0,
0
],
"W": [
[
1,
2,
0,
0
],
[
0,
0,
1,
2
]
],
"Q": [
[
1,
0
],
[
0,
1
]
],
"l": [
0,
0
]
},
{
"k": 2,
"x0": [
0,
0,
0,
1
],
"W": [
[
1,
2,
0,
0
],
[
0,
0,
1,
2
]
],
"Q": [
[
1,
0
],
[
0,
2
]
],
"l": [
0,
1
]
},
{
"k": 2,
"x0": [
0,
0,
0,
2
],
"W": [
[
1,
2,
0,
0
],
[
0,
0,
1,
2
]
],
"Q": [
[
1,
0
],
[
0,
0
]
],
"l": [
0,
0
]
},
{
"k": 2,
"x0": [
0,
1,
0,
0
],
"W": [
[
1,
2,
0,
0
],
[
0,
0,
1,
2
]
],
"Q": [
[
2,
0
],
[
0,
1
]
],
"l": [
1,
0
]
},
{
"k": 2,
"x0": [
0,
1,
0,
1
],
"W": [
[
1,
2,
0,
0
],
[
0,
0,
1,
2
]
],
"Q": [
[
2,
0
],
[
0,
2
]
],
"l": [
1,
1
]
},
{
"k": 2,
"x0": [
0,
1,
0,
2
],
"W": [
[
1,
2,
0,
0
],
[
0,
0,
1,
2
]
],
"Q": [
[
2,
0
],
[
0,
0
]
],
"l": [
1,
0
]
},
{
"k": 2,
"x0": [
0,
2,
0,
0
],
"W": [
[
1,
2,
0,
0
],
[
0,
0,
1,
2
]
],
"Q": [
[
0,
0
],
[
0,
1
]
],
"l": [
0,
0
]
},
{
"k": 2,
"x0": [
0,
2,
0,
1
],
"W": [
[
1,
2,
0,
0
],
[
0,
0,
1,
2
]
],
"Q": [
[
0,
0
],
[
0,
2
]
],
"l": [
0,
1
]
},
{
"k": 2,
"x0": [
0,
2,
0,
2
],
"W": [
[
1,
2,
0,
0
],
[
0,
0,
1,
2
]
],
"Q": [
[
0,
0
],
[
0,
0
]
],
"l": [
0,
0
]
}
],
"coeffs": [
"1/3",
"exp(2*I*pi/9)/3",
"exp(4*I*pi/9)/3",
"exp(2*I*pi/9)/3",
"exp(4*I*pi/9)/3",
"exp(2*I*pi/3)/3",
"exp(4*I*pi/9)/3",
"exp(2*I*pi/3)/3",
"exp(8*I*pi/9)/3"
]
}
}