χR(∣T5⟩⊗4) ≥ 6

Tâ‚… orbit, ququint.

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

attested · 2/74 re-run   certificate script asserted: CERTIFIED chi(T5^4) >= 6; re-ran 2 of 74 stored batches from scratch chosen from seed 20261001 and only checked the SHA-256 of the other 72 against research/t5q_m2_rank5/batch_manifest.json; the full enumeration (13.4 CPU-h 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 (the rank-5 census of |T5>^2, research/t5q_m2_rank5 at commit 2b751cb)) was not re-run

Compute

0 runs; 0 CPU-hours; 0 h wall-clock; on none beyond the m=3 certificate, which this cell re-runs.

Notes

χ(ψ ⊗ φ) ≥ χ(ψ) when φ has a nonzero computational amplitude, applied 1 time to χ(T5^3) ≥ 6 (Lean: stabRankP_powVecP_mono in lean_proofs/LeanProofs/Stabilizer/SliceP.lean); every amplitude of |T5⟩ is nonzero. The certificate is the m=3 attested one (bounds/T5-m3-lower-6.json), which prints this line after certifying χ(T5^3) ≥ 6; the cell inherits the attested tier. Puts the cell at 6 ≤ χ(T5^4) ≤ 25 (bounds/T5-m4-upper-25.json), replacing the lower bound of 5 projected from the m=2 cell. Whether χ(T5^4) < 25 is open.

Attribution

this repository · stabrank research/t5_m3_lift · projection monotonicity applied to the attested slice-and-lift exclusion of rank 5 at m=3

Submission

JSON
{
  "schema_version": "0.1",
  "orbit": "T5",
  "m": 4,
  "direction": "lower",
  "rank": 6,
  "certificate": {
    "script": "verify_challenge/cert_t5_m3_lift_attested.py",
    "expect": "CERTIFIED chi(T5^4) >= 6",
    "budget_s": 3600,
    "attested": {
      "batches": "research/t5q_m2_rank5/batch_manifest.json",
      "recomputed": 2,
      "compute_hours": 13.4,
      "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 (the rank-5 census of |T5>^2, research/t5q_m2_rank5 at commit 2b751cb)",
      "note": "The listing of every 5-set of two-ququint stabilizer states whose span contains |T5>^2, one per orbit of the unitary symmetry group, lives in the stored batch outputs under research/t5q_m2_rank5/results/ (74 batches, 155,422 pivot-partner units, every unit run, 0 undecided, one hit: the five Z(x)Z eigensectors, a set fixed by the group). The enumeration was not re-run under the budget. The certificate re-enumerates the plan, re-runs the exact k = 1..4 censuses, verifies the hashes and geometry of every output, re-decides the stored hit, fails on any undecided unit, re-runs two batches from scratch (seed 20261001: batches 12 and 47), and then runs the exact lift decision of research/t5_m3_lift/lift.py on the listed set. Completeness rests on the stored outputs and on research/t5q_m2_rank5/batch.py, which regenerates any batch (batch.py K), under the modular assumption every kernel census of the project makes: a member whose image is nonzero over Q(zeta_5) is nonzero modulo 65521. An independent re-run of all 74 batches on 2026-10-02 (research/t5_m3_lift/results/pod/census/) reproduced every deterministic hash; it is recorded in provenance.compute and does not change the tier."
    }
  },
  "provenance": {
    "author": "this repository",
    "reference": "stabrank research/t5_m3_lift",
    "method": "projection monotonicity applied to the attested slice-and-lift exclusion of rank 5 at m=3",
    "date": "2026-10-02",
    "github": [
      "vprusso"
    ],
    "compute": {
      "cpu_hours": 0.0,
      "wall_clock_hours": 0.0,
      "runs": 0,
      "hardware": "none beyond the m=3 certificate, which this cell re-runs"
    }
  },
  "notes": "chi(psi (x) phi) >= chi(psi) when phi has a nonzero computational amplitude, applied 1 time to chi(T5^3) >= 6 (Lean: stabRankP_powVecP_mono in lean_proofs/LeanProofs/Stabilizer/SliceP.lean); every amplitude of |T5> is nonzero. The certificate is the m=3 attested one (bounds/T5-m3-lower-6.json), which prints this line after certifying chi(T5^3) >= 6; the cell inherits the attested tier. Puts the cell at 6 <= chi(T5^4) <= 25 (bounds/T5-m4-upper-25.json), replacing the lower bound of 5 projected from the m=2 cell. Whether chi(T5^4) < 25 is open."
}