The combinatorial induction: KT Lemmas 4.5 and 4.6, and the contraction of a subgraph #
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 and D = bodyBarDim n, with G̃ = (D-1)·G and its matroid M(G̃), it proves:
- that a base of
M(G̃)contains at leastDcopies of the two edges at a vertex of degree two (lem:base-vfiber-count), and that an edge atvcan move into a forest with no edge atv(lem:acyclic-insert-vfiber,lem:packing-move), the steps ofrem:kt-lemma-41;sec:molecular-induction-forest; - KT Lemma 4.5 (i) and (ii) (
lem:no-rigid-edge-count,lem:edge-set-indep-pos), and from the proof of KT Lemma 4.6 a vertex of degree at most two and one of degree two (lem:low-degree-vertex,lem:reducible-vertex);sec:molecular-induction-dof; - that a minimal
k-dof-graph with no proper rigid subgraph is simple (lem:simple-minimal-noRigid), and two adjacent vertices of degree two whend ≥ 3(lem:adjacent-degree-two-pair);sec:simplicity-and-adjacent-pair; - that a
0-dof-graph with two vertices is not simple (lem:theorem-55-base-producer); - edge-splitting (
def:graph-operations), the contractionG / E(H)of a subgraph (def:rigid-contraction), and its number of vertices (lem:reduction-measure).
Contraction.lean proves that the contraction of a proper rigid subgraph of a minimal k-dof-graph
is again one.
A base contains D copies of the edges at v (lem:base-vfiber-count) #
A base contains at least D copies of the edges at a vertex of degree two
(lem:base-vfiber-count): let D ≥ 2, and let the edges eₐ ≠ e_b join v to a, b ≠ v and be
the only edges of G at v (hdeg2). Then every base B of M(G̃) contains at least D of the
2(D - 1) copies of eₐ and e_b. The other elements of B are edges of (G_v)̃, where
G_v = G - v, and they are independent in its matroid, a restriction of M(G̃)
(matroidMG_restrict_mulTilde). So KT eq. (2.4) (isBase_ncard_add_deficiency_eq,
rank_add_deficiency_eq) gives |B ∩ (ẽₐ ∪ ẽ_b)| ≥ D + def((G_v)̃) - def(G̃), and KT Lemma 4.4
(removeVertex_deficiency_ge, which uses D ≥ 2) gives def(G̃) ≤ def((G_v)̃). rem:kt-lemma-41
uses the count to partition a base into D forests each of which has an edge at v
(exists_balanced_forest_packing, lem:balanced-forest-packing).
Moving an edge at v into a forest with none (lem:acyclic-insert-vfiber, #
lem:packing-move)
The step of rem:kt-lemma-41 (2): if a forest of a partition of a base of M(G̃) into D forests
has no edge at v, then another has two of the at least D copies at v
(isBase_vfiber_ncard_ge), and moving one of them gives a new partition, as the moved edge is a
pendant edge at v. Each move lowers the number of forests with no edge at v;
exists_balanced_forest_packing (ForestSurgery/Reduction.lean) repeats it.
A forest with no edge at v accepts an edge at v (lem:acyclic-insert-vfiber): let F
be independent in the cycle matroid of G̃ (a forest) with no edge incident with v, and let x
be an edge of G̃ joining v to a vertex w ≠ v. Then insert x F is a forest. In
G̃ ↾ insert x F the only edge at v is x, so deleting x leaves v isolated and separates it
from w (Isolated.connBetween_iff_eq): x is a bridge (IsLink.isBridge_iff_not_connBetween),
and a forest with a bridge added is a forest (IsForest.of_deleteEdges_singleton). The argument
uses only that no edge of F is at v, not the degree of v; it needs w ≠ v, as a loop is a
cycle.
Moving an edge at v into a forest with none (lem:packing-move): let Fs : Fin D → Set _
be forests of G̃ (hindep) with union I (hcover), let no edge of Fs j be incident with v
(hFjv), and let x ∈ I join v to a vertex w ≠ v in G̃. Then the family Fs' with
Fs' j = insert x (Fs j) and Fs' i = Fs i \ {x} for i ≠ j is again a family of forests with
union I: Fs' j is a forest by acyclicSet_insert_vfiber_of_not_inc, the others are subsets of
forests, and x ∈ I moves from the others to Fs' j. The conclusion names the new family, which
exists_balanced_forest_packing uses to keep the forests disjoint and to count those with an edge
at v.
KT Lemma 4.5(i): an edge bound with no proper rigid subgraph (lem:no-rigid-edge-count) #
G̃ has (D - 1)|E(G)| edges (a step of lem:no-rigid-edge-count):
|E(G̃)| = bodyHingeMult n · |E(G)|, as G̃ = (D-1)·G has D - 1 = bodyHingeMult n copies of each
edge of G (edgeMultiply_edgeSet_ncard). It turns a count of the edges of G̃ into one of the
edges of G.
KT Lemma 4.5(i): an edge bound with no proper rigid subgraph (lem:no-rigid-edge-count; KT
p. 663): let D ≥ 2, and let G be a minimal k-dof-graph with a vertex and no proper rigid
subgraph. Then (D - 1)|E(G)| < D(|V(G)| - 1) - k + (D - 1), in ℤ. Katoh and Tanigawa prove it
for k = 0, and the proof follows theirs at every k. If G has no edge, the right side is
rank M(G̃) + D - 1 > 0 (KT eq. (2.4), rank_add_deficiency_eq). Otherwise fix an edge e, and
let B* be a base of M(G̃) meeting ẽ in the least number h* of elements, where h* ≥ 1 as
G is minimal. Every edge f ∉ ẽ of G̃ lies in B* (KT eq. (4.3)). Otherwise its fundamental
circuit X has V(X) = V(G) (fundCircuit_inducedSpan_vertexSet_eq). If X missed ẽ, then X
less one element would be an independent set with D(|V(G)| - 1) elements
(circuit_induces_isTight), so k = 0, and it would be a base missing ẽ. So X contains a copy
e_j ∈ ẽ, and insert f B* \ {e_j} is a base meeting ẽ in h* - 1 elements. Hence
(D - 1)|E(G)| = |B*| + (D - 1 - h*) ≤ D(|V(G)| - 1) - k + (D - 2).
KT Lemma 4.5(ii): E(G̃) is independent when k > 0 (lem:edge-set-indep-pos) #
KT Lemma 4.5(ii): E(G̃) is independent when k > 0 (lem:edge-set-indep-pos; KT p. 663):
let D ≥ 2, and let G be a minimal k-dof-graph with k > 0 and no proper rigid subgraph. Then
E(G̃) is independent in M(G̃). Otherwise it contains a circuit C, and H = G[V(C)] is a rigid
subgraph (circuit_induces_isRigidSubgraph) with at least two vertices, as G has no loops
(loopless_of_isMinimalKDof); so V(H) = V(G). Then M(H̃) has rank D(|V(G)| - 1)
(rank_matroidMG_of_isKDof_zero) and is a restriction of M(G̃) (matroidMG_restrict_mulTilde),
and KT eq. (2.4) (rank_add_deficiency_eq) gives k ≤ 0.
E(G̃) is the only base when k > 0 (lem:edge-set-indep-pos; KT Lemma 4.5(ii)): under
the hypotheses of indep_edgeSet_mulTilde_of_noRigid_of_pos, every base B of M(G̃) is E(G̃),
as E(G̃) is independent and contains B (IsBase.eq_of_subset_indep).
removeVertex_deficiency_gt_of_noRigid (KT Lemma 4.7) uses it.
A vertex of degree two, from the proof of KT Lemma 4.6 (lem:low-degree-vertex, #
lem:reducible-vertex)
A vertex of degree at most two (lem:low-degree-vertex; from the proof of KT Lemma 4.6,
eq. (4.5), p. 664): let D ≥ 3, that is n ≥ 2, and let G be a minimal k-dof-graph with a
vertex and no proper rigid subgraph. Then some v ∈ V(G) has G.degree v ≤ 2. As k ≥ 0, KT
Lemma 4.5(i) (no_rigid_edge_count) gives (D - 1)|E(G)| < D|V(G)| - 1, so 2|E(G)| < 3|V(G)| as
D ≥ 3. The degrees sum to 2|E(G)| (Graph.handshake_degree_subtype, of the Matroid package),
so one of them is less than 3 (Finset.exists_lt_of_sum_lt). exists_degree_eq_two gives a
vertex of degree exactly two.
A vertex of degree two (lem:reducible-vertex; from the proof of KT Lemma 4.6, p. 664): let
D ≥ 3, and let G be a 2-edge-connected minimal k-dof-graph with at least two vertices and no
proper rigid subgraph. Then G has a vertex of degree two: exists_degree_le_two gives one of
degree at most two, and every vertex has degree at least two (two_le_degree_of_twoEdgeConnected,
lem:two-edge-connected-degree).
A minimal k-dof-graph with no proper rigid subgraph is simple #
(lem:simple-minimal-noRigid)
A minimal k-dof-graph with no proper rigid subgraph is simple
(lem:simple-minimal-noRigid; KT p. 677, in the proof of their Lemma 6.7): let D ≥ 2, and let G
be a minimal k-dof-graph with at least three vertices and no proper rigid subgraph. Then G is
simple. It has no loops (loopless_of_isMinimalKDof). If edges e ≠ f joined x and y, then the
subgraph of G with the vertices x, y and the edges e, f would be a 0-dof-graph
(isKDof_zero_of_parallel_pair) with two vertices, fewer than G has: a proper rigid subgraph.
A 0-dof-graph with two vertices is not simple (lem:theorem-55-base-producer) #
A 0-dof-graph with two vertices is not simple (lem:theorem-55-base-producer; KT p. 671):
let D ≥ 1, and let G be a 0-dof-graph with two vertices u and v. Then G is not simple:
at least two edges join u to the other vertex (two_le_crossingEdges_of_isKDof_zero), and each of
them joins u and v. This is the case of two parallel edges of the base case of Katoh and
Tanigawa's induction for their Theorem 5.5 (lem:two-vertex-trichotomy).
Two adjacent vertices of degree two (lem:adjacent-degree-two-pair) #
For d ≥ 3, that is D ≥ 6, a count of degrees gives two adjacent vertices of degree two, where
Katoh and Tanigawa prove their Lemma 4.6 with maximal chains (pp. 664–665).
Two adjacent vertices of degree two (lem:adjacent-degree-two-pair; from KT Lemma 4.6, for
d ≥ 3): let D ≥ 6, and let G be a minimal 0-dof-graph with at least three vertices and no
proper rigid subgraph. Then two adjacent vertices of G have degree two. Suppose not, and let X₂
be the set of vertices of degree two and X₃ that of the others. Two edges of a 0-dof-graph leave
each vertex (two_le_crossingEdges_of_isKDof_zero), so the vertices of X₃ have degree at least
three, and the degrees sum to at least 2|X₂| + 3|X₃|. An edge at a vertex of X₂ has its other
end in X₃, so the degrees on X₂ sum to at most those on X₃ (an exchange of sums over
incFun), and the degrees sum to at least 4|X₂|. Hence 5|E(G)| ≥ 6|V(G)|, against KT
Lemma 4.5(i) (no_rigid_edge_count) at k = 0 as D ≥ 6.
Edge-splitting H_{ab}^v (def:graph-operations; KT p. 660), the reverse of splitting off:
H.edgeSplit a b v e₀ e₁ e₂ has the vertices of H and v. It keeps the edges of H other than
e₀, e₁ and e₂, and it adds e₁ joining a and v when a ∈ V(H), and e₂, if e₂ ≠ e₁,
joining v and b when b ∈ V(H). When e₀ joins a and b in H, v ∉ V(H), and e₁ ≠ e₂
are not edges of H, it replaces the edge e₀ by the path a v b, as Katoh and Tanigawa define
it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The collapse map collapseTo r S (the vertex map of def:rigid-contraction): the map
α → α sending every vertex of S to r and fixing the others.
Instances For
The contraction of a subgraph G / E(H) (def:rigid-contraction): G with the edges of
H deleted and every vertex of V(H) sent to r, (G.deleteEdges E(H)).map (collapseTo r V(H)).
An edge of G not in H keeps its label, and each of its ends in V(H) becomes r. When H is a
rigid subgraph of G with r ∈ V(H) and D ≥ 2, the matroid of (G / E(H))̃ is the contraction
M(G̃) / E(H̃) (matroidMG_rigidContract_eq_contract, Contraction.lean).
Equations
- G.rigidContract H r = Graph.map (Graph.collapseTo r H.vertexSet) (G.deleteEdges H.edgeSet)
Instances For
The contraction has fewer vertices (lem:reduction-measure): if V(H) ⊆ V(G) has at least
two vertices, then |V(G / E(H))| < |V(G)|, as V(G / E(H)) = collapseTo r V(H) '' V(G) lies in
(V(G) \ V(H)) ∪ {r}. KT Theorem 4.9's induction contracts proper rigid subgraphs, which have at
least two vertices, and so lowers the number of vertices (p. 667).
The number of vertices of the contraction (lem:reduction-measure): if r ∈ V(H) and
V(H) ⊆ V(G), then |V(G / E(H))| = (|V(G)| - |V(H)|) + 1, as collapseTo r V(H) maps V(G) onto
(V(G) \ V(H)) ∪ {r}. rigidContract_isMinimalKDof and rigidContract_deficiency_eq
(Contraction.lean) use it to compare D(|V(G / E(H))| - 1) with D(|V(G)| - |V(H)|).
The edges of the contraction (a step of lem:rigidContract-isMinimalKDof):
E(G / E(H)) = E(G) \ E(H), as relabelling the vertices (map) keeps the edges.