fix(polytime): reject unsupported certificate predicates and guard imported verification keys #756

Focused D1 diagnostic/regression follow-up to #750. The existing plain key/consumer fix was approved in #676 ac297bf/#728 and has landed in main; it is not reimplemented here. Worker review_559 under coordinator-codex-01a16ab8, branch fix/program-certificate-diagnostic-750, isolated worktree codex-750-certificate-guard, refreshed onto verified main c1762c5.

Baseline at ac297: both actual SignatureScheme/MACScheme verification metadata keys and production named-only lookup pass across ordinary imports; no compositional/default/builtin path is used in the temporary named-only probe. But an unrelated NotEfficiency List.reverse theorem is silently accepted and stored, confirming missing diagnostic work.

Scope: reject predicates outside the seven existing documented forms (TM plain/tidy polynomial time, IsPPTOn, IsPPT, WordRAM.Refines, WordRAM.ComputableInPolyTime and WordRAM.UniformComputableInPolyTime); preserve their current indexing/consumer behavior and registry format. Document all supported forms, add ordinary-import actual projection key checks, reuse the existing external opaque negative-fun_prop/positive-polytime fixture, and check useful unsupported-predicate/zero-argument diagnostics. Existing WordRAMController/PT/PPT tests protect the documented forms. No aliases, derivation machinery, new runtime registry, schema broadening, unfolding workaround or Crypto model changes.

Latest frozen S1 consumer integration is a separate explicit verification gate coordinated with its owner; no joint D1 success before the actual imported projection tests run there. Required checks and independent external review before integration; no author approval.