3.1 External facts and commit-time status

Some facts come from outside the claim engine. A public register may establish who holds an office. A separate instrument, rule, and current status must establish whether that office carries authority for the requested transaction. That authority can end by law even if the office record remains unchanged. A compliance service may establish holder eligibility. A custodian may establish asset control. A payment system may establish final settlement. A tribunal or court may establish a disputed outcome.

Fix ambient types \mathsf{Principal}, \mathsf{Time}, and \mathsf{Snapshot}. Fix also a global type \mathsf{OccurrenceKey} of issuer-authenticated identifiers for external occurrences. A family admits such an identifier only through its own typed canonicalization map.

The payment example needs an identity for the credit itself as well as an identity for each assertion about it. An amount correction changes an assertion about the credit. It must not create another credit that the engine can use for a second discharge. The following record separates those identities.

Write \mathsf{Fact} for the type of well-typed tuples in this definition.

The definition does not make an external fact true. It makes the asserted source, scope, occurrence, and evidence explicit. The issuer remains responsible for the identifier namespace that it authenticates.

An effect premise is an admitted fact asserting an external occurrence that an obligation transformer consumes. A settlement-observation premise reports the evidentiary state of a settlement occurrence without changing the obligation. A status premise asserts a condition such as authority, capacity, or eligibility. Every single-use external effect must be expressed as a keyed occurrence. An authority fact used to issue a claim is a status premise. A provider assertion below the route’s final class is a settlement-observation premise. A payment used to discharge the claim is an effect premise.

Authority can change while a request is being evaluated. The engine therefore needs an authenticated view of the relevant sources at commitment. A source head identifies its current recorded state; the snapshot records the heads used by this decision.

Every admitted event time satisfies \theta\leq\tau. A policy may bound how far into the past an event may be recorded; it cannot admit a future event.

The admitted set has a canonical order and digest. Admission proves only that the named policy allowed reliance on the assertion for this request under h_\Sigma. It does not prove the assertion or the policy’s legal adequacy.

3.2 Claim families

The interface groups the zero-coupon example’s requirements into explicit mathematical data. State, events, and the safety predicate describe valid local behavior. The obligation and holder projections expose what a transition changes. A derivation then separates effects justified by external occurrences from changes, such as issuance, that its authority permits directly.

The remaining data record consumption, settlement evidence, and permitted reliance on receipts. Settlement evidence uses a preorder because two different assertions can have equal evidentiary strength. Its least element means that no evidence has been admitted. A finite map records the exceptional entries; all other entries retain that least value.

The family lists the individual external uses in a derivation. Their image under the key map is the set of occurrences consumed by that step:

Write W_F(\pi):=\mathsf{key}_F[V_F(\pi)]. The obligation carrier depends on the family. It can be one amount, a dated multiset, or a set of covered duties. A transition derivation \pi exposes the authority, holder, and external-effect premises used by that transition. The common engine verifies the derivation but does not interpret the private obligation carrier.

The settlement ledger is indexed only by settlement effects. Tribunal, corporate-action, insurance, and other obligation-changing occurrences remain general effect keys; they need not have settlement-ledger entries. The ledger is not one scalar status for the whole claim. A final 60-unit payment and a pending 40-unit payment therefore occupy different keys. For a settlement key k on one route, the evidentiary order can contain \mathsf{None}_{F,k}\prec_{F,k}\mathsf{Submitted} \prec_{F,k}\mathsf{ProviderAccepted}\prec_{F,k}\mathsf{Final}_{F,k}. \mathsf{Final}_{F,k} means that the route’s content-addressed status map classifies the settlement as irrevocable and unconditional under that route’s rules and legal basis. A reversible provider success cannot map to \mathsf{Final}_{F,k}. The preorder compares evidentiary strength. It does not replace the route’s temporal state machine.

A reliance scope names the class of relying party, the proposition that the receipt supports, the jurisdiction or rule context, and an expiry. The order \sqsubseteq_F means “no broader than.” A technical receipt can therefore support engine audit without purporting to create contractual, regulatory, or third-party legal reliance.

One family can govern many individual claims. Each instance binds the exact semantics that currently interpret its state. A template pack, defined below, adds the institutional conditions for using the family in a named setting.

Some events become due without a fresh human instruction, such as a coupon payment date or milestone review. The scheduler must recognize the same due event after a retry or a software change. Otherwise it could create another execution opportunity for an already decided event.

A scheduled occurrence has an enduring economic duty identifier d, admitted from its constituting act and occurrence index. Section 7 defines its canonical registry and migration rule. For event class c and authorized decision generation g, define u=H(\mathsf{Enc}(d,c,g)). The active semantic binding separately identifies the program that evaluates this event. A family due key resolves to its registered d, never to a new duty merely because a content digest changes. The trace gives each derived identifier a disposition in \{\mathsf{Pending},\mathsf{Accepted},\mathsf{Refused}\}. Every due pair returned by \delta_F uses the displayed identifier. A due identifier with no terminal decision is pending. The schedule returns no terminal identifier. Awaiting leaves the identifier pending. Acceptance and refusal are terminal for that identifier. Reactivation after refusal requires an authorized new decision generation for the same duty. It preserves the refusal and the economic history.

A derived event does not mutate a claim inside another event’s atomic step. The authorized scheduler submits it through the ordinary transition interface with origin \mathsf{Derived}(u). Each derived event therefore has its own request, decision, result, receipt, and trace step. The engine recomputes \delta_F after every committed step and orders only pending due identifiers. After an awaiting result, a retry uses the same derived identifier, a fresh nonce, and the current base. A conflicting authored event cannot pass a pending higher-priority derived event. Evidence input and cure remain available while that event awaits. Section 3.6 gives their transitions and progress conditions.

3.3 Family admission packs

A family definition states possible claim behaviour. It does not state that a particular institution may issue, transfer, settle, or rely on that claim in a particular legal setting. That second question belongs to an admission pack.

\mathsf{SettlementAsset}_F is a finite set of records (\mathit{asset},h_P,\mathit{evidence},\mathit{reviewCycle}). The digest h_P binds a settlement policy. Its evidence must meet the policy’s current-use conditions.

For the pack’s admission check, an instrument’s harbor set lists jurisdictions recorded as admitting its constitution or operation. The issuer’s harbor set supplies the corresponding entity-level boundary. The following inclusion requires each instrument jurisdiction to lie within that boundary.

For an instrument S issued by an entity E, the pack also requires \mathcal H(S)\subseteq\mathcal H(E), where \mathcal H gives the set of jurisdictions in which the instrument or entity is harbored. A composite instrument needs an explicit recognition record for the composition. Recognition of each component does not imply recognition of the composite.

The Claim as Primitive defines the payoff program and pricing interface that each family instantiates [21]. One Entity in Many Jurisdictions defines the composed standing and instrument harbor set that constrain holder eligibility [22].

An obligation of 100 units needs a rule identifying which asset and transfer count as those 100 units of performance. That rule also determines the evidence needed for the intended amount and recipient. The settlement policy records these conditions explicitly, including conversion when the units differ.

Netting can replace several gross obligations with a smaller set under a specified legal arrangement. Its arithmetic and its legal basis are separate requirements. The pack records the latter before any joint transformer can use it.

Registration and legal recognition are different relations. A pack is registered when its fields are complete, mutually consistent, and accepted by the engine registry. It is recognized by a regime for a purpose only when a named authority or published rule gives the pack that effect. Recognition is indexed by both regime and purpose. \mathsf{Unknown} fails a recognition condition; it is neither recognition nor rejection. Registration alone creates no legal recognition.

