Rank transport under an adjacency-preserving vertex equivalence

This file provides a narrow graph-transport layer for chip-firing certificates. Two CFGraphs are related when a vertex equivalence preserves every edge multiplicity. That is exactly the data used by prin, so divisors, firing scripts, winnability, rank bounds, and Brill--Noether existence transport without requiring a general graph isomorphism API.

structure Utilities.Certificate.LaplacianEquiv (G : CFGraph) (H : CFGraph) : Type (max u v)

A vertex equivalence preserving the multiplicity of every unordered edge.

The name emphasizes the only graph structure used below: preservation of the chip-firing Laplacian. No equality of the oriented edge multisets is required.

• toEquiv : G.V ≃ H.V

  The vertex equivalence preserving edge multiplicities, hence transporting the graph Laplacian.

• num_edges_eq (x y : G.V) : numEdges H (self.toEquiv x) (self.toEquiv y) = numEdges G x y

@[instance_reducible]

instance Utilities.Certificate.LaplacianEquiv.instCoeFunForallV {G : CFGraph} {H : CFGraph} : CoeFun (LaplacianEquiv G H) fun (x : LaplacianEquiv G H) => G.V → H.V

Equations

• Utilities.Certificate.LaplacianEquiv.instCoeFunForallV = { coe := fun (equivalence : Utilities.Certificate.LaplacianEquiv G H) => ⇑equivalence.toEquiv }

def Utilities.Certificate.LaplacianEquiv.trans {G : CFGraph} {H : CFGraph} {K : CFGraph} (first : LaplacianEquiv G H) (second : LaplacianEquiv H K) : LaplacianEquiv G K

Compose adjacency-preserving vertex equivalences. This belongs in the basic transport API rather than in a particular subdivision construction, so proof-carrying normalization certificates can combine independent graph presentations without changing universes.

Equations

• first.trans second = { toEquiv := first.toEquiv.trans second.toEquiv, num_edges_eq := ⋯ }

def Utilities.Certificate.LaplacianEquiv.symm {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) : LaplacianEquiv H G

Reverse an adjacency-preserving vertex equivalence.

Equations

• equivalence.symm = { toEquiv := equivalence.toEquiv.symm, num_edges_eq := ⋯ }

def Utilities.Certificate.LaplacianEquiv.mapDiv {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) (D : CFDiv G) : CFDiv H

Transport a divisor forward along the vertex equivalence.

Equations

• equivalence.mapDiv D y = D (equivalence.toEquiv.symm y)

def Utilities.Certificate.LaplacianEquiv.mapScript {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) (script : firingScript G) : firingScript H

Transport a firing script forward along the vertex equivalence.

Equations

• equivalence.mapScript script y = script (equivalence.toEquiv.symm y)

@[simp]

theorem Utilities.Certificate.LaplacianEquiv.mapDiv_apply {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) (D : CFDiv G) (y : H.V) : equivalence.mapDiv D y = D (equivalence.toEquiv.symm y)

@[simp]

theorem Utilities.Certificate.LaplacianEquiv.mapScript_apply {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) (script : firingScript G) (y : H.V) : equivalence.mapScript script y = script (equivalence.toEquiv.symm y)

@[simp]

theorem Utilities.Certificate.LaplacianEquiv.symm_mapDiv {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) (D : CFDiv G) : equivalence.symm.mapDiv (equivalence.mapDiv D) = D

@[simp]

theorem Utilities.Certificate.LaplacianEquiv.mapDiv_symm {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) (D : CFDiv H) : equivalence.mapDiv (equivalence.symm.mapDiv D) = D

@[simp]

theorem Utilities.Certificate.LaplacianEquiv.mapDiv_zero {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) : equivalence.mapDiv 0 = 0

@[simp]

theorem Utilities.Certificate.LaplacianEquiv.mapDiv_add {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) (D E : CFDiv G) : equivalence.mapDiv (D + E) = equivalence.mapDiv D + equivalence.mapDiv E

@[simp]

theorem Utilities.Certificate.LaplacianEquiv.mapDiv_sub {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) (D E : CFDiv G) : equivalence.mapDiv (D - E) = equivalence.mapDiv D - equivalence.mapDiv E

@[simp]

theorem Utilities.Certificate.LaplacianEquiv.mapDiv_neg {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) (D : CFDiv G) : equivalence.mapDiv (-D) = -equivalence.mapDiv D

@[simp]

theorem Utilities.Certificate.LaplacianEquiv.mapDiv_one_chip {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) (x : G.V) : equivalence.mapDiv (oneChip x) = oneChip (equivalence.toEquiv x)

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

Vertex valence is preserved by an adjacency-preserving equivalence.

