The combinatorial induction: splitting off, KT Theorem 4.9 and the surgery of KT Lemma 4.1

Results of the combinatorial induction (sec:molecular-induction) after Katoh and Tanigawa (2011, A proof of the molecular conjecture, Discrete Comput. Geom. 45, §§4 and 6). For a multigraph G, D = bodyBarDim n and G̃ = (D - 1)·G, a vertex v whose edges eₐ and e_b join it to a, b ≠ v, and the label e₀ ∉ E(G) of the new edge ab of G_v^{ab}, whose copies in G̃_v^{ab} are ẽ₀ = edgeFiber e₀ n, it proves:

• KT Lemma 4.8(i) (pp. 665–666): if G is a minimal 0-dof-graph with at least three vertices and no proper rigid subgraph, and v has degree two, then G_v^{ab} is a minimal 0-dof-graph (lem:reduction-step); a step is KT eq. (4.10), that every circuit of M(G̃_v^{ab}) meets ẽ₀;
• the induction principle from which KT Theorem 4.9 (pp. 666–667) follows (thm:minimal-kdof-reduction), with the two edges at a vertex of degree two of a 0-dof-graph; the induction over all deficiencies of Katoh and Tanigawa's proof of their Theorem 5.5 (p. 671; thm:minimal-kdof-reduction-all-k); and an induction over all multigraphs (thm:pencil-reduction);
• a vertex of degree two in a minimal 0-dof-graph with no proper rigid subgraph, which Case III takes, and, when d ≥ 3, a chain b v a c (lem:chain-data-of-noRigid);
• the surgery of KT Lemma 4.1 (p. 660) on a base of M(G̃): a partition of the base into D forests each of which has an edge at v (lem:balanced-forest-packing), the surgery on such a partition (lem:forest-surgery-count), and the bound def(G̃_v^{ab}) ≤ def(G̃) that it gives (lem:forest-surgery-split);
• KT Lemma 4.3(ii) (p. 661; lem:splitoff-kdof-criterion); from the proof of KT Claim 6.11 (p. 684), that G - v is a minimal k'-dof-graph with k' ≤ D - 2 when G is a minimal 0-dof-graph (lem:case-III-gap3-minimalKDof); the second assertion of KT Lemma 4.4 (p. 662; lem:removal-deficiency-equality); KT Lemma 4.7 (p. 665; lem:removal-deficiency-strict); and KT Lemma 4.8(ii) (pp. 665–666; lem:reduction-step-pos).

EdgeSplitting.lean proves KT Lemma 4.2 and the changes that the surgery makes to one forest; ChainExtraction.lean proves KT Lemma 4.6 at k = 0.

Every circuit of M(G̃_v^{ab}) meets the copies of ab (KT eq. (4.10))

theorem Graph.circuit_splitOff_meets_fiber {α : Type u_1} {β : Type u_2} [DecidableEq β] [Finite α] [Finite β] {G : Graph α β} [G.Loopless] {n : ℕ} (hD : 1 ≤ bodyBarDim n) {v a b : α} {e₀ : β} (hvG : v ∈ G.vertexSet) (he₀ : e₀ ∉ (G.removeVertex v).edgeSet) (hnp : ∀ (H : Graph α β), ¬H.IsProperRigidSubgraph G n) {X : Set (β × Fin (bodyHingeMult n))} (hX : ((G.splitOff v a b e₀).matroidMG n).IsCircuit X) : (X ∩ edgeFiber e₀ n).Nonempty

Every circuit of M(G̃_v^{ab}) meets the copies of ab (KT eq. (4.10), pp. 665–666; a step of lem:reduction-step): let D ≥ 1, let G be a loopless multigraph with no proper rigid subgraph, let v ∈ V(G), and let e₀ ∉ E(G − v), so that G.splitOff v a b e₀ is G_v^{ab}. Then every circuit X of M(G̃_v^{ab}) meets the copies ẽ₀ = edgeFiber e₀ n of the new edge ab.

Otherwise X is a set of edges of (G_v)̃, where G_v = G - v (edgeSet_mulTilde_splitOff_diff_fiber_of_notMem_removeVertex). As G_v is a subgraph of G_v^{ab} and of G, X is a circuit of M((G_v)̃) and of M(G̃) (matroidMG_restrict_mulTilde). So G[V(X)] is a rigid subgraph of G (circuit_induces_isRigidSubgraph, KT Lemma 3.4). It has the two ends of an edge of X, which differ as G has no loops, and not v, as no edge of G_v is incident with v: it is a proper rigid subgraph, which G has none of. The lemma asks neither that G be minimal nor that v have degree two; splitOff_isMinimalKDof obtains the looplessness from minimality (loopless_of_isMinimalKDof).

Splitting off keeps a minimal 0-dof-graph minimal (lem:reduction-step)

theorem Graph.splitOff_isMinimalKDof {α : Type u_1} {β : Type u_2} [DecidableEq β] [Finite α] [Finite β] {G : Graph α β} {n : ℕ} (hD : 2 ≤ bodyBarDim n) (hV3 : 3 ≤ G.vertexSet.ncard) {v a b : α} {e₀ eₐ e_b : β} (hav : a ≠ v) (hbv : b ≠ v) (hla : G.IsLink eₐ v a) (hlb : G.IsLink e_b v b) (hdeg2 : ∀ (e : β) (x : α), G.IsLink e v x → e = eₐ ∨ e = e_b) (he₀ : e₀ ∉ (G.removeVertex v).edgeSet) (hG : G.IsMinimalKDof n 0) (hnp : ∀ (H : Graph α β), ¬H.IsProperRigidSubgraph G n) : (G.splitOff v a b e₀).IsMinimalKDof n 0

Splitting off keeps a minimal 0-dof-graph minimal (lem:reduction-step (i); KT Lemma 4.8(i), pp. 665–666): let D ≥ 2, and let G be a minimal 0-dof-graph with at least three vertices and no proper rigid subgraph, whose vertex v has exactly the two edges eₐ, e_b (hdeg2), joining it to a, b ≠ v. Then G_v^{ab}, formed with a label e₀ ∉ E(G − v), is a minimal 0-dof-graph. The label may be eₐ or e_b, and the edges need not differ: only the upper bound of dof_tracking is used, and it asks neither.

