A Server-Side Model for Gating Agent-Initiated Human-Sourced Asynchronous HTTP Tasks on Payment or Entitlement

1.1. Document Status and Maturity of the Cited Protocols

The intended status of this document is Informational. It is an analytical description of a model, and it deliberately contains no requirements language; BCP 14 key words are not used, and nothing in this document is a conformance target. It defines no new protocol elements and requests no registrations.¶

The cited mechanisms have different maturity and governance models that affect implementation risk:¶

• [I-D.ryan-httpauth-payment] is an individual-submission Internet-Draft. As of July 2026 it stands at revision -01 (published 18 March 2026), expires on 19 September 2026, and has no IETF working-group adoption; it is not an IETF standard.¶

• [I-D.ietf-httpapi-idempotency-key-header] was adopted by the IETF HTTPAPI Working Group and has expired: its latest revision, -07, was published on 15 October 2025 and expired in April 2026. It is cited in this document as provenance for an established pattern, not as a settled standard.¶

• MPP [MPP-STRIPE] [MPP-SPECS] is vendor documentation and a vendor-maintained specification (maintained by Tempo Labs and Stripe, launched 18 March 2026). Its maintainers describe it as an open standard; it is not the product of a standards body.¶

• x402 [X402] is an independent protocol created by Coinbase. The Linux Foundation's 14 July 2026 release [X402-LF] announced the operational launch of the x402 Foundation and the completed contribution of the x402 protocol by Coinbase, and records that the Foundation's formation had been announced on 2 April 2026.¶

• AP2 was announced by Google on 16 September 2025 [AP2]; its specification stands at v0.2, a pre-1.0 document [AP2-SPEC].¶

• The Model Context Protocol (MCP) [MCP] is an application-layer tool-invocation specification, cited here only for product discovery and invocation context and not as part of the settlement layer. This document cites protocol version 2025-11-25; it is not an IETF standard.¶

3.1. The Layer Map

The stack runs top to bottom (Figure 1). The access layer can expose Representational State Transfer (REST) APIs. A request descends through access, decision, and payment/settlement layers before crossing the gate. The artefact and delivery receipt return to the caller; the operator retains the audit record. Throughout this document, the operator-controlled audit record comprises L and Omega; verify_Omega checks Omega only and does not verify or bind L.¶

+---------------------------------------------------------------+
| Client / client agent                                         |
|   holds mandate M = <c, a, aud, b, sigma_auth, d_lim, chi,    |
|   epsilon> for delegated spend                                |
+------------------------------+--------------------------------+
                               v
+---------------------------------------------------------------+
| Product interface (access layer)                              |
|   tool-invocation surface (agent-facing) . REST/domain APIs   |
|   (system of record)                                          |
|   carries no money, decides no price; routes request inward   |
+------------------------------+--------------------------------+
                               v
+---------------------------------------------------------------+
| Decision layer                                                |
|   pricing price(p, rho) -> Money, frozen at quote time .      |
|   authority check authorises(M, q) . entitlement resolution   |
|   . attaches R to every quote; derives the 402 challenge      |
|   from R only where a fresh machine payment is needed         |
+------------------------------+--------------------------------+
                               v
+---------------------------------------------------------------+
| Payment/settlement abstraction                                |
|   one payment-or-entitlement gate, many settlement methods:   |
|   402 challenge-credential-receipt on top; the settlement     |
|   method S in Settle selected beneath                         |
+------------------------------+--------------------------------+
                               v
+===============================================================+
| THE GATE g*  (task state pending_payment_or_plan_check)       |
|   validate(R, S, M) <=> credentialValid AND authorises        |
|                         AND current AND fresh AND NOT expired |
|   true => enter region Phi     false => refuse                |
+==============================+================================+
                               v
+---------------------------------------------------------------+
| Fulfilment system (region Phi)                                |
|   async task engine (state machine) . contributor sourcing    |
|   against chi . append-only ledger L .                        |
|   partial F: ValidatedReq -> Artefact                         |
+------------------------------+--------------------------------+
                               v
