Sequential Provenance Comparison: A Formal Verification Framework for Macroeconomic Settlement Protocols

Version 1.0 release of Sequential Provenance Comparison (SPC), a provenance-sensitive formal verification framework for macroeconomic settlement protocols. Macroeconomic identities and end-of-period balance sheets establish conservation relations but do not, by themselves, specify executable transaction histories. This article introduces Sequential Provenance Comparison (SPC), a formal audit method that combines structural operational semantics, labelled transition systems, and double-entry accounting. SPC represents institutional configurations as states, economic operations as guarded transitions, and transaction histories as provenance traces. It distinguishes event-level causal precedence, protocol-level feasibility comparison, and equality under aggregate observation. The method is applied to two order-sensitive problems. First, in a closed investment–saving model, a bank-credit protocol is feasible throughout an explicitly defined common augmentation family, whereas a strict prior-saving protocol additionally requires an inherited monetary balance. Second, in a closed sovereign-currency model, monetary tax settlement requires antecedent currency issuance in a Genesis or valid extended provenance; under a spending-only issuance regime, this becomes a spending-precedence result. In both applications, the reverse protocols are shown to be non-vacuous under mirror-consistent inherited-balance augmentations, while null augmentations provide strict witnesses for feasibility dominance. The article also formulates an operational projection-loss criterion: a valid provenance-changing segment that leaves the chosen aggregate observation unchanged is a concrete witness that the observation map suppresses executable history. SPC supplements stock-flow-consistent accounting by auditing the intraperiod event sequences required to reach balanced terminal states. Accounting determines what must balance, whereas protocol verification determines which institutionally specified sequences can reach those balances. This record contains the publication PDF, complete LaTeX source, reproducibility build log, README, CC BY 4.0 license notice, and SHA-256 integrity manifest. The PDF is not tagged for PDF/UA; Appendix H provides textual descriptions for Figures 1–5 and the unnumbered SPC Standard Views.