Apoth3osis

PCN Feasibility

Machine-checked Lean 4 formalization of Pickhardt's payment channel network feasibility theory. Wealth constraints, cut capacity bounds, Hall completeness for multi-path payments, rebalancing invariance, and EVM seam for on-chain settlement. 42 modules, 0 sorry.

42
Lean 4 Modules
120+
Theorems
0
Sorry Count
Hall + Cut
Key Results
Solidity
EVM Seam
1
C Files
4/4
Rust Tests
3
Archives
>_VERIFICATION.SEAL
FORMALLY VERIFIED • LEAN 4 • MACHINE-CHECKED • APOTH3OSIS∀∃⊢→∧∨¬≡QED120 theorems • 0 sorry42 modules0 SORRY

Formal Verification Certificate

Every theorem in this project has been machine-checked by the Lean 4 kernel. No axiom is assumed without proof. No gap exists in the verification chain.

120 THEOREMS VERIFIED42 MODULES0 SORRY

PCN Feasibility • Lean 4 + Mathlib • Apoth3osis Labs

✓KERNEL-CHECKED42 modules · 120+ theorems · 0 sorry

Key Mathematics

Wealth Feasibility

wealth(v)=∑e∋vcap(e)feasible(v,a)  ⟺  wealth(v)≥a\text{wealth}(v) = \sum_{e \ni v} \text{cap}(e) \qquad \text{feasible}(v, a) \iff \text{wealth}(v) \geq a

Lean: node_wealth, wealth_feasible

Cut Capacity

cutCap(S)=∑e∈δ(S)cap(e)(max flow≤min cut)\text{cutCap}(S) = \sum_{e \in \delta(S)} \text{cap}(e) \qquad \text{(max flow} \leq \text{min cut)}

Lean: cutCapacity, cut_completeness

Rebalancing Invariance

∑e∈Ecap(e)=const(total capacity preserved under rebalancing)\sum_{e \in E} \text{cap}(e) = \text{const} \qquad \text{(total capacity preserved under rebalancing)}

Lean: rebalancing_invariance, total_capacity

Paper ↔ Proof Correspondence

ClaimTheoremStatus
Wealth feasibility: sender has sufficient capacitywealth_feasible✓
Cut capacity bounds maximum flowcutCapacity✓
Total capacity invariant under rebalancingrebalancing_invariance✓
Hall condition for complete feasibilityhall_completeness✓
Cut completeness characterizationcut_completeness✓
EVM seam: on-chain settlement correctnessseam_theorem✓
View on GitHubLean ProofsVerified CSafe Rust
← All PPC ProjectsResearch Page →