+---------------------------------------------------------------+
| Result + receipt + audit                                      |
|   delivered artefact . receipt Omega (verify_Omega checkable) |
|   . audit record . contributor payment outside this model     |
+---------------------------------------------------------------+

The gate g* is the point after which the modelled fulfilment side effects may begin. Everything above it prepares quotation, authorisation, and settlement evidence; everything below it is the fulfilment region Phi.¶

3.2. Protocol Placement

The layer map assigns each cited mechanism to the function it provides. A tool-invocation protocol such as MCP [MCP] makes a product discoverable and callable by an agent; AP2-style mandates record who authorised what; an asynchronous task engine fulfils; receipts and audit make the outcome checkable against operator-controlled records. In this model, none of these layers is treated as the settlement layer. Between an agent-readable product surface and paid access sits the payment/settlement layer that the access, authority, and fulfilment layers do not themselves provide: the point at which a machine presents a valid payment, the server validates it, and only then does fulfilment begin.¶

The model places the cited protocols as follows:¶

The "Payment" HTTP authentication scheme and MPP.

The wire mechanism is the "Payment" HTTP authentication scheme of [I-D.ryan-httpauth-payment]: the server returns 402 Payment Required carrying a "WWW-Authenticate: Payment" challenge; the client pays out of band and retries with an "Authorization: Payment" credential; on success the response can carry the scheme's "Payment-Receipt" header, a payment receipt distinct from the delivery receipt Omega; the scheme pairs that header with "Cache-Control: private". MPP is the protocol built over that scheme [MPP-STRIPE]. In the model this pair occupies exactly one tier: the machine-payment requirement inside the decision layer, realised over a settlement-flexible abstraction. It replaces none of the other tiers. The wire challenge is derived from and bound to the payment requirement R, supplying the parameters that the scheme requires, and the credential it elicits is what the gate validates.¶

x402.

x402 [X402] demonstrated the 402 paid-resource pattern in practice: its settlement is crypto-native, using stablecoin transfers settled on-chain. Verification and settlement are performed either directly by the resource server or through an optional facilitator service, which may be managed, self-hosted, or run in process. In the model that binding makes x402 one settlement path among several (a stablecoin settlement method in Settle), rather than the shape of the gate itself. Its governance transition to the x402 Foundation under the Linux Foundation, announced 2 April 2026, completed with the x402 Foundation's operational launch on 14 July 2026 [X402-LF].¶

AP2.

AP2 [AP2] [AP2-SPEC] supplies the delegated-authority layer: signed Checkout and Payment Mandates intended to provide tamper-evident evidence of recorded user instructions within AP2's trust model, with a human-not-present form carrying price limits, timing, and conditions, and a human-present form binding exact items and price. (The 2025 announcement named these Intent and Cart Mandates; the v0.2 specification restructures them as Checkout and Payment Mandates. This document uses the human-not-present versus human-present distinction without asserting term-for-term equivalence with the current specification.) In the model the mandate M is one input to the gate, alongside R. Authority is necessary but not sufficient: a validated mandate provides evidence of the authority represented in its signed fields, but does not price the work, move money, source a contributor, or deliver a result.¶

Adjacent layers.

The access layer (tool invocation plus REST and domain APIs backed by the system of record) standardises how an agent calls the product and carries no semantics for payment, delegated authority, pricing, or settlement. Inter-agent protocols and commerce-channel wrappers sit at the edges, relevant only where a coordinating agent or an external commerce surface is operated. These layers are named here only to fix what the gate does not replace.¶

3.3. Scope of the Gate

Table 1 separates the gate from the access, authority, pricing, settlement, and fulfilment responsibilities around it.¶

3.4. The Gated Exchange

On the wire, the model's transaction is a seven-step exchange gated on a single validation.¶

1. Request. The agent calls a product or quote endpoint, presenting M and an idempotency key k that remains stable for every retry of this logical request. On the machine-payment path the server records only the challenge state for that request: k, the authenticated client, a collision-resistant digest of a canonical encoding of all processing-relevant request fields, and the resulting quote. That record is not a task record, and no task identifier exists before the gate commit; reuse of k with different data is rejected.¶

