Require a deterministic Z3 budget (SMTT("rN")) in the proof prompts

[tangruize]

What

Add one constraint to the two agentic proof prompts
(proof-completion.txt, proof-from-scratch.txt): proofs must bound the
SMT/Z3 backend with a deterministic budget SMTT("rN") (capped at "r30"),
not the wall-clock forms SMT / SMTT(n).

Why

Wall-clock SMT timeouts make a proof's pass/fail depend on CPU speed and load,
so the same proof can close on one machine and time out on another — a source of
non-reproducible grading. tlapm's SMTT("rN") (tlaplus/tlapm#283) bounds Z3 by
a deterministic resource count instead, so the outcome is identical across
machines and reruns for a fixed Z3 build. Capping at "r30" and requiring
decomposition beyond it keeps per-obligation cost bounded and pushes toward
finer-grained proofs.

Scope / notes

• Only the two agentic modes; the one-shot prompts are left unchanged, since a
  single tool-free response doesn't iterate on or tune backend timeouts.
• Requires a tlapm that includes Add a deterministic Z3 rlimit budget via SMTT("rN") tlaplus/tlapm#283. The 1.6.0-pre rolling
  pre-release the Docker image pulls was rebuilt from main right after #283
  merged, so it already carries SMTT("rN").