lean t3_m3_stabRankP_le_eight in LeanProofs.T3M3StabRank, machine-checked by Lean
Implied per-copy exponent γ ≤ 0.6309 against a published 0.5000, no improvement.
This bound is backed by a machine-checked theorem: t3_m3_stabRankP_le_eight in LeanProofs.T3M3StabRank. The recorded lake build confirms it compiles.
explicit eight-term witness; Kocia-Sarovar recorded this as 8? The eight terms are those of stabrank/examples/t3m3_rank8_certificate.py, found by annealing; here each is given in the flat-and-phase-form parametrisation and the identity is re-verified in exact arithmetic. Now at the lean tier: t3_m3_stabRankP_le_eight in LeanProofs.T3M3StabRank proves stabRankP 3 |T3⟩⊗3 ≤ 8 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": 3,
"direction": "upper",
"rank": 8,
"provenance": {
"author": "Labib and Russo",
"reference": "arXiv:2605.28586",
"method": "literature",
"date": "2026-05-27",
"github": [
"FarLab",
"vprusso"
]
},
"notes": "explicit eight-term witness; Kocia-Sarovar recorded this as 8? The eight terms are those of stabrank/examples/t3m3_rank8_certificate.py, found by annealing; here each is given in the flat-and-phase-form parametrisation and the identity is re-verified in exact arithmetic. Now at the lean tier: t3_m3_stabRankP_le_eight in LeanProofs.T3M3StabRank proves stabRankP 3 |T3>^3 <= 8 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.T3M3StabRank",
"theorem": "t3_m3_stabRankP_le_eight"
},
"witness": {
"terms": [
{
"k": 3,
"x0": [
0,
0,
0
],
"W": [
[
1,
0,
0
],
[
0,
1,
0
],
[
0,
0,
1
]
],
"Q": [
[
0,
1,
1
],
[
0,
1,
2
],
[
0,
0,
1
]
],
"l": [
1,
0,
0
]
},
{
"k": 1,
"x0": [
0,
1,
1
],
"W": [
[
1,
1,
1
]
],
"Q": [
[
1
]
],
"l": [
1
]
},
{
"k": 3,
"x0": [
0,
0,
0
],
"W": [
[
1,
0,
0
],
[
0,
1,
0
],
[
0,
0,
1
]
],
"Q": [
[
2,
1,
1
],
[
0,
0,
2
],
[
0,
0,
0
]
],
"l": [
1,
0,
0
]
},
{
"k": 3,
"x0": [
0,
0,
0
],
"W": [
[
1,
0,
0
],
[
0,
1,
0
],
[
0,
0,
1
]
],
"Q": [
[
2,
2,
2
],
[
0,
2,
2
],
[
0,
0,
2
]
],
"l": [
2,
2,
2
]
},
{
"k": 1,
"x0": [
0,
1,
1
],
"W": [
[
1,
1,
1
]
],
"Q": [
[
1
]
],
"l": [
2
]
},
{
"k": 3,
"x0": [
0,
0,
0
],
"W": [
[
1,
0,
0
],
[
0,
1,
0
],
[
0,
0,
1
]
],
"Q": [
[
2,
0,
0
],
[
0,
2,
0
],
[
0,
0,
2
]
],
"l": [
0,
0,
0
]
},
{
"k": 3,
"x0": [
0,
0,
0
],
"W": [
[
1,
0,
0
],
[
0,
1,
0
],
[
0,
0,
1
]
],
"Q": [
[
2,
1,
1
],
[
0,
2,
1
],
[
0,
0,
2
]
],
"l": [
2,
2,
2
]
},
{
"k": 2,
"x0": [
0,
0,
2
],
"W": [
[
1,
0,
2
],
[
0,
1,
2
]
],
"Q": [
[
2,
0
],
[
0,
0
]
],
"l": [
1,
0
]
}
],
"coeffs": [
"1/3 - exp(2*I*pi/3)/3",
"-exp(2*I*pi/3)/3 + exp(8*I*pi/9)/3 - exp(-8*I*pi/9)/3 + exp(2*I*pi/9)/3",
"2/3 + exp(2*I*pi/3)/3",
"-2*exp(2*I*pi/9)/3 - exp(8*I*pi/9)/3",
"-exp(2*I*pi/9)/3 + exp(-8*I*pi/9)/3 - exp(8*I*pi/9)/3 + exp(2*I*pi/3)/3",
"1/3 - exp(2*I*pi/3)/3 + exp(2*I*pi/9)/3 + 2*exp(8*I*pi/9)/3",
"-1/3 - exp(8*I*pi/9)/3 + exp(2*I*pi/9)/3 + exp(2*I*pi/3)/3",
"-sqrt(3)*exp(2*I*pi/3)/3 + sqrt(3)*exp(8*I*pi/9)/3 + sqrt(3)*exp(4*I*pi/9)/3"
]
}
}