Formal Verification Certificate
All theorems formally verified in Lean 4 with zero sorry gaps.
Tensor Logic + Homology • Lean 4 + Mathlib • Apoth3osis Labs
The Central Question
Can logic programs compute homology? This project shows that Datalog-style programs evaluated over F₂ (XOR) semantics naturally encode chain complexes. Simplicial data enters as facts, boundary maps emerge from rules, and fixpoint iteration yields cycle and boundary spaces. Gaussian elimination over GF(2) then extracts Betti numbers. The entire pipeline — from TSV input to topological invariants — is formally verified in Lean 4.
Simplicial TSV Input: vertex/edge/triangle facts
|
AST Parser Logic program construction
|
┌────┼────┐
│ │ │
Bool Fuzzy F₂ Three evaluation modes
│ │ │
└────┼────┘
|
Chain Complex F₂ boundary maps: ∂ₖ
|
Gauss Elim (GF2) RREF, pivot tracking
|
Betti Numbers rank(Zₖ) - rank(Bₖ)Three Evaluation Modes
Boolean
Standard Datalog: true/false fixpoint iteration. Classical deductive database semantics.
Fuzzy
Real-valued [0,1] propagation. Soft inference for probabilistic reasoning.
F₂ (XOR)
Parity semantics encoding homological information. Chain complexes via XOR boundary maps. This mode computes Betti numbers.