A guard is one condition that the request must satisfy. Ordered guards make a negative decision reproducible when several conditions fail or need evidence. The decision certificate records the first such condition and the facts used to classify it.

The content-addressed family and pack semantics declare a finite guard sequence. It covers family derivability and all applicable conditions (A1)–(A8). The order respects each guard’s typed input dependencies and fixes failure precedence. A canonical negative certificate \nu\in\mathsf{NegativeCert}_{F,T} names the first failed or missing condition and binds the facts that establish that classification. Define the total pre-receipt decision type \begin{aligned} \mathsf{Decision}_{F,T}={}&\mathsf{Accept}(\mathcal{S}_F\times\Pi_F\times\Omega_{F,T})\\ &\uplus\mathsf{Refuse}(\mathsf{Reason}_F\times\mathsf{NegativeCert}_{F,T})\\ &\uplus\mathsf{Await}(\mathsf{Requirement}_F\times\mathsf{NegativeCert}_{F,T}). \end{aligned} For fixed inputs, \mathsf{PackDecision}_F(T_F,s,a,E,\theta,\tau,\Sigma) \in\mathsf{Decision}_{F,T} returns the accept constructor when the family derivation and all eight conditions hold. It returns the refusal constructor for the first resolved false condition and the awaiting constructor for the first missing party-supplied premise after successful ingress. An unavailable or unauthenticated mandatory commit-current source is an ingress failure. The certificate of an accepted decision is \omega; otherwise it is \nu; this defines the projection \mathit{cert}(\eta). The permitted-scope function has type Z_{F,T}:\mathcal{S}_F\times\mathcal{A}_F\times\mathcal{P}_{\mathrm{fin}}(\mathsf{Fact})\times \mathsf{Decision}_{F,T}\to\mathcal Y_F. Z_{F,T} is evaluated after the decision exists and before its receipt is constructed.

The following catalogue shows how the pack question varies with claim meaning:

Each entry calls for a family and one or more packs. The table describes possible admission questions; it does not supply their answers or prove the family laws. Intellectual-property and royalty claims use the final entry unless the instrument has another family’s legal and economic form.

A compliance tier groups states by a threshold in an order of compliance conditions. A state passes when it meets that threshold. Nested thresholds retain this ordering when conditions compose; an unexplained color label does not specify such a rule [20].

3.4 Serialized engine environment

Two valid requests may both name the same unpaid 40 units. The store must choose a serial order and let the second request see the first decision. Comparing the requested base with the current base supplies that check. A new revision distinguishes a later record even if its private balance returns to a value seen before.

An ordinary request must name the active binding \beta in the observed base. Changing that binding requires an authorized carriage or economic transformation that commits the old and new bindings and a new base. The trace theorem below applies within a binding. Section 7 extends preservation across meaning-preserving carriage and separates it from amendment.

The family owns claim meaning. The environment owns serialization, content resolution, time, status freshness, and idempotency. A theorem about a family alone cannot establish those engine properties.

3.5 Transition requests, results, and receipts

The request binds the event and the evidence proposed for it. The decision records what the evaluator concluded. The receipt then commits that conclusion together with the inputs and changes needed to audit it. This order avoids letting a receipt’s description determine its own permitted effect.

The three results distinguish a permitted change, a known failure, and a question that needs evidence from its named authority. Refusal and awaiting preserve the private claim state. Each novel committed decision still advances the audit revision and receipt root. Thus non-mutation here concerns the private claim state, not the absence of an audit record.

The receipt’s obligation delta is the pair of before and after projections, rather than an untyped numeric difference. This permits a family to expose several dated or contingent obligations through the same receipt structure.

A receipt is evidence of the engine decision under committed inputs. It is not evidence that an external payment settled, that title passed, or that a court will recognize the result. Those propositions require the external evidence and reliance policy named in the receipt.

The family state records the operational position represented by the engine. It does not decide the legal position. Applicable law and the instrument determine whether an entry is constitutive, evidentiary, or neither. For example, under sections 112 and 127 of the Companies Act 2006, membership outside the initial subscribers requires agreement to become a member and entry in the register, while the register is prima facie evidence of the matters it must contain  [7]. Under section 136 of the Law of Property Act 1925, a legal assignment of a debt or other legal thing in action requires an absolute assignment in writing under the assignor’s hand and express written notice to the debtor, trustee, or other person from whom the assignor would have been entitled to claim [18]. An engine receipt commits to and retains evidence of those acts. It cannot supply a missing agreement, signature, entry, or notice. A reliance scope identifies the proposition and audience for which the receipt may be used. It does not decide the proposition’s legal effect.

3.6 Typed diagnostics and evidence cure

The transfer to a holder with missing eligibility evidence needs a precise answer: which assertion is missing, about whom, and from which source. A diagnostic pairs a fixed reason tag with those particular values. A cure supplies evidence for a recorded requirement and triggers a fresh evaluation under the applicable current rules.

A diagnostic separates a finite reason vocabulary from its data. For schema version v, define \mathsf{Reason}_F=\sum_{t\in\mathsf{ReasonTag}_F}\mathsf{Payload}_{v,t}, \qquad \mathsf{Requirement}_F= \sum_{t\in\mathsf{RequirementTag}_F}\mathsf{Payload}_{v,t}. These dependent sums need not be finite. A missing-fact tag can carry a predicate, subject, authority, and evaluation date. The same tag therefore describes different entities and dates without adding codes. The content-addressed schema fixes field types, canonical encoding, and size limits. It rejects unknown fields, ill-typed values, and unsupported schema versions before any claim write. A malformed certificate is a validation error. It supplies neither a refusal nor an awaiting judgment.

The concrete schema uses identifiers of at most 256 UTF-8 bytes, nonnegative integers of at most 256 bits, and canonical ISO calendar dates. A diagnostic occupies at most 4096 bytes. Its finite tags distinguish missing facts, blocked predicates, quantity bounds, consumed allocations, lifecycle conditions, and pending derived events. The payload identifies the exact subject and required source.

Evidence must remain admissible while execution awaits it. The input interface has three constructors: \begin{aligned} &\mathsf{Input}(\widehat E),\\ &\mathsf{Cure}(d(r),m,\widehat E),\\ &\mathsf{Review}(d(r),\mathit{reviewKind}). \end{aligned} Each signed envelope binds the claim, submitter, operation, and input nonce. Input standing permits delivery. It grants no authority to assert the delivered facts. A cure names an existing awaiting receipt and its exact requirement. A review requests a named reconsideration procedure. The resulting decision or evidence enters through its ordinary authenticated source.

Input operations append to a separate immutable journal and proposed-fact store. Their nonce namespace is distinct from claim-transition nonces. An exact retry returns the recorded input result. They change no private claim state, claim revision, receipt root, allocation, funding reservation, or derived disposition. The input service accepts adverse or superseded assertions as historical records. Only admission selects the authoritative, current assertion for a transition. Evidence delivery cannot advance an authority source’s status root.

A recorded relevant input wakes the scheduler. A retry binds an explicit proposed-fact bundle, current base, and fresh transition nonce. The evaluator recomputes all guards, including current authority and prohibitions. A known prohibition therefore remains a refusal after an unrelated cure. An awaiting derived identifier remains pending. A refused identifier remains terminal. An authorized family transition may advance the decision generation after changed facts. It retains the same economic duty, the earlier refusal, and the new event’s authority.

Evidence delivery and claim decisions use separate journals because uploading a fact should not change the obligation. The first proposition states this separation for an execution whose decision inputs remain fixed. The next adds the availability and scheduling premises needed for delivered evidence to resolve pending work.

