lean qubit_t_m4_stabRankP_le_three in LeanProofs.QubitTM4StabRank, machine-checked by Lean
Implied per-copy exponent γ ≤ 0.3962 against a published 0.3962, no improvement.
This bound is backed by a machine-checked theorem: qubit_t_m4_stabRankP_le_three in LeanProofs.QubitTM4StabRank. The recorded lake build confirms it compiles.
matches the QPG exponent by direct algebra Witness: the three states sigma_1, sigma_2, sigma_3 of LeanProofs.QubitTM4, with phases in the fourth roots of unity, verified here in exact arithmetic. The Lean module was broken and orphaned from the library root when this witness was added; its main case proof has since been rewritten (one controlled simp only, then linear_combination over I*I = -1 and √2*√2 = 2) and it builds, so the cell now holds the lean tier with the witness as an independent check.
Labib and Russo · arXiv:2605.28586 · literature
{
"schema_version": "0.1",
"orbit": "qubit_T",
"m": 4,
"direction": "upper",
"rank": 3,
"provenance": {
"author": "Labib and Russo",
"reference": "arXiv:2605.28586",
"method": "literature",
"date": "2026-05-27",
"github": [
"FarLab",
"vprusso"
]
},
"notes": "matches the QPG exponent by direct algebra Witness: the three states sigma_1, sigma_2, sigma_3 of LeanProofs.QubitTM4, with phases in the fourth roots of unity, verified here in exact arithmetic. The Lean module was broken and orphaned from the library root when this witness was added; its main case proof has since been rewritten (one controlled simp only, then linear_combination over I*I = -1 and sqrt2*sqrt2 = 2) and it builds, so the cell now holds the lean tier with the witness as an independent check.",
"lean": {
"module": "LeanProofs.QubitTM4StabRank",
"theorem": "qubit_t_m4_stabRankP_le_three"
},
"witness": {
"terms": [
{
"k": 3,
"x0": [
0,
0,
0,
0
],
"W": [
[
1,
0,
1,
0
],
[
0,
1,
0,
0
],
[
0,
0,
0,
1
]
],
"Q": [
[
0,
0,
0
],
[
0,
0,
1
],
[
0,
0,
0
]
],
"l": [
1,
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,
0,
1,
0
],
[
0,
0,
0,
1
],
[
0,
0,
0,
0
],
[
0,
0,
0,
0
]
],
"l": [
0,
1,
0,
1
]
},
{
"k": 3,
"x0": [
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0
],
[
0,
1,
0,
1
],
[
0,
0,
1,
0
]
],
"Q": [
[
0,
0,
1
],
[
0,
0,
0
],
[
0,
0,
0
]
],
"l": [
1,
1,
1
]
}
],
"coeffs": [
"sqrt(sqrt(3)/9 + 2/9) + I*sqrt(2/9 - sqrt(3)/9)",
"2/3",
"sqrt(sqrt(3)/9 + 2/9) - I*sqrt(2/9 - sqrt(3)/9)"
]
}
}