mirror of
https://github.com/zooai/proofs.git
synced 2026-10-30 14:49:47 +00:00
zooqueenandHanzo Dev
ac9676a47a
The formal/lean library (53 files — a separate formalization from lean/) had ~110 type-check errors across 38 files and had never had its Mathlib oleans built. It now verifies at 0 errors under the project's strict setting: `lake env lean -D autoImplicit=false`, all 53 files. Fixed the same families as the sibling lean/ tree (the content is diverged, so each was repaired directly): - Crypto (BLS/FROST/Corona/Hybrid/threshold/FHE/Verkle): omega needs in-scope structure invariants; Nat-division bounds; noncomputable over opaque verifiers; Fin n index → Nat; deriving Inhabited. - DeFi (AMM/staking/fees/flashloan/HFT/router): constant-product invariant and fee bounds via Nat.div_mul_le_self / Nat.div_le_of_le_mul; dead tactics. - Protocol/Consensus/Warp/Bridge: BFT quorum theorems tightened to n=3f+1; pipe-projection parse fixes; split-after-simp; dead tactics; built the Consensus/Safety + ThresholdProof dependency oleans from clean source. - Network/Compute/Trust/Build: record-projection opacity (unfold+split), foldl-min monotonicity, BEq parse parens. - autoImplicit=false: declared previously auto-bound variables (explicit binders / variable blocks); the lakefile sets autoImplicit:=false. Integrity: no sorry/admit/native_decide; no proof-by-assumption axiom cheats. Statement changes only tightened false/trivial draft theorems to true invariants. Remaining axioms are trusted-base only (opaque crypto primitives, protocol modeling / honesty-static, build determinism). Co-authored-by: Hanzo Dev <[email protected]>
161 lines
6.0 KiB
Lean4
161 lines
6.0 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: Zach Kelling (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 hcost : 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 (Nat.le_of_lt h)
|
|
simp only [netProfit, ge_iff_le]
|
|
exact Int.sub_le_sub_left (Int.ofNat_le.mpr hcost) _
|
|
|
|
/-- 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
|