Proof Exchange Docs

Appearance

Glossary & Notation ​

This is the reference sheet for the rest of the corpus: the core terms, the symbols, and the units and conventions the other docs assume. It defines things once, in one place, so the mechanism and math docs can use a term or a symbol without re-explaining it every time.

Two reading orders work. If you are new, read the glossary top to bottom — it builds from the umbrella concept down to the individual instruments and identities. If you already know the product and just hit an unfamiliar symbol, jump to Notation and symbols or Units and conventions and look it up.

A note on scope: this corpus is conceptual and mechanism-focused. It describes how the exchange behaves and how prices and risk relate, in plain language and inline math. It is not an SDK or API reference — there are no endpoints, wire formats, field layouts, or code here. Where you see a number, treat it as illustrative unless stated otherwise.

Glossary of core terms ​

Terms are grouped so related ideas sit together. Each entry is a one-line, public-safe definition; the deeper treatment lives in the dedicated docs.

The product ​

Conditional market. A market to trade an underlying asset conditioned on whether a real-world event happens, together with a market on the event's own probability. This is the umbrella term for the whole product area.

Conditional-market family (the family). The linked set of five order books created together from one underlying perpetual and one binary event. "The family" is the whole conditional market as one object.

Event. The real-world question a family conditions on — for example a scheduled economic decision, or whether an asset closes above a level. It resolves to one of three dispositions: YES, NO, or Void (unresolvable).

Branch. One of a family's two outcomes: YES or NO. A position "fires" in the branch that wins.

Leg. One specific order book within a family.

Conditional legs. The four event-driven books of a family — the two conditional perpetuals and the two prediction binaries. The underlying perpetual is not a conditional leg; it is a standalone perp that the family is built over.

The five instruments ​

Perpetual (perp). A perpetual future on an asset: a leveraged position with no expiry, kept tethered to the underlying price by funding. The standard building block.

Underlying perpetual (underlying perp). The standard perpetual that anchors a family. Its price is the forward, F. It is referenced by the family, not re-created — which is why one creation step produces a five-book family but only four new books.

Conditional perpetual (conditional perp). A perpetual on the underlying that only pays out if its branch wins, and is voided otherwise. It trades on its own order book at its own price (its "conditional forward"), and it carries leverage — configurable initial and maintenance margin, like any perp, applied in the branch where it fires.

Conditional perp (YES) / (NO). The two conditional perpetuals of a family. The YES leg, priced CY, tracks the asset given a YES outcome; the NO leg, priced CN, tracks it given a NO outcome. At resolution the winning leg cash-settles to the underlying's mark; the losing leg voids.

Prediction binary. A $0–$1 instrument whose price is the market-implied probability of its outcome. It pays $1 if it wins and $0 if it loses. Prediction binaries carry no separate position margin — their maximum loss is already reflected in account equity.

Prediction binary (YES) / (NO). The two prediction binaries of a family. The YES binary, priced BY, is ≈ p; the NO binary, priced BN, is ≈ 1 − p.

Outcomes and settlement ​

Resolution. The point at which the event's outcome is determined and the family's books settle or void, atomically. The outcome is one of YES, NO, or Void.

Void. The disposition of a conditional perpetual whose branch did not win, or of an event that cannot be resolved. On a Void, profit-and-loss is zero and margin is returned — it is not a loss to $0. This is a defining property: the losing conditional perp is unwound with no cash flow, and its margin is released. On a Void, both prediction binaries pay $0.

Settlement. The transfer of value when an outcome is decided. The winning conditional perp settles at the underlying's mark; the losing one voids; the prediction binaries pay $1 to the winner and $0 to the loser.

Cash-out (early exit). Closing a conditional perpetual before resolution does not pay cash directly. It crystallizes the realized profit-and-loss into prediction-binary tokens entered at $0, which you then sell on the binary book. So the realizable value is roughly (the binary's quoted price) × (the position's face). There is no separate split, merge, or mint step; the close-then-sell pairing is the early-exit path, executed against the binary book.

Pricing concepts ​

Forward / fair price. The price at which a fresh position has zero expected edge. For a conditional perp, the fair price is its conditional mean (its expected value given its branch wins) — not the underlying forward F.

Forward (F). The underlying's fair/forward price; one value shared by every book in a family.

Probability (p). The probability the event resolves YES. It lives in [0, 1] and equals the YES prediction binary's price.

Impact (Δ). The conditional spread, Δ = CY − CN: how far the underlying's expected price differs between the YES and NO outcomes. The impact is driven by how informative the event is about the underlying — that is, by correlation and volatility.

Implied probability. The probability backed out of the conditional perps, p = (F − CN) / (CY − CN). It cross-checks against the binary price, which is the directly-traded p.