2. Quote plus requirement. The pricing engine freezes the price and the decision layer emits the quote q with its requirement R. If a fresh machine payment is needed, the server returns 402 Payment Required carrying a method-specific "WWW-Authenticate: Payment" challenge derived from and bound to R, which supplies the parameters that the scheme requires; R itself remains the model's internal, settlement-method-neutral requirement. If an entitlement may cover q, the server returns no 402, and the client presents entitlement evidence in step 3 for validation and atomic reservation at the gate in step 5.¶

3. Obtain payment evidence. The agent obtains evidence accepted by the selected payment path. The task record distinguishes transfer, capture, authorisation for later capture, and entitlement coverage; these states are not interchangeable.¶

4. Retry with credential. The agent retries the original request, carrying the credential in an "Authorization: Payment" header and its idempotency key.¶

5. Validate (the gate g*). The server evaluates validate(R, S, M); the nonce binds the credential to this specific challenge, and a stale or expired challenge fails closed.¶

6. Activate and return a handle. On true, and only on true, the task engine enters Phi; the server returns a task identifier.¶

7. Receipt and audit. The gate commit of step 6 durably recorded the settlement reference rho_pay before entry to Phi; the server returns that reference, and constructs and returns the artefact-bound Omega at delivery.¶

Steps 2, 4, and 5 establish the challenge, retry, and validation sequence: the challenge in step 2 names the price and the nonce, the retry in step 4 satisfies exactly that challenge, and the gate in step 5 admits the request to Phi only on full validation. Because eta is bound into R and re-presented in the credential, a credential cannot be replayed against a different challenge; the separate idempotency-key binding supports server-side idempotency (Section 7.2).¶

4.1. Quotes and Pricing

At quote creation, the decision layer returns a price, scope descriptor, and deadline. The quote q = <a, p, rho, m, sigma, d, R> records the requesting agent so authority can be checked against it. C1 (Section 6.1) freezes m(q), the scope, and the deadline for the life of that quote; a later quote may reflect different inputs or pricing state.¶

4.2. Mandates and Authority

Cumulative committed spend under a mandate is spent(M), the sum in currency(cap(M)) of m(q) over quotes committed under M, with the empty sum equal to zero in that currency; spent(M) is monotonic, so refunds and credits do not reduce it or restore mandate capacity, and replacement capacity requires a new or amended mandate outside this model. A quote is committed when its task crosses the gate. The accessors read tuple components by position: agent(q), scp(q), dl(q), m(q), and R(q) read a, sigma, d, m, and R of q; issuer(M), holder(M), audience(M), cap(M), sigma_auth(M), and d_lim(M) read c, a, aud, b, sigma_auth, and d_lim of M; payee(R), eta(R), and t_exp(R) read payee, eta, and t_exp of R. The predicate requesterAuthenticatedAs(x) holds when the authenticated client identity is x. The budget test is total: withinBudget(M, q) is false when currency(m(q)) differs from currency(cap(M)), and is otherwise the truth value of spent(M) + m(q) <= cap(M) evaluated in that currency. Authority alone is:¶

authorises(M, q) <=>  requesterAuthenticatedAs(holder(M))
                  AND holder(M) = agent(q)
                  AND payee(R(q)) is in audience(M)
                  AND scp(q) is in sigma_auth(M)
                  AND withinBudget(M, q)
                  AND current_time < dl(q)
                  AND dl(q) <= d_lim(M)
                  AND active(M, current_time)

Authority and escalation are two separate predicates, both evaluated at the state pending_authority, with escalation taking precedence. For a mandate M, chi_M(e) evaluates its contributor-criteria predicate for contributor e, and epsilon_M(q) evaluates its escalation predicate for quote q. The predicate epsilon_M(q) is not a conjunct of authorises and is checked first. When epsilon_M(q) is true the operator records re-approval bound to M, q, the authenticated approver, and the approval time before the task can reach the gate; the task does not advance automatically (C6). The contributor-criteria predicate chi_M is likewise not part of authority; it constrains fulfilment through the ledger invariant (C4), and a chi_M failure surfaces inside the fulfilment region as the no-qualifying-contributor transition, not as an authority failure.¶

