One-step reduction across a degree-one vertex

LeafPruning identifies a graph with a degree-one vertex, up to a Laplacian-preserving relabeling, with an explicit LeafExtension.addLeaf of the graph obtained by deleting that vertex. This file records the invariant facts needed to use that construction recursively:

• deleting the leaf preserves genus;
• deleting the leaf preserves connectivity when the original graph is connected; and
• a recursive rank-one existence result on the smaller connected graph lifts to the original graph.

The last theorem is deliberately a one-step interface. A global iteration still needs a well-founded wrapper (for example, recursion on the number of vertices) and a choice of a degree-one vertex at every nonterminal step.

theorem Utilities.Certificate.LaplacianEquiv.vertexDegree_eq {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) (x : G.V) : vertexDegree H (equivalence.toEquiv x) = vertexDegree G x

A Laplacian-preserving vertex equivalence preserves every vertex degree.

theorem Utilities.Certificate.LaplacianEquiv.cardEdges_eq {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) : H.edges.card = G.edges.card

A Laplacian-preserving vertex equivalence preserves the edge count.

theorem Utilities.Certificate.LaplacianEquiv.genus_eq {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) : H.genus = G.genus

A Laplacian-preserving vertex equivalence preserves cyclomatic genus.

theorem Utilities.Certificate.LeafReduction.graph_connected_of_addLeaf (H : CFGraph) (root : H.V) (hExtended : graphConnected (LeafExtension.addLeaf H root)) : graphConnected H

If the graph obtained by adjoining a leaf is connected, then the original graph was connected. In the lifted cut, the new leaf is placed on the same side as its root, so the new edge cannot witness the cut.

theorem Utilities.Certificate.LeafReduction.graph_connected_addLeaf_iff (H : CFGraph) (root : H.V) : graphConnected (LeafExtension.addLeaf H root) ↔ graphConnected H

Connectivity is equivalent before and after adjoining one leaf.

theorem Utilities.Certificate.LeafReduction.card_vertices_deleteLeaf_add_one (G : CFGraph) (leaf : G.V) (hDegree : vertexDegree G leaf = 1) : Fintype.card (LeafPruning.deleteLeaf G leaf hDegree).V + 1 = Fintype.card G.V

Deleting one leaf removes exactly one vertex. This is the decreasing measure needed by a future well-founded pruning loop.

theorem Utilities.Certificate.LeafReduction.card_vertices_deleteLeaf_lt (G : CFGraph) (leaf : G.V) (hDegree : vertexDegree G leaf = 1) : Fintype.card (LeafPruning.deleteLeaf G leaf hDegree).V < Fintype.card G.V

The pruned graph is strictly smaller in its number of vertices.

@[simp]

theorem Utilities.Certificate.LeafReduction.genus_deleteLeaf (G : CFGraph) (leaf : G.V) (hDegree : vertexDegree G leaf = 1) : (LeafPruning.deleteLeaf G leaf hDegree).genus = G.genus

Deleting a degree-one vertex preserves genus.

theorem Utilities.Certificate.LeafReduction.graph_connected_deleteLeaf (G : CFGraph) (leaf : G.V) (hG : graphConnected G) (hDegree : vertexDegree G leaf = 1) : graphConnected (LeafPruning.deleteLeaf G leaf hDegree)

Deleting a degree-one vertex from a connected graph leaves a connected graph. No positive-genus assumption is required.

theorem Utilities.Certificate.LeafReduction.graph_connected_deleteLeaf_iff (G : CFGraph) (leaf : G.V) (hDegree : vertexDegree G leaf = 1) : graphConnected (LeafPruning.deleteLeaf G leaf hDegree) ↔ graphConnected G

Under the exact degree-one hypothesis, connectivity is equivalent before and after deleting the leaf.

theorem Utilities.Certificate.LeafReduction.bnExists_rank_one_leafStep (G : CFGraph) (leaf : G.V) (hG : graphConnected G) (hDegree : vertexDegree G leaf = 1) {d : ℤ} (recursive : graphConnected (LeafPruning.deleteLeaf G leaf hDegree) → (LeafPruning.deleteLeaf G leaf hDegree).genus = G.genus → BNExists (LeafPruning.deleteLeaf G leaf hDegree) 1 d) : BNExists G 1 d

One recursive leaf-pruning step for rank-one Brill--Noether existence.

The recursive continuation receives the smaller graph together with the two invariants normally needed by a genus-fixed core classification.

theorem Utilities.Certificate.LeafReduction.bnExists_rank_one_degree_three_genus_four_leafStep (G : CFGraph) (leaf : G.V) (hG : graphConnected G) (hGenus : G.genus = 4) (hDegree : vertexDegree G leaf = 1) (recursive : graphConnected (LeafPruning.deleteLeaf G leaf hDegree) → (LeafPruning.deleteLeaf G leaf hDegree).genus = 4 → BNExists (LeafPruning.deleteLeaf G leaf hDegree) 1 3) : BNExists G 1 3

Genus-four specialization of the recursive leaf-removal step.

theorem Utilities.Certificate.LeafReduction.bnExists_rank_one_of_leafless (targetGenus degree : ℤ) (terminal : ∀ (H : CFGraph), graphConnected H → H.genus = targetGenus → (∀ (vertex : H.V), vertexDegree H vertex ≠ 1) → BNExists H 1 degree) (G : CFGraph) (hG : graphConnected G) (hGenus : G.genus = targetGenus) : BNExists G 1 degree

A rank-one existence theorem for connected leafless graphs of a fixed genus automatically extends across every pendant tree. This genus- and degree-independent form is the pruning boundary needed by the Atanasov--Ranganathan genus-five argument.

theorem Utilities.Certificate.LeafReduction.bnExists_rank_one_degree_three_genus_four_of_leafless (terminal : ∀ (H : CFGraph), graphConnected H → H.genus = 4 → (∀ (vertex : H.V), vertexDegree H vertex ≠ 1) → BNExists H 1 3) (G : CFGraph) (hG : graphConnected G) (hGenus : G.genus = 4) : BNExists G 1 3

A theorem for connected leafless genus-four graphs automatically extends to every connected genus-four graph. The recursion is internal and uses only the strictly decreasing vertex count of deleteLeaf; callers never need to choose or expose a globally pruned graph.