Rocq M1 fix: accept Verified_tier3_provenance in close_or_fail

CI surfaced the real next gap once Vampire was in the manifest list:

  File "./rocq-bridge/hammer/Test.v", line 45, characters 2-14:
  Error: proof_broker: cert minted but verifier rejected
         (reason=verified_tier3_provenance,
          tier=3 format=tstp-thf backend=vampire/5.0.1)

Good news: Vampire mints a clean Tier-3 tstp-thf cert for the HOL
goal and the SDK's TSTP verifier accepts it
(`Verified_tier3_provenance`). Bad news: the Rocq plugin's
`close_or_fail` only matches the older verified reasons
(`Verified_envelope | Verified_farkas | Verified_case_split |
Verified_tier3`) — the `Verified_tier3_provenance` constructor
was added on the Lean side when Phase-3 M2 (TSTP verifier)
landed, and the Rocq mirror never picked it up.

Add `Verified_tier3_provenance` to both:
* `close_or_fail`'s accept arm — invokes `closer_for_fragment`
  on the cert's fragment, which now routes HOL/FOL to
  `proof_broker_hol_closer` (hauto when ProofBrokerHammer is
  imported).
* The `render_path` verbose form's `ok` boolean — so
  `proof_broker?` debug output reports `ok=true` instead of
  `false` for HOL Tier-3 certs.

Soundness: same gate as `Verified_farkas` gating lia. The
OCaml TSTP verifier has accepted the cert's envelope and
provenance (no smuggled axioms, refutes the negated goal,
reaches $false); whatever proof term hauto emits is then
kernel-checked, and the test theorem's `Print Assumptions`
footprint is gated by `tools/check_axioms.py`. Audit H1
unchanged.

Locally verified: SDK + Rocq plugin sources build clean.
The trust-gate verdict on hauto's actual axiom footprint
remains the open question — CI will report it.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: levineuwirth

rocq-bridge/src/pb_rocq_main.ml

@@ -135,7 +135,8 @@ let render_path (p : path) : string =
       let kind = Proof_broker.Verifier.kind_of_reason r in
       let ok = match r with
         | Verified_envelope | Verified_farkas
-        | Verified_case_split | Verified_tier3 -> true
+        | Verified_case_split | Verified_tier3
+        | Verified_tier3_provenance -> true
         | _ -> false
       in
       Printf.sprintf "  verify:   %dms, ok=%b (%s)" p.verify_ms ok kind
@@ -220,7 +221,18 @@ let close_or_fail (p : path) : unit Proofview.tactic =
     let kind = Proof_broker.Verifier.kind_of_reason r in
     (match r with
      | Verified_envelope | Verified_farkas
-     | Verified_case_split | Verified_tier3 ->
+     | Verified_case_split | Verified_tier3
+     (* Verified_tier3_provenance gates the home-system closer
+        (kernel check, audit H1) exactly as Verified_farkas gates
+        lia: the OCaml-side TSTP verifier accepted the cert's
+        envelope + provenance (no smuggled axioms, refutes the
+        negated goal, reaches $false), so the registered
+        proof_broker_hol_closer (hauto, opted-in via
+        ProofBrokerHammer) can produce a kernel-checked proof
+        term. Same arm the Lean closer added when M2 (TSTP
+        verifier) shipped — Verified_tier3_provenance is the
+        gate for the Vampire HOL path. *)
+     | Verified_tier3_provenance ->
        closer_for_fragment cert.refinement_record.fragment
      | Tier_check_deferred _ ->
        (* Tier 0 oracle path: no soundness verifier ran but the