4.3. Payment Requirement, Settlement, and Validation

The requirement R is issued at quote time and is settlement-method-neutral. The map from quotes to requirements is total and injective: it issues exactly one R per quote, and no two quotes share a requirement. Therefore q(R) denotes the unique quote whose requirement is R. How money moves is a separate concern: a settlement method S realises R by producing the credential realise(S, R). The settlement method affects validation through realise: the same R admits different credentials under different settlement methods, and a method that cannot produce a valid credential fails the credential-validity conjunct. R is settlement-method-neutral at the model boundary; for a particular wire exchange the selected method determines the challenge and credential that realise it. On the entitlement and credit paths the evidence is not self-authenticating, so the gate resolves it to an account the authenticated client may draw on under M; presenting another principal's identifier fails the credential-validity conjunct.¶

The gate predicate conjoins credential validity, authority, active-requirement status, nonce freshness, and temporal validity:¶

validate(R, S, M) <=>  credentialValid(realise(S, R), R)
                   AND authorises(M, q(R))
                   AND current(R, q(R))
                   AND fresh(eta(R))
                   AND NOT expired(R)

Validation fails closed on any conjunct, and the wire response distinguishes the class of failure. A payment credential that fails verification follows the 402 retry path. A credential that verifies but does not satisfy the mandate (over budget, outside the authorised scope, past the authority expiry, or presented by the wrong holder) is refused without a fresh payment challenge; under [I-D.ryan-httpauth-payment] that refusal is a 403 response. Both outcomes fail closed and admit no fulfilment side effect. A successful validation consumes the nonce atomically: after consume(eta(R)), fresh(eta(R)) is false. Nonce consumption makes the requirement non-repeatable; the task transition and C7 prevent a second gate crossing. The authorises conjunct at settlement time re-asserts authority already established at pending_authority; it is a defensive re-check because budget availability and mandate status may have changed in the interim, not a second authority gate. Escalation is resolved earlier, at pending_authority; contributor criteria are enforced inside fulfilment; neither is checked at this gate.¶

4.4. Fulfilment, Ledger, and Receipt

ValidatedReq is the set of (q, S, M) whose requirement passed the gate, and F denotes fulfilment processing for a validated request; its artefact and ledger effects are represented by task-state transitions. The restriction of F to gated requests is an implementation invariant, which is what ties the safety argument of Section 7.1 to a successful validation.¶

The receipt Omega = <M, rho_pay, taskId, hashAlg, artefactHash, t, mode> binds, in one verifiable record, who authorised (M), what was paid (rho_pay), which task (taskId), and exactly which artefact (artefactHash, computed over the exact delivered bytes under the algorithm named by hashAlg). The mode field records the settlement mode as executed, including test or mock modes in non-production deployments; when an entitlement satisfied the gate, mode records the entitlement path (for example, package drawdown); the receipt structure and verify_Omega semantics are unchanged. The receipt gives the operator a structured consistency check across the delivered artefact and its own records; it does not provide operator-independent evidence.¶

5.1. States

The start state is q0 = draft. Term = {cancelled, failed, credited_or_refunded}. delivered is a completed fulfilment state with one possible transition, on an upheld dispute, to credited_or_refunded. credited_or_refunded records a compensation obligation and the remedy selected against rho_pay: a refund returns funds, while a credit leaves the charge standing and grants offsetting value. It does not assert that the settlement-side remedy succeeded; a separate settlement result records the outcome, and a compensating receipt written against rho_pay links the obligation and its result (Section 9).¶

5.2. Level Function, Gate, and Fulfilment Region

A pipeline-position map orders the happy path and isolates the gate. The level function is defined on the eleven pipeline (non-exception) states only; the three exception terminals carry no level and are not in Phi:¶

draft 0 . quoted 1 . accepted 2 . pending_authority 3 . g* 4 .
pending_expert_match 5 . awaiting_expert_input 6 .
needs_client_clarification 6 . in_review 7 . ready 8 . delivered 9

