3.1 Scoped capabilities

Mira can delegate only the authority she received. The record must therefore identify both the permitted act and its permitted effects. Judgment authority needs an answer scope as well: permission to answer one question need not include every possible determination. A capability is a tuple

c=(i,h,O_c,A_c,F_c,Y_c,[t_0,t_1],n,\pi,\sigma).

The issuer i delegates to the holder h. The set O_c is the object scope. The set A_c is the action scope. The set F_c\subseteq O_c\times\mathsf{Field} is the field scope. The set Y_c is the allowed judgment-answer scope. The interval [t_0,t_1] is the validity window. The natural number n is the remaining delegation depth. The value \pi identifies the parent capability, or a trusted root when no parent exists. The value \sigma is the issuer’s authentication evidence over the other fields.

A trusted root is a capability whose authority the model accepts as an axiom. A capability chain for principal p is a finite sequence from a trusted root to a capability held by p. The chain is well formed at time t when:

1. Every authentication check succeeds.

2. Every parent points to the preceding capability.

3. Each child issuer is the holder of its parent capability.

4. Each child object scope is a subset of its parent’s object scope.

5. Each child action scope is a subset of its parent’s action scope.

6. Each child field scope is a subset of its parent’s field scope.

7. Each child answer scope is a subset of its parent’s answer scope.

8. Each child validity interval is contained in its parent’s interval.

9. Time t lies in every link’s validity interval.

10. Delegation depth strictly decreases at each link.

11. No revocation or competent authority notice terminating any link, effective at or before t, appears in the trace prefix.

The chain’s effective scope is the intersection of all object, action, field, answer, and time scopes in the chain. Intersections are used because a delegate cannot grant more than it received.

Let \Gamma_\tau be the authority context recorded in trace prefix \tau. It contains trusted roots, issued capabilities, revocations, recorded authority terminations, and authentication material. We write

\Gamma_\tau \vdash_\chi p \triangleright (a,o)

when the named chain \chi is well formed and live at the evaluation time, ends at p, and its effective scope contains action a and object o. Naming \chi prevents different chains from supplying different parts of one authorization.

3.2 Rule outcomes and discretion holes

The filing rule needs the request history as well as the company record. Otherwise it could overlook an unanswered question or reuse an answer whose permitted use has ended. Let \Gamma^J_\tau be the auxiliary ledger derived from accepted events in trace prefix \tau. It records request revisions, consumption, discretion holes, original resolutions, derived uses, carriage, supersessions, and eligibility changes. It supplies evidence to the evaluator and leaves institutional state S unchanged. For each action a, the evaluator returns one of three results. It either permits the act, refuses it with a reason, or requests judgment:

R_a(s,q,\Gamma^J_\tau,t)\in \{\operatorname{Permit}(b),\operatorname{Refuse}(r), \operatorname{Awaiting}(j)\}.

A permit carries a rule receipt b=(r_b,\nu_b,e_b,\omega_b,J_b,\mathcal{G}_b).

A rule receipt records what supported the permission. The final commit receipt will also bind the actor, authority, actual change, and commit time. A judgment dependency is an answer used by that evaluation. An observation guard records a fact or query result that must still hold at use. The receipt identifies the rule, immutable version, evaluated evidence, request revision, exact judgment dependencies J_b, and observation guards \mathcal{G}_b. Every judgment dependency names a judgment-use record for \omega_b. It contains a direct resolution or an authorized derived-use certificate, as defined below. All guards of each derived-use record also belong to \mathcal{G}_b. The guards record relevant values, range results, and absence predicates. They include the current revision, consumption status, unresolved holes, superseding acts, conflicts, quorum membership, and policy-selected authoritative sources whenever the evaluation uses those facts.

3.3 Mutation footprints

The address example requires more than the action name. The operation must change only the fields its authority covers. We call the operation that proposes this concrete state change a primitive. For each action, a primitive transition function proposes a next state:

F_a(s,q)=s'.

The function also declares a write footprint W_a(s,q)\subseteq O\times\mathsf{Field}. The footprint lists every authoritative field the primitive may change. Primitive soundness requires the actual difference between s and s' to be contained in the declared footprint.

The footprint is part of authority, not only an engineering optimization. Permission to change a company’s address does not imply permission to change its shareholders. A capability that names an object but not its relevant action is incomplete. The pair of action scope and write footprint supplies the finer boundary.

3.4 Trace events

The ordinary filing submits a request, waits if judgment is needed, records an authorized answer, and attempts a commit. Authority notices or conflicting changes can intervene. The event rules below specify what each step must establish and which record it may change.

