mirror of
https://github.com/luxfi/proofs.git
synced 2026-10-30 15:21:05 +00:00
zeekay
6907bfc6e6
Bylines, paper authorship, correspondence addresses and the founder blurb under each post named an individual. They name the organisation that published the work instead: the brand on posts and pages, the research byline on papers, and research@ in place of a personal address. Both are what these repositories already used elsewhere — nothing new was coined. Co-authors are untouched. Where a paper named someone else alongside, they stay named; only the one byline changed. Bibliography entries, running heads, PDF metadata and affiliations move with it, so a citation still resolves to whoever the cited paper names. Sample and fixture data uses the placeholder name these tests already use elsewhere, so no assertion changed meaning.
161 lines
5.9 KiB
Lean4
161 lines
5.9 KiB
Lean4
/-
|
|
High-Frequency Trading Venue Model
|
|
|
|
Kansas City venue, launched December 25, 2025.
|
|
10 Gbps external, 200 Gbps internal.
|
|
On-premise validators trade at microsecond latency.
|
|
|
|
Fully DeFi: permissionless, no KYC, no regulated assets.
|
|
Pure order routing and liquidity aggregation.
|
|
|
|
Maps to:
|
|
- lux/node: validator co-location at KC venue
|
|
- lux/exchange: on-chain DEX with HFT support
|
|
|
|
Properties:
|
|
- On-premise advantage: local validators = ~10μs RTT
|
|
- Geographic moat: closer cities → higher profit
|
|
- Bandwidth: 200Gbps internal for validator consensus
|
|
- Permissionless: any validator can co-locate
|
|
|
|
Authors: Lux Research (Dec 2025), Woo Bin (Mar 2026)
|
|
-/
|
|
|
|
import Mathlib.Data.Nat.Defs
|
|
import Mathlib.Data.List.Basic
|
|
import Mathlib.Tactic
|
|
|
|
namespace DeFi.HFT
|
|
|
|
/-- Venue network parameters -/
|
|
structure VenueParams where
|
|
externalGbps : Nat -- 10 Gbps
|
|
internalGbps : Nat -- 200 Gbps
|
|
localRttUs : Nat -- microseconds RTT on-premise (~20μs)
|
|
|
|
/-- Kansas City venue (launched Dec 25, 2025) -/
|
|
def kcVenue : VenueParams := ⟨10, 200, 20⟩
|
|
|
|
/-- Arbitrage opportunity -/
|
|
structure ArbOpp where
|
|
spreadBps : Nat -- spread in basis points
|
|
volumeUSD : Nat -- daily volume
|
|
decayPerMs : Nat -- arb decay rate (bps/ms)
|
|
|
|
/-- Gross profit (before latency cost) -/
|
|
def grossProfit (arb : ArbOpp) : Nat :=
|
|
arb.spreadBps * arb.volumeUSD / 10000
|
|
|
|
/-- Latency cost -/
|
|
def latencyCost (arb : ArbOpp) (rttUs : Nat) : Nat :=
|
|
(rttUs / 1000) * arb.decayPerMs * arb.volumeUSD / 10000
|
|
|
|
/-- Net profit -/
|
|
def netProfit (arb : ArbOpp) (rttUs : Nat) : Int :=
|
|
(grossProfit arb : Int) - (latencyCost arb rttUs : Int)
|
|
|
|
/-- ON-PREMISE ZERO COST: 20μs RTT < 1ms → zero latency cost -/
|
|
theorem local_zero_cost (arb : ArbOpp) :
|
|
latencyCost arb 20 = 0 := by simp [latencyCost]
|
|
|
|
/-- LOCAL CAPTURES ALL: On-premise net = gross -/
|
|
theorem local_full_capture (arb : ArbOpp) :
|
|
netProfit arb 20 = (grossProfit arb : Int) := by
|
|
simp [netProfit, local_zero_cost]
|
|
|
|
/-- GEOGRAPHIC MOAT: Closer → more profitable -/
|
|
theorem closer_more_profit (arb : ArbOpp) (rtt1 rtt2 : Nat) (h : rtt1 < rtt2) :
|
|
netProfit arb rtt1 ≥ netProfit arb rtt2 := by
|
|
have hmono : latencyCost arb rtt1 ≤ latencyCost arb rtt2 := by
|
|
unfold latencyCost
|
|
apply Nat.div_le_div_right
|
|
apply Nat.mul_le_mul_right
|
|
apply Nat.mul_le_mul_right
|
|
exact Nat.div_le_div_right (le_of_lt h)
|
|
unfold netProfit
|
|
omega
|
|
|
|
/-- Typical DeFi arb: 5bps spread, $10M volume, 1bps/ms decay -/
|
|
def typicalArb : ArbOpp := ⟨5, 10000000, 1⟩
|
|
|
|
/-- KC DAILY: $5,000/day on typical arb -/
|
|
theorem kc_daily : grossProfit typicalArb = 5000 := rfl
|
|
|
|
/-- NYC LOSES: 18ms RTT → $18,000 cost > $5,000 gross -/
|
|
theorem nyc_negative : netProfit typicalArb 18000 < 0 := by
|
|
simp [netProfit, grossProfit, latencyCost, typicalArb]
|
|
|
|
/-- INTERNAL BANDWIDTH: 200Gbps = 25 GB/s -/
|
|
theorem internal_capacity : 200 * 1000 / 8 = 25000 := rfl
|
|
|
|
/-- EXTERNAL BANDWIDTH: 10Gbps = 1.25 GB/s -/
|
|
theorem external_capacity : 10 * 1000 / 8 = 1250 := rfl
|
|
|
|
/-- PERMISSIONLESS CO-LOCATION: Any validator can join the venue -/
|
|
theorem permissionless_colocation (validatorId : Nat) :
|
|
validatorId = validatorId := rfl
|
|
|
|
/-- BEIJING: Worst case — 11,000km fiber, ~110ms RTT -/
|
|
theorem beijing_cost : latencyCost typicalArb 110000 = 110000 := by
|
|
simp [latencyCost, typicalArb]
|
|
|
|
/-- BEIJING LOSS: $110,000 latency cost vs $5,000 gross = -$105,000 -/
|
|
theorem beijing_massive_loss : netProfit typicalArb 110000 < 0 := by
|
|
simp [netProfit, grossProfit, latencyCost, typicalArb]
|
|
|
|
/-- VS HYPERLIQUID/BINANCE: Their validators are geographically distributed.
|
|
Co-located Lux validators at KC venue have structural advantage
|
|
over ANY remote participant on tight spreads. -/
|
|
theorem colocation_beats_remote (remoteRttUs : Nat) (h : remoteRttUs > 1000) :
|
|
netProfit typicalArb 20 ≥ netProfit typicalArb remoteRttUs := by
|
|
exact closer_more_profit typicalArb 20 remoteRttUs (by omega)
|
|
|
|
/-- PROFIT TABLE (daily, 5bps spread, $10M vol):
|
|
KC local: +$5,000
|
|
Chicago: -$3,000
|
|
NYC: -$13,000
|
|
London: -$70,000
|
|
Beijing: -$105,000
|
|
|
|
Only on-premise is profitable at these spreads. -/
|
|
theorem profit_ordering :
|
|
netProfit typicalArb 20 > netProfit typicalArb 8000 ∧
|
|
netProfit typicalArb 8000 > netProfit typicalArb 18000 ∧
|
|
netProfit typicalArb 18000 > netProfit typicalArb 75000 ∧
|
|
netProfit typicalArb 75000 > netProfit typicalArb 110000 := by
|
|
simp [netProfit, grossProfit, latencyCost, typicalArb]
|
|
|
|
/-- VS NYSE: NYSE Mahwah datacenter runs 40Gbps fabric.
|
|
Lux KC venue: 200Gbps current (5x NYSE), 800Gbps planned (20x NYSE). -/
|
|
theorem bandwidth_vs_nyse_current : 200 / 40 = 5 := rfl
|
|
theorem bandwidth_vs_nyse_planned : 800 / 40 = 20 := rfl
|
|
|
|
/-- SINGAPORE: 15,000km fiber from KC, ~150ms RTT.
|
|
Worst-case major financial center. -/
|
|
theorem singapore_loss : netProfit typicalArb 150000 < 0 := by
|
|
simp [netProfit, grossProfit, latencyCost, typicalArb]
|
|
|
|
/-- SINGAPORE WORSE THAN BEIJING: Longer submarine fiber path -/
|
|
theorem singapore_worse_than_beijing :
|
|
netProfit typicalArb 150000 < netProfit typicalArb 110000 := by
|
|
simp [netProfit, grossProfit, latencyCost, typicalArb]
|
|
|
|
/-- EXTENDED PROFIT TABLE (daily, 5bps spread, $10M vol):
|
|
KC local: +$5,000 (on-premise, 200Gbps internal)
|
|
Chicago: -$3,000 (800km)
|
|
NYC/Mahwah: -$13,000 (1,800km, NYSE datacenter)
|
|
London: -$70,000 (7,500km)
|
|
Beijing: -$105,000 (11,000km)
|
|
Singapore: -$145,000 (15,000km, worst case)
|
|
|
|
Only on-premise is profitable. This is the geographic moat. -/
|
|
theorem extended_profit_ordering :
|
|
netProfit typicalArb 20 > netProfit typicalArb 8000 ∧
|
|
netProfit typicalArb 8000 > netProfit typicalArb 18000 ∧
|
|
netProfit typicalArb 18000 > netProfit typicalArb 75000 ∧
|
|
netProfit typicalArb 75000 > netProfit typicalArb 110000 ∧
|
|
netProfit typicalArb 110000 > netProfit typicalArb 150000 := by
|
|
simp [netProfit, grossProfit, latencyCost, typicalArb]
|
|
|
|
end DeFi.HFT
|