Every finite multigraph as a unit subdivision

This module is the base case for a later weighted-core suppression argument. For an arbitrary CFGraph G, it gives every occurrence in the edge multiset its own ordered edge slot, labels the vertices by Fin, assigns length one to every slot, and identifies G with the resulting SubdivisionGraph.Spec.graph by a LaplacianEquiv.

The edge enumeration deliberately uses Mathlib's multiset-as-type G.edges. Thus two equal pairs occurring with multiplicity two give two different terms of G.edges, hence two different slots. No conversion through toFinset is used, so parallel edges are never collapsed.

noncomputable def Utilities.Certificate.UnitSubdivisionPresentation.vertexEquiv (G : CFGraph) : G.V ≃ Fin (Fintype.card G.V)

A fixed finite label for each vertex of G.

Equations

• Utilities.Certificate.UnitSubdivisionPresentation.vertexEquiv G = Fintype.equivFin G.V

noncomputable def Utilities.Certificate.UnitSubdivisionPresentation.edgeEquiv (G : CFGraph) : G.edges.ToType ≃ Fin G.edges.card

A fixed finite label for each occurrence in the edge multiset of G.

The domain is the multiset-as-type: its second dependent coordinate distinguishes repeated copies of the same endpoint pair.

Equations

• Utilities.Certificate.UnitSubdivisionPresentation.edgeEquiv G = ⋯.mp (Fintype.equivFin G.edges.ToType)

noncomputable def Utilities.Certificate.UnitSubdivisionPresentation.edgeOccurrence (G : CFGraph) (slot : Fin G.edges.card) : G.edges.ToType

The actual multiset occurrence occupying an ordered edge slot.

Equations

• Utilities.Certificate.UnitSubdivisionPresentation.edgeOccurrence G slot = (Utilities.Certificate.UnitSubdivisionPresentation.edgeEquiv G).symm slot

noncomputable def Utilities.Certificate.UnitSubdivisionPresentation.edgeAt (G : CFGraph) (slot : Fin G.edges.card) : G.V × G.V

The endpoint pair underlying an ordered edge slot.

Equations

• Utilities.Certificate.UnitSubdivisionPresentation.edgeAt G slot = (Utilities.Certificate.UnitSubdivisionPresentation.edgeOccurrence G slot).fst

@[simp]

theorem Utilities.Certificate.UnitSubdivisionPresentation.edgeEquiv_edgeOccurrence (G : CFGraph) (slot : Fin G.edges.card) : (edgeEquiv G) (edgeOccurrence G slot) = slot

@[simp]

theorem Utilities.Certificate.UnitSubdivisionPresentation.edgeOccurrence_edgeEquiv (G : CFGraph) (occurrence : G.edges.ToType) : edgeOccurrence G ((edgeEquiv G) occurrence) = occurrence

theorem Utilities.Certificate.UnitSubdivisionPresentation.edgeEquiv_inj (G : CFGraph) (first second : G.edges.ToType) : (edgeEquiv G) first = (edgeEquiv G) second ↔ first = second

Distinct multiset occurrences always receive distinct slots, even when their coerced endpoint pairs are equal.

@[simp]

theorem Utilities.Certificate.UnitSubdivisionPresentation.edgeAt_edgeEquiv (G : CFGraph) (occurrence : G.edges.ToType) : edgeAt G ((edgeEquiv G) occurrence) = occurrence.fst

theorem Utilities.Certificate.UnitSubdivisionPresentation.edgeAt_mem (G : CFGraph) (slot : Fin G.edges.card) : edgeAt G slot ∈ G.edges

theorem Utilities.Certificate.UnitSubdivisionPresentation.edgeAt_fst_ne_snd (G : CFGraph) (slot : Fin G.edges.card) : (edgeAt G slot).1 ≠ (edgeAt G slot).2

noncomputable def Utilities.Certificate.UnitSubdivisionPresentation.core (G : CFGraph) : ExplicitPotential.Core (Fintype.card G.V) G.edges.card

The ordered loopless core having one slot for every edge occurrence.

Equations

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

@[simp]

theorem Utilities.Certificate.UnitSubdivisionPresentation.core_tail (G : CFGraph) (slot : Fin G.edges.card) : (core G).tail slot = (vertexEquiv G) (edgeAt G slot).1

@[simp]

theorem Utilities.Certificate.UnitSubdivisionPresentation.core_head (G : CFGraph) (slot : Fin G.edges.card) : (core G).head slot = (vertexEquiv G) (edgeAt G slot).2

theorem Utilities.Certificate.UnitSubdivisionPresentation.core_tail_edgeEquiv (G : CFGraph) (occurrence : G.edges.ToType) : (core G).tail ((edgeEquiv G) occurrence) = (vertexEquiv G) occurrence.fst.1

