lean qubit_h_m4_stabRankP_le_four in LeanProofs.QubitHStabRank, machine-checked by Lean
Implied per-copy exponent γ ≤ 0.5000 against a published 0.3962, no improvement.
This bound is backed by a machine-checked theorem: qubit_h_m4_stabRankP_le_four in LeanProofs.QubitHStabRank. The recorded lake build confirms it compiles.
1 run; 0.01 CPU-hours; 0.01 h wall-clock; on Apple silicon laptop, 8 annealing chains.
Witness found here by the package's annealer (search_decomposition.py, target qubit_real, seed 1, one run of 8 chains) and re-verified in exact arithmetic with coefficients recovered by fit_coeffs.
Labib and Russo · arXiv:2605.28586 · literature
{
"schema_version": "0.1",
"orbit": "qubit_H",
"m": 4,
"direction": "upper",
"rank": 4,
"provenance": {
"author": "Labib and Russo",
"reference": "arXiv:2605.28586",
"method": "literature",
"date": "2026-05-27",
"github": [
"FarLab",
"vprusso"
],
"compute": {
"cpu_hours": 0.01,
"wall_clock_hours": 0.01,
"runs": 1,
"hardware": "Apple silicon laptop, 8 annealing chains"
}
},
"notes": "Witness found here by the package's annealer (search_decomposition.py, target qubit_real, seed 1, one run of 8 chains) and re-verified in exact arithmetic with coefficients recovered by fit_coeffs.",
"lean": {
"module": "LeanProofs.QubitHStabRank",
"theorem": "qubit_h_m4_stabRankP_le_four"
},
"witness": {
"terms": [
{
"k": 3,
"x0": [
0,
0,
0,
1
],
"W": [
[
1,
0,
0,
1
],
[
0,
1,
0,
1
],
[
0,
0,
1,
1
]
],
"Q": [
[
0,
0,
0
],
[
0,
0,
0
],
[
0,
0,
0
]
],
"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": [
[
0,
1,
1,
1
],
[
0,
0,
1,
1
],
[
0,
0,
0,
1
],
[
0,
0,
0,
0
]
],
"l": [
2,
2,
2,
2
]
},
{
"k": 1,
"x0": [
0,
0,
0,
0
],
"W": [
[
1,
1,
1,
1
]
],
"Q": [
[
0
]
],
"l": [
2
]
},
{
"k": 1,
"x0": [
0,
0,
0,
0
],
"W": [
[
1,
1,
1,
1
]
],
"Q": [
[
0
]
],
"l": [
0
]
}
],
"coeffs": [
"1/2",
"-1/2",
"1/2",
"sqrt(2)/2"
]
}
}