χR(∣S⟩⊗2) ≤ 2

Strange 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   strange_m2_stabRank_le_two in LeanProofs.Stabilizer.IsStab, machine-checked by Lean

Implied per-copy exponent γ ≤ 0.3155 against a published 0.3155, no improvement.

Lean proof

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

Notes

Two full-support terms; the smallest known exponent across the four qutrit orbits. The Lean theorem is now a statement about stabRank itself: strange_m2_stabRank_le_two proves Stabilizer.stabRank IsStab |S⟩⊗2 ≤ 2 against a concrete stabilizer predicate (a nonzero multiple of a sum over an injectively parametrised flat with a quadratic-plus-linear phase mod 3), rather than a pointwise identity between hand-written vectors whose stabilizer-ness Lean never checked. The pointwise identity strange_m2_vector_decomposition in StrangeM2Pointwise is what it builds on.

Attribution

Labib and Russo · arXiv:2605.28586, Theorem 2 · carry decomposition

Submission

JSON
{
  "schema_version": "0.1",
  "orbit": "S",
  "m": 2,
  "direction": "upper",
  "rank": 2,
  "witness": {
    "terms": [
      {
        "k": 2,
        "x0": [
          0,
          0
        ],
        "W": [
          [
            1,
            0
          ],
          [
            0,
            1
          ]
        ],
        "Q": [
          [
            1,
            1
          ],
          [
            0,
            1
          ]
        ],
        "l": [
          0,
          0
        ]
      },
      {
        "k": 2,
        "x0": [
          0,
          0
        ],
        "W": [
          [
            1,
            0
          ],
          [
            0,
            1
          ]
        ],
        "Q": [
          [
            1,
            2
          ],
          [
            0,
            1
          ]
        ],
        "l": [
          0,
          0
        ]
      }
    ],
    "coeffs": [
      "3/4 + sqrt(3)*I/4",
      "-3/4 - sqrt(3)*I/4"
    ]
  },
  "provenance": {
    "author": "Labib and Russo",
    "reference": "arXiv:2605.28586, Theorem 2",
    "method": "carry decomposition",
    "date": "2026-05-27",
    "github": [
      "FarLab",
      "vprusso"
    ]
  },
  "notes": "Two full-support terms; the smallest known exponent across the four qutrit orbits. The Lean theorem is now a statement about stabRank itself: strange_m2_stabRank_le_two proves Stabilizer.stabRank IsStab |S>^2 <= 2 against a concrete stabilizer predicate (a nonzero multiple of a sum over an injectively parametrised flat with a quadratic-plus-linear phase mod 3), rather than a pointwise identity between hand-written vectors whose stabilizer-ness Lean never checked. The pointwise identity strange_m2_vector_decomposition in StrangeM2Pointwise is what it builds on.",
  "lean": {
    "module": "LeanProofs.Stabilizer.IsStab",
    "theorem": "strange_m2_stabRank_le_two"
  }
}