proofs: query assumptions for every compiled witness, not only the controls #131

Found in review of #130 (Codex P1). The instrument proves the escape-hatch scan is
correct and the kernel-level controls query assumptions with Print Assumptions /
#print axioms, but the witnesses the lane actually compiles only take the
compile path:

• scripts/check-proofs.sh runs coqc <module> and treats exit 0 as a closed proof.
  A Rocq witness that imports and uses an axiom declared in another module still
  compiles, the lexical ledger scan sees no declaration inside the artifact, and
  axioms: [] is accepted.
• Nothing queries Lean's #print axioms, so sorryAx reachable through an
  imported module would not be caught either.

What "wired" should look like

1. For each gated Rocq module, after it compiles:
   • coqchk -silent -o <module> on the built .vo, and fail if it reports any
     axiom not named in that leg's axioms (and fail on any axiom at all when the
     leg records axioms: []);
   • or a generated driver that Requires the module and runs Print Assumptions
     for every declaration in statement_formal.declarations, comparing the output
     with the ledger entry.
2. For each gated Lean module, a generated probe that imports it and runs
   #print axioms for each recorded declaration, failing on sorryAx or on any
   axiom the ledger does not name.
3. The receipt records the query output verbatim, so the claim is reproducible
   rather than merely asserted.

The gate already refuses a proven leg whose declared axioms do not match what
the lexical scan finds; this closes the remaining path, where an axiom is imported
rather than declared in the artifact.

Until then the honest description of the lane is: compiles the witnesses and
reports the ledger's axiom lists, and the kernel-level axiom query is exercised
on the control fixtures only. PROOF-STATUS.adoc should say exactly that.