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
Resources
MENTAT Contribution Certificates
MENTAT Contribution Record
IDEA
Conceptual Contribution
CONTRIBUTION LEVEL: IDEA
Ontological EngineerPayment Channel Network Feasibility via Graph-Theoretic Constraints
Contributor
Rene Pickhardt
Independent Researcher
Core conceptual insight: the feasibility of payments in a payment channel network is determined by graph-theoretic constraints — wealth at nodes, cut capacity across partitions, and Hall-type matching conditions. A payment is feasible if and only if every cut separating sender from receiver has sufficient capacity. This transforms the routing problem from heuristic pathfinding to a mathematically grounded feasibility characterization.
MENTAT Contribution Record
THEORY
Mathematical Foundation
CONTRIBUTION LEVEL: THEORY
Ontological EngineerComplete PCN Geometry: Cuts, Hall Conditions, EVM Settlement
Contributor
Rene Pickhardt
Independent Researcher
Full mathematical framework: (1) Channel graphs with node-indexed edges and capacity attributes, (2) Wealth as sum of incident edge capacities, (3) Cut capacity as sum of crossing-edge capacities, (4) Rebalancing invariance — total capacity is constant under state updates, (5) Hall completeness — payment is feasible iff every relevant cut has sufficient capacity, (6) EVM seam — on-chain settlement correctness linking off-chain state to smart contract enforcement.
Builds Upon
MENTAT Contribution Record
PROOF
Formally Verified
CONTRIBUTION LEVEL: PROOF
Lean 4 Formalization — 42 Modules, 120+ Theorems, 0 Sorry
Contributor
Apoth3osis Labs
R&D Division
Machine-checked Lean 4 formalization of the complete PCN feasibility framework. 42 modules covering channel graph basics, wealth feasibility, cut capacity, rebalancing invariance, Hall completeness, cut completeness characterization, and EVM seam theorem. All theorems proved without sorry/admit.
Builds Upon
MENTAT Contribution Record
KERNEL
Computationally Verified
CONTRIBUTION LEVEL: KERNEL
PCN Feasibility Verified Kernel — C & Rust Transpilation
Contributor
Apoth3osis Labs
R&D Division
Verified C and safe Rust transpilations of the core PCN feasibility modules. C: gcc -std=c11 -Wall -Wextra -Werror, 0 warnings. Rust: cargo build 0 warnings, cargo test 4/4 pass. ChannelGraph, node_wealth, wealth_feasible, cut_capacity, and total_capacity faithfully translated.
Builds Upon
Governed by MENTAT-CA-001 v1.0 · March 2026