Global Model

Fix a family of markets $k$, accounts $a$, and per-account-per-market positions. The engine is the transition system $S' = f_e(S, u)$ where $e$ ranges over a finite alphabet of engine events — deposit and withdrawal, order submission with matching, cancel/expiry, funding accrual, funding settlement, and the liquidation cascade — and $u = (P_{oracle,k}, t_{last,k})_k$ is an exogenous input: a trusted price and its timestamp per market, handed to the engine as given. From $u$ and its own trade window $W_k$ the engine derives the mark $m_k = w\,P_{oracle,k} + (1-w)\,P_{trade}(W_k)$ ((O.8), (O.7)); every event map below is a function of $(S, u)$ through $m_k$ alone. The orbit of the Exchange is the trajectory of $S$ under an interleaving of these maps: fills build entry prices ((T.1)), marks revalue them ((T.2)), funding transfers value between the sides ((F.4)), and the cascade repossesses positions whose equity has fallen to the maintenance floor ((L.4)).

The coupling quantity that organizes the whole engine is equity, $E = C + \Pi$ ((M.5)): affine in the mark, additive over positions, and read by every guard that matters. Admission compares equity headroom against initial margin ((M.13), (M.14)); the liquidation trigger compares it against maintenance margin ((L.4)); withdrawal deliberately ignores it and moves only realized collateral ((M.16)). Because maintenance is strictly inside initial ($r_m < r_i$, (M.4) vs (M.2)), the state space is stratified into a healthy region, a buffer, and the liquidation region — and the engine's dynamics are precisely the story of how event maps move accounts between these strata while conserving value at every step.

The state space

The state set. A state is the tuple

$S = \big( (C_a, M_{resv,a}, n_{resv,a})_a,\ (s_{a,k}, P_{e,a,k})_{a,k},\ (B_k, A_k, T_k, W_k, \Phi_k, \Sigma_{\mathrm{abs},k}, \Sigma_{\mathrm{rec},k})_k,\ C_{pool},\ C_{fee} \big)$

with components, per account, realized collateral, reserved margin, and the open-reservation count; per position, a signed size $s$ (direction $\sigma = \operatorname{sign}(s)$, magnitude $q = |s|$) and a volume-weighted entry price $P_e$; per market, the resting-order multiset $B_k$ (each order carrying side, limit price, and remaining quantity $q - q_f$), the funding accumulator pair $(A_k, T_k)$, the five-trade window $W_k$, and the insurance fund balance $\Phi_k$ with its lifetime ledgers; and two system accounts, the funding pool $C_{pool}$ and the Exchange fee account $C_{fee}$. The input $u_k = (P_{oracle,k}, t_{last,k})$ and its guard bookkeeping $\Omega_k$ (ten-print history, pending re-anchor block) are input-process state, exogenous to the engine but declared here because Part II's map writes them.

The per-position funding accumulator is not a coordinate. The corpus fixes the convention $\varphi_{a,k} \equiv 0$: funding accrual touches only the market pair $(A_k, T_k)$ ((F.2)), and settlement computes each payment fresh from $(A, T)$ and resets atomically — no event map ever writes a nonzero value into a per-position accumulator, so carrying one would be writer-less state, not well-defined dynamics. Consequently the funding-integral term of (M.8) reads identically zero at every observable state, and live equity is $E_{pf} = C + \sum_i s_i (m_i - P_{e,i})$: the funding channel into equity is the collateral debit at settlement, nothing else.

The admissible region $\mathcal{A}$ is cut out by: strictly positive stored position sizes $q_{a,k} > 0$ with $|s|$ on the lot lattice $\ell\mathbb{Z}$ ((B.1)); positive entry prices; resting limit prices strictly positive on the tick lattice $\delta\mathbb{Z}$ ((B.2)) with the book uncrossed, $P_b < P_a$; strictly positive remaining quantity on every resting order; $M_{resv} \ge 0$ and $n_{resv} \ge 0$; market parameters with $0 \le r_m < r_i$ (validated at parse, the ordering behind (M.4) $\le$ (M.2)); $\Phi_k \ge 0$ with $\Phi = \Sigma_{\mathrm{rec}} - \Sigma_{\mathrm{abs}}$; $T_k \ge 0$; and $C_a$ unrestricted in sign — collateral can be driven negative by unguarded engine-internal debits, and the model keeps that honesty rather than assuming $C_a \ge 0$.

The event alphabet and totality. The engine and input alphabets are

$\begin{gathered} \Sigma_E = \{\texttt{deposit\_withdrawal},\ \texttt{order\_submission\_fill},\ \texttt{order\_cancel\_expiry}, \\ \texttt{funding\_accrual},\ \texttt{funding\_settlement},\ \texttt{liquidation\_cascade}\}, \qquad \Sigma_O = \{\texttt{oracle\_print}\}. \end{gathered}$

Every map is well-defined on $\mathcal{A}$ because each carries explicit domain guards: withdrawal is gated by the flat-and-unreserved predicate ((M.16)); admission by alignment, collar, and headroom guards evaluated before any mutation; the funding rate is total via its explicit $T = 0$ branch ((F.3)); accrual accepts only strictly advancing time and positive anchor ((F.2)); every $\min$/$\max$ in the cascade and the fund ((I.1), (I.9)) is total and sign-safe; tick alignment clamps to one tick rather than producing non-positive prices ((L.9)); and the reduce-only guard ((L.13)) rejects the one known oversized-close regime before the book is touched.

State coordinates

Symbol	Name	Scope	Description	Units
$C_a$	account_collateral	account	Realized USDX collateral of account $a$: the only coordinate deposits and withdrawals touch, the cash leg of realized PnL, fees, funding, and liquidation settlement. Sign-unrestricted — engine-internal debits (funding settlement, penalties) are unguarded.	USDX
$M_{resv}$	reserved_margin	account	Initial margin reserved by resting orders of account $a$, carried with the open-reservation count $n_{resv}$; written at admission, released on fill or cancel, and read by the cross admission gate (M.14) and the withdrawal guard (M.16).	USDX
$s_{a,k}$	signed_position_size	position	Signed position size of account $a$ in market $k$: $\sigma = \operatorname{sign}(s)$, $$q =	s
$P_{e,a,k}$	entry_price	position	Volume-weighted entry price maintained exclusively by (T.1): same-side fills blend, reductions leave it untouched, flips re-seed it at the fill price. The anchor of every PnL and bankruptcy computation.	USDX per base unit
$B_k$	order_book	market	Resting-order multiset of market $k$ — per order: side, limit price on the tick lattice, remaining quantity $q - q_f > 0$ — with its id index in exact agreement. Uncrossed ($P_b < P_a$) in every reachable state; mutated by matching, resting, cancel/expiry, and self-trade prevention (B.8).	multiset of orders
$A_k$	accumulated_premium	market	Time-weighted premium accumulator of the current funding interval, written only by (F.2) and reset to zero atomically at settlement.	dimensionless-seconds
$T_k$	interval_clock	market	Elapsed accumulated time of the current funding interval; $T \ge 0$ always (saturating subtraction), reset with $A_k$ at settlement; the $T = 0$ branch of (F.3) keeps the rate total.	seconds
$W_k$	trade_window	market	The last five executed fills $(P^{\star}, q^{\star})$ of market $k$, written by the fill map (including liquidation close fills) and read by the volume-weighted median (O.7) — the engine-owned leg of the mark blend and the channel by which the engine feeds back into its own input.	five (price, size) pairs
$\Phi_k$	insurance_fund_balance	system	Per-market insurance fund balance, carried with its lifetime ledgers $\Sigma_{\mathrm{abs}}, \Sigma_{\mathrm{rec}}$ satisfying $\Phi = \Sigma_{\mathrm{rec}} - \Sigma_{\mathrm{abs}}$; credited by spread profit (I.7) and penalties (I.10), debited by absorption (I.2); $\Phi \ge 0$ with exact depletion.	USDX
$C_{pool}$	funding_pool	system	The funding pool book through which every funding transfer routes ((S.6)): positive payments flow account-to-pool, negative pool-to-account. Across the matched open interest of one settlement it nets to zero exactly.	USDX
$C_{fee}$	exchange_fee_account	system	The Exchange fee account: credited taker fees, debited maker rebates ((S.2), (S.3)), with closure $V = F - R$ ((S.5)). Liquidation penalties never enter it — they route to the fund.	USDX
$P_{oracle,k}$	oracle_anchor	market	The trusted anchor price of market $k$ — the engine's input $u_k$. Input-process state: moved only by the guarded accept and re-anchor promotion branches of the oracle map, never by any engine event.	USDX per unit of asset
$t_{last,k}$	anchor_timestamp	market	Timestamp of the last trusted anchor update, read by the staleness predicate (O.4); frozen together with the anchor while a re-anchor is pending.	milliseconds
$\Omega_k$	oracle_guard_state	market	The input process's defense bookkeeping: the ten-print history $H$ behind (O.2) and the pending re-anchor block $(P_{cand}, n_p, t_0)$ behind (O.5) and (O.6). Declared per the state-completeness directive; touched only by the oracle map.	prints and milliseconds

