Fundamentals

The formal statements behind the design, with their proofs, their measurements, and the grade of evidence each one carries.

The companion document, Determinism as a product decision, argues the design in prose. Several of its central claims are not metaphors: they are propositions with proofs, or empirical laws with fitted parameters and falsifiable predictions. This document states them that way.

The reason to bother is that a prose claim and a theorem fail differently. "The venue never owes more than it holds" is a sentence a reader has to trust. "Payout equals escrow identically in the outcome variable" is a sentence a reader can check, and can check against the code. Claims that survive that treatment come out stronger, and section 10 records what each one rests on: proof by construction, enforcement by a checker, or measurement with a stated range.

Everything here is stated against the implementation. Where the formalisation disagrees with the narrative whitepaper, the disagreement is marked and the whitepaper is the thing that is wrong.

0. Notation

The engine is a state machine. Write S for the set of states, C for the set of commands, E for the set of events.

δ is a pure function: no IO, no clock read, no randomness, no floating point. The current time is a field on the command, assigned by the gateway before journaling, not read by δ. Write δ*(S₀, w) for the iterated application of δ along a word w ∈ C*.

Money and quantity live in ℤ. For a currency of scale d, an Amount is in minor units (10^-d of the unit). For a market with quantity scale s, a Qty is in units of 10^-s contracts. A Price is the price of one whole contract in the settlement currency's minor units. Each market carries a tick τ, a lot λ, and bounds [P_min, P_max]. Write V = P_max - P_min for the contract's full value.

Notional is the one multiplication that matters:

computed in a 128 bit intermediate, returning an error rather than a value when the division has a remainder.

Ledger states are functions L: (tenant, account, asset) → ℤ. An asset is a currency or a market's contract, so positions are ledger entries, not a separate table.

1. Replay

1.1 The transition is a function of the log alone

The content is not in the proof, which is trivial, but in the hypothesis: δ must actually be a function of (state, command) and nothing else. Every impurity, a clock read, a map iteration, a random tiebreak, silently replaces δ by a relation, and every result below collapses. That is why the book's pending delta set is sorted before emission: Go's map iteration order is randomised, so an unsorted emission would make δ a relation with 2^k branches per command.

1.2 A total order is a precondition, not an optimisation

So commands do not commute, and any deployment that admits two independent writers without agreeing an order admits two distinct legal states of the same market. That is the formal content of "matching is single homed".

Correction to the whitepaper. The narrative says active-active matching across regions "is not an engineering trade off, it is a contradiction". That overstates the case, and the honest version is stronger because it is quantitative. Active-active is possible: run consensus and pay for it. The cost is a lower bound of one inter-region round trip per command, since the order must be agreed before δ can be applied. Matching costs 1.17 µs per order (section 5). A transatlantic round trip is roughly 70 ms. The ratio is about 6 × 10⁴. Active-active matching is not impossible, it is a decision to make the cheapest part of the system four to five orders of magnitude more expensive than the part it was protecting. That is an argument a reader can check; "contradiction" is one they cannot.

1.3 Four corollaries of one proposition

1.4 What the state hash actually proves

H is SHA-256 over a length-prefixed serialisation of the ledger, walked in a canonical key order. Length prefixing makes the encoding injective: distinct states have distinct byte strings. Therefore H(S) = H(S′) with S ≠ S′ requires a SHA-256 collision.

So the migration check is not a proof of equality, it is a proof up to a collision on a hash for which none is known, at 2^-256 under the standard assumption. This is worth stating precisely rather than claiming equality, because the distinction is exactly the one an auditor will ask about, and the honest answer is comfortable.

2. Exactness: the condition under which nothing ever rounds

2.1 The grid

Admissible prices are p ∈ τ·ℤ ∩ [P_min, P_max]; admissible quantities are q ∈ λ·ℤ, q > 0. Market creation additionally requires P_min ≡ P_max ≡ 0 (mod τ).

The implemented predicate is exactly this:

so the check is necessary and sufficient, not a conservative approximation, whenever P_min ≤ τ. When P_min > τ the check is sufficient but strictly stronger than needed; it rejects some markets that would in fact have been exact. That is the right direction to err and it costs nothing, since a market with a minimum price above its own tick is not a shape anyone has asked for.

2.2 The single rounding site

Fees are a proportion and cannot be exact. The implemented rule is

that is, round half away from zero, at basis point resolution, in a 128 bit intermediate.

The consequence is the one the whitepaper claims: a rebate (β < 0) rounds by exactly the same rule as a charge, so the venue cannot extract value from the rounding convention. Among the standard rules only truncation, half-away-from-zero and half-to-even have this symmetry; half-up does not, and half-up is the default in most naive implementations.