The proposition names its environmental progress premises. An unanswered discretionary question remains awaiting until its authorized source answers. It creates no substitute authority and changes no pending obligation.

3.7 Finality strata and lifecycle records

The word “final” has four distinct referents. Engine finality means that the serialized claim trace has committed a result. Asset finality means that the authoritative asset book treats its position entry as irrevocable under its rules. Cash finality means that the designated payment system treats its cash leg as irrevocable and unconditional. Legal settlement means that the instrument, applicable law, and governing rulebook treat the obligation as discharged. A bound rule may map one stratum to another. No mapping is implicit. In particular, engine finality alone implies none of the other three.

A funding instruction, a settlement-ledger confirmation, and credit to the named beneficiary are different records. A claim is described as paid only when authenticated evidence establishes beneficiary credit under its bound rule. For example, Regulation J makes a Fedwire funds transfer final between the relevant participants at the event specified by section 210.31. The receiving bank’s obligation to its beneficiary remains a separate question under Appendix A [5]. Participant finality therefore does not by itself establish beneficiary credit.

Op: A Typed Bytecode for Compliance-Carrying Operations defines the typed external-effect boundary and authenticated provider-finality evidence consumed here [23]. Recourse defines the contested-outcome route and keeps award, execution, satisfaction, and recovery separate [24].

The authoritative asset book can be external to the engine. A central securities depository, registrar, or other named book can establish the asset position under the pack’s adapter and authentication rules. The engine records that evidence. It does not become the authoritative book by observing it.

An institution can expose the distinction through a lifecycle projection J_F(T_{\leq i}) from the committed trace prefix. The projection can give each instruction one stable identifier and an append-only sequence such as \begin{aligned} \mathsf{Received}&\longrightarrow\mathsf{Validated} \longrightarrow\mathsf{Matched}\longrightarrow\mathsf{RiskAccepted}\\ &\longrightarrow\mathsf{SettlementInstructed} \longrightarrow(s_A,s_C), \end{aligned} where each leg is pending, ready, or final. Ready means that every condition for issuing the external settlement instruction is satisfied; it does not mean final. The projection can show \mathsf{LegallySettled} only when both legs are final and the bound instrument, legal rule, and authority evidence establish that consequence. Rejection, an unresolved match, or a curable hold is a typed result. Cancellation, correction, force transfer, and reclamation are new events. None rewrites an earlier event or receipt. The projections B_F and L_F are inputs to J_F but do not determine validation, matching, risk acceptance, or legal settlement by themselves. The lifecycle record is not an independent claim state. Prefix extension can append or refine a current status under the bound temporal rules; it cannot erase an earlier record.

3.8 Corporate actions

Splits, dividends, mergers, rights offerings, tenders, conversions, and redemptions are family events rather than exceptional edits. A corporate-action request must bind its type, declaration, record and effective times, parameters, authority, affected positions and holders in that claim, and requested base. Its family derivation must state exact holder, issued, burnt, cash, escrow, reserve, and obligation deltas. It must also establish the relevant funding, issuance-cap, target-holder, settlement, and lifecycle conditions. This engine commits one atomic effect block only when the action belongs to one claim record. An action spanning claims requires either one composite claim state or an engine extension with a joint base and vector compare-and-swap. The theorem below does not establish that extension. A missing curable condition yields \mathsf{Awaiting}; an invalid action yields \mathsf{Refused}. Neither decision changes claim state. Conflicting actions need an ordering rule in the bound family semantics. Calendar order alone does not supply one.

For example, a cash-dividend activation map fixes the declared amount, record snapshot, eligible positions, payment date, funding route, and rounding rule. It emits one complete effect record per credited position. A split activation map fixes the ratio, record snapshot, treatment of fractional positions, and effective time, then emits the exact old and new quantities. Declaration does not prove funding, and an emitted payment instruction does not prove beneficiary credit. One complete action-effect record has the typed fields \begin{aligned} (&\mathit{actionId},\mathit{positionId},\mathit{holder},\mathit{effectKind}, \mathit{oldQuantity},\mathit{newQuantity},\\ &\mathit{cashAmount},\mathit{currency},\mathit{settlementKey},\mathit{status}), \end{aligned} with an explicit none value for a field that the effect kind does not use. Formally, the partial activation map has type \alpha_F:T_{\leq i}\times\mathcal{S}_F\times\mathsf{CorporateAction}_F \rightharpoonup\mathcal{P}_{\mathrm{fin}}(\mathsf{ActionEffect}_F). It is defined only when the authority, record-time, effective-time, pack, and family guards hold. Both displayed action classes use this map.

The theorem also excludes an outcome-sensitive batch of several instructions. Any such extension must bind the batch membership and order digest before the outcome is revealed. It must then resolve the outcome, execute the already fixed instructions in that order, and reject any post-revelation addition, removal, or resequencing. The derived-event schedule does not supply those batch semantics.

4.1 Engine laws

These are assumptions on a conforming engine, not conclusions about every storage system. The remote protocol below realizes the current-source check under additional cooperation and recovery premises. Concrete family constructors later show how the local transition laws can be discharged.

4.2 A protocol for remote commit-current predicates

A source can report valid authority and then change before the claim commits. A separate store can also allocate the proposed payment elsewhere during that interval. Preparation reserves the records a transaction needs while one durable decision is formed. A fence prevents a conflicting write from passing an unresolved preparation. The transaction’s footprint is the complete set of records and predicates it reads or changes.

The commit-current premise has an operational realization when every required source supports authenticated preparation and fences conflicting head updates. The following protocol defines that realization. Each transaction has a stable identifier t. It binds the request, semantic digests, participant set, remote predicate set, and complete read and write footprints. The dependencies include the policy and authority roots that determine the current owners, participants, and footprint. Preparing previously selected participants does not validate a changed participant-selection policy.

A source that must change a prepared head first resolves each conflicting transaction. If commit wins, the head update follows that commit. If abort wins, the update follows the abort. The source cannot advance the head while leaving an undecided prepared vote usable. The same rule applies to governing policy roots and owner mappings.

Expiry prevents a later commit. It does not authorize unilateral release of a prepared fence. A valid earlier commit may exist behind a failed connection. The participant obtains a terminal decision before releasing the fence. The decision service records abort after expiry if no commit exists. Recovery queries that durable decision record and never infers abort from silence. It reconstructs unresolved preparations and their fences before accepting successor writes. An epoch change cannot discard a preparation that the decision service may already have committed.

This protocol lets independent institutions retain their own source write authority. It requires cooperation in the named transaction rather than a shared global institutional ledger. External settlement retains its own provider occurrence and finality evidence.

4.3 Family laws

For the zero-coupon claim, issuance creates the debt, transfer changes the holder, and a final payment reduces the debt. The family must justify each change under the same interface. In particular, every external fact that determines an obligation delta must appear as a keyed effect. Hiding the same payment inside another transformer would evade a consumption check.

This law says that every accepted event has the authority witness required by the family rule. It does not prove that the family rule correctly states applicable law.

These laws form the interface. A new family enters the common lifecycle only after it supplies a concrete derivation system and proves the family laws. A conforming engine separately establishes its registry, status-freshness, evidence-retention, nonce, serialization, and receipt obligations. A product label is insufficient.

5.1 Disjoint claims and the boundary of netting

The single-claim result allows concurrent work only when its dependencies permit it. Separate claims can still compete for one payment, cash balance, or authority record. The next two propositions give conditions under which changing the execution order leaves both results unchanged.

