Dependencies

The amortizing contracts, defined as deltas over PAM: a linear principal redemption (LAM), interest-first redemption (NAM), and constant-instalment annuity with rate-reset re-amortization (ANN).

The annuity amount sizes the constant ANN instalment so the notional is fully repaid by maturity:

with \(a\) the accrued interest at \(s\), \(r\) the rate, and \(t_1,\dots ,t_m\) the future PR-schedule times of the annuity (§5.5).

Array schedules generalise \(S\) to vector inputs \(\vec{s}=(s_0,\dots ,s_m)\), \(\vec{c}=(c_0,\dots ,c_m)\):

coinciding with \(S\) for \(m=1\). Used by LAX (§5.3).

The child-contract observer lets a parent read its children: future events \(U^{ev}:i,t,a\mapsto \{ e_v^k,\dots \} \), a child state variable \(U^{sv}:i,t,x,a\mapsto \mathbb {R}\), or a child attribute \(U^{ca}:i,x\mapsto y\) — the basis for evaluating swaps, options and credit enhancement over their underlyings.

Call money: PAM state transitions with interest capitalizing until maturity. The open “call has no fixed maturity — it closes on an observed exercise (\(\texttt{XD}=\sup \tau (O^{ev}(\texttt{CID},))\)), settling the grown notional after the exercise-notice period.

The end-of-month convention EOMC fixes whether cyclic times anchored on a short month-end fall on the same day or the month-end; the business-day convention BDC shifts a time off a non-business day (following/preceding, modified or not, calculate-before or -after the shift); and the business-day calendar \(B:t\mapsto \{ \text{true,false}\} \), selected by CLDR, decides which days are business days (NoHoliday, MondayToFriday, …).

CEG (guarantee) and CEC (collateral, §5.18) over covered contracts: a premium at purchase, and on a covered contract’s observed credit event the covered exposure settles — capped at the observed collateral value for CEC.

Combined contracts derive their payoff from child contracts (underlyings) referenced through the attribute CTST, a list of contract references each carrying an object, a type and a role. We write \(\texttt{CTST}_{role}^{type}\) to query a referenced child (omitting the index of the first match), e.g. \(\texttt{CTST}_{FirstLeg}^{Contract}\) for a swap’s first leg or \(\texttt{CTST}_{Underlying}^{Contract}\) for an option’s underlying.

Cash-settled derivatives: a European option’s intrinsic value (OPTNS, §5.15), a future’s linear payoff \(S-F\) (FUTUR, §5.16), an FX outright’s two-currency settlement (FXOUT), and an interest-rate cap/floors rate-excess over a child contract’s reset rate (CAPFL, §5.14).

genSchedule builds the full event Schedule (IED, IP/IPCI, PR, RR/RRF, FP, SC, MD, …) for a stateful contract from its dictionary terms, following the Contract-Schedule tables above; runSchedule then folds the contract’s stf/pof over it. This is the type-agnostic core shared by every contract family.

IPCITrace is the chain of zero or more admissible interest capitalizations (IPCI) of a UMP deposit; ipciFactor accumulates the multiplicative growth factor \(\prod _i (1 + \mathtt{rate}\cdot Y_i)\) along it.

LAXPRTrace is the chain of zero or more admissible LAX principal redemptions (PR) with non-negative instalments.

LAX (exotic amortizer) redeems or draws principal on piecewise array schedules; UMP (§5.7) is a non-maturity deposit whose interest capitalizes, settling at the agreed price plus accrued interest on termination. Both carry the relational Step and functional stf/pof models (proven to agree), alongside their executable builders.

The relational one-step transition; each constructor’s target is the functional next-state stf of the table above, so the relation is exactly the graph of stf (Theorem 21).

The PAM state-transition function \(\mathrm{STF}\_ k\_ PAM()\), one branch per event type, together with the payoff function \(\mathrm{POF}\_ k\_ PAM()\), as given by the table below.

COM (commodity, §5.10) and STK (stock): a purchase (PRD) and termination (TD) at the observed price, plus observed dividends (DV) for stock. (CSH, §5.8, has no scheduled cash flow.)

PRTrace is the sub-relation of the LAM execution trace consisting of zero or more admissible principal-redemption (PR) steps — the regime in which the notional should be conserved (events like IED/IPCI reset or grow it).

The risk-factor observer is the interface through which a contract reads its uncertain environment. In rate mode it returns a market state, \(O^{rf}:i,t\mapsto \mathbb {R}\), and in event mode it returns observed unscheduled events, \(O^{ev}:i,k,t\mapsto \{ e_t^k,\dots \} \) — e.g. \(O^{rf}(\texttt{RRMO},t)\) for a reset reference rate, or \(O^{ev}(\texttt{CID},\texttt{PP},t)\) for observed prepayments. The interface fixes structure only; implementations encode whatever assumption a forward-looking analysis requires.

The schedule function maps an anchor \(s\), a cycle \(c\) and an end date \(T\) to the cyclic sequence

with \(t_i{\lt}t_{i+1}\). Cycles have the form \(NPS\) (\(N\) an integer, \(P\in \{ D,W,M,Q,H,Y\} \) a period unit, \(S\in \{ +,-\} \) a stub rule). An optional boolean \(B\) in \(S(s,c,T,B)\) controls whether the end date \(T\) belongs to the schedule, and the EOMC/BDC conventions (below) may shift the resulting times, so the sequence need not be equidistant.