Truncation is symmetric but biased: it loses on average half a minor unit of magnitude per fee. Half-away is unbiased except exactly on ties, where it rounds outward; half-to-even is unbiased including on ties. The residual bias of the implemented rule is therefore one half minor unit on the set of notionals where |N|·|β| ≡ 5000 (mod 10⁴), which for a notional uniform over its range is a set of density 10^-4. At USDC scale that is an expected bias of 5 × 10^-5 minor units per fee, or one cent per two hundred thousand fills. This is small enough to be a deliberate choice rather than an oversight, and stating the number is better than claiming there is none.

3. Conservation: one proof obligation instead of n

3.1 The invariant

For a tenant t and asset α define

summing over every account including the system accounts. The claim is K(t, α) = 0 at every instant, for every t and α.

The value of this proof is its shape rather than its difficulty. Conservation is not a property that each of the twenty-odd command handlers has to establish separately; it is a property of the single primitive through which all of them mutate. That turns n proof obligations into one, plus one structural obligation: that no handler bypasses the primitive.

This reframes what the invariant checker is for. It is not checking that the handlers are correct about conservation. Theorem 3.1 already settles that, unconditionally, for any handler that only uses move. The checker is checking that the theorem's hypothesis holds, that is, that nothing has written to the balance map directly. It is a guard against a future bypass, not against present arithmetic. Stated that way, running it after every command in debug builds and after every snapshot in production is obviously the right frequency: the risk is introduced by edits, not by traffic.

3.2 System accounts as mirror liabilities

A credit is not an exception to conservation. It is a transfer from sys:external, which is therefore negative by construction, and its magnitude is exactly the value the tenant asserts exists outside Clobber. The double entry reading is that sys:external carries the venue's liability to the outside world, and conservation says the books balance against it at all times.

sys:fees is permitted to be negative, which is the correct modelling of a negative maker fee: a venue running a rebate programme is paying out of its own equity, and the ledger should show that as a negative fee balance rather than refusing the configuration.

3.3 Open interest is a corollary, not a counter

Σ_{x > 0} x = Σ_{x < 0} (-x) =: OI

Long open interest equals short open interest because conservation says so, not because a counter is maintained and hopefully kept in step. This is the concrete payoff of putting positions in the ledger rather than in a table of their own: one invariant covers cash and contracts, and the quantity that collateral has to be sized against is derived rather than tracked.

4. Collateral: why the rule is a function of position

This is the section where a property test corrected the design, and the correction has an exact statement.

4.1 The collateral function

For a signed position x in a market that permits shorts:

Only short exposure is collateralised; a long already paid for what it holds. The required change on a trade of signed size δ is

read from the position before the trade. The rejected alternative, the rule that looks obviously right, is the per-trade rule Δ_naive(δ) = C(δ): buyer escrows the price, seller escrows one minus the price, per trade, regardless of what either already holds.

4.2 Exactly when the obvious rule is right

Write u = -x and v = -δ, so C(x) = V·u⁺/10^s with u⁺ = max(0, u).

• u ≥ 0, v ≥ 0: (u+v) - u = v. Holds.
• u ≤ 0, v ≤ 0: 0 - 0 = 0. Holds.
• u > 0, v < 0: left side is (u+v)⁺ - u, right side is 0, so we need (u+v)⁺ = u, which for u > 0 forces u + v = u, that is v = 0, contradiction. Fails.
• u < 0, v > 0: left side is (u+v)⁺, right side is v, so we need (u+v)⁺ = v, which forces u = 0 or v = 0, both excluded. Fails. ∎

The whitepaper says the naive rule "is right only when both sides are starting from flat". Theorem 4.1 is sharper: flat is sufficient but not necessary. Adding to a short, or adding to a long, is also safe. There are exactly two failure modes, and they are the two directions of reducing exposure:

• u > 0, v < 0, holding a short and buying. Δ_naive charges nothing for a buy, but the correct change is a refund, so the naive rule strands collateral in escrow.
• u < 0, v > 0, holding a long and selling. Δ_naive charges full short collateral V·q, but the correct change is zero while the account is still net long. The naive rule collateralises exposure that does not exist.

Both produce the same symptom the whitepaper reports, escrow holding more than the market needs, by two different routes.

4.3 The naive rule fails safe

So the discarded rule always over-collateralises and never under-collateralises. The bug found on the second generated trade could lock more of a user's money than necessary, and could not make the venue insolvent. That distinction is worth naming: it was a liveness and capital-efficiency defect, not a solvency defect. The whitepaper presents it as a design error caught before customer money existed, which is true; the sharper reading is that this particular error was in the safe direction, and the reason to still care is that an account that cannot open a position it can afford is a broken product even when the ledger is sound.

