docs(spec): operator provisioning plane — Tamarin S9 model + TLA/conformance prose (stacked on #1657)

[tlongwell-block]

Stacked on #1657 (mini/community-provisioning) — the formal-model and prose follow-through for the operator provisioning plane. Docs-only: no code changes; merge after #1657.

Tamarin: new S9 section (docs/spec/MultiTenantAuth.spthy)

Models POST /operator/communities as a protocol surface: operator-signed NIP-98 requests whose signed preimage includes the payload hash h(<host, owner>), a relay provision rule and a converge/rotate rule both gated on the !OperatorKey allowlist (RELAY_OPERATOR_PUBKEYS), and a UniqueHostBinding restriction importing the append-only host map from ensure_configured_community's ON CONFLICT upsert.

Three new safety lemmas (+3 exists-trace probes, incl. the create-then-converge lifecycle end to end):

Lemma	Claim
provisioning_requires_operator_authorization	every owner bootstrap/rotation names an operator-registered key — no compromise disjunct, since compromising a secret doesn't extend the allowlist
provision_accepts_only_operator_signed_payload	the accepted (host, owner) pair is exactly one the operator signed — a captured Authorization header can only replay (benign convergence), never re-target
rotation_confined_to_host_community	rotation lands only in the request host's bound community (S5/S6 single-witness framing)

Verified: full run green, all 38 lemmas (32 existing + 6 new), Tamarin 1.12.0 / Maude 3.5.1, ~141 s.

Three mutations confirmed red (each uncommented in isolation and falsified):

• MUTATION_Provision_Unsigned_Body — models the review finding that buzz-auth's NIP-98 payload tag is verified only if present; falsifies the payload-binding lemma in an 8-step trace. This makes require-the-payload-tag on this endpoint a conformance obligation, not a review nit.
• MUTATION_Provision_Any_Client — allowlist replaced by "any valid signature"; falsified, 8 steps.
• MUTATION_Rotate_Ignore_Host — rotation escaping the named host's community; falsified, 12 steps.

TLA+: stated assumption, no remodel (docs/spec/MultiTenantRelay.tla)

Comment-only header note P-HOST-APPEND: HostCommunity stays a constant-per-segment function because the host map is append-only — provisioning extends the domain, never re-points a binding — so every existing TLC result remains valid across provisioning events. SANY-checked; the .cfg harness is untouched and no TLC re-run is needed.

Prose (docs/multi-tenant-relay.md)

• S9 added to §Authorization soundness.
• P-HOST-APPEND conformance row: append-only admission via the upsert, a migration lint (no UPDATE communities SET host), and the two endpoint obligations — payload tag required, allowlist checked against the NIP-98 signer.
• §Mechanized Verification + verification-status figures updated (32 → 38 lemmas, current run time; noted that older per-lemma step counts predate the model growth).
• Machine-check-hygiene classification for the new lemmas; fixed two stale .spthy line references.