By splitOff_deficiency_le (KT Lemma 4.3(i)), def(G̃_v^{ab}) ≤ def(G̃) = 0, so G_v^{ab} is a 0-dof-graph. The subgraph G_v = G - v has the |V(G)| - 1 ≥ 2 vertices of G other than v, so it is not rigid, and def((G_v)̃) > 0: the case k = 0 of KT Lemma 4.7. By circuit_splitOff_meets_fiber (KT eq. (4.10)), E((G_v)̃) contains no circuit of M(G̃_v^{ab}), so it is the only base of the restriction M((G_v)̃), and KT eq. (2.4) (isBase_ncard_add_deficiency_eq) gives |E((G_v)̃)| < D(|V(G)| - 2), the size of a base B' of M(G̃_v^{ab}). If B' missed the copies ẽ of an edge e of G_v^{ab}, it would have at most |E((G_v)̃)| elements: for e = e₀ it lies in E((G_v)̃), and otherwise it has at most D - 1 copies of ab and misses the D - 1 elements of ẽ ⊆ E((G_v)̃). Katoh and Tanigawa end instead by exchanging the copies of ab in such a base for copies of e, along the circuits of KT eq. (4.10); the count replaces the exchange. The three vertices are needed: splitting off a vertex of the two-vertex double edge leaves a loop at one vertex, a 0-dof-graph that is not minimal.

KT Theorem 4.9 and the induction for KT Theorem 5.5 (sec:molecular-induction-thm49)

Katoh and Tanigawa reduce a minimal 0-dof-graph with at least two vertices to the two-vertex double edge, by splitting off at vertices of degree two and contracting proper rigid subgraphs (KT Theorem 4.9, pp. 666–667). minimal_kdof_reduction is the induction principle from which it follows, and minimal_kdof_reduction_all_k the induction over all deficiencies of their proof of Theorem 5.5 (p. 671). Splitting off takes the two edges at the vertex as data, which the first lemma finds.

theorem Graph.exists_splitOff_data_of_degree_eq_two {α : Type u_1} {β : Type u_2} [Finite α] [Finite β] {G : Graph α β} {n : ℕ} (hD1 : 1 ≤ bodyBarDim n) (hG0 : G.IsKDof n 0) {v b₀ : α} (hvG : v ∈ G.vertexSet) (hb₀G : b₀ ∈ G.vertexSet) (hb₀v : b₀ ≠ v) (hdeg : G.degree v = 2) : ∃ (a : α) (b : α) (eₐ : β) (e_b : β), a ≠ v ∧ b ≠ v ∧ a ∈ G.vertexSet ∧ b ∈ G.vertexSet ∧ eₐ ≠ e_b ∧ G.IsLink eₐ v a ∧ G.IsLink e_b v b ∧ ∀ (e : β) (x : α), G.IsLink e v x → e = eₐ ∨ e = e_b

The two edges at a vertex of degree two of a 0-dof-graph (a step of thm:minimal-kdof-reduction, lem:chain-cycle-dichotomy, lem:chain-data-of-noRigid and lem:case-III): let D ≥ 1, let G be a 0-dof-graph, and let v ∈ V(G) have degree two, with another vertex b₀ of G. Then two edges eₐ ≠ e_b join v to vertices a, b ≠ v of G, and every edge at v is one of them. The degree counts each loop at v twice and each other edge at v once (degree_eq_ncard_add_ncard, of the Matroid package), and at least two edges join v to the other vertices (two_le_crossingEdges_of_isKDof_zero, KT Lemma 3.1, lem:two-edge-conn, at the cut between {v} and the rest, whose crossing edges are not loops). So v has no loop and two other edges. The vertex b₀ is needed only for the cut.

A vertex of degree two in a minimal 0-dof-graph

Case III of the algebraic induction (lem:case-III) takes one when the graph has three vertices.

theorem Graph.exists_degree_eq_two_of_noRigid {α : Type u_1} {β : Type u_2} [DecidableEq β] [Finite α] [Finite β] {G : Graph α β} {n : ℕ} (hD : 3 ≤ bodyBarDim n) (hV2 : 2 ≤ G.vertexSet.ncard) (hG : G.IsMinimalKDof n 0) (hnp : ∀ (H : Graph α β), ¬H.IsProperRigidSubgraph G n) : ∃ v ∈ G.vertexSet, G.degree v = 2

A vertex of degree two in a minimal 0-dof-graph (a step of lem:case-III; from the proof of KT Lemma 4.6, p. 664): let D ≥ 3, and let G be a minimal 0-dof-graph with at least two vertices and no proper rigid subgraph. Then some v ∈ V(G) has degree two. exists_degree_le_two (lem:low-degree-vertex) gives a vertex of degree at most two, and every vertex of a 0-dof-graph with at least two vertices has degree at least two (two_le_degree_of_isKDof_zero, lem:deficiency-zero-connected). It is the case k = 0 of exists_degree_eq_two (lem:reducible-vertex), without that lemma's hypothesis of 2-edge-connectivity, which a 0-dof-graph has (KT Lemma 3.1).

A chain b v a c when d ≥ 3 (lem:chain-data-of-noRigid)

For d = 3, Katoh and Tanigawa's Case III starts from such a chain (KT §6.4.1, p. 680). Case III here extracts a chain of length d at every d (chainData_extract, lem:chain-data-extract), and does not use this lemma.

theorem Graph.exists_chain_data_of_noRigid {α : Type u_1} {β : Type u_2} [DecidableEq β] [Finite α] [Finite β] {G : Graph α β} {n : ℕ} (hD : 6 ≤ bodyBarDim n) (hV4 : 4 ≤ G.vertexSet.ncard) (hG : G.IsMinimalKDof n 0) (hnp : ∀ (H : Graph α β), ¬H.IsProperRigidSubgraph G n) : ∃ (v : α) (a : α) (b : α) (c : α) (eₐ : β) (e_b : β) (e_c : β), v ∈ G.vertexSet ∧ a ∈ G.vertexSet ∧ b ∈ G.vertexSet ∧ c ∈ G.vertexSet ∧ a ≠ v ∧ b ≠ v ∧ b ≠ a ∧ c ≠ v ∧ c ≠ a ∧ b ≠ c ∧ eₐ ≠ e_b ∧ eₐ ≠ e_c ∧ G.IsLink eₐ v a ∧ G.IsLink e_b v b ∧ G.IsLink e_c a c ∧ (∀ (e : β) (x : α), G.IsLink e v x → e = eₐ ∨ e = e_b) ∧ ∀ (e : β) (x : α), G.IsLink e a x → e = eₐ ∨ e = e_c

