lean qubit_h_m6_stabRankP_le_six in LeanProofs.QubitHM6StabRank, machine-checked by Lean
Implied per-copy exponent γ ≤ 0.4308 against a published 0.3962, no improvement.
This bound is backed by a machine-checked theorem: qubit_h_m6_stabRankP_le_six in LeanProofs.QubitHM6StabRank. The recorded lake build confirms it compiles.
χ(|H⟩⊗6) ≤ 6 from the cat-state construction: |T⟩⊗6 = (|cat6⟩ + |cat_6^→)/√ 2 with |cat_6^+→ = (|T⟩⊗6 +- |Tperp⟩⊗6)/√ 2, and |cat6⟩ = 2^{-3/2}(|0^6> - i|1^6>) + 2^{-1/2} e^{3 i π/4}(|E6⟩ + i|K6⟩) has rank 3 (their Eq. 7), which refuted the conjecture of Bravyi, Smith, and Smolin that χ(|H⟩⊗6) = 7 and gives exponent log_2(6)/6 = 0.431. Witness built here: a single-qubit Clifford C with C|T⟩ proportional to |H⟩ is applied to the three QPG terms, giving a cat-like state a|H⟩⊗6 + b|Hperp⟩⊗6, and Hadamard on five of the six qubits, which fixes |H⟩ and negates |Hperp⟩, gives a second one with a different relative phase; |H⟩⊗6 is a combination of the two, so the six Clifford images span it. Verified here in exact arithmetic. This entry restores the value an earlier revision had listed under Bravyi and Gosset (arXiv:1601.07601, which bounds the approximate rank only) and then, in a faulty correction, replaced by 7. Now at the lean tier: qubit_h_m6_stabRankP_le_six in LeanProofs.QubitHM6StabRank proves stabRankP 2 |qubitH⟩⊗6 ≤ 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).
Qassim, Pashayan, and Gosset · arXiv:2106.07740 · literature
{
"schema_version": "0.1",
"orbit": "qubit_H",
"m": 6,
"direction": "upper",
"rank": 6,
"lean": {
"module": "LeanProofs.QubitHM6StabRank",
"theorem": "qubit_h_m6_stabRankP_le_six"
},
"witness": {
"terms": [
{
"k": 6,
"x0": [
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0,
0
],
[
0,
0,
1,
0,
0,
0
],
[
0,
0,
0,
1,
0,
0
],
[
0,
0,
0,
0,
1,
0
],
[
0,
0,
0,
0,
0,
1
]
],
"Q": [
[
0,
1,
1,
1,
1,
1
],
[
0,
0,
1,
1,
1,
1
],
[
0,
0,
0,
1,
1,
1
],
[
0,
0,
0,
0,
1,
1
],
[
0,
0,
0,
0,
0,
1
],
[
0,
0,
0,
0,
0,
0
]
],
"l": [
2,
2,
2,
2,
2,
2
]
},
{
"k": 1,
"x0": [
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
1,
1,
1,
1,
1
]
],
"Q": [
[
0
]
],
"l": [
2
]
},
{
"k": 5,
"x0": [
0,
0,
0,
0,
0,
1
],
"W": [
[
1,
0,
0,
0,
0,
1
],
[
0,
1,
0,
0,
0,
1
],
[
0,
0,
1,
0,
0,
1
],
[
0,
0,
0,
1,
0,
1
],
[
0,
0,
0,
0,
1,
1
]
],
"Q": [
[
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0
],
[
0,
0,
0,
0,
0
]
],
"l": [
0,
0,
0,
0,
0
]
},
{
"k": 5,
"x0": [
0,
0,
0,
0,
0,
1
],
"W": [
[
1,
0,
0,
0,
0,
1
],
[
0,
1,
0,
0,
0,
1
],
[
0,
0,
1,
0,
0,
1
],
[
0,
0,
0,
1,
0,
1
],
[
0,
0,
0,
0,
1,
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": [
2,
2,
2,
2,
2
]
},
{
"k": 6,
"x0": [
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0,
0
],
[
0,
0,
1,
0,
0,
0
],
[
0,
0,
0,
1,
0,
0
],
[
0,
0,
0,
0,
1,
0
],
[
0,
0,
0,
0,
0,
1
]
],
"Q": [
[
0,
0,
0,
0,
0,
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
],
[
0,
0,
0,
0,
0,
0
]
],
"l": [
0,
0,
0,
0,
0,
2
]
},
{
"k": 2,
"x0": [
0,
0,
0,
0,
0,
0
],
"W": [
[
1,
1,
1,
1,
1,
0
],
[
0,
0,
0,
0,
0,
1
]
],
"Q": [
[
0,
1
],
[
0,
0
]
],
"l": [
2,
0
]
}
],
"coeffs": [
"-sqrt(2)/4",
"1/2",
"1/2",
"-sqrt(2)/4",
"1/2",
"1/2"
]
},
"provenance": {
"author": "Qassim, Pashayan, and Gosset",
"reference": "arXiv:2106.07740",
"method": "literature",
"date": "2021-06-14",
"github": []
},
"notes": "chi(|H>^6) <= 6 from the cat-state construction: |T>^6 = (|cat_6> + |cat_6^->)/sqrt 2 with |cat_6^+-> = (|T>^6 +- |T_perp>^6)/sqrt 2, and |cat_6> = 2^{-3/2}(|0^6> - i|1^6>) + 2^{-1/2} e^{3 i pi/4}(|E_6> + i|K_6>) has rank 3 (their Eq. 7), which refuted the conjecture of Bravyi, Smith, and Smolin that chi(|H>^6) = 7 and gives exponent log_2(6)/6 = 0.431. Witness built here: a single-qubit Clifford C with C|T> proportional to |H> is applied to the three QPG terms, giving a cat-like state a|H>^6 + b|H_perp>^6, and Hadamard on five of the six qubits, which fixes |H> and negates |H_perp>, gives a second one with a different relative phase; |H>^6 is a combination of the two, so the six Clifford images span it. Verified here in exact arithmetic. This entry restores the value an earlier revision had listed under Bravyi and Gosset (arXiv:1601.07601, which bounds the approximate rank only) and then, in a faulty correction, replaced by 7. Now at the lean tier: qubit_h_m6_stabRankP_le_six in LeanProofs.QubitHM6StabRank proves stabRankP 2 |qubit_H>^6 <= 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)."
}