lean t5_m1_stabRankP_le_three in LeanProofs.T5M1StabRank, machine-checked by Lean
Implied per-copy exponent γ ≤ 0.6826 against a baseline 0.6826 (single-copy product bound; no published exponent), no improvement.
This bound is backed by a machine-checked theorem: t5_m1_stabRankP_le_three in LeanProofs.T5M1StabRank. The recorded lake build confirms it compiles.
1 run; 0.001 CPU-hours; 0.001 h wall-clock; on Apple silicon laptop, one core.
|T5⟩ = 5^(-1/2) sum_x w5^(x^3) |x⟩ is a combination of |0⟩, |1⟩ and the full-support state 5^(-1/2) sum_y w5^(4y^2 + 4y) |y⟩, with the coefficients above recovered exactly by fit_coeffs.fit from the normal equations and the identity checked symbolically by the verifier. The pivot search lists ten rank-3 decompositions over the 30 single-ququint states in all. With the exact rank-2 exclusion of cert_t5_m1_rank2.py this settles χ(|T5⟩) = 3, which is below the local dimension, unlike T3 where χ(|T3⟩) = 3 = p. The implied γ log_5(3) = 0.6826 is the single-copy product bound; no exponent has been published for any p = 5 state, so it is the baseline the orbit is measured against.
this repository · stabrank docs/notes/new_orbits_design.md · pivot search over the 30 single-ququint stabilizer states, then exact refit with fit_coeffs.fit
{
"schema_version": "0.1",
"orbit": "T5",
"m": 1,
"direction": "upper",
"rank": 3,
"witness": {
"terms": [
{
"k": 0,
"x0": [
0
],
"W": [],
"Q": [],
"l": []
},
{
"k": 0,
"x0": [
1
],
"W": [],
"Q": [],
"l": []
},
{
"k": 1,
"x0": [
0
],
"W": [
[
1
]
],
"Q": [
[
4
]
],
"l": [
4
]
}
],
"coeffs": [
"-1/4 + sqrt(5)/4 + I*sqrt(sqrt(5)/40 + 1/8)",
"1/2 + I*sqrt(1/4 - sqrt(5)/10)",
"-1/4 + sqrt(5)/4 - I*sqrt(sqrt(5)/8 + 5/8)"
]
},
"provenance": {
"author": "this repository",
"reference": "stabrank docs/notes/new_orbits_design.md",
"method": "pivot search over the 30 single-ququint stabilizer states, then exact refit with fit_coeffs.fit",
"date": "2026-09-20",
"github": [
"vprusso"
],
"compute": {
"cpu_hours": 0.001,
"wall_clock_hours": 0.001,
"runs": 1,
"hardware": "Apple silicon laptop, one core"
}
},
"notes": "|T5> = 5^(-1/2) sum_x w5^(x^3) |x> is a combination of |0>, |1> and the full-support state 5^(-1/2) sum_y w5^(4y^2 + 4y) |y>, with the coefficients above recovered exactly by fit_coeffs.fit from the normal equations and the identity checked symbolically by the verifier. The pivot search lists ten rank-3 decompositions over the 30 single-ququint states in all. With the exact rank-2 exclusion of cert_t5_m1_rank2.py this settles chi(|T5>) = 3, which is below the local dimension, unlike T3 where chi(|T3>) = 3 = p. The implied gamma log_5(3) = 0.6826 is the single-copy product bound; no exponent has been published for any p = 5 state, so it is the baseline the orbit is measured against.",
"lean": {
"module": "LeanProofs.T5M1StabRank",
"theorem": "t5_m1_stabRankP_le_three"
}
}