4.4 The ordering of legs is a feasibility result

Fills apply in a fixed order: release holds, pay refunds, move cash, move the position, post new collateral, charge fees. The placement of refunds before the cash leg is not a style preference.

The ordering therefore admits strictly more economically valid trades, and since all intermediate states are internal to a single command, no observer can tell the difference other than by which trades are accepted. An implementation that gets this backwards rejects trades that the ledger could have supported, and the rejection looks like insufficient balance, which is the most misleading error it could possibly produce.

4.5 The pre-trade reserve is exactly the post-trade collateral net of proceeds

A resting sell of size q at price p reserves (P_max - p)·q in settlement cash. On fill, the account must hold V·q = (P_max - P_min)·q, and it receives proceeds N = (p - P_min)·q.

So the system never asks an account to fund the part of its collateral that the trade itself is about to provide. The reserve is not a conservative approximation of the collateral requirement; it is the requirement minus the known inflow.

Price improvement therefore always leaves surplus, never a deficit, which is why a resting order can never discover at fill time that it cannot pay.

4.6 Pathwise solvency

and by the escrow invariant the escrow balance is exactly OI·V/10^s. ∎

Three things are worth saying about this.

It holds for every outcome, not on average. V_ω cancels. There is no distribution over outcomes anywhere in the argument, no expectation, no confidence level. This is the formal difference between a fully collateralised venue and a margined one: on a margined venue solvency is the statement Pr[shortfall] ≤ α under an assumed return distribution, and the assumption is where the venue's tail risk lives. Here the assumption set is empty.

It covers scalar markets for free. The proof never used ω ∈ {0, 1}; it used only that V_ω lies in the bounds and that the two payout legs sum to V. So the scalar case is the same theorem, and the "normalised inside [min, max]" language in the design docs is not a separate mechanism.

Escrow lands exactly on zero. Not approximately, and not with a residual to sweep. The escrow account is empty after settlement, and the invariant checker treats stranded escrow as a violation, which is how a rounding bug in this path would surface immediately rather than as a slowly growing balance.

5. Durability: a fitted law and what it forbids

5.1 The model

Group commit means a writer appends its bytes and then queues behind whoever is currently syncing; the batch is whatever accumulated during the previous fsync. Let k be the number of concurrent writers, F the storage's fsync latency, b(k) the effective batch size, and s the per-command serial cost outside the fsync. Then

cost per command c(k) = F / b(k) + s
throughput X(k) = 1 / c(k)

Encoding is 92 ns and matching is about 1.1 µs, so s ≈ 1.2 × 10^-3 ms against an F of a few ms: s is four orders of magnitude below F and drops out. Take c(k) ≈ F/b(k).

F is measured independently: fsync p50 of 3.93 ms on the development machine, APFS on an Apple SSD, which performs a full barrier and is unusually slow.

5.2 The fit, and the point at which it breaks

The published numbers came from two harnesses on two days and stop at k = 64. Writing this section was a good reason to extend the microbenchmark to k = 128 and rerun the whole sweep, which is a genuine out-of-sample test of a fit made on the shorter range. All six points below are one run, one machine, one day (Apple M1, APFS, 2026-08-02, -benchtime 2s), with b(k) = c(1)/c(k):

The "local exponent" is the slope of ln b against ln k between consecutive rows. A single power law would hold it constant. It does not: it climbs to 0.85 through k = 32 and then falls by half.

Fitting one power law to all six points gives

and the R² is misleading, because the residuals are not noise, they are a curve: positive at k = 32, negative at k = 128. The intercept coming out at 0.99, where theory requires exactly 1, does say the model has the right form locally; the exponent simply is not one number over the whole range.

The out-of-sample prediction was wrong, and by how much. Fitting only the previously published data (k ≤ 64, across both harnesses) gives an exponent of 0.75 and predicts b(128) = 38.1, that is, 0.104 ms per command. Measured: b(128) = 24.9 and 0.160 ms. The model overpredicts throughput at k = 128 by 54%. The three quarter power law is a good description of the range it was fitted on and degrades outside it, in the direction of the batch doing less well than hoped as concurrency rises.

Older measurements are consistent with the new sweep where they overlap, within harness-to-harness scatter of roughly 25%: 3.9 / 2.4 / 0.92 / 0.27 ms at k = 1, 2, 8, 32 from the earlier microbenchmark run, and 0.165 and 0.171 ms at k = 64 from two make perf runs against today's 0.212 ms. That 25% is the real precision of any of this, and it should be attached to every number below.

Applying Little's Law, L(k) = k/X(k), the pair of laws is