The gate is g* = pending_payment_or_plan_check, at level 4. The fulfilment region is Phi = {states of level 5 or above} = {pending_expert_match, awaiting_expert_input, needs_client_clarification, in_review, ready, delivered}. The expensive, not freely reversible side effects of fulfilment (committing contributor sourcing, soliciting and recording paid contributions, generating the artefact) occur only on transitions entering or internal to Phi.¶

Property 1 relies on one structural condition, that the only edge from outside Phi into Phi is the gate edge:¶

pending_payment_or_plan_check
    --[ validate(R, S, M) = true ]-->  pending_expert_match

Authority resolution and escalation happen strictly before the gate, at pending_authority, and resolve only to the gate state on approval, to cancelled on refusal or decline when no capture is recorded, or to credited_or_refunded on refusal or decline when a capture is recorded; none of these exits enters Phi. The mid-fulfilment state needs_client_clarification is reachable only from within Phi (from awaiting_expert_input): an intra-Phi edge, not an entry.¶

5.3. Transitions

Guards are necessary preconditions and, for each state, mutually exclusive under the convention that expiry is evaluated before client events and events are processed one at a time. The deadline rows apply only from quoted onward, since draft has no quote and therefore no dl(q). epsilon, authorises, and chi_M are evaluated on the in-force (M, q).¶

Three cross-cutting notes. First, the terminal failed is reserved for an unrecoverable system fault, which can terminate any task that has not reached delivered, cancelled, or credited_or_refunded; this family of fault edges is omitted from the per-state rows for readability. A fault edge from a state in Phi targets credited_or_refunded, because the gate commit has already recorded an accepted payment, credit, or entitlement reference that requires reconciliation. Before the gate, a fault edge targets failed when no capture is recorded, and targets credited_or_refunded when a capture is recorded. Both failed and credited_or_refunded are outside Phi, and the model does not represent whether the later settlement-side refund, credit, or entitlement reconciliation itself succeeds. Second, a no-qualifying-contributor outcome is a post-gate business outcome and routes to credited_or_refunded (the client has paid; the charge is reconciled), not to failed. Third, validation failure before funds move cancels the task. If the credential records funds already captured, failure routes to credited_or_refunded and reconciles the settlement against rho_pay. A fresh wire challenge ([I-D.ryan-httpauth-payment]) begins a new payment attempt; the wire scheme does not tie that attempt to this model's task machine. In this model the key k remains claimed by the terminated request's challenge record or its tombstone (C8), so a new attempt proceeds as a new activation under a fresh idempotency key against a new quote.¶

   states at or before the gate: quotation, authorisation, and
   payment validation (no fulfilment effects)

 draft --> quoted --> accepted --> pending_authority
   |          |                      |           |
   | abandon  | reject /    refused/ |           | authorised /
   |          | expired(R)  declined |           | re-approved
   v          v                      v           v
 cancelled <--+----------------------+   +-----------------+
   ^                                     | g* = pending_   |
   |   validate = false, no capture      | payment_or_     |
   +-------------------------------------+ plan_check      |
                                         +--------+--------+
                                                  |
                                 validate(R, S, M) = true
                                 (the only edge from outside
                                  Phi into Phi)
 =================================================|===========
   fulfilment region Phi (level >= 5)             |
 .    +-------------------------------------------+         .
 .    v                                                     .
 .  pending_expert_match --- no qualifying contributor ---+ .
 .    | contributor e with chi_M(e) = true found          | .
 .    v                                                   | .
 .  awaiting_expert_input <--+  (self-loop: contribution  | .
 .    |    |     |___________|   appended to L)           | .
 .    |    |                                              | .
 .    |    | clarification required                       | .
 .    |    v                                              | .
 .    |  needs_client_clarification                       | .
 .    |    |  answer received: back to                    | .
 .    |    |  awaiting_expert_input                       | .
 .    |    |  timeout / withdraw ---------------------+   | .
 .    | inputs sufficient                             |   | .
 .    v                                               v   v .
 .  in_review --- unrecoverable defect ---->  credited_or_  .
 .    | review passed                         refunded      .
 .    v                                          ^          .
 .  ready --- Omega constructed and written --+  |          .
 .                                            v  | dispute  .
 .                                    delivered -+ upheld   .
 .                                                          .
 ............................................................

