Magnitude Homology Program
How many genuinely different points does a space have?
Count the points in a metric space and you get cardinality. But cardinality ignores geometry: two points on top of each other shouldn't count as two. Magnitude is Leinster's answer—a single number measuring the “effective size” of a metric space, where nearby points partially cancel.
But a single number is lossy. Magnitude homology lifts that number into a graded sequence of groups MHn,ℓ(X) that detect genuine metric-geometric structure the bare magnitude cannot see. Chains are consecutively-distinct tuples, graded by degree and metric length. The differential squares to zero, giving cycles, boundaries, and homology.
This project formalizes the entire theory in Lean 4: from the chain complex through Künneth decomposition, Mayer-Vietoris gluing, diagonal concentration, persistent/VR bridges, LLM-enriched magnitude with Tsallis entropy, to iterated spectral convergence. Every theorem is machine-checked. Zero sorry. Six hostile audit rounds, all clean.
Why this is Ruliology
Magnitude homology is a universal detector for metric space structure. It applies to any finite metric space whatsoever—any rule that produces pairwise distances generates a magnitude homology. The program doesn't study one rule; it studies what all rules with metric structure have in common.
The Noneist commitment: we prove theorems about spaces we never construct. The unit-edge diagonality theorem holds for every finite metric space with unit distances, without enumerating them. The Mayer-Vietoris exactness holds for every finite cover. These are properties of the Platonic state potential, not of any computed instance.
The formal verification commitment: the type checker is the arbiter. Not “we believe d² = 0” but “Lean has verified d² = 0 for the alternating face-map differential on consecutively-distinct tuples in any decidably-equal finite type.”
Basic (cardinality) │ Homology (chains, d, d²=0) │ HomologyGroups (Z/B, Betti, F₂ matrices) │ │ │ Weighting KünnethMV Diagonality (similarity, (products, (bigrading, fixed-point) covers, MV) unit-edge) │ │ │ EnrichedMagnitude BlurredPersistent IteratedMH (LLM, Tsallis) (persistence, VR) (nerve, spectral)
Chain Complex & Homology Groups
Foundation: magnitude chains as consecutively-distinct tuples, alternating differential via face maps, d² = 0, cycles Zₙ = ker(d), boundaries Bₙ = im(d), homology MHₙ = Z/B, Betti numbers over F₂ via boundary matrices and rank-nullity.
- •magnitudeDifferential_squared (d² = 0)
- •boundary_subset_cycles (B ⊆ Z)
- •magnitudeHomologyGroupAdd (Z/B as additive group)
- •Betti numbers via F₂ matrix rank
Künneth Formula & Mayer-Vietoris
Product decomposition: chain-level Künneth map (multiplicative separation), Betti convolution, tensor-product complex over F₂ via Kronecker products. Cover gluing: Mayer-Vietoris exactness at direct sums, cardinality identity |U|+|V| = |X|+|U∩V|.
- •kunnethMap_mul (multiplicative separability)
- •Künneth verified computationally for Bool × Fin 3
- •mv_exact_at_direct_sum (MV exactness)
- •mv_cover_cardinality
Diagonality
Metric magnitude spaces with chain length grading. Diagonal concentration: all chains live on the n = ℓ diagonal. Unit-edge metric spaces are diagonal. Diagonality descends along metric retracts.
- •unitEdge_implies_diagonal
- •median_implies_diagonal
- •diagonal_retract (descent along retracts)
- •chainLength_eq_degree_of_unitEdge
Blurred Persistent & Vietoris-Rips Bridge
Threshold-bounded chains with persistence functoriality. Blurred differential with d² = 0 under support conditions. Vietoris-Rips chains, ℓₚ families, ℓ∞ chains. VR ↔ blurred bridges including hypothesis-free degree-1 equivalence.
- •blurredDifferential_squared
- •blurred_persistence_commutes
- •blurred_eq_vr_l1_degreeOne (unconditional VR bridge)
- •vrToBlurredScaled / vrToLpScaled
LLM-Enriched Magnitude & Tsallis Entropy
Enriched similarity spaces with [0,1]-valued kernels. LLM enrichment: sim(p₁,p₂) = Σ nextToken(p₁,v)·nextToken(p₂,v). Tsallis q-entropy bridge: enriched magnitude decomposes as |Vocab| + Σ H₂(nextToken(p,·)) under shape hypothesis.
- •llmEnrichment (all axioms proved)
- •tsallisEntropy_two (closed form at q=2)
- •magnitude_eq_tsallis_sum_of_magnitude_shape
- •llm_similarity_pos_for_distinct_with_overlap
Iterated MH & Spectral Convergence
k-layered nerve vertices, Moore complex via iterated alternating differential, simplicial law for face maps. Iterated homology Z/B with cycle subtype. k=1 bridge recovers bar simplices. Spectral convergence via ratchet stabilization.
- •nerveFace_comp (simplicial identity)
- •iteratedMH (Z/B quotient)
- •magnitudeNerveOneEquivBarSimplex (k=1 bridge)
- •iteratedMH_paged_converges
Three Branches from One Foundation
Information Theory
EnrichedMagnitude connects Leinster magnitude to LLM next-token distributions via Tsallis entropy. The “effective size” of prompt space depends on output diversity.
Applied Topology (TDA)
BlurredPersistent bridges magnitude homology to Vietoris-Rips complexes—the standard tool in topological data analysis. Degree-1 equivalence is unconditional.
Homotopy Theory
IteratedMH generalizes to k-layered nerve vertices with spectral convergence. At k=1, recovers classical magnitude homology via bar simplices.
Hostile Audit History
| Round | Scope | Findings | Status |
|---|---|---|---|
| 1 | Phase 4 initial | P1–P6 | CLOSED |
| 2 | P1–P6 remediation | N1–N3 | CLOSED |
| 3 | N1–N3 remediation | F1–F2 | CLOSED |
| 4 | F1–F2 remediation | G1–G2 (cosmetic) | CLOSED |
| 5 | Phase 5+6 new content | H1–H4 | CLOSED |
| 6 | H1–H4 remediation | None | CLEAN |
Contribution Certificates
Immutable contribution records per MENTAT-CA-001. Each certificate is a cryptographically anchored MCR documenting authorship, contribution level, and provenance chain. Artifacts are content-addressed and pinned to IPFS.
MENTAT Contribution Record
IDEA
Conceptual Contribution
CONTRIBUTION LEVEL: IDEA
Ontological EngineerMagnitude as Effective Size of Metric Spaces
Contributor
Tom Leinster
University of Edinburgh
Conceptual insight that the Euler-characteristic-like magnitude of enriched categories can be lifted into a graded homology theory for metric spaces. Key idea: consecutively-distinct tuples form chains graded by degree and metric length, with an alternating face-map differential. This 'effective number of points' captures genuine geometric structure that bare cardinality and even magnitude itself cannot see.
MENTAT Contribution Record
THEORY
Mathematical Foundation
CONTRIBUTION LEVEL: THEORY
Ontological EngineerMagnitude Homology of Metric Spaces
Contributor
Tom Leinster
University of Edinburgh
Complete mathematical framework: magnitude homology groups MH_{n,ℓ}(X), Künneth decomposition for metric products, Mayer-Vietoris exactness for covers, diagonal concentration for unit-edge spaces, and the relationship between magnitude homology and classical magnitude via Euler characteristic.
Builds Upon
MENTAT Contribution Record
APPLICATION
Applied Contribution
CONTRIBUTION LEVEL: APPLICATION
Ontological EngineerMagnitude Homology Applications to TDA and Information Theory
Contributor
Tom Leinster
University of Edinburgh
Applied connections from magnitude homology to three production domains: (1) Vietoris-Rips complexes in topological data analysis via blurred persistence. (2) LLM next-token distributions via Tsallis entropy enrichment — the 'effective size' of prompt space depends on output diversity. (3) Iterated nerve structures with spectral convergence for hierarchical metric decomposition.
Builds Upon
MENTAT Contribution Record
PROOF
Formally Verified
CONTRIBUTION LEVEL: PROOF
Lean 4 Formalization of Magnitude Homology Program
Contributor
Apoth3osis Labs
R&D Division
Machine-checked Lean 4 formalization of the complete magnitude homology theory. 11 modules (Basic, Homology, HomologyGroups, KunnethMV, Diagonality, BlurredPersistent, EnrichedMagnitude, IteratedMH, Weighting, Bridge, README), 2242 lines of proof code, 90+ theorems. Covers chain complexes through spectral convergence. Zero sorry/admit. Built on Mathlib.
Builds Upon
MENTAT Contribution Record
KERNEL
Computationally Verified
CONTRIBUTION LEVEL: KERNEL
Magnitude Homology Verified Kernel — 6-Round Hostile Audit
Contributor
Apoth3osis Labs
R&D Division
Complete formal verification through six rounds of adversarial hostile audit. R1: P1–P6. R2: N1–N3. R3: F1–F2. R4: G1–G2 (cosmetic). R5: H1–H4 (Phases 5+6). R6: CLEAN. All findings resolved. Final round produced zero findings. 90+ theorems kernel-checked by Lean 4.
Builds Upon
MENTAT Contribution Record
BRIDGE
Cross-Level Connection
CONTRIBUTION LEVEL: BRIDGE
Magnitude Homology → LLM Enrichment & TDA Bridge
Contributor
Apoth3osis Labs
R&D Division
Three production bridges from pure magnitude homology: (1) EnrichedMagnitude connects to LLM next-token distributions via Tsallis entropy — the 'effective size' of prompt space depends on output diversity. (2) BlurredPersistent bridges to Vietoris-Rips complexes — the standard TDA tool — with unconditional degree-1 equivalence. (3) IteratedMH generalizes to k-layered nerve vertices with spectral convergence, recovering classical magnitude homology at k=1.
Builds Upon
Governed by MENTAT-CA-001 v1.0 · March 2026