Pruning a degree-one vertex

This is the structural inverse to LeafExtension.addLeaf. From a vertex of valence exactly one we construct the graph on the remaining subtype, identify the unique neighbor, and exhibit the original graph as a LaplacianEquiv of the corresponding explicit leaf extension. The rank-one lifting theorem is then an immediate composition of the two small certificate interfaces.

@[reducible, inline]

abbrev Utilities.Certificate.LeafPruning.Remaining (G : CFGraph) (leaf : G.V) : Type u

The vertices remaining after deleting leaf.

Equations

• Utilities.Certificate.LeafPruning.Remaining G leaf = { x : G.V // x ≠ leaf }

The unique neighbor of a degree-one vertex

structure Utilities.Certificate.LeafPruning.LeafData (G : CFGraph) (leaf : G.V) : Type u

The unique neighbor and edge-count facts certified by a degree-one leaf.

• root : G.V

  The unique neighbor of the leaf, joined to it by exactly one edge occurrence.

• count_root : numEdges G leaf self.root = 1
• count_other (x : G.V) : x ≠ self.root → numEdges G leaf x = 0

theorem Utilities.Certificate.LeafPruning.exists_leafData (G : CFGraph) (leaf : G.V) (hDegree : vertexDegree G leaf = 1) : Nonempty (LeafData G leaf)

noncomputable def Utilities.Certificate.LeafPruning.leafData (G : CFGraph) (leaf : G.V) (hDegree : vertexDegree G leaf = 1) : LeafData G leaf

Choose the unique-neighbor data supplied by the hypothesis that the leaf has degree one.

Equations

• Utilities.Certificate.LeafPruning.leafData G leaf hDegree = Classical.choice ⋯

noncomputable def Utilities.Certificate.LeafPruning.root (G : CFGraph) (leaf : G.V) (hDegree : vertexDegree G leaf = 1) : Remaining G leaf

The leaf's neighbor regarded as a vertex of the graph remaining after deletion of the leaf.

Equations

• Utilities.Certificate.LeafPruning.root G leaf hDegree = ⟨(Utilities.Certificate.LeafPruning.leafData G leaf hDegree).root, ⋯⟩

def Utilities.Certificate.LeafPruning.NonLeafEdge (G : CFGraph) (leaf : G.V) (edge : G.V × G.V) : Prop

An edge has both endpoints away from the deleted leaf.

Equations

• Utilities.Certificate.LeafPruning.NonLeafEdge G leaf edge = (edge.1 ≠ leaf ∧ edge.2 ≠ leaf)

noncomputable def Utilities.Certificate.LeafPruning.keptEdges (G : CFGraph) (leaf : G.V) : Multiset (G.V × G.V)

The original edges with both endpoints different from the deleted leaf.

Equations

• Utilities.Certificate.LeafPruning.keptEdges G leaf = Multiset.filter (Utilities.Certificate.LeafPruning.NonLeafEdge G leaf) G.edges

def Utilities.Certificate.LeafPruning.restrictEdge (G : CFGraph) (leaf : G.V) (edge : G.V × G.V) (hEdge : NonLeafEdge G leaf edge) : Remaining G leaf × Remaining G leaf

Regard an edge avoiding the deleted leaf as an edge on the remaining vertices.

Equations

• Utilities.Certificate.LeafPruning.restrictEdge G leaf edge hEdge = (⟨edge.1, ⋯⟩, ⟨edge.2, ⋯⟩)

@[reducible, inline]

noncomputable abbrev Utilities.Certificate.LeafPruning.deleteLeaf (G : CFGraph) (leaf : G.V) (hDegree : vertexDegree G leaf = 1) : CFGraph

Delete leaf, retaining precisely the edges whose endpoints remain.

Equations

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

@[simp]

theorem Utilities.Certificate.LeafPruning.deleteLeaf_edges (G : CFGraph) (leaf : G.V) (hDegree : vertexDegree G leaf = 1) : (deleteLeaf G leaf hDegree).edges = Multiset.pmap (restrictEdge G leaf) (keptEdges G leaf) ⋯

@[simp]

theorem Utilities.Certificate.LeafPruning.num_edges_deleteLeaf (G : CFGraph) (leaf : G.V) (hDegree : vertexDegree G leaf = 1) (x y : Remaining G leaf) : numEdges (deleteLeaf G leaf hDegree) x y = numEdges G ↑x ↑y

Deleting a leaf does not change edge multiplicities among old vertices.

Structural equivalence and rank-one lifting

noncomputable def Utilities.Certificate.LeafPruning.rootInDeleteLeaf (G : CFGraph) (leaf : G.V) (hDegree : vertexDegree G leaf = 1) : (deleteLeaf G leaf hDegree).V

The chosen neighbor, regarded as a vertex of the bundled pruned graph.

Equations

• Utilities.Certificate.LeafPruning.rootInDeleteLeaf G leaf hDegree = id (Utilities.Certificate.LeafPruning.root G leaf hDegree)

@[simp]

theorem Utilities.Certificate.LeafPruning.mk_eq_rootInDeleteLeaf_iff (G : CFGraph) (leaf : G.V) (hDegree : vertexDegree G leaf = 1) (x : G.V) (hx : x ≠ leaf) : (have this := ⟨x, hx⟩; this) = rootInDeleteLeaf G leaf hDegree ↔ x = (leafData G leaf hDegree).root

noncomputable def Utilities.Certificate.LeafPruning.vertexEquiv (G : CFGraph) (leaf : G.V) (hDegree : vertexDegree G leaf = 1) : G.V ≃ (LeafExtension.addLeaf (deleteLeaf G leaf hDegree) (rootInDeleteLeaf G leaf hDegree)).V

The canonical relabeling from the original vertices to a new leaf plus the remaining vertices.

Equations

• Utilities.Certificate.LeafPruning.vertexEquiv G leaf hDegree = id (Equiv.optionSubtypeNe leaf).symm

@[simp]

theorem Utilities.Certificate.LeafPruning.vertexEquiv_leaf (G : CFGraph) (leaf : G.V) (hDegree : vertexDegree G leaf = 1) : (vertexEquiv G leaf hDegree) leaf = none

@[simp]

theorem Utilities.Certificate.LeafPruning.vertexEquiv_of_ne (G : CFGraph) (leaf : G.V) (hDegree : vertexDegree G leaf = 1) (x : G.V) (hx : x ≠ leaf) : (vertexEquiv G leaf hDegree) x = some ⟨x, hx⟩

noncomputable def Utilities.Certificate.LeafPruning.laplacianEquivDeleteLeafAddLeaf (G : CFGraph) (leaf : G.V) (hDegree : vertexDegree G leaf = 1) : LaplacianEquiv G (LeafExtension.addLeaf (deleteLeaf G leaf hDegree) (rootInDeleteLeaf G leaf hDegree))

A graph with a degree-one vertex is the explicit leaf extension of the graph on the remaining subtype, up to Laplacian-preserving relabeling.

Equations

• Utilities.Certificate.LeafPruning.laplacianEquivDeleteLeafAddLeaf G leaf hDegree = { toEquiv := Utilities.Certificate.LeafPruning.vertexEquiv G leaf hDegree, num_edges_eq := ⋯ }

theorem Utilities.Certificate.LeafPruning.bnExists_rank_one_of_deleteLeaf (G : CFGraph) (leaf : G.V) (_hG : graphConnected G) (hDegree : vertexDegree G leaf = 1) {d : ℤ} (hPruned : BNExists (deleteLeaf G leaf hDegree) 1 d) : BNExists G 1 d

Rank-one Brill--Noether existence on the pruned graph lifts back to the original connected graph. The local lifting calculation uses only the exact valence-one hypothesis.