This is a deterministic behavioral replay checksum, not a digital signature and not independently attested. Verification applies an exact schema to the evidence object and the telemetry, rejecting unknown properties and any injection scheduled beyond the sealed tick, validating every recorded injection against a per action schema with required fields, permitted fields, and semantic value checks, recognized principals and responsibilities, a single supported value domain shared with the engine and the replay, so an unportable value yields a named refusal rather than an exception, typed hold durations, where a recorded duration outside the configured bound remains verifiable because the arbiter refuses it deterministically and the refusal is reproduced by the replay, and an explicit supervisor actor for veto engagement and clearing, recomputes the digest, confirms the frozen config hash, replays a fresh run from the same seed and injection schedule, and requires the entire replayed telemetry, the board, the go state, the failed set, the epochs, the statistics, and the ledger root, to equal the sealed telemetry field for field. It does not include or attest the per run capability identity, which is verified in memory by the authority and grant chain audits but is not part of the portable record.

Anchor: positive human control of a single critical, irreversible until commit authorization, expressed as an authority governance invariant. Governance and assurance only, no dynamics, no actuation, no targeting, no weapons. The guarded action is an abstraction; the model carries no operational or weapon detail.

Demonstrated model invariant: within the modeled scripted and seeded scenarios the arbiter maintains exactly one eligible authenticated holder for each responsibility. The two authorization keys are human only, a machine principal is never eligible to hold either, and they must be held by two distinct authenticated humans. The guarded action is representable as authorized, the go state, only when both keys are held by two distinct authenticated humans and no supervisor veto is in force; otherwise the state is the failure safe no-go. A supervisor veto is an explicit human action that names the available supervisor and moves the system to no-go with a bounded hold; a request that does not name the available supervisor, or that states a hold duration outside the configured bound, is refused and recorded rather than silently corrected. The arbiter may also engage a separately named fail safe hold on an autonomous allocator request, recorded as an arbiter action with its trigger and never as a human action. Clearing a hold is itself a supervised human action that requires the available supervisor, is refused and recorded otherwise, and can never be performed by the untrusted allocator, while an uncleared hold ends only at its recorded deadline. Either holder may revoke, returning to no-go. A commit is recorded only in the go state, and it is voided immediately whenever the current authorization state no longer exactly matches the committed go state, whether by revocation, holder loss, supervisor veto, lease expiry, or reassignment, opening a new epoch from no-go. The live audit reconstructs every authority transition and every commit from the ledger and compares them with the authenticated grant history, including the predecessor holder of each grant, the reason and basis pair bound to each event type, the reconstructed prior holder, justification, head grant, epoch, and exact expiry tick of every recorded role clearing, authorization key clearing, veto held key clearing, distinctness clearing, and lease expiry, the justification of every recorded commitment void and principal availability change, the non overlap and exact configured duration of every fail safe hold, the reconstructed conditions behind every recorded refusal and forged grant observation, a closed event vocabulary in which an unknown event type is itself a finding, a binding of every externally driven event in a scripted run to a matching recorded input, field for field including actors, durations, malformed payloads, and forged grant flags, resolving each scalar control request to the single effective input the arbiter actually used at that tick and consuming that input once, so a second event cannot claim the same source, and the actor, source, and supervisor availability of every recorded veto engagement, fail safe hold, and veto clearing, and a replay consistency check reproduces the complete private state, the commitment object, the veto deadline, the failed set, the generator state, the grant history including the type exact identity fields of every quarantined invalid grant, and the recorded run mode, from immutable run metadata captured at construction, the seed and mode fixed in the genesis record, together with the recorded injections, and remains the definitive provenance check for allocator driven behavior. The untrusted allocator issues only requests; it cannot name a grantor, install a grant, or mint a valid capability tag. Every request entering the documented interface must lie in a single supported value domain, bounded strings, finite numbers, booleans, null, and bounded plain arrays and objects with data properties only, and a request outside that domain is refused at the interface before it is stored rather than being partially accepted, so the live run, the private replay, and the portable record always admit exactly the same inputs and identity values are canonical data values.

Never a machine, in depth: machine principals are out of scope for the authorization keys, so a proposal to place a machine on a key is rejected at the interface; a forged grant that names a machine holder fails the capability check and is quarantined; and the arbiter clears any authorization key whose holder is not an available, in scope, authenticated human. The human control audit further scans the whole ledger and rejects any recorded key issuance to a machine and any commit not backed by two distinct humans.

Per-run capability, in-process and private: at run start the arbiter mints a random secret using the platform secure random source and holds it inside a private closure keyed to the run context. The whole engine runs inside a single private closure; the secret, the signing routine, the simulation state, and ledger mutation are never attached to the page global scope. The hash and random primitives are captured as immutable references at load. Randomness is fail closed. Every grant is bound by a keyed tag over its immutable authorization fields; an injected, stale, cross-run, or higher-epoch grant fails the tag or run identifier check, is quarantined, and never becomes the effective holder. This is an in-process capability marker for the simulation, not a hardware backed key or a public key credential. The authenticated identities are synthetic; this is not real authenticated human control.

Threat boundary: the adversary is the untrusted allocator, the proposal and injection data entering the documented interface. The browser host and pre engine scripts are trusted. A single HTML file cannot fully defend against a co resident script that executes before the engine; for high assurance use the engine would run as an isolated module or service.

Not yet established: this v0.13 build does not include formal model checking, property based adversarial testing, mutation testing, a digital signature, human credential authentication, implementation identity, a sealed release manifest, or an independent verifier. The invariant is demonstrated over the modeled scenarios, not proven over arbitrary distributed concurrency.

(c) 2026 Burak Oktenli, MBA. Georgetown University M.P.S. Applied Intelligence. ORCID 0009-0001-8573-1667. Washington, DC. CC BY 4.0.