Read-back: resistance_triangle

Let $V$ be a finite type (with decidable equality), and let $c : V \times V \to \mathbb{R}$ be a function satisfying the bundled hypothesis "is a conductance": $c(x,y) \ge 0$ for all $x, y$ and $c(x,y) = c(y,x)$ for all $x, y$. (Nothing forbids nonzero self-conductances $c(x,x)$, and $c$ need not be nonzero anywhere beyond what the other hypotheses force.) Write $c(x) = \sum_{y \in V} c(x,y)$ for the total conductance at a vertex $x$; the theorem assumes $c(x) > 0$ for every $x \in V$. Define the transition matrix $P$ of the "network walk" by $P(x,y) = c(x,y)/c(x)$ (real division, so this is the usual random-walk matrix under the positivity assumption). The theorem further assumes $P$ is "irreducible" in the following sense: for every pair $x, y \in V$ there exists a natural number $t \ge 0$ with $(P^t)(x,y) > 0$ — note $t = 0$ is allowed, and $P^0$ is the identity matrix, so the diagonal case $x = y$ is automatically satisfied by $t = 0$. Given two designated vertices $a, z$, the "voltage" at $x$ is defined as $v_{a,z}(x) = \sum_{t=0}^{\infty} q_t(x)$, where $q_t(x)$ is the sum, over all length-$t$ vertex sequences $\omega = (\omega_0, \dots, \omega_t)$ with $\omega_0 = x$, of the path weight $\prod_{i=0}^{t-1} P(\omega_i, \omega_{i+1})$, restricted to sequences that end at $\omega_t = a$, avoid $a$ at every index before the last one, and avoid $z$ at every index including index $0$ (so this is a probability that the walk started at $x$ hits $a$ strictly before $z$; in particular $v_{a,z}(z) = 0$, and the infinite series is Lean's tsum, which takes the value $0$ if the series fails to be summable). The "current strength" from $a$ to $z$ is $I(a,z) = \sum_{y \in V} c(a,y)\,\bigl(v_{a,z}(a) - v_{a,z}(y)\bigr)$, and the "effective resistance" is defined as the multiplicative inverse $R(a,z) = I(a,z)^{-1}$ — with the Lean convention that $0^{-1} = 0$, so if the current strength vanishes the effective resistance is $0$ by fiat rather than infinite. Under all of the above hypotheses, and for three vertices $a, b, z \in V$ assumed pairwise distinct ($a \ne b$, $b \ne z$, $a \ne z$), the theorem asserts the triangle inequality

i.e. the effective resistance (as defined above, via the inverse of current strength) between $a$ and $z$ is at most the sum of the effective resistances between $a$ and $b$ and between $b$ and $z$. The inequality is non-strict, and nothing beyond the stated hypotheses (symmetry and nonnegativity of $c$, strictly positive vertex conductances, irreducibility of the walk, pairwise distinctness of $a, b, z$) is assumed.