> For the complete documentation index, see [llms.txt](https://docs.nexus.xyz/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://docs.nexus.xyz/math-engine/global.md). # 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)](/math-engine/oracle.md), [(O.7)](/math-engine/oracle.md)); 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)](/math-engine/position-tracker.md)), marks revalue them ([(T.2)](/math-engine/position-tracker.md)), funding transfers value between the sides ([(F.4)](/math-engine/funding-rate.md)), and the cascade repossesses positions whose equity has fallen to the maintenance floor ([(L.4)](/math-engine/liquidation-engine.md)). The coupling quantity that organizes the whole engine is **equity**, $$E = C + \Pi$$ ([(M.5)](/math-engine/margin-math.md)): affine in the mark, additive over positions, and read by every guard that matters. Admission compares equity headroom against initial margin ([(M.13)](/math-engine/margin-math.md), [(M.14)](/math-engine/margin-math.md)); the liquidation trigger compares it against maintenance margin ([(L.4)](/math-engine/liquidation-engine.md)); withdrawal deliberately ignores it and moves only realized collateral ([(M.16)](/math-engine/margin-math.md)). Because maintenance is strictly inside initial ($$r\_m < r\_i$$, [(M.4)](/math-engine/margin-math.md) vs [(M.2)](/math-engine/margin-math.md)), 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)](/math-engine/funding-rate.md)), 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)](/math-engine/margin-math.md) 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)](/math-engine/order-book.md)); positive entry prices; resting limit prices strictly positive on the tick lattice $$\delta\mathbb{Z}$$ ([(B.2)](/math-engine/order-book.md)) 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)](/math-engine/margin-math.md) $$\le$$ [(M.2)](/math-engine/margin-math.md)); $$\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)](/math-engine/margin-math.md)); admission by alignment, collar, and headroom guards evaluated before any mutation; the funding rate is total via its explicit $$T = 0$$ branch ([(F.3)](/math-engine/funding-rate.md)); accrual accepts only strictly advancing time and positive anchor ([(F.2)](/math-engine/funding-rate.md)); every $$\min$$/$$\max$$ in the cascade and the fund ([(I.1)](/math-engine/insurance-fund.md), [(I.9)](/math-engine/insurance-fund.md)) is total and sign-safe; tick alignment clamps to one tick rather than producing non-positive prices ([(L.9)](/math-engine/liquidation-engine.md)); and the reduce-only guard ([(L.13)](/math-engine/liquidation-engine.md)) 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)](/math-engine/margin-math.md) and the withdrawal guard [(M.16)](/math-engine/margin-math.md). | 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)](/math-engine/position-tracker.md): 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)](/math-engine/order-book.md). | multiset of orders | | $$A\_k$$ | accumulated\_premium | market | Time-weighted premium accumulator of the current funding interval, written only by [(F.2)](/math-engine/funding-rate.md) 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)](/math-engine/funding-rate.md) 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)](/math-engine/oracle.md) — 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)](/math-engine/insurance-fund.md) and penalties [(I.10)](/math-engine/insurance-fund.md), debited by absorption [(I.2)](/math-engine/insurance-fund.md); $$\Phi \ge 0$$ with exact depletion. | USDX | | $$C\_{pool}$$ | funding\_pool | system | The funding pool book through which every funding transfer routes ([(S.6)](/math-engine/settlement.md)): 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)](/math-engine/settlement.md), [(S.3)](/math-engine/settlement.md)), with closure $$V = F - R$$ ([(S.5)](/math-engine/settlement.md)). 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)](/math-engine/oracle.md); 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)](/math-engine/oracle.md) and the pending re-anchor block $$(P\_{cand}, n\_p, t\_0)$$ behind [(O.5)](/math-engine/oracle.md) and [(O.6)](/math-engine/oracle.md). 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)](/math-engine/margin-math.md): 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)](/math-engine/order-book.md), [(B.2)](/math-engine/order-book.md)), the mark collar ([(B.3)](/math-engine/order-book.md)), FOK availability ([(B.5)](/math-engine/order-book.md)), and margin headroom — the isolated path [(M.13)](/math-engine/margin-math.md) at the effective rate [(M.1)](/math-engine/margin-math.md), the cross path [(M.14)](/math-engine/margin-math.md) charging only added exposure ([(M.11)](/math-engine/margin-math.md), [(M.12)](/math-engine/margin-math.md)) 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)](/math-engine/order-book.md), [(B.7)](/math-engine/order-book.md)), bounded for market orders by the running-VWAP slippage band ([(B.9)](/math-engine/order-book.md), [(B.10)](/math-engine/order-book.md)). Self-trade prevention fires inside this loop: [(B.8)](/math-engine/order-book.md) 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)](/math-engine/position-tracker.md), reduce [(T.3)](/math-engine/position-tracker.md) realizing [(T.4)](/math-engine/position-tracker.md) into $$C\_a$$ at the fill price, flip [(T.5)](/math-engine/position-tracker.md) — debits the taker fee and credits the maker rebate between $$C\_a$$ and $$C\_{fee}$$ ([(S.2)](/math-engine/settlement.md), [(S.3)](/math-engine/settlement.md), closure [(S.5)](/math-engine/settlement.md)), 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)](/math-engine/order-book.md)), the reduce-only rejection of an oversized liquidation close ([(L.13)](/math-engine/liquidation-engine.md)), and self-trade prevention's cancel-of-the-fully-reduced-side ([(B.8)](/math-engine/order-book.md)) — 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)](/math-engine/margin-math.md) guards on $$n\_{resv} = 0$$ and [(M.14)](/math-engine/margin-math.md) 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)](/math-engine/funding-rate.md)) — not the mark — and adds its time-weighted contribution to the interval accumulator ([(F.2)](/math-engine/funding-rate.md)). 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)](/math-engine/funding-rate.md)); each open position's payment is $$\Pi^f = \sigma, q, P\_{oracle,k}, f$$ ([(F.4)](/math-engine/funding-rate.md)), 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)](/math-engine/settlement.md)): 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)](/math-engine/liquidation-engine.md)) over [(L.1)](/math-engine/liquidation-engine.md), [(L.2)](/math-engine/liquidation-engine.md), [(L.3)](/math-engine/liquidation-engine.md). Collateral is apportioned — cross accounts split the shared pool loss-proportionally with the remainder fold conserving it exactly ([(L.6)](/math-engine/liquidation-engine.md), [(L.7)](/math-engine/liquidation-engine.md)); isolated positions use their stamped cushion ([(L.5)](/math-engine/liquidation-engine.md)). Close orders are sized ([(L.11)](/math-engine/liquidation-engine.md), [(L.12)](/math-engine/liquidation-engine.md)), guarded reduce-only ([(L.13)](/math-engine/liquidation-engine.md) — a negative share yields an oversized order that is rejected each scan, a stall not a flip), priced from the bankruptcy price ([(L.8)](/math-engine/liquidation-engine.md)) tick-aligned toward executability ([(L.9)](/math-engine/liquidation-engine.md), [(L.10)](/math-engine/liquidation-engine.md)), 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)](/math-engine/liquidation-engine.md), mark-valued residual [(L.16)](/math-engine/liquidation-engine.md), and spread profit [(L.14)](/math-engine/liquidation-engine.md); bad debt is $$D\_i = \max(0, -X\_i)$$ ([(L.17)](/math-engine/liquidation-engine.md)). 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)](/math-engine/settlement.md) capped at the retained collateral ([(I.9)](/math-engine/insurance-fund.md)) — a debit whose fund-side destination is witnessed: [(I.10)](/math-engine/insurance-fund.md) and [(I.11)](/math-engine/insurance-fund.md) 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)](/math-engine/insurance-fund.md), [(I.7)](/math-engine/insurance-fund.md)), then absorption $$\min(D, \Phi\_1)$$ ([(I.1)](/math-engine/insurance-fund.md), [(I.2)](/math-engine/insurance-fund.md)) with lockstep ledgers ([(I.3)](/math-engine/insurance-fund.md), [(I.8)](/math-engine/insurance-fund.md)). ADL arms through two **nested** predicates: the settle amount $$D\_{\mathrm{adl}} = \max(D - \Phi\_1, 0) > 0$$ ([(I.4)](/math-engine/insurance-fund.md)) and, after absorption, the threshold $$\Phi' \le \kappa$$ ([(I.5)](/math-engine/insurance-fund.md)). 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)](/math-engine/liquidation-engine.md), [(I.6)](/math-engine/insurance-fund.md)); 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)](/math-engine/position-tracker.md) 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)](/math-engine/funding-rate.md) 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)](/math-engine/settlement.md)) 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)](/math-engine/order-book.md), with reduces and flips per [(T.3)](/math-engine/position-tracker.md) and [(T.5)](/math-engine/position-tracker.md)) — 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)](/math-engine/funding-rate.md)), 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)](/math-engine/settlement.md)). *Composes:* [*(F.4)*](/math-engine/funding-rate.md) [*(F.3)*](/math-engine/funding-rate.md) [*(S.6)*](/math-engine/settlement.md) [*(B.6)*](/math-engine/order-book.md) [*(T.3)*](/math-engine/position-tracker.md) [*(T.5)*](/math-engine/position-tracker.md) ### 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)](/math-engine/liquidation-engine.md), [(L.7)](/math-engine/liquidation-engine.md)); every unit of bad debt [(L.17)](/math-engine/liquidation-engine.md) is covered exactly once, split between fund absorption [(I.1)](/math-engine/insurance-fund.md) and the ADL settle amount [(I.4)](/math-engine/insurance-fund.md) 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)](/math-engine/insurance-fund.md), [(I.10)](/math-engine/insurance-fund.md)). 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)](/math-engine/insurance-fund.md) commits before [(I.2)](/math-engine/insurance-fund.md)). 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)*](/math-engine/liquidation-engine.md) [*(L.7)*](/math-engine/liquidation-engine.md) [*(L.17)*](/math-engine/liquidation-engine.md) [*(I.1)*](/math-engine/insurance-fund.md) [*(I.4)*](/math-engine/insurance-fund.md) [*(I.7)*](/math-engine/insurance-fund.md) [*(I.2)*](/math-engine/insurance-fund.md) [*(I.9)*](/math-engine/insurance-fund.md) [*(I.10)*](/math-engine/insurance-fund.md) ### 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)](/math-engine/margin-math.md) vs [(M.2)](/math-engine/margin-math.md), [(M.10)](/math-engine/margin-math.md) vs [(M.9)](/math-engine/margin-math.md)), so the liquidation region [(L.4)](/math-engine/liquidation-engine.md) 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)](/math-engine/funding-rate.md)), the taker-fee debit that admission headroom does not charge ([(S.2)](/math-engine/settlement.md) vs [(M.14)](/math-engine/margin-math.md)), 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)](/math-engine/margin-math.md)). 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)*](/math-engine/margin-math.md) [*(M.2)*](/math-engine/margin-math.md) [*(M.10)*](/math-engine/margin-math.md) [*(M.9)*](/math-engine/margin-math.md) [*(M.1)*](/math-engine/margin-math.md) [*(M.14)*](/math-engine/margin-math.md) [*(L.4)*](/math-engine/liquidation-engine.md) [*(S.2)*](/math-engine/settlement.md) [*(F.4)*](/math-engine/funding-rate.md) ### 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)](/math-engine/funding-rate.md)), and the payment is linear in the rate ([(F.4)](/math-engine/funding-rate.md)), 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)](/math-engine/settlement.md)) — no map between the clamp and the ledger can amplify the amount. *Composes:* [*(F.3)*](/math-engine/funding-rate.md) [*(F.4)*](/math-engine/funding-rate.md) [*(S.6)*](/math-engine/settlement.md) ### 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)](/math-engine/settlement.md), [(S.3)](/math-engine/settlement.md), [(S.5)](/math-engine/settlement.md)), the closure is preserved linearly under batch merge ([(S.7)](/math-engine/settlement.md)), and liquidation penalties never contaminate it — they route to the fund, never to $$C\_{fee}$$ ([(S.4)](/math-engine/settlement.md)). *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)*](/math-engine/settlement.md) [*(S.3)*](/math-engine/settlement.md) [*(S.5)*](/math-engine/settlement.md) [*(S.7)*](/math-engine/settlement.md) [*(S.4)*](/math-engine/settlement.md) [*(S.1)*](/math-engine/settlement.md) ## 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)](/math-engine/margin-math.md)), while total maintenance is piecewise-linear with slope $$\sum\_i q\_{i,k}, r\_{m,k}$$ ([(M.10)](/math-engine/margin-math.md)) — 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)](/math-engine/position-tracker.md)), with the bankruptcy price ([(T.9)](/math-engine/position-tracker.md)) strictly beyond it for any under-collateralized position. Margin requirements scale linearly in size ([(M.2)](/math-engine/margin-math.md)), the effective rate never undercuts the market rate ([(M.1)](/math-engine/margin-math.md)), added exposure is non-negative so admission never pre-credits a reduce ([(M.11)](/math-engine/margin-math.md)), and the slippage cap is monotone in its band ([(B.10)](/math-engine/order-book.md)). **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)](/math-engine/funding-rate.md)), 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)](/math-engine/funding-rate.md), [(S.6)](/math-engine/settlement.md)). 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)](/math-engine/liquidation-engine.md)), 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)](/math-engine/oracle.md) | 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)](/math-engine/oracle.md) | 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)](/math-engine/funding-rate.md) | 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)](/math-engine/funding-rate.md) | 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)](/math-engine/funding-rate.md) | 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)](/math-engine/position-tracker.md) | 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)](/math-engine/margin-math.md) | 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)](/math-engine/margin-math.md) | Maintenance margin at the mark; coherence-merged with the portfolio and liquidation-engine instances. | | `initial_margin` | $$M\_i$$ | USDX | [(M.2)](/math-engine/margin-math.md) | Initial margin at the mark (stamped allocated margin where set); coherence-merged with the portfolio instance. | | `available_margin` | $$M\_{avail}$$ | USDX | [(M.7)](/math-engine/margin-math.md) | Equity minus total initial margin held; can be negative; gates order admission, not withdrawal. | | `added_exposure` | $$\Delta q$$ | base units | [(M.11)](/math-engine/margin-math.md) | 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)](/math-engine/margin-math.md) | 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)](/math-engine/liquidation-engine.md) | 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)](/math-engine/liquidation-engine.md) | 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)](/math-engine/liquidation-engine.md) | 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)](/math-engine/position-tracker.md) | 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)](/math-engine/liquidation-engine.md) | 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)](/math-engine/liquidation-engine.md) | Largest lot-multiple size whose 1.5x-padded initial margin the collateral share covers. | | `liquidation_qty` | $$q\_{liq}$$ | base units | [(L.12)](/math-engine/liquidation-engine.md) | Close-order quantity: full size in Full mode or degenerate cases, else reduction to safe size. | | `fill_quantity` | $$q^{\star}$$ | base units | [(B.6)](/math-engine/order-book.md) | 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)](/math-engine/order-book.md) | 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)](/math-engine/position-tracker.md) | 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)](/math-engine/liquidation-engine.md) | 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)](/math-engine/liquidation-engine.md) | 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)](/math-engine/liquidation-engine.md) | Mark-valued PnL of the unfilled remainder of the close order; zero on complete fill. | | `bad_debt` | $$D$$ | USDX | [(L.17)](/math-engine/liquidation-engine.md) | Non-negative shortfall after fills-aware settlement against the collateral share; drawn from the fund, then ADL. | | `absorbed_amount` | $$D\_{abs}$$ | USDX | [(I.1)](/math-engine/insurance-fund.md) | min(bad debt, fund balance): the delta by which the fund and its absorption ledger move. | | `adl_settle_amount` | $$D\_{adl}$$ | USDX | [(I.4)](/math-engine/insurance-fund.md) | Shortfall handed to ADL after the fund is drained; an instruction is emitted only when strictly positive. | | `adl_priority_score` | $$\rho$$ | dimensionless | [(L.18)](/math-engine/liquidation-engine.md) | 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)](/math-engine/settlement.md) | Penalty owed on filled liquidation notional at the market's penalty rate. | | `penalty_charged` | $$\Lambda$$ | USDX | [(I.9)](/math-engine/insurance-fund.md) | Penalty actually debited/credited: the owed amount capped at available collateral, so the pair cannot mint USDX. | | `fill_notional` | $$V^{\star}$$ | USDX | [(S.1)](/math-engine/settlement.md) | Notional of a single fill, size times price, exact decimal. | | `net_exchange_revenue` | $$V$$ | USDX | [(S.5)](/math-engine/settlement.md) | Settlement-record closure: total taker fees minus total maker rebates. | | `margin_ratio` | $$\rho\_M$$ | dimensionless | [(M.6)](/math-engine/margin-math.md) | Equity over total notional; undefined at zero notional; diagnostic — gates nothing in the corpus. | | `max_position_size` | $$q\_{max}$$ | base units | [(M.15)](/math-engine/margin-math.md) | Largest lot-aligned position openable with given collateral at the market rate; sizing/display analysis. | | `withdrawable_collateral` | $$W\_{max}$$ | USDX | [(M.16)](/math-engine/margin-math.md) | 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)](/math-engine/order-book.md) | 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)](/math-engine/order-book.md) | 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)](/math-engine/order-book.md) | 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)](/math-engine/position-tracker.md) [(S.2)](/math-engine/settlement.md) [(S.3)](/math-engine/settlement.md) | · | · | [(F.4)](/math-engine/funding-rate.md) | [(L.15)](/math-engine/liquidation-engine.md) [(L.16)](/math-engine/liquidation-engine.md) [(I.9)](/math-engine/insurance-fund.md) | · | · | · | · | | `reserved_margin` (per-account) | · | [(M.12)](/math-engine/margin-math.md) | ✓ | · | · | · | · | · | · | · | | `signed_position_size` (per-position) | · | [(T.3)](/math-engine/position-tracker.md) [(T.5)](/math-engine/position-tracker.md) ✓ | · | · | · | [(T.3)](/math-engine/position-tracker.md) | · | · | · | · | | `entry_price` (per-position) | · | [(T.1)](/math-engine/position-tracker.md) | · | · | · | [(T.1)](/math-engine/position-tracker.md) | · | · | · | · | | `order_book` (per-market) | · | [(B.6)](/math-engine/order-book.md) [(B.8)](/math-engine/order-book.md) | ✓ | · | · | [(B.6)](/math-engine/order-book.md) | · | · | · | · | | `accumulated_premium` (per-market) | · | · | · | [(F.2)](/math-engine/funding-rate.md) | ✓ | · | · | · | · | · | | `interval_clock` (per-market) | · | · | · | ✓ | ✓ | · | · | · | · | · | | `trade_window` (per-market) | · | [(B.7)](/math-engine/order-book.md) | · | · | · | [(B.7)](/math-engine/order-book.md) | · | · | · | · | | `insurance_fund_balance` (per-market) | · | · | · | · | · | [(I.7)](/math-engine/insurance-fund.md) [(I.2)](/math-engine/insurance-fund.md) [(I.10)](/math-engine/insurance-fund.md) | · | · | · | · | | `insurance_fund_total_absorbed` (per-market) | · | · | · | · | · | [(I.3)](/math-engine/insurance-fund.md) | · | · | · | · | | `insurance_fund_total_received` (per-market) | · | · | · | · | · | [(I.8)](/math-engine/insurance-fund.md) [(I.11)](/math-engine/insurance-fund.md) | · | · | · | · | | `funding_pool` (global) | · | · | · | · | [(S.6)](/math-engine/settlement.md) | · | · | · | · | · | | `exchange_fee_account` (global) | · | [(S.2)](/math-engine/settlement.md) [(S.3)](/math-engine/settlement.md) [(S.7)](/math-engine/settlement.md) | · | · | · | [(S.2)](/math-engine/settlement.md) | · | · | · | · | | `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](/math-engine/funding-rate.md) | 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](/math-engine/funding-rate.md) | 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](/math-engine/funding-rate.md) | 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](/math-engine/funding-rate.md) | 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](/math-engine/funding-rate.md) | 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](/math-engine/insurance-fund.md) | 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](/math-engine/insurance-fund.md) | 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](/math-engine/insurance-fund.md) | 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](/math-engine/insurance-fund.md) | 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](/math-engine/insurance-fund.md) | 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](/math-engine/insurance-fund.md) | 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](/math-engine/liquidation-engine.md) | component Judge | | 13 | The trigger threshold is inclusive: an account with $$E = \sum\_i M\_i$$ is liquidated ((L.4)). | component | [Liquidation](/math-engine/liquidation-engine.md) | 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](/math-engine/liquidation-engine.md) | 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](/math-engine/liquidation-engine.md) | 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](/math-engine/liquidation-engine.md) | 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](/math-engine/liquidation-engine.md) | 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](/math-engine/liquidation-engine.md) | 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](/math-engine/margin-math.md) | 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](/math-engine/margin-math.md) | 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](/math-engine/margin-math.md) | 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](/math-engine/margin-math.md) | 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](/math-engine/margin-math.md) | 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](/math-engine/margin-math.md) | 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](/math-engine/margin-math.md) | 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](/math-engine/oracle.md) | 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](/math-engine/oracle.md) | 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](/math-engine/oracle.md) | 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](/math-engine/oracle.md) | 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](/math-engine/oracle.md) | component Judge | | 31 | The book is never crossed: whenever both sides are non-empty, $$P\_b < P\_a$$. | component | [The Order Book](/math-engine/order-book.md) | 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](/math-engine/order-book.md) | 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](/math-engine/order-book.md) | component Judge | | 34 | Every resting order has strictly positive remaining quantity, $$q - q\_f > 0$$. | component | [The Order Book](/math-engine/order-book.md) | 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](/math-engine/order-book.md) | 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](/math-engine/order-book.md) | component Judge | | 37 | Every stored position has strictly positive size: $$q > 0$$. | component | [Position Tracking](/math-engine/position-tracker.md) | 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](/math-engine/position-tracker.md) | 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](/math-engine/position-tracker.md) | 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](/math-engine/position-tracker.md) | 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](/math-engine/position-tracker.md) | 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](/math-engine/settlement.md) | 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](/math-engine/settlement.md) | 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](/math-engine/settlement.md) | 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](/math-engine/settlement.md) | 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](/math-engine/closed-loop.md) * Component model: [funding-rate](/math-engine/funding-rate.md) * Component model: [insurance-fund](/math-engine/insurance-fund.md) * Component model: [liquidation-engine](/math-engine/liquidation-engine.md) * Component model: [margin-math](/math-engine/margin-math.md) * Component model: [oracle](/math-engine/oracle.md) * Component model: [order-book](/math-engine/order-book.md) * Component model: [position-tracker](/math-engine/position-tracker.md) * Component model: [settlement](/math-engine/settlement.md) --- # Agent Instructions This documentation is published with GitBook. GitBook is the documentation platform designed so that both humans and AI agents can read, navigate, and reason over technical content effectively. Learn more at gitbook.com. ## Querying This Documentation If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question. Perform an HTTP GET request on the current page URL with the `ask` query parameter, and the optional `goal` query parameter: ``` GET https://docs.nexus.xyz/math-engine/global.md?ask=&goal= ``` `ask` is the immediate question: it should be specific, self-contained, and written in natural language. `goal` is optional and describes the broader end goal you are ultimately trying to accomplish on behalf of the user. GitBook uses it to tailor the answer towards what is most useful for that goal. The response will contain a direct answer to the question and relevant excerpts and sources from the documentation. Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.