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

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].