Show #1 (U.System): effectful API boundary (algebraic effects intuition)

System: A “Payment Authorize” service.

• Signature layer (A.6.0).

  • Vocabulary: PaymentRequest, AuthDecision, MerchantId, Money, etc.
  • Laws: e.g., “If decision is APPROVED then reservedAmount = requestedAmount” (truth‑conditional).
  • Applicability: bounded context “Payments Authorization”.

• Mechanism layer (A.6.1).

  • Admissibility gate: request is admissible iff tokenValid ∧ merchantActive ∧ amountWithinLimit.
  • Boundary transport details: HTTP headers and idempotency-key carriage. Declare canonical currency-conversion operations under A.6.1.
  • The local Audit and observability section specifies required evidence carriers (e.g., AuthorizationRecord event, log entry) and their fields, correlation IDs and retention class. Retention duties remain D-claims.

• Actual occurrence and work layer.

  • The payment-handling occurrence is U.Work only when its exact actual performer first has the A.13 core and A.15.1 independently admits the occurrence from its Method, time, containing System, and other required direct facts. If this payment account also asks under which assignment the performer acted, add F.6 through the same obtaining A.13 assignment; missing or failed attribution leaves the payment Work intact.
  • The ledger reservation change, event emission, timer transition, or retry effect is a separate actual-occurrence claim under A.3/A.3.4 or its exact interaction or causal-use pattern. Check each effect separately: knowing that the payment Work occurred does not show that the ledger changed, an event was emitted, or a retry happened.
  • Traces, logs, and metrics enter an A.10 evidence path for the exact effect being relied on; carrier presence creates neither Work nor change.

• Publication faces (MVPK).

  • PlainView: narrative for stakeholders (what the service promise is, in plain terms).
  • TechCard: signature or mechanism details (types, error codes, version policy, admissibility predicate refs).
  • InteropCard: machine‑exchange oriented boundary details (canonical field names, schema refs, transport bindings).
  • AssuranceLane: evidence bindings (which carriers exist, how to adjudicate E-* claims, retention and access duties by reference).

Effects-and-handlers analogy. In this software example, the signature exposes the operation interface. A.6.1 governs declared operation semantics and the separate realization relation; the realizing entity supplies the concrete handler implementation. Implementations can change while preserving the declared operation meanings and applicable constraints.

Classification example:

• “A request is admissible iff tokenValid ∧ merchantActive ∧ amountWithinLimit” belongs in Quadrant A (the declared admissibility gate).
• “Clients MUST include Idempotency-Key” belongs in Quadrant D as a normative prescription and should reference the same gate semantics to avoid divergence. It becomes a claim about one obtaining individual U.Commitment only after A.2.8 identifies the actual bearer, constitutive rule, required instituting basis, and direct predicate.
• “System emits AuthorizationRecord” belongs in Quadrant E (an actual event-emission claim).