Resistance distance

Mathematical definition

Let $H = (V, E, \kappa)$ be a hypergraph with conductance matrix $C \in \mathbb{R}^{V \times V}$ derived from the colour weights $\kappa$ , and graph Laplacian $L_\kappa = D - C$ (where $D$ is the diagonal degree matrix). The effective resistance distance between two vertices $u, v \in V$ is

d_H(u, v) \;=\; (e_u - e_v)^\top L_\kappa^{+} (e_u - e_v)

where $L_\kappa^+$ is the Moore–Penrose pseudoinverse and $e_u, e_v$ are the standard basis vectors. Equivalently, because $e_u - e_v$ is orthogonal to $\ker L_\kappa = \operatorname{span}(\mathbf{1})$ ,

d_H(u, v) \;=\; L_\kappa^+[u, u] + L_\kappa^+[v, v] - 2\, L_\kappa^+[u, v] .

Intuition

The resistance distance is defined by an electrical-network thought experiment. Convert the hypergraph into a resistor network, attach a unit current source between the two vertices of interest, and read off the voltage drop — that's the distance.

The conversion from hypergraph to graph is clique expansion: a hyperedge with $k$ incident vertices contributes one unit-conductance resistor between every pair of those vertices (so $\binom{k}{2}$ resistors in total). For our running example — one hyperedge $e$ incident to three vertices $u, v, w$ — that means three resistors, forming a triangle:

Hyperedge → clique → measurement. The triangle (u, v, w) is the network. Inject 1 A at u, extract at v via the bottom-loop battery, and read the voltage drop V(u) − V(v) = R(u, v) = 2/3 Ω. (1 Ω direct in parallel with two 1 Ω in series = 1·2/3.)

The resistance distance $d_H(u, v)$ then measures how hard it is to disconnect $u$ from $v$ by removing inference steps. Many short, parallel proof paths from $u$ to $v$ pull the resistance down; a single bottleneck pulls it up. It is the natural metric for the question how independent are two propositions, given the deductive structure of the surrounding mathematics?

Lean implementation

The non-computability comes from the Real-valued pseudoinverse on the proof side. The compute side (Pipeline/Linalg.lean) instead inverts a regularised Float matrix via hand-rolled Gaussian elimination — equivalent up to the small $\varepsilon$ regularisation because $e_u - e_v$ lies in the image of $L_\kappa$ .

The IsHypergraphMetric instance signature, pulled live from the repo ? error:

LeanSource error: cannot read lean/ProofAtlas/Metric/Resistance/Instance.lean: ENOENT: no such file or directory, open '/vercel/path0/lean/ProofAtlas/Metric/Resistance/Instance.lean'

The signature accepts five preconditions: two structural (hConn, hRange) about the harmonic Laplacian, and three sensitivity witnesses passed in by the caller. The body discharges all seven IsHypergraphMetric fields and contains no sorry.

`IsHypergraphMetric` status

Field	Status	Notes
`d_self`	✓	from `effectiveResistance_self`
`d_symm`	✓	$L_\kappa^+$ is symmetric
`d_triangle`	✓	via Schur-complement / Rayleigh argument
`d_nonneg`	✓	$L_\kappa^+$ is positive semidefinite
`sensitive_to_direction`	hypothesis	parameterised over the existence witness
`sensitive_to_ordering`	hypothesis	parameterised over the existence witness
`sensitive_to_coloring`	hypothesis	parameterised over the existence witness

The instance theorem resistanceDist_isHypergraphMetric lives at ProofAtlas/Metric/Resistance/Instance.lean and is sorry-free; the three sensitivity witnesses are passed in as preconditions to be discharged by the caller (one concrete discharge per example hypergraph).

Rayleigh monotonicity

A clean structural consequence: adding inference rules never increases resistance distance. Formally, if $H'$ is obtained from $H$ by adding hyperedges (more inference paths), then for every $u, v$ ,

d_{H'}(u, v) \;\le\; d_H(u, v) .

This is the Rayleigh monotonicity principle from electrical network theory: adding conductors can only reduce effective resistance. For ProofAtlas it means introducing new lemmas makes the rest of mathematics closer, never farther — exactly the intuition we want from a knowledge-structure metric.

Worked example

For the toy expression id Nat — three vertices (id, Nat, the application node) and one hyperedge forming a triangle — the resistance between any pair is

d_H(u, v) \;=\; \tfrac{2}{3} \;\approx\; 0.667 .

See the front page table for the live #eval output and the Pipeline page for the full report on a small multi-declaration environment.