The first post in this series briefly said that the bind-verify-commit synchronization cycle eliminates structural OEV (oracle extractable value) by design, and promised a separate treatment (Mechanized Proofs for Atomic Cross-Domain State Synchronization). The second post ended similarly: atomic binding changes the structure of extraction opportunities around discrete updates, and the question stayed outside its scope (A Mechanized Functor Tower for Cross-Domain State Preservation). Here we take up that deferred question. That earlier shorthand was too broad without its bound-action scope. The mechanized basis is unchanged, and nothing new is claimed as a theorem. We add the deferred architectural argument: where OEV lives, how discrete and synchronized updates change its window, and why window closure is independent of sequencing. The argument stays paired: why separate publication and consumption create an extraction state, and how atomic binding makes that state unreachable. For bound actions, the conclusion is explicit: the update-structured time component of OEV is eliminated. We keep the line between what is proved, what is design reading, and what is not established.
1. The window in discrete oracle updates
Oracle extractable value has converged on a standard definition: the subset of MEV that arises because an oracle posts an update onchain. The mechanics behind it are equally standard. A price feed updates when a deviation threshold is crossed or a heartbeat expires, so the onchain value is a sparse sample of an offchain signal. When an update lands, its consequences, liquidations first among them, execute after it, in separate transactions that anyone can race for. Two timestamps define the core exposure: the moment the update becomes publicly observable onchain and the moment its consequence is consumed. The interval between them is the internal extraction window. A second interval sits in front of it, between the offchain fact and the update that reflects it, in which the pending update is foreknowable; call it the pre-window. The common OEV cases treated here arise in one of these two intervals or from control over when an eligible update becomes public.
These timing effects have been measured rather than merely postulated. A recent measurement study of one major feed family found that the same offchain price lands at measurably different times on different chains, one chain’s update leading the others by nineteen to twenty-seven seconds on average, Ethereum included, and that on its measured day 39% of successful liquidations across three rollups were speculative, executed against a predicted update rather than a landed one (Sevim and Ferreira Torres 2026). On scale, extractable value of all forms measured on Ethereum over thirty-two months exceeded 540 million dollars (Qin, Zhou, and Gervais 2022); that figure is a broad extraction anchor rather than an OEV estimate, and the canonical OEV instance, the liquidation raced around an update, sits inside it.
What the literature has not stabilized is a taxonomy. Standard MEV taxonomies classify liquidation as a category of extraction and leave the event that creates the opportunity, the oracle update, off the classification axis entirely (Materwala et al. 2024). The update is treated as weather. Section 3 proposes the missing axis; the next section first fixes what current mitigation changes and what it keeps.
2. What auctions change, and what they keep
Two distinct auction designs are in play around extraction, and they should not be conflated.
The first attaches an order-flow auction to a price feed. The feed is wrapped or dual-pathed; the right to execute immediately against the update is sold by sealed bid; a share of the winning bid is returned to the protocol that hosted the opportunity. This class is deployed, and it deserves credit for converting a gas race into a priced allocation on infrastructure that exists today. What it keeps is the window itself. The update remains an event distinct from its consumption, so the internal window of section 1 still exists; it is now monetized rather than open. The auction adds latency on the critical path, and that latency has a documented price: in one large lending market’s governance process, risk providers recommended raising liquidation bonuses by half to one percentage point specifically to compensate for the added delay, a cost that lands on the borrowers being liquidated (governance record). Attribution is unresolved in principle, since a single update can create opportunities across many venues at once, and no rule decides whose recapture it is (early design discussion). A thin auction can create an additional strategic surface: the expansion review notes that a monopolist liquidator may abstain from bidding and induce the fallback path when that timing serves it better (expansion review). None of these are engineering accidents. They are what pricing a window looks like when the window stays.
The second design comes from market design: a commit-reveal batch auction with uniform clearing that removes intra-batch ordering privilege instead of selling it. In WGlynn’s VibeSwap post, the distinction I kept returning to is that batch auctions remove the ordering surface rather than relocate it; the same post marks the mechanism as implemented but not yet proven in adversarial production at scale, a claim discipline this series shares (WGlynn 2026). We apply that distinction to a different channel. Ordering is one extraction precondition; reference-state staleness, the one that defines OEV here, is another. An auction that reprices the stale interval has not touched that precondition; a design that removes the interval has. That doesn’t make the auction ineffective. It solves allocation rather than structural closure.
The pattern is older than this ecosystem. Mutual funds once computed net asset value once a day at stale closing prices; the predictability was worth double-digit annual returns to timers, and the industry’s mitigations, short-term trading fees and monitoring, proved only partly effective, tending to shift the activity toward funds that had not yet adopted them (Zitzewitz 2003). Discrete valuation against a continuous world creates a window wherever it appears, and pricing a window has a long record of being easier than closing one.
3. Three timing surfaces and one control precondition
Where exactly does the value sit, why does it exist, and what would remove it? We can separate three timing surfaces and one conditional control precondition:
- Update-timing extraction. The update transaction is public before its consequences execute. Backrunning it is the canonical OEV trade, and it is the surface the order-flow auctions price.
- Update-anticipation extraction. Thresholds and heartbeats make the next update statistically predictable from offchain data, so the race moves into the pre-window, ahead of the update it ultimately consumes. This surface is measured: the 39% figure above is anticipation, and it bypasses any auction attached to the update it precedes.
- Cross-domain timing extraction. The same offchain fact lands at different times in different domains, so one domain’s update is a signal about another’s near future. The nineteen-to-twenty-seven-second leads above are this surface, and a single-domain auction cannot reach it.
- Publication-timing discretion, a control precondition. Where a party or quorum can delay, withhold, or selectively release an update that already satisfies the feed’s stated publication rule, that power is a timing option over everyone downstream. It is conditional rather than universal, and it is not another interval. It governs when the first three intervals open.
The first three surfaces share a load-bearing feature: their update-structured components exist because the update is an event separate from the state change it causes. They differ only in who observes the separation first (the mempool, a statistical model, another chain). For surface 2 the update-structured component is the predictability of a separately consumable update; foreknowledge of the underlying fact itself is older than any oracle design. The control precondition is different in kind, and section 5 returns to it. The problem and the response can therefore be paired directly:
| exposure or precondition | problem: why value exists | feed-attached auction | atomic state binding: how the update-structured component closes |
|---|---|---|---|
| 1. update-timing | the update becomes visible before its consequence is committed | prices and redistributes the race; keeps the window | commits the update and bound consequence in one transition, leaving no separate update event to backrun |
| 2. update-anticipation | a threshold or heartbeat makes a separately consumable future update predictable | is bypassed because extraction precedes the auction | removes the separately consumable update to anticipate; pre-bind knowledge of the underlying fact remains outside the claim |
| 3. cross-domain timing | one chain observes the same fact before another | is out of reach of a single-domain auction | writes the posterior state to every connected chain in one transition |
| publication-timing discretion | a party or quorum can choose when an otherwise eligible update becomes public | does not address the authority | does not by itself remove the authority; governance addresses pre-submission discretion, and sequencing addresses only post-submission inclusion |
Closure entries in the right column are model-level design claims bounded by section 6.
One more distinction bounds everything that follows. The cross-domain MEV literature separates extractable value into an intrinsic component and a time component, the value of being able to wait and see, and notes that the time component collapses into the intrinsic one as the time to act goes to zero (McMenamin 2023). The update-structured components of surfaces 1 through 3 are time-component value. That is precisely the portion the next section addresses, and the only one.
4. The extraction window under atomic binding
The first post put the claim in one formula and deferred its development. For a discrete oracle, internal timing exposure accumulates over the interval between public visibility and consumption:
with v_u(t) the value at stake while update u remains separately actionable. The expression is a time-weighted exposure measure, not a dollar estimate of realized OEV, and it models the internal term only; the pre-window sits outside the closure claim developed below. Three structural facts govern it. The interval is nonempty by construction in a discrete design because consumption is a separate transaction. Auction latency adds to it, as section 2 documented. And competition does not remove it: the classic market-design result is that continuous serial processing turns even symmetrically observed public information into arbitrage rents, and that the arms race compresses reaction times by an order of magnitude while per-race profitability stays roughly constant (Budish, Cramton, and Shim 2015). Their remedy synchronizes the processing step; the object here is the reference state itself, but the diagnosis transfers whole. A neighboring monotonicity is also on record: in AMM models with discrete block times, arbitrage profit falls as the interval shrinks (Milionis, Moallemi, and Roughgarden 2023), an adjacent setting, cited as analogy and nothing more.
Now the mechanized part. In the model of this series, synchronization is a single transition:
definition sync ::
"chain_id ⇒ reg_action ⇒ asset_id ⇒ global_state ⇒ global_state option"
The body of that definition acquires a per-asset lock, checks the transition’s validity, writes the posterior state to every connected chain, and releases the lock, all inside one step; failure at any point yields None, so no partial state exists. Two theorems carry different parts of the argument. The isolation theorem is stated over the generic sync_all construction; the agreement theorem is proved over the concrete regulatory sync:
theorem sync_isolation:
assumes "sync_all source action aid domain_state = Some ds'"
and "aid' ≠ aid"
shows "ds' d aid' = domain_state d aid'"
theorem regulatory_homomorphism:
assumes current: "get_reg_state gs source aid = Some s"
and trans: "reg_transition s action = Some s'"
and synced: "sync source action aid gs = Some gs'"
and connected: "c ∈ connected_chains gs aid"
shows "get_reg_state gs' c aid = Some s'"
The first establishes per-asset isolation: a synchronization on one asset leaves every other asset unchanged in every domain. It shows that synchronization need not become a global stall; it does not itself prove window closure. The second establishes cross-domain agreement in the regulatory instance: after a successful sync, every connected chain reads the same posterior state, which closes the update-structured component of surface 3 at the transition relation. A third theorem, valid_state_preservation, shows global validity surviving the step. These are model-level theorems from the two previous posts, at the same pinned commit.
One update delivered to three chains: the measured staggered arrivals of a discrete feed, against the modeled single transition that writes every connected chain.
Read against section 1, the consequence is structural. Within the model there is no reachable state in which the update has landed and its bound consequence has not, because they are not two events. For a bound action there is no separately observable update transaction, no interval in which the chain knowingly lags the fact it is about to consume, and so nothing for the update-structured components of surfaces 1 through 3 to inhabit inside the bound transition. In compact state-space notation:
This notation is a design reading of the mechanized transition structure, not an additional Isabelle theorem. It states the elimination claim directly: the state set that the internal extraction strategy would need is empty. Two clarifications pin down its scope.
First, emptiness is not a claim about elapsed time. A cycle’s physical execution takes however long it takes. What the transition structure removes is every reachable state in which the update is visible and its bound consequence is not, and extraction needs such a state to act in. The window is not shortened; it is unrepresentable, in the same sense in which the previous post’s transition relation rejects legally meaningless transitions rather than filtering them at runtime.
Second, the claim carries a closure condition. It covers what the bound transition’s write set covers. A consumer that reads the posterior state but was not bound into the transition reacts after commit, at the boundary between bound and unbound state; that boundary is a real place, and section 9 returns to it.
The two windows of a discrete update, and the bound transition whose extraction-state set is empty; pre-bind foreknowledge stays outside the claim.
Three qualifications keep the claim at its correct strength.
What vanishes is the update-structured time component. In the vocabulary of section 3, binding eliminates the waiting value for the bound action; whatever is intrinsically mispriced at the instant of binding is untouched, and nothing here makes a chain’s whole world-view continuously fresh. In particular, binding removes threshold- and heartbeat-driven anticipation of a separately consumable update; it does not by itself erase foreknowledge of the underlying fact before binding begins. That pre-window exposure is not an update-structure problem, and no update design closes it. The claim covers the bound action, and only that. Within this scope, elimination is the correct word: the opportunity is not repriced, assigned, or made harder to win; the state in which it can be exercised is absent.
Binding state is not bundling execution. Current mitigation stacks also produce atomic artifacts: the update and the winning searcher’s execution land in one transaction. The update event still exists there as a discrete, auctionable fact, and the bundle binds an execution to it. Here the binding is between the state transitions of the two domains themselves, so there is no residual update event to sell. Selling the right to act on a state change and removing the gap in which that right has value are different operations. Only the second is elimination.
Atomicity is not an extractor subsidy. Skepticism about atomic execution is on record in a neighboring setting: in shared-sequencer models, atomicity does not by itself increase an arbitrageur’s profit (Silva and Livshits 2024). That result concerns whether atomicity helps the extractor. The claim here concerns whether the interval hosting the extractor exists. The two are compatible, and the skepticism cuts in this argument’s favor.
One boundary condition belongs in the main text rather than the fine print: the window stays closed only while synchronization actually runs as modeled. A deployment that batches synchronization on a cost-driven cadence reintroduces a discrete interface at that cadence. Section 9 returns to this as an open economic question.
5. Sequencing honesty does not close the window
The first post promised this separation explicitly. Ordering policies, fair ordering, encrypted mempools, time-priority auctions, and batch clearing govern who acts first among transactions contending inside a window. They discipline the race. The window is indifferent to them, because it is a property of the interface between an update and the state consuming it, not of the order in which contenders are processed. A definitional way to see this: MEV is formalized over an adversary’s freedom to reorder, insert, and drop transactions (Bartoletti and Zunino 2023). Ordering discipline constrains how that freedom is exercised. Atomic binding changes the interface so that, for bound actions, the freedom has no object left to act on. Publication-timing discretion is separate again. Governance and authorization address who may withhold an eligible update before submission; sequencing can address inclusion or censorship only after submission. Neither should be credited with the closure grounded in the state-transition structure.
The mechanization keeps the two concerns apart, which is why the separation can be stated with confidence. The consensus-progress layer proves deterministic selection (select_highest_deterministic), bounded waiting (starvation_bound), and completion (eventual_completion) under a Byzantine census assumption and stated fairness assumptions. The preservation layer proves the transition-structure results of section 4 and does not appeal to sequencer honesty for them. The two layers live in different locale hierarchies composed by assume-guarantee, as the first post described. The attribution runs in both directions: a perfectly honest, fully decentralized sequencer running discrete updates does not by itself close the update-structured timing surfaces 1 through 3, and closing those surfaces claims nothing about who should sequence or how. Where the two layers meet is liveness, not window structure: progress guarantees are what make cycle completion more than a hope, and they are the consensus layer’s contribution, under its stated assumptions.
The two locale hierarchies of the mechanization: progress guarantees discharge liveness assumptions, and window structure lives in the preservation layer.
6. What is proved, what is design reading, and what is not established
| Proved in the mechanization | Design reading | Not established |
|---|---|---|
single-transition synchronization with in-transition locking and an all-connected-chains write (sync); per-asset isolation (sync_isolation); cross-domain agreement after sync (regulatory_homomorphism); validity preservation (valid_state_preservation); deterministic selection, bounded waiting, and completion under stated Byzantine and fairness assumptions; category structure of preservation maps; naturality of breadth-forgetting; the two-sided admission pair (over_provisioning_guarantees, no_downward_safety) |
the empty extraction-state set as an information-asymmetry claim about deployments realizing the modeled cycle; the three-surface taxonomy and control-precondition mapping; the characterization of feed-attached auctions as pricing rather than removing the window; the protocol-economics consequences of section 7 | refinement from the model to any implementation; any empirical claim of measured zero OEV in a deployment; behavior under partial synchrony (the model is synchronous); the cost side of continuous synchronization; anything about price-feed oracles serving market-data use cases, which lie outside the state-synchronization category treated here |
All theorems are model level, at the pinned public commit in the artifacts section, from a sorry-free build.
7. Why this matters for protocol economics
The window is already priced. An auction market for the right to act inside it exists, and its revenue is an observable proxy for what bidders will pay for access, not a complete measure of total OEV. Protocol parameters can carry the same risk indirectly. Liquidation bonuses can contain an extraction- and latency-risk premium, and the empirical liquidation literature has observed that liquidation design over-compensates liquidators at borrowers’ expense (Qin et al. 2021). Removing the window for a bound asset class could therefore support repricing those parameters; the governance record of section 2 shows the same lever moving in the opposite direction when latency was added.
For the strongest synchronization classes the stakes go beyond cost. The previous post’s admission pair types which assets require processing at or above their declared degree. Where a deployment maps regulatory actions to its strongest operational synchronization class, a visible-but-unconsumed update becomes a correctness defect rather than merely a cost line: an enforcement action sitting in a window invites extraction against the enforcement itself. The boundary runs the other way too. Assets that tolerate eventual consistency do not need window closure, and nothing here argues for paying a synchronization cost where a discrete feed and a priced auction serve well. The graded model of the previous post gives that boundary a type; this post gives the type an economic reading.
8. Artifacts
- Mechanization:
Cross_Domain_State_Preservationsession, Isabelle/HOL, sorry-free build; theories includingState_Preservation.thy,Regulatory_Instance.thy,Priority_Resolution.thy,Functor_Laws.thy,Hierarchy.thy(repository at commitaafdcf327cce0dbfed4e9123dfe3f46ef786d028). - Paper: The Cross-Domain State Preservation Functor: A Mechanized Theory of Regulatory State Synchronization in Isabelle/HOL, v3.
- The two previous posts are linked in the opening paragraph.
9. Open questions
These are directions under active exploration, and community perspectives are the reason for posting them here.
- Partial synchrony. The model is synchronous. Which part of the window reopens under partial synchrony, and what bounds it? Is the reopened interval an analyzable function of message-delay bounds, or does it reintroduce anticipation extraction wholesale?
- Measuring structural absence. Recapture markets provide an observable proxy for access to the window. What would falsify a claim that the window is absent by construction in a live deployment, and what telemetry would a skeptic accept as evidence of absence rather than of quiet?
- The economics of continuity. Closing the window is not free. A deployment that batches synchronization on a cadence reintroduces a discrete interface at that cadence, so the guarantee is only as continuous as its operation. Where is the per-asset-class break-even between the OEV borne under a discrete feed and the cost of keeping windows closed?
- Extraction at the composition boundary. Recent discussion here refines extraction conservation to hold over open preconditions rather than over channels: closing a surface relocates value, closing a precondition reduces it (Extraction Is Conserved: From MEV to GEV). Atomic binding claims to close the staleness precondition for bound actions. If timing extraction then reappears where bound and feed-priced assets interact, the refined claim says that is evidence the precondition stayed open at the composition boundary, not that closure relocated equal value. How would one measure the difference between residual openness at a boundary and genuine relocation?
- Degree-typed exposure. Can declared synchronization degree double as a typed measure of residual extraction exposure, so that the admission rule of the previous post also classifies extraction risk?
10. Conclusion: when elimination is the right word
The argument reaches a stronger conclusion than mitigation, but a narrower one than universal OEV absence. For any action whose update and consequence are included in the same all-or-nothing synchronization transition, the update-structured time component of OEV is eliminated in the model. The reason is not that the race becomes fairer or less profitable. The reason is that the reachable state the race requires, update visible and bound consequence not yet committed, is absent. Surface 1 has no update transaction to backrun, surface 2 has no separately consumable update to anticipate, and surface 3 has no staggered connected-chain write to exploit.
That is structural elimination for the defined object, not a euphemism for mitigation. The boundary is model level and the bound write set; pre-bind knowledge, unbound consumers, and publication authority remain outside it. One operational condition bears repeating, because the guarantee is only as continuous as the operation carrying it: a deployment that batches synchronization back into discrete ticks reopens the window. Where the modeled bound transition is realized, there is no internal update-to-consumption window to price, allocate, or race through. That is the claim the title makes.