and with b(k) = k^a,

The measured latencies check out against Little's Law, which is an identity and therefore a test of the measurement rather than of the model: with earlier p50s of 3.1, 6.1 and 8.1 ms at k = 1, 8, 64 against Little means of 3.60, 6.37 and 10.59 ms, the mean sits above the median in every case, as it must for a right-skewed distribution. The measured p99s of 8.0, 13.9 and 26.1 ms give a tail factor τ = p99/mean of 2.22, 2.18 and 2.46. That τ is roughly constant in k is a small empirical finding and is used below.

Correction to the whitepaper, and to. Both say the 0.27 ms figure is what sixty four writers cost, and the whitepaper calls the improvement "a factor of twenty". Before this run the microbenchmark stopped at thirty two writers, so 0.27 ms was the k = 32 point and the factor there is 14. The factor of twenty belongs to the other harness: 278 to 6,045 commands per second between k = 1 and k = 64, a factor of 21.7. Every individual number in that sentence is measured; the pairing crossed two harnesses. The model above uses each point with its own k, which is why it fits.

5.3 What the law forbids

A durable acknowledgement cannot be faster than one fsync, at any concurrency, ever. Batching buys throughput by amortising the fsync across commands; it cannot buy latency, because every command still waits on a whole fsync. This is the arithmetic behind the documentation correction recorded in: a published promise of sub-millisecond durable acks was unreachable by construction on any storage with F > 1 ms, which is most storage. It was never a tuning question, and the model says so in one line, independently of the exponent.

and the required concurrency is k = (F·X*)^(1/a).

The exponent is not a detail here: it is the whole answer, and it enters the bound with weight a on the latency budget and 1-a on the throughput target. Applied to the published throughput target, 10,000 orders/s at p99 under 5 ms, and deflating by the tail factor τ ≈ 2.3 so that the p99 rather than the mean meets the budget:

The concurrency the gate needs does not depend on the exponent at all. At the feasibility boundary both constraints bind, so by Little's Law k = X*·L*, which for this gate is 10,000 x 2.17 ms ≈ 22 writers in flight whatever a turns out to be. The exponent decides the disk, not the gateway.

The bottom row is the one to plan against. The gate demands roughly ten thousand commands a second, which on any storage in range puts k in the tens to low hundreds, and that is exactly the region where the measured exponent is 0.42 rather than 0.75. Using the optimistic exponent because it fits the low-k data better would be fitting the model to the region the system will not operate in.

Consequences, all falsifiable, stated at a = 0.42:

• APFS at F = 3.9 ms cannot reach that target at any concurrency. Not slowly, not with tuning: the feasible set is empty, by a factor of ten. Raising k to reach the throughput pushes latency up as k^0.58 while throughput only arrives as k^0.42.
• EBS gp3, typically 0.5 to 1 ms fsync, also fails at a = 0.42, and only passes if the exponent in the operating region turns out closer to 0.75. This is the case that has to be measured rather than argued, because the two exponents disagree about it.
• Local NVMe at 0.05 to 0.1 ms clears it with room: at F = 0.1 ms the bound is satisfied by a factor of nearly four, and one command every 0.1 ms is already 10,000 a second before any batching at all.

Measured afterwards, and it holds. The prediction above was written before the target had been run on this machine. It has now been measured: 4,715 commands a second at 64 writers in flight, against the 10,000 the gate requires, so the gate fails on APFS as predicted. The independent microbenchmark agrees to within a tenth of a percent (0.212 ms per command at k = 64 is 4,717 a second), which is the closest thing to a replication available here.

Anchoring the extrapolation on the measured point rather than on the fitted constant sharpens it. Between k = 64 and k = 128 the measured throughput goes from 4,715 to 6,250 a second, a local exponent of 0.41, in agreement with the 0.42 of section 5.2. Extrapolating from the measured k = 64 point at that exponent, reaching 10,000 a second needs about 400 writers in flight, and Little's Law then puts the mean acknowledgement at 40 ms, eight times the gate's p99 budget before any tail factor is applied. The feasible set is not merely empty, it misses by an order of magnitude.

The engineering conclusion is unchanged in direction and sharper in degree than the whitepaper's: throughput is a question about how many commands share one fsync, the answer has an exponent in it, the exponent decays with concurrency, and therefore the storage choice is less forgiving than the optimistic fit suggests. Provision NVMe.

5.4 The caveats, stated up front

Nothing in the argument explains why the effective batch grows sublinearly at all, let alone why its exponent halves above k = 32. A perfectly batching implementation would give b(k) = k. At k = 128 the measured effective batch is 24.9 against a possible 128, so 81% of the available batching is going somewhere unmeasured. Candidates: contention on the append lock serialising arrivals, writers arriving after a sync has already begun and missing the batch, or an fsync whose own cost grows with the number of dirty pages, which would put a floor under the per-command cost.

