PCN Feasibility Program
The Central Question
When can a payment actually be routed through a payment channel network? The answer is not just about finding a path — it's about graph-theoretic feasibility. A payment succeeds if and only if every cut separating sender from receiver has sufficient capacity. This transforms routing from heuristic pathfinding to a mathematically complete characterization of what payments are possible, with the total network capacity preserved under any rebalancing.
Original Researcher
Lightning Network Research. arXiv 2021, 2022.
Scientific Context
Payment channel networks (PCNs) like the Lightning Network enable off-chain Bitcoin transactions by routing payments through chains of pre-funded channels. The central challenge is determining which payments are feasible — which ones can actually be routed given the current channel capacities.
The key insight: Feasibility is characterized by cut conditions: a payment from sender to receiver of amount a is feasible if and only if for every partition of nodes separating sender from receiver, the total capacity of crossing edges is at least a. This is the Hall-type completeness theorem for PCNs.
What formalization provides: The wealth feasibility check wealth_feasible(v, a) := wealth(v) ≥ a is proved as a necessary condition. Cut completeness gives the full characterization. Rebalancing invariance ensures the total network capacity is conserved. The EVM seam theorem bridges off-chain state to on-chain smart contract settlement.
Layer 1: The Mathematical Ground Truth
A channel graph G = (V, E, cap) consists of nodes (wallets), edges (payment channels), and a capacity function assigning each channel its current balance.
- wealth(v): sum of capacities of all channels incident to v
- cutCap(S): sum of capacities of edges crossing partition S
- totalCap(G): sum of all edge capacities (invariant under rebalancing)
- wealth_feasible(v, a): wealth(v) ≥ a (necessary condition)
The cut completeness theorem provides the full characterization: a payment of amount a from s to t is feasible if and only if every s-t cut has capacity at least a:
- cut_completeness: feasible(s,t,a) ↔ ∀ S. s ∈ S ∧ t ∉ S ⇒ cutCap(S) ≥ a
- hall_completeness: Hall matching condition for multi-path
- rebalancing_invariance: totalCap before = totalCap after
- seam_theorem: off-chain state ↔ on-chain settlement
Basic.lean — Cap type alias, channel graph foundations
Cuts.lean — cutCapacity, partition-crossing edge sums
CutCompleteness.lean — cut_completeness characterization
SeamTheorem.lean — EVM settlement correctness bridge
Project Phases
Complete formalization across 42 modules: channel graph basics, wealth feasibility, cut capacity, rebalancing invariance, Hall completeness, cut completeness, and EVM seam theorem. All theorems proved without sorry/admit.
- ▸wealth_feasible: sender capacity ≥ payment amount
- ▸cut_completeness: feasibility ↔ all cuts sufficient
- ▸rebalancing_invariance: total capacity is conserved
- ▸seam_theorem: EVM settlement correctness
Faithful translation to verified C (gcc -Wall -Wextra -Werror: 0 warnings) and safe Rust (cargo test: 4/4 pass). ChannelGraph, wealth, cut, and total capacity functions faithfully translated.
- ▸gcc -std=c11 -Wall -Wextra -Werror: PASS
- ▸cargo build: 0 warnings
- ▸cargo test: 4/4 pass
- ▸ChannelGraph struct matches Lean specification
All artifacts content-addressed and pinned to IPFS. Lean proofs, verified C, safe Rust archives with CIDv1 identifiers.
- ▸Lean archive: 6 key source files (19.7KB)
- ▸C archive: 1 translation unit (1KB)
- ▸Rust archive: 1 source file + Cargo.toml (1.2KB)
- ▸SHA-256 content hashes for all archives