Mark price (mark). The reference price used to value open positions for margin, equity, and liquidation. A family's underlying perp marks off its oracle; the conditional legs mark off their own book activity.

Oracle. The external price feed for an asset. The underlying perp's oracle is its primary reference and also drives event resolution for threshold-style events. The conditional legs have no continuous oracle of their own.

Funding. A periodic payment between the longs and shorts of a perpetual that keeps its price tethered to the underlying. Funding applies to perpetuals only — the entire conditional-market family is excluded.

Risk and margin ​

Initial margin (IM). The collateral required to open a position.

Maintenance margin (MM). The minimum collateral required to keep a position open; breaching it triggers liquidation. In this corpus MM always means maintenance margin — the market participant who quotes both sides is written out as "market maker," never abbreviated.

Cross-margin. One account, one collateral balance, all positions sharing it. A gain in one position can offset the margin requirement of another.

Scenario margin. The way conditional-market risk is checked: the engine enumerates every YES/NO combination across your active conditional markets and requires you to stay solvent in the worst one. No credit travels between branches — you can never lean on a gain that vanishes in some outcome.

Box / hedged box. A fully offsetting set of positions whose payoff is locked at entry in every branch — for example a long YES conditional perp, a long NO conditional perp, and an offsetting underlying perp. Because nothing is left at risk, a fully matched box requires essentially no extra margin. This capital efficiency is the central reason conditional markets exist.

Liquidation. The forced closing of positions when an account breaches its maintenance requirement. Closing happens at the oracle/risk mark at end-of-block; it does not sweep the order book. Cancelling resting orders first can, on its own, save an account, because reserved order margin is freed.

Backstops (insurance fund, socialized loss, auto-deleverage). The layered loss-absorption machinery that handles a deficit a liquidation can't cover, in order: a protocol vault, a per-pool insurance fund, a capped socialized loss, and finally auto-deleverage of profitable counterparties. Pools are isolated, so a blowout in one cannot drain another.

Market mechanics ​

Order book. Each market is a central limit order book with price-time priority. Orders match at the resting (maker) price; the taker pays it.

Maker / taker. The maker rests a quote that others trade against; the taker crosses the spread to fill against resting orders.

Time-in-force. How long an order stays live: a good-till-cancelled remainder rests on the book, while immediate-or-cancel and fill-or-kill remainders are dropped rather than rested.

Tick / lot. The minimum price increment (tick) and minimum quantity increment (lot) a market accepts. Orders that aren't whole multiples are rejected.

Spread (s). The gap between the best bid and the best ask a market maker quotes; the half-spread is s/2.

Strike / threshold (K). The level a threshold-style event references — for example "the asset closes above K." For "above K" events the YES conditional necessarily prices above K.

Notation and symbols ​

The corpus uses a small, fixed set of symbols. Each is defined on first use in any document; this is the master list. Read every identity below as a relationship between fair prices, not as a rule the matching engine enforces.

Core pricing trio ​

  • F — forward. The underlying's fair/forward price. One value per family.
  • p — probability. P(event = YES), in [0, 1]. Equal to the YES prediction binary's price.
  • Δ — impact. The conditional spread, Δ = CY − CN.

Leg prices ​

  • CY — conditional perp (YES) price. The underlying's expected price given YES: CY = F + (1 − p)·Δ.
  • CN — conditional perp (NO) price. The underlying's expected price given NO: CN = F − p·Δ.
  • BY — prediction binary (YES) price. ≈ p, quoted in dollars between $0 and $1.
  • BN — prediction binary (NO) price. ≈ 1 − p, quoted between $0 and $1.

Risk and market-quality symbols ​

  • σ — volatility. Volatility of the underlying over the relevant horizon.
  • ρ — correlation. Correlation between the underlying and the conditioning event or asset.
  • s — spread. The market maker's quoted bid–ask spread; half-spread written s/2.
  • IM — initial margin. Collateral to open a position.
  • MM — maintenance margin. Collateral to keep a position open. Never "market maker" — that is always spelled out.
  • K — strike / threshold. The level a threshold-style event references.

The identities ​

