Skip to content
DraconiticResearch
Search Sources API
203,952 studies31 sourcesUpdated 52 min ago
PreprintCC BY 4.0Zenodo

Machine-Checked Simplicial Chain Complexes over F_2 and Metric Filtration Invariants for Relational Resolution Theory in Lean 4⁠

  • Ronen Weinberg1
  1. 1Independent Researcher
Open at sourcePDFDOICite

Abstract

We present a self-contained, machine-checked formalization in the Lean 4 theorem prover (Mathlib4) of the core algebraic-topological invariants underlying discrete metric filtrations in Relational Resolution Theory (TRR 3.0). Specifically, we formalize: (1) the monotonicity and downward closure of Vietoris-Rips metric filtration complexes over arbitrary types with decidable equality, (2) the ungraded simplicial chain module modeled via finitely supported functions, (3) the linearity and nilpotency (d^2 = 0) of the simplicial boundary operator, (4) the fundamental cycle inclusion (im d <= ker d), and (5) grading and subcomplex invariance. All ten theorems in the development are verified with zero unproven assumptions (sorryAx is absent) and depend solely on the standard axioms [propext, Classical.choice, Quot.sound].

The underlying algorithmic pipeline and machine-checked formalization for TRR 3.0 are strictly licensed under the GNU Affero General Public License v3.0 (AGPL-3.0). Source code repository: https://github.com/RW-101/TRR3-formalization-

Related

  1. Complementary vectors of simplicial complexes
    Matt Larson, Alan Stapledon
    Forum of Mathematics, SigmaPeer-reviewedCC BY 4.0Full text1 citedCombinatorics & discrete mathematicsCrossref
  2. Adaptive Uncertainty Quantification on Simplicial Complexes with Conformalized Simplicial Neural Networks
    Lekun Wang, Jaidev Goel, Yulia R. Gel +1
    arXivPreprintarXiv licenceFull textStatisticsarXiv
  3. Homological critical points for hypergraphs and simplicial complexes
    Shiquan Ren
    arXivPreprintCC BY 4.0Full textGeometry & topologyarXiv
  4. Simplicial Complexes of Antichains in Root Posets and Related Combinatorics of Dyck Paths
    Lili Mu, Volkmar Welker
    arXivPreprintCC BY 4.0Full textAlgebra & number theoryCombinatorics & discrete mathematicsarXiv
  5. Crossing numbers of simplicial complexes
    Alfredo Hubard, Cheikh Saliou Ndiaye, Oriol Solé-Pi
    arXivPreprintCC BY 4.0Full textCombinatorics & discrete mathematicsProbabilityarXiv

Cite

BibTeXRIS
BibTeX
@misc{weinberg2026machinechecked,
  title = {{Machine-Checked Simplicial Chain Complexes over F_2 and Metric Filtration Invariants for Relational Resolution Theory in Lean 4⁠}},
  author = {Ronen Weinberg},
  howpublished = {Zenodo},
  year = {2026},
  month = oct,
  doi = {10.5281/zenodo.23448711},
  url = {https://zenodo.org/records/23448711},
  note = {CC BY 4.0},
}
RIS
TY  - UNPB
TI  - Machine-Checked Simplicial Chain Complexes over F_2 and Metric Filtration Invariants for Relational Resolution Theory in Lean 4⁠
AU  - Ronen Weinberg
PY  - 2026
DA  - 2026/10/18
PB  - Zenodo
DO  - 10.5281/zenodo.23448711
UR  - https://zenodo.org/records/23448711
AB  - We present a self-contained, machine-checked formalization in the Lean 4 theorem prover (Mathlib4) of the core algebraic-topological invariants underlying discrete metric filtrations in Relational Resolution Theory (TRR 3.0). Specifically, we formalize: (1) the monotonicity and downward closure of Vietoris-Rips metric filtration complexes over arbitrary types with decidable equality, (2) the ungraded simplicial chain module modeled via finitely supported functions, (3) the linearity and nilpotency (d^2 = 0) of the simplicial boundary operator, (4) the fundamental cycle inclusion (im d <= ker d), and (5) grading and subcomplex invariance. All ten theorems in the development are verified with zero unproven assumptions (sorryAx is absent) and depend solely on the standard axioms [propext, Classical.choice, Quot.sound].  The underlying algorithmic pipeline and machine-checked formalization for TRR 3.0 are strictly licensed under the GNU Affero General Public License v3.0 (AGPL-3.0). Source code repository: https://github.com/RW-101/TRR3-formalization-
ER  -