The Sovereign Substrate

The principal paper lists, among the formal specifications it identifies as open, two that concern constitutional currency: a specification of compile-at-commit semantics under which "no act executes under stale governance" can be proved, and a specification of the uniform invalidation surface under which "compiled forms cease to authorise execution within bounded latency after invalidation events" can be proved. This formal companion supplies both, for a model of the surface, and reports the results and their limits plainly.

Two things are established. First, the faithful formalisation of "no act executes under stale governance" is a property of invocation events, not a state invariant over which compiled forms are invocable. The natural state-invariant encoding is false, and a model checker produces the counterexample automatically: in the adoption interval between a governing change and the invalidation of a dependent form, the form is affected and still marked invocable. This is exactly the adoption latency the architecture admits in its own statement of the property.

Second, the bounded-latency claim holds as a single certified theorem: a compiled form affected by any of the six invalidation triggers becomes non-invocable no later than its deadline, fixed at the triggering event plus a bound Delta. The bound is certified by the TLA+ Proof System for arbitrary instance cardinality, over a model in which the constitutional-source update propagates through the genuine transitive closure of the credential-derivation graph, with that cascade independently model-checked to multi-level depth.

The paper corroborates the architecture's stated semantics while refuting a natural but incorrect state-based formalisation of those semantics. The mechanism the architecture describes, uniform per-act refusal of invalidated forms with an admitted and bounded adoption latency, is coherent and is what the model exhibits. These are results about a model; their attribution to the architecture rests on a stated and traceable rendering, with the modelling judgements and scope limits named.