fix(ci): repair + wire status-gate; require coq-build-gate (#301)

Three gate-integrity fixes surfaced by the 2026-06-16 ground-truth sweep
(companion to the proof-status doc PR #300).

## Changes
1. **`scripts/status-gate.sh:3`** — `//` C-style comment → `#`. The
script was a **bash syntax error** and aborted immediately
(delimiter-only fix; owner string unchanged).
2. **`.github/workflows/status-gate.yml`** (new) — runs `status-gate.sh`
on PRs touching `formal/**`, `PROOF-NEEDS.md`, `TEST-NEEDS.md`, or the
script. The gate **never ran in CI before** (only `just status-gate`),
which is why a live count drift went unnoticed. Non-required for now.
3. **`.github/settings.yml`** — adds the always-on `coq-build-gate`
aggregator (PR #254) to `required_status_checks`, so **a broken proof /
new `Admitted` cannot merge to `main` undetected.**

## ⚠ Two things to decide
- **Branch-protection change (owner-only).** Item 3 edits
`required_status_checks`. Please confirm before merge — that's the
intentional completion of PR #254 (the aggregator was built to be
required-safe), but it's your call.
- **Merge order — #300 first.** The new `status-gate` check is
**currently RED on purpose**: it correctly detects the live `main`-wide
count drift (marker says `4`, `coqc`/grep say `5`). PR #300 corrects the
marker to `5`; once that merges, this check goes green. So: **merge
#300, then this.**
- **Unverified:** I did **not** run `cargo test --all-targets --
--list`, so I can't confirm `TEST-NEEDS.md`'s `467` test-count marker is
current. If it has also drifted, the `status-gate` check will stay red
on the *test-count* assertion until that marker is refreshed.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.github/settings.yml

@@ -115,6 +115,10 @@ branches:
         contexts:
           - "hypatia-scan"
           - "codeql"
+          # Added 2026-06-16: make the always-on Coq aggregator (PR #254) a
+          # required check so a broken proof / new Admitted cannot merge to
+          # main undetected. Owner: confirm this branch-protection change.
+          - "coq-build-gate"
       enforce_admins: true
       required_signatures: true
       restrictions: null

.github/workflows/status-gate.yml

@@ -0,0 +1,44 @@
+# SPDX-License-Identifier: MPL-2.0
+# Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+# Status Gate — fail a PR when the PROOF-NEEDS.md / TEST-NEEDS.md count
+# markers drift from coqc/cargo ground truth. This wires the previously
+# broken (`//` syntax error on line 3) + unwired scripts/status-gate.sh
+# into CI so admit-count / test-count drift is caught automatically.
+# NOTE: not yet a required status check — see .github/settings.yml.
+name: Status Gate
+
+on:
+  pull_request:
+    paths:
+      - 'formal/**'
+      - 'PROOF-NEEDS.md'
+      - 'TEST-NEEDS.md'
+      - 'scripts/status-gate.sh'
+      - 'Cargo.toml'
+      - 'Cargo.lock'
+      - '**/Cargo.toml'
+      - '.github/workflows/status-gate.yml'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: status-gate-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  status-gate:
+    name: status-gate
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+      - name: Install Rust toolchain
+        uses: dtolnay/rust-toolchain@3c5f7ea28cd621ae0bf5283f0e981fb97b8a7af9 # stable
+      - name: Cache cargo
+        uses: Swatinem/rust-cache@c19371144df3bb44fab255c43d04cbc2ab54d1c4 # v2
+      - name: Run status-gate (proof + test count drift)
+        env:
+          CARGO_INCREMENTAL: "0"
+        run: ./scripts/status-gate.sh

scripts/status-gate.sh

@@ -1,6 +1,6 @@
 #!/usr/bin/env bash
 # SPDX-License-Identifier: MPL-2.0
-// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+# Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 set -euo pipefail
 
 ROOT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"