A system fault can terminate any task that has not reached delivered, cancelled, or credited_or_refunded; the resulting edge targets failed only before the gate with no capture recorded, and targets credited_or_refunded otherwise. Both are outside Phi. credited_or_refunded is drawn inside the frame only for layout. The fault edges, the dl(q) deadline edges, and the edges to credited_or_refunded on a recorded capture (from quoted on rejection or requirement expiry, from g* on validate = false, and from pending_authority on an authority failure or declined escalation) are omitted from the figure.¶

5.4. Activation Requests, Keys, and Nonces

The gate transition is performed by an activation request: the call that presents (R, S, M) for validation. Each activation request carries an idempotency key k, client-supplied, stable across retries of the same logical request, and namespaced per client. The task store binds k to the task by an atomic compare-and-set CAS(k: bottom -> taskId) that succeeds at most once per key (C8), performed as part of the successful gate commit. On the 402 path the pre-gate record carrying k is challenge state rather than a task record; the credential retry carries the same k and is routed to that record. The key k identifies the logical request; the nonce eta identifies the issued challenge. The gate transition, at most one per task, atomically binds k to the new taskId, confirms it against the canonical-request digest recorded with the challenge, consumes eta(R), commits spent(M), atomically reserves or consumes any finite entitlement, records the accepted payment, credit, or entitlement reference, and enters Phi. A request carrying an existing k is first routed to the record bound to it, the challenge record before the gate commit and the task afterwards; only a completed gate commit bypasses revalidation. If these effects span stores, the implementation requires a documented recovery protocol that blocks entry to Phi until every partial outcome is reconciled. This document does not specify that protocol and does not assume that an external settlement can be reversed. On the entitlement path of Section 3.4, where no 402 retry occurs, the post-quote request that presents (R, S, M) serves as the activation request and carries k.¶

The idempotency-key discipline is established practice on payment-initiating HTTP interfaces, and a generic header-field form was drafted in the HTTPAPI Working Group as [I-D.ietf-httpapi-idempotency-key-header], which has since expired (Section 1.1) and which documents deployed interface patterns. This document cites that draft as provenance for the discipline the model binds to its gate, not as a standard; what the model adds is the binding of the key to the payment gate specifically, confirmed by the same gate commit that consumes the nonce.¶

6.1. Constraints

The properties of Section 7 are statements about well-formed runs, where well-formedness is the following eight constraints:¶

C1 (price-freeze):

A task activates only at the price of its issued quote; any change to the product or parameters requires a new quote and a new R.¶

C2 (scope):

The quote's scope descriptor is in the mandate's authorised scope set.¶

C3 (deadline):

The quote's deadline does not exceed the mandate's authority expiry.¶

C4 (contributor criteria):

Every ledger entry bound to a task under mandate M is from a contributor satisfying chi_M.¶

C5 (authority/budget):

Committed spend plus the quoted amount does not exceed the mandate's cap.¶

C6 (escalation):

When epsilon_M(q) is true, the task is routed to human re-approval at pending_authority, pre-gate, and is never auto-fulfilled.¶

C7 (single requirement):

Exactly one requirement R is issued for each quote. A task has at most one current, unconsumed R. After R expires or is invalidated, continuing requires a new quote, and no R is issued after the task crosses the gate.¶

C8 (atomic activation and idempotency):

A digest of a stable, versioned canonical representation covering every field that affects quotation, authority, settlement, and fulfilment is recorded with k before the gate, and the store binds k to taskId at the gate commit; the representation and digest algorithm are deployment obligations. Reuse with different request data fails. At activation, the following form one recoverable transaction: binding k to taskId, confirming the recorded digest, consuming eta(R), committing spent(M), atomically reserving or consuming any finite entitlement, recording the accepted payment, credit, or entitlement reference, and entering Phi. Requests carrying k after that transaction return the stored state without revalidating R. The binding or a non-reusable tombstone remains available for at least the longest period in which the operator accepts a retry or permits settlement of R. After that period, the old key is rejected rather than allowed to select a new task.¶