theorem Utilities.Certificate.LaplacianEquiv.effective_mapDiv_iff {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) (D : CFDiv G) : effective (equivalence.mapDiv D) ↔ effective D

Effectivity is unchanged by relabeling vertices.

@[simp]

theorem Utilities.Certificate.LaplacianEquiv.deg_mapDiv {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) (D : CFDiv G) : CFDiv.degree (equivalence.mapDiv D) = CFDiv.degree D

Divisor degree is unchanged by relabeling vertices.

theorem Utilities.Certificate.LaplacianEquiv.mapDiv_prin {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) (script : firingScript G) : equivalence.mapDiv ((prin G) script) = (prin H) (equivalence.mapScript script)

The principal divisor of a transported firing script is the transported principal divisor.

theorem Utilities.Certificate.LaplacianEquiv.linearEquiv_mapDiv {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) {D E : CFDiv G} (h : linearEquiv G D E) : linearEquiv H (equivalence.mapDiv D) (equivalence.mapDiv E)

Linear equivalence transports forward.

theorem Utilities.Certificate.LaplacianEquiv.linearEquiv_mapDiv_iff {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) (D E : CFDiv G) : linearEquiv H (equivalence.mapDiv D) (equivalence.mapDiv E) ↔ linearEquiv G D E

Linear equivalence is unchanged by relabeling vertices.

theorem Utilities.Certificate.LaplacianEquiv.winnable_mapDiv {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) {D : CFDiv G} (h : winnable G D) : winnable H (equivalence.mapDiv D)

Winnability transports forward.

theorem Utilities.Certificate.LaplacianEquiv.winnable_mapDiv_iff {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) (D : CFDiv G) : winnable H (equivalence.mapDiv D) ↔ winnable G D

Winnability is unchanged by relabeling vertices.

theorem Utilities.Certificate.LaplacianEquiv.rank_geq_mapDiv_iff {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) (D : CFDiv G) (k : ℤ) : rankGeq H (equivalence.mapDiv D) k ↔ rankGeq G D k

Every rank lower-bound predicate is unchanged by relabeling vertices.

theorem Utilities.Certificate.LaplacianEquiv.rank_mapDiv_ge_iff {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) (D : CFDiv G) (k : ℤ) : rank H (equivalence.mapDiv D) ≥ k ↔ rank G D ≥ k

Numerical rank lower bounds are unchanged by relabeling vertices.

theorem Utilities.Certificate.LaplacianEquiv.graphConnected {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) (hG : _root_.graphConnected G) : _root_.graphConnected H

Graph connectivity is preserved by an adjacency-preserving vertex equivalence.

theorem Utilities.Certificate.LaplacianEquiv.graphConnected_iff {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) : _root_.graphConnected G ↔ _root_.graphConnected H

Connectivity is unchanged by a Laplacian-preserving relabeling.

theorem Utilities.Certificate.LaplacianEquiv.bnExists_iff {G : CFGraph} {H : CFGraph} (equivalence : LaplacianEquiv G H) (r d : ℤ) : BNExists G r d ↔ BNExists H r d

Brill--Noether existence is unchanged by an adjacency-preserving vertex equivalence. The proof transports only the requested rank lower bound; it does not require a general equality theorem for ranks.

A closed parallel-edge relabeling example

@[reducible, inline]

abbrev Utilities.Certificate.LaplacianEquiv.Examples.PairVertex : Type

Vertex labels for the closed two-vertex example.

Equations

• Utilities.Certificate.LaplacianEquiv.Examples.PairVertex = Fin 2

def Utilities.Certificate.LaplacianEquiv.Examples.parallelPair : CFGraph

Two vertices joined by two parallel edges.

Equations

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

def Utilities.Certificate.LaplacianEquiv.Examples.relabeledParallelPair : CFGraph

The same parallel pair with both endpoint labels exchanged.

Equations

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

def Utilities.Certificate.LaplacianEquiv.Examples.parallelPairEquiv : LaplacianEquiv parallelPair relabeledParallelPair

Swapping the two labels preserves every Laplacian entry, including the off-diagonal multiplicity two.

Equations

• Utilities.Certificate.LaplacianEquiv.Examples.parallelPairEquiv = { toEquiv := Equiv.swap 0 1, num_edges_eq := Utilities.Certificate.LaplacianEquiv.Examples.parallelPairEquiv._proof_1 }

theorem Utilities.Certificate.LaplacianEquiv.Examples.parallelPair_multiplicity_relabeling : numEdges parallelPair 0 1 = 2 ∧ numEdges relabeledParallelPair (parallelPairEquiv.toEquiv 0) (parallelPairEquiv.toEquiv 1) = 2