Event dynamics

The engine is event-driven: the state sits still between events, and each event is a deterministic map $S' = f(S, u)$ with the oracle price $u$ given.

Deposit / Withdrawal

Fires when an account moves external USDX in or out. A deposit is unguarded: any positive amount credits $C_a$ and touches nothing else. A withdrawal is guarded by the flat-and-unreserved predicate (M.16): it debits at most $C_a$, and only when $n_{pos} = 0$ and $n_{resv} = 0$ — equity and available margin never enter the withdrawal path, so unrealized PnL can never leave the venue before a close realizes it into collateral. The guard's $n_{resv} = 0$ arm is what the cancel/expiry map (below) makes reachable. Touches: $C_a$ only.

$$C_a' = C_a + x \quad (x > 0,\ \text{deposit}); \qquad C_a' = C_a - x \quad \big(0 < x \le W_{max},\ \ W_{max} = C_a\,\mathbb{1}[\,n_{pos} = 0 \wedge n_{resv} = 0\,]\big) \tag{G.1}$$

Order submission, matching, and fill

Fires on order submission. Admission guards run first, mutating nothing on rejection: lot and tick/positivity alignment ((B.1), (B.2)), the mark collar ((B.3)), FOK availability ((B.5)), and margin headroom — the isolated path (M.13) at the effective rate (M.1), the cross path (M.14) charging only added exposure ((M.11), (M.12)) against equity net of all outstanding reservations. Admission writes $M_{resv}$ atomically with the check. The matching loop then walks price-time priority: each fill exchanges $q^{\star} = \min(q_t, q_m)$ at the maker's price ((B.6), (B.7)), bounded for market orders by the running-VWAP slippage band ((B.9), (B.10)). Self-trade prevention fires inside this loop: (B.8) decrements both same-account orders' quantities with no virtual fill, handing the fully-reduced side to the cancel map. Each fill updates positions — same-side blend (T.1), reduce (T.3) realizing (T.4) into $C_a$ at the fill price, flip (T.5) — debits the taker fee and credits the maker rebate between $C_a$ and $C_{fee}$ ((S.2), (S.3), closure (S.5)), and appends $(P^{\star}, q^{\star})$ to the trade window $W_k$ — the coordinate Part III's mark blend reads. Touches: $B, M_{resv}, s, P_e, C_a, C_{fee}, W$.

$$\begin{aligned} q^{\star} &= \min(q_t, q_m), \qquad P^{\star} = P_{mk}, \qquad W' = W \oplus (P^{\star}, q^{\star}), \qquad B' = B \ominus q^{\star}\ \text{at}\ P_{mk} \\ P_e' &= \frac{q\,P_e + q_f\,P^{\star}}{q + q_f}\ \ (\text{same side}), \qquad q_c = \min(q, q_f), \qquad q_{new} = q_f - q\ \ (\text{flip}) \\ C_a' &= C_a + \sigma\,(P^{\star} - P_e)\,q_c - F_t + F_m, \qquad C_{fee}' = C_{fee} + F_t - F_m \end{aligned} \tag{G.2}$$

Order cancel / expiry

Fires on user cancellation, IOC/FOK/market-remainder expiry, post-only rejection of a crossing order, slippage-cap cancellation ((B.10)), the reduce-only rejection of an oversized liquidation close ((L.13)), and self-trade prevention's cancel-of-the-fully-reduced-side ((B.8)) — this map is where the STP path lands at the composition level. It removes the order from $B_k$ and its id index together (the book/index agreement is preserved by the shared removal helpers), decrements $n_{resv}$, and releases the order's reserved margin from $M_{resv}$. This release is load-bearing: (M.16) guards on $n_{resv} = 0$ and (M.14) reads $M_{resv}$, and both are consistent only because cancellation returns the reservation. The book-side removal is fully witnessed; the corpus contains no expression for the per-order release amount $\mu(o)$, so the collateral-side arithmetic of this map is a named gap (cancel_release_arithmetic_unwitnessed) — nothing is cited for it. Touches: $B, M_{resv}, n_{resv}$.

$$B' = B \setminus \{o\}, \qquad n_{resv}' = n_{resv} - 1, \qquad M_{resv}' = M_{resv} - \mu(o) \quad (\mu(o)\ \text{unwitnessed — named gap}) \tag{G.3}$$

Funding accrual

Fires on each premium sample with strictly advancing time and a strictly positive anchor; otherwise the state passes through unchanged. It computes the premium of the perp reference $P_{trade}$ against the given input $u$ ((F.1)) — not the mark — and adds its time-weighted contribution to the interval accumulator ((F.2)). This map touches exactly two coordinates — $(A_k, T_k)$ — and no account, position, book, or fund coordinate. In particular it writes nothing into any per-position accumulator: this is the $\varphi \equiv 0$ convention made operational, and it is why the funding accumulator is not a state coordinate of this model.

$$A' = A + \frac{P_{trade} - u_k}{u_k}\,\Delta t, \qquad T' = T + \Delta t \qquad (\Delta t > 0,\ u_k > 0); \qquad \text{all other coordinates unchanged} \tag{G.4}$$

Funding settlement

Fires at the end of each funding interval. The rate is the clamped, pro-rated time-weighted average premium plus the fixed interest term, with the total $T = 0$ branch returning zero ((F.3)); each open position's payment is $\Pi^f = \sigma\, q\, P_{oracle,k}\, f$ ((F.4)), struck at the oracle price rather than the mark, computed fresh from $(A, T)$ — settle-and-reset, never read from accrued per-position state. Each payment routes through the funding pool as a transfer of magnitude $|\Pi^f|$ with sign-selected direction ((S.6)): the account leg debits or credits $C_a$, the pool leg mirrors it in $C_{pool}$. The collateral debit is unguarded — no margin check precedes it, so settlement can push an account through its maintenance floor with no input motion (one of the three engine-internal channels scoped into the margin-monotonicity invariant). The interval pair resets atomically: $(A', T') = (0, 0)$. Touches: $C_a$ for every account with an open position, $C_{pool}$, $(A_k, T_k)$.

$$f = \begin{cases} 0 & T = 0 \\ \operatorname{clamp}\!\big((A/T + i)\cdot W/28800,\, -c,\, +c\big) & T > 0 \end{cases}; \qquad C_a' = C_a - \Pi^f_a,\ \ \Pi^f_a = \sigma_a\, q_a\, P_{oracle,k}\, f; \qquad C_{pool}' = C_{pool} + \textstyle\sum_a \Pi^f_a; \qquad (A', T') = (0, 0) \tag{G.5}$$

Liquidation cascade

