Resistance distance

The effective resistance distance on a hypergraph is the oldest and best-behaved of the four candidates: it has a closed-form spectral expression, satisfies the metric axioms unconditionally, and is monotone under hyperedge addition. It is the only metric currently sorry-free.

Definition

Pick a conductance schedule $\kappa : E \times V \times V \to \mathbb{R}_{\ge 0}$ (see below). The associated weighted Laplacian is $L_\kappa = D - A$ where $A_{u,v} = \sum_e \kappa(e, u, v)$ is the total conductance between $u$ and $v$ and $D$ is its row-sum diagonal. Write $L_\kappa^+$ for the Moore–Penrose pseudoinverse.

The resistance distance between $u, v \in V$ is

Here $e_u \in \mathbb{R}^V$ is the standard basis vector at $u$.

Why this is a distance

Three properties drop out of the spectral formula directly:

• $d_H(u, u) = 0$: the vector $e_u - e_u = 0$ kills the quadratic form.
• Symmetry: $L_\kappa^+$ is symmetric (it's a pseudoinverse of a symmetric matrix).
• Non-negativity: $L_\kappa$ is positive semidefinite (it's a weighted Laplacian), and so is its pseudoinverse, so the quadratic form is $\ge 0$.

Triangle inequality is harder; the proof routes through the Klein–Randić formulation — see Metric/Resistance/Algebraic.lean.

Intuition: how hard is it to cut the connection?

Treat each hyperedge as a resistor network with conductance $\kappa(e, u, v)$ between every incident pair. Then $d_H(u, v)$ is literally the electrical resistance of the resulting circuit between terminals $u$ and $v$.

That makes the inequality

obvious. It also explains why two vertices in a densely-connected hyperedge cluster are close (many parallel resistors) while two vertices joined by a long thin chain are far (resistors in series).

Conductance from hyperedges

The conductance comes from the harmonic schedule

when $u$ is the $i_u$-th input of $e$ and $v$ is an output of $e$; symmetrised by adding $\kappa(e, v, u)$. The $\alpha(c)$ factor weights edges by colour, the $1/(i+1)$ factor enforces input monotonicity (the first input carries more weight than the last), and dividing by $|\mathrm{out}(e)|$ spreads the weight uniformly across outputs.

Rayleigh monotonicity

Adding a hyperedge can only decrease every pairwise distance:

Operationally: adding an inference rule can only make two propositions closer together. This is the discrete analogue of the classical electrical fact that adding a resistor in parallel reduces total resistance.

The corollary that drives the headline pitch: hypergraph resistance distance is a non-increasing function of mathematical knowledge.

In the compute layer

Pipeline/Linalg.lean implements the resistance matrix end-to-end in Float:

def IncidenceData.resistanceMatrix (H : IncidenceData) : Array (Array Float)

The pseudoinverse is computed via Gauss–Jordan on $L_\kappa + \varepsilon I$ with $\varepsilon = 10^{-9}$ — the regularisation cancels in the final $L^+[u,u] + L^+[v,v] - 2 L^+[u,v]$ difference up to floating-point noise. This is the formula evaluated when you run #atlas.resistance.

Try it

→ #atlas.resistance Nat.add_zero Nat.add_comm glues both proofs via const-sharing and reports $d_H(\text{root}_A, \text{root}_B)$.

References

[BDF26] §5.1 — resistance distance on hypergraphs.
[KR93] Klein, Randić, Resistance distance, J. Math. Chem. 12, 1993.