ci(coq-build): expand Print Assumptions to all four Phase D theorems

[hyperpolymath]

Summary

• Expands the `coq-build.yml` Print Assumptions audit from 1 theorem to 4 — surfaces `Admitted` / `Axiom` slippage on EVERY Phase D top-level result, not just `preservation_l2_via_l1`.
• Single `coqtop` session amortises ML startup across four prints.
• Tail bumped from 40 to 160 lines to fit four print blocks (~40 lines each).

What changes

The Print Assumptions step now invokes all four Phase D top-level results:

Theorem	File	Landed in
`preservation_l1`	`Semantics_L1.v`	(pre-Phase D — Theorem)
`preservation_l2_via_l1`	`TypingL2.v`	(L2-hybrid landing)
`preservation_l2_app_eff_beta_linear`	`TypingL2.v`	#228
`preservation_l2_app_eff_beta_ground_nonlinear`	`TypingL2.v`	#233

Why this matters

`coq-build.yml` shipped in #231 (closed #227) covered only `preservation_l2_via_l1`. The original acceptance criteria called for the four-theorem set so that every Phase D result the build oracle backs is audited per-PR. Without this, a new `Admitted.` in a β-case lemma would slip through with green CI as long as `preservation_l2_via_l1`'s assumption set didn't change.

Relationship to other in-flight work

• ci(coq-build): run coqorg/coq container as root to fix actions/checkout EACCES #236 (queued, auto-merge SQUASH armed): adds `container.options: --user root` to fix EACCES on `actions/checkout`. Touches a different section of `coq-build.yml` than this PR — no expected conflict either way. Once ci(coq-build): run coqorg/coq container as root to fix actions/checkout EACCES #236 lands, the workflow becomes actually-runnable; once this lands, the runnable workflow audits four theorems instead of one.
• Ruleset gap (owner action): the `Base` ruleset has `deletion`, `non_fast_forward`, `required_signatures`, `pull_request` rules but no `required_status_checks` rule. Even with this PR + ci(coq-build): run coqorg/coq container as root to fix actions/checkout EACCES #236 merged, `Coq build — formal/_CoqProject` remains informational. The standing rule `[[feedback_proof_pr_build_oracle_is_only_truth]]` remains load-bearing until the ruleset adds the check as required.

Test plan

• CI: `Coq build — formal/_CoqProject` reaches the Print Assumptions step (gated on ci(coq-build): run coqorg/coq container as root to fix actions/checkout EACCES #236 landing first to fix EACCES, then the four-theorem step runs)
• Run log shows four `Print Assumptions .` outputs in sequence (one consolidated coqtop transcript)
• No build regression — `coq_makefile` step still passes (no Coq source changed)

Refs

• Closes the per-theorem coverage gap from ci: add Coq build oracle to workflows — admin-merge can land broken main today #227's original acceptance criteria
• Stacks complementarily on ci(coq-build): run coqorg/coq container as root to fix actions/checkout EACCES #236 (different file region)
• Standing rule [[feedback_proof_pr_build_oracle_is_only_truth]] still applies

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 75 issues detected

Severity	Count
🔴 Critical	11
🟠 High	16
🟡 Medium	48

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in abi-verify.yml",
    "type": "missing_timeout_minutes",
    "file": "abi-verify.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "missing_timeout_minutes",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_timeout_minutes",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in coq-build.yml",
    "type": "missing_timeout_minutes",
    "file": "coq-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in governance.yml",
    "type": "missing_timeout_minutes",
    "file": "governance.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in hypatia-scan.yml",
    "type": "missing_timeout_minutes",
    "file": "hypatia-scan.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in instant-sync.yml",
    "type": "missing_timeout_minutes",
    "file": "instant-sync.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in mirror.yml",
    "type": "missing_timeout_minutes",
    "file": "mirror.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in rust-ci.yml",
    "type": "missing_timeout_minutes",
    "file": "rust-ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence