142 Cycle Space Bond Space
142.1 Cycle Space Bond Space
"Full" means as large as the matrix allows — for a \((\nu -1) \times \varepsilon \) basis matrix of the bond space, the square submatrices of order \(\nu - 1\). Theorem 12.3 says such a basis matrix is unimodular, and that is exactly what makes theorem 12.4’s determinant count the spanning trees: each nonsingular full submatrix contributes \((\pm 1)^{2} = 1\).
! Not Matrix.IsTotallyUnimodular, which quantifies over all square submatrices — that is B&M’s strictly stronger totally unimodular of exercise 12.2.3, stated separately below. "Full square submatrix" is rendered as M.submatrix id g for an injective \(g : n \to m\): all rows, and card n columns chosen injectively. Placed in the Matrix namespace so it reads B.IsUnimodular.
Record, for each vertex and each arc, whether the arc leaves the vertex (\(+1\)), enters it (\(-1\)), or misses it (\(0\)). The signs make this the oriented incidence matrix, distinct from the \(0/1\) matrix of §1.3, and they encode the conservation condition exactly: \(M *_{v} f = 0\) says inflow balances outflow at every vertex.
! Missing from Mathlib: SimpleGraph.incMatrix is the unoriented \(0/1\) matrix, and the oriented version is one of Mathlib’s own open TODOs. B&M’s "if \(a\) is a link" clause (i.e. loops map to \(0\)) is automatic in this encoding: a loop has tail a = head a = v, so the two indicators cancel to \(1 - 1 = 0\). Stated over a general [Ring R] so the same definition serves the \(F\)-valued §12.1 and the \(\mathbb {Z}\)-valued §12.2.
Currents that flow round and round without accumulating anywhere. ! Contrast chapter 11, where conservation was imposed only at intermediate vertices; here it holds everywhere, so there is no net source or sink.
The conservation condition (12.1) is packaged as \(M *_{v} f = 0\), i.e. f \(\in \) ker M.mulVecLin — theorem 12.1’s second half is precisely the claim that this repackaging is faithful. Defining \(\mathcal{C}\) as a Submodule directly gives the vector-space structure the book verifies by hand.
Assign a voltage to every vertex and read off the drop across every wire. Theorem 12.1 identifies \(\mathcal{B}\) as the row space of \(M\) and \(\mathcal{C}\) as its orthogonal complement — the duality organising the whole chapter.
\(\delta p\) is \(M^{T} *_{v} p\), so \(\mathcal{B}\) is the range of that map. ! Note the asymmetry with cycleSpace: \(\mathcal{C}\) is a kernel and \(\mathcal{B}\) a range, which is why theorem 12.2(ii) is a genuinely separate argument rather than a formal dual of (i).
\(f\) and \(g\) are orthogonal when \(\sum _{a \in A} f(a)g(a) = 0\). For real coefficients this is the usual inner product; but the chapter also needs it over fields of characteristic \(p\) (exercise 12.2.4), where the form is degenerate and a vector can be orthogonal to itself. That degeneracy is precisely why Shank’s result — dim(\(\mathcal{B}\)_F \(\cap \) \(\mathcal{C}\)_F) > 0 iff \(p \mid \tau (G)\) — is possible at all: over \(\mathbb {R}\) the two spaces meet only in zero.
! Not an inner product, and deliberately so. Used with LinearMap.BilinForm.orthogonal, which works over every field — in particular ZMod p — unlike Submodule.orthogonal/\(^{\perp }\), which needs RCLike and would make exercise 12.2.4 unstateable. The four \(mk_{2}\) obligations are bilinearity, all discharged by simp on sums.
\(u\) and \(v\) are adjacent in \(G\) exactly when some arc runs between them in one direction or the other. The chapter’s counting results — dim \(\mathcal{B}\) = \(\nu \) - \(\omega \), dim \(\mathcal{C}\) = \(\varepsilon \) - \(\nu \) + \(\omega \), \(\tau (G)\) — are all statements about this underlying graph, the orientation being an auxiliary device that cancels out.
! A SimpleGraph underlying graph loses information the arc carrier has: loops (tail a = head a) and parallel arcs both vanish. That is harmless for the counting results, which are about \(G\), but means \(G\) does not determine (tail, head) — hence this is a relation, not a function.
\(G\) is recovered by forgetting directions. The point of §12.2 is that \(\tau (G)\) is an invariant of \(G\) alone, yet is most easily computed through the oriented incidence matrix of an arbitrarily chosen orientation — the signs cancel in the determinant, which is exactly what exercise 12.2.2(a) makes precise.
! Definitionally equal to IsUnderlyingGraph, so "orientation of \(G\)" here means only "has \(G\) as underlying graph" — it does not forbid \(D\) from having both \((u,v)\) and \((v,u)\), which chapter 10’s IsOrientationOf does. For this chapter that is deliberate and harmless: the results are about \(M\) and MM\(^{T}\), which tolerate digons and loops.
A cycle of the underlying graph, traversed in one of its two directions; some arcs point along the direction of travel and some against it, which is what the sign in \(f_C\) records.
! Defective: this structure is degenerate. It carries only a nonempty list of arcs, with no closed-walk condition and no distinctness condition — the docstring’s "the closed/interior-distinct invariants are elided" understates the cost. As a result any nonempty list of arcs is an ArcCycle, and the derived predicate collapses:
IsArcAcyclic tail head S \(\leftrightarrow \) S = \(\emptyset \)
(for nonempty \(S\), pick \(a \in S\) and take the one-element list \([a]\)). Downstream, theorem 12.2(i) then reads "the columns of \(B | S\) are independent iff \(S = \emptyset \)" — false — and lemma 12.2.1 becomes trivially true for the wrong reason. This is not sorry, which makes it more dangerous: the definition looks honest.
The repair needs three fields beyond arcs and nonempty: closed walk — a vertex sequence verts : List V with verts.length = arcs.length such that consecutive arcs meet head-to-tail, cyclically: for each \(i\), {tail arcs[i], head arcs[i]} = {verts[i], verts[i+1 mod n]} (the set form allows an arc to be traversed against its direction, which is exactly what \(C^{+}\) records); interior distinctness — verts.Nodup; optionally no repeated arc — arcs.Nodup.
! SimpleGraph.Walk.IsCycle genuinely cannot serve, as the note says: the chapter’s digraphs admit loops (tail a = head a) and parallel arcs, which a SimpleGraph cannot express. But that argues for building the structure properly, not for omitting its invariants.
No cycle of the digraph lies entirely inside \(S\). Theorem 12.2 makes this combinatorial property equivalent to a linear-algebraic one — the bridge that turns counting spanning trees into counting nonsingular submatrices.
! Defective by inheritance. Because ArcCycle has no closure or distinctness conditions, this predicate collapses to \(S = \emptyset \); see ArcCycle’s docstring for the one-line argument and the repair. The definition here is *correct given a correct ArcCycle* — nothing needs changing at this declaration.
Send one unit of current round the cycle in the chosen direction; arcs pointing with the flow carry \(+1\), those against it \(-1\), everything else nothing. Conservation holds at every vertex because the cycle enters and leaves each of its vertices exactly once. These are the elementary circulations from which all others are built, and they give the cycle space its name.
! Defective: sorry body. \(f_C\) is an opaque function, so isBasisMatrix_cycleSpace_of_maximalForest — whose rows are these — asserts nothing.
The repair depends on repairing ArcCycle first: once a cycle carries its vertex sequence, \(C^{+}\) is definable (arc \(i\) is in \(C^{+}\) when tail arcs[i] = verts[i], i.e. it is traversed forwards), and
f_C a = if a \(\notin \) arcs then 0 else if a \(\in \) C\(^{+}\) then 1 else -1
! With arcs a List, \(a \in C^{+}\) needs the position, not just membership — an arc could in principle occur twice. Adding arcs.Nodup to ArcCycle removes that ambiguity and is the cleaner route.
The arcs crossing the boundary of \(S\), in either direction. The direction matters for the associated potential difference \(g_B\), which takes \(+1\) on arcs leaving \(S\) and \(-1\) on those entering it — the edge cut is undirected, its potential difference is not.
A Set A, not a Finset, matching IsBond’s quantification over arbitrary S : Set V.
An edge cut with nothing to spare. Bonds are dual to cycles: lemma 12.2.2 says the support of a nonzero potential difference contains a bond, exactly as lemma 12.2.1 says the support of a nonzero circulation contains a cycle.
! Missing from Mathlib — and beware two false friends. Dart.lean uses "bond" for an unrelated half-edge notion, and the repo’s IsEdgeCut is a cut without the minimality clause, on a different carrier.
! The minimality clause here quantifies over subsets \(B' \subseteq B\) that are themselves edge cuts (\(\exists \) S’, B’ = edgeCutSet S’). That is the right reading of "minimal nonempty edge cut" and is stronger than minimality among arbitrary subsets; check it against use sites, since lemma 12.2.2 only produces an edge cut inside the support and then needs a bond inside that.
Put every vertex of \(S\) at voltage \(1\) and every other at \(0\); the drops are \(+1\) on arcs leaving \(S\), \(-1\) on arcs entering, \(0\) on arcs with both ends on one side. These are the elementary potential differences, and they give the bond space its name.
Defined directly by the book’s \(\delta p\) formula with \(p\) the indicator of \(S\), rather than by the three-case rule — that makes membership in \(\mathcal{B}\) immediate and turns the book’s "it can be verified" into rfl. Note the definition takes an arbitrary S : Set V, not a bond, so \(g_B\) exists for any vertex set; the bond condition matters only for the basis claims.
Package a basis as the rows of a matrix, so questions about the space become questions about the matrix. This is what lets theorem 12.2 phrase acyclicity as linear independence of columns, and theorem 12.4 count spanning trees by a determinant.
"Rows form a basis" is unfolded into its two halves — LinearIndependent F M and span (range M) = W — rather than using Basis, which would require a chosen index equivalence. The row index \(n\) is a free Fintype, so the same predicate serves matrices indexed by \(T\), by \(T^{c}\), or by \({v // v \ne y}\).
\(M | S\) — B&M’s column restriction (Matrix.submatrix).
A maximal acyclic set of arcs touching every vertex. By theorem 12.2, spanning trees are exactly the \((\nu -1)\)-element subsets \(S\) for which \(B | S\) is nonsingular — which is what makes §12.2’s determinant formula count them.
! Defective: sorry body — the most damaging one in the file. tau counts the Finsets satisfying this predicate, so \(\tau (G)\) is an opaque natural number, and every §12.2 statement about it is vacuous: theorem 12.4, (12.8), corollary 12.4, the matrix-tree theorem, and exercises 12.2.1(b), 12.2.2(b), 12.2.4(a), (b).
The repair, once ArcCycle is fixed:
IsSpanningTree tail head T := IsArcAcyclic tail head T \(\land \) T.card + 1 = Fintype.card V \(\land \) (the underlying subgraph on T is connected)
or equivalently "acyclic and spanning", using the connectivity notion suggested for IsConnectedDigraph. Acyclic plus \(|T| = \nu - 1\) already forces connectivity for a graph on \(\nu \) vertices, so the middle clause plus acyclicity suffices — but only once IsArcAcyclic is genuine.
A maximal acyclic set of arcs — a spanning tree of each component. Its size \(\nu - \omega \) is exactly the rank of the bond space, which is how corollary 12.2 computes dim \(\mathcal{B}\).
! Defective: sorry body. Makes both tree-basis theorems (isBasisMatrix_cycleSpace_of_maximalForest, isBasisMatrix_bondSpace_of_maximalForest) vacuous, and is a hypothesis of fundamentalCycle.
The repair: IsArcAcyclic tail head T \(\land \) \(\forall \) a \(\notin \) T, \(\lnot \) IsArcAcyclic tail head (insert a T) — acyclic and maximally so. Note this is the forest notion, weaker than IsSpanningTree: it does not require connectivity, which is exactly why corollary 12.2 gets \(\nu - \omega \) rather than \(\nu - 1\).
The tree already provides a unique route between the ends of \(a\) (theorem 2.1), and adding \(a\) closes exactly one cycle. The \(\varepsilon - \nu + \omega \) fundamental cycles, one per non-tree arc, give the tree-basis of the cycle space — the matrix \(C\) is a basis matrix because \(C | \bar{T}\) is an identity matrix, so its rank is full.
! Defective: sorry body. An opaque ArcCycle, so isBasisMatrix_cycleSpace_of_maximalForest asserts nothing about it.
The repair. The lever noted in the source comment is right: IsAcyclic.path_unique gives the unique \(T\)-path between \(a\)’s ends, and the cycle is that path closed by \(a\). ! But it is stated for SimpleGraph, while this chapter’s carrier is tail, head : A \(\to \) V with loops and parallel arcs — so either transfer along the underlying graph (losing the multi-arc case) or redo the uniqueness argument on the arc carrier. The hT hypothesis is what makes "unique" true, and \(ha : a \notin T\) what makes the cycle exist.
Deleting \(a\) splits its tree in two, and \(S\) is the vertex set of one half; the arcs crossing between the halves form the fundamental bond. The \(\nu - \omega \) fundamental bonds, one per tree arc, give the tree-basis of the bond space, with \(B | T\) an identity matrix. The exact mirror of the fundamental cycle — theorem 2.6 is to bonds and cotrees as theorem 2.5 is to cycles and spanning trees.
! Defective: sorry body. Makes isBasisMatrix_bondSpace_of_maximalForest vacuous.
The repair: \(S\) is the set of vertices reachable from tail a in \(T \ {a}\) (using the underlying-graph reachability of IsConnectedDigraph’s repair). Then edgeCutSet tail head S is the fundamental bond, and bondPotentialDiff tail head S its potential difference — which is why the definition returns the vertex set rather than the bond, letting bondPotentialDiff be applied directly. ! Leans on B&M’s theorem 2.6, which is out of chapter and not in this repo.
Its defining feature is that \(B | T\) is an identity matrix — the fundamental bond of \(a\) contains \(a\) itself with coefficient \(1\) and no other tree arc. That is what pins down det(B | T) = 1 in the proof of theorem 12.3, and what makes exercise 12.1.2(b)’s change-of-basis identity readable.
! Defective: sorry body. This predicate is a hypothesis of theorems 12.3, 12.4, corollary 12.4 and exercises 12.2.1(b), 12.2.3(a), 12.2.4(a) — all of which therefore constrain nothing.
The repair: \(B\) is the tree-\(T\) basis matrix when its rows are the fundamental-bond potential differences, i.e.
B = fun a : a // a \(\in \) T => bondPotentialDiff tail head (fundamentalBondVertexSet tail head T a.1)
— exactly the matrix appearing in isBasisMatrix_bondSpace_of_maximalForest. ! Alternatively, characterise it axiomatically as *"a basis matrix of \(\mathcal{B}\) whose restriction \(B | T\) is the identity"*, which is weaker to state, enough for theorem 12.3, and does not depend on fundamentalBondVertexSet — probably the better choice, since it is the property every proof actually uses.
The cycle-side mirror of IsBasisMatrixOfTree: \(C | \bar{T}\) is the identity, because the fundamental cycle of \(a\) is the only one using \(a\).
! Defective: sorry body. Hypothesis of (12.8), corollary 12.4 and exercises 12.2.1(b), 12.2.4(a) — all vacuous as a result.
The repair: as for IsBasisMatrixOfTree, either concretely (rows are the fundamental-cycle circulations) or axiomatically (*a basis matrix of \(\mathcal{C}\) with \(C | \bar{T}\) the identity*). The axiomatic form is again preferable and is what the determinant arguments actually consume.
The object §12.2 exists to compute. Theorem 2.8 gave a recursion and theorem 2.9 a closed formula for complete graphs; chapter 12 finally delivers the general determinant formula — the matrix-tree theorem, implicit in Kirchhoff (1847).
! Defective by inheritance. IsSpanningTree has a sorry body, so tau counts an opaque predicate and is itself opaque. This is the single most consequential defect in the file — every §12.2 result is a statement about tau. Nothing here needs changing; repairing IsSpanningTree repairs this.
, first half. *Let \(M\) be the incidence matrix of a digraph \(D\). Then \(\mathcal{B}\) is the row space of \(M\).*
The drop across \(a\) is the signed combination of the vertex potentials, with \(m_v\) picking out the sign. So the bond space is exactly the row space of \(M\), and dim \(\mathcal{B}\) = rank M.
Submodule.span F (Set.range M) is the row space, \(M\) being read as a family of rows indexed by \(V\). Step 3’s identity is the only real content and is worth extracting, since theorem 12.1’s second half needs it too.
, second half. …and \(\mathcal{C}\) is its orthogonal complement.
This duality is the organising idea of the chapter. It gives corollary 12.2’s dimension formula at once, it makes BC’ = 0 in corollary 12.4, and it is the source of the cycle/bond symmetry that, as B&M remark, *finds its proper setting in the theory of matroids*.
! Note this is orthogonality for a possibly degenerate form — over ZMod p a space need not be complementary to its orthogonal, which is exactly what exercise 12.2.4(b) exploits. So "orthogonal complement" here means BilinForm.orthogonal, not "complementary subspace"; do not silently use dim \(\mathcal{B}\) + dim \(\mathcal{C}\) = \(\varepsilon \) in characteristic \(p\).
*If \(f\) is a nonzero circulation, then \(\| f\| \) contains a cycle.*
Current cannot enter a dead end: anything that flows must flow round in a loop.
! Currently trivial for the wrong reason. Since ArcCycle has no closure condition, the goal is satisfied by the one-element list \([a]\) for any \(a \in \| f\| \) — so this is provable in two lines and means nothing. Repair ArcCycle before filling; the skeleton above is for the repaired statement.
*If \(g\) is a nonzero potential difference, then \(\| g\| \) contains a bond.*
The exact dual of lemma 12.2.1; the two together drive theorem 12.2.
Step 4 is where IsBond’s minimality is consumed — see that definition’s note about what "minimal among edge cuts" quantifies over.
*Let \(B\) be a basis matrix of \(\mathcal{B}\). Then for any \(S \subseteq A\), the columns of \(B | S\) are linearly independent if and only if \(S\) is acyclic.*
The theorem converting a combinatorial question into a linear-algebraic one — and it holds over any field, which is why exercise 12.1.5 is subsumed by stating §12.1 over [Field F].
! Currently false. With ArcCycle degenerate, IsArcAcyclic S \(\leftrightarrow \) S = \(\emptyset \), so the right-hand side says \(S = \emptyset \) while the left is true for any independent column set. Repair ArcCycle first. Step 4 additionally needs cycleCirculation, also sorry-bodied.
*Let \(C\) be a basis matrix of \(\mathcal{C}\). Then for any \(S \subseteq A\), the columns of \(C | S\) are linearly independent if and only if \(S\) contains no bond.*
B&M dispatch this with "a similar argument", but it is genuinely a second theorem rather than a formal symmetry: \(\mathcal{C}\) is defined as a kernel and \(\mathcal{B}\) as a range, so step 2 has no counterpart in part (i).
Step 2 is the whole reason this deserves separate treatment; budget for it rather than expecting the (i) proof to transport.
, formula (12.3). dim \(\mathcal{B}\) = \(\nu \) - \(\omega \).
The bond space records the vertex potentials — \(\nu \) of them — modulo an additive constant on each of the \(\omega \) components, leaving \(\nu - \omega \) degrees of freedom.
! Stated over \(\mathbb {R}\) specifically, unlike the rest of §12.1 which is over a general [Field F]; the dimension count is in fact field-independent, so this could be generalised. Step 3 is the out-of-chapter import to budget for. Note the \(\mathbb {N}\)-subtraction card V - card ConnectedComponent never truncates, since \(\omega \le \nu \).
, formula (12.4). dim \(\mathcal{C}\) = \(\varepsilon \) - \(\nu \) + \(\omega \).
\(\varepsilon - \nu + \omega \) is the cycle rank or first Betti number — the number of independent cycles, and exactly the number of arcs outside a maximal forest. That count is realised concretely by the fundamental cycles, one per non-tree arc.
! B&M derive this from orthogonality (dim \(\mathcal{C}\) = \(\varepsilon \) - dim \(\mathcal{B}\)), which is valid over \(\mathbb {R}\) but not in characteristic \(p\), where the form is degenerate and the two spaces can overlap (exercise 12.2.4(b)). The rank–nullity route of step 1 is field-independent and therefore both simpler and more robust — prefer it.
The fundamental cycle basis — the concrete realisation of the claim that every circulation is a combination of cycle circulations, which is what gave the cycle space its name.
! Currently vacuous. Three of the four ingredients — IsMaximalForest, fundamentalCycle, cycleCirculation — have sorry bodies.
The fundamental bond basis, realising the claim that every potential difference is a combination of bond potential differences.
! Currently vacuous — IsMaximalForest and fundamentalBondVertexSet both have sorry bodies. ! Step 2 also leans on B&M’s theorem 2.6, which is out of chapter and absent from this repo.
(proof due to Tutte, 1965b). *The basis matrix \(B\) is unimodular.*
Exactly what theorem 12.4 needs: every full submatrix contributes \(0\) or a determinant of absolute value \(1\), so squaring and summing counts the spanning trees. The proof is due to Tutte (1965b).
! Currently vacuous — IsSpanningTree and IsBasisMatrixOfTree both have sorry bodies. Note step 4 is where the axiomatic reading of IsBasisMatrixOfTree ("basis matrix with \(B | T\) the identity") would pay off directly.
\(\tau \)(G) = det BB’ (12.6).
The chapter’s central computation: the number of spanning trees, a purely combinatorial quantity, is a determinant. Compare theorem 2.8’s deletion–contraction recursion, which B&M called impractical for large graphs, and theorem 2.9’s Cayley formula, valid only for complete graphs — this is general and efficiently computable.
! Currently vacuous — tau (via IsSpanningTree) and IsBasisMatrixOfTree both rest on sorry bodies. Step 1 is an additional, substantial import.
The chapter is organised around such dual pairs — cycles and bonds, kernels and ranges, trees and cotrees.
! Step 3 needs the cycle-side analogue of exercise 12.1.2(b), which is stated in this file only for \(\mathcal{B}\) (basisMatrix_eq_restrict_mul). The cycle version must be proved separately, and — as noted under theorem 12.2(ii) — the \(\mathcal{C}\)-side arguments are not formal transports of the \(\mathcal{B}\)-side ones.
The spanning trees can be counted from either space — through the bonds or through the cycles. Corollary 12.4 combines the two computations into one determinant.
! Currently vacuous — tau and IsBasisMatrixOfTree’ both rest on sorry bodies; and Cauchy–Binet is still missing.
\(\tau \)(G) = \(\pm \) det [B; C], the determinant of the square matrix obtained by stacking a tree-basis matrix of \(\mathcal{B}\) on top of one of \(\mathcal{C}\).
The stacked matrix is square because dim \(\mathcal{B}\) + dim \(\mathcal{C}\) = (\(\nu \) - \(\omega \)) + (\(\varepsilon \) - \(\nu \) + \(\omega \)) = \(\varepsilon \) — the two spaces are complementary, which is theorem 12.1’s orthogonality counted dimensionally.
The \(\lor \) in the conclusion is the book’s \(\pm \). The row index is \({a // a \in T} \oplus {a // a \notin T}\), reindexed to \(A\) by Equiv.sumCompl — that equiv is canonical here, unlike in exercise 12.2.1(b) where one must be supplied. ! Currently vacuous, resting on tau and both IsBasisMatrixOfTree predicates.
(implicit in Kirchhoff, 1847). *\(\tau \)(G) = det KK’, where \(K\) is obtained from the incidence matrix \(M\) by deleting any one row.*
The rows of \(M\) sum to zero — every arc contributes \(+1\) at its tail and \(-1\) at its head — so exactly one row is redundant, and discarding it leaves an independent spanning set of \(\mathcal{B}\). By exercise 12.2.2(a) the product MM’ is the
(B&M’s conductance matrix), so this says every cofactor of the Laplacian equals \(\tau (G)\) — the form in which the matrix-tree theorem is usually quoted, and the closed formula for \(\tau (G)\) promised back in §2.4.
! Currently vacuous — tau and IsConnectedDigraph both rest on sorry bodies. Step 3 is a genuine restructuring worth doing before any of §12.2 is filled.
. A matrix \(K\) obtained from \(M\) by deleting any one row is unimodular.*
The incidence-matrix counterpart of theorem 12.3, and what upgrades exercise 12.1.3 into the matrix-tree theorem \(\tau \)(G) = det KK’. Note it is proved directly, not via theorem 12.3 — \(K\) is not a tree-basis matrix.
! Step 3’s leaf induction is the real work and has no counterpart in theorem 12.3’s slick change-of-basis argument. ! The statement lacks a connectivity hypothesis, unlike isBasisMatrix_deleteRow; step 2 uses that \(K\) is a basis matrix, which does need hconn — so either add it or find a route through step 3 alone.
*The conductance matrix \(C\) of a loopless graph \(G\) satisfies C = MM’, where \(M\) is the incidence matrix of any orientation of \(G\).*
* The cheapest win in the file — a direct computation, no dependency on the defective definitions. This is what Mathlib calls the Laplacian; B&M call it the conductance matrix. Notably the orientation drops out — the signs cancel — so it is an invariant of the undirected graph, as it must be.
Step 3’s parallel-arc caveat is the one thing to pin down before starting; everything else is Finset.sum manipulation.
*All cofactors of the conductance matrix \(C\) are equal to \(\tau (G)\).*
The form in which the matrix-tree theorem is normally stated: *the number of spanning trees is any cofactor of the Laplacian*. It finally delivers, in full generality, the closed formula for \(\tau (G)\) that §2.4 promised and that theorem 2.9 gave only for complete graphs.
This states the principal \((y,y)\)-minor, which is what the matrix-tree theorem gives directly and what every application uses. B&M claim all cofactors equal \(\tau (G)\), including the non-principal ones; that full statement is tau_eq_lapMatrix_cofactor directly below, and this principal case is the one to prove first.
, full form. *All cofactors of the conductance matrix \(C\) are equal to \(\tau (G)\).*
tau_eq_det_lapMatrix_deleteRowCol above states only the principal \((y,y)\)-minor. The triage (log/graphtheory-EXERCISE_TRIAGE.md §A.11) recorded this as a fidelity gap and recommended stating the exercise as written. The general form is the one usually cited, because it is what licenses deleting any row and any column — the principal case alone does not.
! Deleting row \(i\) and column \(j\) for \(i \ne j\) leaves a matrix whose row and column index types are the different subtypes \({v // v \ne i}\) and \({v // v \ne j}\), so Matrix.det does not apply to it. A reindexing equiv \(e\) between the two is therefore threaded through explicitly — the same device tau_eq_det_fromBlocks_K uses further down this file for the same reason. Because \(e\) is not canonical it fixes the column order only up to a permutation, so the conclusion is stated up to sign, absorbing \((-1)^(i+j)\) and sign e together. Taking \(i = j\) and e = Equiv.refl recovers the principal case above.
! Currently vacuous via tau and IsConnectedDigraph, exactly as the principal case is.
*The incidence matrix of a simple graph \(G\) is totally unimodular if and only if \(G\) is bipartite.*
! Note this is the unoriented \(0/1\) incidence matrix of §1.3, not the signed one of this chapter — the signed version is always totally unimodular, for every graph. The classical characterisation underlying the integrality of bipartite matching linear programs, and it links back to theorem 1.2: bipartite means no odd cycle.
* Independent of every defective definition in this file — it mentions only SimpleGraph.incMatrix and IsBipartite, both Mathlib. Together with exercise 12.2.2(a), one of the two items that can be filled today. Step 2’s determinant computation is the concrete part.
(H. Shank). *Let \(F\) be a field of characteristic \(p\). Then dim(\(\mathcal{B}\)_F \(\cap \) \(\mathcal{C}\)_F) > 0 if and only if \(p \mid \tau (G)\).*
Over \(\mathbb {R}\) the two spaces are orthogonal complements and meet only in zero. In characteristic \(p\) the dot form is degenerate — a vector can be orthogonal to itself — so they may genuinely overlap, and Shank’s result says the overlap is nontrivial exactly when \(p \mid \tau (G)\). A purely arithmetic property of \(\tau (G)\) detected by a linear-algebraic degeneracy — a striking illustration of the chapter’s theme.
! Step 1 must not be derived from orthogonality (dim \(\mathcal{C}\) = \(\varepsilon \) - dim \(\mathcal{B}\)), which is exactly what fails here; use the rank–nullity argument recorded under finrank_cycleSpace. Getting this wrong would make the proof circular — the whole point is that the two spaces are not complementary.