lean strange_m4_stabRank_le_four 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_m4_stabRank_le_four in LeanProofs.TensorStabRank. The recorded lake build confirms it compiles.
tight Witness: the four products of the two m=2 terms, verified here in exact arithmetic.
Labib and Russo · arXiv:2605.28586 · literature
{
"schema_version": "0.1",
"orbit": "S",
"m": 4,
"direction": "upper",
"rank": 4,
"provenance": {
"author": "Labib and Russo",
"reference": "arXiv:2605.28586",
"method": "literature",
"date": "2026-05-27",
"github": [
"FarLab",
"vprusso"
]
},
"notes": "tight Witness: the four products of the two m=2 terms, verified here in exact arithmetic.",
"witness": {
"terms": [
{
"k": 4,
"x0": [
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0
],
[
0,
1,
0,
0
],
[
0,
0,
1,
0
],
[
0,
0,
0,
1
]
],
"Q": [
[
1,
1,
0,
0
],
[
0,
1,
0,
0
],
[
0,
0,
1,
1
],
[
0,
0,
0,
1
]
],
"l": [
0,
0,
0,
0
]
},
{
"k": 4,
"x0": [
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0
],
[
0,
1,
0,
0
],
[
0,
0,
1,
0
],
[
0,
0,
0,
1
]
],
"Q": [
[
1,
1,
0,
0
],
[
0,
1,
0,
0
],
[
0,
0,
1,
2
],
[
0,
0,
0,
1
]
],
"l": [
0,
0,
0,
0
]
},
{
"k": 4,
"x0": [
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0
],
[
0,
1,
0,
0
],
[
0,
0,
1,
0
],
[
0,
0,
0,
1
]
],
"Q": [
[
1,
2,
0,
0
],
[
0,
1,
0,
0
],
[
0,
0,
1,
1
],
[
0,
0,
0,
1
]
],
"l": [
0,
0,
0,
0
]
},
{
"k": 4,
"x0": [
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0
],
[
0,
1,
0,
0
],
[
0,
0,
1,
0
],
[
0,
0,
0,
1
]
],
"Q": [
[
1,
2,
0,
0
],
[
0,
1,
0,
0
],
[
0,
0,
1,
2
],
[
0,
0,
0,
1
]
],
"l": [
0,
0,
0,
0
]
}
],
"coeffs": [
"3/8 + 3*sqrt(3)*I/8",
"-3/8 - 3*sqrt(3)*I/8",
"-3/8 - 3*sqrt(3)*I/8",
"3/8 + 3*sqrt(3)*I/8"
]
},
"lean": {
"module": "LeanProofs.TensorStabRank",
"theorem": "strange_m4_stabRank_le_four"
}
}