mirror of
https://github.com/luxfi/proofs.git
synced 2026-10-30 15:21:05 +00:00
zeekayandHanzo Dev
0b87d2a9f2
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. Co-authored-by: Hanzo Dev <[email protected]>
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
|