lean t5_m2_stabRankP_le_five in LeanProofs.T5M2StabRank, machine-checked by Lean
Implied per-copy exponent γ ≤ 0.5000 against a baseline 0.6826 (single-copy product bound; no published exponent), an improvement.
This bound is backed by a machine-checked theorem: t5_m2_stabRankP_le_five in LeanProofs.T5M2StabRank. The recorded lake build confirms it compiles.
74 runs; 13.4 CPU-hours; 1.06 h wall-clock; on RunPod CPU pod, 16 vCPU AMD EPYC 4564P on a shared host, fifteen batches in parallel at nice 19 (2026-09-24 12:32 to 13:36 UTC); about 0.3 laptop CPU-hours of controls before it.
|T5⟩⊗2 = 5^(-1) sum_{x,y} w^(x^3 + y^3) |x,y> with w = exp(2 π i/5). On the line x + y = c the cubic is quadratic in the line parameter, x^3 + (c - x)^3 = c^3 + 3c x^2 - 3c^2 x, so the projection of |T5⟩⊗2 onto the eigenspace Z(x)Z = w^c is w^(c^3)/√5 times the stabilizer state 5^(-1/2) sum_x w^(3c x^2 - 3c^2 x) |x, c - x>. The five terms are these five Z(x)Z eigensectors (x0 = (0, c), W = (1, 4), Q = 3c, l = -3c^2, coefficient w^(c^3)/√5): the Pauli eigensector construction of research/constructions/sectors.py with P = Z(x)Z, and the p = 5 analogue of the two-copy carry decomposition of |T3⟩. Found by the direct rank-5 census of research/t5q_m2_rank5 (docs/notes/t5q_m2_rank5_exclusion.md), which was built to exclude rank 5: the compiled 5-cover kernel over the 155,422 (pivot, partner) units of the 3,900 two-ququint stabilizer states returned exactly one 5-set, dictionary indices [525, 563, 591, 619, 637] (batch 31, unit (637, 525)), decided exactly modulo 2013265921 and numerically; the coefficients were fitted exactly by fit_coeffs.fit and the identity is checked symbolically by the verifier and by hand in Z[w] (an element vanishes iff its five coefficients on 1, w, ..., w^4 agree). The 5-set is fixed by the whole unitary symmetry group of |T5⟩⊗2 (order 50: the local Clifford stabilizer of |T5⟩ cycles the sectors, the swap fixes each) and by the antiunitary symmetry, so with ranks 2 to 4 excluded (bounds/T5-m2-lower-5.json) it is the only rank-5 decomposition of |T5⟩⊗2 over stabilizer states, and the cell is settled: χ(|T5⟩⊗2) = 5, strictly below the product 9 of χ(|T5⟩) = 3. Implied γ log_5(5)/2 = 0.5 against the single-copy baseline log_5(3) = 0.6826; no exponent is published for any p = 5 state. Lean: t5_m2_stabRankP_le_five in LeanProofs.T5M2StabRank.
this repository · stabrank docs/notes/t5q_m2_rank5_exclusion.md · direct census of the 5-sets of two-ququint stabilizer states whose span contains |T5⟩⊗2 (compiled 5-cover kernel, one set per orbit of the unitary symmetry group), then exact refit
{
"schema_version": "0.1",
"orbit": "T5",
"m": 2,
"direction": "upper",
"rank": 5,
"witness": {
"terms": [
{
"k": 1,
"x0": [
0,
0
],
"W": [
[
1,
4
]
],
"Q": [
[
0
]
],
"l": [
0
]
},
{
"k": 1,
"x0": [
0,
1
],
"W": [
[
1,
4
]
],
"Q": [
[
3
]
],
"l": [
2
]
},
{
"k": 1,
"x0": [
0,
2
],
"W": [
[
1,
4
]
],
"Q": [
[
1
]
],
"l": [
3
]
},
{
"k": 1,
"x0": [
0,
3
],
"W": [
[
1,
4
]
],
"Q": [
[
4
]
],
"l": [
3
]
},
{
"k": 1,
"x0": [
0,
4
],
"W": [
[
1,
4
]
],
"Q": [
[
2
]
],
"l": [
2
]
}
],
"coeffs": [
"1/sqrt(5)",
"exp(2*I*pi/5)/sqrt(5)",
"exp(6*I*pi/5)/sqrt(5)",
"exp(4*I*pi/5)/sqrt(5)",
"exp(8*I*pi/5)/sqrt(5)"
]
},
"provenance": {
"author": "this repository",
"reference": "stabrank docs/notes/t5q_m2_rank5_exclusion.md",
"method": "direct census of the 5-sets of two-ququint stabilizer states whose span contains |T5>^2 (compiled 5-cover kernel, one set per orbit of the unitary symmetry group), then exact refit",
"date": "2026-09-24",
"github": [
"vprusso"
],
"compute": {
"cpu_hours": 13.4,
"wall_clock_hours": 1.06,
"runs": 74,
"hardware": "RunPod CPU pod, 16 vCPU AMD EPYC 4564P on a shared host, fifteen batches in parallel at nice 19 (2026-09-24 12:32 to 13:36 UTC); about 0.3 laptop CPU-hours of controls before it"
}
},
"notes": "|T5>^2 = 5^(-1) sum_{x,y} w^(x^3 + y^3) |x,y> with w = exp(2 pi i/5). On the line x + y = c the cubic is quadratic in the line parameter, x^3 + (c - x)^3 = c^3 + 3c x^2 - 3c^2 x, so the projection of |T5>^2 onto the eigenspace Z(x)Z = w^c is w^(c^3)/sqrt(5) times the stabilizer state 5^(-1/2) sum_x w^(3c x^2 - 3c^2 x) |x, c - x>. The five terms are these five Z(x)Z eigensectors (x0 = (0, c), W = (1, 4), Q = 3c, l = -3c^2, coefficient w^(c^3)/sqrt(5)): the Pauli eigensector construction of research/constructions/sectors.py with P = Z(x)Z, and the p = 5 analogue of the two-copy carry decomposition of |T3>. Found by the direct rank-5 census of research/t5q_m2_rank5 (docs/notes/t5q_m2_rank5_exclusion.md), which was built to exclude rank 5: the compiled 5-cover kernel over the 155,422 (pivot, partner) units of the 3,900 two-ququint stabilizer states returned exactly one 5-set, dictionary indices [525, 563, 591, 619, 637] (batch 31, unit (637, 525)), decided exactly modulo 2013265921 and numerically; the coefficients were fitted exactly by fit_coeffs.fit and the identity is checked symbolically by the verifier and by hand in Z[w] (an element vanishes iff its five coefficients on 1, w, ..., w^4 agree). The 5-set is fixed by the whole unitary symmetry group of |T5>^2 (order 50: the local Clifford stabilizer of |T5> cycles the sectors, the swap fixes each) and by the antiunitary symmetry, so with ranks 2 to 4 excluded (bounds/T5-m2-lower-5.json) it is the only rank-5 decomposition of |T5>^2 over stabilizer states, and the cell is settled: chi(|T5>^2) = 5, strictly below the product 9 of chi(|T5>) = 3. Implied gamma log_5(5)/2 = 0.5 against the single-copy baseline log_5(3) = 0.6826; no exponent is published for any p = 5 state. Lean: t5_m2_stabRankP_le_five in LeanProofs.T5M2StabRank.",
"lean": {
"module": "LeanProofs.T5M2StabRank",
"theorem": "t5_m2_stabRankP_le_five"
}
}