lean t3_m5_stabRankP_le_eighteen in LeanProofs.T3M5StabRank, machine-checked by Lean
Implied per-copy exponent γ ≤ 0.5262 against a published 0.5000, no improvement.
This bound is backed by a machine-checked theorem: t3_m5_stabRankP_le_eighteen in LeanProofs.T3M5StabRank. The recorded lake build confirms it compiles.
8 runs; 0.6 CPU-hours; 0.5 h wall-clock; on Apple silicon laptop under heavy load from other jobs, 8 annealing chains per run; claude-fable-5-1, designed the sector decomposition and drove the search.
First entry for this cell; γ = log_3(18)/5 = 0.526 is above the published 1/2, so it fills the cell rather than moving the exponent. The construction is the qutrit analogue of the Qassim-Pashayan-Gosset cat state: since Z ta = t_{a+3}, the three Galois-conjugate cat states cj = sum_i ω3^{ij} t_{1+3i}^{ot 5} are the Z^{ot 5} eigensector projections of |T3⟩⊗5, each living in a 3^4-dimensional stabilizer code, and |T3⟩⊗5 = sum_j cj / 3. Each sector's rank is the stabilizer rank of a 4-qutrit carry state; the annealer found rank 6 for each (from a rank-8 start, pruned) and rank 5 failed in five runs with residuals between 0.455 and 0.494, which is not a clean plateau. Rank 5 in every sector would give χ(|T3⟩⊗5) ≤ 15 and exponent 0.493, the first value below 1/2 for this orbit, and would propagate by the contraction cj ⊗ ck → c_{j+k} to exponent 0.491 at m = 8; a rank-4 exclusion inside the 81-dimensional code is the natural companion. At m = 3 and m = 4 the sector states have rank exactly 3 (exhaustive), reproducing 9 and 9 against the board's 8 and 9, so the route gains nothing there. Now at the lean tier: t3_m5_stabRankP_le_eighteen in LeanProofs.T3M5StabRank proves stabRankP 3 |T3⟩⊗5 ≤ 18 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 · stabrank sector-state search · Z^5 sector (qutrit cat-state) decomposition: each of the three sector projections of |T3⟩⊗5 is a 4-qutrit carry state, annealed to rank 6 on its code space and lifted; exact coefficients over Q(ω9)
{
"schema_version": "0.1",
"orbit": "T3",
"m": 5,
"direction": "upper",
"rank": 18,
"lean": {
"module": "LeanProofs.T3M5StabRank",
"theorem": "t3_m5_stabRankP_le_eighteen"
},
"witness": {
"terms": [
{
"k": 4,
"x0": [
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
2
],
[
0,
1,
0,
0,
2
],
[
0,
0,
1,
0,
2
],
[
0,
0,
0,
1,
2
]
],
"Q": [
[
1,
2,
2,
2
],
[
0,
1,
2,
2
],
[
0,
0,
1,
2
],
[
0,
0,
0,
0
]
],
"l": [
0,
0,
0,
1
]
},
{
"k": 3,
"x0": [
0,
0,
0,
2,
1
],
"W": [
[
1,
0,
0,
0,
2
],
[
0,
1,
0,
0,
2
],
[
0,
0,
1,
0,
2
]
],
"Q": [
[
2,
0,
0
],
[
0,
2,
0
],
[
0,
0,
2
]
],
"l": [
1,
1,
1
]
},
{
"k": 3,
"x0": [
0,
0,
0,
2,
1
],
"W": [
[
1,
0,
0,
1,
1
],
[
0,
1,
0,
1,
1
],
[
0,
0,
1,
0,
2
]
],
"Q": [
[
2,
1,
0
],
[
0,
2,
0
],
[
0,
0,
2
]
],
"l": [
1,
1,
1
]
},
{
"k": 4,
"x0": [
0,
0,
0,
0,
0
],
"W": [
[
1,
0,
0,
0,
2
],
[
0,
1,
0,
0,
2
],
[
0,
0,
1,
0,
2
],
[
0,
0,
0,
1,
2
]
],
"Q": [
[
0,
1,
1,
1
],
[
0,
0,
1,
1
],
[
0,
0,
0,
1
],
[
0,
0,
0,
2
]
],
"l": [
2,
2,
2,
2
]
},
{
"k": 3,
"x0": [
0,
0,
0,
0,
0
],
"W": [
[
1,
1,
0,
0,
1
],
[
0,
0,
1,
0,
2
],
[
0,
0,
0,
1,
2
]
],
"Q": [
[
0,
0,
1
],
[
0,
2,
0
],
[
0,
0,
0
]
],
"l": [
1,
1,
1
]
},
{
"k": 3,
"x0": [
0,
0,
0,
2,
1
],
"W": [
[
1,
0,
0,
2,
0
],
[
0,
1,
0,
2,
0
],
[
0,
0,
1,
1,
1
]
],
"Q": [
[
0,
2,
1
],
[
0,
0,
1
],
[
0,
0,
0
]
],
"l": [
0,
0,
0
]
},
{
"k": 4,
"x0": [
0,
0,
0,
0,
1
],
"W": [
[
1,
0,
0,
0,
2
],
[
0,
1,
0,
0,
2
],
[
0,
0,
1,
0,
2
],
[
0,
0,
0,
1,
2
]
],
"Q": [
[
2,
0,
0,
0
],
[
0,
1,
2,
1
],
[
0,
0,
1,
1
],
[
0,
0,
0,
2
]
],
"l": [
1,
1,
1,
2
]
},
{
"k": 4,
"x0": [
0,
0,
0,
0,
1
],
"W": [
[
1,
0,
0,
0,
2
],
[
0,
1,
0,
0,
2
],
[
0,
0,
1,
0,
2
],
[
0,
0,
0,
1,
2
]
],
"Q": [
[
0,
1,
1,
1
],
[
0,
0,
1,
1
],
[
0,
0,
0,
1
],
[
0,
0,
0,
1
]
],
"l": [
1,
1,
1,
2
]
},
{
"k": 4,
"x0": [
0,
0,
0,
0,
1
],
"W": [
[
1,
0,
0,
0,
2
],
[
0,
1,
0,
0,
2
],
[
0,
0,
1,
0,
2
],
[
0,
0,
0,
1,
2
]
],
"Q": [
[
1,
2,
2,
2
],
[
0,
0,
0,
0
],
[
0,
0,
0,
0
],
[
0,
0,
0,
0
]
],
"l": [
1,
2,
2,
2
]
},
{
"k": 4,
"x0": [
0,
0,
0,
0,
1
],
"W": [
[
1,
0,
0,
0,
2
],
[
0,
1,
0,
0,
2
],
[
0,
0,
1,
0,
2
],
[
0,
0,
0,
1,
2
]
],
"Q": [
[
0,
1,
1,
1
],
[
0,
0,
0,
1
],
[
0,
0,
0,
1
],
[
0,
0,
0,
0
]
],
"l": [
1,
2,
2,
1
]
},
{
"k": 4,
"x0": [
0,
0,
0,
0,
1
],
"W": [
[
1,
0,
0,
0,
2
],
[
0,
1,
0,
0,
2
],
[
0,
0,
1,
0,
2
],
[
0,
0,
0,
1,
2
]
],
"Q": [
[
2,
0,
0,
0
],
[
0,
0,
1,
0
],
[
0,
0,
0,
0
],
[
0,
0,
0,
0
]
],
"l": [
1,
1,
1,
0
]
},
{
"k": 3,
"x0": [
0,
0,
0,
0,
1
],
"W": [
[
1,
0,
0,
0,
2
],
[
0,
1,
1,
0,
1
],
[
0,
0,
0,
1,
2
]
],
"Q": [
[
1,
1,
2
],
[
0,
1,
1
],
[
0,
0,
2
]
],
"l": [
1,
0,
1
]
},
{
"k": 4,
"x0": [
0,
0,
0,
0,
2
],
"W": [
[
1,
0,
0,
0,
2
],
[
0,
1,
0,
0,
2
],
[
0,
0,
1,
0,
2
],
[
0,
0,
0,
1,
2
]
],
"Q": [
[
2,
2,
2,
2
],
[
0,
2,
2,
2
],
[
0,
0,
2,
2
],
[
0,
0,
0,
2
]
],
"l": [
2,
2,
2,
2
]
},
{
"k": 4,
"x0": [
0,
0,
0,
0,
2
],
"W": [
[
1,
0,
0,
0,
2
],
[
0,
1,
0,
0,
2
],
[
0,
0,
1,
0,
2
],
[
0,
0,
0,
1,
2
]
],
"Q": [
[
1,
1,
1,
1
],
[
0,
1,
1,
1
],
[
0,
0,
1,
1
],
[
0,
0,
0,
1
]
],
"l": [
1,
1,
1,
1
]
},
{
"k": 4,
"x0": [
0,
0,
0,
0,
2
],
"W": [
[
1,
0,
0,
0,
2
],
[
0,
1,
0,
0,
2
],
[
0,
0,
1,
0,
2
],
[
0,
0,
0,
1,
2
]
],
"Q": [
[
1,
0,
0,
1
],
[
0,
0,
0,
0
],
[
0,
0,
0,
0
],
[
0,
0,
0,
1
]
],
"l": [
2,
0,
0,
2
]
},
{
"k": 4,
"x0": [
0,
0,
0,
0,
2
],
"W": [
[
1,
0,
0,
0,
2
],
[
0,
1,
0,
0,
2
],
[
0,
0,
1,
0,
2
],
[
0,
0,
0,
1,
2
]
],
"Q": [
[
2,
2,
0,
1
],
[
0,
1,
0,
2
],
[
0,
0,
0,
0
],
[
0,
0,
0,
2
]
],
"l": [
2,
2,
0,
2
]
},
{
"k": 4,
"x0": [
0,
0,
0,
0,
2
],
"W": [
[
1,
0,
0,
0,
2
],
[
0,
1,
0,
0,
2
],
[
0,
0,
1,
0,
2
],
[
0,
0,
0,
1,
2
]
],
"Q": [
[
1,
2,
1,
2
],
[
0,
1,
1,
2
],
[
0,
0,
1,
1
],
[
0,
0,
0,
1
]
],
"l": [
0,
0,
1,
0
]
},
{
"k": 3,
"x0": [
0,
1,
0,
0,
1
],
"W": [
[
1,
0,
0,
0,
2
],
[
0,
0,
1,
0,
2
],
[
0,
0,
0,
1,
2
]
],
"Q": [
[
1,
0,
2
],
[
0,
0,
0
],
[
0,
0,
1
]
],
"l": [
2,
0,
2
]
}
],
"coeffs": [
"sqrt(3)/9 + 2*sqrt(3)*exp(2*I*pi/3)/9",
"exp(2*I*pi/3)/3",
"1/3 + exp(2*I*pi/3)/3",
"-sqrt(3)/9 - 2*sqrt(3)*exp(2*I*pi/3)/9",
"1/3",
"exp(2*I*pi/3)/3",
"sqrt(3)*exp(2*I*pi/9)/9 + 2*sqrt(3)*exp(8*I*pi/9)/9",
"-2*sqrt(3)*exp(2*I*pi/9)/9 - sqrt(3)*exp(8*I*pi/9)/9",
"-sqrt(3)*exp(2*I*pi/9)/9 + sqrt(3)*exp(8*I*pi/9)/9",
"-sqrt(3)*exp(8*I*pi/9)/9 + sqrt(3)*exp(2*I*pi/9)/9",
"-sqrt(3)*exp(8*I*pi/9)/9 + sqrt(3)*exp(2*I*pi/9)/9",
"exp(2*I*pi/9)/3",
"-2*sqrt(3)*exp(4*I*pi/9)/9 - sqrt(3)*exp(-8*I*pi/9)/9",
"sqrt(3)*exp(-8*I*pi/9)/9 + 2*sqrt(3)*exp(4*I*pi/9)/9",
"sqrt(3)*exp(-8*I*pi/9)/9 + 2*sqrt(3)*exp(4*I*pi/9)/9",
"sqrt(3)*exp(-8*I*pi/9)/9 + 2*sqrt(3)*exp(4*I*pi/9)/9",
"-sqrt(3)*exp(4*I*pi/9)/9 - 2*sqrt(3)*exp(-8*I*pi/9)/9",
"-exp(4*I*pi/9)/3"
]
},
"provenance": {
"author": "this repository",
"reference": "stabrank sector-state search",
"method": "Z^5 sector (qutrit cat-state) decomposition: each of the three sector projections of |T3>^5 is a 4-qutrit carry state, annealed to rank 6 on its code space and lifted; exact coefficients over Q(w9)",
"date": "2026-09-17",
"github": [
"vprusso"
],
"compute": {
"cpu_hours": 0.6,
"wall_clock_hours": 0.5,
"runs": 8,
"hardware": "Apple silicon laptop under heavy load from other jobs, 8 annealing chains per run",
"llm": [
{
"model": "claude-fable-5-1",
"role": "designed the sector decomposition and drove the search"
}
]
}
},
"notes": "First entry for this cell; gamma = log_3(18)/5 = 0.526 is above the published 1/2, so it fills the cell rather than moving the exponent. The construction is the qutrit analogue of the Qassim-Pashayan-Gosset cat state: since Z t_a = t_{a+3}, the three Galois-conjugate cat states c_j = sum_i w3^{ij} t_{1+3i}^{ot 5} are the Z^{ot 5} eigensector projections of |T3>^5, each living in a 3^4-dimensional stabilizer code, and |T3>^5 = sum_j c_j / 3. Each sector's rank is the stabilizer rank of a 4-qutrit carry state; the annealer found rank 6 for each (from a rank-8 start, pruned) and rank 5 failed in five runs with residuals between 0.455 and 0.494, which is not a clean plateau. Rank 5 in every sector would give chi(|T3>^5) <= 15 and exponent 0.493, the first value below 1/2 for this orbit, and would propagate by the contraction c_j (x) c_k -> c_{j+k} to exponent 0.491 at m = 8; a rank-4 exclusion inside the 81-dimensional code is the natural companion. At m = 3 and m = 4 the sector states have rank exactly 3 (exhaustive), reproducing 9 and 9 against the board's 8 and 9, so the route gains nothing there. Now at the lean tier: t3_m5_stabRankP_le_eighteen in LeanProofs.T3M5StabRank proves stabRankP 3 |T3>^5 <= 18 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)."
}