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 |