mirror of
https://github.com/zooai/proofs.git
synced 2026-10-30 14:49:47 +00:00
zooqueenandHanzo Dev
d3bff5e2dc
The lean/ proof library (88 files) had ~180 type-check errors across ~45 files plus 31 proof-by-assumption axiom cheats. It now type-checks cleanly under Lean 4.14.0 + Mathlib, with every theorem genuinely proven from definitions. Errors fixed: - Stale Mathlib imports: Data.Nat.Basic / Data.Int.Basic were removed this rev -> Data.Nat.Defs / Data.Int.Defs (57 files). - Shared AI/Agent/Governance/Contract/DeFi/Ecology draft files: same proof-rot as the zoo-labs sibling library (now reconciled): omega missing in-scope bounds, dead tactics after simp, simp over-reduction, doc-comment placement, reserved-word binders, deriving Repr on Finset-bearing structs, noncomputable defs over opaque primitives. - Consensus/Liveness: collapsed a 74-error cascade (undefined shared state model inlined from Safety.lean; the |>. pipe-projection vs comparison parse trap on 14 lines rewritten to explicit dot projection). - Crypto (BLS/FROST/Corona/Hybrid/threshold/FHE), Consensus, Protocol, Warp, Trust, GPU, Compute, Network, DeFi: brought structure invariants into scope for omega, Nat-division bounds via Nat.div_le_of_le_mul / Nat.div_mul_le_self, noncomputable over opaque crypto ops, deriving Inhabited for index access. Integrity: - Removed all 31 `theorem X := X_ax` cheats (axiom asserting the identical statement) and proved each from definitions; removed the UNSOUND content_addressed axiom (hash-injectivity over a struct with free fields). - Quorum-intersection theorems (BFT/Quasar/Flare/Warp/BLS/GPU/Bridge): the draft hypothesis 3f<n is insufficient (n unbounded above makes them false); tightened to the optimal-resilience invariant n=3f+1 / 2t>n. Statement intent preserved. - Net axiom change: -35 / +1 (the one addition, honesty_static, is a fixed-validator-set modeling assumption matching sibling files). - Remaining axioms are trusted-base only: opaque crypto primitives (groups, pairings, hardness, hashes, FHE encrypt/decrypt, BLS soundness, forward secrecy, Fisher-Yates uniformity) and protocol modeling assumptions. No sorry/admit/native_decide. Verified all theorems trace to [propext, Classical.choice, Quot.sound] plus those primitives. Co-authored-by: Hanzo Dev <[email protected]>
166 lines
6.1 KiB
Lean4
166 lines
6.1 KiB
Lean4
/-
|
|
Authors: Antje Worring, Zach Kelling
|
|
|
|
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
|
|
-- latency cost is monotone in RTT, so net profit is antitone
|
|
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 (Nat.le_of_lt h)
|
|
unfold netProfit
|
|
have : (latencyCost arb rtt1 : Int) ≤ (latencyCost arb rtt2 : Int) :=
|
|
Int.ofNat_le.mpr hmono
|
|
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
|