An execution trace is a finite sequence of the following events. Each event time is at least the prior event’s record time.

5.1 Check-time is not commit-time

Remove the live-at-commit premise. Let a capability be valid through time 5. Let the program check it at time 4 and commit at time 6. The trace changes state without a live chain at commit. Proposition 1(1) is false. Caching an earlier authorization result does not make the trace valid because recorded authority is temporal.

The same counterexample applies to revocation and to authority that ends by operation of law. Suppose a winding-up order ends a director’s power at 16:30 while a capability interval runs until 17:00. A 16:40 commit passes unless F10 brings the order into the authority context before the commit. The required legal-event source is therefore part of the hypothesis.

5.2 A hidden write defeats scoped authority

Remove primitive footprint soundness. Give Mira authority only to change the registered-office field. Let the address primitive also change the controlling-shareholder field. The visible action is authorized, but the actual mutation exceeds its scope. A type declaration is useless when the code can write around it.

This counterexample requires an exclusive mutation boundary in the surrounding system. If an administrator, database trigger, or external service can change the authoritative record outside the event rules, the theorem governs only the trace and not the institution.

5.3 Timeout is not judgment

Replace awaiting with “permit after 24 hours if nobody answers,” or let a later permit omit the earlier discretion hole from J_b. No authorized person answers, yet the workflow commits. The unresolved question has become permission through silence or dependency omission. F5 rejects both traces.

Identifier continuity alone does not bind a human answer. The complete pending record binds the payload, evidence, rule, question context, authority interface, validity conditions, and request nonce. A changed request requires a new revision. Earlier obligations remain open until answered, lawfully superseded, or carried to an authenticated successor obligation. A resolution for an earlier revision supports a new revision only through an authorized compatibility derivation and current-use checks.

Dependency completeness also includes predicate observations. Two contexts agreeing on recorded reads but differing in an unrecorded absence condition need not produce the same result. The whole-context condition requires that absence to be guarded whenever the evaluator depends on it.

A supersession creates the same defect if it is treated as an answer. Let Y_j contain \mathsf{suitable} and \mathsf{unsuitable}. A principal with supersession authority but no answer scope closes j. If that receipt could satisfy J_b, the request would commit without either allowed answer. The commit rule excludes that trace.

Fail-closed behavior can still impose harm through delay. The model prevents unauthorized commit. It does not prove that a reviewer answers promptly, that queues are fair, or that awaiting cannot be used strategically.

5.4 Generic delegation amplifies through interpretation

Suppose a parent capability permits “manage company matters,” and the system treats that phrase as containing every later action name. A child capability can then appear formally narrower while acquiring authority that the parent never specifically granted. Scope inclusion is only meaningful over a stable action vocabulary or a signed interpretation rule.

The formal model assumes that scope comparison is decidable and faithful. Schema evolution therefore needs an explicit rule. New action names must not fall inside old wildcard scopes by default.

The four counter-traces establish Theorem 2.

5.5 A receipt can faithfully record a wrong rule

Let the encoded filing rule omit a statutory condition. The workflow may satisfy every formal premise and issue a perfect receipt for a legally invalid change. The theorem still holds because it proves execution relative to the encoded rule. It does not prove semantic equivalence between that rule and law.

This is the central boundary of computational law. Evidence of faithful execution is not evidence that the specification was right.

6.1 Source coverage and authority use

Run B assumed that the boundary knew when Mira’s authority ended. Expiry can appear in the delegation itself. A court order or registry act instead requires information from a competent external source. An authentic source can omit an event. Sequence continuity shows which messages arrived. It does not establish which legal events occurred. A source contract therefore binds the competent owner, covered objects, event classes, jurisdictions, authoritative interfaces, and legal effect. It also binds maximum observation delay, the allowed use stage, outage behavior, conflict resolution, exposure accounting, and remedial owner. The selecting rule identifies the complete required source set. That policy is itself a guarded dependency. An empty source set requires an explicit source-independent rule case. Missing metadata supplies none.

A coverage witness records the source head, covered cutoff, retrieval time, contract version, and any current-use authorization. At use time u, the contract returns \mathsf{Ready}, \mathsf{Pending}, \mathsf{Conflict}, or \mathsf{Breach}. Ready requires valid coverage for every required source and a legally sufficient authority-use condition at u. A watermark records the source’s covered time cutoff. A watermark before u leaves an interval that needs its own justification. A signed no-event statement covers only the scope and time its competent source can establish. An unknown source set is Pending. Its recorded reason distinguishes missing scope, stale coverage, and a sequence gap. Competing competent sources require the contract’s authorized precedence or adjudication rule.