One measurement since narrows this, without closing it. Driving N writers against N independent files, each fsyncing every write, saturates at about 590 fsyncs a second from 16 writers upward: on this device a cache flush is a whole device barrier, so sixteen in flight cost nearly what sixteen in a queue cost. That is a hard ceiling on fsync count, and it is worth knowing on its own, since it is why splitting the log per market would halve throughput rather than multiply it.

But it does not explain the exponent, because at k = 64 the shared log is issuing roughly 250 fsyncs a second, well under that 590 ceiling. We are not running out of fsyncs. Something else is either holding writers out of the batch or making a larger batch's fsync more expensive than a smaller one's, and those two have different fixes: the first is our append lock and would be free to recover, the second is the device and is not. On this machine the two cannot be told apart. Ten minutes with a profiler on the target hardware would settle it, and until someone spends them the honest position is that 81% of the batching is unaccounted for and one of the two explanations for it is our own code.

This matters more than a missing explanation usually does, because Proposition 5.2 is entirely a function of the exponent, and the exponent is the part with no theory behind it. All of it is one machine, one filesystem, one storage device, with harness-to-harness scatter of about 25%. The status of the hardware conclusion is prediction, not result, until it is measured on the target. It is written down anyway because it is precise enough to be wrong, which is the only kind of prediction worth publishing before the measurement, and because this section already contains one worked example of that happening: the k ≤ 64 fit predicted b(128) = 38 and the answer was 25.

6. The power of a differential test

The whitepaper's most transferable claim is that both differential harnesses passed against an engine with time priority deliberately inverted. It attributes the failure to the generator. That is half of it. The full statement needs two independent failure modes, and the second one is the more interesting.

6.1 Definitions

Let δ be the engine and δ′ a mutant. Let φ: S → O be the observation map, that is, whatever the comparison actually inspects. Let G be the generator, a distribution over command sequences.

π(R) = Pr_{w ~ G} [ ∃ n ≤ R: φ(δ*(S₀, w_{1..n})) ≠ φ(δ′*(S₀, w_{1..n})) ]

A test that cannot fail has π = 0. Passing is evidence about the engine only in proportion to π.

(a) Reachability blindness. G's support never enters the region where δ and δ′ differ. (b) Observation blindness. φ ∘ δ = φ ∘ δ′ on the reachable region: the mutation is invisible to the comparison even where it occurs.

The distinction matters because the two have different fixes. (a) is fixed by changing the generator. (b) cannot be fixed by any generator whatsoever; it needs a finer φ.

6.2 Reachability: the collision bound

Time priority is exercised only when two orders from different accounts rest at the same price on the same side. Suppose n orders rest per side, prices are drawn from a distribution p over the admissible ticks, and accounts are drawn uniformly from A. Two independent draws land on the same price with probability Σᵢ pᵢ², so the expected number of priority-bearing pairs per side is

where

is the effective width of the price distribution. For a uniform draw over W ticks, W_eff = W and the formula reduces to n²/(2W), which is the birthday bound. For anything else W_eff is strictly smaller than the nominal band, and it is W_eff, not the band, that governs.

By the Poisson approximation, the probability that a given state exercises priority at all is 1 - exp(-μ). For W_eff ≫ n² this is μ + O(μ²), so

Two things follow. Power decays as 1/W_eff, and it grows quadratically in n. The second holds only while collisions are the scarce ingredient; the appendix measures where it stops. The generator announces neither: every assertion still passes, coverage tools still report the matching path as covered, and the number of cases run can be increased without bound while the probability of ever visiting the relevant state stays fixed. This is the sense in which the original wide-band generator was "faithfully checking a book that could not have the bug".

Writing W_eff rather than W is not pedantry. The appendix measures both, and they diverge by two orders of magnitude in the harness as it actually runs.

The harnesses today use W = 5 ticks on the binary market and W = 3 on the pair market, W = 11 against exchange-core, and W = 31 in the engine property test, with A = 3 or 4.

6.3 Observation: aggregate depth is priority-blind

This is a stronger statement than the whitepaper makes, and it corrects the diagnosis. Narrowing the price band was necessary but it is not what makes that harness able to detect the inversion. What makes it able is that the divergence, once created, persists in the hidden part of the state and is lifted into φ later by an identity-dependent command: a cancel names a specific order id, and after a differently-ordered partial fill that order has different remaining quantity in the two engines, so the cancel removes a different amount and the level sizes finally disagree. The harness cancels roughly one command in four, which is why it converges at all.

