lean strange_m6_stabRank_le_eight in LeanProofs.TensorStabRank, machine-checked by Lean
Implied per-copy exponent γ ≤ 0.3155 against a published 0.3155, no improvement.
This bound is backed by a machine-checked theorem: strange_m6_stabRank_le_eight in LeanProofs.TensorStabRank. The recorded lake build confirms it compiles.
2^3 from the m=2 identity; rank 7 plateaus at √(8/27) Witness: the eight triple products of the two m=2 terms, verified here in exact arithmetic on all 729 amplitudes.
Labib and Russo · arXiv:2605.28586 · literature
{
"schema_version": "0.1",
"orbit": "S",
"m": 6,
"direction": "upper",
"rank": 8,
"provenance": {
"author": "Labib and Russo",
"reference": "arXiv:2605.28586",
"method": "literature",
"date": "2026-05-27",
"github": [
"FarLab",
"vprusso"
]
},
"notes": "2^3 from the m=2 identity; rank 7 plateaus at sqrt(8/27) Witness: the eight triple products of the two m=2 terms, verified here in exact arithmetic on all 729 amplitudes.",
"witness": {
"terms": [
{
"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": [
[
1,
1,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0,
0
],
[
0,
0,
1,
1,
0,
0
],
[
0,
0,
0,
1,
0,
0
],
[
0,
0,
0,
0,
1,
1
],
[
0,
0,
0,
0,
0,
1
]
],
"l": [
0,
0,
0,
0,
0,
0
]
},
{
"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": [
[
1,
1,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0,
0
],
[
0,
0,
1,
1,
0,
0
],
[
0,
0,
0,
1,
0,
0
],
[
0,
0,
0,
0,
1,
2
],
[
0,
0,
0,
0,
0,
1
]
],
"l": [
0,
0,
0,
0,
0,
0
]
},
{
"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": [
[
1,
1,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0,
0
],
[
0,
0,
1,
2,
0,
0
],
[
0,
0,
0,
1,
0,
0
],
[
0,
0,
0,
0,
1,
1
],
[
0,
0,
0,
0,
0,
1
]
],
"l": [
0,
0,
0,
0,
0,
0
]
},
{
"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": [
[
1,
1,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0,
0
],
[
0,
0,
1,
2,
0,
0
],
[
0,
0,
0,
1,
0,
0
],
[
0,
0,
0,
0,
1,
2
],
[
0,
0,
0,
0,
0,
1
]
],
"l": [
0,
0,
0,
0,
0,
0
]
},
{
"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": [
[
1,
2,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0,
0
],
[
0,
0,
1,
1,
0,
0
],
[
0,
0,
0,
1,
0,
0
],
[
0,
0,
0,
0,
1,
1
],
[
0,
0,
0,
0,
0,
1
]
],
"l": [
0,
0,
0,
0,
0,
0
]
},
{
"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": [
[
1,
2,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0,
0
],
[
0,
0,
1,
1,
0,
0
],
[
0,
0,
0,
1,
0,
0
],
[
0,
0,
0,
0,
1,
2
],
[
0,
0,
0,
0,
0,
1
]
],
"l": [
0,
0,
0,
0,
0,
0
]
},
{
"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": [
[
1,
2,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0,
0
],
[
0,
0,
1,
2,
0,
0
],
[
0,
0,
0,
1,
0,
0
],
[
0,
0,
0,
0,
1,
1
],
[
0,
0,
0,
0,
0,
1
]
],
"l": [
0,
0,
0,
0,
0,
0
]
},
{
"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": [
[
1,
2,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0,
0
],
[
0,
0,
1,
2,
0,
0
],
[
0,
0,
0,
1,
0,
0
],
[
0,
0,
0,
0,
1,
2
],
[
0,
0,
0,
0,
0,
1
]
],
"l": [
0,
0,
0,
0,
0,
0
]
}
],
"coeffs": [
"3*sqrt(3)*I/8",
"-3*sqrt(3)*I/8",
"-3*sqrt(3)*I/8",
"3*sqrt(3)*I/8",
"-3*sqrt(3)*I/8",
"3*sqrt(3)*I/8",
"3*sqrt(3)*I/8",
"-3*sqrt(3)*I/8"
]
},
"lean": {
"module": "LeanProofs.TensorStabRank",
"theorem": "strange_m6_stabRank_le_eight"
}
}