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.
102 lines
3.4 KiB
Lean4
102 lines
3.4 KiB
Lean4
/-
|
|
and Yield Protocol
|
|
|
|
Staked assets earn yield while remaining liquid.
|
|
Money at rest is put to work — implicit staking of
|
|
idle liquidity in the DEX pools.
|
|
|
|
Maps to:
|
|
- lux/node: validator staking (P-Chain)
|
|
- lux/exchange: LP staking rewards
|
|
- zoo/contracts: liquid staking derivatives
|
|
|
|
Properties:
|
|
- Yield accrual: staked assets earn validator rewards
|
|
- Liquidity: staked assets remain tradeable (liquid derivatives)
|
|
- No impermanent loss on single-sided staking
|
|
- Compounding: rewards auto-compound into staking position
|
|
|
|
Author: Lux Research (December 2025)
|
|
-/
|
|
|
|
import Mathlib.Data.Nat.Defs
|
|
import Mathlib.Tactic
|
|
|
|
namespace DeFi.LiquidStaking
|
|
|
|
/-- Staking position -/
|
|
structure Position where
|
|
principal : Nat -- original staked amount
|
|
accrued : Nat -- accumulated rewards
|
|
compounded : Nat -- rewards that have been re-staked
|
|
liquidDerivatives : Nat -- tradeable staking receipt tokens
|
|
stakeDuration : Nat -- blocks staked
|
|
|
|
/-- Yield rate: annual percentage in basis points (e.g., 500 = 5%) -/
|
|
def annualYieldBps : Nat := 500 -- 5% APY baseline
|
|
|
|
/-- Per-block yield (simplified: annual / ~2.6M blocks per year) -/
|
|
def blockYield (principal : Nat) : Nat :=
|
|
principal * annualYieldBps / 26000000
|
|
|
|
/-- Accrue one block of yield -/
|
|
def accrueBlock (p : Position) : Position :=
|
|
let yield := blockYield (p.principal + p.compounded)
|
|
{ p with accrued := p.accrued + yield
|
|
, stakeDuration := p.stakeDuration + 1 }
|
|
|
|
/-- Compound: move accrued rewards into principal -/
|
|
def compound (p : Position) : Position :=
|
|
{ p with compounded := p.compounded + p.accrued
|
|
, accrued := 0 }
|
|
|
|
/-- YIELD ACCRUAL: Accrued rewards only increase -/
|
|
theorem yield_monotone (p : Position) :
|
|
(accrueBlock p).accrued ≥ p.accrued := by
|
|
simp [accrueBlock]
|
|
|
|
/-- LIQUIDITY: Liquid derivatives equal principal (1:1 mint) -/
|
|
def mintDerivatives (p : Position) : Position :=
|
|
{ p with liquidDerivatives := p.principal }
|
|
|
|
theorem derivatives_equal_principal (p : Position) :
|
|
(mintDerivatives p).liquidDerivatives = p.principal := by
|
|
simp [mintDerivatives]
|
|
|
|
/-- COMPOUNDING: After compound, accrued resets to 0 -/
|
|
theorem compound_resets_accrued (p : Position) :
|
|
(compound p).accrued = 0 := by
|
|
simp [compound]
|
|
|
|
/-- COMPOUNDING: After compound, compounded increases -/
|
|
theorem compound_increases_base (p : Position) :
|
|
(compound p).compounded ≥ p.compounded := by
|
|
simp [compound]
|
|
|
|
/-- NO IMPERMANENT LOSS: Single-sided staking has no IL.
|
|
Unlike LP positions, staked assets don't change ratio. -/
|
|
theorem no_impermanent_loss (p : Position) :
|
|
(accrueBlock p).principal = p.principal := by
|
|
simp [accrueBlock]
|
|
|
|
/-- DURATION MONOTONE: Stake duration only increases -/
|
|
theorem duration_monotone (p : Position) :
|
|
(accrueBlock p).stakeDuration > p.stakeDuration := by
|
|
simp [accrueBlock]
|
|
|
|
/-- TOTAL VALUE: principal + compounded + accrued -/
|
|
def totalValue (p : Position) : Nat :=
|
|
p.principal + p.compounded + p.accrued
|
|
|
|
/-- TOTAL VALUE MONOTONE: Accruing never decreases total -/
|
|
theorem value_monotone (p : Position) :
|
|
totalValue (accrueBlock p) ≥ totalValue p := by
|
|
simp [totalValue, accrueBlock]
|
|
|
|
/-- MONEY AT REST: Idle liquidity earns yield.
|
|
DEX pool deposits implicitly stake via the liquid staking layer. -/
|
|
theorem idle_earns (p : Position) (_h : p.principal > 0) :
|
|
totalValue (accrueBlock p) ≥ totalValue p := value_monotone p
|
|
|
|
end DeFi.LiquidStaking
|