These hold between fair prices. They are no-arbitrage relationships that well-functioning books converge to because traders arbitrage deviations away — they describe how prices relate, rather than constraints the engine imposes. The engine matches orders and checks margin; prices are set by the order book.

  • Forward identity: F = p·CY + (1 − p)·CN. The underlying equals the probability-weighted blend of the two conditional prices. (Law of total expectation: the asset's price is the average of its YES-world and NO-world prices, weighted by how likely each world is.)
  • Impact: Δ = CY − CN. The gap between the two conditional prices.
  • Implied probability: p = (F − CN) / (CY − CN). Solving the forward identity for p — where F sits between CN and CY tells you the implied odds.
  • Binary box: BY + BN ≈ $1. The two prediction binaries sum to one dollar at resolution — except through a Void, where both pay $0 and the sum collapses. The $1 box identity holds through YES and NO; it breaks through a Void.

Worked example. Suppose an asset's underlying perp trades at F = $100, and an event has p = 0.40 (the YES binary trades near $0.40, the NO binary near $0.60). Suppose the impact is Δ = $5 — the asset is worth $5 more in the YES world than the NO world. Then:

  • CY = F + (1 − p)·Δ = 100 + 0.60 × 5 = $103.00
  • CN = F − p·Δ = 100 − 0.40 × 5 = $98.00

Check the forward identity: 0.40 × 103 + 0.60 × 98 = 41.2 + 58.8 = $100.00 = F. Back out the implied probability: (100 − 98) / (103 − 98) = 2 / 5 = 0.40 = p. All numbers here are illustrative.

The impact Δ itself is driven by correlation and volatility — how much the underlying moves (σ) and how strongly those moves co-vary with the event (ρ). The pricing docs develop that relationship structurally; the size of Δ in any real market is set by the order book, not by a fixed formula.

Units and conventions in plain terms ​

This corpus keeps everything in plain, human-readable units. The exchange's internal representations (integer micro-units, basis points, wire encodings) belong to the integration reference, not here. The conventions below are what the concepts mean.

Money and prices ​

  • Dollars throughout. Balances, profit-and-loss, fees, notional, and perp prices are written in plain dollars. A perp at $100 means $100 per unit of the asset.
  • Binaries are $0–$1. A prediction binary's price is a dollar figure between $0 and $1, and that figure is the market-implied probability of its outcome. A binary at $0.40 implies a 40% chance and pays $1 if it wins, $0 if it loses.
  • No micro-units. You will not see micro-denominated integers or raw on-the-wire price representations in this corpus. Prices are dollars; probabilities are dollars-in-[0,1] or, equivalently, percentages.

Rates, margins, and leverage ​

  • Margins as percentages / leverage. Initial and maintenance margin are fractions of position notional, stated as percentages or as the leverage they imply. A 10% initial-margin requirement is the same as 10× maximum leverage. Maintenance margin is the lower line that triggers liquidation; initial margin is always at least as strict as maintenance.
  • Conservative defaults. Where leverage is mentioned, assume the conservative default posture for conditional-market positions. This corpus uses that posture throughout.
  • Fees in basis points. Trading fees are quoted in basis points (1 bp = 0.01%), charged on the filled notional of each leg. Both maker and taker sides are charged.
  • Funding as a periodic rate. Funding is a small periodic rate applied to perpetual positions, paid from one side to the other to keep the perp tethered to the underlying. It nets to zero across longs and shorts at the index level, and it never applies to the conditional-market family.

Probabilities and the two binaries ​

  • Price = probability. A prediction binary's price expressed in dollars is its market-implied probability. Read $0.65 as "the market prices this outcome at about 65%."
  • Implied, not objective. This is the market-implied probability — what trading currently reflects — not a claim about the true odds.
  • The pair sums to ~$1, except on Void. Under a YES or NO resolution, the YES and NO binaries together are worth about $1. Through a Void they are both worth $0, and the sum collapses to $0.

Marks, oracles, and "two prices" ​

  • Two distinct marks, by design. A perp has a risk mark (oracle-based) that drives margin, equity, and liquidation, and a separate funding mark (derived from recent trade activity — a trade-price EWMA) that drives only funding. They can diverge, and that is intended.
  • The underlying anchors the family. Within a conditional-market family, the underlying perp's oracle is the only continuous external feed; the conditional legs are valued off their own book activity and consult the underlying only for margin and at settlement.

Time and resolution ​

  • Perpetuals have no expiry. A perp position stays open until you close it or it is liquidated; funding is what keeps it priced to the underlying over time.
  • Conditional markets resolve once. A family runs until its event resolves (YES, NO, or Void), at which point all of its books settle or void together in one step. A conditional-perp-plus-underlying-perp pairing hedges within the branch that fires; a fully matched box stays hedged across every branch, including a Void. Standard practice approaching resolution is to be solvent in the post-resolution world — flatten or fully box your positions before an event resolves.

How to read the numbers in this corpus ​

  • Illustrative unless stated otherwise. Every worked figure — prices, probabilities, margins, basis points — is an example chosen to make a mechanism clear. None of them are live or canonical market values.
  • Generic examples only. Examples use placeholder assets and events ("an asset," "asset-PERP," "a scheduled economic decision," "a price-threshold event"). Specific live markets, tickers, and dates are out of scope here.
  • Identities are relationships. Wherever an equation appears, it describes how fair prices relate, not a rule the engine enforces. The engine matches orders and checks margin; it does not pin books to the identities.