Libertaria Proofs

Machine-checked proofs for Libertaria governance mechanisms.

The first governance system in human history with formally verified capture resistance guarantees.

---

Overview

This repository contains Lean4 formalizations of Libertaria's governance primitives:

• Reputation dampening (Tier 1 proofs - complete)
• Dual-Delegation capture bounds (Tier 2 proofs - in progress)
• Exit composition theorem (Tier 3 proof - the prize)

Quick Start

# Clone and enter directory
cd libertaria-proofs

# Install dependencies (requires Lean 4)
lake update

# Build the project
lake build

# Run tests
lake test

Project Structure

libertaria-proofs/
├── Libertaria.lean                 # Main library entry
├── Libertaria/
│   ├── Core/
│   │   ├── Types.lean             # DID, Chapter, Mechanism types
│   │   └── Graph.lean             # QVL trust graph definitions
│   ├── Governance/
│   │   ├── Dampening.lean         # ✅ DAMP-CEIL, DAMP-CONSERVE
│   │   ├── DualDelegation.lean    # ✅ DD-CAPTURE-R3 (0.359 bound)
│   │   ├── Vickrey.lean           # ✅ VICK-TRUTH (dominant strategy)
│   │   ├── Conviction.lean        # ✅ CONV-ASYMP (asymptotic properties)
│   │   ├── Delegation.lean        # ✅ DELEGATION-DAG (acyclicity)
│   │   └── Exit.lean              # 🔴 EXIT-AMPLIFY (the prize)
│   └── Properties/
│       └── CaptureResistance.lean # Top-level theorems
├── Tests/
│   └── Main.lean                  # Test runner
├── doc/
│   └── specification-cards.md     # Property catalog
└── lakefile.lean                  # Lean package configuration

Status

Property	Status	Complexity	Notes
DAMP-CEIL	✅ Proven	Trivial	min_le_right
DAMP-CONSERVE	✅ PROVEN	Trivial	simp [add_sub_cancel']
DD-CAPTURE-R3	✅ PROVEN	Moderate	RFC-0310 v0.2.0: 0.359 bound, Lottery Inheritance
VICK-TRUTH	✅ PROVEN	Moderate	Dominant strategy via case analysis
CONV-ASYMP	✅ PROVEN	Moderate	Asymptotic + monotonicity + limit
DELEGATION-DAG	✅ PROVEN	Moderate	Acyclicity via depth increase
EXIT-AMPLIFY	🔴 Open problem	Hard	The Prize

Completed Proofs (2026-02-13)

6 major properties formally verified:

• DAMP-CEIL + DAMP-CONSERVE: Reputation dampening is correct (ceiling + conservation)
• DD-CAPTURE-R3: Dual-Delegation capture bound ≤ 0.359 with structural guarantees
• VICK-TRUTH: Truthful bidding is dominant strategy in Vickrey auctions
• CONV-ASYMP: Conviction voting asymptotic properties (monotonicity, limit)
• DELEGATION-DAG: Delegation graph acyclicity via depth-bounded argument

The Exit Composition Theorem

The crown jewel of this project:

For any governance mechanism M with capture probability P_c(M), adding costless exit with portable reputation produces a composite system with capture probability P_c(M + Exit) ≤ P_c(M) × (1 - e × p).

If proven, this establishes that exit is a universal capture resistance amplifier – the mathematical formalization of RFC-0650's "votes are noise, exits are signal."

References

• RFC-0310: Dual-Delegation Protocol
• RFC-0315: Governance Graduation Protocol
• RFC-0316: Governance Mechanism Evaluation Standard
• RFC-0650: Exit Arbitrage
• Diehl (2024): "Verified Auctions in Lean4"

License

LSL-1.0 (Libertaria Sovereign License) - See LICENSE file

Contributing

This is research-grade formal verification. The final frontier:

• EXIT-AMPLIFY: The crown jewel - population dynamics proof

---

Status: Phase 1 Complete - 6 of 7 core properties proven

Goal: The first governance system with machine-checked capture resistance proofs.