So the oracle harness's power is a three-event conjunction: collision, then strictly partial consumption of the colliding level, then a later cancel touching an affected order. The naive harness compares per-order Status and Filled, so for it the divergence is immediate and the conjunction has two terms.

6.4 What was measured

Injecting the inversion and varying W turns π from an argument into a curve. The experiment ran, the theory above survived in a corrected form, and two of its assumptions turned out to be wrong in ways that matter more than the result. The numbers are in the measurement appendix below.

6.5 The rule that generalises

A differential test's power is bounded above by two independent quantities: the probability that the generator reaches the differing region, and the resolution of the observation map. Neither is visible in a passing run. Both are measurable, by the same method: inject the mutation you claim to be protected against, and count.

The corollary for anyone testing a matching engine is specific. If your comparison is aggregate depth (and most are, because aggregate depth is what an external oracle exposes), then Theorem 6.3 says your harness is structurally blind to the entire class of intra-level ordering bugs, which is exactly the class that price-time priority consists of. You are not testing priority. You may be testing it indirectly through cancels, which is worth knowing you are relying on.

7. Isolation as a property of the key constructor

Cross-tenant access is then not refused; it is not expressible. The implemented key is

BalanceKey = (Tenant, Account, Asset)

with tenant first, and every other index lives inside a per-tenant structure reached from a tenant map, so the tenant prefix is enforced by containment.

The engineering content is that n checks become one constructor. A check can be omitted from one code path by one distracted edit, and the resulting hole is invisible until someone goes looking. A key type cannot be omitted from a lookup, because the lookup does not compile without it.

That is the formal reason the engine masks cross-tenant probes as not-found. It is not politeness about error semantics; the alternative is an existence oracle, and an existence oracle over customer identifiers is precisely the leak the tenant boundary exists to prevent.

8. Feed convergence: what idempotence buys and what it does not

Book deltas carry absolute sizes, with size zero meaning the level is removed. Let a client hold B: Price → ℤ≥0 and apply a delta (p, σ) as the assignment B[p]:= σ.

Together these say precisely what the absolute-size design achieves. It makes the transport safe under duplication and under reordering across prices, which is why at-least-once delivery is sufficient and no acknowledgement protocol is needed. It does nothing at all for loss, and loss at a single price is permanently corrupting rather than transient.

That asymmetry is the entire justification for the per-market sequence number. Gap detection is not defence in depth on top of a self-correcting stream; it is the only mechanism that addresses the one failure mode idempotence cannot touch. A client that does not check seq is not slightly less robust, it is unprotected against the only error the design leaves open.

9. Terminal states

This is the same shape of argument as Theorem 3.1: one chokepoint carries the property for every handler, so there is one proof obligation rather than one per call site.

It was not true when this document was first drafted, and the way it became true is the point. Order.fill used to write o.Status directly, so the transition into filled bypassed the guard, and immutability rested on a reachability argument: only book residents are ever passed to fill, and residents satisfy IsResting(). That argument was correct. It is also exactly the kind of argument a refactor invalidates with no test noticing, which is the category the chokepoint discipline exists to eliminate, so writing it down as an exception was less useful than closing it.

One direct write survives, in the snapshot decoder, and it is deliberate: rebuilding an order from bytes is deserialisation of an already decided state, not a transition. "One writer" is therefore true of transitions, not literally of the field.

10. What each result rests on

Results in this document come in three grades, and the grade is part of the result. Some hold by construction: they are true of any execution because the code has no path that could make them false. Some hold by guard: a checker enforces them and would catch a violation. Some are empirical: they are measurements with a range of validity, and they are stated with it. Reading the document without the grades would overstate the strong ones and understate the sharp ones.

1. The state hash is a fingerprint at cryptographic strength, not an identity. Migration verifies SHA-256 equality over an injective encoding, so equality of states holds up to a SHA-256 collision. Naming the residual is what makes the guarantee legible.

2. The group commit exponent is empirical, with a stated range. b(k) = k^a is a description fitted to measurement rather than derived from a model, and section 5 shows exactly where it holds and where it stops: the local exponent climbs to 0.85 through k = 32 and then halves, so a single power law is the right form locally and not across the whole range. Any hardware conclusion drawn from it carries that range with it, which is why section 5 states the out-of-sample error rather than quoting one exponent.

3. The tail factor is empirical. τ ≈ 2.3 across three data points is what converts a mean-latency model into a p99 statement. It is stable across the data available and is used as a measured constant, not as theory.

4. Conservation is guarded, not typed. Theorem 3.1 holds for any handler that mutates only through move, and every handler does. The type system does not enforce that; the invariant checker does, after every command, and a violation fails the build rather than reaching production.