A source can provide a synchronous decision at the actual use stage. Alternatively, its institution can grant a transaction-specific authority whose legal effect covers that later use. A database reservation alone cannot postpone an immediately effective legal termination. The contract records which construction applies and who can grant it. Without either construction, a delayed observational feed does not establish F10 for a current authority-dependent act.

Pending or Conflict suspends the affected act and preserves its work, rights, reservations, and unanswered obligations. Independent workflows continue when their complete source sets remain ready. Preparation and counterfactual evaluation retain no dispatch right. A standing lawful emergency or protective procedure can run under its own ready authority contract. An ordinary workflow cannot create that power.

A contract may separately authorize measured exposure while a source is observational. It records a currency or loss unit, a maximum outstanding amount B, and a common reservation account across affected workflows. At observation delay \Delta, a defensible bound is B+v\Delta only when the institution establishes a maximum unreserved loss rate v. This is a conditional exposure bound, not a bound on every legal consequence. Shared reservations prevent concurrent duplication. Such a policy cannot certify F10 where the authority-use premise fails.

An omitted or delayed termination can later reveal a coverage breach. The notice records its actual effective and recording times, the failed contract, the affected acts, and the responsible remediation route. The original decisions remain historical observations. Their legal consequences follow the competent determination and the resulting authorized remedy. The system does not silently reclassify an earlier invalid act as authorized.

The formal admission rules are executable. Their external discharge requires a named competent source, its actual mandate, an agreed coverage service, observed delay and outage evidence, and an accountable owner. The construction does not supply those institutional facts by itself.

6.2 Retained evidence and independent reconstruction

The receipt in Run A names the board resolution and filing rule. A future reviewer must be able to obtain and read those exact materials. A digest identifies bytes. Reconstruction also requires possession and permitted use of those bytes. Each commit therefore carries a retained-evidence manifest. For every required item, the manifest binds its content digest, byte length, format, source act, disclosure class, retention deadline, and available custodian locations. An encrypted item also names its cipher suite, key identifier, authorized decryptors, and succession procedure. The manifest includes the transitive closure of rule inputs, authority acts, judgment origins, derived-use certificates, and source contracts. It also retains a reconstruction checkpoint and the required event suffix. The manifest excludes its enclosing receipt, avoiding a digest cycle. The export carries that receipt beside the manifest and supporting bytes.

Retention admission obtains authenticated custody receipts and an independent retrieval-and-digest check before Commit. The storage contract specifies the number and independence of custodians, repair time after loss, periodic retrieval checks, and key recovery. A pending dispute or continuing obligation extends retention through its applicable evidence duty. Expiry of an ordinary storage period alone cannot erase a live evidence obligation.

An export contains the receipt history, manifests, admitted rule interpreter, and every required preimage available to the receiving reviewer. Encrypted exports carry recipient-authorized key envelopes. The exporter checks disclosure authority before releasing bytes or keys. A successor reviewer can reconstruct the record without the author’s service when its role has the complete disclosure and decryption rights. A narrower role receives an explicit restricted result for hidden inputs.

The reconstruction result distinguishes \mathsf{Verified} from \mathsf{BlockedMissing}, \mathsf{BlockedKey}, \mathsf{BlockedDisclosure}, and \mathsf{Invalid}. Missing or undecryptable bytes produce a blocked result. A digest or authentication mismatch produces Invalid. An available digest without its required preimage cannot produce Verified. These results describe the evidence package, not the legal merits.

Later storage loss leaves historical receipts intact but marks their current reconstructibility as blocked. The retention owner recovers another authorized copy or records the failure and its affected obligations. Key rotation preserves the content digest and authorized access through a new attributable envelope. It never requires rewriting the original institutional event.

7.1 Sequential composition

If two actions commit in sequence, the second evaluates against the state produced by the first. Its authority and rule checks are fresh. A permit receipt from the first action does not authorize the second. This prevents a workflow-level approval from becoming a blanket capability. The second action has a fresh request nonce. Its commit requires fresh authority and an unconsumed current revision. An earlier human judgment can support the new action through its authorized derived-use record and current-use checks.

A composite workflow is authority preserving when every state-changing step passes the same commit rule. The conclusion follows directly from Theorem 1 because the trace proof is event-local.

7.2 Concurrent proposals

