Closed Loop
The Nexus Exchange is one dynamical system. This document formalizes it as a state-space model in three staged parts, from a single corpus of verified component mathematics. Part I is the heart: the Exchange engine alone, a self-contained transition system S′=f(S,u) in which the oracle price u is simply given — every economic fact of the venue (matching, position lifecycle, funding, margining, liquidation, loss absorption) is an event map acting on one state vector. Part II summarizes the input process: u is not raw but the output of a guarded process u′=g(u,prints), detailed in the oracle component document. Part III is the union: the closed loop obtained by composing the two, whose invariants — bounded equity shock per accepted tick, the conditional freeze under staleness — exist only because the guarded input and the engine response interlock.
Notation throughout matches the component corpus: Ca collateral, s signed position size with σ=sign(s) and q=∣s∣, Pe entry price, mk mark, Φ insurance fund, f funding rate, E equity, M margin requirements. Claims are grounded by inline equation references into the component models; where the corpus lacks an expression, the gap is named rather than papered over.
The input process: u′=g(u,sources)
The input is itself a guarded process u′=g(u,prints): an incoming print moves the trusted anchor only if it passes the single-step and path deviation guards ((O.1), (O.2), (O.3)); a silent feed trips the staleness predicate ((O.4)) and routes prints into a multi-print re-anchor confirmation with escalation ((O.5), (O.6)). One event map, given below, summarizes the whole process; the oracle component document carries the detail.
Oracle print (input process)
The single event of the input process u′=g(u,prints). On a fresh anchor, an incoming print is accepted only if it passes the single-step guard ((O.1)) and, once the ten-print history is full, the path guard ((O.2) against (O.3)); acceptance moves (Poracle,tlast) and appends to the history, rejection changes nothing. When the staleness predicate trips ((O.4)), prints route into the re-anchor protocol instead: each print within the active bound of the running candidate advances the confirmation counter, an inconsistent print restarts it ((O.5)), escalation widens the bound by print count or elapsed time ((O.6)), and promotion requires max(k,2)≥2 consecutive confirmations — while pending, the anchor and its timestamp never move. The engine sees only the result: u steps by at most a factor 1+θ per fresh accept, or jumps on a confirmed re-anchor commit. Touches: Poracle,tlast,Ω only — no engine coordinate.
The union: the closed loop
The union is the closed loop: the guarded input process feeds the engine, and the engine feeds back into its own input. Downward, every accepted print re-prices the entire state at once — equity, maintenance floors, funding premium, and the order collar all move with mk — and the guards compose into the closed-loop bounds above: a fresh tick's motion is capped by θ before the engine ever sees it, so the equity shock per tick is bounded ((O.1) composed with (O.8) and (M.5)), while a stale feed freezes exactly the anchor leg ((O.4)) and leaves liquidation live on the trade leg. Upward, every fill — including the cascade's own close fills — enters the five-trade window that shapes the trade reference ((O.7)): the engine influences the mark that will next judge its accounts, damped by (1−w) and by the volume-weighted median's majority-volume requirement. This two-way coupling is what makes the composed system a genuine feedback loop rather than a filter followed by a plant: a liquidation prints fills, the fills move the trade leg, the moved mark re-evaluates the next account.
The composed system's long-run geometry: healthy states at an agreeing mark (mk=Poracle,k, zero premium) are equilibria — accrual adds zero, settlements transfer nothing ((S.6) emits no zero-amount transfer), the trigger is silent. Two absorbing regimes matter. Fund depletion: Φ=0 after an exhausting absorption ((I.2) hits its floor exactly) arms ADL through both nested predicates and stays armed until a spread or penalty credit refills the balance ((I.7), (I.10)); the credit-before-absorb ordering (settled, code-verified) means a single liquidation carrying both profit and debt absorbs against Φ+g, never the pre-credit balance. Liquidation stall: a negative cross share produces an oversized close that (L.13) rejects on every scan — a live-lock fixed point of the cascade in which the account remains triggered but untouched, exiting only when the mark or the share changes.
What the composition does not yet witness, named plainly. (1) adl_settlement_unmodeled: the ADL counterparty settlement map — closing price, per-counterparty size reduction, both sides' Ca updates, open-interest preservation — has no component expressions; the cascade's conservation invariant is scoped up to this leg, and the next cycle derives it from code (v0.0.9 audit, medium). (2) residual_entry_remark_unwitnessed: the settle map values a partial liquidation's unfilled remainder at the mark and folds it into cash ((L.16) inside (L.17)), while the position layer retains the remainder's entry price ((T.1) is untouched by reductions) — consistency requires either excluding Πres from the cash settle or re-anchoring the residual's entry at the mark, and no expression witnesses either; conservation is therefore stated for fully-filled cascades. (3) cancel_release_arithmetic_unwitnessed: the cancel/expiry map's per-order margin release has no corpus expression, though the guards that depend on it ((M.16), (M.14)) fix its required semantics. (4) adl_arming_condition_ambiguity: the two arming predicates are nested, not symmetric — settle-amount firing implies threshold firing, and the surviving question is whether ADL executes when the threshold arms with Dadl=0. Conversely, one previously-open gap is now closed: the liquidation penalty's fund-side destination is witnessed by the v0.0.9 expressions (I.9), (I.10), and (I.11), retiring liquidation_penalty_sink as an open finding of this model.
Invariants of the closed loop
Bounded equity shock per fresh-anchor tick
On the fresh-anchor accept branch of the input process, one oracle tick can shock an account's equity by at most wθPoracle∑iqi per market: the accepted anchor moves by at most θPoracle ((O.1)), the blend damps the anchor leg by w ((O.8)), and equity is affine in the mark with slope bounded by total size ((T.2), (M.5)). Explicitly excluded: the re-anchor commit branch — commits are bounded by θr/θe relative to the candidate, not by θ relative to the prior anchor, and can exceed this bound (simulator result reanchor_commit_exceeds_tick_bound).
Why it holds: This invariant exists only at the composition: the engine alone accepts any u, and the oracle alone bounds prices, not equity. The accept guard rejects before any state write, so a committed fresh tick satisfies ∣ΔPoracle∣≤θPoracle; the mark is a convex combination, so ∣Δmk∣=w∣ΔPoracle∣ with Wk unchanged by an oracle event; and E is affine in mk with slope ∑isi,k, giving the bound by the triangle inequality. The exclusion is forced: re-anchor promotion moves the anchor to the candidate in one step, which the corpus bounds only relative to the candidate chain.
Staleness freezes the anchor leg only
While the anchor is stale ((O.4)), no pending print can move Poracle or tlast — the re-anchor protocol persists only candidate bookkeeping until max(k,2) confirmations ((O.5)) — so the anchor leg of the mark is frozen and mark motion is confined to the trade leg, damped by (1−w) and defended by the volume-weighted median ((O.8), (O.7)). Stated honestly: staleness does not pause liquidations — the trigger (L.4) keeps evaluating at the partially-frozen mark, whose trade leg the engine's own fills keep moving. The fail-closed property is confined to the anchor.
Why it holds: Only the trusted-accept path writes the anchor pair, and the pending branch returns without calling it, with the Trusted/Pending discriminant preventing a silent commit — so the anchor leg's contribution to Δmk is zero under staleness. The mark is a convex combination, so the residual motion is exactly (1−w)ΔPtrade, and shifting Ptrade requires manipulated prices to carry strictly more than half the window's volume. The liquidation half is a non-claim: no component expression conditions the trigger on freshness, so the composed system inherits liquidation-at-the-frozen-leg rather than a pause.
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.
B.1 The state vector
per-market
trade_window
Wk
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.
oracle_anchor
Poracle,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
tlast,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
Ω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.
B.2 Inputs and parameters
Inputs are exogenous — they arrive from outside the state; parameters are constants of market or system configuration.
Inputs
oracle_print_price
Pnew
USDX per unit of asset
An incoming external oracle print being validated against the anchor or the pending re-anchor candidate.
wall_clock_time
tnow
milliseconds
Feed-supplied timestamp of the incoming print or staleness evaluation, in Unix milliseconds.
time_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
Plim
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
β
basis points
Taker-supplied per-order slippage cap on a market order; absent means no cap.
preview_requested_qty
qreq
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
funding_rate_cap
c
fraction per funding interval
per-market
Symmetric cap on the funding rate; specified at 0.5% per settlement window.
adl_threshold
κ
USDX
per-market
ADL trigger threshold on the fund balance; default zero arms ADL only at full depletion.
maintenance_margin_rate
rm
dimensionless ratio
per-market
Market maintenance margin rate; strictly less than the initial margin rate.
initial_margin_rate
ri
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
δ
USDX per base unit
per-market
Minimum price increment; non-positive tick disables alignment.
lot_size
ℓ
base units
per-market
Market lot size; order and position sizes are integer multiples of it; zero disables the alignment check.
taker_fee_bps
bt
basis points
per-market
Taker fee rate charged on fill notional.
maker_rebate_bps
bm
basis points
per-market
Maker rebate rate, stored negative by convention; applied by absolute value.
liquidation_penalty_bps
bliq
basis points
per-market
Penalty rate applied to the notional of liquidation fills and routed to the insurance fund.
price_band_bps
bband
basis points
per-market
Maximum admissible relative deviation of a limit price from the mark (the admission collar).
oracle_deviation_threshold
θ
dimensionless fraction
per-market
Single-step deviation threshold for accepting an oracle print against the anchor.
oracle_history_size
Nh
prints
global
Fixed size of the rolling price-update window used by the path-manipulation check (HISTORY_SIZE = 10).
oracle_staleness_seconds
τs
seconds
per-market
Staleness threshold: the anchor is stale strictly beyond this many seconds since the last trusted update.
reanchor_max_deviation
θr
dimensionless fraction
per-market
Per-step consistency bound for re-anchor confirmations against the running candidate.
escalation_max_deviation
θ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
Ne
prints
per-market
Print-count arm of the re-anchor escalation trigger.
escalation_seconds
τ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).
B.3 Derived observables
Pure functions of state, inputs, and parameters — recomputed, never persisted.
mark_price
mk
USDX per base unit
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
Ptrade
USDX per base unit
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
Fractional deviation of the mark from the anchor at a sample; skipped when the anchor is non-positive.
funding_rate
f
fraction per interval
Clamped time-weighted average premium, recomputed fresh from (A, T) at settlement with the T = 0 branch returning zero.
funding_payment
Πf
USDX
Signed per-position funding payment sigma q m f; simultaneously the settlement event's collateral update delta.
unrealized_pnl
uPnL
USDX
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
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
Mm
USDX
Maintenance margin at the mark; coherence-merged with the portfolio and liquidation-engine instances.
initial_margin
Mi
USDX
Initial margin at the mark (stamped allocated margin where set); coherence-merged with the portfolio instance.
available_margin
Mavail
USDX
Equity minus total initial margin held; can be negative; gates order admission, not withdrawal.
added_exposure
Δq
base units
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
Madd
USDX
Initial margin charged on added exposure at the mark and effective rate; also the amount written into the reservation at admission.
isolated_margin_cushion
Ciso
USDX
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
pb
USDX per base unit
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
p~b
USDX per base unit
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
pliq
USDX per base unit
Analytically-solved mark at which equity meets the maintenance requirement; display/analysis, neither moves state nor gates events.
cross_collateral_share
si
USDX
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
ℓi
USDX
``
max(0, -uPnL_i) per market with entry-price fallback; defined only in variable prose, no corpus expression id.
total_loss
L
USDX
``
Sum of position losses across the positions liquidated together; prose-defined only.
safe_size
qsafe
base units
Largest lot-multiple size whose 1.5x-padded initial margin the collateral share covers.
liquidation_qty
qliq
base units
Close-order quantity: full size in Full mode or degenerate cases, else reduction to safe size.
fill_quantity
q⋆
base units
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⋆
USDX per base unit
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
qc
base units
Portion of an opposing fill that closes existing size: min(size, fill quantity).
total_filled
Qf
base units
``
Sum of the liquidation close order's fill quantities; within-event accumulation, prose-defined only.
spread_profit
g
USDX
Positive part of fills' price improvement over the aligned bankruptcy price, summed over fills; credited to the fund.
realized_fill_pnl
Πfill
USDX
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
Πres
USDX
Mark-valued PnL of the unfilled remainder of the close order; zero on complete fill.
bad_debt
D
USDX
Non-negative shortfall after fills-aware settlement against the collateral share; drawn from the fund, then ADL.
absorbed_amount
Dabs
USDX
min(bad debt, fund balance): the delta by which the fund and its absorption ledger move.
adl_settle_amount
Dadl
USDX
Shortfall handed to ADL after the fund is drained; an instruction is emitted only when strictly positive.
adl_priority_score
ρ
dimensionless
ADL ranking score pi * L, descending with deterministic account-id tie-break; coherence-merged with the insurance-fund instance.
adl_pnl_percent
π
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
Λowed
USDX
Penalty owed on filled liquidation notional at the market's penalty rate.
penalty_charged
Λ
USDX
Penalty actually debited/credited: the owed amount capped at available collateral, so the pair cannot mint USDX.
net_exchange_revenue
V
USDX
Settlement-record closure: total taker fees minus total maker rebates.
margin_ratio
ρM
dimensionless
Equity over total notional; undefined at zero notional; diagnostic — gates nothing in the corpus.
max_position_size
qmax
base units
Largest lot-aligned position openable with given collateral at the market rate; sizing/display analysis.
withdrawable_collateral
Wmax
USDX
Full realized collateral for a flat, unreserved account, zero otherwise; the withdrawal guard's cap.
best_bid
Pb
USDX per base unit
``
Highest resting bid — a structural readout of the order_book coordinate; no corpus expression id.
best_ask
Pa
USDX per base unit
``
Lowest resting ask — a structural readout of the order_book coordinate; no corpus expression id.
mid_price
Pmid
USDX per base unit
Midpoint of best bid and ask, snapshotted once at market-order submission for the slippage cap; undefined when either side is empty.
slippage_span
Δslip
USDX per base unit
Half-width of the admissible VWAP band anchored at the mid-price snapshot.
available_qty
Qavail
base units
``
Pre-match opposing liquidity at prices satisfying the taker's limit; within-event readout of the book, prose-defined only.
taker_remaining
qt
base units
``
Taker's unfilled remainder during the matching walk; within-event intermediate, prose-defined only.
running_notional
Vk
USDX
``
Cumulative notional of fills accepted so far in a market-order walk; within-event accumulator, prose-defined only.
running_filled
Qk
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
P
USDX per base unit
Read-only market-order VWAP preview; undefined when liquidity cannot cover the request.
funding_integral
φ
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
npos
count
``
Count of the account's open positions — a structural readout of the position coordinates; no corpus expression id.
B.4 The transition matrix
Guards
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
oracle_print_accept
oracle_reanchor_step
oracle_reanchor_commit
oracle_anchor (per-market)
✓
·
✓
anchor_timestamp (per-market)
✓
·
✓
oracle_guard_state (per-market)
✓
✓
✓
References
Last updated

