Summary

`coq-build.yml` shipped via #231 (closed #227). EACCES container fix is in flight via #236. Print Assumptions audit expanded to all four Phase D theorems via #243.

Remaining gap: the `Base` branch ruleset on `main` does not include the new Coq build check as a required status check. Until it does, the workflow is informational — `admin-merge` can still land a broken main even after #236 + #243 are in.

Verification

```bash
gh api repos/hyperpolymath/ephapax/rulesets/14285235 --jq '.rules[].type'
```

Returns:
```
deletion
non_fast_forward
required_signatures
pull_request
```

No `required_status_checks` rule. The Coq build runs (or will, post-#236) but its result is not enforced.

Acceptance

• Add `required_status_checks` rule to the `Base` ruleset on `main` listing the context `Coq build — formal/_CoqProject` (and the GitHub Actions integration ID).
• Verify by attempting to admin-merge a no-op PR while the check is red — should be blocked.

Suggested API shape

```bash

First confirm the Actions integration ID for this repo:

gh api repos/hyperpolymath/ephapax/installation --jq '.app_id'

Then PATCH the ruleset to append the required_status_checks rule.

See:

https://docs.github.com/en/rest/repos/rules#update-a-repository-ruleset

```

Why this matters

The standing rule [[feedback_proof_pr_build_oracle_is_only_truth]] is the only safety net while the gate is informational. Marking the check REQUIRED moves enforcement from human discipline to GitHub's merge guard — the original motivation behind #227.

Refs

• ci: add Coq build oracle to workflows — admin-merge can land broken main today #227 — original tracker (CLOSED via ci: add Coq build oracle workflow (closes #227) #231)
• ci: add Coq build oracle workflow (closes #227) #231 — `coq-build.yml` ships
• ci(coq-build): run coqorg/coq container as root to fix actions/checkout EACCES #236 — EACCES fix (queued, auto-merge armed)
• ci(coq-build): expand Print Assumptions to all four Phase D theorems #243 — Print Assumptions expansion to 4 Phase D theorems (auto-merge armed)

🤖 Generated with Claude Code