lean strange_m5_stabRankP_le_eight in LeanProofs.StrangeM5StabRank, machine-checked by Lean
Implied per-copy exponent γ ≤ 0.3786 against a published 0.3155, no improvement.
This bound is backed by a machine-checked theorem: strange_m5_stabRankP_le_eight in LeanProofs.StrangeM5StabRank. The recorded lake build confirms it compiles.
1 run; 0.001 CPU-hours; 0.001 h wall-clock; on Apple silicon laptop.
First entry for this cell. Witness: the eight products of the two m=2 terms, twice, with the two single-copy terms |1⟩, |2⟩; γ = log_3(8)/5 = 0.379, above the published 0.3155 (which the m=2 identity attains), so this fills the cell rather than moving the exponent. Beating the exponent at m=5 would need rank 5. Now at the lean tier: strange_m5_stabRankP_le_eight in LeanProofs.StrangeM5StabRank proves stabRankP 3 |S⟩⊗5 ≤ 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).
this repository · product of board witnesses · tensor product of verified lower-m witnesses
{
"schema_version": "0.1",
"orbit": "S",
"m": 5,
"direction": "upper",
"rank": 8,
"lean": {
"module": "LeanProofs.StrangeM5StabRank",
"theorem": "strange_m5_stabRankP_le_eight"
},
"witness": {
"terms": [
{
"k": 4,
"x0": [
0,
0,
0,
0,
1
],
"W": [
[
1,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0
],
[
0,
0,
1,
0,
0
],
[
0,
0,
0,
1,
0
]
],
"Q": [
[
1,
1,
0,
0
],
[
0,
1,
0,
0
],
[
0,
0,
1,
1
],
[
0,
0,
0,
1
]
],
"l": [
0,
0,
0,
0
]
},
{
"k": 4,
"x0": [
0,
0,
0,
0,
2
],
"W": [
[
1,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0
],
[
0,
0,
1,
0,
0
],
[
0,
0,
0,
1,
0
]
],
"Q": [
[
1,
1,
0,
0
],
[
0,
1,
0,
0
],
[
0,
0,
1,
1
],
[
0,
0,
0,
1
]
],
"l": [
0,
0,
0,
0
]
},
{
"k": 4,
"x0": [
0,
0,
0,
0,
1
],
"W": [
[
1,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0
],
[
0,
0,
1,
0,
0
],
[
0,
0,
0,
1,
0
]
],
"Q": [
[
1,
1,
0,
0
],
[
0,
1,
0,
0
],
[
0,
0,
1,
2
],
[
0,
0,
0,
1
]
],
"l": [
0,
0,
0,
0
]
},
{
"k": 4,
"x0": [
0,
0,
0,
0,
2
],
"W": [
[
1,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0
],
[
0,
0,
1,
0,
0
],
[
0,
0,
0,
1,
0
]
],
"Q": [
[
1,
1,
0,
0
],
[
0,
1,
0,
0
],
[
0,
0,
1,
2
],
[
0,
0,
0,
1
]
],
"l": [
0,
0,
0,
0
]
},
{
"k": 4,
"x0": [
0,
0,
0,
0,
1
],
"W": [
[
1,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0
],
[
0,
0,
1,
0,
0
],
[
0,
0,
0,
1,
0
]
],
"Q": [
[
1,
2,
0,
0
],
[
0,
1,
0,
0
],
[
0,
0,
1,
1
],
[
0,
0,
0,
1
]
],
"l": [
0,
0,
0,
0
]
},
{
"k": 4,
"x0": [
0,
0,
0,
0,
2
],
"W": [
[
1,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0
],
[
0,
0,
1,
0,
0
],
[
0,
0,
0,
1,
0
]
],
"Q": [
[
1,
2,
0,
0
],
[
0,
1,
0,
0
],
[
0,
0,
1,
1
],
[
0,
0,
0,
1
]
],
"l": [
0,
0,
0,
0
]
},
{
"k": 4,
"x0": [
0,
0,
0,
0,
1
],
"W": [
[
1,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0
],
[
0,
0,
1,
0,
0
],
[
0,
0,
0,
1,
0
]
],
"Q": [
[
1,
2,
0,
0
],
[
0,
1,
0,
0
],
[
0,
0,
1,
2
],
[
0,
0,
0,
1
]
],
"l": [
0,
0,
0,
0
]
},
{
"k": 4,
"x0": [
0,
0,
0,
0,
2
],
"W": [
[
1,
0,
0,
0,
0
],
[
0,
1,
0,
0,
0
],
[
0,
0,
1,
0,
0
],
[
0,
0,
0,
1,
0
]
],
"Q": [
[
1,
2,
0,
0
],
[
0,
1,
0,
0
],
[
0,
0,
1,
2
],
[
0,
0,
0,
1
]
],
"l": [
0,
0,
0,
0
]
}
],
"coeffs": [
"3*sqrt(2)/16 + 3*sqrt(6)*I/16",
"-3*sqrt(2)/16 - 3*sqrt(6)*I/16",
"-3*sqrt(2)/16 - 3*sqrt(6)*I/16",
"3*sqrt(2)/16 + 3*sqrt(6)*I/16",
"-3*sqrt(2)/16 - 3*sqrt(6)*I/16",
"3*sqrt(2)/16 + 3*sqrt(6)*I/16",
"3*sqrt(2)/16 + 3*sqrt(6)*I/16",
"-3*sqrt(2)/16 - 3*sqrt(6)*I/16"
]
},
"provenance": {
"author": "this repository",
"reference": "product of board witnesses",
"method": "tensor product of verified lower-m witnesses",
"date": "2026-09-18",
"github": [
"vprusso"
],
"compute": {
"cpu_hours": 0.001,
"wall_clock_hours": 0.001,
"runs": 1,
"hardware": "Apple silicon laptop"
}
},
"notes": "First entry for this cell. Witness: the eight products of the two m=2 terms, twice, with the two single-copy terms |1>, |2>; gamma = log_3(8)/5 = 0.379, above the published 0.3155 (which the m=2 identity attains), so this fills the cell rather than moving the exponent. Beating the exponent at m=5 would need rank 5. Now at the lean tier: strange_m5_stabRankP_le_eight in LeanProofs.StrangeM5StabRank proves stabRankP 3 |S>^5 <= 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)."
}