lean qubit_h_m5_stabRankP_le_six in LeanProofs.QubitHM5StabRank, machine-checked by Lean
Implied per-copy exponent γ ≤ 0.5170 against a published 0.3962, no improvement.
This bound is backed by a machine-checked theorem: qubit_h_m5_stabRankP_le_six in LeanProofs.QubitHM5StabRank. The recorded lake build confirms it compiles.
1 run; 0.02 CPU-hours; 0.02 h wall-clock; on Apple silicon laptop, 8 annealing chains.
The five-copy value of Bravyi, Smith, and Smolin, found there by Monte Carlo and conjectured optimal. Witness found here by the package's annealer (search_decomposition.py, target qubit_real, seed 1, starting rank 6, one run of 8 chains) and verified in exact arithmetic. Whether rank 5 is possible at m=5 is open; the rank-3 exclusion at m=4 and projection monotonicity give χ ≥ 4 here. Now at the lean tier: qubit_h_m5_stabRankP_le_six in LeanProofs.QubitHM5StabRank proves stabRankP 2 |qubitH⟩⊗5 ≤ 6 against IsStabP 2 from this witness, the pointwise identity being decided by the kernel on integer coordinate vectors (see lean_proofs/LeanProofs/Stabilizer/Reflect.lean).
Bravyi, Smith, and Smolin · arXiv:1506.01396 · literature
{
"schema_version": "0.1",
"orbit": "qubit_H",
"m": 5,
"direction": "upper",
"rank": 6,
"provenance": {
"author": "Bravyi, Smith, and Smolin",
"reference": "arXiv:1506.01396",
"method": "literature",
"date": "2015-06-03",
"github": [],
"compute": {
"cpu_hours": 0.02,
"wall_clock_hours": 0.02,
"runs": 1,
"hardware": "Apple silicon laptop, 8 annealing chains"
}
},
"notes": "The five-copy value of Bravyi, Smith, and Smolin, found there by Monte Carlo and conjectured optimal. Witness found here by the package's annealer (search_decomposition.py, target qubit_real, seed 1, starting rank 6, one run of 8 chains) and verified in exact arithmetic. Whether rank 5 is possible at m=5 is open; the rank-3 exclusion at m=4 and projection monotonicity give chi >= 4 here. Now at the lean tier: qubit_h_m5_stabRankP_le_six in LeanProofs.QubitHM5StabRank proves stabRankP 2 |qubit_H>^5 <= 6 against IsStabP 2 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.QubitHM5StabRank",
"theorem": "qubit_h_m5_stabRankP_le_six"
},
"witness": {
"terms": [
{
"k": 4,
"x0": [
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
0
],
[
0,
1,
1,
0,
0
],
[
0,
0,
0,
1,
0
],
[
0,
0,
0,
0,
1
]
],
"Q": [
[
0,
1,
0,
1
],
[
0,
0,
1,
1
],
[
0,
0,
0,
0
],
[
0,
0,
0,
0
]
],
"l": [
2,
0,
0,
2
]
},
{
"k": 3,
"x0": [
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
1
],
[
0,
1,
1,
0,
0
],
[
0,
0,
0,
1,
0
]
],
"Q": [
[
0,
1,
0
],
[
0,
0,
1
],
[
0,
0,
0
]
],
"l": [
2,
0,
0
]
},
{
"k": 4,
"x0": [
0,
0,
0,
0,
1
],
"W": [
[
1,
0,
0,
0,
1
],
[
0,
1,
0,
0,
1
],
[
0,
0,
1,
0,
1
],
[
0,
0,
0,
1,
1
]
],
"Q": [
[
0,
1,
1,
1
],
[
0,
0,
1,
1
],
[
0,
0,
0,
1
],
[
0,
0,
0,
0
]
],
"l": [
0,
2,
2,
0
]
},
{
"k": 5,
"x0": [
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0
],
[
0,
0,
1,
0,
0
],
[
0,
0,
0,
1,
0
],
[
0,
0,
0,
0,
1
]
],
"Q": [
[
0,
1,
1,
1,
1
],
[
0,
0,
1,
1,
1
],
[
0,
0,
0,
1,
1
],
[
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0
]
],
"l": [
0,
0,
0,
2,
0
]
},
{
"k": 4,
"x0": [
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
0
],
[
0,
1,
0,
1,
0
],
[
0,
0,
1,
1,
0
],
[
0,
0,
0,
0,
1
]
],
"Q": [
[
0,
0,
0,
0
],
[
0,
0,
1,
0
],
[
0,
0,
0,
0
],
[
0,
0,
0,
0
]
],
"l": [
0,
0,
0,
0
]
},
{
"k": 5,
"x0": [
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0
],
[
0,
0,
1,
0,
0
],
[
0,
0,
0,
1,
0
],
[
0,
0,
0,
0,
1
]
],
"Q": [
[
0,
0,
0,
0,
0
],
[
0,
0,
0,
1,
0
],
[
0,
0,
0,
1,
0
],
[
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0
]
],
"l": [
0,
0,
0,
0,
0
]
}
],
"coeffs": [
"sqrt(1/2 - sqrt(2)/4)",
"sqrt(1/2 - sqrt(2)/4)",
"-sqrt(1/4 - sqrt(2)/8)",
"sqrt(1/4 - sqrt(2)/8)",
"sqrt(sqrt(2)/4 + 1/2)",
"sqrt(sqrt(2)/4 + 1/2)"
]
}
}