5. The snapshot decoder writes order status directly (section 9). It is deserialisation rather than a transition, so the chokepoint claim of section 9 is precisely about transitions.

6. The exactness converse assumes P_min ≤ τ (Theorem 2.2). Outside that case the implemented check is sufficient but stronger than necessary, which errs toward rejecting a market that would have been exact rather than accepting one that would not.

7. Fee rounding carries a measured residual bias of half a minor unit on a density 10^-4 subset (section 2). It is symmetric in sign, which is the property that decides whether a venue can extract value from its own rounding convention, and it cannot. The residual is quoted because a number is a better answer than a claim of none.

8. Detection power is measured per mutation, and one has been measured. The appendix injects an inverted time priority and counts. That is the standard this project holds itself to, and it is a higher one than a passing test suite: a claim that a test protects against a specific defect means the defect was introduced on purpose and the test caught it. Section 6 derives which further mutations that method applies to.

9. The collision bound is stated in W_eff, corrected from W by measurement (section 6.2). The experiment that was built to quantify the theory also corrected it, which is the outcome an experiment is for.

Appendix: measured detection power

The theory in section 6 is worth exactly as much as its measurement. This is the measurement.

A.1 Method

The mutation is a one line inversion of time priority: Book.Best returns the newest order at a price level instead of the oldest, which is the only point in the engine where intra-level order is consumed. Three unit tests catch it directly, which is the check that the mutation is real and not a no-op: TestBookIsFIFOWithinAPrice, TestPriceTimePriority, and incidentally TestOpenOrderCountSurvivesEveryExit.

The harness measured is the naive differential one, which compares per-order Status and Filled as well as aggregate depth, so by Corollary 6.4 it is the one whose observation map can see the mutation immediately. The price band was parameterised and swept. R = 100 independent repetitions per configuration, 100 rapid checks per repetition.

Three method corrections had to be made before any of the numbers meant anything, and they are more instructive than the result.

A control arm is mandatory. The first sweep widened the binary band to its full range and recorded 90% detection, which would have been a beautiful curve and completely wrong. The unmutated engine fails 18 out of 20 at that band: a binary buy limit at price 0 reserves a hold of zero, which the ledger rejects as not positive while the naive reference accepts it. That is a real pre-existing divergence and has nothing to do with time priority. Every configuration below was re-run unmutated as a control: 0 false positives out of 100, everywhere. A mutation experiment without a control arm measures the sum of the mutation and every unrelated bug in range.

That divergence has since been fixed, and fixing it revealed that the reported severity was too low: the refusal at order entry was the only thing keeping a fill at the floor price from reaching a panic. The experiment was measuring detection power and found a latent crash, which is an argument for control arms on its own.

Seeds have to be genuinely independent. rapid advances its seed cumulatively within a run, so naively spaced base seeds share check seeds at low indices, which is exactly where detections land. Base seeds were respaced 100,000 apart and the first pass discarded.

Median cases-to-first-failure is the wrong statistic, which was not obvious in advance. Regressed on band width it is essentially flat, 32 to 52 across the whole range, R² of 0.5 to 0.6. That is a censoring artifact: once the per-check detection probability falls below 1/100, a geometric variable truncated at 100 looks uniform on [1,100] and its median sits near 50 whatever the parameter is. All of the signal moves into the detection rate. The estimator used below is the censored MLE p̂ = D/(D + S), D detections and S the total surviving checks, and the geometric model checks out (at the highest-power configuration, observed mean 21.0 against 1/p̂ = 22.0).

A.2 Results

Sweeping the nominal band W, with the shipped configuration for reference:

As shipped, both markets in play: 76 detections out of 100, median 30 cases, E[cases] = 66, control 0 out of 100. The whitepaper's claim that the harnesses "now fail within a hundred cases" is correct, and the honest version of it is that they fail within a hundred cases about three quarters of the time.

A.3 The theory survives, in a corrected variable

Regressing log E[cases] on log of the band width:

Against nominal W the linear prediction of section 6.2 fails, badly on the pair market: the band widens by a factor of 3,300 and the cost of detection rises only 17 times. Against effective width it is linear, exponent 1.14 and 0.97 where theory says exactly 1, with R² of 0.995 and 0.982.

The reason is the third column of the results table. rapid's integer range generator is nowhere near uniform. At a nominal band of 10,000 ticks it produces only about 300 distinct prices, the modal price takes 10% of all draws, and the effective width saturates around 40 no matter how wide the band gets. Widening the band past roughly W = 100 buys nothing at all, because the generator will not spread out. This is why W_eff and not W is the right variable, and it is not a refinement anyone would have bothered with before seeing the data.

