ci: add Coq build oracle to workflows — admin-merge can land broken main today #227

Surfaced from

Hotfix PR #226 (2026-05-30 13:57Z). PR #224 admin-merged a duplicate Lemma 7min after PR #223 because the GitHub CI workflows do NOT run `coqc` / `just -f formal/Justfile all`. Resulting compilation error on main:

```
File "./Semantics_L1.v", line 1361, characters 6-32:
Error: tfuneff_lambda_retype_l1_m already exists.
```

All 17 governance / security / scanner checks were green. The duplicate ONLY surfaces when the Coq build runs.

Scope of the gap

Verified by scanning `.github/workflows/*.yml` checks visible in PR #224's `statusCheckRollup`:

• governance / hypatia / scanners / CodeQL all run.
• ZERO check loads OCaml + Coq + builds `formal/`.

Implication: ANY PR that breaks compilation (duplicate Lemma, missing dependency, syntax error, broken proof, new `Admitted.` without policy gate, etc.) merges green on auto-merge. The standing directive "For proof PRs the toolchain build is the ONLY merge oracle" relies entirely on human discipline.

Acceptance

• Add a workflow job that loads OCaml + Coq (Rocq 9.1.1 / Coq 8.18 matches `formal/Justfile`) and runs `just -f formal/Justfile all`.
• Job is REQUIRED (blocks merge — not informational).
• Print `Print Assumptions preservation_l2_via_l1.` (and key Phase D lemmas) to surface any new `Admitted` / `Axiom` slippage.

Phase mapping

Independent of Phase D work. Belongs to infra-hardening (the [[feedback_proof_pr_build_oracle_is_only_truth]] standing rule's automation counterpart).

Refs

• PR feat(L1): Phase D slice 4 Phase 3a — tfuneff_lambda_retype_l1_m #223 (Phase 3a v1) — merged 13:21Z, green.
• PR feat(L1): Phase D slice 4 Phase 3a — tfuneff_lambda_retype_l1_m + is_tfuneff_ty #224 (Phase 3a v2 + `is_tfuneff_ty`) — merged 13:27Z, green, BROKE main.
• PR fix(L1): HOTFIX — dedupe tfuneff_lambda_retype_l1_m (main is broken) #226 (hotfix) — armed 13:57Z, restores compilation.

🤖 Filed 2026-05-30 from hotfix meander.