TSUMS 4.0V-BOI Core: Replayable Accountability Interface (Paper + Verifier + PBAB-mini)

A deterministic, parameter-bound state-machine interface enabling replayable accountability verification under strict boundary-of-intervention constraints (policy-neutral, non-adjudicative). This release includes a core paper, an executable formal verifier (Dafny/Z3), and a minimal synthetic benchmark (PBAB-mini) for reproducing replay invariance and accountability injectivity / vacuum detection results. Reproducibility: dafny verify src/verifier.dfy (Docker/CI in ZIP)