Submit a record

There is no site submission form for this challenge: a record is a pull request to the compiler repository. The correctness theorem is the referee — if your fork builds, the axiom audit is clean, and the frozen spec still elaborates, your rewrite is correct by construction.

1. Fork the repo and branch from arena (the current record) or from any record-NNN tag — building on older records is allowed and encouraged.
2. Optimize. Iterate locally with scripts/opt_harness.sh full against the public corpus, and keep the proof gate green with scripts/opt_harness.sh check.
3. Open a PR targeting arena, stating which record you branched from (Based-on: record-NNN); CI verifies it by git ancestry.
4. When public CI is green and your public-corpus improvement is plausible, a maintainer labels the PR for private scoring: a sandboxed, offline runner re-verifies everything independently and reports one number — total gas.
5. Beat the current record by ≥ 0.1% → your PR is merged, tagged, and you enter the leaderboard permanently.