A shared ordered constraint permits a second case. Each request tightens the constraint by taking a meet, the greatest value below both inputs. If the combined tightening still satisfies both requests’ thresholds, their shared updates can commute. The hypotheses also exclude hidden dependence on the intermediate value.

The proposition is request-specific non-interference, not a closure theorem for families. A product family would also need definitions for initial state, derived-event priority, transition and pack-admission witnesses, obligation and holder projections, authority, tagged occurrence keys, settlement orders, reliance, and combined failures. Each family law would then need a proof for the product. Disjointness of one pair of requests does not supply those definitions. A composite instrument also needs a pack recognized by a named regime for the relevant purpose.

Netting does not satisfy these hypotheses merely because its arithmetic sums to zero. For claims 1,\ldots,m, a netting extension needs the joint obligation vector \mathbf b=(B_{F_1}(s_1),\ldots,B_{F_m}(s_m)) \in\prod_{j=1}^m\mathcal O_{F_j}. The pack must also name a commutative exposure monoid (A,+,0) and typed maps e_j:\mathcal O_{F_j}\to A. For every admitted key k, it names a native effect type \mathsf{EffectDelta}(k) and a typed normalization \iota_k:\mathsf{EffectDelta}(k)\to A. The joint extension binds a total delta \Delta_k\in\mathsf{EffectDelta}(k). Its derivation must bind the included claims, legal basis, authority, pre-net vector \mathbf b, post-net vector \mathbf b', and an allocation (a_{k,1},\ldots,a_{k,m})\in A^m for every canonical effect key k. Here a_{k,j}=0 when k does not change component j, and \sum_j a_{k,j}=\iota_k(\Delta_k). The joint transformer must prove \mathbf b'=N(\mathbf b) under that allocation. The pack must name the conserved exposure projection and prove its exact pre-net and post-net equation; any settlement delta must equal the sum of its allocated final effects. One atomic cross-claim registry must consume each allocated key once. Close-out netting or novation changes obligations under its contract and legal authority. Cash settlement changes them only under admitted final-settlement evidence. These are minimum interface requirements, not a general netting theorem. The pack’s \mathsf{NettingBasis} identifies the asserted legal model. It does not discharge these joint-state obligations.

AMM-Aware Central Counterparty Risk develops multi-claim clearing and risk allocations. This paper supplies the occurrence-attribution and funding contracts for their joint execution under the pack’s declared netting basis [25].

5.2 Occurrence attribution and funding

A completed payment and a current cash balance are different resources. Attributing a receipt determines which obligations that occurrence satisfies. Reserving current cash determines whether another command can spend it. The engine represents both resources and commits their applicable constraints with the affected claim transitions.

Suppose one final credit of 100 supports two claims. Allocating 60 to the first must leave at most 40 for the second. Stable portions record exactly which parts each claim used. A later correction or reassignment must retain those portions’ ownership history, so that restored evidence cannot silently fund another claim.

Each allocation has an immutable identifier subordinate to o. It binds the claim, purpose, exact slice set, quantity, authorizing transaction, and predecessor allocations. A consumed slice retains its allocation provenance after support is disputed. Changing the reporter, legal origin, command, or observation cannot create another Q_o^e. Replaying an allocation identifier returns its recorded disposition. It does not change the partition again.

The consumable identity changes at this extension. The base theorem assigns one whole occurrence to one claim. Partial attribution instead gives each allocated portion its own single-use identifier, while all such identifiers retain the same physical occurrence as their source.

For a monetary settlement effect in this extension, the consumable key is an allocation identifier a. Its evidence package contains the occurrence evidence and the allocation-service witness. The family uses the partial map \kappa_F^+:(\mathsf{OccurrenceKey}\times\mathsf{AllocationId}) \rightharpoonup\mathsf{AllocationId}. It returns a only when the witness binds a to occurrence o, this claim, and the exact supported quantity. This map replaces the occurrence-only canonicalization for allocated effects. The consumed set C_F^+(s) contains allocation identifiers and never shrinks. Nonmonetary effect keys occupy a disjoint tagged namespace. A shared monetary occurrence cannot also supply an unallocated native effect.

The physical occurrence remains separately addressable. Settlement observations are indexed by that occurrence. The family’s allocation-indexed evidence projection follows the bound root and can reach no class above its authenticated evidence. Its obligation delta cannot exceed the supported allocation quantity. The adapter proves the other family laws for this extended state and witness type. Naming an allocation field does not discharge those laws.

The local single-consumption law applies to allocation identifiers. Issuer key discipline supplies one canonical physical occurrence. Allocation-service discipline supplies one canonical identifier for each use. The original single-claim theorem is the special case that assigns one complete occurrence to one claim. The extension admits several partial uses without treating them as several payments.

The partition equation now gives the bound on supported claim credits. Its preservation requires joint claim and allocation writes. Otherwise one store could discharge a claim while another still treats its payment portions as available.

5.3 The zero-coupon family

The opening example instantiates the transition-critical fragment used in the trace theorem. It does not supply a complete registered pack, derived-event schedule, reliance order, or reason algebra. Fix a registered pack whose admission witnesses establish the authority, holder, settlement, reporting, dispute, and reliance conditions used below. The state is either \mathsf{Draft}, \mathsf{Outstanding}(I,h,100,M,L,C), or \mathsf{Discharged}(I,h,100,M,L,C). Fix a precision c and let \mathsf{Amount}_c\subset\mathbb Q_{\geq0} be the representable amounts at that precision. Here M:\mathsf{SettlementKey}_F\rightharpoonup\mathsf{Amount}_c is a finite partial map from final-settlement keys to amounts, L is the settlement-effect ledger, and C=\operatorname{dom}(M) is the consumed-key set; this family has no other consuming effect keys. Assume 100\in\mathsf{Amount}_c, set \mathsf{EffectDelta}_F=\mathsf{Amount}_c, and define B_F(s)=100-\sum_{k\in\operatorname{dom}(M)}M(k), \qquad G_F(s)=\{h\} for an issued state. Define B_F(\mathsf{Draft})=0, G_F(\mathsf{Draft})=\varnothing, C_F(\mathsf{Draft})=\varnothing, and P_F(\mathsf{Draft})=1. The settlement map M belongs to issued states. The issued-state invariant is 0\leq\sum_k M(k)\leq100,\quad C=\operatorname{dom}(M), and every k\in C is bound by admitted provider evidence to this claim, route, currency, and amount M(k).

