[SamuelSchlesinger]

program_certificate could silently register an unrelated predicate using its final argument, leaving an inert entry. Reject unsupported predicates with an actionable error, and document all seven existing forms: TM plain/tidy polynomial time, parameterized/encoded PPT, and the three word-RAM predicates consumed by Tactic.WordRAM. Their existing selection/registration behavior is preserved; the plain driver fix from merged #676/#728 is unchanged.

The new ordinary-import regression checks that the actual SignatureScheme.verify_polyTime and MACScheme.verify_polyTime entries are keyed by their verify projections, exercises polytime on both, and imports the existing irreducible eager-contract fixture from another module (fun_prop must fail before named polytime succeeds). Wrong-predicate and zero-argument annotations now have checked diagnostics. Existing WordRAMController/PT/PPT tests protect all documented forms.

Validation at 311de10232eacb6c82115adca483ff2318c9c263 (base main c1762c51): all six LEAN_NUM_THREADS=4 scripts/check.sh gates pass, plus focused diagnostics/driver/WordRAM tests, hygiene with simp checks, catalogue (14 abstracts/19 headlines), and diff checks. No mathematical or abstract claim changes. Local log: /tmp/codex-756-six-gates-final.log.

D1 integration evidence is deliberately separate: exact approved #676 ac297bf0 passes actual Signature/MAC key checks and an off-tree named-only production-consumer probe, excluding default/builtin/compositional rules. S1 remains a separate, explicitly limited integration check. Its old snapshot intentionally has no MAC source; both actual projections will be retested after the planned single rebase onto swept main, without foreign objects or feature imports. The present Signature/opaque/native paths are checked only after their compatibility closure is repaired. No whole-joint or full-inventory success is claimed by this PR.

Framework friction: existing certificate infrastructure suffices; no new runtime registry, derivation layer, predicate schema, alias or unfolding workaround is introduced.

AI-assisted implementation by worker review_559 under coordinator-codex-01a16ab8. Closes #756; addresses #750 D1 diagnostics without closing its broader integration gate. Independent external final review requested; no author approval.

[SamuelSchlesinger]

Independent coordinator verdict — coordinator-reviewer-codex-20261023 (not Samuel): APPROVED at exact head 311de10232eacb6c82115adca483ff2318c9c263.

The guard admits exactly the seven previously supported predicates and runs before argument extraction/registration. Removing it leaves the prior key-selection logic unchanged. Ordinary-import regressions check the actual Signature/MAC verify keys and named-driver use; the imported irreducible fixture still requires polytime after fun_prop fails. Wrong predicates and zero-argument annotations now produce checked diagnostics. This verdict covers the diagnostic/imported-test change; it does not establish the separately disclosed S1 integration gate. No mathematical or abstract claim changed.

Exact-head PR run 40070240719 is SUCCESS across all six Lean gates. Scoped independent source review is complete; no new local library build is claimed. Ready to enqueue at this exact head under the coordinator’s integration order.