Two programs can read the same state and propose inconsistent changes. Premise 3 atomically compares the expected head with the current head. If they differ, the boundary records a conflict and requires a fresh evaluation. The rule result therefore applies to the state that changes, and an in-scope field cannot be silently overwritten with a stale value. Current revision, consumption, eligibility, and observation guards are checked in the same accepted transition. A conflict leaves request consumption and pending-record status unchanged.

This rule closes the local lost-update case in the sequential model. It does not prove serializability for distributed effects. That theorem still needs a conflict relation, scheduler semantics, and an equivalence proof.

7.3 Compensation

Institutional workflows often include external steps that cannot be rolled back exactly. A bank transfer, public filing, or delivered notice may remain historically true after a later failure. A compensation is a new authorized action that restores a business invariant. It is not deletion of the prior act.

The safe pattern stages external effects after all reversible checks, records an intent before dispatch, and requires a separate capability for compensation. Theorem 1 then covers each forward and compensating commit. It does not prove that the compensation restores an external world state. That claim requires a contract for the external primitive and an extensional proof or empirical test.

A commit receipt may confirm that an instruction was dispatched. Legal finality and beneficiary credit follow the receiving rail’s rulebook and account relationship. Swift carries messages rather than funds (Cipriani, Goldberg, and La Spada 2023). Its speed measure therefore does not establish end-to-end beneficiary credit (Swift 2025). Fedwire finality follows Regulation J and Operating Circular 6, not the sender’s local receipt (Federal Reserve Banks 2026).

Current evidence and a recognized determination may shorten a later evaluation. The commit boundary does not make onboarding, authority, or recognition relationships portable. Each relationship must be formed under the receiving institution’s rules (Du, Huang, and Scharfstein 2026).

7.4 Delegation and revocation

Each step still needs a complete delegation. Combining workflows creates no new source of authority. Scope intersects along one parent chain. A principal may hold several independent chains, and each chain authorizes its own acts. One act must be covered by one complete chain; different chains cannot supply its action, object, and field scopes separately. Quantitative limits add a common economic account to this chain. Section 7.5 gives its containment and consumption rules.

Revocation is checked before each act that uses authority. Already accepted events remain historical facts. A later revocation can stop future commits or trigger a remedy. Notice to a third party is a separate legal act that a receipt can evidence. Irrevocable powers lie outside this capability model. Systems that require retroactive legal effect need a separate remedial transition and a rule for downstream reliance.

7.5 Shared economic authority

Consider a principal who authorizes expenditure of 100 units and appoints ten agents. Giving each agent a limit of 100 permits aggregate expenditure of 1,000. Intersecting each child’s scope with the parent’s scope leaves this error intact. A quantitative limit constrains a history of actions. It therefore needs one account shared by every action in that history.

Fix a competent authority root b and a finite set D of resource coordinates. Each coordinate names a unit, purpose, and accounting window. For example, separate coordinates can constrain total expenditure, expenditure during a day, and expenditure on a named project. Finite overlapping windows also express rate limits on a discrete time domain. Every applicable coordinate receives a charge. Unspecified units and accounting windows require an explicit extension of the mandate.