Fires when an account's fresh-mark equity falls to its maintenance floor: the inclusive trigger $E \le \sum_i M_i$ ((L.4)) over (L.1), (L.2), (L.3). Collateral is apportioned — cross accounts split the shared pool loss-proportionally with the remainder fold conserving it exactly ((L.6), (L.7)); isolated positions use their stamped cushion ((L.5)). Close orders are sized ((L.11), (L.12)), guarded reduce-only ((L.13) — a negative share yields an oversized order that is rejected each scan, a stall not a flip), priced from the bankruptcy price ((L.8)) tick-aligned toward executability ((L.9), (L.10)), and executed through the same matching map as any order — their fills enter $W_k$. Settlement per market: $X_i = s_i + \Pi_{\mathrm{fill},i} + \Pi_{\mathrm{res},i} - g_i$ with realized fill PnL (L.15), mark-valued residual (L.16), and spread profit (L.14); bad debt is $D_i = \max(0, -X_i)$ ((L.17)). The liquidated account's collateral is defined explicitly: $C_a' = \sum_i (\max(X_i, 0) - \Lambda_i)$, where the penalty $\Lambda_i$ is the owed amount (S.4) capped at the retained collateral ((I.9)) — a debit whose fund-side destination is witnessed: (I.10) and (I.11) credit the same $\Lambda$ to $\Phi$ in one atomic no-mint pair (v0.0.9 expressions closing the formerly-open liquidation_penalty_sink finding). Fund sequencing is credit-before-absorb for BOTH credits (settled, code-verified 2026-07-12: apply_liquidation_penalty precedes fill accounting in execute_liquidation, per_market.rs:552-574, and the spread credit precedes absorb_bad_debt): $\Phi_1 = \Phi + \Lambda + g$ ((I.10), (I.7)), then absorption $\min(D, \Phi_1)$ ((I.1), (I.2)) with lockstep ledgers ((I.3), (I.8)). ADL arms through two nested predicates: the settle amount $D_{\mathrm{adl}} = \max(D - \Phi_1, 0) > 0$ ((I.4)) and, after absorption, the threshold $\Phi' \le \kappa$ ((I.5)). Settle-amount firing implies threshold firing ($D_{\mathrm{adl}} > 0$ forces $\Phi' = 0 \le \kappa$); the divergence is one-sided — e.g. $\Phi_1 = 12, D = 5, \kappa = 10$ gives $D_{\mathrm{adl}} = 0$ yet $\Phi' = 7 \le \kappa$: armed with nothing to settle. Whether ADL executes in that regime is the open finding adl_arming_condition_ambiguity. Counterparties rank by $\rho = \pi L$ ((L.18), (I.6)); the counterparty settlement map itself is unmodeled — a named gap (adl_settlement_unmodeled). One further seam is named rather than hidden: on a partial fill the settle map counts $\Pi_{\mathrm{res}}$ as cash in $X$ while the surviving remainder retains entry $P_e$ ((T.1) is untouched by reductions) — no expression re-marks the residual's entry, so the partial-fill case double-carries that PnL across layers (residual_entry_remark_unwitnessed). Touches: $s, P_e, B, W, C_a, \Phi, \Sigma_{\mathrm{abs}}, \Sigma_{\mathrm{rec}}, C_{fee}$. The fee treatment of liquidation close fills (whether the liquidatee is charged taker fees, and resting counterparties earn rebates, on cascade fills) is unwitnessed by any component expression; $C_{fee}$ is therefore excluded from this map's write set and the question is a named gap (liquidation_fill_fee_treatment).

$$\begin{aligned} &\text{fire: } E \le \textstyle\sum_i M_i; \qquad s_i = C\,\tfrac{\ell_i}{\mathcal{L}}\ (+\ \text{remainder fold}), \qquad X_i = s_i + \Pi_{\mathrm{fill},i} + \Pi_{\mathrm{res},i} - g_i, \qquad D = \textstyle\sum_i \max(0, -X_i) \\ &C_a' = \textstyle\sum_i \big( \max(X_i, 0) - \Lambda_i \big), \qquad \Lambda_i = \min\!\big(\Lambda_{\mathrm{owed},i},\ \max(X_i, 0)\big) \\ &\Phi_1 = \Phi + \Lambda + g, \qquad \Phi' = \max(\Phi_1 - D,\ 0), \qquad D_{\mathrm{adl}} = \max(D - \Phi_1,\ 0) \end{aligned} \tag{G.6}$$

Invariants of the engine

Aggregate funding zero-sum across matched open interest

$$\sum_{a} \Pi^{f}_{a} \;=\; f\, P_{oracle,k} \sum_{a} s_{a,k} \;=\; 0 \qquad\Longrightarrow\qquad C_{pool}' = C_{pool} \tag{G.7}$$

Within each market, a funding settlement transfers value between the sides but creates none: the payments (F.4) sum to zero over all accounts because open interest is matched ($\sum_a s_{a,k} = 0$), so the pool's net position across the settlement's transfers ((S.6)) is exactly zero. Honest scope: stated for a solvent payer set. When a payer's debit exceeds its own collateral, the insurance fund covers the shortfall so the receiving side is still paid in full — the fund is a source in that case, not a pure transfer between matched sides, so the account legs no longer cancel exactly and $C_{pool}' = C_{pool}$ does not hold for that window.

Why it holds: Position coordinates are written only by fill maps, and every fill adjusts taker and maker by the same $q^{\star}$ with opposite signs ((B.6), with reduces and flips per (T.3) and (T.5)) — so $\sum_a s_{a,k} = 0$ inductively from the empty market; deposits, withdrawals, cancels, and accrual never touch $s$, and liquidation closes execute through the same fill map. The payment is linear in signed size with the common factor $f\, P_{oracle,k}$ ((F.4)), so the account legs cancel exactly in decimal arithmetic, and each pool transfer carries exactly the account leg's magnitude with mirrored direction ((S.6)).

The one exception, named: the derivation above assumes every payer's debit lands in full, and one engine-internal channel breaks that — the capped-payer funding shortfall. A payer's debit is capped at its own collateral, and the insurance fund contributes the difference so the receiving side is paid in full. What becomes of the payer's uncovered remainder is a ratified decision that has not shipped: ADR-0003 accepts carrying it into pending_funding rather than forgiving it, and as of main that carry does not exist — RiskMutation::FundingSettled has no carried-remainder field, accrue_pending_funding is reached only from the FS-03 close-path flush in fills.rs, and the settlement path resets every touched position's funding_integral along with the rest of the window. So today a covered shortfall leaves no liability recorded anywhere, and one the fund cannot cover books an UncoveredSystemLoss and halts the market fail-closed (ENG-7114). Whenever that path fires, the fund is a source for the settlement rather than a matched counterparty: $\sum_a \Pi^f_a$ equals the covered shortfall instead of zero, and $C_{pool}' = C_{pool}$ fails by exactly that amount for the window. The equality above is therefore an invariant of the solvent-payer regime, not of every settlement — the same shape as the margin-monotonicity invariant's three engine-internal channels below.

No component expression in this corpus witnesses that path. The insurance-fund expressions (I.1)–(I.8) model the liquidation bad-debt waterfall only, and neither the payer-side cap, the fund's funding-side contribution, nor the shortfall's disposition appears in (F.4) or (S.6). So the exception is named here rather than composed, and the citation this clause should eventually carry is a gap rather than an omission (funding_capped_payer_unwitnessed).

Composes: (F.4) (F.3) (S.6) (B.6) (T.3) (T.5)

Collateral conservation through the liquidation cascade

$$\sum_i s_i = C, \qquad D = \min(D, \Phi_1) + \max(D - \Phi_1,\ 0), \qquad \Delta C_a\big|_{\Lambda} = -\Lambda = -\Delta\Phi\big|_{\Lambda}, \qquad \Phi = \Sigma_{\mathrm{rec}} - \Sigma_{\mathrm{abs}} \tag{G.8}$$

Through a fully-filled cascade, equity is apportioned and transferred, never created: the cross pool splits into shares that sum back to it exactly ((L.6), (L.7)); every unit of bad debt (L.17) is covered exactly once, split between fund absorption (I.1) and the ADL settle amount (I.4) at the post-spread-credit balance $\Phi_1$; and the penalty is a no-mint transfer — the account debit and the fund credit are the same capped $\Lambda$ ((I.9), (I.10)). Honest scope: stated for fully-filled liquidations ($Q_f = q$, $\Pi_{\mathrm{res}} = 0$); the partial-fill case is unreconciled by the residual entry-remark gap named in the composition, and the ADL leg conserves only up to the unmodeled counterparty settlement.

Why it holds: The remainder fold adds $C - \sum_j s_j$ to exactly one share, restoring $\sum_i s_i = C$ identically regardless of rounding. The $\min/\max$ pair is a complementary split of $D$ at $\Phi_1$, and credit-before-absorb makes $\Phi_1 = \Phi + g$ the balance absorption actually reads ((I.7) commits before (I.2)). The penalty legs are one atomic mutation carrying a single $\Lambda$ capped at available collateral, so neither side can exceed the other. Fund closure $\Phi = \Sigma_{\mathrm{rec}} - \Sigma_{\mathrm{abs}}$ holds because every fund update moves the balance and exactly one ledger by the same amount.

Composes: (L.6) (L.7) (L.17) (I.1) (I.4) (I.7) (I.2) (I.9) (I.10)

Margin monotonicity (maintenance strictly inside initial)

$$r_m < r_i \;\Longrightarrow\; \big\{\, S : E \le M_{maint}^{pf} \,\big\} \subsetneq \big\{\, S : E \le M_{init}^{pf} \,\big\} \tag{G.9}$$

For every admissible parameter set, maintenance margin is strictly below initial margin position-wise and in the portfolio sums ((M.4) vs (M.2), (M.10) vs (M.9)), so the liquidation region (L.4) is strictly contained in the admission-blocked region and a just-admitted order sits strictly above its maintenance floor at the admission mark. Honest behavioral scope: this is a geometric buffer, not a temporal guarantee — three engine-internal channels can close the gap with no input motion: the unguarded funding-settlement collateral debit ((F.4)), the taker-fee debit that admission headroom does not charge ((S.2) vs (M.14)), and trade-leg mark motion from the engine's own fills entering the blend (findings: unguarded funding debit, admission fee gap, trade-leg self-influence).

Why it holds: Both requirements are the product $q \cdot P \cdot r$ differing only in the rate, and $r_m < r_i$ is validated at parameter parse, so the per-position inequality is strict and survives summation over the identical position set. The effective rate only widens the gap ($r_{eff} \ge r_i$, (M.1)). No engine map weakens the inclusion — the three gap-closing channels move $E$, not the region ordering — so the invariant is preserved by every event while the behavioral contract is scoped to the cited channels.

Composes: (M.4) (M.2) (M.10) (M.9) (M.1) (M.14) (L.4) (S.2) (F.4)

Bounded funding transfer per interval

$$\lvert \Pi^{f}_{a} \rvert \;\le\; c\, q_a\, P_{oracle,k} \qquad \text{per position, per funding interval} \tag{G.10}$$

No funding settlement can move more than the cap fraction of a position's oracle notional in one interval: the rate is clamped to $[-c, +c]$ on both of its branches ((F.3)), and the payment is linear in the rate ((F.4)), so each account's per-position debit or credit is bounded by $c\, q\, P_{oracle,k}$ and the pool's gross throughput by $c\, P_{oracle,k} \sum_a q_a$.

Why it holds: The rate map has exactly two return paths: $T = 0$ returns zero, and $T > 0$ applies the clamp directly, so $|f| \le c$ in every reachable state. The payment map multiplies $f$ by $\sigma\, q\, P_{oracle,k}$ with no other rate dependence, and the settlement transfer carries exactly $|\Pi^f|$ ((S.6)) — no map between the clamp and the ledger can amplify the amount.

Composes: (F.3) (F.4) (S.6)

Fee closure across the fill path

$$\Delta C_{fee} \;=\; F - R \;=\; V, \qquad \Delta C_{fee} + \textstyle\sum_a \Delta C_a \big|_{\text{fees}} = 0 \tag{G.11}$$

Across any batch of fills, the fee flows between accounts and the Exchange fee account close exactly: every taker fee debited from an account is either paid out as a maker rebate or retained as revenue ((S.2), (S.3), (S.5)), the closure is preserved linearly under batch merge ((S.7)), and liquidation penalties never contaminate it — they route to the fund, never to $C_{fee}$ ((S.4)).

Why it holds: Both accumulators are built fill-by-fill from the identical truncated amounts placed into the transfer ledger, and revenue is computed once as their difference — there is no independent revenue path to drift. The account-side legs are the same $F_t$ and $F_m$ the fill map applies to $C_a$, so the system-wide fee sum telescopes to zero. Merge only adds accumulators and concatenates transfers, so closure survives batching; the penalty push site targets the insurance fund and never enters $F$, $R$, or $V$.

Composes: (S.2) (S.3) (S.5) (S.7) (S.4) (S.1)

Structure of the flow

Geometry of the healthy region. For a fixed position set, equity is affine in each mark with slope the net signed size, $\partial E / \partial m_k = \sum_i s_{i,k}$ ((M.8)), while total maintenance is piecewise-linear with slope $\sum_i q_{i,k}\, r_{m,k}$ ((M.10)) — so the healthy region $\{S : E > \sum_i M_i\}$ is, in the mark coordinate of a single-market account, a half-line whose boundary is exactly the displayed liquidation price ((T.8)), with the bankruptcy price ((T.9)) strictly beyond it for any under-collateralized position. Margin requirements scale linearly in size ((M.2)), the effective rate never undercuts the market rate ((M.1)), added exposure is non-negative so admission never pre-credits a reduce ((M.11)), and the slippage cap is monotone in its band ((B.10)).

Fixed points under constant input. Hold $u$ constant with an empty or agreeing trade window (so $m_k = P_{oracle,k}$) and suppress user events. Then the premium vanishes ((F.1)), accrual adds $0 \cdot \Delta t$ to $A$ while only the clock $T$ advances — that half of the claim still holds — but settlement no longer computes $f = 0$: the fixed interest term makes the resting rate $f = i \cdot W/28800$, so settlement still moves a small amount through the pool even at an agreeing mark ((F.3), (S.6)). The trigger stays silent on every healthy account and the position, book, and fund coordinates $(s, P_e, B, \Phi, C_{fee})$ are fixed, but $C_a$, $C_{pool}$, and the funding pair $(A, T)$ still cycle through nonzero settlements. Healthy states at an agreeing mark are thus not full equilibria of the autonomous engine — only the non-funding coordinates are fixed. The interesting non-equilibria are one-sided: once $E \le \sum M_i$, the cascade fires and the account's position coordinates contract monotonically toward flat; and because the trigger is inclusive ((L.4)), the boundary itself belongs to the liquidation region, not the healthy one.

Appendix — the complete formal system

This appendix is rendered mechanically from the state-space classification (models/state-space.json) — derived, not written. Its completeness claim is checked: the closure gate (ci/closure.py) verifies on every run that every corpus expression is classified, every state coordinate is written by an event and read somewhere, and every event map cites only defined coordinates. The state space factors into 16 coordinates (global fund and cash books; per-market book, trade window, premium accumulator, oracle anchor and re-anchor pending block; per-account collateral and reserved margin; per-position size/entry/direction and funding accumulator), 9 inputs, 20 parameters, and 54 derived observables, with all 133 corpus variables and 84 expressions classified totally across 10 events. Alphabet completion added adl_execution, oracle_reanchor_step, oracle_reanchor_commit — including adl_execution emitted with empty writes so the closure gate keeps flagging the unmodeled ADL counterparty settlement map. Deliberately uncited update maps (deposit/withdrawal transfer, cancel removal and reservation release, anchor assignments, trade-window push, funding resets) remain named gaps rather than inventions.

A.1 The state vector

global

Coordinate	Symbol	Units	Owner	Description
funding_pool	$C_{pool}$	USDX	settlement	The funding pool book through which every funding transfer routes; nets to zero exactly across the matched open interest of one settlement. No component variable persists it — declared by the global composition; its only witnessed update is the transfer-magnitude map.
exchange_fee_account	$C_{fee}$	USDX	settlement	The Exchange fee account, carried with its settlement-record accumulators (total fees F, total rebates R, net revenue V = F - R, and their batch-merge operands): credited taker fees, debited maker rebates; liquidation penalties never enter it.

per-market

Coordinate	Symbol	Units	Owner	Description
order_book	$B_k$	multiset of orders (side, limit price, remaining quantity, fill progress)	order-book	Resting-order multiset of the market with its id index in exact agreement; per-order fill progress (filled_qty) lives inside this composite; uncrossed (P_b < P_a) in every reachable state.
accumulated_premium	$A_k$	dimensionless-seconds	funding-rate	Time-weighted premium accumulator of the current funding interval, written only by the sample-contribution map and reset to zero atomically at settlement.
interval_clock	$T_k$	seconds	funding-rate	Elapsed accumulated time of the current funding interval, advanced with each sample and reset with A_k at settlement; the T = 0 branch of the rate keeps the map total. (The component text calls it derived; the composed system persists it as the interval's clock.)
trade_window	$W_k$	five (price, size) pairs	oracle	The last five executed fills of the market, written by the fill map (including liquidation close fills) and read by the volume-weighted median trade reference — the engine-owned leg of the mark blend.
insurance_fund_balance	$\Phi_k$	USDX	insurance-fund	Per-market insurance fund balance: credited by spread profit and penalties, debited by bad-debt absorption; Phi >= 0 with exact depletion, and Phi = Sigma_rec - Sigma_abs against its lifetime ledgers.
insurance_fund_total_absorbed	$\Sigma_{\mathrm{abs}}$	USDX	insurance-fund	Lifetime bad-debt absorption ledger of the fund; monotonically non-decreasing, incremented in lockstep with each absorption.
insurance_fund_total_received	$\Sigma_{\mathrm{rec}}$	USDX	insurance-fund	Lifetime receipts ledger of the fund (initial balance plus spread profits and penalty credits); monotonically non-decreasing, moving in lockstep with balance credits. The initial-balance credit has no event in the alphabet (initialization, not dynamics).
oracle_anchor	$P_{oracle,k}$	USDX per unit of asset	oracle	The trusted anchor price of the market — the engine's exogenous input process state; moved only by the guarded fresh-accept and re-anchor-commit branches of the oracle map, never by any engine event.
anchor_timestamp	$t_{last,k}$	milliseconds	oracle	Timestamp of the last trusted anchor update, read by the staleness predicate; frozen together with the anchor while a re-anchor is pending.
oracle_guard_state	$\Omega_k$	prints and milliseconds	oracle	The input process's defense bookkeeping: the ten-print history (whose oldest element the path check reads) and the pending re-anchor block (candidate price, pending print count, confirmation counter, opening timestamp); touched only by the oracle map.

per-account

Coordinate	Symbol	Units	Owner	Description
account_collateral	$C_a$	USDX	margin-math	Realized USDX collateral of an account: the cash leg of deposits/withdrawals, realized PnL, fees, funding, and liquidation settlement; sign-unrestricted because engine-internal debits are unguarded.
reserved_margin	$M_{resv}$	USDX	margin-math	Initial margin reserved by resting/in-flight orders, carried with the open-reservation count n_{resv}; written at admission, released on fill or cancel, read by the cross admission gate and the withdrawal guard.

per-position

Coordinate	Symbol	Units	Owner	Description
signed_position_size	$s_{a,k}$	base units, signed	position-tracker	Signed position size (sigma = sign(s), q = |s| > 0 for a stored position, |s| a lot multiple); written only by the fill map (open, increase, reduce, flip) and the cascade's close fills.
entry_price	$P_{e,a,k}$	USDX per base unit	position-tracker	Volume-weighted entry price maintained exclusively by the VWAP blend: same-side fills blend, reductions leave it untouched, flips re-seed it at the fill price.

A.2 Inputs and parameters

Inputs are exogenous — they arrive from outside the state; parameters are constants of market or system configuration.

Inputs

Input	Symbol	Units	Description
oracle_print_price	$P_{new}$	USDX per unit of asset	An incoming external oracle print being validated against the anchor or the pending re-anchor candidate.
wall_clock_time	$t_{now}$	milliseconds	Feed-supplied timestamp of the incoming print or staleness evaluation, in Unix milliseconds.
time_delta	$\Delta t$	seconds	Exogenous elapsed time since the previous funding premium sample; non-advancing samples are ignored.
order_quantity	$q$	base units	Quantity of an arriving order; must be a lot multiple to pass admission.
order_limit_price	$P_{lim}$	USDX per base unit	Limit price of an arriving limit order; must be strictly positive, tick-aligned, and inside the mark collar.
order_signed_size	$o$	base units, signed	Signed size of an arriving order (buy positive, sell negative), read by the added-exposure computation.
max_slippage_bps	$\beta$	basis points	Taker-supplied per-order slippage cap on a market order; absent means no cap.
preview_requested_qty	$q_{req}$	base units	Quantity requested by a hypothetical market order in the read-only VWAP preview; undefined for non-positive requests.
external_transfer_amount	$x$	USDX	External USDX amount of a deposit or withdrawal; not a corpus variable — carried by the composition's deposit/withdrawal event.

Parameters

Parameter	Symbol	Units	Scope	Description
funding_rate_cap	$c$	fraction per funding interval	per-market	Symmetric cap on the funding rate. The crypto perps use 0.001 (0.1%); the FX, commodity, and index perps (seven markets, including NDQ) are configured at 0.0005. Which of the seven are actually deployed changes with the venue's rollout state — see Market Specifications for the live per-market set rather than a fixed snapshot here.
adl_threshold	$\kappa$	USDX	per-market	ADL trigger threshold on the fund balance; default zero arms ADL only at full depletion.
maintenance_margin_rate	$r_m$	dimensionless ratio	per-market	Market maintenance margin rate; strictly less than the initial margin rate.
initial_margin_rate	$r_i$	dimensionless ratio	per-market	Market initial margin rate, equal to one over the market's maximum leverage.
account_leverage	$L$	multiplier	per-account	Account-selected leverage per market (integer >= 1, validated before storage); user configuration with no state-mutating expression in the corpus, hence a parameter, not a coordinate.
tick_size	$\delta$	USDX per base unit	per-market	Minimum price increment; non-positive tick disables alignment.
lot_size	$\ell$	base units	per-market	Market lot size; order and position sizes are integer multiples of it; zero disables the alignment check.
taker_fee_bps	$b_t$	basis points	per-market	Taker fee rate charged on fill notional.
maker_rebate_bps	$b_m$	basis points	per-market	Maker rebate rate, stored negative by convention; applied by absolute value.
liquidation_penalty_bps	$b_{liq}$	basis points	per-market	Penalty rate applied to the notional of liquidation fills and routed to the insurance fund.
price_band_bps	$b_{band}$	basis points	per-market	Maximum admissible relative deviation of a limit price from the mark (the admission collar).
oracle_deviation_threshold	$\theta$	dimensionless fraction	per-market	Single-step deviation threshold for accepting an oracle print against the anchor.
oracle_history_size	$N_h$	prints	global	Fixed size of the rolling price-update window used by the path-manipulation check (HISTORY_SIZE = 10).
oracle_staleness_seconds	$\tau_s$	seconds	per-market	Staleness threshold: the anchor is stale strictly beyond this many seconds since the last trusted update.
reanchor_max_deviation	$\theta_r$	dimensionless fraction	per-market	Per-step consistency bound for re-anchor confirmations against the running candidate.
escalation_max_deviation	$\theta_e$	dimensionless fraction	per-market	Widened per-step bound applied once the escalation trigger has fired.
required_confirmations	$k$	prints	per-market	Consecutive mutually-consistent prints required to promote a re-anchor; floored at 2 effectively.
escalation_prints	$N_e$	prints	per-market	Print-count arm of the re-anchor escalation trigger.
escalation_seconds	$\tau_e$	seconds	per-market	Wall-clock arm of the re-anchor escalation trigger, measured from the opening of the pending sequence.
oracle_mark_weight	$w$	dimensionless fraction	per-market	Oracle weight in the mark blend; unit-interval, default 0.95 (oracle-dominant).

A.3 Derived observables

Pure functions of state, inputs, and parameters — recomputed, never persisted.

Quantity	Symbol	Units	Defined by	Description
mark_price	$m_k$	USDX per base unit	(O.8)	Convex blend of the trusted anchor and the volume-weighted trade reference; equals the anchor when no trade reference exists. Recomputed on demand, never persisted.
trade_ref	$P_{trade}$	USDX per base unit	(O.7)	Volume-weighted median price of the five-trade window; falls back to the last trade price when the window is short.
premium_index	$p$	dimensionless	(F.1)	Fractional deviation of the perp reference (NOT the mark) from the anchor at a sample; skipped when the anchor is non-positive.
funding_rate	$f$	fraction per interval	(F.3)	Clamped, pro-rated time-weighted average premium plus the fixed interest term — $\text{clamp}((A/T + i) \cdot W/28800, -c, +c)$ — recomputed fresh from (A, T) at settlement with the T = 0 branch returning zero.
funding_payment	$\Pi^f$	USDX	(F.4)	Signed per-position funding payment sigma q P_oracle f, struck at the oracle price rather than the mark; simultaneously the settlement event's collateral update delta.
unrealized_pnl	$\mathrm{uPnL}$	USDX	(T.2)	Per-position mark-to-market PnL; the account total is its sum over open positions (coherence-merged with liquidation-engine.fresh_unrealized_pnl).
account_equity	$E$	USDX	(M.8)	Collateral plus mark-to-market PnL (net of funding integrals in the portfolio form); coherence-merged across margin-math.equity, margin-math.portfolio_equity, and liquidation-engine.account_equity.
maintenance_margin	$M_m$	USDX	(M.4)	Maintenance margin at the mark; coherence-merged with the portfolio and liquidation-engine instances.
initial_margin	$M_i$	USDX	(M.2)	Initial margin at the mark (stamped allocated margin where set); coherence-merged with the portfolio instance.
available_margin	$M_{avail}$	USDX	(M.7)	Equity minus total initial margin held; can be negative; gates order admission, not withdrawal.
added_exposure	$\Delta q$	base units	(M.11)	Magnitude of newly-opened exposure an order adds: growth on increase, zero on reduce/close, the whole new side on a flip.
admission_added_margin	$M_{add}$	USDX	(M.12)	Initial margin charged on added exposure at the mark and effective rate; also the amount written into the reservation at admission.
isolated_margin_cushion	$C_{iso}$	USDX	(L.5)	Collateral backing an isolated position: the margin allocated at fill time if recorded, otherwise the open-time initial margin at market rate; the trigger ((L.4)) and the liquidation pricing both use this single value.
bankruptcy_price	$p_b$	USDX per base unit	(L.8)	Price at which the position's backing collateral is exactly exhausted; coherence-merged with position-tracker.bankruptcy_price; may be zero or negative before alignment.
aligned_bankruptcy_price	$\tilde{p}_b$	USDX per base unit	(L.9)	Tick-aligned close-order limit: floor for sells (liquidation-engine.aligned_price_sell), ceil for buys (liquidation-engine.aligned_price_buy), clamped to one tick.
liquidation_price	$p_{liq}$	USDX per base unit	(T.8)	Analytically-solved mark at which equity meets the maintenance requirement; display/analysis, neither moves state nor gates events.
cross_collateral_share	$s_i$	USDX	(L.6)	Loss-proportional share of the shared cross pool per market, with the remainder folded into the largest-loss position's share.
collateral_share_sum	$S$	USDX	``	Sum of the proportional shares before the remainder fold; prose-defined only — no corpus expression id (read by the remainder fold).
position_loss	$\ell_i$	USDX	``	max(0, -uPnL_i) per market with entry-price fallback; defined only in variable prose, no corpus expression id.
total_loss	$\mathcal{L}$	USDX	``	Sum of position losses across the positions liquidated together; prose-defined only.
safe_size	$q_{safe}$	base units	(L.11)	Largest lot-multiple size whose 1.5x-padded initial margin the collateral share covers.
liquidation_qty	$q_{liq}$	base units	(L.12)	Close-order quantity: full size in Full mode or degenerate cases, else reduction to safe size.
fill_quantity	$q^{\star}$	base units	(B.6)	Quantity of a single fill: min of taker and front-maker remainders; coherence-merged with settlement.size and position-tracker.fill_quantity.
fill_price	$P^{\star}$	USDX per base unit	(B.7)	Price of a single fill — always the maker's limit price; coherence-merged with settlement.price and position-tracker/liquidation-engine fill prices.
closed_quantity	$q_c$	base units	(T.3)	Portion of an opposing fill that closes existing size: min(size, fill quantity).
total_filled	$Q_f$	base units	``	Sum of the liquidation close order's fill quantities; within-event accumulation, prose-defined only.
spread_profit	$g$	USDX	(L.14)	Positive part of fills' price improvement over the aligned bankruptcy price, summed over fills; credited to the fund.
realized_fill_pnl	$\Pi_{fill}$	USDX	(L.15)	Signed realized PnL of liquidation fills, each at its own fill price; a component of the cascade's per-market settlement X_i.
residual_unfilled_pnl	$\Pi_{res}$	USDX	(L.16)	Mark-valued PnL of the unfilled remainder of the close order; zero on complete fill.
bad_debt	$D$	USDX	(L.17)	Non-negative shortfall after fills-aware settlement against the collateral share; drawn from the fund, then ADL.
absorbed_amount	$D_{abs}$	USDX	(I.1)	min(bad debt, fund balance): the delta by which the fund and its absorption ledger move.
adl_settle_amount	$D_{adl}$	USDX	(I.4)	Shortfall handed to ADL after the fund is drained; an instruction is emitted only when strictly positive.
adl_priority_score	$\rho$	dimensionless	(L.18)	ADL ranking score pi * L, descending with deterministic account-id tie-break; coherence-merged with the insurance-fund instance.
adl_pnl_percent	$\pi$	fraction	``	ADL candidate's unrealized PnL as a fraction of position value; no corpus expression defines it — a gap for the closure gate.
liquidation_penalty_owed	$\Lambda_{owed}$	USDX	(S.4)	Penalty owed on filled liquidation notional at the market's penalty rate.
penalty_charged	$\Lambda$	USDX	(I.9)	Penalty actually debited/credited: the owed amount capped at available collateral, so the pair cannot mint USDX.
fill_notional	$V^{\star}$	USDX	(S.1)	Notional of a single fill, size times price, exact decimal.
net_exchange_revenue	$V$	USDX	(S.5)	Settlement-record closure: total taker fees minus total maker rebates.
margin_ratio	$\rho_M$	dimensionless	(M.6)	Equity over total notional; undefined at zero notional; diagnostic — gates nothing in the corpus.
max_position_size	$q_{max}$	base units	(M.15)	Largest lot-aligned position openable with given collateral at the market rate; sizing/display analysis.
withdrawable_collateral	$W_{max}$	USDX	(M.16)	Full realized collateral for a flat, unreserved account, zero otherwise; the withdrawal guard's cap.
best_bid	$P_b$	USDX per base unit	``	Highest resting bid — a structural readout of the order_book coordinate; no corpus expression id.
best_ask	$P_a$	USDX per base unit	``	Lowest resting ask — a structural readout of the order_book coordinate; no corpus expression id.
mid_price	$P_{mid}$	USDX per base unit	(B.4)	Midpoint of best bid and ask, snapshotted once at market-order submission for the slippage cap; undefined when either side is empty.
slippage_span	$\Delta_{slip}$	USDX per base unit	(B.9)	Half-width of the admissible VWAP band anchored at the mid-price snapshot.
available_qty	$Q_{avail}$	base units	``	Pre-match opposing liquidity at prices satisfying the taker's limit; within-event readout of the book, prose-defined only.
taker_remaining	$q_t$	base units	``	Taker's unfilled remainder during the matching walk; within-event intermediate, prose-defined only.
running_notional	$V_k$	USDX	``	Cumulative notional of fills accepted so far in a market-order walk; within-event accumulator, prose-defined only.
running_filled	$Q_k$	base units	``	Cumulative quantity of fills accepted so far in a market-order walk; within-event accumulator, prose-defined only.
walk_notional	$V$	USDX	``	Total notional of a hypothetical price-time-priority walk for the VWAP preview; prose-defined only.
vwap_estimate	$\overline{P}$	USDX per base unit	(B.11)	Read-only market-order VWAP preview; undefined when liquidity cannot cover the request.
funding_integral	$\varphi$	USDX	``	Per-position accumulated funding read by portfolio equity; identically zero under the composed settle-and-reset convention (phi = 0) — no accrual map exists in the corpus, by design.
total_notional	$N$	USDX	``	Sum of size times mark over open positions; prose-defined only, the margin ratio's denominator.
open_positions	$n_{pos}$	count	``	Count of the account's open positions — a structural readout of the position coordinates; no corpus expression id.

A.4 The transition matrix

Guards

Event	Guard	Reads
deposit_withdrawal	deposit: x > 0 unguarded; withdrawal: 0 < x \le W_{max} = C_a , \mathbb{1}[n_{pos} = 0 \wedge n_{resv} = 0] (margin-math.withdrawable_collateral)	account_collateral, withdrawable_collateral, open_positions, reserved_margin
order_submission_fill	admission conjunction, nothing mutated on rejection: lot residue = 0 (order-book.lot_alignment) \wedge tick residue = 0 \wedge P_{lim} > 0 (order-book.tick_alignment) \wedge band deviation \le b_{band} (order-book.price_band) \wedge FOK availability (order-book.fok_availability) \wedge margin headroom \ge 0 (isolated: margin-math.order_margin_headroom; cross: margin-math.cross_admission_headroom); each market-order fill additionally gated by the running-VWAP band (order-book.running_vwap)	account_collateral, reserved_margin, signed_position_size, entry_price, order_book, trade_window, exchange_fee_account, mark_price, account_equity, available_margin, initial_margin, added_exposure, admission_added_margin, best_bid, best_ask, mid_price, slippage_span, available_qty, taker_remaining, running_notional, running_filled, fill_quantity, fill_price, closed_quantity
order_cancel_expiry	user cancel \vee IOC/FOK/market-remainder expiry \vee post-only cross rejection \vee slippage-cap breach (order-book.running_vwap strict breach) \vee reduce-only rejection q_{liq} > q (liquidation-engine.reduce_only_guard fails) \vee STP full reduction (order-book.stp_decrement)	order_book, reserved_margin, mid_price, slippage_span, liquidation_qty
funding_accrual	\Delta t > 0 \wedge u_k > 0 (non-advancing or non-positive-anchor samples pass state through unchanged)	accumulated_premium, interval_clock, oracle_anchor, mark_price, premium_index, trade_window
funding_settlement	funding interval boundary reached (schedule is configuration; the corpus contributes the T = 0 totality branch of funding-rate.funding_rate)	accumulated_premium, interval_clock, funding_rate, funding_payment, mark_price, signed_position_size, account_collateral, funding_pool
liquidation_cascade	E \le \sum_i M_i at the fresh mark, inclusive (liquidation-engine.liquidation_trigger)	account_collateral, signed_position_size, entry_price, order_book, trade_window, insurance_fund_balance, insurance_fund_total_absorbed, insurance_fund_total_received, exchange_fee_account, mark_price, unrealized_pnl, account_equity, maintenance_margin, position_loss, total_loss, cross_collateral_share, collateral_share_sum, bankruptcy_price, aligned_bankruptcy_price, safe_size, liquidation_qty, fill_price, fill_quantity, total_filled, spread_profit, realized_fill_pnl, residual_unfilled_pnl, bad_debt, absorbed_amount, liquidation_penalty_owed, penalty_charged, adl_settle_amount
adl_execution	D_{adl} = \max(D - \Phi_1, 0) > 0 (insurance-fund.adl_settle_amount) nested with \Phi' \le \kappa (insurance-fund.adl_trigger); the one-sided divergence (armed with nothing to settle) is the open finding adl_arming_condition_ambiguity	adl_settle_amount, insurance_fund_balance, adl_priority_score, adl_pnl_percent, signed_position_size, entry_price, account_collateral
oracle_print_accept	\neg stale (oracle.is_stale = 0) \wedge \Delta_{step} \le \theta (oracle.single_step_deviation) \wedge (|H| = N_h \Rightarrow \Delta_{path} \le \theta\sqrt{N_h}) (oracle.path_deviation vs oracle.path_threshold)	oracle_anchor, anchor_timestamp, oracle_guard_state
oracle_reanchor_step	stale (oracle.is_stale = 1) \wedge print arrives \wedge confirmations after this step < \max(k, 2); active per-step bound is \theta_r, widened to \theta_e once the escalation trigger fires (oracle.reanchor_step_deviation, oracle.escalation_trigger)	oracle_guard_state, oracle_anchor, anchor_timestamp
oracle_reanchor_commit	stale \wedge consecutive mutually-consistent confirmations \ge \max(k, 2) (oracle.reanchor_step_deviation within the active bound on the promoting print)	oracle_guard_state, anchor_timestamp

Writes — rows are state coordinates, columns are events; a cell cites the component equation defining that update; · means provably untouched.

Coordinate	deposit_withdrawal	order_submission_fill	order_cancel_expiry	funding_accrual	funding_settlement	liquidation_cascade	adl_execution	oracle_print_accept	oracle_reanchor_step	oracle_reanchor_commit
account_collateral (per-account)	✓	(T.4) (S.2) (S.3)	·	·	(F.4)	(L.15) (L.16) (I.9)	·	·	·	·
reserved_margin (per-account)	·	(M.12)	✓	·	·	·	·	·	·	·
signed_position_size (per-position)	·	(T.3) (T.5) ✓	·	·	·	(T.3)	·	·	·	·
entry_price (per-position)	·	(T.1)	·	·	·	(T.1)	·	·	·	·
order_book (per-market)	·	(B.6) (B.8)	✓	·	·	(B.6)	·	·	·	·
accumulated_premium (per-market)	·	·	·	(F.2)	✓	·	·	·	·	·
interval_clock (per-market)	·	·	·	✓	✓	·	·	·	·	·
trade_window (per-market)	·	(B.7)	·	·	·	(B.7)	·	·	·	·
insurance_fund_balance (per-market)	·	·	·	·	·	(I.7) (I.2) (I.10)	·	·	·	·
insurance_fund_total_absorbed (per-market)	·	·	·	·	·	(I.3)	·	·	·	·
insurance_fund_total_received (per-market)	·	·	·	·	·	(I.8) (I.11)	·	·	·	·
funding_pool (global)	·	·	·	·	(S.6)	·	·	·	·	·
exchange_fee_account (global)	·	(S.2) (S.3) (S.7)	·	·	·	(S.2)	·	·	·	·
oracle_anchor (per-market)	·	·	·	·	·	·	·	✓	·	✓
anchor_timestamp (per-market)	·	·	·	·	·	·	·	✓	·	✓
oracle_guard_state (per-market)	·	·	·	·	·	·	·	✓	✓	✓

A.5 The invariant registry

Every invariant the corpus states — component and global — with its scope and how it is verified.

Stale relative to the model above. Rows 46 and 49 below are machine-rendered from an earlier revision of the state-space model (models/state-space.json) and still state the pre-ENG-7077 forms of G.7 and G.10 — f · m_k and c · q_a · m_k — rather than the P_{oracle,k} forms already fixed in the Event dynamics and Invariants sections above. Regenerating this appendix requires the Modeling & Security pod's pipeline to re-derive it from the current Rust source, which is out of scope for this doc-alignment pass; flagging here rather than hand-editing generated output or silently leaving it uncaveated.

#	Invariant	Scope	Where	Verification
1	The funding rate always lies in the cap band: $f \in [-c, +c]$ for every reachable state ((F.3)).	component	Funding	component Judge
2	(F.3) is total: it is defined for every state, including the empty interval, where $T = 0$ yields $f = 0$.	component	Funding	component Judge
3	Funding is zero-sum between matched sides: for equal size $q$, the long and short payments cancel exactly, $\Pi^{f}_{long} + \Pi^{f}_{short} = 0$ ((F.4)).	component	Funding	component Judge
4	When the clamp is inactive, the sign of the rate matches the sign of the average premium: a perpetual trading persistently rich yields $f > 0$ and a perpetual trading cheap yields $f < 0$ ((F.3)).	component	Funding	component Judge
5	The accumulator $A$ is a well-formed time-weighted sum: only samples with strictly advancing time and a strictly positive oracle price contribute ((F.2)).	component	Funding	component Judge
6	Non-negativity with exact depletion: $\Phi \ge 0$ after every operation, and the balance is exactly zero — no dust, no overdraw — whenever an ADL instruction is emitted ((I.2)).	component	The Insurance Fund	component Judge
7	Accounting closure: $\Phi = \Sigma_{\mathrm{rec}} - \Sigma_{\mathrm{abs}}$ at all times — including through the penalty receipt path, which required no correction on the fund side.	component	The Insurance Fund	component Judge
8	Bad-debt conservation: $D = \min(D, \Phi) + \max(D - \Phi, 0)$ — every liquidation's debt is covered exactly once, split between fund absorption ((I.1)) and ADL settlement ((I.4)).	component	The Insurance Fund	component Judge
9	Monotone ledgers: $\Sigma_{\mathrm{abs}}$ and $\Sigma_{\mathrm{rec}}$ never decrease, and liquidation processing leaves $\Sigma_{\mathrm{rec}}$ untouched — ADL counterparty settlements live entirely outside the fund's books.	component	The Insurance Fund	component Judge
10	Credit-before-absorb sequencing: for a single liquidation carrying both spread profit $g > 0$ and bad debt $D > 0$, the spread credit lands first, so absorption evaluates against the post-credit balance — the fund absorbs $\min(D, \Phi + g)$ and ADL settles $\max(D - \Phi - g, 0)$ ((I.7), (I.1), (I.4)).	component	The Insurance Fund	component Judge
11	No-mint penalty pair: the liquidatee debit and the fund credit are the same capped amount $\Lambda = \min(\Lambda_{\mathrm{owed}}, \max(C, 0))$ ((I.9)) — the penalty transfers USDX, it never creates it.	component	The Insurance Fund	component Judge
12	For a long position with positive backing collateral, the bankruptcy price (L.8) lies strictly below the entry price and at or below the liquidation-trigger price; for a short, strictly above and at or above, respectively.	component	Liquidation	component Judge
13	The trigger threshold is inclusive: an account with $E = \sum_i M_i$ is liquidated ((L.4)).	component	Liquidation	component Judge
14	Cross-collateral shares conserve the pool exactly: after (L.7), $\sum_i s_i = C$, so aggregate bad debt over a fully-unfilled liquidation equals $\mathcal{L} - C$, the true portfolio shortfall.	component	Liquidation	component Judge
15	Tick alignment concedes at most one tick and never produces a non-positive limit: for $\delta > 0$, $\|P - P^{\downarrow}\| < \delta$ and $P^{\downarrow} \ge \delta$ (mirrored for (L.10)); for $\delta \le 0$ the price passes through unchanged.	component	Liquidation	component Judge
16	In Partial mode, $q_{\text{liq}} \in (0, q]$ holds if and only if the collateral share backing the position is non-negative. When $C < 0$, $q_{\text{safe}} < 0$ and (L.12) yields $q_{\text{liq}} = q - q_{\text{safe}} > q$ — an oversized close that would flip the position if executed (finding liquidation_close_order_exceeds_position_size, v0.0.9 audit, high).	component	Liquidation	component Judge
17	A non-positive or missing mark never fabricates losses or prices an order: the trigger and the pool split evaluate such markets at entry (zero PnL contribution, (L.1)), and no liquidation order is generated for them.	component	Liquidation	component Judge
18	A fully-filled liquidation whose every fill prints at or above the raw bankruptcy price produces at most the sub-tick alignment concession $q\,\delta$ of bad debt in (L.17) — exactly zero when the bankruptcy price is already tick-aligned.	component	Liquidation	component Judge
19	Maintenance never exceeds initial margin: for the same $(q, P)$, (M.4) $\leq$ (M.2), per position and in the portfolio sums.	component	Margining	component Judge
20	The effective rate never undercuts the market: $r_{eff} \geq r_i$ for every admissible leverage, so a selected leverage only ever reserves more margin ((M.1)).	component	Margining	component Judge
21	Added exposure is non-negative: (M.11) satisfies $\Delta q \geq 0$ for all $(s_0, o)$, so the admission charge (M.12) can only hold the portfolio requirement flat or raise it — a reduce is never pre-credited margin.	component	Margining	component Judge
22	Required margin never rounds down: the computed (M.2) and (M.4) always satisfy $M \geq q \cdot P \cdot r$ exactly.	component	Margining	component Judge
23	For $C \geq 0$, (M.15) returns a non-negative integer multiple of $\ell$ with $q_{max} \cdot P \cdot r_i \leq C$; the invariant is scoped to non-negative collateral.	component	Margining	component Judge
24	Withdrawals move only realized collateral from flat accounts: an account with any open position or outstanding reservation withdraws nothing, and a flat account withdraws at most $C$ ((M.16)); unrealized PnL is never withdrawable.	component	Margining	component Judge
25	Concurrent orders cannot double-spend headroom: the admission comparison in (M.14) includes all outstanding reservations $M_{resv}$, and the check and the reservation write are atomic.	component	Margining	component Judge
26	The mark price always lies between the oracle anchor and the trade reference: $\min(P_{oracle}, P_{trade}) \le P_{mark} \le \max(P_{oracle}, P_{trade})$, and $P_{mark} = P_{oracle}$ exactly when no trade reference exists.	component	The Oracle	component Judge
27	While a re-anchor is pending, the trusted anchor and its timestamp never move: $P_{oracle}$ and $t_{last}$ are unchanged by every pending print, so an unconfirmed candidate can never reach the mark.	component	The Oracle	component Judge
28	On a fresh anchor, every trusted print satisfies $\Delta_{step} \le \theta$ ((O.1)), and once the history window is full, $\Delta_{path} \le \theta\sqrt{N_h}$ ((O.3)) as well — the anchor moves by at most a factor $1+\theta$ per print and its ten-print path is square-root bounded.	component	The Oracle	component Judge
29	A large move off a stale anchor is never trusted from a single print: promotion requires at least $\max(k, 2) \ge 2$ consecutive prints each within the active step bound of the running candidate, even when escalated.	component	The Oracle	component Judge
30	A single trade — including a wash or self-trade fired immediately before a liquidation check — cannot move the mark by more than the volume-weighted median allows: shifting $P_{trade}$ requires manipulated prices to carry strictly more than half the window's total traded size.	component	The Oracle	component Judge
31	The book is never crossed: whenever both sides are non-empty, $P_b < P_a$.	component	The Order Book	component Judge
32	No order overfills: $q_f \le q$ throughout an order's life, so remaining quantity $q - q_f$ never goes negative.	component	The Order Book	component Judge
33	Every fill respects the taker's limit: a buy fills at $P^{\star} \le P_{lim}$ and a sell at $P^{\star} \ge P_{lim}$.	component	The Order Book	component Judge
34	Every resting order has strictly positive remaining quantity, $q - q_f > 0$.	component	The Order Book	component Judge
35	The order index and the book agree exactly: the index holds precisely the ids of resting orders, each mapped to its true side and price.	component	The Order Book	component Judge
36	The slippage cap is monotone: for a fixed book and taker, a larger cap $\beta$ fills at least as much quantity as a smaller one.	component	The Order Book	component Judge
37	Every stored position has strictly positive size: $q > 0$.	component	Position Tracking	component Judge
38	The entry price is a convex combination of the fill prices that built the current side, so $P_e > 0$ and $q\,P_e$ equals the total notional paid; the aggregate entry is independent of the order of same-side fills.	component	Position Tracking	component Judge
39	A partial close changes size but never entry price, and the settled amount is exactly (T.4) at the closing fill's price, not the mark.	component	Position Tracking	component Judge
40	Bankruptcy is at least as adverse as liquidation: $\sigma\,(P_{liq} - P_{bkr}) \ge 0$ for any position that is not over-collateralized ($C \le P_e\,q$, $0 \le r_m < 1$).	component	Position Tracking	component Judge
41	P&L channels are disjoint: a funding payment changes only the funding accumulator, fees change only the fee channel, and neither moves the entry price, size, or realized P&L.	component	Position Tracking	component Judge
42	Fee accounting closure: within any settlement record, $V = F - R$ ((S.5)) holds exactly — every unit collected as a taker fee is either paid out as a maker rebate or retained as revenue, and money is neither created nor destroyed.	component	Settlement	component Judge
43	Non-negativity of all transfer amounts: $\text{fee}_t \ge 0$ ((S.2)), $\text{rebate}_m \ge 0$ ((S.3)), and $\text{penalty} \ge 0$ ((S.4)), and every emitted funding transfer carries a strictly positive amount $\|x\| > 0$ ((S.6)).	component	Settlement	component Judge
44	Liquidation-penalty destination: every liquidation penalty transfer originates at the taker (the liquidated account) and terminates at the insurance fund — it is never routed to the Exchange fee account and never enters $F$, $R$, or $V$.	component	Settlement	component Judge
45	Merge conservation: for any batch, each merged accumulator equals the sum of that accumulator over the constituents ((S.7)), the merged transfer count equals the sum of constituent transfer counts, and the merged period is $[\min_j \text{start}_j, \max_j \text{end}_j]$.	component	Settlement	component Judge
46	$\sum_{a} \Pi^{f}_{a} \;=\; f\, m_k \sum_{a} s_{a,k} \;=\; 0 \qquad\Longrightarrow\qquad C_{pool}' = C_{pool}$ — Aggregate funding zero-sum across matched open interest	open-loop	global model	composition Judge
47	$\sum_i s_i = C, \qquad D = \min(D, \Phi_1) + \max(D - \Phi_1,\ 0), \qquad \Delta C_a\big\|_{\Lambda} = -\Lambda = -\Delta\Phi\big\|_{\Lambda}, \qquad \Phi = \Sigma_{\mathrm{rec}} - \Sigma_{\mathrm{abs}}$ — Collateral conservation through the liquidation cascade	open-loop	global model	composition Judge
48	$r_m < r_i \;\Longrightarrow\; \big\{\, S : E \le M_{maint}^{pf} \,\big\} \subsetneq \big\{\, S : E \le M_{init}^{pf} \,\big\}$ — Margin monotonicity (maintenance strictly inside initial)	open-loop	global model	simulator, 512 trials
49	$\lvert \Pi^{f}_{a} \rvert \;\le\; c\, q_a\, m_k \qquad \text{per position, per funding interval}$ — Bounded funding transfer per interval	open-loop	global model	simulator, 512 trials
50	$\big\lvert E(S, u') - E(S, u) \big\rvert \;\le\; w\, \theta\, P_{oracle} \sum_i q_i \qquad \text{(fresh-anchor accept branch only)}$ — Bounded equity shock per fresh-anchor tick	closed-loop	global model	composition Judge
51	$\mathrm{stale} \;\Longrightarrow\; (P_{oracle}',\, t_{last}') = (P_{oracle},\, t_{last}) \quad\text{and}\quad \lvert \Delta m_k \rvert \le (1 - w)\, \lvert \Delta P_{trade} \rvert$ — Staleness freezes the anchor leg only	closed-loop	global model	composition Judge
52	$\Delta C_{fee} \;=\; F - R \;=\; V, \qquad \Delta C_{fee} + \textstyle\sum_a \Delta C_a \big\|_{\text{fees}} = 0$ — Fee closure across the fill path	open-loop	global model	composition Judge

References

• The oracle-endogenous closed loop: closed-loop
• Component model: funding-rate
• Component model: insurance-fund
• Component model: liquidation-engine
• Component model: margin-math
• Component model: oracle
• Component model: order-book
• Component model: position-tracker
• Component model: settlement