The Claim as Primitive

Abstract

A contingent payment requires an observed outcome, a rule for calculating the amount owed, and evidence that the obligation was performed. These remain distinct when the same claim trades through different markets. We define a claim by a finite payoff program, its evaluation dates, and its financial and payment terms. The numerical language computes exactly the functions that are polynomial on finitely many regions selected by polynomial comparisons. Historical references and a certified extension for calculations within one event give an order in which dependent claims can resolve. Exact arithmetic, financial types, and retained evidence preserve the meaning of the resulting amount. An entitlement journal preserves unpaid balances through partial payment, correction, and local interruption, under stated authority and storage premises. We then separate this payment model from market pricing. Cost-function curvature determines local price impact and finite-trade error bounds. For logarithmic market scoring rules, this curvature is proportional to payoff covariance under the market’s implied probabilities. External input authority, funding, and settlement completion remain separate requirements.

The author has a commercial interest in systems of the kind this paper describes.

1 Introduction

1.1 A payment, its calculation, and its performance

Consider a cash-settled call option: its holder is owed the amount by which an observed asset price exceeds a fixed strike, if positive. The contract must identify the price source, observation date, underlying quantity, payment currency, and payment date. The source must supply admissible evidence before the amount can be calculated. The resulting obligation then remains due until performance satisfies the contract’s evidence rule. A quoted market price answers a further question: what someone pays to acquire this contingent right before its outcome is known.

Write S_h for the attested asset price at observation height h, and K for the fixed strike. A height is the integer position of an observation or resolution in the ledger’s sequence. The price and strike are measured in USD per underlying unit. Subtracting them and taking the positive part gives \max(S_h-K,0) per underlying unit. Multiplication by the contractual quantity gives the USD amount payable in the declared payment context. A quantity of one is numerically one, but its asset unit and payment date remain part of the contract.

Three records have different jobs. The resolved value records the calculation and the observations it used. An entitlement records the resulting amount owed by a named debtor to a named creditor. Discharge records satisfaction of that obligation under the governing evidence rule. For example, a later payment can reduce an entitlement while leaving the resolved value unchanged. A price observation alone establishes neither payment nor final settlement. The settlement distinction follows the cited financial-infrastructure rules [49].

The call calculation needs four operations: read the attested price, supply the strike, subtract, and take the maximum with zero. We write these as \mathrm{Oracle}, \mathrm{Const}, \mathrm{LinComb}, and \mathrm{Floor}. Here the zero offset in \mathrm{Oracle}(S,0) selects the current observation. The program \mathrm{Floor}\!\left( \mathrm{LinComb}(1,-1;\mathrm{Oracle}(S,0),\mathrm{Const}(K)),0 \right) emits \max(S_h-K,0), the call payoff. Its syntax fixes the resolved amount. Its schedule fixes when that amount is evaluated. Its financial declarations supply the contractual quantity and payment terms. A market can quote this same claim using its own pricing rule.

Options, state claims, parimutuel orders, and reserve positions already have established pricing mechanisms [13, 14, 34, 6, 28]. The question here is how to specify their payoff calculations independently while retaining the information required for evaluation and performance. A common representation must identify exactly what it expresses, order its dependencies, and preserve the obligations that survive calculation. Only then can we ask which pricing properties come from a chosen market.

Our central construction attaches these requirements to the claim itself. A finite graph records the payoff calculation, with each operation using earlier computed arguments. References identify earlier resolved claims, allowing coupons and historical statistics to reuse recorded values. An immutable entitlement records the resulting obligation, while a separate payment journal records its performance. The language computes exactly the piecewise-polynomial functions specified in Theorem 4.1. The call illustrates this class: the payoff is zero below the strike and S_h-K at or above it.

The execution results explain when these formulas determine an amount and what survives a retry. The basic reference rule requires earlier heights. A larger certified profile also admits calculations within one event when every producer dependency has an order. These results depend on admitted inputs, financial declarations, and resource limits. They do not establish the authority of an external source or the completion of an external payment.

Market pricing uses the resulting claims as inputs. For a smooth cost-function market, the Hessian measures how marginal prices change with traded quantities. At an equilibrium with positive-definite Hessian, it gives the quadratic correction to a trade’s marginal-price mark. For log-partition markets it also represents covariance under the market’s implied probabilities. Other markets require a separate source for the joint distribution of claim outcomes.

1.2 Relationship to prior work

Contract languages.

Peyton Jones, Eber, and Seward introduced the combinator treatment of financial contracts: a small typed language whose terms denote contracts and compose [46]. Our language belongs to that line but is built for on-chain resolution: every node fixes its arity at construction, evaluation has a finite arithmetic-operation count per edge, with bit cost governed by Section 2.6 (and, for the window leaf of Section 5, one read per height in its window under the indexed-access model of Definition 2.11), and references across claims carry explicit time offsets. The results proved here are an exact expressiveness characterisation for this language and a well-foundedness theorem for its cross-claim references.

Cost-function market makers.

Hanson’s logarithmic market scoring rule (LMSR) is the canonical bounded-loss prediction market [28, 29]. Chen and Pennock formulated the general cost-function market maker: a convex potential over outstanding quantities whose difference prices every trade and whose gradient is the price vector [20]. Abernethy, Chen, and Vaughan characterised the admissible cost functions as convex conjugates of regularisers on the price simplex, with bounded loss and no arbitrage [3]; Othman, Pennock, Reeves, and Sandholm developed liquidity-sensitive variants [44]. Definition 8.4 is exactly the Chen-Pennock object, Proposition 8.14 is a second-order statement at an equilibrium of that object, and Proposition 8.20 instantiates the classical exponential-family identity — the Hessian of a log-partition function is the covariance of its sufficient statistic [15] — at the LMSR potential.

Constant-function markets.

Angeris, Kao, Chiang, Noyes, and Chitra analysed the constant-product market and the level-set geometry of constant-function market makers [6]; Angeris and Chitra treated their price-oracle behaviour [7]. Angeris, Evans, and Chitra introduced the portfolio value function V(p) = \inf_{R \in K} p^\top R over the reserve set and the replication theory built on it [8]. Frongillo, Papireddygari, and Waggoner proved that constant-function markets and cost-function prediction markets are equivalent up to convex duality [24]. We use the portfolio-value form to place the constant-product market in our catalogue; the invariant is a level set, and we do not read it as a cost function.

Parimutuel and auction clearing.

Lange and Economides designed the demand-based parimutuel exchange [33, 34]; Peters, So, and Ye convexified it into a convex parimutuel call auction mechanism (CPCAM) cleared by one convex program [45]. Plott and Sunder established experimentally that such mechanisms aggregate dispersed information [47, 48].

Options.

Black-Scholes-Merton price and replicate option payoffs [13, 42]; Breeden-Litzenberger recover state prices from strikes [14]; Hull systematises the payoff taxonomy [31]. Vanilla call and put payoffs are one-line \Sigma-programs. Closed-form Black-Scholes-Merton prices are pricing functions rather than payoffs and require the normal cumulative distribution function in addition to elementary analytic operations (Open problem 1).

Time-indexed reference languages.

The condition that every cyclic reference cross a strictly positive delay is the causality rule of synchronous dataflow languages: a cyclic definition is admissible in LUSTRE only when every cycle crosses a unit delay [19, 27], and Esterel’s causality analysis is the standard treatment of what fails when it does not, behavioural in the language definition [11] and constructive in its later semantics [12]. The same rule recurs as temporal stratification in Datalog, where a predicate may depend on itself only at an earlier time index [9, 5], and as guarded recursion under the later modality [43]. Lemma 3.1 is that rule instantiated at block height.

Resolution, discharge, and settlement liquidity.

The Principles for Financial Market Infrastructures define final settlement as the irrevocable and unconditional transfer of an asset or discharge of an obligation [49]. Fedwire provides one concrete rule under which an interbank transfer is immediate, final, and irrevocable once processed [23]. Other systems reduce funding demand by waiting for offsetting obligations. CLS combines payment-versus-payment settlement with multilateral netting and liquidity-saving tools [17, 18]; CHIPS uses a liquidity-saving algorithm [50]; and the theoretical literature states the trade-off between liquidity use and delay [40, 25, 16]. Du’s payment-innovation analysis places the same boundary around tokenised systems [22]. These sources do not define claim semantics. They fix the distinction used here: resolution determines an entitlement, while discharge requires the external system and evidence rule named by the claim.

Provenance.

The convex analysis of Section 8 is applied from the market-maker literature above. This paper defines one typed language and proves both directions of its exact expressiveness characterisation. It also defines a bounded window-reduction leaf for schedule-adaptive historical statistics and a pre-issued recurrence for memory coupons (Proposition 5.3, Proposition 5.7). Lemma 3.1 applies the cited dataflow-causality condition at block height. The claim model makes a strict-positive reference offset part of well-formedness and derives the evaluation schedule in Corollary 3.2.

1.3 Order of the argument

The argument follows the information needed to turn a payoff formula into a recorded obligation. We first define inputs, operations, and financial meaning. Exact arithmetic then distinguishes a known amount from an unresolved comparison, while schedule admission checks every promised evaluation date. Historical references give the basic evaluation order, and the entitlement journal retains the amount still due. The expressiveness theorem identifies the resulting numerical function class. Historical payoffs and the complete evaluator show how these parts compose. The producer certificate extends this order to computations within one event.

Only after fixing the claim do we introduce markets over it. The reserve construction explains which rights can be held and transferred as funded instruments. The curvature results then state what a chosen pricing function determines. The catalogue uses both constructions, while the final examples and open problems identify their remaining hypotheses.

2 Specifying the amount and its financial meaning

The call uses a fixed strike and an observed price. A coupon can also use a value calculated at an earlier date. These give the three input categories below: fixed literals, attested observations, and prior resolutions. An attestation is a source’s recorded assertion of a value, subject to the claim’s evidence rule.

Time is indexed by block heights h\in\mathbb{N}. A state \omega\in\Omega specifies the joint outcomes of oracle attestations and prior claim resolutions. The measurable space (\Omega,\mathcal{F}) records which events these outcomes define. The information available at height h forms the \sigma-algebra \mathcal{F}_h. Thus an input available at h is measurable with respect to \mathcal{F}_h.

2.1 Inputs and types

Definition 2.1 (Input categories).

A claim’s payoff is a function of three input categories:

