lean h3_m4_stabRankP_le_eight in LeanProofs.H3M4StabRank, machine-checked by Lean
Implied per-copy exponent γ ≤ 0.4732 against a published 0.4206, no improvement.
This bound is backed by a machine-checked theorem: h3_m4_stabRankP_le_eight in LeanProofs.H3M4StabRank. The recorded lake build confirms it compiles.
rank 6 plateaus at √(70-37 √ 3)/12 Witness: the four m=3 terms of H3M3Pointwise tensored with the rank-2 single-copy decomposition |H3⟩ in span{|0⟩, |+⟩}, verified here in exact arithmetic. Now at the lean tier: h3_m4_stabRankP_le_eight in LeanProofs.H3M4StabRank proves stabRankP 3 |H3⟩⊗4 ≤ 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": "H3",
"m": 4,
"direction": "upper",
"rank": 8,
"provenance": {
"author": "Labib and Russo",
"reference": "arXiv:2605.28586",
"method": "literature",
"date": "2026-05-27",
"github": [
"FarLab",
"vprusso"
]
},
"notes": "rank 6 plateaus at sqrt(70-37 sqrt 3)/12 Witness: the four m=3 terms of H3M3Pointwise tensored with the rank-2 single-copy decomposition |H3> in span{|0>, |+>}, verified here in exact arithmetic. Now at the lean tier: h3_m4_stabRankP_le_eight in LeanProofs.H3M4StabRank proves stabRankP 3 |H3>^4 <= 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.H3M4StabRank",
"theorem": "h3_m4_stabRankP_le_eight"
},
"witness": {
"terms": [
{
"k": 3,
"x0": [
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0
],
[
0,
1,
0,
0
],
[
0,
0,
1,
0
]
],
"Q": [
[
2,
0,
0
],
[
0,
2,
0
],
[
0,
0,
1
]
],
"l": [
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": [
[
2,
0,
0,
0
],
[
0,
2,
0,
0
],
[
0,
0,
1,
0
],
[
0,
0,
0,
0
]
],
"l": [
0,
0,
0,
0
]
},
{
"k": 3,
"x0": [
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0
],
[
0,
1,
0,
0
],
[
0,
0,
1,
0
]
],
"Q": [
[
1,
0,
0
],
[
0,
1,
0
],
[
0,
0,
2
]
],
"l": [
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,
0,
0,
0
],
[
0,
1,
0,
0
],
[
0,
0,
2,
0
],
[
0,
0,
0,
0
]
],
"l": [
0,
0,
0,
0
]
},
{
"k": 1,
"x0": [
0,
0,
0,
0
],
"W": [
[
0,
0,
1,
0
]
],
"Q": [
[
0
]
],
"l": [
0
]
},
{
"k": 2,
"x0": [
0,
0,
0,
0
],
"W": [
[
0,
0,
1,
0
],
[
0,
0,
0,
1
]
],
"Q": [
[
0,
0
],
[
0,
0
]
],
"l": [
0,
0
]
},
{
"k": 2,
"x0": [
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0
],
[
0,
1,
0,
0
]
],
"Q": [
[
0,
0
],
[
0,
0
]
],
"l": [
0,
0
]
},
{
"k": 3,
"x0": [
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0
],
[
0,
1,
0,
0
],
[
0,
0,
0,
1
]
],
"Q": [
[
0,
0,
0
],
[
0,
0,
0
],
[
0,
0,
0
]
],
"l": [
0,
0,
0
]
}
],
"coeffs": [
"-3/16 + 3*sqrt(3)/16 + I*(-3/16 + 3*sqrt(3)/16)",
"-3/16 + 3*sqrt(3)/16 + I*(-3/16 + 3*sqrt(3)/16)",
"-3/16 + 3*sqrt(3)/16 + I*(3/16 - 3*sqrt(3)/16)",
"-3/16 + 3*sqrt(3)/16 + I*(3/16 - 3*sqrt(3)/16)",
"3/8",
"3/8",
"3/8",
"3/8"
]
}
}