The root binds its owner, accounting rule, validity interval, and canonical account identity. Every child retains that identity. An alias, a new workflow, or another service identity creates no additional root account. For each capability c, let B_c\in\mathbb{Q}_{\geq0}^{D} be its limit. A child satisfies B_{c'}\leq B_c coordinatewise, narrows the purpose scope, and has a contained validity interval. The ordinary chain rules continue to apply. Creating a child changes no resource balance.

For command k, let u_k\in\mathbb{Q}_{\geq0}^{D} bound its charge. The command binds its request revision, complete economic dependencies, effect description, and one capability chain. The accounting rule must justify u_k against every permitted external outcome. A local estimate alone supplies no bound on a provider’s actual performance. Let r_k be the unresolved reservation and s_c the cumulative charge already attributed to capability c and its descendants. Define U_c=s_c+\sum_{k:\,c\in\operatorname{chain}(k)}r_k. \tag{E1} The sum ranges over all descendants, including sibling agents and suspended workflows. Each command appears once in an ancestor’s sum. The root’s counter therefore represents aggregate delegated use.

Admission compares the entire chain and reserves u_k in the same transition that admits the immutable command. It requires U_c+u_k\leq B_c at every ancestor c. A batch reserves the sum of its new commands. Distinct commands can then execute concurrently from their separate reservations. Local serial admission leaves their external work parallel. The construction does not require a distributed serializability claim.

When authenticated performance incurs charge d\leq r_k, reconciliation replaces r_k by r_k-d and adds d to each ancestor’s s_c. An exact command retry returns the recorded admission without reserving again. Each fresh dispatch still checks current authority and the complete current dependency set. A suspended or uncertain attempt retains r_k. Unused capacity returns only through an admitted release proving that further charged performance is excluded. A timeout supplies no such proof. Historical performance can be recorded after authority has ended without granting a new dispatch right.

A lifetime expenditure coordinate retains its consumed charge after a refund. A replenishable balance requires its own accounting rule and authenticated receipt. An exposure coordinate can permit release when its specified risk ends. Neither transition proves performance of an unrelated delivery obligation. Cash availability, expenditure authority, and outstanding duties have distinct projections of the same state.

Theorem 3 (aggregate economic attenuation). Suppose one boundary owns every counter for a canonical root. Assume complete command coverage, nonnegative charges, faithful charge bounds, atomic admission, and the transitions above. Starting with 0\leq U_c\leq B_c, every reachable state satisfies that inequality for every capability c. The result includes all sibling delegates, exact retries, suspended commands, and concurrent external execution.

Proof. Creating a child adds zero usage. Admission adds the new reservation to each affected ancestor and checks its limit atomically. Reconciliation moves d from reservation to consumed charge, so U_c is unchanged. A justified release decreases U_c. An exact retry changes no counter. Revocation changes authority and leaves historical charges and unresolved reservations intact. These cases exhaust the transitions. Induction on the admitted history proves the result. Concurrent external actions retain their separate reservations throughout their execution. \square

Two agents with limits 40 and 60 can reserve and execute both commands against a root limit of 100. If both hold limits of 100, one reservation of 100 excludes another. A shared intermediate capability with limit 50 also constrains the sum of its children, even when the root has unused capacity. Parent attenuation and aggregate accounting perform different parts of the argument.

This construction makes the common reservation account of Section 6.1 precise. Its economic dependencies use Lemma 2 and the same guarded membership and range observations as the commit boundary. It adds no alternative test for dependency completeness. A physical resource shared between separate institutional roots requires an explicit common allocation authority or a sound partition. Different root names alone establish neither construction.

7.6 Authority over affected rights

The shared account limits aggregate use. It does not identify whose rights an admitted use changes. A one-field change can alter many rights. Replacing a fee schedule may change the amount owed by every client whose contract refers to that schedule. The field footprint correctly identifies the written field. An additional projection identifies the resulting economic and legal changes.

Fix a guarded universe I of affected institutional relationships. For i\in I, define \rho_i(s) as its rights projection in state s. This projection includes the holder, obligor, applicable terms, amount or performance, priority, maturity, and discharge conditions relevant to the action. A created or removed relationship has a distinguished absent value on the other side. Define its actual impact by \mathcal I(s,s')=\{i\in I:\rho_i(s)\ne\rho_i(s')\}. \tag{E2} The action declares a set J containing \mathcal I(s,s') and supplies the current amendment authority for each changed projection. This authority names the exact old and new terms and their effective time. It includes consent when the governing rule requires consent. A competent public power or constitutional mandate can supply a different lawful basis. The construction does not convert every institutional duty into a commercial agreement.

The registered universe and its membership generation are guarded inputs. The dependency analysis includes the rules that interpret each relationship, their relevant data, and any range query that selects affected parties. A new affected contract invalidates a proposal’s old membership guard. The boundary recomputes the impact before committing it. Source completeness and competent authority remain the explicit institutional premises of Section 6.1.

Proposition 2 (economic impact attribution). Assume the registered universe covers every relationship in scope, the projections are faithful, and the impact guards hold at commit. If \mathcal I(s,s')\subseteq J and each changed projection has the required current amendment authority, every changed right in scope has that authority. Every relationship outside J has the same projection before and after the commit.

Proof. A changed projection belongs to \mathcal I(s,s'), hence to J, where its exact amendment authority is checked. If i\notin J, then i\notin\mathcal I(s,s'). Equation (E2) gives \rho_i(s)=\rho_i(s'). \square

For example, existing contracts can bind a fixed schedule while new contracts adopt a separately authorized schedule. A change for future contracts then preserves the existing clients’ projections. Charging those clients a higher fee instead requires their applicable amendment basis. Permission to write the schedule field supplies only the field part of that authority.

Complete impact analysis is a semantic obligation. The proposition does not infer an unrecorded right from a database field. Finite explicit contract families permit direct evaluation of every projection. More general rule languages need a sound abstraction or their own completeness argument. This is the same distinction between a declared write footprint and its faithful implementation, applied to the meaning of the record.

7.7 Viable continuations

A workflow can respect both its resource limits and its amendment authority, yet fail its obligation to deliver. An authorized action can leave no funded route to the required result. Spending 60 from a balance of 100 is within a limit of 100. It still strands a delivery that requires a further 60. A useful program therefore needs a continuation condition in addition to next-action permission.

For the balance of 100, a delivery route costing 90 can be viable, as can a route costing 80. The policy retains both when their declared outcomes meet the goal. The 60-unit preliminary purchase is excluded when every subsequent delivery costs another 60 and further funding is unavailable. Its local authority remains valid. It fails the stated continuation goal. A lawful refund route can remain available as a remedy while lying outside a delivery-only goal.

A continuation must work after every response allowed by the contract. We compute such continuations backward from the permitted outcomes. The first construction assumes the program sees the complete state. Here S denotes the safe subset of workflow states, distinct from the institutional state space used in Section 3.

We give an exact finite construction. Let X be a finite, fully observed state space. A state records current authority, source coverage, budget counters, outstanding rights, external outcomes, and the remaining time. Let S\subseteq X be the states allowed by the governing safety and risk contract. Let G\subseteq S be a nonempty set of authorized terminal outcomes. Delivery, discharge, and a permitted remedy have explicit predicates. A refund belongs to G only when that goal permits it. Public-service performance can define G through its governing mandate.

A policy chooses the next action from the state it observes. The environmental contract states how providers and other authorities can respond before the policy chooses again. At x, the finite set A(x) contains the actions or batches that satisfy the current commit, economic, and affected-rights rules. The finite environmental contract gives a finite family \mathcal P_E(x,a) of complete observable response paths for each action. Each path starts at x and contains at least one transition. Write \operatorname{Post}_E(x,a)\subseteq X for their final states. Terminal states occur only at response endpoints and admit no further act. The contract states the covered provider outcomes, evidence delays, authority changes, and losses. An executable action has at least one successor. An empty successor set cannot certify completion by a vacuous universal statement. The contract also binds the identities and versions that give these states and transitions their meaning.

For example, a safe first purchase must leave a permitted continuation after every allowed price, performance, and authority outcome. The sets V_h below collect states from which completion remains guaranteed within h decisions. The sets \Pi_h(x) collect all next actions preserving that guarantee.

Write \mathsf{SafePath}(x,a) when every state on every response path lies in S. For a horizon of h decision rounds, define \begin{align*} V_0&=G,\qquad \Pi_0(x)=\varnothing,\\ \Pi_{h+1}(x)&=\{a\in A(x):\mathsf{SafePath}(x,a),\; \varnothing\ne\operatorname{Post}_E(x,a)\subseteq V_h\},\\ V_{h+1}&=G\cup\{x\in S:\Pi_{h+1}(x)\ne\varnothing\}. \tag{E3} \end{align*} At a terminal state the policy stops. Elsewhere it retains every member of \Pi_h(x). Outside S, define \Pi_h(x)=\varnothing. The remaining horizon decreases after every response path.

Theorem 4 (finite viable continuation). For the stated fully observed contract, x\in V_h exactly when a policy can keep every reached state in S and terminate in G within h rounds, against every response path in \mathcal P_E. Here the horizon counts decision rounds. Every action in \Pi_h(x) at x\in S\setminus G preserves this guarantee. Any action outside that set at x\notin G fails to supply such a guarantee for the remaining horizon.

Proof. For h=0, completion means x\in G. Suppose the equivalence holds for h. From a nonterminal state, a policy must select an executable action whose response paths stay in S and whose every final state admits a remaining policy of horizon h. The induction hypothesis makes this exactly the condition defining \Pi_{h+1}(x). The state itself must belong to S. Conversely, choose any action in that set. After observing its outcome, use the corresponding policy furnished by the induction hypothesis. Its horizon decreases and it reaches G. Empty successor sets were excluded, so this implication cannot use an impossible transition. The same argument proves the claim for every retained action and excludes each other first action. \square

An intermediate violation followed by restoration fails \mathsf{SafePath}. Safe endpoints alone establish no such guarantee. Each response path also retains the per-event guards of Theorem 1. An initial batch decision supplies no authority for an unchecked later act. Each response contract has a finite duration bound, represented by the clock in X. A deadline belongs to S and G when the mandate requires it. Waiting beyond that deadline is then an explicit losing outcome.

The recursion is ordinary finite backward reachability. Its institutional content lies in the state, action, and environmental contracts being composed. Theorem 3 contributes aggregate resource bounds. Proposition 2 contributes authority over changed rights. The original commit theorem supplies current authority, complete dependencies, and effect attribution. No one of these properties implies the others.

A safety contract can permit a measured loss. The theorem does not require every transaction to be riskless. Its universal quantifier ranges over the declared environmental outcomes. A provider failure or authority change outside that set is a contract breach, requiring a fresh analysis from the observed state. A rejected transition preserves existing rights and obligations. It cannot replace delivery with a newly convenient goal.

The finite reference construction evaluates every action and successor in Equation (E3). It includes parallel sibling reservations, ancestor limits, revocation before dispatch, uncertain performance, and fee changes affecting existing and future contracts. Its witnesses distinguish an authorized dead end, a viable alternative, an impossible transition, and a refund outside the delivery goal. These establish the stated finite semantics. The next construction treats partial observation. Unbounded service and production adapter refinement require additional results.

7.8 Acting from incomplete observations

A delayed answer can arrive after the acting delegate loses authority. The answer resolves the judgment. A current authority check still governs the next effect. Meanwhile, independently authorized preparation can continue. The program needs to distinguish these three conditions while retaining every useful continuation supported by its evidence.

Example 1 (useful work through suspension). One party reserves 80 units of money. The other reserves one service slot. A pending judgment can approve or refuse performance. Its answer arrives within two admitted service opportunities. Here a service opportunity is an admitted chance to obtain that answer. The acting delegate can lose authority during either opportunity or during independent preparation. The evidence returned to the program reports the judgment. The authority change remains hidden until a guarded attempt returns its result.

After approval, the program can still be uncertain about its delegate’s authority. The same observation is compatible with a live delegate and a revoked delegate. A command must therefore be safe in both cases, and its observed response determines what can happen next. This requires a set of possible states rather than one assumed state.

Let X and \overline A be finite sets of states and command choices. Let S\subseteq X be the safe states and G\subseteq S the fulfilled or expressly permitted terminal outcomes. A state includes all memory that constrains later responses, including hidden authority and pending response obligations. The initial contract supplies a nonempty set B_0\subseteq X containing every initially possible state. A belief B is the nonempty set of states consistent with the complete action and observation history.

The controller is the program that implements the policy. For each x and a, the contract supplies finite response paths \mathcal P_E(x,a). Each path starts at x and ends at the next controller decision. Intermediate steps obey the same authority, rights, and resource guards as a separately issued act. The controller makes no intervening choice. Its transcript \operatorname{obs}(p) contains exactly the evidence and timing it observes. Hidden state labels never enter that transcript automatically.

A program cannot choose different actions in states its observations do not distinguish. Its next choice must have a defined response in each possible state. An action is uniformly executable at B when \mathcal P_E(x,a)\ne\varnothing for every x\in B. One guarded attempt can therefore succeed under live authority and return a local refusal under revoked authority. Both are responses to the same choice. Refusal preserves the outstanding duties and their reservations. An empty response family in one possible world prevents uniform execution.

The update keeps precisely the endpoints compatible with the response actually observed. Thus approval can settle the judgment while leaving authority uncertain; a later guarded attempt can resolve that uncertainty.

For a possible transcript z, define the updated belief U(B,a,z)=\{\operatorname{last}(p):x\in B,\; p\in\mathcal P_E(x,a),\;\operatorname{obs}(p)=z\}. \tag{E4} Write Z(B,a) for the transcripts that these paths produce. Every update for z\in Z(B,a) is nonempty. An observation outside Z(B,a) is a contract breach. It supplies no completion certificate.

The actual endpoint belongs to every successive belief. Initially this holds by the state contract. Each actual response starts in the prior belief and produces the received transcript. Equation (E4) therefore retains its endpoint. Complete state memory makes the update exact. A conservative transition contract instead gives a conservative belief, which can exclude actions that the actual environment would permit.

Actual fulfillment and knowledge of fulfillment differ. Completion can be declared precisely when B\subseteq G. A belief containing a fulfilled world and a pending world still requires evidence. Unlike the terminal convention in Section 7.7, fulfilled states here can admit evidence-only responses. The controller’s declaration ends the policy.

We now apply the same backward argument to sets of possible states. \mathcal W_h contains the beliefs from which safety and known completion can be guaranteed within h decisions. The set \widehat\Pi_h(B) retains every first choice with that property. Each possible observation must lead to a belief with a shorter guaranteed continuation.

Let \mathsf{SafePath}(B,a) require every state on every response path from B to lie in S. Define \begin{align*} \mathcal W_0&=\{B:\varnothing\ne B\subseteq G\}, &\widehat\Pi_0(B)&=\varnothing,\\ \widehat\Pi_{h+1}(B)&=\{a\in\overline A: a\text{ is uniformly executable at }B,\\[-2pt] &\qquad\mathsf{SafePath}(B,a),\quad U(B,a,z)\in\mathcal W_h\text{ for every }z\in Z(B,a)\},\\ \mathcal W_{h+1}&=\mathcal W_0\cup \{B:\varnothing\ne B\subseteq S,\; \widehat\Pi_{h+1}(B)\ne\varnothing\}. \tag{E5} \end{align*} Set \widehat\Pi_h(B)=\varnothing when B is unsafe or B\subseteq G. At other winning beliefs choose any retained action. After receiving its complete response, apply Equation (E4) and decrease h by one.

Theorem 5 (viable continuation from observations). Under the complete finite contract, B\in\mathcal W_h exactly when an observation-based policy guarantees safety and known completion within h decision rounds. The guarantee covers every permitted response path. At a nonterminal safe belief, \widehat\Pi_h(B) contains exactly the first actions of such policies. Every retained action preserves the guarantee for the remaining horizon.

Proof. At horizon zero, every possible world must satisfy the declared goal. This is exactly \mathcal W_0, and G\subseteq S supplies safety. At a nonterminal belief, a policy chooses before observing the next response. Its choice applies uniformly across all possible worlds. Each response must exist and remain safe at every intermediate step. After transcript z, Equation (E4) gives precisely the remaining worlds. Induction identifies their winning continuation policies with U(B,a,z)\in\mathcal W_h. These are exactly the conditions in Equation (E5). Conversely, each retained action and the corresponding posterior policies satisfy those conditions. The decreasing horizon forces completion. This also proves the assertion about all first actions. \square

The theorem uses universal path guarantees. Its objective differs from almost-sure reachability under a probability model. Subset constructions for imperfect-information games are established methods. Reif (1984) studies games of incomplete information. Chatterjee and Doyen (2011) explain why belief alone can fail for other stochastic objectives. Here the belief and remaining horizon suffice because they determine all future choices and responses under the stated contract.

Return to the 80-unit service in Example 1. With six rounds remaining, both preparation and a service request are winning first actions under a delivery-or-permitted-cancellation goal. Consider preparation, one pending response, then approval. The next guarded attempt either performs or records local refusal. Refusal keeps the money, service slot, and both parties’ duties intact. A separately authorized owner action can then transfer the unused reservation to a fresh command. The owner performs under its own current authority. The original command retains its identity and refusal history.

The refusal branch uses six rounds:

1. Preparation completes.

2. A service opportunity returns a pending response.

3. The next service opportunity returns approval.

4. The guarded attempt records local refusal.

5. The authorized owner transfers the unused reservation.

6. The owner performs under its current authority.

This path pays 80 once and performs the service once. An adverse judgment instead requires the admitted joint cancellation and its simultaneous releases and discharge. The delivery-only goal is losing when that adverse answer is possible. Returning money alone does not discharge the other party’s performance claim. The example’s mandates and response competence are explicit premises. The finite transition table implements their modeled consequences.

Example 2 (progress without forced approval). A response monitor records the original obligation and its remaining service opportunities. At each required opportunity, it supplies an allowed answer or decreases the counter. At zero, the next opportunity must yield an allowed answer, refusal, expiry, or authenticated failure. The contract determines which of these outcomes can meet the goal.

The counter belongs to the hidden state whenever its value is unobserved. Retries retain the original counter. Resetting it permits indefinite delay and invalidates the finite guarantee. Weak fairness alone also permits arbitrary finite delay. A calendar bound additionally requires a schedule and a duration bound for the complete decision round. If each round, including the controller’s choice, takes at most d time units, h rounds take at most hd. An absent competent response at expiry breaches that contract.

Retaining every action into an eventual winning set would permit an idle loop. Equation (E5) retains idle only while enough rounds remain for completion. In the two-party example, idle is available at horizon seven and excluded at horizon six. The policy preserves freedom within the specified deadline.

The finite reference evaluates Equation (E5) on demand. It also checks complete observation-policy trees for small games and traces all retained choices in the two-party example. These tests distinguish hidden deadlock, intermediate unauthorized effects, lost observation history, false completion, and response-counter resets. The construction requires complete institutional and provider contracts. Large state spaces call for abstractions whose soundness and useful action retention are proved against the same semantics.

The accompanying Programmable Institutions: supplementary construction contains the finite observation controller, the two-party example, and their reproduction tests.