The event alphabet contains \mathsf{Issue}(A), \mathsf{Transfer}(h'), and \mathsf{Observe}(k,z,x), where z is a route-defined evidence class; in this example \mathsf{Final} abbreviates \mathsf{Final}_{F,k} for the displayed key. The accepted issuance transition starts at \mathsf{Draft} and requires a current issuer-authority fact. It creates the 100-unit obligation with empty M and C, and with L at its default \mathsf{None} entries. It has no external-effect premise: V_F(\pi)=\varnothing and D_F^0(\pi) is the constant map b\mapsto100. Transfer requires authority from the current holder and an admitted eligibility fact for the destination. It has empty effect use, D_F^0(\pi) is the identity, and it changes G_F but leaves B_F, M, L, and C unchanged.

For \mathsf{Observe}(k,z,x), require k\in\mathsf{SettlementKey}_F. Admitted provider evidence must authenticate k=(\mathit{authoritativeNamespace},\mathit{recordKind}, \mathit{stableEventId}) through the nominated recipient-credit record. A provider transaction reference can be an authenticated alias. Its account, asset, book, and identifier epoch must satisfy the admission policy. A related interbank posting or foreign-exchange leg is distinct, not an alias. The evidence must bind the claim, amount x, and currency as attributes. The derivation records Q_F(\pi)(k)=z. If z\prec_{F,k}\mathsf{Final}, it can change L(k) under the route’s temporal state machine but has the identity D_F^0(\pi) and V_F(\pi)=\varnothing. If z=\mathsf{Final}, it requires k\notin C and 0<x\leq B_F(s). It supplies one effect use u with \mathsf{key}_F(u)=k, sets \Delta_F^{\mathrm{eff}}(\pi)(k)=x, adds M(k)=x, and uses R_F(x)(b)=b-x with identity D_F^0(\pi). The state becomes discharged exactly when the result is zero. A final amount above the outstanding amount is retained in the evidence store and returns \mathsf{Refused}(\mathsf{AmountExceedsOutstanding},r) for this claim. An attempt to finalize a consumed key returns \mathsf{Refused}(\mathsf{EffectAlreadyConsumed},r). A corrected assertion about a known key updates its attributes under the route rule; it cannot create a second occurrence. Before consumption, a correction may replace or lower a sub-final ledger entry only under the bound route’s temporal state machine. An assertion that no longer binds this claim, route, and currency cannot later promote the entry. If the correction changes a consumed amount or finality classification, it cannot rewrite the earlier discharge. The route must supply a distinct corrective or reversal occurrence, or the request remains non-accepted.

A later return, reversal, or insolvency avoidance does not reinterpret the original \mathsf{Final} occurrence. It is a new authenticated occurrence with its own key. The governing terms determine whether that occurrence creates a new obligation, which then enters this family through a new admissible transition or enters another claim family.

On a shared settlement rail, this example uses the full-allocation special case of Section 5.2. The allocation service binds the use of k to one immutable allocation identifier for the exact claim and amount. It reserves that attribution and commits consumption with the claim transition. The private consumed set alone does not establish this cross-claim condition. General partial allocations use allocation identifiers as monetary effect keys while retaining k as the physical occurrence. Attributing a completed receipt does not debit current cash again. A later return uses its own debit occurrence and governing recovery transition.

The settlement ledger is a finite map with \mathsf{None} as its default. The permitted reliance scope always includes the proposition “this engine evaluated this request” for engine auditors. A provider-settlement proposition is available to a claim party only when the admission policy explicitly permits that proposition, party class, route, jurisdiction, and expiry. No zero-coupon rule creates third-party legal reliance.

The eight transitions map to the interface as follows. k_{60} and k_{40} are different provider effect keys. \Delta L shows the old and new value for each changed entry.

These cases define U_F. The displayed authority and holder premises define A_F and H_F(\pi,p). The two transformers, consumed-key updates, and per-key evidence ceilings prove obligation accounting, keyed effect allocation, single consumption, holder admissibility, and finality non-escalation by case analysis. Refusal and awaiting cases are non-mutating. The family invariant follows because a final event requires 0<x\leq B_F(s).

5.4 Two concrete family constructors

The zero-coupon example has only an unconditional payable amount. To test the same interface on a different obligation, consider a grant whose payment becomes due after a milestone. Completion must move quantity from contingent to payable, while payment moves it from payable to settled. Assignment leaves both quantities intact. These changes determine the two-component state below.

A closed interpreter instantiates the interface for transferable receivables and milestone grants. A receivable starts with one payable obligation. A grant starts with contingent rights and makes each payable after authenticated completion. Both families support assignment, partial payment, final payment, and historical replay.

The parameter record fixes issuer, initial holder, asset unit, positive integer quantities, component dates, authorities, settlement policy, and reliance scope. It contains a constructor name and declarative fields, with no supplied callback. Schema validation rejects unknown fields, ambiguous identities, nonpositive quantities, and inconsistent units or due order. The family digest binds both constructor semantics and parameters. The reference implementation bounds component sets to 1024 entries. The following rules apply to every finite admitted parameter set.

6.1 Private retention and offline replay

A receipt digest cannot supply the facts needed to recompute a decision. The archive must retain the actual inputs and the ability to authenticate them. Privacy adds a second requirement: the archive must control who can recover those inputs. The following storage rules preserve replay under changes of encryption keys and archive location.

A retention policy \rho names controller, governing source, permitted purposes, recipients, retention intervals, holds, key custodians, and disposal authority. A replay manifest binds the initial base, nonce map, ordered records, terminal root, and their complete transitive input closure. The closure includes semantic objects, proposed facts, historical public keys, authentication rules, source snapshots, and shared allocation evidence. A retained checkpoint defines a replay range. It does not recreate earlier inputs.

Canonical digests remain inside the private archive. Each object is encrypted under a fresh data key with authenticated encryption. The associated data binds its digest and retention policy. Recipient keys wrap the data key for an exact authorized access class. Public references are random opaque handles. Publishing a plaintext hash of a low-entropy private fact can disclose that fact through enumeration, so that hash is not a public privacy mechanism.

An offline grant binds recipient, manifest, purpose, operation, and permitted disconnected use. Its recipient receives the full authorized input closure. Replay verifies historical authentication and canonical digests locally. It performs no current-status request and executes no external action. A policy requiring current authorization instead requires an online access check. Revocation cannot recall plaintext already disclosed under an earlier grant.

Key rotation rewraps each required data key and verifies that every canonical plaintext remains recoverable before retiring the previous managed key path. An archive transfer decrypts, verifies, and imports the complete authorized closure. The receiving archive confirms the same terminal replay result before source disposal. Historical signature verification retains public trust material, rather than old signing keys.

Full replay, selective disclosure, and commitment verification have distinct results. A missing preimage, missing key, denied access, or invalid authentication prevents full replay of any range whose closure needs that object. A tombstone cannot act as the missing evaluator input.

Disposal requires the named authority, expired retention duty, and absence of a hold. Its record identifies exact managed objects, key copies, replicas, and affected ranges. The archive records disposal intent before removal and records each completed removal. Unknown external copies remain outside a claim about completed managed disposal. The remaining commitment can authenticate a later produced record. It cannot establish full replay while the required content remains unavailable.

The executable archive uses AES-256-GCM, per-object data keys, recipient wrapping, private SHA-256 digests, and random public handles. Its offline bundle binds signed source material, the requested manifest, and the exact loaded reference-program digest. The loader fixes the program identity at initialization and rejects later source drift. The tests recover and replay both families with network access disabled. They check access denial, rotation, retention holds, authorized disposal, missing inputs, and ciphertext or manifest alteration. The deployment authority must supply the applicable policy and control its actual recipients, key custody, replicas, and deletion records.

The replay theorem fixes the interpretation as well as the event sequence. A one-threshold holder rule already shows why this matters.

6.2 Committed refusals

Refusals matter because they explain why a submitted claim event did not change state. A system that commits only accepted effects cannot distinguish a rejected transfer from a transfer that was never evaluated.

The proposition does not prove that every attempted request entered the log. A censored request leaves no committed receipt. Submission evidence and log-inclusion evidence remain separate requirements.

7.1 The enduring duty and its representations

An admitted constituting act creates an economic duty identifier d=H(\mathsf{Enc}(\mathit{issuerNamespace}, \mathit{constitutingAct},\mathit{occurrenceIndex})). The issuer’s admission rule identifies the authoritative act and its aliases. It registers an occurrence index once within that act. A changed template, family, price, route, or program cannot register another copy of the same duty. This is an institutional identity premise, strengthened by a unique registry entry. Collision resistance alone does not identify two descriptions of one legal act. A genuinely additional issue receives its own constituting act.

A quantity coordinate lets the record distinguish portions without tying them to a particular family’s position names. Mark each portion with its current rights and whether it is contingent, payable, or discharged. The journal also retains the acts that produced those labels. This retained history is needed when a later return or correction refers to an earlier payment.

The interval coordinate identifies portions of one duty. It does not identify money in a bank account. A settlement allocation separately identifies the provider occurrence that discharges a portion. For indivisible performance, the same construction uses a finite set with its declared measure. Quantities in different assets, units, or performance classes remain separate.

For a rights tuple t and disposition label \ell, write X_d(t,\ell) for the portions of duty d carrying that tuple and label in the journal. In the 100-unit example, these labeled portions distinguish the paid 60 from the payable 40 before either is assigned to a successor position.

This adapter is a substantive family proof obligation. Equality of a displayed balance is insufficient. A grant with 100 contingent units and a receivable with 100 payable units have the same total and different obligations. The disposition-indexed projection distinguishes them. It also prevents coalescing two creditors into a scalar balance that conceals who may collect.

An event address is u=H(\mathsf{Enc}(d,\mathit{eventClass},g)). Its execution address additionally records the active binding \beta. An accepted evaluation need not discharge a duty. A refusal never does so by itself. A permitted cure can authorize generation g+1 for the same d, retaining the earlier refusal. Rearming changes an execution opportunity. It cannot create another economic entitlement or clear a payment allocation.

7.2 The carriage transition

Carriage replaces the family representation while keeping the same journal. Its witness must show exact coverage by the old and new representations. It must also establish that the old program loses permission to execute new work when the successor becomes active.

Extend a committed claim base to contain z=(F,\beta,s,\nu,\rho,J,\mathcal R). The family still supplies its private state and laws. The additional journal connects the obligation projections of different families. Its content digest is bound into the state digest and every migration request.

The mutable footprint includes the query that discovers affected duties and participants. A changed discovery result, alias map, absence condition, or range invalidates the prepared migration. The joint protocol in Section 4.2 supplies the required commit discipline for remote records. A list of the records found before preparation does not establish that the list remains complete.

The old-binding fence controls new dispatch. A command dispatched before carriage retains its original duty portions and reservation. Its delayed outcome is reconciled under that original binding, even after activation of the new family. The current family sees the resulting change to J. An unresolved old command therefore cannot be forgotten, redispatched as new, or used to release its reservation. Moving execution between stores additionally needs exclusive handover of the canonical registry and the same funding authority. A local receipt cannot supply that remote exclusion by itself.

7.3 Amendment and useful execution

The journal makes a rights change visible as a different operation from relabeling positions. This matters for the transferred or amended remainder in the opening example: the new representation must preserve whichever rights the authorized economic event actually created.

Pure carriage preserves meaning. An assignment changes the beneficiary under its own authority. A novation, maturity extension, conversion, release, or additional issue changes other rights under its own admitted rule. Such an event records an economic transformation and its lineage before or after carriage. A repayment extension cannot be presented as a lossless decoder. An exchange of currencies requires its denomination rule and evidence. The engine can compose these events while retaining the separate justification for each change.

The finite-integer construction instantiates X_d by integer cells. It uses signed carriage witnesses, current authority epochs, exact base comparison, partition checks, and one serialized journal. It reserves payable duty portions. The funding-domain field identifies the external cash authority and does not implement its cash ledger. A 100-unit coupon paid before a template change remains discharged. A 60-unit payment can pass into a paid 60-unit position and an unpaid 40-unit position. The remaining payment can then settle, and both positions can coalesce. A command prepared before the change can settle afterward against its retained duty reservation.

The same construction reads the concrete receivable and milestone-grant states of Section 5.4. It retains their source state, trace, and occurrence allocations. The receivable continues from 60 paid units to full payment. The grant retains its contingent 100 units across a semantic change. This read adapter does not deactivate the source engine. A deployed handover must realize (M3)–(M4), the family adapters, authenticated provider semantics, and the institution’s actual migration authority.

7.4 Durable execution through a changed representation

The carriage theorem specifies the required agreement between representations. To execute payments after the change, a concrete service must enforce that agreement on every write. The resolved-duty construction does this by keeping one original entitlement ledger. A successor position acts as a payment alias, an address for selected portions of an existing duty.

A representation becomes operational when a payment addressed to it changes the original duty. This requires a common write authority for the entitlement ledger and the portion journal. Comparing two independently maintained balances does not supply that authority.

Here the construction specializes to a finite cohort whose duties have already resolved into payable amounts. Adoption places that original ledger and its portion journal under one write authority. The payable and discharged labels used here are the corresponding part of the more general journal; future unresolved obligations retain their original lifecycle.

Consider a finite cohort of resolved duties in an executable payoff ledger. Each duty retains its original program, constituting identity, directed parties, governing terms, and maturity. Fix a positive rational quantum for each asset. The canonical portion journal measures each duty in those quanta. Its labels record current payable and discharged portions. Historical allocations and their later authorized reopenings remain separate records.

A successor program executes on its own temporary ledger with the declared inputs. Each resolved output names portions of the original cohort. The admission checks every emitted duty, the exact partition, and the matching economic fields. It retains the successor checkpoint and its evidence. The resulting output names are payment aliases for original duties. The temporary duties remain outside the active entitlement ledger.

An alias payment selects payable portions owned by that alias. The service then invokes the original ledger’s allocation operation for their total. One transaction commits the allocation, its physical support, and the selected portions. Ordinary payments and authorized reopenings use the same write mediator. An outstanding command retains its original target and recipient. Its eventual outcome updates the original duty through this common authority.

The reference service adopts the existing SQLite store under one write transaction. Its successor schema retains original program checkpoints, ordered ledger records, command outcomes, and authentication data. The old client checks the schema within its own write transaction. It therefore rejects a write after adoption. A write committed first changes the base and invalidates the prepared adoption. The successor service continues original requests under their original program identities.

An executable coupon illustrates the distinction. Of a 30-unit duty, 20 units are discharged. A successor program produces a paid 20-unit alias and a payable 10-unit alias. Payments of five units from remaining physical support and five units from another credit complete the original duty. A second program coalesces the aliases into one discharged position. The original ledger contains the same duty throughout. Another unfinished coupon request then resolves under its original program.

The service executes this trace through the payoff evaluator and entitlement ledger. It retains a partially settled operation’s target, source digest, command, and reservation across adoption. Recovery retains the same committed outcome when the payment response is lost. The interval construction below represents large quantities while preserving these allocation histories.

This construction covers resolved duties with fungible canonical portions. It leaves correction duties as distinct directed obligations. A later original-program resolution retains its ordinary lifecycle outside the adopted cohort. Transfer of unresolved computations requires a further constructor. Section 7.6 supplies one for programs with the same instructions and rational position partitions. Arbitrary future-input equivalence remains outside these constructions. Actual migration authority, provider facts, and exclusion between independent stores remain institutional premises. The local transaction establishes the common write authority within the declared store.

7.5 Exact interval representation

The resolved-duty construction assigns a coordinate to each smallest permitted quantity, or quantum. Enumerating those coordinates makes storage grow with monetary quantity. Intervals can store consecutive portions together, provided they retain the selections and history used by later payments and returns.

Consider four units paid by one allocation. Two units are returned and become payable again under the governing rule. A replacement payment discharges those two units. A further return against the first allocation must concern its remaining discharge; it cannot reopen the replacement payment’s units.

Number the original units from zero through three and call the allocations a and b. A return against a reopens cells 0 and 1, which b then discharges again. A further return of one cell against a must reopen cell 2. The current payable balance alone cannot determine that choice.

An alias row is the ordered list of portions addressed by one successor position. A triple names a duty and the beginning and excluded endpoint of one consecutive portion. Thus a partial payment can depend on the row’s order even when two rows cover the same portions.

Order also matters before a payment. When all four cells are payable, the alias row ((d,2,4),(d,0,2)) first selects cell (d,2). Sorting its intervals first selects (d,0) instead. The rows have equal support and quantity, but different partial-payment behavior. We therefore distinguish ordered sequences from membership sets throughout the construction.

A membership set has sorted disjoint maximal runs within each duty. An ordered list retains the order of its entries. Only consecutive entries (d,a,b),(d,b,c) can coalesce without changing their expansion. Duplicate portions are rejected before normalization can conceal their overlap. Equal indices belonging to different duties remain distinct coordinates.

The following operations act on ordered lists. Intersection and difference first express the mask as a sorted disjoint union. Within each source run, they split at the mask endpoints and retain the appropriate successive subintervals. They visit source runs in their original order. The prefix operation visits runs in order and consumes their lengths until the requested count is reached. Its last run is shortened when necessary.

A membership mask specifies which cells qualify, without prescribing their order. Filtering an alias by that mask must preserve the alias’s order. The lemma states this fact and then identifies a partial payment with a prefix of the resulting sequence. Square brackets on the right denote order-preserving sequence selection or a prefix.

For each duty, a label partition covers [0,q_d) with disjoint intervals marked \mathsf{Payable} or \mathsf{Discharged}. Relabeling splits at the selected endpoints and changes precisely those portions. Adjacent intervals with equal labels then coalesce. An alias installation retains the complete, disjoint coverage of every duty and each row’s order. It checks the parties, governing terms, quantum, maturity, context, and all other required economic fields. The quantity of each label in an alias is the length of their intersection, multiplied by the quantum. Finite additivity therefore preserves the aggregate quantity of each duty and label across all aliases. The exact economic bindings preserve the corresponding rights classes.

A duty label answers whether a portion is currently paid. A restoration record answers which earlier allocation has had that portion returned. The four-unit example requires both answers: a portion restored from the first allocation can now be discharged by the replacement allocation.

For allocation a, retain its ordered original sequence A_a and its own restored support R_a. Its current discharge support is L_a=S(A_a)\setminus R_a. Historical supports S(A_a) can overlap after a return and replacement payment. The supports L_a must remain pairwise disjoint. Their disjoint union is the discharged support, whose complement is payable. In addition, R_a\subseteq S(A_a) for each allocation.

For the four-cell example, the original sequence of a is (0,1,2,3). After its first return, R_a=\{0,1\} and L_a=\{2,3\}. The replacement allocation b has original sequence (0,1) and empty restored support. Its current discharge is L_b=\{0,1\}. A further return against a selects the first cell of its remaining sequence, namely cell 2, while retaining the discharge recorded by b.

Alias rows determine selection order, and labels determine current payable status. Allocation sequences and restoration records determine which earlier payment a return can reopen. The separate physical support below records which portions of an external credit have already been consumed.

Adopting a ledger assigns portion coordinates where it previously retained only quantities and allocation history. Converting an existing cell state instead preserves its coordinates and order. The refinement proof treats these two entry cases separately.

The adoption rule constructs these supports from the existing ledger in its retained allocation order. For an allocation with total t and restored quantity r, choose t-r cells from the remaining free support. Then choose r historical cells from the duty domain outside that allocation’s selected active support. The allocation stores the active sequence followed by this restored sequence. Only its active support is removed from the free support. Prefixes and differences perform both selections without enumerating their cells. Thus active discharges remain distinct while historical restoration coordinates can be reused by later allocations.

A new payment selects a prefix from the alias’s payable support. It creates an allocation with that ordered sequence and empty restored support. A return against allocation a instead selects T=\operatorname{take}(\operatorname{subtract}(A_a,R_a),k). It adds S(T) to R_a and marks those cells payable. The original ledger’s return evidence and governing-rule checks authorize this change. An interval membership test supplies no such authority.

Physical credit has a separate coordinate (o,j), with 1\leq j\leq Q_o. Here o identifies the canonical external occurrence admitted by the original ledger. A legal origin, beneficiary, or payment alias does not change that occurrence identity. Consumed physical supports remain disjoint within each occurrence. Their union remains consumed after a duty reopens. A replacement payment therefore requires other unconsumed physical support and its admitted evidence. Explicit physical selections retain their supplied order and pass extent and overlap checks.

For an alias spanning several duties, selected cells are grouped by duty in first-occurrence order. Each group retains its internal selection order. The physical sequence is then split by the successive group quantities. This rule fixes the allocation pairing when an alias revisits a duty later in its ordered row.

The comparison cell construction uses the stated transition rules on arbitrary finite cell sets. It imposes no additional bound on the number of cells. It supplies a mathematical interpretation, while the interval representation executes without enumerating that interpretation.

Refinement means that expanding the stored intervals gives the same execution as representing every cell individually. The proof uses ordered selection for payments and returns, and disjoint supports for current discharges. Physical payment portions have a separate consumption history, which reopening a duty must preserve.

The decoding theorem compares economic state and ordered selections. A new receipt can encode a selected sequence as intervals. Its serialized bytes then differ from a receipt that lists the individual cells. Converting the store preserves previously committed receipt objects and their request bindings exactly. Different orders of physical selection remain different requests even when their supports agree. Old writers check the active schema within their own transaction, so that the adopted store retains one write authority.

7.6 Position partitions across future observations

A coupon can depend on observations that arrive after its positions change. Its present balance alone does not carry that unfinished computation. The following constructor retains the program’s instructions and changes its position partition. It preserves historical dependencies and later requests, including requests beyond those pending at admission.

The source program continues against the current entitlement ledger. A second evaluator runs the successor program against a private ledger. Both receive the same admitted requests and observation refinements. Either may finish first.

A source duty can receive payment while the successor remains suspended. Once both evaluators resolve the instance, their paired results give a correspondence with original duties. The conditions below determine when it can also become a payment alias.

For each source and successor position, interval additivity gives \sum_j a_{ij}=q_i,\qquad \sum_i a_{ij}=r_j. \tag{1} Thus several source positions can regroup into several successor positions. The certificate preserves their individual original identities through the intersections. Within this construction, equality of compiled expressions supplies the required agreement of numerical meanings. Authenticity of the admitted program objects remains a premise. A digest check alone does not validate hostile changes to their internal structure.

8.1 Fixed income

A fixed-income family stores dated principal and coupon obligations. Events include issue, transfer, record-date capture, coupon determination, payment, amendment, default, and redemption. The obligation projection is a dated multiset. A payment delta removes only the obligation supported by final settlement evidence. An amendment needs the authority named by the instrument. A transfer needs the holder rule that applies at the event time.

ACTUS already gives a detailed algorithmic account of contract events and cash flows [1]. The present interface can consume such an event model as a family. It does not replace it.

8.2 Parametric insurance

An insurance family stores coverage, trigger source, limit, deductible, premium status, notice conditions, assessment state, and payment state. A trigger attestation can move the claim into assessment. It cannot itself establish coverage, satisfy notice, or make payment final. The family invariant caps aggregate final payments at the covered limit after deductible and permitted reinstatement rules.

The common engine sees only that the family transition and laws passed. It does not reduce an insurance claim to a binary token.

8.3 Trade receivables

A receivable family stores seller, buyer, invoice, acceptance status, defences, assignment status, maturity, and collections. Assignment changes the holder of a right. It does not remove a buyer defence unless applicable law and the instrument permit that effect. Collection reduces the outstanding obligation only on the family’s accepted finality evidence.

This family shows why a generic holder field is not enough. Family-private state records whom the engine treats as the current holder and which defences and assignment limits remain represented.

8.4 Options

An option family stores writer, holder, underlying, strike, exercise window, style, payoff rule, collateral rule, and settlement route. Exercise is a family event. The payoff language can describe the amount [28]. The lifecycle interface decides whether exercise was authorized and timely, whether settlement evidence is strong enough, and what obligation remains.

The same request and receipt structure can surround each of these state models. Their transition relations must still establish the authority, accounting, consumption, and evidence laws for those particular obligations.

Financial contract languages.

Peyton Jones, Eber, and Seward define compositional financial contracts and a denotational valuation semantics [28]. Findel gives a declarative derivative language for blockchain execution [8]. Marlowe gives executable financial agreements with a small semantics [26]. These systems establish that product terms and payoffs can be expressed compositionally. The present work starts after expression. It models authority, lifecycle state, non-acceptance, external finality, and reliance around the family semantics.

LexiFi’s Contract Description Language also gives self-contained, compositional descriptions of financial contracts. It keeps the mapping from abstract to actual parties outside the language and treats extraordinary events outside nominal contract behavior [19]. Those boundaries agree with the separation here between family semantics, external facts, and the engine envelope.

Algorithmic standards.

ACTUS Technical Specification v1.1 represents contract types through state variables, scheduled events, state-transition functions, and payoff functions [1]. The ISDA Common Domain Model Design Definition v1.0 standardizes product and lifecycle concepts and describes parametric processing [10]. Both are close prior art. This paper does not claim a wider product taxonomy.

FpML is ISDA’s XML business-information exchange standard for derivatives. Its Version 5.13 recommendation covers pre-trade, trade, post-trade, and lifecycle processes [9]. It can carry messages around a family implementation; it does not supply the serialized safety contract proved here.

The FINOS Common Domain Model now maintains a modular representation of financial products, trades, and lifecycle events, with mappings and executable logic [11]. Its event vocabulary can supply family semantics. The joint contract studied here instead asks which external facts, occurrence identities, commit-time checks, and reliance limits a serialized evaluator must bind around those semantics.

Concurrency and idempotence.

Optimistic concurrency control, linearizability, and idempotent message handling are established techniques [16, 13, 12]. The revision, nonce, and occurrence-key mechanisms in this paper are applications of those techniques. The contribution is their typed coupling to W_F, C_F, effect-indexed evidence, and the family laws. It is not the invention of nonces, optimistic validation, or linearizable storage.

Payment-message identity and status.

ISO 20022’s pacs.002 message reports a positive, negative, or pending status for an earlier payment instruction [14]. SWIFT’s 2026 cover-payment guideline requires the pacs.009 COV to carry the same Universal End-to-End Transaction Reference as its underlying pacs.008; the two messages describe the same transaction [32]. Both support the separation used here: a message identifier identifies an assertion, while a stable external reference can identify the occurrence described by several assertions. Neither standard by itself proves that the occurrence is final under the relevant route.

Ledger and workflow platforms.

Corda combines agreement states, contract code, required signatures, time windows, external data, consuming transitions, and a uniqueness service [2]. Daml combines template-private state, consuming choices, authorization, delegation, and compositional multi-party workflows [3]. Hyperledger Fabric validates read-set key versions against committed state before applying writes [4]. These systems already establish important parts of authorization, single consumption, and stale-state rejection. The present paper does not claim those mechanisms separately. It states one joint interface between family-private claim semantics and a serialized engine, including commit-time status, effect-key support, effect-indexed settlement evidence, and bounded reliance metadata.

Credential status.

The W3C Bitstring Status List distinguishes status purposes such as revocation and suspension and requires verifiers to authenticate status-list credentials [33]. It confirms that issuer status is a separate, time-sensitive input. This paper uses a more general authenticated snapshot abstraction because authority, provider, and rule-policy status need not be verifiable credentials.

Smart legal contracts.

Clack, Bakshi, and Braine distinguish operational code from legal agreement and enforcement [6]. Their separation is essential here. The external-fact interface prevents an operational engine from presenting its own result as legal authority.

Typestate and proof-carrying execution.

Typestate systems make permitted operations depend on current state [31]. Proof-carrying code lets a consumer check a producer-supplied safety argument against a fixed policy [27]. The transition envelope applies the same broad discipline to a claim lifecycle. The family supplies the policy and state relation. The evaluator checks the relation before mutation.

Event logs and state-machine replication.

Deterministic state-machine replication requires replicas to apply the same ordered operations under the same semantics [17]. The audit replay theorem here is elementary and conditional. Its purpose is to enumerate the content, time, status, nonce, and evidence inputs that must be fixed when the state machine consumes institutionally sourced facts.

11.1 Legal adequacy

The family authority predicate can be wrong. A rule translation can omit a statute or misread a contract. A status service can omit a revocation or authenticate the wrong issuer. Formal preservation under wrong content or a false snapshot is still wrong. Legal adequacy and status-source governance need independent validation.

11.2 Realizing the engine assumptions

Canonical encoding, registry immutability, trusted time, and truthful source evidence remain explicit premises. Section 4.2 constructs a prepared transaction for current recorded heads and joint writes. Section 5.2 supplies its occurrence-attribution and funding contracts. A concrete implementation must establish refinement, including recovery, expiry, dependency completeness, and concurrent reservation. Its evidence must include linearizability checks, failure-injection tests, and exact cryptographic and wire specifications. The source-head result does not establish legal authority at a later external use stage.

11.3 Insolvency and priority

Outstanding-obligation accounting does not determine priority in insolvency. It also does not create perfection, property rights, set-off, or close-out netting. A family can record those asserted states only through accepted legal evidence. Their effect remains jurisdiction specific. For example, sections 238–241 of the Insolvency Act 1986 provide statutory consequences for transactions at an undervalue and preferences, including orders that restore the position [15]. An earlier engine receipt cannot displace that power.

11.4 Privacy

Section 6.1 separates private full replay from public references and selective disclosure. Encryption protects stored content under its key and access assumptions. An authorized recipient can retain disclosed plaintext. A deployment must establish its actual access grants, retention duties, and managed deletion scope.

11.5 Cross-claim netting

The original lifecycle theorem applies to one claim trace. Section 5.2 establishes attribution conservation under its joint-commit and evidence premises. It separates attribution from current funding capacity. General netting additionally requires the joint obligation transformer, exposure maps, authority, and legal basis in Section 5.1. Each netting construction must prove those family-specific requirements. Attribution conservation alone establishes neither novation, close-out netting, nor legal extinction of an obligation.

11.6 Family migration

Section 7 establishes preservation under authorized semantic carriage, including splits, coalescence, and delayed outcomes. Novation, restructuring, and conversion may change economic rights. Their family-specific transformations need authority, explicit lineage, and their own preservation laws. The carriage theorem preserves their recorded consequences without claiming that these different transformations are lossless changes of meaning.

11.7 Liveness

Section 3.6 establishes progress after finite sufficient cure under explicit availability, stability, and fairness premises. A provider action, tribunal decision, or discretionary judgment retains its named external owner. The engine preserves awaiting obligations while that input remains unresolved. A changing current-source head can require reevaluation. The remote protocol’s recovery and timing assumptions determine progress there.