theorem Utilities.Certificate.UnitSubdivisionPresentation.core_head_edgeEquiv (G : CFGraph) (occurrence : G.edges.ToType) : (core G).head ((edgeEquiv G) occurrence) = (vertexEquiv G) occurrence.fst.2

def Utilities.Certificate.UnitSubdivisionPresentation.unitLength (G : CFGraph) : Fin G.edges.card → ℕ

Every edge occurrence receives length one.

Equations

• Utilities.Certificate.UnitSubdivisionPresentation.unitLength G _slot = 1

@[simp]

theorem Utilities.Certificate.UnitSubdivisionPresentation.unitLength_apply (G : CFGraph) (slot : Fin G.edges.card) : unitLength G slot = 1

noncomputable def Utilities.Certificate.UnitSubdivisionPresentation.spec (G : CFGraph) : SubdivisionGraph.Spec (Fintype.card G.V) G.edges.card

The unit-length subdivision presentation of an arbitrary CFGraph.

Equations

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

@[simp]

theorem Utilities.Certificate.UnitSubdivisionPresentation.spec_length (G : CFGraph) (slot : Fin G.edges.card) : (spec G).length slot = 1

noncomputable def Utilities.Certificate.UnitSubdivisionPresentation.stepEquiv (G : CFGraph) : (spec G).Step ≃ G.edges.ToType

With unit lengths, a unit step is exactly an original edge occurrence.

Equations

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

@[simp]

theorem Utilities.Certificate.UnitSubdivisionPresentation.stepEquiv_apply (G : CFGraph) (step : (spec G).Step) : (stepEquiv G) step = edgeOccurrence G step.fst

@[simp]

theorem Utilities.Certificate.UnitSubdivisionPresentation.stepEquiv_symm_fst (G : CFGraph) (occurrence : G.edges.ToType) : ((stepEquiv G).symm occurrence).fst = (edgeEquiv G) occurrence

theorem Utilities.Certificate.UnitSubdivisionPresentation.noInterior (G : CFGraph) (interior : (spec G).Interior) : False

There are no interior vertices when every slot has length one.

noncomputable def Utilities.Certificate.UnitSubdivisionPresentation.graphVertexEquiv (G : CFGraph) : G.V ≃ (spec G).graph.V

The original vertices are exactly all vertices of the unit subdivision.

Equations

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

@[simp]

theorem Utilities.Certificate.UnitSubdivisionPresentation.graphVertexEquiv_apply (G : CFGraph) (vertex : G.V) : (graphVertexEquiv G) vertex = (spec G).coreVertex ((vertexEquiv G) vertex)

theorem Utilities.Certificate.UnitSubdivisionPresentation.unitEdge_eq (G : CFGraph) (step : (spec G).Step) : (spec G).unitEdge step = ((graphVertexEquiv G) (edgeAt G step.fst).1, (graphVertexEquiv G) (edgeAt G step.fst).2)

The endpoints emitted by a unit step are the relabeled endpoints of its underlying original edge occurrence.

theorem Utilities.Certificate.UnitSubdivisionPresentation.card_filter_occurrences {α : Type u_1} [DecidableEq α] (edges : Multiset α) (predicate : α → Prop) [DecidablePred predicate] : {occurrence : edges.ToType | predicate occurrence.fst}.card = (Multiset.filter predicate edges).card

Filtering the type of occurrences has the same cardinality as filtering the underlying multiset. This is the bookkeeping lemma that retains parallel edge multiplicities in the final numEdges proof.

theorem Utilities.Certificate.UnitSubdivisionPresentation.num_edges_graphVertexEquiv (G : CFGraph) (x y : G.V) : numEdges (spec G).graph ((graphVertexEquiv G) x) ((graphVertexEquiv G) y) = numEdges G x y

Unit subdivision preserves every unordered edge multiplicity.

noncomputable def Utilities.Certificate.UnitSubdivisionPresentation.laplacianEquiv (G : CFGraph) : LaplacianEquiv G (spec G).graph

Every finite loopless multigraph is Laplacian-equivalent to the unit-length subdivision with one distinct slot per edge occurrence.

Equations

• Utilities.Certificate.UnitSubdivisionPresentation.laplacianEquiv G = { toEquiv := Utilities.Certificate.UnitSubdivisionPresentation.graphVertexEquiv G, num_edges_eq := ⋯ }

theorem Utilities.Certificate.UnitSubdivisionPresentation.transmissionExistence_iff (G : CFGraph) (u v : G.V) : TransmissionExistence (spec G).graph ((graphVertexEquiv G) u) ((graphVertexEquiv G) v) ↔ TransmissionExistence G u v

Full finite-length transmission existence is unchanged when an arbitrary finite graph is presented as its occurrence-safe unit subdivision. Parallel edges remain distinct slots, and both marks are carried to their corresponding embedded core vertices.