A chain b v a c whose inner vertices have degree two (lem:chain-data-of-noRigid; KT §6.4.1, p. 680): let D ≥ 6, that is d ≥ 3, and let G be a minimal 0-dof-graph with at least four vertices and no proper rigid subgraph. Then G has distinct vertices v, a, b, c and edges eₐ = va, e_b = vb and e_c = ac, with eₐ ≠ e_b and eₐ ≠ e_c, such that eₐ and e_b are the only edges at v, and eₐ and e_c the only edges at a.

exists_adjacent_degree_two_pair (lem:adjacent-degree-two-pair) gives adjacent vertices v and a of degree two, joined by eₐ, and exists_splitOff_data_of_degree_eq_two gives the two edges at each. As G is simple (simple_of_isMinimalKDof_of_noRigid), the other edge at v joins it to a vertex b ∉ {v, a} (IsLink.unique_edge), and the other edge at a joins it to a vertex c ∉ {v, a}. If b = c, the three edges form a triangle, a proper rigid subgraph of G as |V(G)| ≥ 4 (triangle_isProperRigidSubgraph), which G has none of.

The two inductions (thm:minimal-kdof-reduction, thm:minimal-kdof-reduction-all-k)

theorem Graph.minimal_kdof_reduction {α : Type u_1} {β : Type u_2} [DecidableEq β] [Finite α] [Finite β] {n : ℕ} (hD : 3 ≤ bodyBarDim n) {P : Graph α β → Prop} (hbase : ∀ (G : Graph α β), G.IsMinimalKDof n 0 → G.vertexSet.ncard = 2 → P G) (hsplit : ∀ (G : Graph α β) (v a b : α) (eₐ e_b : β), G.IsMinimalKDof n 0 → (∀ (H : Graph α β), ¬H.IsProperRigidSubgraph G n) → v ∈ G.vertexSet → a ≠ v → b ≠ v → a ∈ G.vertexSet → b ∈ G.vertexSet → eₐ ≠ e_b → G.IsLink eₐ v a → G.IsLink e_b v b → (∀ (e : β) (x : α), G.IsLink e v x → e = eₐ ∨ e = e_b) → (∀ e₀ ∉ (G.removeVertex v).edgeSet, P (G.splitOff v a b e₀)) → P G) (hcontract : ∀ (G : Graph α β), G.IsMinimalKDof n 0 → 3 ≤ G.vertexSet.ncard → (∃ (H : Graph α β), H.IsProperRigidSubgraph G n) → (∀ (G' : Graph α β), G'.IsMinimalKDof n 0 → 2 ≤ G'.vertexSet.ncard → G'.vertexSet.ncard < G.vertexSet.ncard → P G') → P G) (G : Graph α β) : G.IsMinimalKDof n 0 → 2 ≤ G.vertexSet.ncard → P G

Reduction of minimal 0-dof-graphs (thm:minimal-kdof-reduction (ii); the induction principle of KT Theorem 4.9, pp. 666–667): let D ≥ 3, that is n ≥ 2, and let a property P of multigraphs hold of every minimal 0-dof-graph G in each of three cases:

• hbase: G has two vertices;
• hsplit: G has no proper rigid subgraph, its vertex v has exactly the two edges eₐ ≠ e_b, joining it to a, b ≠ v, and P holds of G_v^{ab}, formed with every label e₀ ∉ E(G − v) (fmlnote:graph-operations: the formal G.splitOff v a b e₀ is G_v^{ab} exactly then);
• hcontract: G has at least three vertices and a proper rigid subgraph, and P holds of every minimal 0-dof-graph with at least two and fewer than |V(G)| vertices.

Then P holds of every minimal 0-dof-graph with at least two vertices, with no condition on the labels: the label eₐ is always admissible (notMem_edgeSet_removeVertex_iff). The proof is an induction on |V(G)|. A graph G with at least three vertices and no proper rigid subgraph is 2-edge-connected (twoEdgeConnected_of_isKDof_zero), so it has a vertex v of degree two (exists_degree_eq_two, lem:reducible-vertex), whose two edges join it to vertices a, b ≠ v (exists_splitOff_data_of_degree_eq_two). Then G_v^{ab} is a minimal 0-dof-graph (splitOff_isMinimalKDof, lem:reduction-step) with one vertex fewer (splitOff_vertexSet_ncard_lt, lem:reduction-measure), and the induction hypothesis gives the premise of hsplit at each admissible label. This is hsplit read as a statement about every formal G_v^{ab}; it implies the form with one label, and the form with a label outside E(G).

The contraction case is given the induction hypothesis at every smaller graph, not the contraction: Katoh and Tanigawa's proof of their Theorem 5.5 needs it at both H and G/E(H) (p. 673), and G/E(H) is again a minimal 0-dof-graph (rigidContract_isMinimalKDof, lem:rigidContract-isMinimalKDof). No declaration uses the theorem; the algebraic induction runs minimal_kdof_reduction_all_k.

KT Theorem 4.9 (i): the reduction sequence

def Graph.KTReductionStep {α : Type u_1} {β : Type u_2} [DecidableEq β] (n : ℕ) (G G' : Graph α β) : Prop

A step of the reduction sequence (a step of thm:minimal-kdof-reduction): G' is a minimal 0-dof-graph obtained from G by KT Theorem 4.9's two operations, a splitting off at a vertex v of degree two with the label e₀ ∉ E(G - v) of the new edge (so that G' is G_v^{ab}, fmlnote:graph-operations), or the contraction of a proper rigid subgraph.

Equations

• One or more equations did not get rendered due to their size.

def Graph.IsDoubleEdge {α : Type u_1} {β : Type u_2} (G : Graph α β) : Prop

The double edge (a step of thm:minimal-kdof-reduction): the graph on two vertices with two edges, each joining them, where the sequence of KT Theorem 4.9 (i) ends.

Equations

• G.IsDoubleEdge = ∃ (x : α) (y : α) (e : β) (f : β), x ≠ y ∧ e ≠ f ∧ G.vertexSet = {x, y} ∧ G.edgeSet = {e, f} ∧ G.IsLink e x y ∧ G.IsLink f x y

theorem Graph.minimal_kdof_reduction_sequence {α : Type u_1} {β : Type u_2} [DecidableEq β] [Finite α] [Finite β] {n : ℕ} (hD : 3 ≤ bodyBarDim n) (G : Graph α β) (hG : G.IsMinimalKDof n 0) (hV : 2 ≤ G.vertexSet.ncard) : ∃ (Gm : Graph α β), Relation.ReflTransGen (KTReductionStep n) G Gm ∧ Gm.IsDoubleEdge

The reduction sequence (thm:minimal-kdof-reduction (i), KT Theorem 4.9, pp. 666–667): let D ≥ 3. A minimal 0-dof-graph G with at least two vertices reduces to a double edge by a finite sequence of steps (KTReductionStep): splitting off at a vertex of degree two, and contracting a proper rigid subgraph. As in Katoh and Tanigawa's proof, it follows from minimal_kdof_reduction with P G the existence of such a sequence. The two-vertex case is isMinimalKDof_ncard_le_two_trichotomy, a split step extends the sequence of G_v^{ab} at the label eₐ, which is always admissible (notMem_edgeSet_removeVertex_iff), and a contraction step extends that of G/E(H). No hypothesis on the labels.

theorem Graph.minimal_kdof_reduction_all_k {α : Type u_1} {β : Type u_2} [DecidableEq β] [Finite α] {n : ℕ} {P : Graph α β → Prop} (hbase : ∀ (k : ℤ) (G : Graph α β), G.IsMinimalKDof n k → G.vertexSet.Nonempty → G.vertexSet.ncard ≤ 2 → P G) (hcut : ∀ (k : ℤ) (G : Graph α β), G.IsMinimalKDof n k → 3 ≤ G.vertexSet.ncard → ¬G.TwoEdgeConnected → (∀ (k' : ℤ) (G' : Graph α β), G'.IsMinimalKDof n k' → G'.vertexSet.Nonempty → G'.vertexSet.ncard < G.vertexSet.ncard → P G') → P G) (hcontract : ∀ (k : ℤ) (G : Graph α β), G.IsMinimalKDof n k → 3 ≤ G.vertexSet.ncard → (∃ (H : Graph α β), H.IsProperRigidSubgraph G n) → (∀ (k' : ℤ) (G' : Graph α β), G'.IsMinimalKDof n k' → G'.vertexSet.Nonempty → G'.vertexSet.ncard < G.vertexSet.ncard → P G') → P G) (hsplitPos : ∀ (k : ℤ) (G : Graph α β), G.IsMinimalKDof n k → 0 < k → 3 ≤ G.vertexSet.ncard → G.TwoEdgeConnected → (∀ (H : Graph α β), ¬H.IsProperRigidSubgraph G n) → (∀ (k' : ℤ) (G' : Graph α β), G'.IsMinimalKDof n k' → G'.vertexSet.Nonempty → G'.vertexSet.ncard < G.vertexSet.ncard → P G') → P G) (hsplitZero : ∀ (G : Graph α β), G.IsMinimalKDof n 0 → 3 ≤ G.vertexSet.ncard → G.TwoEdgeConnected → (∀ (H : Graph α β), ¬H.IsProperRigidSubgraph G n) → (∀ (k' : ℤ) (G' : Graph α β), G'.IsMinimalKDof n k' → G'.vertexSet.Nonempty → G'.vertexSet.ncard < G.vertexSet.ncard → P G') → P G) (k : ℤ) (G : Graph α β) : G.IsMinimalKDof n k → G.vertexSet.Nonempty → P G

Induction over all deficiencies (thm:minimal-kdof-reduction-all-k; the induction of Katoh and Tanigawa's proof of their Theorem 5.5, with its hypothesis KT eq. (6.1), p. 671): let a property P of multigraphs hold of every minimal k-dof-graph G with one or two vertices, for every k (hbase), and of every minimal k-dof-graph G with at least three vertices in each of Katoh and Tanigawa's four cases, given that P holds of every minimal k'-dof-graph with at least one and fewer than |V(G)| vertices, for every k':

• hcut: G is not 2-edge-connected (KT §6.1);
• hcontract: G has a proper rigid subgraph (KT §6.2);
• hsplitPos: G is 2-edge-connected, has no proper rigid subgraph, and k > 0 (KT §6.3);
• hsplitZero: G is 2-edge-connected, has no proper rigid subgraph, and k = 0 (KT §6.4).

Then P holds of every minimal k-dof-graph with a vertex, for every k. The proof is an induction on |V(G)| for all k at once; the four cases cover every G with at least three vertices, as k ≥ 0 when G has a vertex (deficiency_nonneg). The statement asks nothing of D and no finiteness of the labels: each case makes its own reduction. This is the induction that the algebraic induction runs (PanelHingeFramework.theorem_55_minimalKDof_k_all_k); minimal_kdof_reduction (KT Theorem 4.9) is the one for k = 0.

An induction over all multigraphs (sec:pencil-reduction)

The pencil chapter's induction runs over all multigraphs, not only over minimal k-dof-graphs. Without minimality its cases still cover every multigraph: when D ≥ 4, a loopless multigraph with at least three vertices, each of degree at least three, has a proper rigid subgraph (exists_isProperRigidSubgraph_of_three_le_degree, lem:pencil-min-degree-rigid). So if it has none, some vertex has degree less than three, and exactly two when the multigraph is 2-edge-connected (two_le_degree_of_twoEdgeConnected).

theorem Graph.pencil_reduction {α : Type u_1} {β : Type u_2} [Finite α] [Finite β] {n : ℕ} (hD : 6 ≤ bodyBarDim n) {P : Graph α β → Prop} (hloop : ∀ (G : Graph α β), (∃ (e : β) (x : α), G.IsLoopAt e x) → (∀ (G' : Graph α β), G'.vertexSet.Nonempty → G'.vertexSet.ncard < G.vertexSet.ncard ∨ G'.vertexSet.ncard = G.vertexSet.ncard ∧ G'.edgeSet.ncard < G.edgeSet.ncard → P G') → P G) (hbase : ∀ (G : Graph α β), G.Loopless → G.vertexSet.Nonempty → G.vertexSet.ncard ≤ 2 → P G) (hcut : ∀ (G : Graph α β), G.Loopless → 3 ≤ G.vertexSet.ncard → ¬G.TwoEdgeConnected → (∀ (G' : Graph α β), G'.vertexSet.Nonempty → G'.vertexSet.ncard < G.vertexSet.ncard → P G') → P G) (hcontract : ∀ (G : Graph α β), G.Loopless → 3 ≤ G.vertexSet.ncard → (∃ (H : Graph α β), H.IsProperRigidSubgraph G n) → (∀ (G' : Graph α β), G'.vertexSet.Nonempty → G'.vertexSet.ncard < G.vertexSet.ncard → P G') → P G) (hsplit : ∀ (G : Graph α β), G.Loopless → 3 ≤ G.vertexSet.ncard → G.TwoEdgeConnected → (∀ (H : Graph α β), ¬H.IsProperRigidSubgraph G n) → (∃ v ∈ G.vertexSet, G.degree v = 2) → (∀ (G' : Graph α β), G'.vertexSet.Nonempty → G'.vertexSet.ncard < G.vertexSet.ncard → P G') → P G) (G : Graph α β) : G.vertexSet.Nonempty → P G

Reduction on all multigraphs (thm:pencil-reduction; cf. KT Theorem 4.9, without minimality): let D ≥ 6, and let a property P of multigraphs hold of a nonempty multigraph G in each of five cases:

• hloop: G has a loop, and P holds of every nonempty G' smaller in the lexicographic order of (|V(G')|, |E(G')|); deleting the loop keeps |V(G)| and lowers |E(G)|, and this is the only case in which the number of vertices stays;
• hbase: G is loopless with at most two vertices;
• hcut: G is loopless with at least three vertices and not 2-edge-connected;
• hcontract: G is loopless with at least three vertices and has a proper rigid subgraph;
• hsplit: G is loopless and 2-edge-connected, with at least three vertices, no proper rigid subgraph and a vertex of degree two;

the last three given that P holds of every nonempty multigraph with fewer vertices than G, minimal or not. Then P holds of every nonempty multigraph. The proof is an induction on |V(G)| and, for a fixed number of vertices, on |E(G)|. In the last case the vertex of degree two exists: exists_isProperRigidSubgraph_of_three_le_degree, whose bound 4 ≤ D the proof takes from hD, gives a vertex of degree less than three, and two_le_degree_of_twoEdgeConnected gives every vertex degree at least two.

A base of M(G̃) has a balanced partition into forests (lem:balanced-forest-packing)

Katoh and Tanigawa's proof of their Lemma 4.1 (p. 660) assumes a partition of an independent set of M(G̃) into D forests each of which has an edge at v (rem:kt-lemma-41 (2)). A base has one. Its partition into forests (matroidMG_indep_iff_exists_forest_packing) is made disjoint, and the base has at least D copies of the edges at v (isBase_vfiber_ncard_ge). If a forest F_j has no edge at v, these copies lie in the other D - 1 forests, so one of them, F_i, has two. Moving one of the two to F_j (exists_packing_move_of_not_inc) keeps the forests disjoint, as the moved edge lay in F_i only, and F_i keeps the other: the number of forests with no edge at v drops. forest_surgery_split and splitOff_exists_base_inter_fiber_lt use the partition.

theorem Graph.exists_balanced_forest_packing {α : Type u_1} {β : Type u_2} [DecidableEq β] [Finite α] [Finite β] {G : Graph α β} {n : ℕ} (hD : 2 ≤ bodyBarDim n) {v a b : α} {eₐ e_b : β} (hav : a ≠ v) (hbv : b ≠ v) (heab : eₐ ≠ e_b) (hla : G.IsLink eₐ v a) (hlb : G.IsLink e_b v b) (hdeg2 : ∀ (e : β) (x : α), G.IsLink e v x → e = eₐ ∨ e = e_b) {B : Set (β × Fin (bodyHingeMult n))} (hB : (G.matroidMG n).IsBase B) : ∃ (Fs : Fin (bodyBarDim n) → Set (β × Fin (bodyHingeMult n))), ⋃ (i : Fin (bodyBarDim n)), Fs i = B ∧ (∀ (i : Fin (bodyBarDim n)), (G.mulTilde n).cycleMatroid.Indep (Fs i)) ∧ Pairwise (Function.onFun Disjoint Fs) ∧ ∀ (i : Fin (bodyBarDim n)), ∃ p ∈ Fs i, (G.mulTilde n).Inc p v

A base has a balanced partition into forests (lem:balanced-forest-packing; the partition that Katoh and Tanigawa's proof of their Lemma 4.1, p. 660, assumes): let D ≥ 2, and let eₐ ≠ e_b join v to a, b ≠ v and be the only edges at v (hdeg2). Then every base B of M(G̃) is the union of D pairwise disjoint forests of G̃ (sets independent in its cycle matroid), each of which has an edge incident with v.

The proof makes the forests of matroidMG_indep_iff_exists_forest_packing pairwise disjoint (disjointed) and inducts on a bound for the number of forests with no edge at v. By isBase_vfiber_ncard_ge, B has at least D copies of eₐ and e_b, so if Fs j has none, another forest Fs i has two, and one of them moves to Fs j (exists_packing_move_of_not_inc). The forests stay disjoint, Fs j gains an edge at v and Fs i keeps one, so fewer forests have none. For a base, Katoh and Tanigawa's assumption is thus a gap and not an error (rem:kt-lemma-41).

The surgery on a balanced partition (lem:forest-surgery-count, KT Lemma 4.1)

Katoh and Tanigawa's surgery (KT p. 660) on a partition of a set I into D disjoint forests of G̃, each of which has an edge at v. A forest has at most one copy of eₐ and one of e_b, as two copies of an edge form a cycle (fiber_inter_subsingleton_of_isAcyclicSet_mulTilde), so it has one or two edges at v. A forest with two, pa and pb, replaces them by the copy r = (e₀, pa.2) of ab (isAcyclicSet_splitOff_reroute); a forest with one loses it and gains nothing (isAcyclicSet_splitOff_of_diff_fiberAtVertex). Each forest loses one edge, so the new union has |I| - D elements. With h the number of copies of eₐ and e_b in I and h' that of the forests with two, 2h' + (D - h') = h, Katoh and Tanigawa's count; as h ≤ 2(D - 1), h' ≤ D - 2, so the union has fewer than D - 1 copies of ab. The copies r of distinct forests differ, as their pa, copies of eₐ in disjoint forests, differ in their second coordinate.

theorem Graph.forest_surgery_count {α : Type u_1} {β : Type u_2} [DecidableEq β] [Finite β] {G : Graph α β} {n : ℕ} (hD : 2 ≤ bodyBarDim n) {v a b : α} {eₐ e_b e₀ : β} (hab : a ≠ b) (hav : a ≠ v) (hbv : b ≠ v) (heab : eₐ ≠ e_b) (he₀ : e₀ ∉ G.edgeSet) (hla : G.IsLink eₐ v a) (hlb : G.IsLink e_b v b) (hdeg2 : ∀ (e : β) (x : α), G.IsLink e v x → e = eₐ ∨ e = e_b) {I : Set (β × Fin (bodyHingeMult n))} (Fs : Fin (bodyBarDim n) → Set (β × Fin (bodyHingeMult n))) (hcover : ⋃ (i : Fin (bodyBarDim n)), Fs i = I) (hindep : ∀ (i : Fin (bodyBarDim n)), (G.mulTilde n).cycleMatroid.Indep (Fs i)) (hdisj : Pairwise (Function.onFun Disjoint Fs)) (hmeet : ∀ (i : Fin (bodyBarDim n)), ∃ p ∈ Fs i, (G.mulTilde n).Inc p v) : ∃ (Fs' : Fin (bodyBarDim n) → Set (β × Fin (bodyHingeMult n))), (∀ (i : Fin (bodyBarDim n)), ((G.splitOff v a b e₀).mulTilde n).cycleMatroid.Indep (Fs' i)) ∧ Pairwise (Function.onFun Disjoint Fs') ∧ ((G.splitOff v a b e₀).matroidMG n).Indep (⋃ (i : Fin (bodyBarDim n)), Fs' i) ∧ (⋃ (i : Fin (bodyBarDim n)), Fs' i).ncard + bodyBarDim n = I.ncard ∧ ((⋃ (i : Fin (bodyBarDim n)), Fs' i) ∩ edgeFiber e₀ n).ncard < bodyHingeMult n

The surgery on a balanced partition (lem:forest-surgery-count; the surgery of KT Lemma 4.1, p. 660): let D ≥ 2, and let eₐ ≠ e_b join v to vertices a ≠ b of G, both ≠ v, and be the only edges at v (hdeg2). Let Fs : Fin D → Set _ be pairwise disjoint forests of G̃ with union I, each of which has an edge incident with v. Then, for a label e₀ ∉ E(G), there are pairwise disjoint forests Fs' of G̃_v^{ab} whose union I' is independent in M(G̃_v^{ab}), with |I'| + D = |I| and fewer than D - 1 copies of ab (|I' ∩ ẽ₀| < bodyHingeMult n): KT Lemma 4.1's two conclusions, for the partition of a base that exists_balanced_forest_packing gives. forest_surgery_split and splitOff_exists_base_inter_fiber_lt apply it.

Splitting off does not raise the deficiency, by the surgery (lem:forest-surgery-split)

theorem Graph.forest_surgery_split {α : Type u_1} {β : Type u_2} [Finite α] [Finite β] {G : Graph α β} {n : ℕ} (hD : 2 ≤ bodyBarDim n) {v a b : α} {eₐ e_b e₀ : β} (hab : a ≠ b) (hav : a ≠ v) (hbv : b ≠ v) (heab : eₐ ≠ e_b) (hla : G.IsLink eₐ v a) (hlb : G.IsLink e_b v b) (hdeg2 : ∀ (e : β) (x : α), G.IsLink e v x → e = eₐ ∨ e = e_b) (he₀ : e₀ ∉ G.edgeSet) : (G.splitOff v a b e₀).deficiency n ≤ G.deficiency n

Splitting off does not raise the deficiency, by the surgery (lem:forest-surgery-split, which cor:forest-surgery-deficiency restates; KT eq. (4.1), p. 661, from KT Lemma 4.1): let D ≥ 2, and let eₐ ≠ e_b join v to vertices a ≠ b, both ≠ v, and be the only edges at v (hdeg2). Then def(G̃_v^{ab}) ≤ def(G̃), for a label e₀ ∉ E(G). A base B of M(G̃) has a balanced partition into forests (exists_balanced_forest_packing), and the surgery on it (forest_surgery_count) gives an independent set of M(G̃_v^{ab}) with |B| - D elements. As G_v^{ab} has one vertex fewer than G, KT eq. (2.4) (isBase_ncard_add_deficiency_eq, rank_add_deficiency_eq) gives the bound, as Katoh and Tanigawa derive their eq. (4.1). splitOff_deficiency_le (lem:splitoff-deficiency) proves it by comparing the values of partitions, for D ≥ 1 and without a ≠ b, and the formal proof of KT Theorem 5.5 uses that lemma (rem:forest-surgery-kt-steps).

KT Lemma 4.3(ii), the forward half (lem:splitoff-kdof-criterion)

theorem Graph.splitOff_exists_base_inter_fiber_lt {α : Type u_1} {β : Type u_2} [DecidableEq β] [Finite α] [Finite β] {G : Graph α β} {n : ℕ} {k : ℤ} (hD : 2 ≤ bodyBarDim n) {v a b : α} {eₐ e_b e₀ : β} (hab : a ≠ b) (hav : a ≠ v) (hbv : b ≠ v) (heab : eₐ ≠ e_b) (hla : G.IsLink eₐ v a) (hlb : G.IsLink e_b v b) (hdeg2 : ∀ (e : β) (x : α), G.IsLink e v x → e = eₐ ∨ e = e_b) (he₀ : e₀ ∉ G.edgeSet) (hG : G.IsKDof n k) (hH : (G.splitOff v a b e₀).IsKDof n k) : ∃ (B' : Set (β × Fin (bodyHingeMult n))), ((G.splitOff v a b e₀).matroidMG n).IsBase B' ∧ (B' ∩ edgeFiber e₀ n).ncard < bodyHingeMult n

A base with few copies of ab when splitting off keeps the deficiency (lem:splitoff-kdof-criterion, the forward half; KT Lemma 4.3(ii), p. 661): let D ≥ 2, let G be a k-dof-graph, and let eₐ ≠ e_b join v to vertices a ≠ b, both ≠ v, and be the only edges at v (hdeg2). If G_v^{ab}, formed with a label e₀ ∉ E(G), is also a k-dof-graph, then M(G̃_v^{ab}) has a base B' with fewer than D - 1 copies of ab (|B' ∩ ẽ₀| < bodyHingeMult n), so a copy of ab lies outside B'. A base B of M(G̃) has a balanced partition into forests (exists_balanced_forest_packing), and the surgery on it (forest_surgery_count) gives an independent set I' of M(G̃_v^{ab}) with |I'| = |B| - D and fewer than D - 1 copies of ab. By KT eq. (2.4), |B| = D(|V(G)| - 1) - k, and the rank of M(G̃_v^{ab}) is D(|V(G)| - 2) - k = |I'|, so I' is a base (Indep.isBase_of_ncard). This is Katoh and Tanigawa's proof, with the balanced partition that it assumes (rem:kt-lemma-41).

G - v is a minimal k'-dof-graph with k' ≤ D - 2 (lem:case-III-gap3-minimalKDof)

theorem Graph.splitOff_removeVertex_minimalKDof {α : Type u_1} {β : Type u_2} [DecidableEq β] [Finite α] [Finite β] {G : Graph α β} {n : ℕ} (hD : 2 ≤ bodyBarDim n) {v a b : α} {eₐ e_b e₀ : β} (hab : a ≠ b) (hav : a ≠ v) (hbv : b ≠ v) (heab : eₐ ≠ e_b) (hla : G.IsLink eₐ v a) (hlb : G.IsLink e_b v b) (hdeg2 : ∀ (e : β) (x : α), G.IsLink e v x → e = eₐ ∨ e = e_b) (he₀ : e₀ ∉ G.edgeSet) (hG : G.IsMinimalKDof n 0) : (G.removeVertex v).IsMinimalKDof n ((G.removeVertex v).deficiency n) ∧ 0 ≤ (G.removeVertex v).deficiency n ∧ (G.removeVertex v).deficiency n ≤ ↑(bodyBarDim n) - 2

G - v is a minimal k'-dof-graph with k' ≤ D - 2 (lem:case-III-gap3-minimalKDof; from the proof of KT Claim 6.11, p. 684): let D ≥ 2, let G be a minimal 0-dof-graph, and let eₐ ≠ e_b join v to vertices a ≠ b, both ≠ v, and be the only edges at v (hdeg2). Then G_v = G - v is a minimal k'-dof-graph for k' = def((G_v)̃), and 0 ≤ k' ≤ D - 2.

The minimality is KT Lemma 3.3 (subgraph_minimality), and k' ≥ 0 as G_v has the vertex a (deficiency_nonneg). For the upper bound, G_v^{ab}, formed with a label e₀ ∉ E(G), is a 0-dof-graph (splitOff_deficiency_le), so M(G̃_v^{ab}) has a base B' with h = |B' ∩ ẽ₀| < D - 1 (splitOff_exists_base_inter_fiber_lt) and D(|V(G)| - 2) elements (KT eq. (2.4)). The set B' ∖ ẽ₀ is a set of edges of (G_v)̃ (edgeSet_mulTilde_splitOff_diff_fiber), independent in M((G_v)̃), the restriction of M(G̃_v^{ab}) (matroidMG_restrict_mulTilde, as G_v ≤ G_v^{ab} by removeVertex_le_splitOff). So rank M((G_v)̃) ≥ |B'| - h, and KT eq. (2.4) for G_v gives k' ≤ h ≤ D - 2. PanelHingeFramework.exists_nested_rankPolynomial_lower_all_k (lem:case-III-nested-rank-lower, KT eq. (6.22)) uses the lemma.

KT Lemma 4.3(ii), the backward half (lem:splitoff-kdof-criterion)

theorem Graph.splitOff_isKDof_of_exists_base_inter_fiber_lt {α : Type u_1} {β : Type u_2} [DecidableEq β] [Finite α] [Finite β] {G : Graph α β} {n : ℕ} {k : ℤ} (hD : 2 ≤ bodyBarDim n) {v a b : α} {eₐ e_b e₀ : β} (hab : a ≠ b) (hav : a ≠ v) (hbv : b ≠ v) (heab : eₐ ≠ e_b) (hla : G.IsLink eₐ v a) (hlb : G.IsLink e_b v b) (hdeg2 : ∀ (e : β) (x : α), G.IsLink e v x → e = eₐ ∨ e = e_b) (he₀ : e₀ ∉ G.edgeSet) (hG : G.IsKDof n k) {B' : Set (β × Fin (bodyHingeMult n))} (hB' : ((G.splitOff v a b e₀).matroidMG n).IsBase B') (hlt : (B' ∩ edgeFiber e₀ n).ncard < bodyHingeMult n) : (G.splitOff v a b e₀).IsKDof n k

Splitting off keeps the deficiency when a base has few copies of ab (lem:splitoff-kdof-criterion, the backward half; KT Lemma 4.3(ii), p. 661): let D ≥ 2, let G be a k-dof-graph, and let eₐ ≠ e_b join v to vertices a ≠ b, both ≠ v, and be the only edges at v (hdeg2). If M(G̃_v^{ab}), for G_v^{ab} formed with a label e₀ ∉ E(G), has a base B' with fewer than D - 1 copies of ab, then G_v^{ab} is a k-dof-graph. By case (i) of KT Lemma 4.2 (splitOff_indep_extend_of_fiber_lt), M(G̃) has an independent set with |B'| + D elements, so KT eq. (2.4) gives def(G̃_v^{ab}) ≥ k, and the upper bound of KT Lemma 4.3(i) (splitOff_deficiency_le) gives def(G̃_v^{ab}) ≤ k.

The second assertion of KT Lemma 4.4 (lem:removal-deficiency-equality)

theorem Graph.exists_isBase_vb_fiber_eq_one_of_removeVertex_isKDof {α : Type u_1} {β : Type u_2} [DecidableEq β] [Finite α] [Finite β] {G : Graph α β} {n : ℕ} {k : ℤ} (hD : 2 ≤ bodyBarDim n) {v a b : α} {eₐ e_b e₀ : β} (hab : a ≠ b) (hav : a ≠ v) (hbv : b ≠ v) (heab : eₐ ≠ e_b) (hla : G.IsLink eₐ v a) (hlb : G.IsLink e_b v b) (he₀ : e₀ ∉ G.edgeSet) (hG : G.IsKDof n k) (hGv : (G.removeVertex v).IsKDof n k) : ∃ (B : Set (β × Fin (bodyHingeMult n))), (G.matroidMG n).IsBase B ∧ (B ∩ edgeFiber e_b n).ncard = 1

A base with one copy of e_b when removal keeps the deficiency (lem:removal-deficiency-equality; the second assertion of KT Lemma 4.4, p. 662): let D ≥ 2, let G be a k-dof-graph, and let eₐ ≠ e_b join v to vertices a ≠ b, both ≠ v. If G_v = G - v is also a k-dof-graph, then M(G̃) has a base B with |B ∩ ẽ_b| = 1. A base B' of M((G_v)̃) is independent in M(G̃_v^{ab}), for G_v^{ab} formed with a label e₀ ∉ E(G), as G_v ≤ G_v^{ab} (removeVertex_le_splitOff, matroidMG_restrict_mulTilde), and it has no copy of ab. Case (i) of KT Lemma 4.2 (splitOff_indep_extend_of_fiber_lt) extends it to an independent set I of M(G̃) with |I| = |B'| + D and |I ∩ ẽ_b| = 1, and KT eq. (2.4) gives |I| = D(|V(G)| - 1) - k, the rank of M(G̃): I is a base. This is Katoh and Tanigawa's proof. The lemma does not ask v to have degree two.

KT Lemma 4.7 (lem:removal-deficiency-strict)

theorem Graph.removeVertex_deficiency_gt_of_noRigid {α : Type u_1} {β : Type u_2} [DecidableEq β] [Finite α] [Finite β] {G : Graph α β} {n : ℕ} {k : ℤ} (hD : 3 ≤ bodyBarDim n) {v a b : α} {eₐ e_b e₀ : β} (hab : a ≠ b) (hav : a ≠ v) (hbv : b ≠ v) (heab : eₐ ≠ e_b) (hla : G.IsLink eₐ v a) (hlb : G.IsLink e_b v b) (hdeg2 : ∀ (e : β) (x : α), G.IsLink e v x → e = eₐ ∨ e = e_b) (he₀ : e₀ ∉ G.edgeSet) (hG : G.IsMinimalKDof n k) (hnp : ∀ (H : Graph α β), ¬H.IsProperRigidSubgraph G n) : k < (G.removeVertex v).deficiency n

Removal raises the deficiency (lem:removal-deficiency-strict; KT Lemma 4.7, p. 665): let D ≥ 3, let G be a minimal k-dof-graph with no proper rigid subgraph, and let eₐ ≠ e_b join v to vertices a ≠ b, both ≠ v, and be the only edges at v (hdeg2). Then def((G_v)̃) > k, where G_v = G - v. KT Lemma 4.4 (removeVertex_deficiency_ge) gives def((G_v)̃) ≥ k; suppose equality. If k = 0, G_v is a rigid subgraph of G whose vertices, those of G other than v, include a ≠ b: a proper rigid subgraph. If k > 0, the second assertion of KT Lemma 4.4 (exists_isBase_vb_fiber_eq_one_of_removeVertex_isKDof, with a label e₀ ∉ E(G)) gives a base B of M(G̃) with |B ∩ ẽ_b| = 1; but B = E(G̃) (KT Lemma 4.5(ii), isBase_eq_edgeSet_mulTilde_of_noRigid_of_pos), which has all D - 1 ≥ 2 copies of e_b. This is Katoh and Tanigawa's proof.

KT Lemma 4.8(ii) (lem:reduction-step-pos)

theorem Graph.splitOff_isMinimalKDof_of_pos {α : Type u_1} {β : Type u_2} [DecidableEq β] [Finite α] [Finite β] {G : Graph α β} {n : ℕ} {k : ℤ} (hD : 3 ≤ bodyBarDim n) (hk : 0 < k) {v a b : α} {eₐ e_b e₀ : β} (hab : a ≠ b) (hav : a ≠ v) (hbv : b ≠ v) (heab : eₐ ≠ e_b) (hla : G.IsLink eₐ v a) (hlb : G.IsLink e_b v b) (hdeg2 : ∀ (e : β) (x : α), G.IsLink e v x → e = eₐ ∨ e = e_b) (he₀ : e₀ ∉ G.edgeSet) (hG : G.IsMinimalKDof n k) (hnp : ∀ (H : Graph α β), ¬H.IsProperRigidSubgraph G n) : (G.splitOff v a b e₀).IsMinimalKDof n (k - 1)

Splitting off when k > 0 (lem:reduction-step-pos; KT Lemma 4.8(ii), pp. 665–666): let D ≥ 3, let G be a minimal k-dof-graph with k > 0 and no proper rigid subgraph, and let eₐ ≠ e_b join v to vertices a ≠ b, both ≠ v, and be the only edges at v (hdeg2). Then H = G_v^{ab}, formed with a label e₀ ∉ E(G), is a minimal (k-1)-dof-graph. The proof has three steps.

(1) def(H̃) is k - 1 or k (dof_tracking).

(2) def(H̃) ≠ k, as in Katoh and Tanigawa's proof (p. 666). Otherwise KT Lemma 4.3(ii) (splitOff_exists_base_inter_fiber_lt) gives a base B' of M(H̃) that misses a copy p of ab. Let X be the fundamental circuit of p with respect to B', and G' = H[V(X)], a rigid subgraph of H (circuit_induces_isRigidSubgraph). If V(G') = V(H), then rank M(H̃) ≥ rank M(G̃') = D(|V(H)| - 1) (rank_matroidMG_of_isKDof_zero), and def(H̃) ≤ 0 < k. So V(G') ⊊ V(H), and V(G') contains a and b, the ends of p. Let K = G[V(G') ∪ {v}], so that K_v^{ab} = G' (induce_insert_splitOff). The set I = X ∖ {p} is independent in M(G̃') with D(|V(G')| - 1) elements (circuit_induces_isTight), and it has fewer than D - 1 copies of ab, as I ⊆ B'. Case (i) of KT Lemma 4.2 for K (splitOff_indep_extend_of_fiber_lt) extends it to an independent set of M(K̃) with D(|V(K)| - 1) elements, so K is a proper rigid subgraph of G, which G has none of.

(3) H is minimal, by Katoh and Tanigawa's proof of the minimality in KT Lemma 4.3 (p. 661). Let a base B' of M(H̃) miss the copies ẽ of an edge e of H. If B' missed a copy of ab, then def(H̃) = k by KT Lemma 4.3(ii) (splitOff_isKDof_of_exists_base_inter_fiber_lt); so B' has all of them, and e is none of e₀, eₐ and e_b. Case (ii) of KT Lemma 4.2 (splitOff_indep_extend_of_fiber_subset) extends B' to an independent set J of M(G̃) with |B'| + D - 1 elements and J ∖ (ẽₐ ∪ ẽ_b) = B' ∖ ẽ₀. By KT eq. (2.4), J is a base of M(G̃), and it misses ẽ, against the minimality of G.