C2, C3, and C5 are conjuncts of authorises; C1 and C7 are enforced by the quote/requirement issuing map and the task engine; C4 by the ledger invariant; C6 by pre-gate escalation routing; C8 by the task store's atomic activation transaction.¶

6.2. Assumptions

The properties hold within the model under the following named operating conditions. Each is checkable, and each names what would have to be re-established if a deployment context differs.¶

• Mandate authenticity: the mandate and payment credential are cryptographically verifiable, and credentialValid(cred, R) is evaluable by the operator without trusting the calling agent; authority rests on signature verification, not the agent's assertion.¶

• Deterministic pricing: the pricing function returns one value for the product, parameters, and pricing state at quote time; challenge expiry bounds the window in which a frozen price is honoured. All components participating in the gate commit use a consistent time source and boundary convention for t_exp, dl, and d_lim.¶

• Gate-before-fulfilment is enforceable: the operator controls the ordering of its own task state machine, so no transition into Phi occurs before the gate is satisfied. This is an invariant of the operator's own task engine, not of any external protocol, and it holds regardless of settlement method.¶

• Contributor supply and deadlines: lack of a qualifying contributor leads to credited_or_refunded. Expiry of dl(q) before the gate leads to cancelled when no capture is recorded, and to credited_or_refunded when one is; expiry after the gate and before delivery leads to credited_or_refunded. These deadline edges are evaluated before other events.¶

• Hash collision-resistance: hashAlg identifies the hash algorithm and artefactHash is computed over a stable byte representation of the delivered artefact using that collision-resistant hash, making substitution of a different artefact computationally infeasible under the assumed hash security.¶

• Idempotency keys are client-supplied, stable, retained at least as long as a payment can be retried, and bound to a request fingerprint: a retry within that period carries the same key, so the retry properties apply when client retries cause duplicate processing.¶

• Receipt and ledger integrity: the ledger L is append-only and the receipt store is durable and tamper-evident, so unauthorised rewriting is detectable; durability alone does not provide integrity.¶

• Record identity and final-receipt cardinality: taskId identifies exactly one task record; rho_pay identifies exactly one record within its method-specific payment, credit, or entitlement store; and the receipt store accepts at most one final Omega per taskId.¶

• Gate-commit integrity: the operator mints nonces with negligible collision probability; the properties are conditional on no nonce collision occurring. The gate-commit transaction of C8 occurs as one atomic or recoverably journalled operation; a crash cannot commit only a subset of its effects. A consumed nonce never returns to fresh.¶

• Budget accounting: spent(M) is committed atomically with the gate transition, so concurrent activations under one mandate serialise against the cap and cannot jointly exceed it.¶

7.1. Property 1: Gate-before-Fulfilment Safety

Statement. In every reachable trace, no side effect of the fulfilment function F occurs unless validate(R, S, M) = true held at that or an earlier step.¶

Argument (by construction over the transition table).¶

• (a) Phi excludes the start state: draft has level 0, below 5.¶

• (b) Enumerating the in-edges of Phi from Table 3: the only states outside Phi with edges that could target Phi are the pre-gate states, draft through g* (level 4 or below); the exception terminals have no out-edges; and the cross-cutting fault edges target failed or credited_or_refunded, neither of which is in Phi. Inspection shows that the set of edges from outside Phi into Phi is the singleton {g* to pending_expert_match}, guarded by validate(R, S, M) = true. In particular pending_authority resolves only to g*, cancelled, or credited_or_refunded, all outside Phi, and needs_client_clarification is entered only from awaiting_expert_input, an intra-Phi edge.¶

• (c) Every other edge with target in Phi has its source already in Phi.¶

• (d) Hence any trace reaching a state in Phi contains the gate step taken under validate = true. Since the side effects of F fire only on transitions entering or internal to Phi, each occurs no earlier than that successful validation. The guard is evaluated atomically with the transition, and consume(eta(R)) makes fresh(eta(R)) false, so no trace leaves Phi and later re-enters it: re-entry could occur only through the gate edge, whose freshness conjunct cannot hold again for this task (C7).¶

