Rigidity of a subdivided cycle

A metric cycle in the subdivision model is represented by two distinct core slots joining two core vertices, each assigned an arbitrary positive integral length. This file proves that every such subdivision has no one-edge cut and therefore satisfies the pointed genus-one rigidity interface.

Two-regular connected graphs have no one-edge cuts

def Utilities.internalDegree (H : CFGraph) (S : Finset H.V) (v : H.V) : ℤ

The contribution to the degree of v from vertices inside S.

Equations

• Utilities.internalDegree H S v = ∑ w ∈ S, ↑(numEdges H v w)

def Utilities.internalMultiplicity (H : CFGraph) (S : Finset H.V) : ℤ

The sum of all directed internal edge multiplicities of S.

Equations

• Utilities.internalMultiplicity H S = ∑ v ∈ S, Utilities.internalDegree H S v

theorem Utilities.vertex_degree_eq_internalDegree_add_outdeg_S (H : CFGraph) (S : Finset H.V) (v : H.V) : vertexDegree H v = internalDegree H S v + outdegreeSet H S v

theorem Utilities.internalMultiplicity_even (H : CFGraph) (S : Finset H.V) : Even (internalMultiplicity H S)

Restricted handshaking: the directed internal multiplicity is even.

theorem Utilities.sum_vertex_degree_eq_internalMultiplicity_add_cutMultiplicity (H : CFGraph) (S : Finset H.V) : ∑ v ∈ S, vertexDegree H v = internalMultiplicity H S + cutMultiplicity H S

Sum the degree decomposition over a vertex set.

theorem Utilities.cutMultiplicity_pos_of_connected {H : CFGraph} (hConnected : graphConnected H) (S : Finset H.V) (hNonempty : S.Nonempty) (hProper : S ≠ Finset.univ) : 0 < cutMultiplicity H S

A nontrivial cut in a connected graph has positive outgoing multiplicity.

theorem Utilities.twoEdgeCutCondition_of_connected_vertexDegree_two {H : CFGraph} (hConnected : graphConnected H) (hDegree : ∀ (vertex : H.V), vertexDegree H vertex = 2) : TwoEdgeCutCondition H

Every connected two-regular loopless multigraph satisfies the two-edge cut condition.

The explicit two-path cycle subdivision

def Utilities.TwoPathCycle.core : Certificate.ExplicitPotential.Core 2 2

The ordered core with two parallel slots from vertex 0 to vertex 1.

Equations

• Utilities.TwoPathCycle.core = { tail := fun (x : Fin 2) => 0, head := fun (x : Fin 2) => 1 }

theorem Utilities.TwoPathCycle.core_connected : core.Connected

def Utilities.TwoPathCycle.spec (length : Fin 2 → ℕ) (hLength : ∀ (edge : Fin 2), 0 < length edge) : Certificate.SubdivisionGraph.Spec 2 2

Two positive subdivided paths with common endpoints.

Equations

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

theorem Utilities.TwoPathCycle.connected (length : Fin 2 → ℕ) (hLength : ∀ (edge : Fin 2), 0 < length edge) : graphConnected (spec length hLength).graph

theorem Utilities.TwoPathCycle.genus_one (length : Fin 2 → ℕ) (hLength : ∀ (edge : Fin 2), 0 < length edge) : (spec length hLength).graph.genus = 1

Valence calculation for the explicit cycle

theorem Utilities.Certificate.SubdivisionGraph.Spec.vertex_degree_coreVertex_eq_incidentSlots {n p : ℕ} (spec : Spec n p) (vertex : Fin n) : vertexDegree spec.graph (spec.coreVertex vertex) = ∑ edge : Fin p, ((if spec.core.tail edge = vertex then 1 else 0) + if spec.core.head edge = vertex then 1 else 0)

A core vertex has one incident unit edge for every core slot incident to it. Parallel slots are retained separately.

theorem Utilities.Certificate.SubdivisionGraph.Spec.vertex_degree_interiorVertex_eq_two {n p : ℕ} (spec : Spec n p) (edge : Fin p) (offset : Fin (spec.length edge - 1)) : vertexDegree spec.graph (spec.interiorVertex edge offset) = 2

Every interior subdivision vertex has valence exactly two.

Cycle cut condition and pointed rigidity

theorem Utilities.TwoPathCycle.vertex_degree_two (length : Fin 2 → ℕ) (hLength : ∀ (edge : Fin 2), 0 < length edge) (vertex : (spec length hLength).graph.V) : vertexDegree (spec length hLength).graph vertex = 2

theorem Utilities.TwoPathCycle.twoEdgeCutCondition (length : Fin 2 → ℕ) (hLength : ∀ (edge : Fin 2), 0 < length edge) : TwoEdgeCutCondition (spec length hLength).graph

theorem Utilities.TwoPathCycle.exists_vertex_ne (length : Fin 2 → ℕ) (hLength : ∀ (edge : Fin 2), 0 < length edge) (marked : (spec length hLength).graph.V) : ∃ (other : (spec length hLength).graph.V), other ≠ marked

theorem Utilities.TwoPathCycle.pointedGenusOneRigid (length : Fin 2 → ℕ) (hLength : ∀ (edge : Fin 2), 0 < length edge) (marked : (spec length hLength).graph.V) : PointedGenusOneRigid (spec length hLength).graph marked

Every marked vertex of every positive two-path subdivision is a pointed rigid genus-one graph.