(I1): Constant amounts. \mathbb{R}-valued literals fixed at claim-creation time.
(I2): Oracle-attested commitments. An attested data stream O carries one \mathcal{F}_h-measurable random variable O_h : \Omega \to \mathbb{R} per height h at which O is attested. The leaf \mathrm{Oracle}(O, \tau) has an integer offset \tau \in \mathbb{N}_0 and, when evaluated at height h, retrieves O_{h-\tau}. The case \tau = 0 reads the attestation published at the evaluation height itself. The attestation supplies an input to payoff evaluation. It does not transfer value or establish legal finality. Oracle leaves create no claim-reference edges. Their producer dependencies require the explicit contracts and certificate of Section 7.
(I3): Resolved-claim references. For another claim c', the reference \mathrm{Ref}(c', \tau) has an integer offset \tau \in \mathbb{N}_{\geq 1} and, when evaluated at height h, retrieves v_{c'}(h - \tau), the value carried by c' at height h - \tau. The leaf is well-formed when c' resolves at height h - \tau (Definition 2.11). Strict positivity of the offset makes cross-claim resolution well-founded (Section 3).

Remark 2.2 (Bounded payoffs).

The language and its expressiveness theorem admit bounded and unbounded real-valued payoff programs. A collateral or risk rule may admit only essentially bounded payoffs (\|f\|_\infty < \infty), or it may require a stated tail-integrability and collateral standard. A terminal \mathrm{Cap}–\mathrm{Floor} pair supplies an explicit finite bound. None of these conditions establishes that a venue has sufficient resources or that an entitlement will be discharged. Open problem 4 states the remaining admissibility question for unbounded payoffs.

2.2 The operator language \Sigma

The call’s subtraction and lower bound are examples of arithmetic and selection. A digital payment also needs a comparison, and a conditional coupon needs a choice between two amounts. The language \Sigma collects these operations with the three input constructors. A constructor specifies one kind of operation. Its arity is its number of argument expressions. The numerical sorts below distinguish real amounts from Boolean decisions, whose values are zero and one.

Definition 2.3 (Operator language).

The numerical language has two value sorts, \mathsf{Num}=\mathbb{R} and \mathsf{Bool}=\{0,1\}. We use the canonical inclusion \iota:\mathsf{Bool}\hookrightarrow\mathsf{Num} when a Boolean output enters a numeric input; there is no coercion from \mathsf{Num} to \mathsf{Bool}. The operator language \Sigma consists of nine constructors; each node fixes its arity at construction — a stated constant for eight of them, any finite integer k\geq 1 for \mathrm{LinComb}: \begin{align*} &\mathrm{Const}(c) && \text{(constant; arity 0; }c\in\mathbb{R}\text{)} \\ &\mathrm{Oracle}(O, \tau) && \text{(oracle; arity 0; }\tau\in\mathbb{N}_0\text{)} \\ &\mathrm{Ref}(c', \tau) && \text{(reference; arity 0; }\tau\in\mathbb{N}_{\geq1}\text{)} \\ &\mathrm{LinComb}(\alpha_1, \dots, \alpha_k; e_1, \dots, e_k) && \text{(linear; arity } k\geq1;\ \alpha_i\in\mathbb{R}\text{)} \\ &\mathrm{Mul}(e_1, e_2) && \text{(product; arity 2)} \\ &\mathrm{Cap}(e, \mathit{ub}) && \text{(upper bound; arity 1; }\mathit{ub}\in\mathbb{R}\text{)} \\ &\mathrm{Floor}(e, \mathit{lb}) && \text{(lower bound; arity 1; }\mathit{lb}\in\mathbb{R}\text{)} \\ &\mathrm{Ind}(\bowtie, e_1, e_2) && \text{(indicator; arity 2)} \\ &\mathrm{IfElse}(b, e_+, e_-) && \text{(branch; arity 3)} \end{align*} At height h, the first three nodes emit the \mathsf{Num} values c, O_{h-\tau}, and v_{c'}(h-\tau). The remaining nodes emit \sum_i\alpha_i e_i, e_1e_2, \min(e,\mathit{ub}), \max(e,\mathit{lb}), \mathbb{1}[e_1\bowtie e_2], and b e_+ +(1-b)e_-. Here \bowtie\in\{<,\leq,=,\geq,>\}. The first seven operators consume and return \mathsf{Num} values as their displayed formulas require. \mathrm{Ind} consumes two \mathsf{Num} values and returns \mathsf{Bool}. \mathrm{IfElse} requires one \mathsf{Bool} condition and two \mathsf{Num} branches and returns \mathsf{Num}. Six constructors form the unique minimal subset of this vocabulary under the input-preserving comparison in Proposition 4.3. \mathrm{Cap}, \mathrm{Floor}, and \mathrm{IfElse} are definable conveniences (Proposition 4.3).

The nested call formula can share intermediate calculations with other parts of a payoff. We represent each calculation once and connect it to the operations that use its result. A directed acyclic graph, abbreviated DAG, is a directed graph with no directed cycle. It supplies an order in which arguments are available before their consuming operation runs.

Definition 2.4 (Payoff program).

A payoff program is a finite labelled directed acyclic graph (DAG) whose root is a single \mathsf{Num} output node and whose internal nodes are operators in \Sigma, with edges directed from arguments to the operator they enter. The numerical edges match their input and output sorts, with the sole implicit Boolean inclusion. A financial program additionally satisfies the scalar-type and retained-evidence rules in Definition 2.6, and its root matches its declared claim output type. Leaves are arity-zero operators (\mathrm{Const}, \mathrm{Oracle}, \mathrm{Ref}); internal nodes are arity-\geq 1 operators. The DAG is in static single-assignment (SSA) form, the standard compiler discipline [21]: each node’s output is consumed by zero or more downstream operators, but the node itself is computed exactly once.

2.3 Financial dimensions and declared conversions

In the call, a USD-per-unit price difference becomes a USD payment only after multiplication by the contractual underlying quantity. A number alone also fails to distinguish dollars from cents, or an amount due today from an amount due later. Financial types record these distinctions before evaluation.

The type has three components: dimension, numerical scale, and economic context. Dimension identifies units such as USD or an underlying asset. Scale distinguishes representations such as dollars and cents. Context records valuation basis and payment maturity. The free abelian groups below allow products and inverse units, as in USD per asset unit. Their identity elements describe a dimensionless number and an observation with no payment context. Observation dates remain attached as evidence even when their numeric samples share a type.

Definition 2.5 (Financial scalar types).

Let D be the free abelian group on named currency, asset, and quantity dimensions. Distinct currencies and assets have distinct generators. Gold mass uses one dimension, while grams and kilograms use different scales. Let K be the free abelian group on named economic contexts. Each context records its valuation basis and payment maturity. Its identity 1_K denotes observation data, while products and quotients describe intermediate quantities and context maps. A scalar type is \theta=(d,s,k),\qquad \mathsf{Num}[\theta], \qquad d\in D,\quad s\in\mathbb Q_{>0},\quad k\in K. The represented number x denotes sx canonical units of dimension d in context k. Type multiplication acts componentwise: \theta_1\otimes\theta_2=(d_1d_2,s_1s_2,k_1k_2). The Boolean inclusion maps into the neutral type \mathbf1=(1_D,1,1_K).

An input manifest \Gamma declares every literal, input, coefficient, and conversion rule. Declarations fix scalar types, permitted uses, and evidence identifiers. Dimensioned literals require their governing declarations. An instance context \kappa fixes the evaluation height, required output type, and current rules for evidence use. A monetary output names its settlement asset, scale, and payment context.

The input manifest \Gamma is the collection of declarations that fixes these types and their allowed uses. The instance context \kappa specializes those declarations to one evaluation date and required output. The judgment below states both what an expression means financially and which evidence its calculation must retain. This second component matters when algebra simplifies a term whose source still has contractual relevance.

Definition 2.6 (Typing and retained evidence).

The judgment \Gamma;\kappa\vdash e:\mathsf{Num}[\theta]\;!\;E states a scalar type and its retained evidence identifiers. Evidence records bind source, authority, observation height, source context, and the exact attested value. The rules are:

Declared literals and oracle inputs use their manifest types and retain their declaration or attestation identifiers.
A reference declares an amount read or a sample read. An amount read preserves the complete source type. A sample of type (d,s,k) returns (d,s,1_K) and retains the source identifier, context, and height. Sampling records a numeric observation and grants no position in the source claim.
A linear combination requires equal argument types and dimensionless scalar coefficients. Its output has that same type. Dimensioned coefficients enter as declared values through multiplication.
Multiplication maps \theta_1,\theta_2 to \theta_1\otimes\theta_2.
A cap or floor requires its bound to have the argument’s type and preserves that type.
An indicator compares equal scalar types and returns a Boolean. The observation heights may differ.
A conditional requires a Boolean and two branches of the same scalar type, which is its output type.

Each operator retains the union of all operand evidence, including zero-weight operands and both branches. Algebraic optimization therefore preserves a separate evidence manifest even when it eliminates numerical work. Every root matches the output type declared by its claim context.

Changing cents to dollars changes the representation of one currency amount. Changing BTC to USD also requires a rate and a rule permitting its use. A conversion witness records that rule and the source of the rate. The same distinction applies between valuing a future amount today and replacing the underlying payment obligation. In the next formula, |e| and |r| mean numerical elaboration: the corresponding expressions with financial annotations removed. These bars distinguish elaborated expressions here, rather than absolute values of numbers.

Definition 2.7 (Rescaling and witnessed conversion).

Rescaling from (d,s,k) to (d,s',k) multiplies the represented number by s/s'. It preserves dimensions, context, and evidence. For a conversion to (d',s',k'), a witness w binds the source and target types, permitted use, rate direction, observation, authority, and rule. A maturity conversion also binds its authorized discounting rule or obligation-replacement record. A rate r has type (d'd^{-1},s_r,k'k^{-1}). The checked conversion has numerical elaboration |\mathrm{Convert}_{w}(e,r)| =\mathrm{LinComb}\!\left(\frac{s s_r}{s'}; \mathrm{Mul}(|e|,|r|)\right). Its evidence includes E_e\cup E_r\cup\{\operatorname{id}(w)\}. The manifest requires this use witness for an observed conversion rate. An erased multiplication cannot bypass that requirement. Fixed contractual coefficients instead retain the issuance declaration that assigns their types and permitted uses.

A valuation witness authorizes a numerical valuation. Physical exchange and obligation replacement use their separately applicable authority and effect records. The replacement preserves the predecessor obligation’s history. Rescaling and conversion are checked elaboration forms over the nine numerical constructors.

The first preservation result checks that composing valid operations cannot silently change the required currency, scale, maturity, or evidence. Its proof follows the graph’s evaluation order and checks each typing rule against its numerical formula.

Proposition 2.8 (Financial type preservation).

Assume every declared input and conversion witness satisfies its manifest and instance context. Evaluation of a well-typed finite DAG preserves its declared root type and all required evidence. Its represented numeric value equals the result of its numerical elaboration into \Sigma.

Proof. Induct over a topological node order. Declared leaves supply their types and evidence. Equal-type arithmetic and bounds preserve their common type. Multiplication composes dimensions, scales, and contexts. Compatible comparisons return Booleans, and the two conditional branches share their output type. Rescaling multiplies by s/s', which preserves the canonical quantity. Conversion multiplies by s s_r/s' and the represented rate, giving the declared target quantity. The conversion witness establishes its admitted context and use. Every rule retains operand evidence, while each numerical formula agrees with its elaboration. The induction proves both conclusions. ◻

The converse construction starts with a financially specified formula. It requires enough declared coefficient types to make each monomial produce the promised output type. Under that premise, the numerical expressiveness construction also yields a financially well-typed program.

Proposition 2.9 (Lifting a financial payoff specification).

Fix typed inputs and a required output type \theta. Consider a finite piecewise-polynomial specification with compatible comparisons. For every monomial, its manifest supplies the coefficient type required to produce that polynomial’s declared output type. All declarations and conversion uses satisfy the instance context. Then the specification has a well-typed payoff program. Its numerical elaboration computes the specified function exactly.

Proof. For a monomial c_\alpha\prod_jX_j^{\alpha_j}, the manifest supplies its coefficient with type \theta\otimes\bigotimes_j\theta_j^{-\alpha_j}. Multiplying the coefficient and factors gives type \theta. Adding monomials with dimensionless weights preserves that type. Compatible polynomial comparisons give neutral numeric indicators through the Boolean inclusion. Products of those indicators remain neutral, so multiplication by each regional polynomial preserves \theta. The region construction in Theorem 4.1 gives the required program. Every coefficient and context map remains subject to its declared authority and use. ◻

For example, direct USD-plus-BTC addition fails, as does addition of gold mass and currency. An observed rate of 60{,}000 USD per BTC converts 10^8 satoshis into 6{,}000{,}000 cents. The scale factor is 10^{-8}/10^{-2}=10^{-6}, and the witness retains the named rate observation and its authority. A scale annotation alone cannot supply that factor. Historical price samples can be compared or averaged while retaining their distinct observation heights. Dated payment amounts require a declared context map before combining different maturities.

Remark 2.10 (Deterministic lowering).

A topological instruction order evaluates each numerical DAG node after its arguments and stores shared values once. Financial elaboration retains its independent evidence manifest through optimization. The exact rational implementation and its refinement proof appear in Section 2.4. The schedule and bit envelopes in Section 2.5 and Section 2.6 bound admission and execution work.

The program now specifies a calculation with financial units. A claim must additionally say when that calculation applies and which contractual terms govern its result. The schedule is the set of evaluation heights. Program cases allow an initial calculation and a different recurring calculation under one fixed issuance.

Definition 2.11 (Claim).

A claim is a tuple c=(\mathit{id},H_c,\mathcal P_c,\mathit{ctx}). Its identifier is unique, its resolution schedule is nonempty, and \mathcal P_c is a finite table of program cases. Definition 2.17 gives their finite-prefix and periodic-tail representation. A single case (H_c,P) gives a fixed-program claim. The context records the parties, jurisdiction, governing clause, settlement asset, discharge route, evidence predicate, and attached venue. It also declares the input manifest, instance output type, reference read modes, and governing conversion uses.

The instance at b\in H_c selects its unique program P_i and evaluates it at b. Its immutable result is v_c(b), with directed entitlements and payment records defined in Definition 3.4. Structural admission checks every case and leaf through Proposition 2.18. It fixes valid oracle heights and strictly historical source references. Readiness separately requires their authentic input values to be available. An absent input keeps the instance pending.

A one-shot claim has schedule \{h_{\mathrm{res}}\}. A coupon bond has its finite coupon schedule. Per-height feeds and initialized recurring programs use their declared periodic cases. Section 2.6 accounts for their schedule and numerical bit costs.

A claim describes the payment per unit of holding. A position records how many such units a party holds, including a negative holding when that party bears the opposite obligation.

Definition 2.12 (Position).

A position in a claim c is a signed real-valued holding q \in \mathbb{R}, with q > 0 representing a long claim on the payoff and q < 0 representing a short. The entitlement is per instance. At each b \in H_c, evaluation determines the amount q \cdot v_c(b), where v_c(b) is the value of the payoff program in the realised state \omega \in \Omega (Definition 2.11). For a one-shot claim, evaluation determines q \cdot P(\omega) once at h_{\mathrm{res}}. Discharge follows the route and evidence rule in \mathit{ctx}.

2.4 Exact evaluation and certified numerical decisions

A digital payoff pays its full stated amount when a threshold condition holds and zero otherwise. Near the threshold, rounding an observation can therefore change the whole payment. The evaluator must decide the comparison before rounding a payment amount. Rational arithmetic represents admitted decimal inputs exactly. Certified intervals instead record uncertainty in an input and can leave a comparison unresolved. The ideal real-valued semantics remains the denotation used in the expressiveness theorem.

The reference numerical implementations use Python integers and JavaScript BigInt. The next definition fixes their common input representation and a resource envelope, which bounds the sizes and work an evaluation may use.

Definition 2.13 (Rational execution envelope).

A rational value has a signed integer numerator and a positive denominator, reduced by their greatest common divisor. Canonical ASCII integer and finite decimal strings admit exact conversion to this representation. The wire form excludes exponent notation, redundant leading or trailing zeros, and negative zero. Case identifiers are strings, so identifiers above 2^{53} retain their exact bytes across both implementations. The input contract declares units, scale, observation identity, and the relevant authority evidence. A decimal string denotes its stated rational value, rather than a binary floating-point approximation.

An execution envelope bounds input length, node and argument counts, numerator and denominator bits, and operation count. Before each allocation, the evaluator checks the required intermediate size against that envelope. For multiplication, unreduced numerator and denominator bit bounds add. For addition or comparison, cross-product bounds add, with one additional bit for a sum. The implementation returns BudgetExceeded before an operation exceeds its bound. This result preserves the pending calculation and its entitlement context. A larger admitted envelope permits the same program to resume from its bound inputs.

Proposition 2.14 (Exact rational refinement).

For rational inputs, coefficients, and bounds, every successful evaluation of a finite \Sigma DAG equals its real-valued denotation. Every comparison, including equality at a strike, has the same Boolean value. A topological instruction sequence that reads the same inputs computes the same result.

Proof. Reduced rational arithmetic embeds into the real field and preserves addition, multiplication, and order. Constants and admitted input leaves therefore have their specified denotations. Induction over a topological order proves equality at every arithmetic node. Exact cross multiplication by positive denominators proves every comparison. The resulting Boolean selects the same branch in both interpretations. The formulas for minimum, maximum, and affine combination preserve the induction. Shared nodes retain one value, so the instruction sequence and DAG agree. The budget check either permits this exact operation or emits a separate unresolved result. It never substitutes a wrapped or rounded value. ◻

Exact arithmetic removes representation error for a supplied rational input. An uncertain observation needs a different record: an interval containing every value still permitted by its evidence. A comparison can be committed only when all values in the intervals give the same answer. A continuation saves the unfinished calculation and the evidence still needed to complete it.

Definition 2.15 (Certified intervals).

An interval [l,u], with rational endpoints l\leq u, certifies that the input value lies between its endpoints. Addition adds endpoints, and multiplication takes the minimum and maximum of the four endpoint products. Positive scaling, minimum, and maximum use their monotone interval extensions. Signed scaling reverses endpoints when necessary. For a relation \bowtie, a comparison returns True when every pair in the operand intervals satisfies it. It returns False when no pair satisfies it, and Ambiguous otherwise. Thus equality is true only for equal singleton intervals, and false for disjoint intervals. Ambiguous records evaluator knowledge. It is not an additional value of the language’s Boolean type. A branch requiring that comparison retains its pending continuation until the evidence is refined or its governing failure route applies.

Proposition 2.16 (Interval soundness and boundary separation).

Every successful interval evaluation contains every exact output consistent with its input intervals. Every certified Boolean comparison agrees with all those exact evaluations. For a numeric comparison with threshold K, rational inputs K-\epsilon,K,K+\epsilon have exact outcomes for each declared relation whenever \epsilon>0. An interval straddling K can remain ambiguous even when its width is arbitrarily small.

Proof. Each interval operator encloses the corresponding real operation on its operand intervals. Induction over the DAG proves containment. The comparison rule quantifies over the enclosed operands, which proves its Boolean conclusions. Exact order decides the three rational inputs, including the equality case. For the predicate x\geq K, the interval [K-\epsilon,K+\epsilon] contains both outcomes. Multiplication by a notional N then permits outputs 0 and N. Interval width alone therefore supplies no vanishing error bound for this digital payoff. ◻

A payment quantum \Delta>0 acts after payoff evaluation. For a nonnegative entitlement a, downward quantization sends q=\Delta\lfloor a/\Delta\rfloor and retains r=a-q, where 0\leq r<\Delta. The entitlement ledger retains r until an applicable allocation or discharge rule consumes it. A signed payoff first fixes debtor and creditor, then applies this rule to its nonnegative amount. A valid currency conversion retains its exact observation evidence through evaluation and quantization.

The reference numerical implementations use Python integers and JavaScript BigInt independently. Their common vectors include every comparison around a boundary, 2^{53}+1, signed arithmetic, payment residuals, and deterministic budget failures. These implementations establish the specified arithmetic behavior on their supplied vectors. The proposition gives the general mathematical refinement argument. A deployment compiler must still establish that it implements this instruction relation and preserves the input evidence bindings.

2.5 Admitting finite and recurring schedules

A coupon that reads its preceding state needs a source value at every promised coupon date. Checking a single date cannot establish this for a recurring contract. We describe schedules by a finite initial part and a repeating pattern, so one finite check can cover all dates. The cutoff starts the repeating pattern, its period gives the repeat length, and its residues select dates within each period. A finite schedule has no repeating dates.

The admission test also covers a bounded historical window: all source dates scheduled within a specified number of earlier heights. Definition 5.1 will use such a window for an average, total, minimum, or maximum. Admission first checks that the selected set exists. Readiness later checks that every selected value has arrived.

Definition 2.17 (Schedule descriptors and program cases).

A descriptor (a,p,F,R) has a,p\geq1, F\subseteq\{1,\ldots,a-1\}, and R\subseteq\{0,\ldots,p-1\}. It denotes H=F\cup\{h\geq a:h\bmod p\in R\}. A finite schedule has R=\varnothing. A claim declares a nonempty schedule H and a finite case table (U_i,P_i). Each U_i has the same descriptor form, and each P_i is a finite payoff program. Exactly one case applies at every scheduled height: \sum_i\mathbb{1}_{U_i}(h)=\mathbb{1}_H(h)\qquad(h\geq1). The issuance fixes every descriptor, program, and referenced claim identifier. A single case (H,P) recovers the original fixed-program form.

After the last cutoff, each schedule membership test repeats periodically. The least common multiple aligns those periods. It is therefore enough to check the initial dates and one aligned repeat, including every shifted source date used by a reference.

Proposition 2.18 (Finite admission of recurring programs).

For case coverage, let T be the largest cutoff and L the least common multiple of all participating periods. Check the displayed coverage equality at 1\leq h<T+L. For a consumer case U=(a,p,F,R) and target H'=(b,q,F',R'), let L=\operatorname{lcm}(p,q). A reference with offset \tau\geq1 is admissible exactly when h-\tau\in H' for every h\in U with 1\leq h<\max(a,b+\tau)+L. A window of length W\geq1 is admissible exactly when h\geq W+1,\qquad \{h-1,\ldots,h-W\}\cap H'\ne\varnothing for every h\in U with 1\leq h<\max(a,b+W)+L. An oracle offset \tau\geq0 additionally requires h>\tau for all consumer heights. It suffices to check 1\leq h<\max(a,1+\tau)+p. This checks the observation domain, while attestation availability remains a readiness condition. These finite checks decide the corresponding universal requirements.

Proof. Below the stated threshold, the check visits each possible height directly. At and above that threshold, every relevant schedule uses its periodic tail. The shifted target predicates therefore have period L. The next L consecutive heights contain every remaining residue class. This proves both necessity and sufficiency for each check. ◻

The mathematical decision terminates for every finite descriptor. Binary-encoded periods can make its scan exponentially long. The executable admission envelope therefore bounds descriptor sizes, the least common multiple, scan horizon, and total membership work before scanning. An oversized instance returns BudgetExceeded, while a failed predicate returns Invalid with its witness height. The former permits a larger resource envelope without changing the schedule’s meaning. The checker tests multiplication bounds before constructing an oversized least common multiple. It scans heights directly and needs no array proportional to the horizon.

An admitted instance becomes ready when its own oracle inputs and referenced instances are available. A window selects all prescribed source heights before retrieving any value. A missing selected value yields \mathsf{Await}(M), which names the missing inputs. It never turns an average over scheduled heights into an average over the subset that happened to arrive. A deadline activates the continuation specified by the claim context while retaining its unresolved rights and evidence. Independent ready instances can proceed despite another claim’s missing input.

The ancestor closure of an instance contains all instances reached by recursively following its prerequisite references. Admission gives a valid finite dependency calculation for each requested instance. Completion also requires the observations to arrive and ready work to receive execution time. A fair scheduler eventually selects each ready calculation. The proposition states progress with these availability and resource premises explicit.

Proposition 2.19 (Conditional progress).

Every admitted instance has a finite ancestor closure. If every oracle input in that closure eventually arrives, a fair scheduler eventually evaluates the instance successfully within a sufficient arithmetic envelope.

Proof. Reference heights decrease strictly, and each selected program has finite fan-out. A starting height bounds the reference depth, so the ancestor closure is finite. The claim has finitely many required oracle inputs in this closure. Their eventual arrival supplies a time after which all are available. Induction on height and fair selection then evaluates every required ancestor and the requested instance. ◻

2.6 Resource cost in bits

A small graph can still create very large exact numbers. Repeated squaring doubles the exponent at each step, while repeated fractional scaling grows a denominator. An operation count therefore describes only part of the required resources. The following bound also counts the bits needed to represent every intermediate rational number. For one rational evaluation, expand the selected window reductions and count their inputs and arithmetic nodes. Let A count nodes, argument ports, and selected historical inputs. Let b_0\geq1 bound numerator and denominator bit lengths of all input values, literals, and scalar parameters. This count includes linear coefficients and the averaging coefficient 1/r for r selected heights. Let d be the maximum binary-multiplication depth. Let s count primitive scalar occurrences, let \ell count linear-combination nodes, and let k_v be their arities. A conservative bound on every reduced intermediate numerator and denominator bit length is B_* = 1+2^d\left[(s+\ell+1)b_0+ \sum_v\lceil\log_2 k_v\rceil\right] =O(A b_0 2^d).

To prove this bound, fix the outcomes of comparisons for the evaluated input. Treat primitive scalar occurrences as distinct variables. Each selected expression is a polynomial whose individual primitive-variable degrees are at most 2^d. If Q is the product of the primitive denominators, its reduced denominator divides Q^{2^d}. Define m(z)=\log_2\max(1,|z|). At a linear node, this magnitude bound increases by at most b_0+\lceil\log_2 k_v\rceil over the largest input magnitude. A multiplication adds the two logarithmic bounds. These denominator and magnitude bounds give the stated numerator bound, including reduced partial sums.

Schoolbook integer multiplication and elementary Euclidean normalization give the conservative bit bound O(A B_*^3). Faster integer algorithms improve this implementation bound without changing the program. Schedule checks add their stated finite scan costs. Membership using sorted prefix and residue lists costs O(b^2+b\log(s_H+1)) on b-bit heights with s_H stored entries. Historical retrieval also reads the complete encoded value. Per-instance accounting includes retrieved values in b_0. Whole-resolution accounting instead expands the finite ancestor closure and counts its complete graph.

For example, z_0=2/3 and z_{j+1}=z_jz_j produce z_d=2^{2^d}/3^{2^d} from d multiplication nodes. Repeated unary scaling by 1/3 also grows denominator size while d=0. The envelope therefore limits coefficients and intermediate sizes as well as graph depth. Preflight bounds and checks before each allocation prevent unbounded intermediate memory use within an admitted run.

3 Ordering resolutions and retaining unpaid amounts

A finite program orders its own arithmetic operations. References introduce a second ordering problem: one claim can need the result of another. A strictly historical reference always moves to a smaller height, so following prerequisites must eventually stop. This gives an evaluation order for the basic language. Section 7 later permits dependencies within one event when a complete certificate supplies their order.

The graph below draws an edge from a consumer to the prerequisite it reads. Evaluation follows those edges in reverse: it computes prerequisites first. This orientation differs from the argument-to-operation edges inside a payoff program.

Lemma 3.1 (Strict-forward-temporal DAG well-foundedness).

Let \mathcal{C} be a finite set of claims closed under every reference in its program cases, each with a finite program case table (Definition 2.17) whose selected payoff program (Definition 2.4) has reference leaves \mathrm{Ref}(c', \tau) carry strict-positive offsets \tau \geq 1 (Definition 2.1), well-formed at every instance in the sense of Definition 2.11. Let G_\mathcal{C} be the global dependency graph whose nodes are the claim instances (c, b) with c \in \mathcal{C} and b \in H_c, and whose edges run from (c, b) to (c', b - \tau), one for each reference leaf \mathrm{Ref}(c', \tau) of the program selected at that instance. Then G_\mathcal{C} is a directed acyclic graph graded by block height with well-founded descent: every edge strictly decreases the height, so no infinite descending chain of references exists, and the restriction of G_\mathcal{C} to any finite range of heights is finite.

Proof. We argue at two scales. Intra-program (within a single payoff program). Each payoff program is a finite DAG by Definition 2.4; acyclicity within a program holds by construction.

Inter-program (across instances). Every reference edge of G_\mathcal{C} runs from an instance (c, b) to (c', b - \tau) with \tau \geq 1, and b - \tau \in H_{c'} by the well-formedness condition of Definition 2.11, so the target is again a node of G_\mathcal{C} and its height is strictly smaller. Suppose for contradiction that G_\mathcal{C} contains a cycle (c_1, b_1) \to (c_2, b_2) \to \dots \to (c_K, b_K) \to (c_1, b_1) whose edges carry offsets \tau_1, \dots, \tau_K \geq 1, so that b_{i+1} = b_i - \tau_i for i < K and b_1 = b_K - \tau_K. Walking the cycle: b_1 \;=\; b_1 - \sum_{i=1}^{K} \tau_i, \qquad \text{hence} \qquad 0 \;=\; \sum_{i=1}^{K} \tau_i \;\geq\; K. This contradicts K \geq 1. The dependency graph contains no cycles.

The grading follows: block height is an \mathbb{N}-valued rank that strictly decreases along every reference edge, and \mathbb{N} is well-ordered, so no infinite descending chain of references exists; no edge, hence no path, joins two instances at one height. Each payoff program is finite, so each node has finite out-degree; restricting G_\mathcal{C} to a finite block-height window gives a finite DAG. Its edges run from an instance to the instances it reads, so listing the instances of each finite restriction by decreasing height is a topological order of that restriction. Evaluation follows the reverse order, increasing height, in which the instances of each height may be permuted freely. ◻

Corollary 3.2 (Resolution scheduling).

Given a finite set of claims, payoff evaluation proceeds in block-height order. By Lemma 3.1, an instance (c,b) reads only instances at lower heights. No edge joins two instances at one height. The instances at height b can therefore be evaluated in any order or concurrently after their own referenced instances and oracle inputs are available. Proposition 2.19 states the corresponding progress conditions. The resulting immutable entitlements retain their discharge journals independently under Definition 3.4.

Remark 3.3 (Resolution and discharge).

Resolution evaluates P and records the amount v_c(b). Discharge is the later satisfaction of the resulting entitlement through the external system and evidence rule in \mathit{ctx}. An instance can be resolved and remain undischarged. The finality rule belongs to that external system; the Principles for Financial Market Infrastructures define final settlement as the irrevocable and unconditional transfer of an asset or discharge of an obligation [49]. A later correction does not rewrite a resolved instance. It enters as a follow-on claim that references the earlier instance. Any dispute follows the governing clause in \mathit{ctx}.

3.1 Entitlements that survive payment failure

Consider a USD 10 coupon that carries missed coupons forward until a successful trigger. Two misses followed by a success produce a USD 30 amount owed. That success resets the counter for future calculations. A later payment of less than USD 30 must leave the unpaid part due, even though the counter has reset. Proposition 5.7 gives the recurrence that produces these amounts.

An entitlement records the debtor, creditor, and resolved amount independently of that computational state. Its identity must remain stable under retries and corrections. A discharge journal then records how much of the obligation has been satisfied.

Definition 3.4 (Immutable resolution entitlement).

An issuance, position lot, resolution height, and contractual leg determine the key \eta=(\mathit{issuance},\mathit{positionLot},b,\mathit{leg}). The registered leg fixes holder H, counterparty D, signed quantity q, settlement asset, and payment context. Resolution binds the exact issuance, program, position record, and input commitments. It records z_\eta=qv_c(b) and A_\eta=|z_\eta| under the exact rational interpretation. If z_\eta>0, D owes H. If z_\eta<0, H owes D. A zero amount has zero residual. An auxiliary claim without an external position creates no external entitlement.

The record also binds the discharge route, evidence predicate, governing rules, and payment window under the route’s named clock. Resolution inserts this record once. An identical retry returns it, while a conflicting record under the same key is rejected. Program revisions, reported amounts, or beneficiary attributes cannot create another key. An authorized assignment changes a separate effective-party record and preserves the original entitlement and ownership history. A correction creates a linked follow-on claim.

A physical occurrence is one recorded external receipt or debit. Its support is the quantity currently justified by its admitted evidence. Historical attribution records which entitlement already used that quantity. A later correction can reduce support while leaving this allocation history intact.

One receipt can pay part of one entitlement or portions of several. Its supported quantity must be allocated only once across them. The journal therefore links a legal discharge to an allocation from one shared receipt record. A signed discharge delta increases effective discharge when positive and reinstates an amount when negative.

Definition 3.5 (Discharge journal).

A legal-effect entry has a unique identifier, entitlement key, signed discharge delta, authority, and evidence. For entries accepted by cutoff t, define L_\eta(t)=\sum_{j\in\mathcal J_\eta(t)}\delta_j, \qquad B_\eta(t)=A_\eta-L_\eta(t), \qquad 0\leq L_\eta(t)\leq A_\eta. Here L_\eta is effective legal discharge and B_\eta is the outstanding amount. A payment of x requires a supported allocation of that quantity from the shared receipt ledger to this entitlement. Its witness binds the asset, parties, route, legal purpose, and required evidence. One atomic transition consumes the allocation and adds \delta=x, subject to x\leq B_\eta. An allocation supplies one consumption across all claims and account views. A reporter, command, assertion revision, or legal-origin label supplies no additional physical receipt.

The shared ledger partitions each supported receipt quantity among unallocated, reserved, attributed, and reconciliation-held slices. It retains the owner of every consumed slice. Loss of support identifies unsupported consumed slices without making them available for fresh allocation. Restored support returns to the same owner before any new allocation. An evidence revision alone supplies no legal discharge delta. An authorized reassignment transfers effective discharge x from entitlement \eta to entitlement \xi. One joint transition records deltas -x,+x, subject to x\leq L_\eta and x\leq B_\xi. It transfers the corresponding allocation and retains both histories. Ordinary spending changes the recipient’s current cash, while the receipt’s lifetime attribution remains unchanged.

A physical return or reversal has a distinct debit occurrence. The governing route can reinstate an amount through \delta=-x, with x\leq L_\eta, or create its specified recovery claim. The transition applies that legal consequence once. A quantity correction revises evidence about the original occurrence and creates no physical debit. Adverse evidence remains recordable even when it exposes a deficit or disputed attribution.

Payment-grid residuals remain explicit. For example, a 1/3 entitlement with a payment of 33/100 retains 1/300 due. A separate governing rounding rule can allocate that residual, but numerical precision alone cannot remove it. Replay reconstructs recorded entitlements and discharge entries without external dispatch.

A corrected observation or ruling can change the target amount while the original resolution remains an immutable fact of the record. A linked correction supplies the difference still needed to reach the current target. Each correction uses the latest accepted predecessor, preventing two concurrent corrections from both treating the same old total as current.

Definition 3.6 (Linked corrections).

Let z_0 be an immutable signed entitlement. An authenticated correction act sets target t_j in the same asset and account orientation. Its follow-on claim has amount d_j=t_j-z_0-\sum_{i<j}d_i. Acceptance atomically compares and advances the current correction head. Two successors of the same head cannot both commit. A repeated correction-act identifier returns its existing claim. Each corrective instance resolves after the instances that it reads, preserving strictly positive reference offsets. Every correction binds the governing authority and affected parties independently of current token balances. The signed portfolio then satisfies z_0+\sum_{i\leq j}d_i=t_j. Each entitlement retains its own residual until payment or an authorized set-off.

Proposition 3.7 (Entitlement preservation).

Under the shared allocation contract and the admitted transitions above, every accepted finite trace preserves one amount per origin key, A_\eta=L_\eta+B_\eta,\qquad B_\eta\geq0, one consumption per allocated quantity, and the linked correction identity. Replay has the same entitlement and allocation projections.

Proof. Resolution initializes L_\eta=0 and B_\eta=A_\eta. The immutable-key check prevents another amount under that key. Payment adds x to discharge and subtracts it from the residual, with x\leq B_\eta. Reinstatement reverses those two changes, with x\leq L_\eta. Both preserve the equation and nonnegativity. Reassignment applies the same bounded decrease and increase to its two entitlements while transferring one allocation. The joint allocation transition and retained consumption owner prevent duplicate use. Evidence corrections preserve the attribution history and require separate authority for legal changes. The protected correction head fixes the predecessor sum, and substitution proves the target identity. Replay folds the same accepted records and issues no commands. ◻

For a 10 coupon and triggers 0,0,1,1, resolution produces entitlements 30 and 10. A 35 receipt can discharge them by 30 and 5, leaving 5 due despite the memory reset. A second claim cannot allocate the same 35 again under another legal origin. For corrected targets 100\to80\to70, the linked amounts are -20,-10. Computing both corrections against the original would produce the wrong total 50, which the protected predecessor rule prevents.

Remark 3.8 (The historical reference profile).

The inequality \tau \geq 1 in Definition 2.1-(I3) prevents inter-claim same-block cycles. Allowing \tau = 0 admits two claims c, c' at the same height, each referencing the other. Each program remains internally acyclic, but the two instances form a cross-program cycle. The strict-positive offset extends acyclicity to the inter-program dependency graph. Example 10.3 gives the explicit counterexample. Because the graph contains instances rather than claim identifiers, two claims may reference each other at different heights without creating a cycle. The offset forbids every cycle among claim instances; it does not forbid those mutual references across time. The certified extension in Section 7 admits same-height dependencies whose complete graph has a strict local rank.

4 Exact expressiveness of \Sigma

The call has two regions: below the strike its payoff is zero, and at or above the strike its payoff is S_h-K. Both regional formulas are polynomials, and the comparison with the strike selects the region. Repeated arithmetic and comparisons produce the general class defined below.

For this numerical question, X_1,\dots,X_m are the variable external oracle and reference inputs. Constants remain fixed literal parameters. We temporarily erase financial annotations to obtain a function F:\mathbb{R}^m\to\mathbb{R}, \qquad f(\omega)=F\bigl(X_1(\omega),\dots,X_m(\omega)\bigr). Expressiveness concerns the functions F that this numerical language computes. Financial programs additionally satisfy Proposition 2.9. The exact rational execution profile uses rational literals, coefficients, and observations. Its function class has the corresponding rational polynomial coefficients.

4.1 The characterisation

The theorem has two directions. The construction shows that every function in the stated class has a program. The converse checks that none of the constructors leaves that class. Both are needed to characterize the language exactly.

Theorem 4.1 (Exact expressiveness).

Call F : \mathbb{R}^m \to \mathbb{R} piecewise-polynomial if there is a finite partition \mathbb{R}^m = \bigsqcup_{i=1}^N R_i, each cell R_i a finite intersection of regions \{x : g(x) \bowtie h(x)\} with g, h polynomials and \bowtie \in \{<,\leq,=,\geq,>\}, such that F agrees with a polynomial p_i on each R_i. Then:

(a): each piecewise-polynomial F has a payoff program in \Sigma over the leaves X_1, \dots, X_m;
(b): conversely, every payoff program in \Sigma computes a piecewise-polynomial function of its leaves.

\Sigma-programs therefore compute exactly the piecewise-polynomial payoffs.

Proof. (a) Construction. Three steps: polynomial sub-programs, region sub-programs, assembly.

Step 1 (polynomials). Every nonzero polynomial p_i \in \mathbb{R}[X_1, \dots, X_m] decomposes into monomials, p_i(X_1, \dots, X_m) \;=\; \sum_\alpha c_\alpha \prod_{j=1}^m X_j^{\alpha_j}, \qquad \alpha \in \mathbb{N}^m, \;\; |\alpha| \leq d_i. For |\alpha|=0, the monomial is \mathrm{Const}(1). For |\alpha|\geq1, repeat each leaf X_j exactly \alpha_j times and multiply the |\alpha| factors; this uses no \mathrm{Mul} node at degree one and |\alpha|-1 nodes at higher degree. A single \mathrm{LinComb} with the coefficients c_\alpha forms the sum. The zero polynomial is \mathrm{Const}(0). Shared sub-monomials are computed once in SSA form.

Step 2 (regions). Each cell R_i = \bigcap_{k=1}^{K_i} \{g_{i,k} \bowtie_{i,k} h_{i,k}\} has indicator b_i \;=\; \prod_{k=1}^{K_i} \mathbb{1}[g_{i,k} \bowtie_{i,k} h_{i,k}], where each atomic indicator is \mathrm{Ind}(\bowtie_{i,k}, g_{i,k}\text{-prog}, h_{i,k}\text{-prog}) over the Step-1 sub-programs. For K_i\geq1, the product is a balanced \mathrm{Mul}-tree of depth \lceil \log_2 K_i \rceil; for the empty intersection, set b_i:=\mathrm{Ind}(=,\mathrm{Const}(0),\mathrm{Const}(0)). On every x, b_i(x) \in \{0,1\} and b_i(x) = 1 iff x \in R_i.

Step 3 (assembly). Since the R_i partition \mathbb{R}^m, exactly one b_i = 1 at every x, so F \;=\; \mathrm{LinComb}\bigl(1, \dots, 1; \;\mathrm{Mul}(b_1, p_1), \;\dots, \;\mathrm{Mul}(b_N, p_N)\bigr) computes F exactly. The result is a finite SSA-form DAG over \Sigma.

(b) Structural induction. Order the nodes of a program P topologically and show, node by node, that the function computed at each node is piecewise-polynomial in the leaves, with cells cut out by finitely many polynomial inequalities.

Leaves. \mathrm{Const}(c) computes the constant polynomial c; \mathrm{Oracle} and \mathrm{Ref} leaves compute coordinate functions. Trivial partition.
\mathrm{LinComb}, \mathrm{Mul}. Take the common refinement of the argument partitions: a finite partition whose cells are intersections of cells, hence again finite intersections of polynomial-inequality regions. On each cell every argument is a polynomial, and linear combinations and products of polynomials are polynomials.
\mathrm{Ind}(\bowtie, e_1, e_2). Refine the two argument partitions; on a cell where e_1 = g and e_2 = h, split into the sub-cell \{g \bowtie h\} (value 1) and the sub-cells of the complementary relation (value 0). The complement of one polynomial relation is a union of at most two polynomial relations (for instance the complement of = is < together with >), so every sub-cell is again a finite intersection of polynomial-inequality regions.
\mathrm{Cap}(e, u), \mathrm{Floor}(e, l). On each cell where e = g, split by \{g \leq u\} (value g) and \{g > u\} (value u); symmetrically for \mathrm{Floor}.
\mathrm{IfElse}(b, e_+, e_-). The node emits b\,e_+ + (1-b)\,e_-, a polynomial in three piecewise-polynomial arguments; refine and conclude as for \mathrm{LinComb} and \mathrm{Mul}.

The root node therefore computes a piecewise-polynomial function of the leaves. ◻

Remark 4.2 (Measurability and boundedness).

Measurability is automatic: every cell is a finite intersection of polynomial-inequality regions in measurable leaves, hence measurable, and every representable payoff is therefore measurable. Boundedness (Remark 2.2) is a separate admissibility condition for a stated collateral or risk rule. It depends on the leaf ranges and the program, and the characterisation above is independent of it.

4.2 Minimality within the stated vocabulary

Some operations make programs easier to write even though the others can express them. For example, comparisons can select either an argument or a fixed bound. The minimality question asks which constructors remain necessary if we remove operations from this particular vocabulary.

Fix the numerical sorts, Boolean inclusion, constructor signatures, and parameters of Definition 2.3. Compare sublanguages obtained by deleting constructors from \Sigma. An encoding preserves its declared external-input categories and identifiers and agrees for every independent real valuation. Oracle and reference leaves remain opaque accesses. Encodings add no proxy attestations and do not inline referenced claims. The comparison includes programs with zero external inputs. Financial typing and evidence preservation remain separate obligations after numerical elaboration.

Proposition 4.3 (Derived operators and relative minimality).

Let \Sigma_0 := \{\mathrm{Const}, \mathrm{Oracle}, \mathrm{Ref}, \mathrm{LinComb}, \mathrm{Mul}, \mathrm{Ind}\}.

(i): \mathrm{Cap}, \mathrm{Floor}, and \mathrm{IfElse} are definable over \Sigma_0. Abbreviating u' := \mathrm{Const}(u), l' := \mathrm{Const}(l), g_{\bowtie} := \mathrm{Ind}(\bowtie, e, u'), and g'_{\bowtie} := \mathrm{Ind}(\bowtie, e, l'): \begin{align*} \bar b &:= \mathrm{LinComb}\bigl(1, -1;\; \mathrm{Const}(1),\, b\bigr), \\ \mathrm{Cap}(e, u) &= \mathrm{LinComb}\bigl(1, 1;\; \mathrm{Mul}(g_{\leq},\, e),\; \mathrm{Mul}(g_{>},\, u')\bigr), \\ \mathrm{Floor}(e, l) &= \mathrm{LinComb}\bigl(1, 1;\; \mathrm{Mul}(g'_{\geq},\, e),\; \mathrm{Mul}(g'_{<},\, l')\bigr), \\ \mathrm{IfElse}(b, e_+, e_-) &= \mathrm{LinComb}\bigl(1, 1;\; \mathrm{Mul}(b,\, e_+),\; \mathrm{Mul}(\bar b,\, e_-)\bigr). \end{align*} Hence \Sigma and \Sigma_0 compute the same class, and \Sigma_0 is the unique inclusion-minimal equivalent subset of this vocabulary.
(ii): Each of \mathrm{Oracle}, \mathrm{Ref}, \mathrm{LinComb}, \mathrm{Mul}, \mathrm{Ind} is necessary: removing it from all nine constructors of \Sigma strictly shrinks the computed class under the stated comparison.
(iii): \mathrm{Const} is necessary for programs with zero external inputs. Over any leaf set containing some leaf \ell, constants are derived: c = \mathrm{LinComb}(c;\, \mathrm{Ind}(=, \ell, \ell)). The fixed-payment claim — a payoff using no oracle and no reference — is representable only with \mathrm{Const}, because a program must contain at least one arity-zero node.

Proof. (i) Direct evaluation gives the stated cap, floor, and conditional formulas. The fixed Boolean inclusion permits each indicator in a numeric multiplication.

(ii) Consider deletion from the entire nine-constructor vocabulary. Without an oracle or reference constructor, programs cannot distinguish two valuations differing only at that corresponding opaque input. The missing coordinate function distinguishes those valuations.

Without \mathrm{LinComb}, each numeric program selects among finitely many monomials. Constants and input coordinates have this property, multiplication preserves it, and caps, floors, and conditionals only select from existing expressions or literal bounds. Indicators select zero or one. For one free input x, each equality c x^k=x+1 has finitely many solutions. A finite collection cannot cover all real x.

Without \mathrm{Mul}, the same induction gives a finite selection of affine functions. No finite selection of affine functions equals x^2 on the whole real line. Without \mathrm{Ind}, no remaining constructor produces a Boolean, so a well-typed conditional cannot occur. The remaining numeric operators preserve continuity and cannot compute \mathbb{1}[x\geq0].

(iii) With an external leaf \ell, the displayed numerical constant formula equals c. With zero external inputs and no \mathrm{Const}, no available constructor can supply a leaf. Every equivalent vocabulary subset must therefore contain all six members of \Sigma_0. Part (i) proves their sufficiency, which gives the stated unique inclusion-minimal subset. Dimensioned constants additionally require their manifest declarations. ◻

The following scope statement concerns the historical reference profile defined so far. Its restriction on same-height references applies without a complete dependency certificate. Section 7 constructs the separate acyclic same-event profile. The remaining genuinely cyclic case requires fixed-point semantics.

Remark 4.4 (Scope).

This paper characterises exact piecewise-polynomial payoffs over scheduled oracle and prior-claim inputs, four historical reductions, and three convex forms of price formation. The reductions supply discrete extrema, totals, and averages. Log-return statistics and smooth indicators can enter as oracle-attested values or through an analytic extension. Continuous-time observations enter through an attested aggregate. Vanilla call and put payoffs already belong to \Sigma; a closed-form Black-Scholes-Merton price additionally needs the normal cumulative distribution function. Order-driven venues use the same claim representation with their own price-formation rule. Cross-claim references remain strictly historical; a same-height reference requires a separate fixed-point semantics.

5 Path-dependent payoffs: the window-reduction leaf

An option can depend on several observations rather than one terminal price. An Asian option uses an average [32], while a lookback uses an extremum [26]. A barrier option tests whether that extremum crossed a threshold [42, 31]. A range accrual totals observations satisfying a condition. These calculations need both the selected historical dates and a rule for reducing their values.

At height six, suppose the source schedule contains only heights one, three, and five, with values 100,120,80. A five-height historical window selects all three values and has average 100. If the height-three value is missing, the average must wait for it. Averaging only the available values would change the promised calculation. The later currency example in Section 6.4 uses this same sparse history.

When every height has a source value, W fixed references already compute a window statistic with O(W) syntax. The window leaf packages this selection and reduction in one node, while retaining its historical reads. A memory coupon needs an additional state: the number of consecutive misses since the preceding success. After the window construction, the pre-issued recurrence supplies this reset state.

5.1 Definition

Definition 5.1 (The window-reduction operator).

Fix a bounded window parameter W_{\max} \in \mathbb{N}. The window-reduction operator \mathrm{RefReduce}(c', W, \rho) (arity 0; parameters a referenced claim c', a window length W \in \{1, \dots, W_{\max}\}, and a reduction kind \rho \in \{\mathrm{Min}, \mathrm{Max}, \mathrm{Sum}, \mathrm{Avg}\}), evaluated at block height h \geq W + 1, emits \mathrm{RefReduce}(c', W, \rho)(h) \;=\; \rho\bigl(\,\{\, v_{c'}(b) \;:\; b \in [h-W,\, h-1] \cap H_{c'} \,\}\,\bigr), where v_{c'}(b) is the sample value carried by the instance of c' at height b (Definition 2.11), the reduction is taken over the multiset of values the schedule H_{c'} places in the window, and \rho is respectively the minimum, maximum, sum, or arithmetic mean of that multiset. Selected records have one common dimension and scale. The reduction returns that sample type and retains every selected source identifier, original context, and height. The node is well-formed exactly when [h-W,\, h-1] \cap H_{c'} \neq \emptyset, as decided for every case by Proposition 2.18. For a given instance, the schedule representation of Definition 2.11 decides this condition with at most W membership tests. The window is strictly historical — every read targets h - \tau with \tau \in \{1, \dots, W\} — so the offset discipline of Definition 2.1 is preserved.

Remark 5.2 (The window bound).

W_{\max} is a fixed resource bound. Counting arithmetic operations and indexed reads, one \mathrm{RefReduce} evaluation uses at most W constant-time membership tests and historical reads, hence O(W) work. With membership cost T_H and retrieval cost T_R, the access cost is O(W(T_H+T_R)). The arithmetic bit cost is added separately under Section 2.6. The operator defined here does not represent windows longer than W_{\max}. Such windows require a larger bound or a separately defined stateful aggregate. General nesting is insufficient because intermediate windows can overlap, which changes sums and averages.

5.2 The function class after adding windows

A window produces one numerical input for the surrounding program. The closure result first treats each aggregate as a leaf and applies the existing expressiveness theorem. The following compilation result then opens that leaf and shows how finite program cases recover its selected historical reads.

Proposition 5.3 (Window-reduction closure).

Let \Sigma' := \Sigma \cup \{\mathrm{RefReduce}\}. Programs in \Sigma' compute exactly the piecewise-polynomial payoffs over the leaf set of Theorem 4.1 extended by the window aggregates \mathrm{RefReduce}(c', W, \rho) of Definition 5.1, with \rho \in \{\mathrm{Min}, \mathrm{Max}, \mathrm{Sum}, \mathrm{Avg}\} and W \leq W_{\max}.

Proof. Each window aggregate is one \mathrm{RefReduce} node, and each \mathrm{RefReduce} node emits one real value at each evaluation height, exactly as the other arity-zero leaves do. Both directions of Theorem 4.1 therefore apply over the extended leaf set: the three-step construction of part (a) builds any piecewise polynomial of the extended leaves, and the structural induction of part (b) gains one base case — a \mathrm{RefReduce} node computes a coordinate function of the extended leaf-space — and is otherwise unchanged. Boundedness is preserved: for bounded resolved values, \mathrm{Min}, \mathrm{Max}, and \mathrm{Avg} are bounded by \max_b |v_{c'}(b)|, and \mathrm{Sum} by W_{\max} \max_b |v_{c'}(b)|. ◻

Remark 5.4 (Program size and schedule adaptivity).

Over an underlying resolving at every height of the window, \Sigma' adds no payoffs: each aggregate is itself a \Sigma-payoff of the fixed leaves \mathrm{Ref}(c', 1), \dots, \mathrm{Ref}(c', W) — \mathrm{Sum} and \mathrm{Avg} are one \mathrm{LinComb}, \mathrm{Max} and \mathrm{Min} are W - 1 nested binary extrema (\mathrm{IfElse} on \mathrm{Ind}). The extension is conservative there and reduces program size from O(W) to O(1) while retaining O(W) reads. For a fixed-program case with consumer schedule H_c and target claim c', define the admissible fixed-offset set D(c,c'):=\{\tau\in\mathbb{N}_{\geq1}:H_c-\tau\subseteq H_{c'}\}, \qquad H_c-\tau:=\{b-\tau:b\in H_c\}. One fixed leaf \mathrm{Ref}(c',\tau) is well-formed at every instance of c exactly when \tau\in D(c,c'). Thus nonidentical schedules can admit a fixed offset; translated schedules are the simplest case. For a single fixed program, the window leaf adapts when D(c,c')=\varnothing but [b-W,b-1]\cap H_{c'} is nonempty for every b\in H_c. Finite program-case refinement can instead represent those changing offset patterns, as proved below. It re-selects the historical instances at each evaluation, and \mathrm{Avg} divides by their number (Definition 5.1). For a one-shot claim, fixed offsets can hit any known finite set of earlier instances, so only the program-size reduction remains.

Proposition 5.5 (Compiling bounded windows into program cases).

For the admitted ultimately periodic schedules, every program with bounded window reductions has an equivalent finite table of fixed-offset \Sigma programs. The window form represents the same computation with one reduction node per window instead of its expanded cases and reads.

Proof. Fix every window in a selected program case. Below the largest shifted schedule cutoff, finitely many heights determine finitely many selected-offset patterns. Above it, all relevant schedule memberships repeat with the least common multiple of their periods. A finite partition into prefix heights and tail residue classes therefore fixes the selected offsets of every window. In each partition cell, replace a reduction by its selected fixed-offset references and ordinary sum, average, or extremum program. The averaging coefficient is the reciprocal of the fixed selected count in that cell. The cells are disjoint and cover the original schedule, so the resulting case table computes exactly the same values. It also retains the same selected input evidence. ◻

For consumer heights h\geq3, odd source heights, and window W=2, the selected set always contains one height. An odd-height case reads offset two, and an even-height case reads offset one. One window node expresses both cases while preserving the same observations. The representation saves case expansion, although its evaluation still performs the declared membership and retrieval work.

Example 5.6 (The path-dependent catalogue).

Historical price and reference reads below use sample mode. In (P1)–(P3), each displayed formula is a per-unit sample output F_i. Its financial root is \mathrm{Mul}(\mathrm{Const}(N_i),F_i), where the declared underlying quantity carries the payment context. Unit quantities have represented value one. Trigger values and miss counters have neutral types. Contractual coupon and quantity declarations supply each instance’s payment-context type. Five product families compile into \Sigma' through constant-size sub-programs. In each the referenced claim resolves at every block of the window, so the aggregate reads a full sample path; a sparser schedule aggregates every height prescribed by that schedule, awaiting any missing selected value (Definition 5.1).

(P1): Asian option on underlying claim c_S with strike K and averaging window W [32]: \begin{align*} \bar{S}_W &:= \mathrm{RefReduce}(c_S, W, \mathrm{Avg}), \\ \text{payoff} &= \mathrm{Floor}\bigl(\mathrm{LinComb}(1,-1; \bar{S}_W, \mathrm{Const}(K)),\, 0\bigr). \end{align*}
(P2): Lookback option (Goldman-Sosin-Gatto [26]) with window W: \begin{align*} S_W^{\max} &:= \mathrm{RefReduce}(c_S, W, \mathrm{Max}), \\ \text{payoff} &:= \mathrm{LinComb}(1, -1;\, S_W^{\max},\, \mathrm{Ref}(c_S, 1)). \end{align*} emitting S_W^{\max} - S_{h-1}, the floating-strike put; the floating-strike call pairs \mathrm{Ref}(c_S, 1) with the \mathrm{Min} reduction, and the fixed-strike call is \mathrm{Floor}(S_W^{\max} - K, 0).
(P3): Discrete knock-in barrier option with barrier B, strike K, window W [42, 31]: \begin{align*} S_W^{\max} &:= \mathrm{RefReduce}(c_S, W, \mathrm{Max}), \qquad b := \mathrm{Ind}(\geq, S_W^{\max}, \mathrm{Const}(B)), \\ \text{vanilla} &:= \mathrm{Floor}\bigl(\mathrm{LinComb}(1,-1;\, \mathrm{Ref}(c_S,1),\, \mathrm{Const}(K)),\; 0\bigr), \\ \text{payoff} &= \mathrm{IfElse}(b,\; \text{vanilla},\; \mathrm{Const}(0)). \end{align*} Knock-out is symmetric with \mathrm{IfElse}(b, \mathrm{Const}(0), \text{vanilla}); floor barriers use the \mathrm{Min} reduction.
(P4): Memory-coupon schedule. Fix coupon heights h_1<\cdots<h_K, coupon amount c>0, and trigger threshold \theta. The reset rule below matches disclosed notes under which a paid missed coupon cannot be paid again [41]. Before the first observation, issue one-shot coupon-payoff claims y_1,\ldots,y_K and auxiliary one-shot state claims m_0,\ldots,m_K. Choose h_0<h_1, set H_{m_0}=\{h_0\}, and give m_0 the program \mathrm{Const}(0). For j\geq1, set H_{m_j}=H_{y_j}=\{h_j\}, put d_j=h_j-h_{j-1}>0, and abbreviate \begin{align*} b_j&:=\mathrm{Ind}\bigl(\geq,\mathrm{Oracle}(S,0),\mathrm{Const}(\theta)\bigr),\\ r_{j-1}&:=\mathrm{Ref}(m_{j-1},d_j),\\ P_{m_j}&:=\mathrm{IfElse}\bigl(b_j,\mathrm{Const}(0), \mathrm{LinComb}(1,1;\mathrm{Const}(1),r_{j-1})\bigr),\\ P_{y_j}&:=\mathrm{IfElse}\bigl(b_j, \mathrm{Mul}(\mathrm{Const}(c), \mathrm{LinComb}(1,1;\mathrm{Const}(1),r_{j-1})), \mathrm{Const}(0)\bigr). \end{align*} Every claim identifier, schedule, offset, and program is fixed before h_1; no claim is created after observing a trigger. The auxiliary claims carry the state but no external position. Each state or coupon-payoff program has O(1) nodes, while the complete pre-issued family has O(K) claims.
(P5): Range accrual over a corridor [L, U]: an underlying claim c_{\text{in}} carries the in-corridor indicator program \mathrm{Mul}\bigl(\mathrm{Ind}(\geq, \mathrm{Ref}(c_S, 1), \mathrm{Const}(L)),\, \mathrm{Ind}(\leq, \mathrm{Ref}(c_S, 1), \mathrm{Const}(U))\bigr), and the accrual \mathrm{Mul}\bigl(\mathrm{RefReduce}(c_{\text{in}}, W, \mathrm{Avg}),\, \mathrm{Const}(c)\bigr) pays the per-window coupon c scaled by the fraction of in-corridor blocks.

Proposition 5.7 (No missed coupon enters two resolved payoffs).

In the pre-issued family of Example 5.6-(P4), let B_j\in\{0,1\} be the realised value of b_j. Then v_{m_j}(h_j) equals the number of consecutive failed triggers ending at j. If B_j=1, v_{y_j}(h_j) includes the current coupon and exactly those consecutive missed coupons since the preceding success. At the payoff-evaluation layer, no missed coupon enters two resolved payoffs: each enters the resolved value of at most one coupon-payoff claim. Discharge remains separate under Remark 3.3.

Proof. Write M_j:=v_{m_j}(h_j). The initial value is M_0=0. The program gives M_j=0 when B_j=1 and M_j=M_{j-1}+1 when B_j=0. Induction therefore identifies M_j with the length of the failed run ending at j. At a success j, the resolved payoff is c(1+M_{j-1}), which contains the current coupon and the failed run immediately before it. The same success sets M_j=0, so no member of that run can enter a later resolved payoff. A failed coupon with no later success remains absent from every resolved payoff; otherwise it enters the first later successful payoff exactly once. ◻

Corollary 5.8 (Coupon memory and persistent residuals).

For each registered coupon position, a successful trigger creates its immutable entitlement while resetting the state counter. Partial payment changes that entitlement’s residual and leaves the resolved counter unchanged. Every unpaid amount therefore remains due in its original entitlement.

Proof. The recurrence reads triggers and previous state claims. The discharge journal supplies none of those inputs. Its residual instead uses the immutable coupon amount and accepted payment effects. Each transition preserves the other’s recorded values. ◻

Example 5.9 (An initialized infinite coupon family).

Fix h_0,\Delta\geq1 and H^+=\{h_0+j\Delta:j\geq1\}. A state claim m uses a seed case \{h_0\}\mapsto0 and a repeated case H^+\mapsto\mathrm{IfElse}(b,0,1+\mathrm{Ref}(m,\Delta)). The coupon claim y has schedule H^+ and program \mathrm{IfElse}\bigl(b,c(1+\mathrm{Ref}(m,\Delta)),0\bigr), \qquad b=\mathrm{Ind}(\geq,\mathrm{Oracle}(S,0),\theta). These formulas abbreviate the corresponding \Sigma constructors. All identifiers, cases, and programs are fixed at issuance. Both repeated programs read the preceding state, so same-height evaluation remains independent. Proposition 2.18 admits the complete recurring family. The preceding induction proves the same missed-coupon property at every finite height. Its payment amount carries the instance’s declared maturity context, while the state counter has the neutral type.

5.3 What an aggregate forgets

Minimum, maximum, sum, and mean do not retain every interior observation value. For example, the samples \{0,1,2,7,10\} and \{0,1,4,5,10\} have equal values for all four aggregates. Their medians differ. The next remark separates this loss of information from the language’s ability to compute a rank statistic when every original sample remains an input.

Remark 5.10 (Expressive limit of the four reductions).

\mathrm{Min} and \mathrm{Max} carry the lookback and barrier families; \mathrm{Sum} carries accruals and within-window totals; \mathrm{Avg} carries time-averaging. Over a fully resolved window \mathrm{Avg} equals \mathrm{Sum} scaled by 1/W; it is a separate kind because source schedules may be sparse, and \mathrm{Avg} divides by the number of scheduled heights selected by the window, not by W. Every selected value must be available before evaluation.

The memory schedule of Proposition 5.7 instead carries a reset state through strict-positive references.

Median, p-quantiles, and mode are not functions of these four reductions. Over a fully resolved window they are \Sigma-payoffs of the fixed leaves X_j := \mathrm{Ref}(c', j), j = 1, \dots, W: the stable rank r_i of X_i and the k-th smallest value X_{(k)} are \begin{align*} r_i &:= \#\{j : X_j < X_i\} + \#\{j < i : X_j = X_i\}, \\ X_{(k)} &= \sum_{i=1}^{W} \mathrm{Mul}\bigl(X_i,\; \mathrm{Ind}(=, r_i, \mathrm{Const}(k-1))\bigr), \end{align*} where each r_i is a \mathrm{LinComb} of \mathrm{Ind} nodes, the ranks form a permutation of \{0, \dots, W-1\}, and the whole is a program of O(W^2) nodes; quantiles select by rank, and the mode selects by multiplicity in the same way once a tie rule fixes which of the values of maximal multiplicity it returns, for instance the least.

The four reductions do not provide constant-size rank statistics or schedule-adaptive rank selection. For every W \geq 5 no program over the four aggregates of a window computes the median (at W \leq 3 it is one of the four or \mathrm{Sum} - \mathrm{Min} - \mathrm{Max}, and at W = 4 the midpoint of the two middle values is half of that), since for W = 5 the samples \{0,1,2,7,10\} and \{0,1,4,5,10\} share minimum, maximum, sum, and mean and have medians 2 and 4, and padding both samples with one shared value 3 when W is even and then with shared pairs \{0, 10\} carries the witness to every larger W.

The fixed-leaf program reads at fixed offsets, so it binds to one schedule (Remark 5.4). A constant-size form when the finite-offset set is empty therefore needs a rank-selecting reduction kind or an oracle-side projection that attests the statistic directly (Remark 4.4).

Historical aggregation must also preserve the dependency order. Expanding a window adds several reference edges, but each still points to an earlier height. The same decreasing-height argument therefore applies to every selected member.

Corollary 5.11 (\mathrm{RefReduce} preserves DAG well-foundedness).

Let G_\mathcal{C} be the dependency graph of Lemma 3.1 extended to include the reference edges of \mathrm{RefReduce}(c', W, \rho) nodes. Such a node in the program of an instance (c, h) contributes one edge to each instance (c', b) with b \in [h-W,\, h-1] \cap H_{c'}, so every contributed edge carries an offset h - b \in \{1, \dots, W\}, all strictly positive. Block height therefore still strictly decreases along every edge, the argument of Lemma 3.1 carries through unchanged, and G_\mathcal{C} is a DAG graded by block height with well-founded descent.

Proof. \mathrm{RefReduce} nodes contribute reference edges only at offsets \tau \in \{1, \dots, W\}, all \geq 1. The cycle-walk of Lemma 3.1 sums the offsets around a putative K-cycle; since every offset is \geq 1, it still yields 0 = \sum_i \tau_i \geq K, a contradiction. Every \mathrm{RefReduce} edge strictly decreases block height, so the grading is unaffected. ◻

6 Suspended evaluation and durable entitlements

A coupon can await an observation while another claim resolves. Its evaluator must save the calculations already completed and the inputs still missing. This saved unfinished computation is its continuation. When the missing evidence arrives, evaluation resumes from that continuation.

Payment adds a second requirement. A process can stop after recording payment but before returning its response. Retrying the same request must return the recorded outcome while preserving the amount already paid. The evaluator below composes numerical values, financial types, schedules, and entitlements. The transaction construction then saves its continuation with the current payment ledger and command outcomes.

6.1 Admitted programs and suspended values

Definition 6.1 (Executable program).

An executable program fixes a finite collection of named claims, oracle contracts, issuance declarations, position lots, and one evaluation-context identifier. Each claim supplies the schedule and finite case table of Definition 2.11. Each case contains a finite shared expression graph over all nine constructors of \Sigma and \mathrm{RefReduce}. The financial interfaces additionally admit \mathrm{Rescale} and \mathrm{Convert} from Section 2.3. Both historical reference modes, sample and amount, retain their stated meanings. All four window reductions are admitted. Literal names bind immutable declarations. Every conversion names an exact rate, direction, target type, and current-use witness. A rate can be declared, observed, or obtained from a strictly historical claim reference. The latter reference belongs to the dependency graph even though it is metadata on the conversion node.

The executable interface represents linear-combination coefficients and cap or floor bounds by typed expression children. Literal children recover the nine-constructor syntax exactly. Dimensionless coefficient expressions abbreviate multiplication followed by addition. Expression bounds abbreviate a comparison and conditional selection. These forms therefore preserve the numerical function class of Theorem 4.1. They retain all child evidence under the financial rules. No special coupon or foreign-exchange instruction is added.

At construction, a traversal emits each shared expression node once, after its children. The result is a sequence of single-assignment instructions with explicit operand indices. Schedule admission examines every selected case and every nested temporal dependency, including both conditional branches and conversion-rate references. An instance request (c,h) expands its finite historical ancestor closure. Its height-specific type check instantiates declared maturity parameters and checks every instruction before evaluation. This check applies to requested instances, while schedule admission covers the complete recurring schedule.

A cached value stores a completed intermediate calculation for reuse. It must retain more than the numerical interval: its units, original historical records, and conversion witnesses remain necessary to justify the final amount. The state below records these components separately so resumption can preserve them together.

Definition 6.2 (Suspended evaluator state).

For a fixed program, the state consists of requested instances, expanded instruction sequences, cached values, pending dependencies, admitted observations and witnesses, resolved records, and resource counters. A cached numerical value is V=(I,\theta,E,H,W),\qquad I=[l,u],\quad l,u\in\mathbb{Q},\quad l\leq u. Here \theta is its financial type, E is its declaration and observation evidence, H is its historical-read evidence, and W is its conversion-witness evidence. An exact value has l=u. A historical-read record retains the source claim, height, resolution identity, and original type. A Boolean cache entry contains a certified truth value or an unresolved comparison. An unavailable operand leaves the instruction pending with the dependency or deadline action that explains it.

The evaluator visits instances in increasing height and name order, then visits their instructions in operand order. It retains completed instructions when another instruction awaits evidence. The conditional waits for its guard and both branch values because the financial rule retains both branches’ evidence. An independent ready branch can still be calculated and cached during that wait. An ambiguous comparison remains unresolved through every dependent expression. An interval refinement must be contained in the admitted interval and must carry admissible evidence. It invalidates affected pending computation while retaining immutable exact resolutions. These rules allow useful progress without interpreting missing evidence as zero or an unresolved comparison as false.

The local proofs now combine along one evaluation order. The reference rules put source resolutions first. The arithmetic and typing rules then propagate value, type, and evidence through each instruction. The proposition’s exact-root condition determines when this computation may create an entitlement.

Proposition 6.3 (Composed evaluation preservation).

Fix an admitted program and requested instances with valid height-specific type derivations. Suppose declarations, observations, historical records, and conversion witnesses satisfy their named admission and current-use predicates. Each completed numerical instruction encloses its denotational value. Each certified Boolean instruction agrees with its exact predicate. Every cached record retains its derived type and required transitive evidence. Every committed root is an exact amount in its declared type. For a root represented by v with scale s and signed position q, the canonical amount is qsv. Its immutable entitlement identity is the identity of Definition 3.4. Resumption preserves previously resolved amounts and unpaid balances. For a fixed initial state, admitted inputs, witness sequence, envelopes, and command order, the resulting state is deterministic.

Proof. Order cross-claim instances by height and each instance’s instructions by operand order. Every reference and selected window member precedes its consumer by Lemma 3.1 and the strict historical-window rule. Constants and admitted oracle values satisfy the enclosure and type assertions directly. A reference copies its resolved value and appends the source identity and original type. A sample reference removes only the working maturity context. A window applies the stated finite reduction to exactly the selected records and retains all their evidence.

For an arithmetic instruction, Proposition 2.14 and Proposition 2.16 supply numerical preservation. The financial typing rules supply its result type. Multiplication combines dimensions and contexts, and linear combination requires matching summands and dimensionless coefficients. Cap, floor, and comparison require matching operand types. A certified comparison agrees with the predicate throughout the operand enclosures. An ambiguous comparison supplies a pending cache record and no Boolean denotation. A certified conditional selects one branch’s numerical enclosure and retains evidence from all three children. An unresolved guard yields no branch result. Rescaling changes the represented number by the exact ratio of scales. Conversion checks its source, target, rate, direction, and current-use witness before applying the typed exact factor. Each case unions the children’s evidence with its own required record, which proves transitive retention by induction.

Only a singleton numerical root can enter the entitlement binding. Multiplication by its scale and position gives the canonical directed amount qsv. Preflight checks all position identities before the ledger transition. An identical binding returns its existing record, while a conflicting binding is rejected. Proposition 3.7 then preserves unpaid amounts through later payment and correction transitions. Pending instructions create no amount by default. All traversals, reductions, exact operations, and admission checks have fixed inputs and order, so their composed transition is deterministic. ◻

6.2 Cumulative resource accounting

An admitted envelope bounds scalar bit length, primitive work, cumulative number-size charges, graph nodes, argument edges, expanded instances, window width, input bytes, and schedule-admission horizon. Let b be the scalar-bit limit, w the consumed primitive-work counter, and n the consumed number-size counter. These are explicit algorithm counters, rather than elapsed time or peak memory measurements. The reference evaluator uses the following charges.

Operation	Charge and admission rule
Instruction, type step, or window membership	Increase w before the step.
Integer parsing, addition, or multiplication	Increase w and charge b to n before the bounded operation.
Euclidean remainder step	Increase w and charge 2b to n.
Retained provenance record occurrence	Charge 256 to n when combining evidence.
Expanded graph and observations	Check cumulative node, edge, instance, and encoded-input limits.
Schedule construction	Bound the finite admission scan before it runs and include its membership bound in w.

Dimension and context exponents and dynamic scale calculations use the same bounded arithmetic interface. Static program metadata is bounded before admission. A failed charge stops the affected step and retains earlier charges and completed values. A larger envelope can resume the state, with every limit at least its preceding value and with w,n unchanged at admission. Cached completed instructions need no second evaluation unless an admitted refinement requires recomputation of pending work. The bit-cost result of Section 2.6 describes mathematical arithmetic cost. The counters here specify the concrete evaluator’s stopping policy. The number-size charge is a conservative accounting unit for named allocations, not a bound on all Python objects or encoding temporaries. Serialized command and checkpoint size limits separately bound accepted encodings.

6.3 One durable state and its commands

Suppose a saved coupon calculation predates the USD 35 payment against the USD 30 and USD 10 entitlements. Restoring the whole old snapshot would lose that payment and incorrectly restore the old unpaid balances. Resumption must therefore use the current shared ledger while retaining the saved calculation.

A continuation lineage identifies successive accepted states of one calculation. Its head is the current accepted revision, and a handle identifies the revision a caller intends to use. A command identifier binds a request to its stored result, allowing a retry to return that result after a lost response. The state below stores these identities with the current ledger: S=(r,L,J,I,D). Here r is the store revision, L is the complete entitlement and resource ledger, and J maps continuation lineages to current revisions. For each instance name i, I(i) contains its fixed program and context identities, handle revision \nu_i, and authenticated evaluator continuation. The command map D binds (i,k) to one exact request and its stored outcome, where k is a caller-supplied command identifier.

The ledger serialization retains map insertion order as ordered key-value sequences. This order matters when a quantity correction reduces support for several earlier allocations. Historical ownership and support priority must survive restoration together. The continuation authenticates its own payload and checks that retained immutable ledger records still exist. Restoration uses the current complete ledger, including intervening payments from other program instances.

An allowed evaluator command requests an instance, supplies an observation or conversion witness, or runs ready work. An allowed ledger command records a credit or alias, allocates performance, records a return, reopens an entitlement, corrects a target or quantity, reserves cash, or records a cash spend. These commands operate on the ledger model. Their external facts and legal permissions are supplied through the stated admission predicates. A reservation retains its encumbrance in the current implementation. Settlement or release of that reservation requires an additional specified transition.

The ledger retains historical attribution when a correction or return reduces its present physical support. For an occurrence o, let s_o be its current nonnegative support and let a_o be its total historical allocation. A new allocation \delta must satisfy 0<\delta\leq\max(s_o-a_o,0). After support decreases, a_o>s_o can hold. The ledger reports the shortfall against the existing owners instead of making their historical capacity available again. For one account and asset, write C for booked cash, R for reservations, and E for other encumbrances. Available cash and its deficit are F=\max(C-R-E,0),\qquad \Delta=\max(R+E-C,0). Each new reservation or ordinary spend is bounded by the same current F. An admitted return can expose \Delta>0 without deleting R. A quantity correction changes attribution support and can expose a_o>s_o while leaving booked cash unchanged. Both transitions retain historical allocation ownership. These two ledgers distinguish allocation of performance from present capacity to spend cash.

In the handle (i,\nu_i,p), p identifies the fixed program. For a handle (i,\nu_i,p), a new request binds x=(i,p,\text{context},\text{service},\text{method},\text{arguments}). The durable command transition proceeds as follows.

Begin one write transaction and read the authenticated current state. Bind the instance to the requested program and context.
If D(i,k) exists, compare the exact request digest. Return its stored outcome on equality, or reject conflicting content. This check precedes the handle-revision check.
For a new command, require the handle revision to equal the current instance revision. Restore its continuation against the current ledger and consume its continuation head.
Apply the selected transition. Retain a successful result or a specified domain, type, or numerical rejection together with its actual completed prefix and counters. An infrastructure exception aborts the transaction.
Store the new continuation, full ledger, lineage heads, outcome, and command binding together. Increment the instance revision and update r by comparison with the revision read in step 1. Commit the transaction before returning the outcome.

The concrete store is SQLite in write-ahead-log mode with synchronous=FULL, a single authenticated state row, and BEGIN IMMEDIATE for writers. A conditional row update supplies the revision comparison. Read-only reconstruction runs inside one read transaction and does not restore or execute the evaluator. SQLite’s durability depends on its documented operating-system, filesystem, and synchronization premises [1, 2].

The local guarantee depends on a current transactional store and on admitted command authority. Atomicity means recovery sees the whole old state or the whole new state. It does not make an external payment provider part of the database transaction. The following assumptions identify exactly where storage, authorization, and external facts enter the proof.

Assumption 6.4 (Durable execution premises).

The database provides atomic transactions and the stated durable-commit behavior on the selected storage system. All writers use the command transition above and share the current store. The store is not replaced by an older valid database image. Such replacement requires a separately maintained monotonic anchor to detect. Program identities and request digests are collision resistant, and authentication keys remain controlled by the store authority. Callers authenticate and authorize commands, evidence, conversion uses, corrections, and physical-occurrence identities before admission. For each resumed command, this authorization covers the fixed program context and every retained authority premise on which the action relies. Accepted local transitions preserve the evaluator and ledger rules, including their retained prefixes on specified rejection. No admitted transition dispatches an external provider operation inside the database transaction.

The theorem combines two invariants. A command can have only one committed application, and each application must preserve the current entitlement and resource records. Its proof orders committed transactions and checks the retry and new-command cases separately.

Theorem 6.5 (Durable retry and conservation).

Under Assumption 6.4, start from a valid state and apply any finite sequence of commands, retries, concurrent requests, and process interruptions. Every recovered committed state satisfies the following properties.

(i): Each key (i,k) identifies at most one committed command transition and its exact stored outcome. An identical retry returns that outcome, including after a lost response.
(ii): A new command requires the current instance revision. It cannot restore an older continuation over a later accepted command or replace intervening shared-ledger work.
(iii): Resolution preserves canonical amount, type, transitive evidence, and immutable entitlement identity. Payment, correction, and return transitions retain outstanding rights and historical allocation ownership under Proposition 3.7. All instances share the ledger’s allocation and available-cash checks.
(iv): Committed resource counters and completed computation are retained together with the ledger and command outcome. A specified rejection retains its accepted prefix. Recovery exposes the entire pre-transaction or post-transaction state, with no partial combination.

Proof. Serialize committed write transactions in their database order. The initial state satisfies the evaluator and ledger invariants. Suppose they hold before the next transaction. An existing command key either returns its stored result without applying a transition or rejects different content. Thus this case preserves the state and cannot duplicate an amount or allocation. For a new key, the revision check selects the current instance continuation. Restoration checks its current lineage head and uses the current complete ledger, so it retains other instances’ intervening work.

Proposition 6.3 preserves every newly calculated amount and binding. The ledger transitions preserve their admitted allocation, discharge, cash, and correction invariants. In particular, a new allocation increases a_o by at most s_o-a_o when that difference is positive. A decrease in s_o retains a_o and its owners, so a repeated report cannot turn lost support into new capacity. A reservation increases R by at most F, and an ordinary spend decreases C by at most F. Their shared transaction order therefore prevents simultaneous requests from consuming the same free cash. Their specified rejected prefixes satisfy the same invariants by assumption. The transaction stores this exact resulting state, its counters, and its outcome under one new command key. Consequently induction extends to the next committed state, including rejected outcomes with useful completed work. The shared revision comparison and serialized writer transaction prevent competing commands from committing against the same obsolete ledger state.

Atomic recovery selects the old state or the complete new state when an interruption overlaps a commit. If it selects the old state, the command has no committed record and may be attempted again against that state. If it selects the new state, the command map returns its stored outcome before checking the stale handle. Thus a lost response cannot cause a second committed application. The same case distinction retains the continuation, ledger, lineage heads, and counters together. Induction over committed transactions proves all four assertions. ◻

The theorem concerns committed local transitions. Arithmetic performed before an uncommitted interruption can run again, so committed counters do not bound total processor work across crashes. Store authentication establishes integrity, while current-store custody supplies freshness against whole-database rollback. Caller authentication supplies authority to act, which knowledge of a continuation or command identifier does not establish. The stored context identifies fixed rules. Migration of a pending instance to changed rules requires a separately authorized transition. An external provider can complete independently of the local database. Its observed occurrence must enter the ledger through its own authenticated identity and allocation rule. Local transaction atomicity therefore preserves records and entitlements without asserting simultaneous external settlement.

6.4 Two complete programs through the same evaluator

The first program tests the distinction between a coupon counter and an unpaid entitlement. The second tests sparse historical selection, a negative payoff, and conversion into a different payment currency. They use ordinary expression graphs, so their behavior depends on the common rules just proved.

For a recurring coupon, instantiate Proposition 5.7 with unit spacing, initial state m_1=0, and a USD 10 coupon. For h\geq2, use the complete expressions \begin{aligned} b_h&=\mathrm{Ind}(\geq,\mathrm{Oracle}(S,0),1),\\ m_h&=\mathrm{IfElse}(b_h,0,1+\mathrm{Ref}(m,1)),\\ y_h&=\mathrm{IfElse}(b_h,10(1+\mathrm{Ref}(m,1)),0). \end{aligned} Addition and multiplication abbreviate their typed constructors. The coefficient in y_h carries USD and the payment context for h. Triggers (0,0,1,1) at heights 2,3,4,5 give coupons (0,0,30,10) and memory states (1,2,0,0). A separate ready claim resolves while a coupon observation is missing. After resumption, allocating one USD 35 occurrence to the two positive entitlements leaves balances 0 and 5. The zero memory state and the unpaid USD 5 coexist through process restart. Neither coupon state transition pays or deletes that balance.

For a signed currency claim, let an EUR observation claim resolve only at heights 1,3,5, with sample values 100,120,80. At height 6, define \begin{aligned} A&=\mathrm{RefReduce}(c,5,\mathrm{Avg})=100,\\ M&=\mathrm{RefReduce}(c,5,\mathrm{Min})=80,\\ z&=\mathrm{IfElse}\!\left(\mathrm{Ind}(\geq,M,70), \mathrm{Cap}(\mathrm{Floor}(-3(A-90),-50),20),0\right). \end{aligned} All numerical bounds carry the required EUR sample type. The sparse average divides by three selected observations, rather than by the window width five. The result is EUR -30. Rescaling gives -3000 EUR cents. A current-use conversion witness binds the exact rate 5/4 USD per EUR, its observation, and the height-6 USD payment context. The converted represented result is -3750 USD cents. A unit signed position therefore creates a canonical USD 37.50 entitlement from holder to issuer. Every source height and the conversion witness remain attached to that resolution. Missing height-3 evidence suspends the consumer while the available historical instances resolve.

Both programs are ordinary expression graphs through the same evaluator and durable command interface. The reference implementation exercises all admitted constructors, four window reductions, exact and interval inputs, and declared or historical conversion rates. Its 23 evaluator tests, 18 durable-integration tests, and two nested-rate tests run in normal and optimized Python modes. The nested-rate cases retain upstream and consumer conversion witnesses through direct evaluation and durable restart. The durable-integration cases include separate process exits before action, after action, after writing, before commit, and after commit. Only the after-commit retry returns an already stored outcome in those observations. Concurrent reservations of 70 and 70 against cash 100 admit one request. A later reservation of 20 leaves free cash 10. These observations exercise shared resources and complete payoff graphs. The general theorem is the induction above, relative to its transition and storage premises. Compiler refinement, distributed scheduling, provider authority, and external completion remain separate relations to establish.

7 Ordering all producers within one event

A fee and its net payment can be calculated in one event. The fee reads the gross amount. The net payment reads both. Neither calculation needs an artificial delay once those dependencies have an order. The relevant restriction is the absence of a dependency cycle, rather than a positive delay on every edge. The historical language above obtains that restriction from height alone. We now give a larger, explicitly certified profile.

The complete graph must include the sources of inputs. An oracle can publish a risk calculation, a clearing price, or a settlement observation. Calling its output external to a payoff evaluator does not remove those producer dependencies. For example, a payoff that reads a price computed from its own clearing result forms a cycle. Its internal payoff graph can nevertheless remain acyclic.

Definition 7.1 (Producer contract and event instance).

A producer has an identifier, a schedule, an output type, and a finite declared read set. Its contract binds its implementation or declared external semantics, authority, and input-selection rule. A read (u,d) by producer v at height h requires u at height h-d, with d\geq0. The instance must belong to the source schedule. The producer set includes claim resolutions, oracle publications, clearing calculations, risk calculations, and settlement-derived observations. Immutable programme declarations are precommitted inputs. A primitive external producer instead names its exogeneity or prior-commitment contract. An uninspected producer retains an explicit assumption that its contract contains every relevant read.

An event binds its programme, producer contracts, applicable rules, and admitted primitive-input commitments. Derived outputs retain those bindings and the exact predecessor records they use. A changed input creates a distinct evidence record under the existing refinement or correction rule. It cannot rewrite an earlier exact resolution. Dependency completeness concerns data and control reads, including conversion-rate inputs and every admitted conditional branch. It is established by inspecting an internal producer’s code or by its named external contract. A digest identifies that contract. It proves no omitted physical fact.

Definition 7.2 (Causal event certificate).

Let N bound the number of active producer instances at one height. For each height h, a certificate supplies a rank r_h(v)\in\{0,\ldots,N-1\} for every active producer v. Every zero-delay read v\to u satisfies r_h(u)<r_h(v). Positive-delay reads name scheduled instances at positive earlier heights. The certificate binds the exact programme, selected cases, producer manifest, and all rank profiles. Within each payoff instance, its original finite instruction order remains in force.

Theorem 7.3 (Resolution under complete producer dependencies).

Assume the producer contracts contain every actual dependency and satisfy Definition 7.2. Then the complete instance graph is well founded, with rank R(v,h)=Nh+r_h(v). Every requested instance has a finite ancestor closure. Evaluation in increasing (h,r_h) order respects each producer dependency. If every required producer eventually returns admissible evidence, and every local computation succeeds within its envelope, fair scheduling completes that closure. Numerical ambiguity, an unresolved conversion witness, or a pending external outcome retains its stated continuation.

Proof. A zero-delay prerequisite has the same height and smaller local rank, so it has smaller R. For a read with delay d\geq1, R(u,h-d)\leq N(h-1)+N-1<Nh\leq R(v,h). Every dependency therefore decreases a natural number. Each node has finitely many prerequisites, so induction on R gives a finite ancestor closure. The local payoff DAG also has a finite prerequisite order. Replacing each claim node by that DAG preserves the order of external inputs and internal operands. Induct on R after the required evidence becomes available. Fair execution completes each ready finite computation under the stated envelope and numerical conditions. The original typed transitions then commit its exact resolution and retained entitlement. No part of this argument converts producer availability into authority, payment, or finality. ◻

The rank can change with the event’s programme case. For example, claim A can supply claim B at odd heights, while B supplies A at even heights. Each event has a first calculation even though the union of the two unlabelled graphs contains a cycle. One fixed ordering of producer names would reject this useful case unnecessarily.

Proposition 7.4 (Finite certification of periodic producer profiles).

Suppose all producer and case schedules have the finite-prefix, periodic-tail form of Definition 2.17. Let a be their largest cutoff, D their largest declared read delay, and L the least common multiple of their periods. Set T=a+D. It suffices to check producer availability and zero-delay acyclicity at 1\leq h<T+L. A successful check gives an event-dependent certificate for every height. A failed acyclicity check returns a closed dependency path at its witness height.

Proof. For h\geq T, every source height h-d is at least a. Thus both ends of every read, and every case-selection predicate, lie in their periodic tails. The complete selected graph repeats with period L. The checked prefix and one complete period cover every graph profile. Topologically order each acyclic profile from prerequisites to consumers. Its position indices supply r_h. If ordering stops, each remaining node has a remaining prerequisite. Following those prerequisites in the finite remainder repeats a node and exhibits a cycle. ◻

The reference checker bounds the least common multiple, scan horizon, graph size, and producer-frontier traversal. An exhausted envelope returns BudgetExceeded, which supplies no validity decision. A larger admitted envelope can complete the same mathematical check. Historical windows still select their scheduled past members before evaluation. Resolved conversion-rate references retain their separately stated historical-use contract. Exact declared rates are precommitted programme inputs. Their stored values do not certify their external provenance.

Proposition 7.5 (Conservative extension of the payoff evaluator).

Add \mathrm{Ref}(c,0) only when the complete programme has a causal event certificate. Read the committed source resolution with the original sample-or-amount rule and its retained evidence. Use certified event order for claim evaluation. For the historical sublanguage, these rules preserve every original payoff, type, conversion witness, and entitlement transition. For an admitted same-event programme, each reference reads an earlier completed source in that event. The exact-output and resource-conservation conclusions of Proposition 6.3 and Theorem 6.5 retain their original premises.

Proof. For a historical reference, the source height is unchanged and remains smaller than the consumer height. Changing the order among independent same-height instances changes no operand or ledger identity. For a zero-delay reference, the certificate puts its source first. The evaluator reads that source’s exact resolution and joins its evidence, conversion witnesses, and resolution identity as before. The remaining instruction transitions are unchanged. Induction over the certified instance order and the internal instruction order therefore gives the same local preservation statements. Resolution still creates each immutable entitlement under its original origin and binding. The transaction wrapper still commits the continuation, shared ledger, and command outcome together. Its source-bound identity now also includes the causal certificate. Each execution retains its exact programme identity. Moving saved state between different programmes requires its own admitted migration. No new transition dispatches an external action or allocates a physical receipt. ◻

A fee and a net entitlement.

At one height, an admitted account observation supplies a gross amount of USD 100. A fee claim reads that amount and applies a contractual coefficient 1/10. A net claim reads the gross amount and the fee, giving USD 90. The fee and net claims create distinct entitlements of USD 10 and USD 90. The certificate orders observation, gross calculation, fee, and net calculation. All calculations occur at the same height. The numerical identity 10+90=100 supplies no discharge. Subsequent payments use the shared allocation journal. The executable example deliberately names the net claim before its source in lexical order. Only dependency order supplies the correct first execution.

Settlement as an input to later computation.

An amount can be calculated before its provider reports partial performance. A settlement producer names that amount as a dependency. Its later observation binds the actual source resolution and can report, for example, receipt of 7 against a calculated amount of 10. The dependent calculation remains pending until the admissible observation arrives. The three-unit shortfall remains an obligation under its governing rule. Provider authentication, recipient credit, and finality are separate conditions supplied by the execution contract.

The reference implementation extracts claim, window, oracle, and conversion-rate reads from the complete compiled programme. It checks finite graph profiles and evaluates same-height claims in certified order. Observation admission binds the certificate, producer, height, exact declaration, mapped predecessor observations, and resolved claim frontier. Missing mapped predecessors block admission. Opaque producer stages retain their explicit computation and dependency-completeness contracts. The binding helper creates no signature or provider evidence. The implementation preserves all nine operators, historical reductions, rescaling, conversion, exact arithmetic, and the durable transaction wrapper. Its correspondence tests exercise the historical programmes as well as same-event, periodic-order, late-observation, cycle, and interruption cases. The mathematical proofs concern the stated transition rules. A mechanized compiler and external-producer refinement remain separate proof obligations.

7.1 Executable producers

A calculated input can be defined by the same language as its consumer. For example, a cross-currency rate can be computed by a witnessed conversion, then used by a payoff. The intermediate calculation has a value and evidence. Its calculation alone creates no payment obligation. This distinction lets one evaluator execute the complete internal dependency graph.

Definition 7.6 (Executable producer).

An executable producer owns one named input source and supplies a scheduled, typed payoff body without position lots. Its output type equals the source’s declared type. The programme assigns the body a reserved auxiliary claim name. That name binds the complete compiled programme, input contracts, external producer contracts, and execution semantics. Ordinary declarations and historical-rate aliases cannot shadow an owned source. A consumer reaches the body through the source’s oracle or conversion-rate interface. The producer’s read set is extracted from its compiled instructions, including both conditional branches. Its exact resolution supplies the source publication. External observations cannot replace that publication.

An auxiliary resolution retains the evaluator’s complete value V=(x,\theta,E,H,W) from Proposition 6.3. Here x is the exact scalar, \theta its type, and E,H,W its input, historical, and conversion evidence. Boolean roots use the existing numerical interpretation in \{0,1\}. Reading the publication retains this value and adds its exact auxiliary resolution identity. A conversion consumer also requires its own current-use witness for the computed rate. The upstream conversion witnesses remain present.

Proposition 7.7 (Execution through auxiliary resolutions).

Replace each executable producer by the auxiliary claim of Definition 7.6. Admit the resulting complete graph under Definition 7.2. Assume its external inputs, conversion witnesses, arithmetic, and storage satisfy their original contracts. Then every published internal scalar is the exact result of its declared body. Every executed claim or input-source dependency belongs to the extracted graph. Consumers retain the body’s input evidence, historical records, and conversion witnesses. Each producer resolution adds an auxiliary record and creates no entitlement or physical allocation. The transaction wrapper commits that record with the corresponding continuation and command outcome. For admitted programmes, useful same-event computation and initialized historical recurrence retain their existing evaluation rules.

Proof. Induct first over the producer body’s finite instruction graph. A literal reads its fixed declaration. An oracle instruction names its source and delay. A claim reference names one resolution, while a historical reduction names its scheduled window members. A conversion names its historical rate, fixed rate declaration, or input source, together with its required use witness. Each remaining constructor reads its argument instructions. The compiler retains every branch and extracts every such source dependency. Thus the certified graph contains each claim and input-source dependency of the body. Governing conversion witnesses remain separately admitted conditions.

Now induct over the instance rank of Theorem 7.3. The producer’s predecessors supply the same typed operands as ordinary claim evaluation. The unchanged instruction rules therefore produce the same complete value V. An inexact scalar retains its continuation until the exact-output condition holds. Once it holds, the ordinary resolution transition commits V under the auxiliary identity. The body has no positions, so that transition creates only its auxiliary record. Publication is a deterministic projection of this committed resolution, rather than an independent mutable observation. Its consumer receives V with the publication and resolution evidence added. Conversion joins the consumer’s witness with the witnesses already in V. The durable transaction theorem applies to the same continuation, ledger, and command outcome. ◻

For example, let a declared GBP-per-EUR quantity equal 2 and a witnessed USD-per-GBP rate equal 5/8. Their typed product supplies a USD-per-EUR rate of 5/4. A consumer can then convert EUR 8 into USD 10 with its own conversion witness. Its evidence retains both uses and the original input, while only the consumer’s position creates the USD 10 entitlement.

The reference implementation lowers these bodies through the existing payoff compiler and commits them through the shared entitlement ledger. Reserved names include external producer contracts because two otherwise equal programmes can rely on different authorities. Digest-based names retain the usual collision-resistance premise. Tests execute a signed historical-window body, nested witnessed conversions, initialized recurrence, interval refinement, and interruption at each local transaction boundary. Opaque external computations still require their declared dependency and authority contracts. The executable profile transfers their inspection obligation only when their actual computation has been expressed in the admitted language.

The hidden feedback example has no certificate: payoff reads oracle, oracle reads clearing, and clearing reads payoff at the same height. Its rejection includes that closed path. A positive lag can remove the cycle when the corresponding earlier source is scheduled and admitted. A genuinely simultaneous market model instead requires an existence theorem, a solution-selection rule, and certified numerical execution for that fixed point. Neither an oracle label nor a larger computation budget supplies those results.

8 Markets over claims: curvature and covariance

The claim model now fixes what is calculated, when its inputs permit resolution, and how the resulting obligation remains recorded. A market adds the price paid to acquire or transfer that claim. The payment formula can stay fixed when the pricing mechanism changes.

Two forms describe markets that post prices continuously. A cost-function market charges the change in a specified function of outstanding quantities. A constant-function market permits exchanges that preserve a reserve constraint. The Peters-So-Ye auction instead chooses orders through one convex optimization problem per batch [45]. The local curvature theorem concerns the first form. A reserve market first requires an account of which instruments its reserve quantities represent.

8.1 Reserve instruments and signed positions

The numeraire is the unit in which the market states trade prices and charges. A reserve quantity counts transferable units of a specified instrument. A payoff number becomes such an instrument through its ownership, funding, and redemption rules. Those rules distinguish a funded note from an unfunded obligation with the same numerical payoff.

Definition 8.1 (Funded reserve instruments).

An instrument specifies its asset unit, issuer, custody, title rule, transfer rule, and redemption rule. Its custody record identifies resources assigned to issued units after senior restrictions and prior pledges. Each unit has one current owner, and reserved redemption units remain assigned to that request. The pool’s available reserve quantity excludes those reserved units.

A unit-delivery instrument u_X gives its holder the specified right to one asset unit X. A redemption request locks existing units and creates a deduplicated one-shot claim with program \mathrm{Const}(1). The position quantity fixes the requested asset amount. Its context binds the provider, beneficiary, asset, title rule, discharge route, and evidence requirements. Partial performance consumes only the corresponding quantity and preserves the remaining entitlement. An identical request retains its original entitlement and reservations.

A completed reserve trade requires authenticated instrument-title transfers and the reserve constraint. Partial external execution retains the actual occurrences, unpaid amounts, and outstanding command capacity. If custody or redemption ceases to satisfy the representation contract, the instrument enters its impaired state. Its residual rights and recovery route remain explicit, while reserve accounting uses its actual current eligibility.

A signed payoff can require payment in either direction. A reserve instrument instead represents a transferable funded right held in nonnegative units. For a payoff with known lower and upper bounds, the construction below adds a fixed principal to make each complementary note positive. Keeping the financing leg records the original signed economic gain.

Proposition 8.2 (Funded representation of a signed payoff).

Fix one resolution instance of a \Sigma payoff program f. Its complementary notes have that instance’s one-shot schedule. Suppose f satisfies -L\leq f\leq U throughout a declared funding domain, with L,U\geq0. For \epsilon>0, set a=L+\epsilon,\quad b=U+\epsilon, \qquad W^+=a+f,\quad W^-=b-f. Both notes are \Sigma programs and satisfy W^+\geq\epsilon,\quad W^-\geq\epsilon, \quad W^++W^-=a+b. A complementary pair funded by a+b dedicated cash units covers both note payouts under the stated funding domain. With one contributed cash unit worth one settlement unit, their net gains are W^+-a=f and W^--b=-f. Thus qf=\begin{cases}qW^+-qa,&q\geq0,\\|q|W^--|q|b,&q<0.\end{cases} A reserve market trades the funded note, while the economic position retains its separate principal or financing-debt leg.

Proof. The payoff bounds give both positivity inequalities. Adding the notes cancels f and yields their fixed backing amount. The shared allocation ledger distributes that one dedicated pot and consumes each allocation once. Constants and linear combinations construct both notes. Subtracting each stated principal proves the net-gain identities and the two cases for q. ◻

Recurring families use separately funded pairs or explicitly reserved aggregate backing for their admitted payout schedule. The backing pot and the pool’s numeraire reserves are separate resource domains. A financing agreement records its payer, recipient, amount, and discharge route separately. The valuation identity therefore preserves the whole signed position, including its capital cost. For example, f\in[-2,3] and \epsilon=1 give notes 3+f and 4-f, funded by seven cash units. At f=-2, their payouts are 1 and 6, with net gains -2 and 2. Ten pairs require a separate backing pot of 70. A pool holding ten long notes and 30 numeraire can sell one note for 10/3 numeraire under constant product. The trade changes note ownership while the backing remains assigned to the notes.

Remark 8.3 (Signed margin and recurring exposure).

An unbounded two-sided payoff has no complementary representation with a single finite fixed backing pot. For every proposed shift a, some state with f<-a makes a+f negative. A signed cash-settled margin venue preserves the original payoff and quotes outstanding exposure z, for example through \varphi_t(z)=m_tz+\tfrac12\lambda z^2,\qquad\lambda>0. This is a strictly convex cost-function market with Hessian \lambda. Its cash accounts provide margin and settlement funding under an explicit risk and default policy. Each resolution creates its directed entitlement. New commands reserve available funds, and any later funding deficit retains the unpaid entitlement and recovery continuation. The payoff and its negative outcomes remain unchanged. Successive funded intervals provide another perpetual implementation. Each interval admits its own backing, while existing entitlements survive a failure to fund the next interval.

8.2 Two venue forms

In the first form, the market records outstanding claim quantities and charges the numeraire. A potential is the function whose change gives the exact trade charge. Its gradient gives the price of an infinitesimal additional quantity. The second form holds reserve instruments and constrains the quantities left after a trade.

Definition 8.4 (Cost-function market).

A cost-function market on n claims c_1, \dots, c_n is a pair (\varphi, x) where \varphi : \mathcal{D}\to \mathbb{R} is a C^2 convex function on an open convex set \mathcal{D}\subseteq \mathbb{R}^n (the potential, or cost function) and x \in \mathcal{D} is the vector of outstanding quantities. A buyer of the bundle \Delta x (with x + \Delta x \in \mathcal{D}) pays \varphi(x + \Delta x) - \varphi(x) in numeraire; the marginal price vector is p := \nabla \varphi(x). This is the market-maker form of Chen-Pennock [20]; the admissible potentials are characterised in [3] as convex conjugates of regularisers on the price simplex.

Remark 8.5 (Quantities are claim positions).

The quantities x_i in Definition 8.4 are signed positions in claim c_i (Definition 2.12). Funded reserve instruments have their additional representation relation in Definition 8.1 and Proposition 8.2.

Example 8.6 (LMSR).

For n outcomes, the logarithmic market scoring rule is the cost-function market with \varphi_b(q) = b \log \textstyle\sum_{i} \exp(q_i/b), \qquad b > 0, on \mathcal{D}= \mathbb{R}^n [28]. Prices are the implied probabilities p_i(q) = \exp(q_i/b)/\sum_j \exp(q_j/b). Since \varphi_b(q + c\mathbf{1}) = \varphi_b(q) + c, prices are invariant under q \mapsto q + c\mathbf{1} and the complete bundle — one unit of every outcome — always costs exactly its riskless payout; the economically distinct states form the quotient \mathbb{R}^n / \operatorname{span}(\mathbf{1}). Proposition 8.20 computes the Hessian and shows it is positive definite exactly on this quotient.

Strict quasiconcavity means a nontrivial mixture of distinct reserve vectors has trading-function value strictly above the smaller endpoint value. Consequently, each superlevel set of permitted reserves is convex. The increasing-coordinate condition means that adding any reserve instrument increases the trading function. These are the two geometric conditions imposed below.

Definition 8.7 (Constant-function market).

A constant-function market on eligible transferable reserve instruments (Definition 8.1) with reserve quantities R \in \mathbb{R}_{>0}^n is specified by a level set \psi(R)=k. We impose two conditions on the trading function:

(C1): \psi is strictly quasiconcave;
(C2): \psi is strictly increasing in every reserve coordinate.

A trade \Delta R is admissible if \psi(R+\Delta R)\geq k, and the transfer occurs in the reserve assets [6].

Remark 8.8 (The invariant is not a cost function).

The two forms are not interchangeable. A cost-function market charges \varphi(x + \Delta) - \varphi(x) in an external numeraire; a constant-function market holds \psi constant along trades, so \psi prices nothing by differences, and reading a level-set defining function as a potential produces nonsense: \nabla(-\log R_1 - \log R_2) = (-1/R_1, -1/R_2) is not a price vector. The convex object a constant-function market does carry is its reserve set K := \{R : \psi(R) \geq k\} with the portfolio value function V(p) \;:=\; \inf_{R \in K} \, p^\top R, the lower support function of K, which is concave in the external price vector. Fix p and assume the infimum is attained at R^\star(p)\in K. Then V(p')\leq p'^\top R^\star(p) =V(p)+R^\star(p)^\top(p'-p), so every attained minimiser is a supergradient of V at p. If V is differentiable at p, the supergradient is unique and R^\star(p)=\nabla V(p) [8]. Without attainment, there is no reserve vector to recover; without differentiability, the attained minimisers need not define one gradient. The full correspondence between the two venue forms is a convex duality: constant-function markets and cost-function prediction markets are equivalent up to conjugacy [24]. We use only the portfolio-value form.

Example 8.9 (Constant product through the duality).

Take the constant-product invariant R_M R_B = k — a risky asset M pooled against a numeraire B [4] — at positive external price p>0 of M. Minimising p R_M + R_B subject to R_M R_B = k gives R_M^\star = \sqrt{k/p}, \qquad R_B^\star = \sqrt{kp}, \qquad V(p) = 2\sqrt{kp}, \qquad V'(p) = \sqrt{k/p} = R_M^\star. V is concave, and the marginal pool price at equilibrium is R_B^\star / R_M^\star = p: the arbitrage-equilibrium statement of [6]. The constant-product market enters the catalogue of Section 9 in this form, not as a cost function on reserves.

Two pools can retain separate reserve constraints. Combining them by multiplying their defining functions would need to preserve the required reserve geometry. The next counterexample shows why that shortcut fails, even when both original pools satisfy the stated conditions.

Lemma 8.10 (Products do not preserve the market conditions).

Let two constant-function markets satisfy (C1)–(C2) on disjoint reserve coordinates. Their trading functions cannot in general be replaced by their product while preserving (C1).

Proof. For i\in\{1,2\}, define \psi_i(x_i,y_i)=\exp\!\bigl((x_iy_i)^2\bigr), \qquad (x_i,y_i)\in\mathbb{R}_{>0}^2. Each \psi_i is strictly increasing in both coordinates. It is strictly quasiconcave because it is a strictly increasing transform of x_iy_i, whose logarithm is strictly concave. Now set \Psi=\psi_1\psi_2, let a=4^{1/4} and \varepsilon=0.05, and consider A=(a,a,\varepsilon,\varepsilon), \qquad B=(\varepsilon,\varepsilon,a,a). Both endpoints satisfy \log\Psi=4+\varepsilon^4>4. At their midpoint, \log\Psi\!\left(\frac{A+B}{2}\right) =2\left(\frac{a+\varepsilon}{2}\right)^4<0.58<4. The superlevel set \{R:\Psi(R)\geq e^4\} contains A and B but not their midpoint. Hence \Psi is not quasiconcave. ◻

Remark 8.11 (Disjoint reserve surfaces).

When two pools use disjoint reserves, the combined state retains the pair of constraints \psi_1(R_1)\geq k_1 and \psi_2(R_2)\geq k_2. Multiplying the functions can destroy the convex reserve geometry even when each market satisfies (C1)–(C2). Independence therefore means separate surfaces, not one product surface.

8.3 Equilibrium and local curvature

A finite order generally changes the marginal price as it executes. Multiplying its size by the initial quote therefore need not give its total cost. The Hessian, the matrix of second derivatives of the cost function, measures the first change in that quote. We expand the exact trade charge around an equilibrium, where the marginal price agrees with an external observed price.

Definition 8.12 (Equilibrium).

Let (\varphi, x^\star) be a cost-function market. The point x^\star \in \mathcal{D} is an equilibrium if \nabla \varphi(x^\star) =: p^\star equals the externally observed price vector for the n claims, so that no profitable arbitrage against outside venues remains at x^\star.

Remark 8.13 (Existence and uniqueness).

When \nabla \varphi is injective on \mathcal{D} — in particular when \varphi is strictly convex — and p^\star \in \nabla\varphi(\mathcal{D}), the equilibrium exists and is unique; this is the standard arbitrage argument [6, 7]. For potentials with a price invariance, uniqueness holds on the quotient by the invariance directions (Example 8.6, Remark 8.19).

Proposition 8.14 (Local expansion of total trade cost).

Let (\varphi, x^\star) be a cost-function market at equilibrium with \varphi \in C^2 on \mathcal{D} and C := \nabla^2 \varphi(x^\star) \succ 0. Then:

(i): Total cost and its quadratic correction. For \delta with x^\star + \delta \in \mathcal{D}, the total amount charged is T(\delta):=\varphi(x^\star+\delta)-\varphi(x^\star) =p^{\star\top}\delta+\tfrac12\delta^\top C\delta+o(\|\delta\|^2) \qquad(\|\delta\|\to0). Thus the excess above the current marginal-price mark, Q(\delta):=T(\delta)-p^{\star\top}\delta, has the positive-definite quadratic correction \tfrac12\delta^\top C\delta+o(\|\delta\|^2). If \varphi \in C^3 near x^\star, the remainder is O(\|\delta\|^3).
(ii): Bilinear aggregation of the correction. For an aggregate trade \delta = \sum_k w_k \delta_k, \delta^\top C \delta \;=\; \sum_{k,k'} w_k w_{k'}\, \delta_k^\top C\, \delta_{k'} : the Hessian form expands bilinearly in the component trades. The leading correction is one half of the displayed sum, and \delta_k^\top C \delta_{k'} measures the interaction of trades k and k' through the venue’s curvature.
(iii): Cross price impact. C_{ij} = \partial p_i/\partial x_j\big|_{x^\star}: entry (i,j) is the marginal response of claim i’s price to claim j’s quantity, and the matrix is symmetric, C_{ij} = C_{ji}.

Proof. (i) Taylor’s theorem with Peano remainder for a C^2 function at x^\star gives T(\delta)=\nabla\varphi(x^\star)^\top \delta + \tfrac12 \delta^\top C \delta + o(\|\delta\|^2). The equilibrium condition identifies the linear term as p^{\star\top}\delta. Subtracting it gives Q(\delta). Positive-definiteness of the quadratic correction is the hypothesis. Under \varphi \in C^3, the integral form of the remainder on a compact neighbourhood of x^\star gives the O(\|\delta\|^3) bound. (ii) is bilinearity of the quadratic form. (iii) Differentiating p = \nabla \varphi once more gives \partial p_i/\partial x_j = \partial^2 \varphi / \partial x_i \partial x_j = C_{ij}; symmetry of second partials for C^2 functions is Schwarz’s theorem. ◻

A local expansion alone does not certify the error for a chosen finite trade. The next bound controls how much the Hessian varies along the trade segment. It also admits errors in the supplied price and curvature estimates, so the certificate states a numerical allowance for the resulting quote.

Proposition 8.15 (Certified remainder for a finite trade).

Let the segment x+t d, 0\leq t\leq1, lie in the domain of a C^2 potential \varphi. Put H=\nabla^2\varphi, \rho=\|d\|, and suppose \|H(x+t d)-H(x)\|_{\mathrm{op}}\leq\omega(t\rho). The remainder after the linear and quadratic terms satisfies |R_2(d)|\leq\rho^2\int_0^1(1-t)\omega(t\rho)\,dt. In particular, an L-Lipschitz Hessian gives |R_2(d)|\leq L\rho^3/6. If \|\nabla\varphi(x)-\widehat p\|\leq\alpha and \|H(x)-\widehat C\|_{\mathrm{op}}\leq\beta, then \left|\varphi(x+d)-\varphi(x) -\widehat p^\top d-\tfrac12 d^\top\widehat C d\right| \leq\alpha\rho+\tfrac12\beta\rho^2+\tfrac16L\rho^3.

Proof. Apply the fundamental theorem of calculus twice to g(t)=\varphi(x+t d). It gives R_2(d)=\int_0^1(1-t)d^\top[H(x+t d)-H(x)]d\,dt. The operator-norm bound proves the first inequality. For a Lipschitz Hessian, substitute \omega(s)=Ls and use \int_0^1t(1-t)\,dt=1/6. The price-vector and Hessian approximation errors contribute at most \alpha\rho and \beta\rho^2/2 by their norm bounds. ◻

Example 8.16 (Sharp constant and a useful trade radius).

For a,L>0, take \varphi(z)=p_0z+az^2/2+Lz^3/6 on (-a/(2L),a/(2L)). Its Hessian is a+Lz>a/2, so it defines a strictly convex local cost function. At x=0, its remainder equals Ld^3/6. The constant 1/6 is therefore attained under the stated market hypotheses.

If H(x)\succeq mI with m>0, the relative error in the quadratic correction is at most L\rho/(3m). A trade radius \rho\leq3\epsilon m/L therefore certifies relative error at most \epsilon, within the admitted domain. An absolute error allowance \eta permits \rho\leq(6\eta/L)^{1/3}. The case L=0 gives an exact quadratic expression throughout the certified region. A third-derivative norm bound supplies L by integration along each segment. Certified interval bounds on the third partial derivatives supply a conservative tensor-norm bound. Digital payoffs require their separate comparison certificates, because their switching sets do not satisfy this smoothness hypothesis.

Remark 8.17 (The Hessian hypothesis).

Strict convexity does not imply \nabla^2\varphi(x^\star) \succ 0. The potential \varphi(x)=x^4 is strictly convex, but \varphi''(0)=0. At the equilibrium x^\star=0, the total cost and its excess above the zero marginal-price mark are quartic, with no quadratic correction (Example 10.1). The theorem therefore assumes a positive-definite Hessian at the equilibrium.

Remark 8.18 (Represented curvature certificates).

For a rational symmetric matrix, exact leading principal determinants decide positive definiteness by Sylvester’s criterion [30, Theorem 7.2.5]. For a certified approximation \widehat C with operator error at most \beta, an exact check \widehat C-\mu I\succ0 with \mu>\beta gives C\succeq(\mu-\beta)I. Validated derivative bounds then supply the quote certificate in Proposition 8.15. An interval determinant containing zero is unresolved and certifies neither positivity nor a null direction. An exact zero determinant for a known positive semidefinite matrix permits a kernel solve under the stated representation.

Remark 8.19 (Degenerate directions and quotients).

Suppose instead C \succeq 0 with kernel \mathcal{K}\neq \{0\}. The expansion of (i) still holds, with a positive semi-definite quadratic correction vanishing on \mathcal{K}. Two structurally different cases arise. If \varphi is affine along \mathcal{K} — \varphi(x + v) = \varphi(x) + \ell(v) for all x \in \mathcal{D}, v \in \mathcal{K} with x + v \in \mathcal{D}, and a fixed linear functional \ell — then prices are invariant along \mathcal{K}, states differing by \mathcal{K} are economically identical, and the market descends to the quotient \mathbb{R}^n/\mathcal{K}; when the kernel of C is exactly \mathcal{K}, the induced Hessian on the quotient is positive definite and Proposition 8.14 applies there. The LMSR is this case with \mathcal{K}= \operatorname{span}(\mathbf 1) (Proposition 8.20), as is the linear-fibre potential of Example 10.2. Without such an invariance the degeneracy is genuine — the quartic potential of Example 10.1 — and second-order analysis at x^\star says nothing; the venue needs a strictly curved potential or an external risk model. In the extreme C = \mathbf 0 of a linear potential (a constant-sum venue), total trade cost is exactly linear and carries no curvature information.

8.4 When curvature also gives implied covariance

Price impact measures the market’s response to an order. Covariance measures how claim payoffs vary together under a specified probability law. The two coincide up to scale for the log-partition potential below. Its implied probabilities supply the law, and its riskless complete bundle explains the direction in which curvature vanishes.

Proposition 8.20 (Covariance in the log-partition class).

Let \varphi_b(q)=b\log\sum_{i=1}^n\exp(q_i/b), \qquad b>0. Let p=p(q) be the implied probability vector. Let e\in\{0,1\}^n be the outcome-indicator vector, where e_i=1 exactly on outcome i and \mathbb{P}(\text{outcome }i)=p_i. Then \nabla^2 \varphi_b(q) \;=\; \tfrac{1}{b}\bigl(\mathop{\mathrm{diag}}(p) - p\, p^\top\bigr) \;=\; \tfrac{1}{b}\, \mathop{\mathrm{Cov}}_p(e). For q \in \mathbb{R}^n the matrix is positive semi-definite with kernel exactly \operatorname{span}(\mathbf 1), and it is positive definite on the quotient \mathbb{R}^n/\operatorname{span}(\mathbf 1) — equivalently on \{v : \sum_i v_i = 0\} — where Proposition 8.14 applies. More generally, if \varphi(q) = b\,A(q/b) for the log-partition function A of an exponential family with sufficient statistic T, then \nabla^2 \varphi(q) = \tfrac{1}{b} \mathop{\mathrm{Cov}}_{q/b}(T) [15].

Proof. Differentiating, \partial \varphi_b/\partial q_i = p_i and \partial p_i/\partial q_j = \tfrac{1}{b}(\delta_{ij} p_i - p_i p_j), which assembles to \tfrac1b(\mathop{\mathrm{diag}}(p) - pp^\top). Its (i,j) entry is \tfrac1b(\mathbb{E}[e_i e_j] - \mathbb{E}[e_i]\,\mathbb{E}[e_j]), since \mathbb{E}[e_i e_j] = \delta_{ij} p_i and \mathbb{E}[e_i] = p_i; this is \tfrac1b \mathop{\mathrm{Cov}}_p(e). For any v \in \mathbb{R}^n, v^\top \bigl(\mathop{\mathrm{diag}}(p) - pp^\top\bigr) v \;=\; \sum_i p_i v_i^2 - \Bigl(\sum_i p_i v_i\Bigr)^{\!2} \;=\; \mathop{\mathrm{Var}}_p(v_\omega) \;\geq\; 0, with equality iff v is constant across the outcomes in the support of p; since every p_i > 0 for q \in \mathbb{R}^n, equality holds iff v \in \operatorname{span}(\mathbf 1). The general statement is the exponential-family identity \nabla^2 A = \mathop{\mathrm{Cov}}(T) [15], applied at \theta = q/b with the chain rule. ◻

Corollary 8.21 (One matrix in the log-partition class).

For a venue with a log-partition potential, the matrix of Proposition 8.14 — the quadratic correction to total cost and the cross price impact — equals 1/b times the covariance of the outcome payoffs under the venue’s implied probabilities. The trading function therefore encodes these implied second moments.

Remark 8.22 (Scope of the covariance reading).

The identification in Corollary 8.21 is a property of the log-partition class, not of convex venues in general. Curvature determines price impact. Covariance belongs to the joint law of resolutions. The constant-product market makes the distinction concrete: its dual description (Example 8.9) contains no information about statistical dependence between the pooled assets. For every other venue class, a portfolio risk model must obtain covariance from a resolution model, empirical attestations, or another stated source.

Two companion results supply event-probability inputs without changing this boundary. One-way coupling gives a mechanism by which a prediction-market signal changes an automated-market-maker reference price [35]. Parlay identification recovers pairwise dependence from single-event and parlay probabilities under an Ising model [36]. These are inputs to claim pricing. Curvature of an arbitrary venue does not infer them.

Admissible Obligation Transitions describes the claim lifecycle that consumes each external effect once and replays every accepted trace [37]. Event-Collect BFT defines the event-atomic ledger transition that produces a resolution input [38]. Recourse treats contested resolution and records a correction as a follow-on claim instead of rewriting a resolved instance [39].

9 A reduction catalogue: eight standard market types

An automated market maker (AMM) determines admissible trades or quotes from its stated mathematical rule. The convex parimutuel call auction mechanism is abbreviated CPCAM. The catalogue now keeps two choices visible for each example: its payoff calculation and its pricing mechanism. The proposed decompositions also need the schedules, financial declarations, and instrument contracts already defined. In particular, a constant unit payoff supplies a redemption amount only after custody and title rules establish the corresponding instrument.

Proposition 9.1 (Reduction catalogue).

Each of the following market types (a) decomposes into payoff-program schemas in \Sigma under Definition 2.11 and Definition 2.4, and (b) admits a price-formation mechanism that is a cost-function market (Definition 8.4), a constant-function market (Definition 8.7), or a convex clearing program. A schema becomes an admissible claim through checked scalar types, a schedule, an entitlement context, and the venue’s resource contract. Reserve-pool implementations additionally provide funded transferable instruments. Signed obligations can use the margin construction:

(M1): Constant-product AMM (Uniswap-v2 family [4, 6]).
(M2): Bonding curve with shifted-power pricing [10].
(M3): Logarithmic market scoring rule (LMSR) [28, 29].
(M4): Peters-So-Ye convex parimutuel call auction [45, 33, 34].
(M5): Binary prediction contract.
(M6): Linear perpetual contract.
(M7): Fixed-coupon bond.
(M8): Linear-payoff option (call, put, collar).

Proof. We give the eight decompositions, one paragraph each.

(M1) Constant-product AMM.

The reserve assets are transferable unit-delivery instruments from Definition 8.1. A redemption request locks existing units and creates a one-shot \mathrm{Const}(1) claim, with its position quantity fixing the asset amount. The pool maintains R_1R_2=k on available reserve units. At a positive relative price p, Example 8.9 gives R_1^\star=\sqrt{k/p}, R_2^\star=\sqrt{kp}, and V(p)=2\sqrt{kp}. The custody and title records supply the instruments, while the invariant supplies their exchange geometry.

(M2) Bonding curve.

One claim has resolved value one unit of the curve-issued token, with discharge specified as in (M1). Price formation uses the cost-function market \varphi(s) = \int_0^s P(u)\,du, \qquad P(u) = P_0 \bigl((u + S_{\mathrm{init}})/S_0\bigr)^{\gamma}, \qquad P_0, S_0, S_{\mathrm{init}} > 0, so buying ds at supply s costs P(s)\,ds and the pay-the-difference form is exact [10]. Since \varphi''(s) \;=\; P'(s) \;=\; \frac{\gamma P_0}{S_0}\,\bigl((s + S_{\mathrm{init}})/S_0\bigr)^{\gamma - 1} \;>\; 0 \quad \text{for every } \gamma > 0 \text{ and } s \geq 0, the potential has positive (scalar) Hessian everywhere and Proposition 8.14 applies at any equilibrium. At \gamma = 0 the price is constant, \varphi is linear, and the curvature degenerates (Remark 8.19). Sigmoid curves require the analytic extension in Open problem 1.

(M3) Logarithmic market scoring rule.

n outcomes; n claims c_i, each paying 1 on outcome i and 0 otherwise. Payoff program for c_i, with \omega the outcome index attested at the resolution height: \mathrm{Ind}\bigl(=, \mathrm{Oracle}(\omega, 0), \mathrm{Const}(i)\bigr). Price formation: the cost-function market \varphi_b(q) = b \log \sum_i \exp(q_i/b) (Example 8.6), with prices the implied probabilities. By Proposition 8.20, \nabla^2 \varphi_b = \tfrac1b(\mathop{\mathrm{diag}}(p) - pp^\top) with kernel \operatorname{span}(\mathbf 1): positive definite on the quotient by the riskless bundle direction, where Proposition 8.14 and Corollary 8.21 apply.

(M4) Peters-So-Ye call auction.

Let i=1,\ldots,S index states and j=1,\ldots,J index orders. Order j has state-incidence coefficients a_{ij}\in\{0,1\}, limit quantity q_j, and limit price \pi_j. Define \begin{align*} e_i&:=\mathrm{Ind}(=,\mathrm{Oracle}(\omega,0),\mathrm{Const}(i)), &&i=1,\ldots,S,\\ P_j&:=\mathrm{LinComb}(a_{1j},\ldots,a_{Sj};e_1,\ldots,e_S). \end{align*} The claim program P_j emits a_{ij} when state i occurs. For strictly positive starting orders \theta_i, the Peters-So-Ye CPCAM chooses fills x_j, a common state payout M, and state slacks s_i by [45] \begin{align*} \text{maximize}\quad &\pi^\top x-M+\sum_{i=1}^{S}\theta_i\log s_i,\\ \text{subject to}\quad &\sum_{j=1}^{J}a_{ij}x_j+s_i=M &&(i=1,\ldots,S),\\ &0\leq x\leq q,\qquad s\geq0. \end{align*} The effective domain has s_i>0. Equivalently, the mechanism minimises M-\pi^\top x-\sum_i\theta_i\log s_i under affine constraints. Peters, So, and Ye prove that every optimum has the same slack vector s^\star and hence the same state-price vector p_i^\star=\theta_i/s_i^\star. The order-fill vector x need not be unique. For \theta(\mu)=\mu\bar\theta with \bar\theta_i>0, \sum_i\bar\theta_i=1, and \mu\downarrow0, they also prove that the state-price vector has a unique limit. The program gives a convex formulation of the limit-order parimutuel call auction of Lange and Economides [33, 34]. The payoff layer is the state-contingent program above; the price-formation layer is a batch program rather than a posted cost function.

(M5) Binary prediction contract.

Encode yes as 1 and no as 0. Two claims c_+ (yes) and c_- (no) read the numeric outcome attestation \omega\in\{0,1\}. The payoff program for c_+ is \mathrm{Ind}\bigl(=, \mathrm{Oracle}(\omega, 0), \mathrm{Const}(1)\bigr), and the program for c_- replaces \mathrm{Const}(1) with \mathrm{Const}(0). Price formation is selectable: the two-outcome LMSR (M3 with n = 2) or the parimutuel auction (M4 with S = 2); the claim-and-program layer is unchanged either way.

(M6) Linear perpetual contract.

A perpetual on a spot price S with funding F, resolving at every height of the interval H \subseteq \mathbb{N} over which the contract is open (Definition 2.11), reads a spot claim c_S and a funding claim c_F carrying the per-block funding payment, per-block feeds (Definition 2.11) with h-1, h-2 \in H_{c_S} and h-1 \in H_{c_F} for every h \in H, through the payoff program \mathrm{LinComb}(1, -1, -1; \;\mathrm{Ref}(c_S, 1), \;\mathrm{Ref}(c_S, 2), \;\mathrm{Ref}(c_F, 1)), emitting (S_{h-1} - S_{h-2}) - F_{h-1} at each h \in H: the one-block increment of the most recently resolved spot, net of the funding amount resolved at h-1, all read at strictly historical offsets. Under Definition 2.12, evaluation determines an entitlement equal to q times this increment at every height of H. For q>0, the entitlement increases with a spot-price rise and decreases with a spot-price fall or a positive funding amount. Over any sub-interval of H, the spot terms telescope to the change in S across it: the mark-to-market of a linear perpetual. Discharge remains governed by the route and evidence in the claim context. The amount qv_c(h) is a signed obligation whose sign determines debtor and creditor. For constant q on \{r,\ldots,s\}, \sum_{h=r}^{s}qv_c(h)=q\left(S_{s-1}-S_{r-2}-\sum_{h=r}^{s}F_{h-1}\right). The signed margin venue of Remark 8.3 provides cost-function price formation. A reserve-pool implementation instead trades a funded note from Proposition 8.2 against numeraire. The underlying spot pool transfers the asset units of (M1), and its authenticated price observations supply c_S. Each resolved amount retains its directed entitlement and discharge residual.

(M7) Fixed-coupon bond.

A fixed-coupon bond decomposes into two claims (Definition 2.11). A coupon strip has schedule \{h_1, \dots, h_K\} and resolved value c at each height. A principal claim has schedule \{h_K\} and resolved value F at maturity. Their programs are \mathrm{Const}(c) and \mathrm{Const}(F). The bond is the portfolio holding one unit of each (Definition 2.12); each context specifies how the corresponding entitlement is discharged. A transferable bond instrument can trade against numeraire under the title and reserve rules of (M1). Its promised cash flows retain their issuer and discharge risks. A funded-note representation supplies the explicit backing contract when that guarantee is required. The claim structure is independent of the trading venue.

(M8) Linear-payoff option.

A European call with strike K on underlying S has program \mathrm{Floor}\bigl(\mathrm{LinComb}(1, -1; \;\mathrm{Oracle}(S, 0), \;\mathrm{Const}(K)), \; 0\bigr). It emits \max(S-K,0). A put uses \mathrm{Floor}\bigl(\mathrm{LinComb}(-1,1;\;\mathrm{Oracle}(S,0),\;\mathrm{Const}(K)),0\bigr), and a standard collar combines one unit of the underlying, a long put at its lower strike, and a short call at its upper strike through one \mathrm{LinComb}. The option can use signed margin price formation or a funded-note reserve pool under Proposition 8.2 and Remark 8.3. Black-Scholes-Merton replication [13, 42] is a separate analysis. Asian, lookback, and barrier variants are covered by Proposition 5.3; smooth-indicator variants require transcendentals (Open problem 1).

This completes the eight decompositions. ◻

Remark 9.2 (Rounding and floors in a traditional parimutuel pool).

This mechanism is separate from CPCAM. Let stakes a_j\in\mathbb{Q}_{\geq0} and a commission rate \gamma\in\mathbb{Q}\cap[0,1) define the net pot P=(1-\gamma)\sum_j a_j. For a nonempty winning set W with A_W:=\sum_{j\in W}a_j>0, define y_j=\begin{cases}P\,a_j/A_W,&j\in W,\\0,&j\notin W.\end{cases} The exact payouts are rational and sum to P. Choose a fixed-point grid with \Delta\in\mathbb{Q}_{>0} and P/\Delta\in\mathbb{N}. Rounding each winning payout down leaves r:=P-\sum_{j\in W}\Delta\left\lfloor y_j/\Delta\right\rfloor, \qquad 0\leq r<|W|\Delta. A complete mechanism must specify which account receives r, or the deterministic order in which units of \Delta are assigned. A guaranteed floor replaces y_j by \max(y_j,g_j) and can exceed the pot. It therefore requires a named writer and a funding rule for the shortfall. These conclusions concern the traditional realised-pot mechanism just defined, not the fixed-payout CPCAM claims in (M4).

9.1 Tabular summary

Table 1. Payoff calculation and price formation for the eight constructions in Proposition 9.1. Read each row from the promised unit or conditional amount to the rule that prices its trade. The formulas abbreviate \Sigma programs and retain the stated financial types, entitlement terms, and reserve representation contracts. Price formation uses a cost function, a constant-function reserve constraint, or a convex clearing program. Central limit order books and request-for-quote systems use the same claim representation with their own price-formation rules (Remark 4.4).
Market type	Payoff program skeleton	Price formation	Reference
Constant-product AMM (M1)	\mathrm{Const}(1), unit resolved value	invariant R_1 R_2 = k; dual value V(p) = 2\sqrt{kp}	[4, 6]
Bonding curve (M2)	\mathrm{Const}(1), unit resolved value	cost function \int_0^s P(u)\,du, strictly convex for \gamma > 0	[10]
LMSR (M3)	\mathrm{Ind}(=, \omega, i)	cost function b \log \sum_i e^{q_i/b}	[28, 29]
Call auction (M4)	\sum_i a_{ij}\mathbb{1}[\omega=i] for order j	maximise \pi^\top x-M+\sum_i\theta_i\log s_i under affine balance and fill constraints; unique s^\star,p^\star	[45, 33]
Binary prediction (M5)	\mathrm{Ind}(=, \omega, 1) or \mathrm{Ind}(=, \omega, 0)	M3 at n = 2 or M4 at S = 2	[28, 47]
Perpetual (M6)	\mathrm{LinComb}(1,-1,-1; S_{h-1},\,S_{h-2},\,F_{h-1})	signed margin cost function, or funded-note reserve pool	[6]
Bond (M7)	\mathrm{Const}(c) strip; \mathrm{Const}(F) at h_K	transferable bond instrument, or funded-note representation	[6]
Linear option (M8)	\mathrm{Floor}(S{-}K, 0)	signed margin venue, or funded-note reserve pool	[13, 42, 31]

10 Sensitivity analysis

The two hypotheses support different conclusions. A positive-definite Hessian is necessary for a positive-definite quadratic leading form at the chosen equilibrium. A strict-positive reference offset is necessary for the simple height-grading guarantee. The next examples show the corresponding failures.

10.1 Relaxing the Hessian hypothesis

Example 10.1 (Strictly convex, zero curvature).

\varphi(x) = x^4 on \mathbb{R} is strictly convex, yet \varphi''(0) = 0. At the equilibrium x^\star = 0 (external price 0), total cost is T(\delta)=\delta^4 and the current marginal-price mark is zero. The first nonzero correction is quartic, not a positive-definite quadratic form. Strict convexity of the potential therefore does not deliver the hypothesis of Proposition 8.14; positive-definiteness of the Hessian at the equilibrium itself must be assumed.

Example 10.2 (Degenerate fibre and multiple equilibria).

Take n = 2 and \varphi(x_1, x_2) = (x_1 + x_2 - 1)^2/2. Then \nabla \varphi = (x_1 + x_2 - 1)(1,1) and C = \nabla^2\varphi = \mathbf{1}\mathbf{1}^\top everywhere, with kernel \operatorname{span}((1,-1)). For any external price vector p^\star = c\,(1,1), every point on the line x_1 + x_2 = 1 + c is an equilibrium: the equilibrium set is a fibre, not a point. The kernel direction is an exact invariance of \varphi, so the venue descends to the quotient coordinate s = x_1 + x_2, where \bar\varphi(s) = (s-1)^2/2 has \bar\varphi'' = 1 > 0 and Proposition 8.14 applies (Remark 8.19). As a two-claim venue it is well-posed only after the quotient, or after adding a strictly convex regulariser in the transverse direction.

10.2 Relaxing the strict-positive time offset

Example 10.3 (\tau = 0 admits cross-program cycles).

Relax Definition 2.1-(I3) to allow \tau = 0, and construct two claims c_1, c_2 whose schedules share a height, h \in H_{c_1} \cap H_{c_2}: c_1’s program contains \mathrm{Ref}(c_2, 0) and c_2’s program contains \mathrm{Ref}(c_1, 0). Each program is internally a well-formed DAG, yet the dependency graph has the 2-cycle (c_1, h) \to (c_2, h) \to (c_1, h) among instances at the single height h. The cycle-walk of Lemma 3.1 now gives 0 = \tau_1 + \tau_2, which \tau_1 = \tau_2 = 0 satisfies, so the contradiction is lost and the lemma fails: the scheduler has no first-resolved instance. Determining either payoff then requires a separate fixed-point semantics and can have zero or many solutions.

Remark 10.4 (Path dependence is not the same relaxation).

Path-dependent claims reference historical heights only — \mathrm{Ref} offsets and \mathrm{RefReduce} windows are strictly historical (Definition 5.1) — so they satisfy the strict-positive offset constraint as stated. The relaxation in Example 10.3 is qualitatively different: reference within the same block, not reference to history.

10.3 Local versus global

Remark 10.5 (The expansion is local).

Proposition 8.14 is a statement at the equilibrium point x^\star. Across a regime change that moves the reserve point substantially, a clearinghouse must integrate C(x) along the trajectory or refit at the new equilibrium; the local expansion is not a substitute for covariance estimation across regime switches. Open problem 5 quantifies the natural target.

11 Theorems, executable evidence, and external premises

The paper gives mathematical proofs of numerical expressiveness, relative constructor minimality, financial type preservation, rational refinement, schedule admission, entitlement preservation, funded signed representation, and the quantified curvature bound. The dependency and historical-reduction results apply to the selected program cases and their declared inputs. The market catalogue supplies conditional constructions whose instrument and provider premises remain explicit.

The accompanying reference implementations exercise the scalar-type rules, exact Python and JavaScript arithmetic, finite schedule admission, persistent entitlements, and funded-note identities. The complete evaluator implements all stated constructors and financial interfaces through one instruction graph. Its continuation retains observations, witnesses, historical evidence, pending work, completed values, and cumulative counters. The SQLite composition stores that continuation with the current shared ledger and command outcomes. Proposition 6.3 and Theorem 6.5 give the corresponding induction arguments and their explicit premises. The two complete programs and process-interruption observations exercise these relations in executable code. Their source identities and test inputs define the reproducible implementation scope. A mechanized proof over the implementation, compiler refinement, distributed scheduling, and authenticated provider integration require their own correspondence results. The local transaction construction supplies neither external settlement atomicity nor an external anchor against whole-database rollback.

The accompanying The Claim as Primitive: reference supplement contains these implementations, tests, input vectors, and reproduction instructions. Its SHA-256 digest is

a2569c787ab68c7bd62b334235d32317bda18c5504d8173208aff5f50da4f178.

12 Open problems

The constructions leave three kinds of question. A larger numerical language needs a new expressiveness theorem. More efficient execution and quoting need certificates that preserve the same values and evidence. Actual payment completion needs provider-specific assumptions and a correspondence with the entitlement journal. The problems below state these requirements without changing the claims already defined.

Open Problem 1 (Analytic extensions of \Sigma).

Extend \Sigma with stated analytic primitives and characterise the resulting exact function class. \mathrm{Log} represents log-return statistics; \mathrm{Exp} and a logistic primitive represent smooth indicators; \mathrm{Sqrt} represents square-root transforms. Vanilla call and put payoffs already belong to \Sigma. A closed-form Black-Scholes-Merton price [13, 42] is a pricing function rather than a payoff and additionally requires the normal cumulative distribution function \Phi, equivalently \operatorname{erf}. Determine which finite primitive set suffices for each target family and state the domain of every partial primitive.

Open Problem 2 (Clearing complexity).

Peters-So-Ye clearing is one convex program per batch, and their path-following method gives a fully polynomial-time approximation scheme [45]. Determine whether sparsity, bounded bundle size, or block structure in the state-incidence matrix improves its arithmetic bound, and establish any matching lower bound.

Open Problem 3 (Mechanism-design bounds for the operator language).

Given \Sigma as the language of expressible payoffs, characterise the strictly proper mechanisms expressible as cost-function markets (Definition 8.4) over \Sigma payoffs. Hanson’s LMSR [28] fits, as does the conjugate class of Abernethy-Chen-Vaughan [3]; the Peters-So-Ye auction clears by a batch program rather than a posted potential (Section 9), and the liquidity-sensitive maker of Othman-Pennock-Reeves-Sandholm [44] achieves liquidity sensitivity by allowing prices to sum above one. Whether \Sigma constrains the admissible potentials beyond the conjugate characterisation is open.

Open Problem 4 (Admissibility and collateral for unbounded payoffs).

The language already represents unbounded linear, polynomial, perpetual, and option payoffs. Specify conditions under which a venue admits such a program and collateralises the resulting position. Candidate conditions include a stated liquidation rule, integrability against a named distribution, a coherent tail-risk bound, and collateral that changes with the position. Determine which conditions are sufficient for finite loss coverage without changing the payoff semantics.

Open Problem 5 (Sharper computed curvature certificates).

Proposition 8.15 gives the integral modulus bound and sharp Lipschitz constant. Develop efficient certified bounds for structured high-dimensional venue potentials and finite-precision inputs. The certificate should select a useful trade radius while retaining measured numerical and derivative errors. For piecewise-smooth potentials, identify every crossed boundary and combine region certificates under the applicable transition rule.

Open Problem 6 (Efficient certified evaluation).

Proposition 2.14 and Proposition 2.16 establish exact rational refinement and sound comparison certification. Develop smaller certificates and faster evaluation for large shared payoff graphs while preserving their evidence manifests. Quantify refinement effort for uncertain inputs near switching sets, including exact-boundary cases that require additional authoritative evidence. A returned ambiguity must remain an explicit evaluator result throughout compilation and resumption.

Open Problem 7 (Provider completion guarantees).

The entitlement journal preserves delayed and partial performance under Proposition 3.7. Establish completion-time guarantees for specified providers, currencies, reservation mechanisms, and evidence routes. Prove the correspondence between their command and occurrence records and the shared allocation contract. The result must retain pending and recovery states when its availability assumptions fail.

13 Conclusion

The call introduced at the start requires an observation, a calculation, and a payment obligation with identified parties and terms. The claim construction keeps these records connected as formulas become dependent programs, historical schedules, and recurring coupons. The exact expressiveness theorem identifies the numerical functions those programs represent. The evaluation and entitlement results explain how their values, evidence, and unpaid balances survive composition and local retry under the stated premises. A complete producer certificate also permits ordered calculations within one event.

The market then prices the specified right. Its curvature determines local price impact, with a certified error bound when the Hessian’s variation is controlled. A covariance interpretation additionally requires the log-partition structure and its implied probability law. Funding makes a bounded signed payoff available as complementary transferable notes while preserving its financing leg. External evidence authority, custody, and completion of payment retain their own contractual and verification requirements. The common claim representation makes those requirements explicit throughout the calculation and its performance record.

References

[1] SQLite. Write-ahead logging. Technical documentation. https://www.sqlite.org/wal.html.

[2] SQLite. PRAGMA statements: synchronous. Technical documentation. https://www.sqlite.org/pragma.html#pragma_synchronous.

[3] J. Abernethy, Y. Chen, and J. Wortman Vaughan. Efficient market making via convex optimization, and a connection to online learning. ACM Transactions on Economics and Computation, 1(2):12:1-12:39, 2013.

[4] H. Adams, N. Zinsmeister, and D. Robinson. Uniswap v2 core. Technical report, Uniswap Labs, 2020.

[5] P. Alvaro, W. R. Marczak, N. Conway, J. M. Hellerstein, D. Maier, and R. Sears. Dedalus: Datalog in time and space. In Datalog Reloaded, Lecture Notes in Computer Science 6702, pp. 262-281. Springer, 2011.

[6] G. Angeris, H.-T. Kao, R. Chiang, C. Noyes, and T. Chitra. An analysis of Uniswap markets. Cryptoeconomic Systems, 1(1), 2021.

[7] G. Angeris and T. Chitra. Improved price oracles: Constant function market makers. In Proceedings of the 2nd ACM Conference on Advances in Financial Technologies (AFT’20), 2020.

[8] G. Angeris, A. Evans, and T. Chitra. Replicating market makers. arXiv:2103.14769, 2021.

[9] K. R. Apt, H. A. Blair, and A. Walker. Towards a theory of declarative knowledge. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pp. 89-148. Morgan Kaufmann, 1988.

[10] E. Hertzog, G. Benartzi, and G. Benartzi. Bancor protocol: Continuous liquidity for cryptographic tokens through their smart contracts. Whitepaper, 2017.

[11] G. Berry and G. Gonthier. The Esterel synchronous programming language: Design, semantics, implementation. Science of Computer Programming, 19(2):87-152, 1992.

[12] G. Berry. The constructive semantics of pure Esterel. Draft book, version 3, 1999.

[13] F. Black and M. Scholes. The pricing of options and corporate liabilities. Journal of Political Economy, 81(3):637-654, 1973.

[14] D. T. Breeden and R. H. Litzenberger. Prices of state-contingent claims implicit in option prices. Journal of Business, 51(4):621-651, 1978.

[15] L. D. Brown. Fundamentals of Statistical Exponential Families. IMS Lecture Notes Monograph Series 9, 1986.

[16] A. Capponi and J.-W. Chang. Settlement speed and financial stability. Finance and Economics Discussion Series 2025-101, Board of Governors of the Federal Reserve System, November 2025. https://doi.org/10.17016/FEDS.2025.101.

[17] D. Bullmann. Keeping settlement risk high on the public policy agenda. The Eurofi Magazine, 30 September 2025.

[18] CLS and FNA. Reimagining same-day FX: Exploring the case for additional settlement cycles. ShapingFX report, 6 March 2025.

[19] P. Caspi, D. Pilaud, N. Halbwachs, and J. A. Plaice. LUSTRE: A declarative language for programming synchronous systems. In Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL’87), pp. 178-188, 1987.

[20] Y. Chen and D. M. Pennock. A utility framework for bounded-loss market makers. In Proceedings of UAI 2007, pp. 49-56, 2007.

[21] R. Cytron, J. Ferrante, B. K. Rosen, M. N. Wegman, and F. K. Zadeck. Efficiently computing static single assignment form and the control dependence graph. ACM Transactions on Programming Languages and Systems, 13(4):451-490, 1991.

[22] W. Du. Three myths about payment innovations. Panel remarks, Jackson Hole Economic Policy Symposium, 29 August 2026.

[23] Federal Reserve Financial Services. Fedwire Funds Service. Service description and operating rules, updated 25 June 2024.

[24] R. Frongillo, M. Papireddygari, and B. Waggoner. An axiomatic characterization of CFMMs and equivalence to prediction markets. arXiv:2302.00196, 2023.

[25] C. Ates, M. L. Bech, R. Garratt, and M. Nanut Petrič. Auction-based liquidity saving mechanisms. BIS Working Papers 1318, December 2025; revised January 2026.

[26] M. B. Goldman, H. B. Sosin, and M. A. Gatto. Path dependent options: “Buy at the low, sell at the high”. Journal of Finance, 34(5):1111-1127, 1979.

[27] N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous data flow programming language LUSTRE. Proceedings of the IEEE, 79(9):1305-1320, 1991.

[28] R. Hanson. Combinatorial information market design. Information Systems Frontiers, 5(1):107-119, 2003.

[29] R. Hanson. Logarithmic market scoring rules for modular combinatorial information aggregation. Journal of Prediction Markets, 1(1):3-15, 2007.

[30] R. A. Horn and C. R. Johnson. Matrix Analysis. Cambridge University Press, 2nd edition, 2013.

[31] J. C. Hull. Options, Futures, and Other Derivatives. Pearson, 10th edition, 2017.

[32] A. G. Z. Kemna and A. C. F. Vorst. A pricing method for options based on average asset values. Journal of Banking and Finance, 14(1):113-129, 1990.

[33] J. Lange. Financial products having a demand-based, adjustable return, and trading exchange therefor. U.S. Patent 6,321,212, 2001.

[34] J. Lange and N. Economides. A parimutuel market microstructure for contingent claims. European Financial Management, 11(1):25-49, 2005.

[35] R. Lorgat. One-Way Coupling of Prediction Markets to Automated Market Makers. Technical paper, 2026.

[36] R. Lorgat. Parlay Identification of Ising Couplings in Correlated Binary Event Markets. Technical paper, 2026.

[37] R. Lorgat. Admissible Obligation Transitions. Companion paper, 2026.

[38] R. Lorgat. Event-Collect BFT. Companion paper, 2026.

[39] R. Lorgat. Recourse. Companion paper, 2026.

[40] A. Martin and J. McAndrews. Liquidity-saving mechanisms. Journal of Monetary Economics, 55(3):554-567, 2008.

[41] Marex Group Limited. Contingent Income (with Memory) Barrier Notes linked to the worst performing of three common stocks. Preliminary pricing supplement filed under Rule 424(b)(2), Registration No. 333-289203, 8 July 2026. https://www.sec.gov/Archives/edgar/data/1997464/000110465926081706/tm2619531d2_424b2.pdf.

[42] R. C. Merton. Theory of rational option pricing. Bell Journal of Economics and Management Science, 4(1):141-183, 1973.

[43] H. Nakano. A modality for recursion. In Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS’00), pp. 255-266, 2000.

[44] A. Othman, D. M. Pennock, D. M. Reeves, and T. Sandholm. A practical liquidity-sensitive automated market maker. ACM Transactions on Economics and Computation, 1(3):14:1-14:25, 2013.

[45] M. Peters, A. M.-C. So, and Y. Ye. A convex parimutuel formulation for contingent claim markets. In Proceedings of the 7th ACM Conference on Electronic Commerce (EC’06), 2006. https://web.stanford.edu/~yyye/cpcam-ec.pdf.

[46] S. Peyton Jones, J.-M. Eber, and J. Seward. Composing contracts: an adventure in financial engineering. In Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming (ICFP’00), pp. 280-292, 2000.

[47] C. R. Plott and S. Sunder. Efficiency of experimental security markets with insider information: An application of rational-expectations models. Journal of Political Economy, 90(4):663-698, 1982.

[48] C. R. Plott and S. Sunder. Rational expectations and the aggregation of diverse information in laboratory security markets. Econometrica, 56(5):1085-1118, 1988.

[49] Committee on Payment and Settlement Systems and Technical Committee of the International Organization of Securities Commissions. Principles for Financial Market Infrastructures. Bank for International Settlements, April 2012. https://www.bis.org/publications/principles-financial-market-infrastructures.pdf.

[50] The Clearing House. CHIPS delivers record value and resilience for participants in 2025. 7 April 2026.