The n² half of the law also holds. The dimensionless group c = p̂ · W_eff / n² stays within 2.0 to 4.1 across all eighteen configurations, spanning a factor of 3,300 in nominal W. And at matched W_eff the pair market detects 2.8 to 3.7 times faster than the binary one, against a predicted ratio (n_pair/n_binary)² of 2.3 to 2.9.

A.4 The finding that outranks the curve

Instrumenting the book after every command, over roughly 36,000 snapshots per configuration:

mean resting orders per side, binary market 0.12 to 0.14
mean resting orders per side, pair market 0.19 to 0.23

Flat in W. The book is empty almost all of the time. A fifth of an order per side is nowhere near the n > 1 regime the n²/W_eff argument assumes, and it is the binding constraint on this harness's power, not the price band. Since power goes as n² and as 1/W_eff, and W_eff cannot be pushed past about 40 by any choice of band, the remaining lever is n.

That also revises the comment in the test that records the original lesson, which attributed the blindness to uniform prices over a wide range. The band does matter, 0.83 detection against 0.10 on the binary market, but the mechanism named is about a third right: the prices were never uniform, and the dominant limiter is n.

A.5 Acting on it, and where the law stops holding

The generator was changed and the experiment re-run. Three loss channels were measured first, and the one everybody would have guessed was the smallest:

The action mix dominated. A halt action drawn on a fair coin left the market shut about half the time, which nobody had counted. Immediate crossing, the mechanism the narrow band is supposed to trade against, cost only a quarter of the orders that could rest at all.

The changes: order entry split into passive quotes and aggressive takes, so entry is 40% of the stream rather than 25%; quotes priced one or two ticks off a fixed mid, the idiom the realistic flow generator already used; half the quotes two sided; halts resuming three times in four; cancels aimed at a pruned live list four times in five. Takes keep the full TIF mix, because detection needs a level consumed strictly partially and a book that only grows is as blind as an empty one.

Detection power rose 8.05 times. Runtime for the property test rose 3.5%.

And the n² law dies partway up. Three configurations give an exponent rather than a ratio: from the shipped generator to the mix-and-passive change, n rose 1.96x and power rose 3.43x, an exponent of 1.83 against a predicted 2. Adding two sided quoting, n rose a further 2.37x and power rose 2.35x: an exponent of 0.99. End to end the change bought 8.05x where n² predicted 16.95x.

The mechanism was measured rather than guessed. The fraction of samples where the best price on a side holds two orders from different accounts rose 12.9 times while power rose 8.1 times. Detection needs a taker to arrive at a contested level while it is contested, so two sided quoting raises the stock of contested levels without raising the flow of takers, and the second half of the conjunction gives back part of what the first half won. The n² bound is a statement about the collision term only; once collisions stop being the scarce thing, it stops being the binding one. Raising the taker rate is the obvious next lever and it has not been tested.

A.6 The cancel hit rate, which nobody was looking at

The number in that table that should be most alarming is not the detection rate. It is that 9.8% of the cancels the harness sent were accepted. Ninety per cent of them were refused, so the cancel path, which is where book bookkeeping is most likely to be wrong, was barely exercised at all.

The whitepaper already tells this story. It records a realistic flow generator whose first version cancelled orders that had already filled, so 97% of its cancels were refused, and draws the lesson that "a generator that mostly produces rejections is testing the rejection path and calling it coverage". That lesson was written down, and the same disease was sitting untreated in a different generator in the same package. It was found by measuring something else.

Writing a lesson down is not the same as having applied it. The only thing that distinguishes the two is a number, and nobody had taken this one.

A.7 What was not measured

• The exchange-core harness. Corollary 6.4 predicts it is strictly weaker, a three-event conjunction against the naive harness's two, and that its detections arrive only through a later cancel. That prediction is untested; running it needs the Java oracle in the loop.
• Whether a deeper book raises power against any other class of mutation. Only the time priority inversion was injected. The n² argument is specific to intra-level collisions and does not transfer on its own.
• The taker rate, which section A.5 identifies as the next binding term and does not test.
• Anything past W_eff ≈ 42. rapid will not produce a flatter price distribution, so the wide band asymptote of section 6.2 is unreachable through this generator. Testing it needs an explicit uniform draw, not a wider range.
• n during matching. The book was sampled between commands, so a level transiently holding two orders inside one match loop is invisible. The reported n is a lower bound on what matching actually sees.
• μ directly. Multi-order level occupancy was used as a proxy and is too sparse to fit on its own at these counts, which is why the fit runs through p̂.

Companion to Determinism as a product decision. Source references are to the Clobber repository at the commit this document was written against; the API contract is published at docs.clobberhq.com.