7.2. Property 2: Idempotency under an Idempotency Key

Statement. While the C8 binding is retained, for activation requests in one client namespace that carry the same key and request fingerprint, at most one task record is selected. Later requests observe the same record; reuse with a different fingerprint is rejected. This property does not establish settlement-side charge uniqueness.¶

Argument. The gate commit for the first activation carrying k runs CAS(k: bottom -> taskId) (C8), which succeeds and binds exactly one task record to k. On the 402 path the pre-gate challenge record carries k, the credential retry maps to that record, and the gate commit it drives performs the single CAS for k. A concurrent retry that does not win the CAS is routed to the task created by the winning commit once its request fingerprint matches. Any request carrying k after the gate commit finds the outcome recorded; the server returns the existing taskId and settlement reference rho_pay (and, after delivery, the same Omega) without re-invoking F or repeating the gate commit. Whether a settlement method can create more than one transfer, authorisation, or capture is outside this property and requires a settlement-side uniqueness guarantee. Hence a retained key selects at most one task record and one gate commit. Later requests address that evolving record.¶

7.3. Property 3: Single Acceptance per Payment Requirement

Statement. For any issued requirement R, at most one successful gate transition consumes R. This model does not prevent multiple out-of-band payments or settlement-side charges unless the selected settlement method provides a uniqueness guarantee bound to R. Any subsequent compensation issues a refund or credit against the settlement reference rho_pay.¶

Argument.¶

• (a) The issuing map produces exactly one R per quote, with a nonce generated with negligible collision probability, and by C7 at most one unconsumed R is in force per task.¶

• (b) Validation consumes the nonce atomically; thereafter fresh is false, so re-presenting the same proof cannot produce a second successful gate transition. Nonce consumption alone does not prove that only one transfer, authorisation, or capture occurred.¶

• (c) A second, distinct R requires a new quote (C1 and C7); no replacement requirement is issued for the existing quote or after the task crosses the gate.¶

• (d) By Property 2, the keyed request produces at most one task selection and one gate commit; this does not establish settlement-side charge uniqueness.¶

Combining (a) through (d): at most one successful gate transition consumes any issued R; this constrains server activation only, and settlement idempotency remains a separate property of the selected method. A later credited_or_refunded transition issues a refund or credit against rho_pay; it never captures a second charge.¶

7.4. Property 4: Operator-Checkable Audit Record

Statement. Every task in state delivered has an operator-issued receipt Omega whose fields can be checked against the operator-controlled mandate, settlement, task, and receipt stores under the assumptions of Section 6. This property does not provide evidence against a dishonest or compromised operator.¶

Argument. The only in-edge to delivered is from ready, guarded by the construction and writing of Omega; hence delivered implies Omega exists. Omega embeds hashAlg and artefactHash (binding the exact artefact under the hash algorithm named by hashAlg), rho_pay (identifying the settlement record), taskId, and M. Under the record-identity and final-receipt-cardinality assumption of Section 6, the final delivery receipt is immutable. Compensation records are separate append-only records linked to rho_pay and, where a delivery receipt exists, to Omega; they neither replace Omega nor violate final-receipt cardinality. verify_Omega resolves taskId to the stored final receipt and requires equality, recomputes artefactHash over the exact delivered bytes using hashAlg and checks equality, resolves rho_pay against the method-specific payment, credit, or entitlement record, resolves M against the mandate registry, and checks the taskId binding against the task store; these checks depend on the assumptions of Section 6 and on the operator-controlled stores.¶

7.5. Composition

Together, the scoped properties state that modelled fulfilment effects follow a successful gate transition (Property 1), a correctly keyed request selects at most one task record (Property 2), one requirement can produce at most one successful gate acceptance (Property 3), and delivery creates an operator-controlled record (Property 4). Bounded delegated spend is not a separate proven property: non-exceedance of the mandate cap is delivered by the budget conjunct withinBudget of authorises, which enforces C5, together with the budget-accounting assumption of Section 6, under which concurrent activations serialise against the cap. They do not establish payment-fulfilment atomicity, settlement-side charge uniqueness, or operator-independent verification.¶