χR(∣qubit_T⟩⊗2) ≤ 2

BK T-type orbit, qubit.

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   qubit_t_m2_stabRankP_le_two in LeanProofs.QubitTStabRank, machine-checked by Lean

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

Lean proof

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

Compute

1 run; 0.01 CPU-hours; 0.01 h wall-clock; on Apple silicon laptop, 8 annealing chains.

Notes

Found here by the package's annealer (search_decomposition.py, target qubit_ttype, seed 1, one run of 8 chains) and verified in exact arithmetic with coefficients recovered by fit_coeffs. The phases need the fourth roots of unity, which the witness format now carries for qubits. Rank 1 is impossible since the amplitudes of |T⟩⊗2 do not share a modulus, so this settles χ(|T⟩⊗2) = 2.

Attribution

this repository · stabrank annealer · simulated annealing over stabilizer states, then exact refit

Submission

JSON
{
  "schema_version": "0.1",
  "orbit": "qubit_T",
  "m": 2,
  "direction": "upper",
  "rank": 2,
  "witness": {
    "terms": [
      {
        "k": 1,
        "x0": [
          0,
          0
        ],
        "W": [
          [
            1,
            1
          ]
        ],
        "Q": [
          [
            0
          ]
        ],
        "l": [
          1
        ]
      },
      {
        "k": 2,
        "x0": [
          0,
          0
        ],
        "W": [
          [
            1,
            0
          ],
          [
            0,
            1
          ]
        ],
        "Q": [
          [
            0,
            1
          ],
          [
            0,
            0
          ]
        ],
        "l": [
          0,
          0
        ]
      }
    ],
    "coeffs": [
      "sqrt(2)/2 - sqrt(6)*I/6",
      "sqrt(3)/3 + sqrt(3)*I/3"
    ]
  },
  "provenance": {
    "author": "this repository",
    "reference": "stabrank annealer",
    "method": "simulated annealing over stabilizer states, then exact refit",
    "date": "2026-09-16",
    "github": [
      "vprusso"
    ],
    "compute": {
      "cpu_hours": 0.01,
      "wall_clock_hours": 0.01,
      "runs": 1,
      "hardware": "Apple silicon laptop, 8 annealing chains"
    }
  },
  "notes": "Found here by the package's annealer (search_decomposition.py, target qubit_ttype, seed 1, one run of 8 chains) and verified in exact arithmetic with coefficients recovered by fit_coeffs. The phases need the fourth roots of unity, which the witness format now carries for qubits. Rank 1 is impossible since the amplitudes of |T>^2 do not share a modulus, so this settles chi(|T>^2) = 2.",
  "lean": {
    "module": "LeanProofs.QubitTStabRank",
    "theorem": "qubit_t_m2_stabRankP_le_two"
  }
}