χR(∣T3⟩⊗1) ≥ 3

T₃ orbit, qutrit.

Participate

Run it yourself, or point a coding agent at it.

git clone https://github.com/unitaryfoundation/stabrank
cd stabrank
# describe your decomposition in bounds/mybound.json
make fit BOUND=bounds/mybound.json ARGS=--write
make verify BOUND=bounds/mybound.json

fit solves for the exact coefficients, or tells you no exact combination of your terms reproduces the target. verify rebuilds the identity in exact arithmetic. If it passes, open a pull request adding the file and the leaderboard picks it up on the next build.

A bound the pipeline cannot check is recorded as cited and never takes a record.

← back to the board

Verification

lean   t3_m1_stabRank_gt_two in LeanProofs.T3M1StabRank, machine-checked by Lean

Lean proof

This bound is backed by a machine-checked theorem: t3_m1_stabRank_gt_two in LeanProofs.T3M1StabRank. The recorded lake build confirms it compiles.

Notes

Settles χ(|T3⟩) = 3 with the rank-3 upper bound. On one qutrit there are only 12 stabilizer states, so the rank-2 question is 66 pairs and is decided by exhaustion rather than by the Galois argument, which reaches the same bound at every m but is not yet formalized. The exclusion is numerical and rests on a margin: the closest any two candidate directions come to parallel is 0.956 against a threshold of 1 - 1e-6, so no rounding at the 1e-15 level of these inputs can close the gap. The Strange state at m=1 has a known rank-2 decomposition, which the same code finds as a positive control. Now also proved in Lean, and against stabRank itself: t3_m1_stabRank_gt_two shows Stabilizer.stabRank IsStab |T3⟩ > 2 by the Galois argument. T3Galois gives the dimension count (the three conjugates t1, t4, t7 are independent, a Vandermonde), T3GaloisDescent discharges its hypothesis (the span of vectors over Z[ω3] containing t1 contains every conjugate: descend coefficients to Q(ω9), then apply the embedding ω9 → ω9^e for e in {1, 4, 7}, which fixes Z[ω3]), and every IsStab vector is a multiple of a vector over Z[ω3]. The pair exhaustion above remains as the reproduced-tier certificate; the Lean theorem is what the cell now holds.

Attribution

this repository · stabrank PR #19 · exhaustion over all 66 pairs of 1-qutrit stabilizer states

Submission

JSON
{
  "schema_version": "0.1",
  "orbit": "T3",
  "m": 1,
  "direction": "lower",
  "rank": 3,
  "certificate": {
    "script": "verify_challenge/cert_t3m1_rank2.py",
    "expect": "CERTIFIED chi(T3^1) >= 3"
  },
  "provenance": {
    "author": "this repository",
    "reference": "stabrank PR #19",
    "method": "exhaustion over all 66 pairs of 1-qutrit stabilizer states",
    "date": "2026-09-16",
    "github": [
      "vprusso"
    ]
  },
  "notes": "Settles chi(|T3>) = 3 with the rank-3 upper bound. On one qutrit there are only 12 stabilizer states, so the rank-2 question is 66 pairs and is decided by exhaustion rather than by the Galois argument, which reaches the same bound at every m but is not yet formalized. The exclusion is numerical and rests on a margin: the closest any two candidate directions come to parallel is 0.956 against a threshold of 1 - 1e-6, so no rounding at the 1e-15 level of these inputs can close the gap. The Strange state at m=1 has a known rank-2 decomposition, which the same code finds as a positive control. Now also proved in Lean, and against stabRank itself: t3_m1_stabRank_gt_two shows Stabilizer.stabRank IsStab |T3> > 2 by the Galois argument. T3Galois gives the dimension count (the three conjugates t_1, t_4, t_7 are independent, a Vandermonde), T3GaloisDescent discharges its hypothesis (the span of vectors over Z[w3] containing t_1 contains every conjugate: descend coefficients to Q(w9), then apply the embedding w9 -> w9^e for e in {1, 4, 7}, which fixes Z[w3]), and every IsStab vector is a multiple of a vector over Z[w3]. The pair exhaustion above remains as the reproduced-tier certificate; the Lean theorem is what the cell now holds.",
  "lean": {
    "module": "LeanProofs.T3M1StabRank",
    "theorem": "t3_m1_stabRank_gt_two"
  }
}