The canonical payoff of a contract aggregates all future event payoffs under frozen risk-factor conditions, \(F(x,t)=\sum _{c\in C}c\). When a contract settles in a currency CURS other than its denomination CUR, payoffs are scaled by the settlement FX rate

which appears as the leading factor of every payoff function below.

The contract-role sign \(R:\texttt{CNTRL}\to \{ -1,+1\} \) maps a contract role to \(+1\) for a claim (asset) or \(-1\) for an obligation, fixing the direction of every role-sensitive cash flow and state (a positive flow runs from CPID to CRID). E.g. \(\texttt{RPA}\mapsto +1\), \(\texttt{RPL}\mapsto -1\), \(\texttt{GUA}\mapsto -1\), \(\texttt{OBL}\mapsto +1\). We abbreviate \(R(\texttt{CNTRL})\).

SWPPV pays a fixed and a floating interest leg per period (with the relational Step and functional stf/pof models, proven to agree); SWAPS (§5.13) is a composite of two child legs run by the ordinary engine and combined gross or net.

The year-fraction interface \(Y:s,t,\texttt{DCC}\mapsto \mathbb {R}\) gives the fraction of a year between two times under a day-count convention DCC (Actual/360, Actual/365, 30E/360, Actual/Actual ISDA, Business/252). Per-annum rates are accrued by multiplying with \(Y\).

For each of the eight stateful contracts (PAM, LAM, NAM, ANN, CLM and LAX, SWPPV, UMP) every relational step lands on the functional next-state for some event and time; conversely every admissible event/time yields a step. Each relation is exactly the graph of its stf.

With a strictly positive notional and instalment a redemption strictly decreases the notional (guaranteed progress); once the instalment reaches the outstanding notional the step drives it to exactly \(0\) (clean repayment).

Along an entire principal-redemption trace the notional stays in \([0, \mathtt{Nt}_0]\) and never increases in magnitude — the single-step non-overshoot lifted to whole executions by induction over the trace. Every PRTrace is moreover a genuine LAM execution trace, so this is a statement about real runs.

An FX outright’s two delivery legs net to the par difference \(R \cdot (\mathtt{Nt_1} - \mathtt{Nt_2})\) at unit FX; a swap’s per-period fixed and floating legs net to \(R \cdot N \cdot (\mathtt{fix} - \mathtt{flt}) \cdot Y\) — exactly what the net-settlement fold computes from the two gross legs. For SWPPV this is now proven on the actual stf/pof state machine (swppv_pof_net), and at par (\(\mathtt{fix}=\mathtt{flt}\)) the netted period flow is zero.

A collateral payout \(\min (\mathtt{coverage}\cdot \mathtt{exposure}, \mathtt{value})\) never exceeds either the posted collateral value or the covered claim; the covered exposure, a sum of per-leg magnitudes, is non-negative, so the payout carries the contract-role sign.

The cap/floor rate-excess kernel \(\max (r - \mathtt{cap}, 0) + \max (\mathtt{floor} - r, 0)\) and the European call/put intrinsics \(\max (S - K, 0)\), \(\max (K - S, 0)\) are all \(\ge 0\), so a long cap, floor, or option never settles negative; a call is in the money exactly when the underlying exceeds the strike.

The IPCI event moves accrued interest into the notional and resets accrued interest to \(0\): value is relocated, not created. (This one holds definitionally at any amount type.)

On the long side (\(\mathrm{sign} \ge 0\)) a LAX redemption with a non-negative instalment never increases the notional, so along an entire redemption trace \(\mathtt{Nt}' \le \mathtt{Nt}_0\) (monotone repayment). Unlike LAM’s capped redeemed this is a one-sided bound, since STF_PR_LAX subtracts the raw instalment. Every such trace is a genuine LAX execution.

The maturity event zeroes the notional principal (and accrued interest and fees); termination additionally zeroes the interest rate.

Along any execution trace the status date is non-decreasing: each step requires \(\mathtt{Sd} \le t\) and sets \(\mathtt{Sd} := t\).

A principal redemption never overshoots: with a sign-normalised nonnegative state the post-redemption notional stays in \([0, \mathtt{Nt}]\), and the redeemed amount never exceeds the outstanding notional in magnitude (\(|\, \mathrm{redeemed}\, | \le |\mathtt{Nt}|\)).

After a rate reset the nominal rate lies within the life floor/cap window \([\mathtt{RRLF}, \mathtt{RRLC}]\) (whenever both are present and well-ordered). Holds for PAM, for ANN (by reuse of PAM’s rate logic), and for SWPPV’s floating-rate reset. With every cap/floor absent the reset instead returns the raw repricing target \(O^{rf}(\mathtt{RRMO},t)\cdot \mathtt{RRMLT}+\mathtt{RRSP}\) (pam_rr_uncapped).

A swap exchanges interest, not principal: no SWPPV event moves the notional, and only a rate reset (RR) changes the floating rate. Status dates are non-decreasing along any execution (even though the fixed leg and reset leave \(\mathbf{Sd}_{}\) untouched and only the floating leg advances it).

Along a capitalization trace the notional grows multiplicatively to \(\mathtt{Nt}' = \mathtt{Nt}_0 \cdot \prod _i (1 + \mathtt{rate}\cdot Y_i)\); the nominal rate is invariant under IPCI (justifying the single \(\mathtt{rate}\)), and with a non-negative rate and year fraction each capitalization never shrinks the deposit.