The fossil of a chip-firing graph

In this library, fossil is a deliberately short name for the graph's degree-one Abel--Jacobi image. For a connected graph this is the construction usually called its 2-edge-connectivization: contract every separating edge, map the remaining edge occurrences across the quotient, and discard the loops created by contraction. “Fossil” is local terminology, not a replacement for either standard name in mathematical prose.

Concretely, two vertices have the same fossil image when their one-chip divisors are linearly equivalent.

This module begins with the quotient construction and its canonical divisor pushforward. The main objective is to prove that this pushforward identifies the divisor class groups, hence preserves winnability, rank, and Brill--Noether existence. Unlike a chosen sequence of bridge contractions, the fossil is canonical and can therefore serve as a common target for constructions which differ only by attached trees.

Vertex classes and the quotient graph

def Utilities.chipEquivalent (G : CFGraph) (v w : G.V) : Prop

Two vertices belong to the same fossil class when their one-chip divisors are linearly equivalent.

Equations

• Utilities.chipEquivalent G v w = linearEquiv G (oneChip v) (oneChip w)

def Utilities.chipSetoid (G : CFGraph) : Setoid G.V

Linear equivalence of one-chip divisors, packaged as a setoid.

Equations

• Utilities.chipSetoid G = { r := Utilities.chipEquivalent G, iseqv := ⋯ }

@[reducible, inline]

abbrev Utilities.FossilVertex (G : CFGraph) : Type u

A vertex of the fossil is a linear-equivalence class of vertices.

Equations

• Utilities.FossilVertex G = Quotient (Utilities.chipSetoid G)

def Utilities.fossilVertex (G : CFGraph) (v : G.V) : FossilVertex G

The canonical map from the original vertex set to its fossil classes.

Equations

• Utilities.fossilVertex G v = ⟦v⟧

instance Utilities.fossilVertexNonempty (G : CFGraph) : Nonempty (FossilVertex G)

@[instance_reducible]

noncomputable instance Utilities.fossilVertexDecidableEq (G : CFGraph) : DecidableEq (FossilVertex G)

Equations

• Utilities.fossilVertexDecidableEq G = Classical.decEq (Utilities.FossilVertex G)

@[instance_reducible]

noncomputable instance Utilities.fossilVertexFintype (G : CFGraph) : Fintype (FossilVertex G)

Equations

• Utilities.fossilVertexFintype G = Fintype.ofFinite (Utilities.FossilVertex G)

@[simp]

theorem Utilities.fossilVertex_eq_iff (G : CFGraph) (v w : G.V) : fossilVertex G v = fossilVertex G w ↔ chipEquivalent G v w

def Utilities.fossilEdge (G : CFGraph) (edge : G.V × G.V) : FossilVertex G × FossilVertex G

Map the two endpoints of an edge to their fossil classes.

Equations

• Utilities.fossilEdge G edge = (Utilities.fossilVertex G edge.1, Utilities.fossilVertex G edge.2)

noncomputable def Utilities.fossil (G : CFGraph) : CFGraph

The fossil of G: its degree-one Abel--Jacobi image, equivalently (when G is connected) its 2-edge-connectivization. It quotients vertices by one-chip divisor class and discards edge occurrences that become loops.

Equations

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

@[simp]

theorem Utilities.fossil_edges (G : CFGraph) : (fossil G).edges = Multiset.filter (fun (edge : FossilVertex G × FossilVertex G) => edge.1 ≠ edge.2) (Multiset.map (fossilEdge G) G.edges)

Canonical contraction and divisor pushforward

noncomputable def Utilities.fossilContraction (G : CFGraph) : Certificate.GraphContractionCertificate G (fossil G)

The quotient map, viewed as a graph-contraction certificate.

Equations

• Utilities.fossilContraction G = { vertexMap := Utilities.fossilVertex G }

@[simp]

theorem Utilities.fossilContraction_vertexMap (G : CFGraph) (v : G.V) : (fossilContraction G).vertexMap v = fossilVertex G v

theorem Utilities.fossilContraction_valid (G : CFGraph) : (fossilContraction G).Valid

The fossil really is the quotient graph associated to its vertex map: between two distinct classes its multiplicity is the sum of all source multiplicities between the two fibres.

noncomputable def Utilities.fossilPushforward (G : CFGraph) (D : CFDiv G) : CFDiv (fossil G)

Push a divisor to the fossil by summing its coefficients over each linear-equivalence class of vertices.

Equations

• Utilities.fossilPushforward G D = (Utilities.fossilContraction G).pushDiv D

@[simp]

theorem Utilities.fossilPushforward_apply (G : CFGraph) (D : CFDiv G) (q : FossilVertex G) : fossilPushforward G D q = ∑ v : G.V, if fossilVertex G v = q then D v else 0

@[simp]

theorem Utilities.fossilPushforward_zero (G : CFGraph) : fossilPushforward G 0 = 0

@[simp]

theorem Utilities.fossilPushforward_add (G : CFGraph) (D E : CFDiv G) : fossilPushforward G (D + E) = fossilPushforward G D + fossilPushforward G E

@[simp]

theorem Utilities.fossilPushforward_sub (G : CFGraph) (D E : CFDiv G) : fossilPushforward G (D - E) = fossilPushforward G D - fossilPushforward G E

@[simp]

theorem Utilities.fossilPushforward_one_chip (G : CFGraph) (v : G.V) : fossilPushforward G (oneChip v) = oneChip (fossilVertex G v)

theorem Utilities.effective_fossilPushforward (G : CFGraph) {D : CFDiv G} (hD : effective D) : effective (fossilPushforward G D)

@[simp]

theorem Utilities.deg_fossilPushforward (G : CFGraph) (D : CFDiv G) : CFDiv.degree (fossilPushforward G D) = CFDiv.degree D

noncomputable def Utilities.fossilPushforwardHom (G : CFGraph) : CFDiv G →+ CFDiv (fossil G)

Fibre summation, packaged as an additive homomorphism.

Equations

• Utilities.fossilPushforwardHom G = { toFun := Utilities.fossilPushforward G, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Utilities.fossilPushforwardHom_apply (G : CFGraph) (D : CFDiv G) : (fossilPushforwardHom G) D = fossilPushforward G D

theorem Utilities.fossilPushforward_zsmul (G : CFGraph) (n : ℤ) (D : CFDiv G) : fossilPushforward G (n • D) = n • fossilPushforward G D

A canonical section on divisors

noncomputable def Utilities.fossilRepresentative (G : CFGraph) (q : FossilVertex G) : G.V

A noncomputably chosen original vertex in each fossil class. The mathematical statements below do not depend on this choice.

Equations

• Utilities.fossilRepresentative G q = Classical.choose ⋯

@[simp]

theorem Utilities.fossilVertex_representative (G : CFGraph) (q : FossilVertex G) : fossilVertex G (fossilRepresentative G q) = q

theorem Utilities.divisor_eq_sum_smul_oneChip {K : CFGraph} (D : CFDiv K) : D = ∑ v : K.V, D v • oneChip v

Every divisor is the coefficient-weighted sum of its one-chip divisors.

noncomputable def Utilities.fossilLift (G : CFGraph) (D : CFDiv (fossil G)) : CFDiv G

Lift a fossil divisor by placing the coefficient of each class at its chosen representative.

Equations

• Utilities.fossilLift G D = ∑ q : Utilities.FossilVertex G, D q • oneChip (Utilities.fossilRepresentative G q)

@[simp]

theorem Utilities.fossilPushforward_lift (G : CFGraph) (D : CFDiv (fossil G)) : fossilPushforward G (fossilLift G D) = D

The chosen lift is a right inverse to fibre summation.

noncomputable def Utilities.fossilPullScript (G : CFGraph) (tau : firingScript (fossil G)) : firingScript G

Pull a fossil firing script back to the original graph.

Equations

• Utilities.fossilPullScript G tau = (Utilities.fossilContraction G).pullScript tau

@[simp]

theorem Utilities.fossilPullScript_apply (G : CFGraph) (tau : firingScript (fossil G)) (v : G.V) : fossilPullScript G tau v = tau (fossilVertex G v)

theorem Utilities.fossilPushforward_prin_pullScript (G : CFGraph) (tau : firingScript (fossil G)) : fossilPushforward G ((prin G) (fossilPullScript G tau)) = (prin (fossil G)) tau

The quotient Laplacian identity for the fossil.

The easy half of divisor-class invariance

theorem Utilities.linear_equiv_zsmul {K : CFGraph} {D E : CFDiv K} (h : linearEquiv K D E) (n : ℤ) : linearEquiv K (n • D) (n • E)

Linear equivalence is preserved by integer scaling.

theorem Utilities.linear_equiv_sum {K : CFGraph} {ι : Type u_1} [Fintype ι] {D E : ι → CFDiv K} (h : ∀ (i : ι), linearEquiv K (D i) (E i)) : linearEquiv K (∑ i : ι, D i) (∑ i : ι, E i)

A finite sum of termwise linearly equivalent divisors is linearly equivalent.

theorem Utilities.linear_equiv_one_chip_representative (G : CFGraph) (v : G.V) : linearEquiv G (oneChip v) (oneChip (fossilRepresentative G (fossilVertex G v)))

Each vertex is linearly equivalent, as a one-chip divisor, to the chosen representative of its fossil class.

theorem Utilities.linear_equiv_lift_fossilPushforward (G : CFGraph) (D : CFDiv G) : linearEquiv G D (fossilLift G (fossilPushforward G D))

Every divisor is linearly equivalent to the chosen lift of its pushforward: redistributing chips inside a fossil fibre only moves them between linearly equivalent vertices.

theorem Utilities.linear_equiv_of_fossilPushforward_eq (G : CFGraph) {D E : CFDiv G} (h : fossilPushforward G D = fossilPushforward G E) : linearEquiv G D E

Divisors with the same fossil pushforward are linearly equivalent. Their only difference is redistribution inside the quotient fibres.

theorem Utilities.linear_equiv_of_fossilPushforward (G : CFGraph) {D E : CFDiv G} (h : linearEquiv (fossil G) (fossilPushforward G D) (fossilPushforward G E)) : linearEquiv G D E

Reflection of linear equivalence through the fossil. This is the formal version of pulling a quotient firing script back and observing that the remaining discrepancy only moves chips inside quotient fibres.

theorem Utilities.fossil_chipEquivalent_iff_eq (G : CFGraph) (q r : (fossil G).V) : chipEquivalent (fossil G) q r ↔ q = r

The fossil has no further degree-one vertex identifications: two of its vertices carry equivalent one-chip divisors exactly when they are the same quotient class.

theorem Utilities.fossilVertex_fossil_injective (G : CFGraph) : Function.Injective (fossilVertex (fossil G))

Consequently the second fossil quotient has singleton fibres.

Script descent and class-group invariance

theorem Utilities.fossilPushforward_prin_normalizeScript (G : CFGraph) {x y : G.V} (cut : SeparatingEdgeCut G x y) (sigma : firingScript G) : fossilPushforward G ((prin G) (cut.normalizeScript sigma)) = fossilPushforward G ((prin G) sigma)

Adding the correcting constant on one side of a separating bridge does not change the fossil pushforward of the principal divisor.

noncomputable def Utilities.separatingBadPairs (G : CFGraph) (sigma : firingScript G) : Finset (G.V × G.V)

Ordered separating-edge pairs on which a script has unequal endpoint values. Orienting both ways is harmless and avoids making an arbitrary orientation part of the API.

Equations

• Utilities.separatingBadPairs G sigma = {pair : G.V × G.V | Nonempty (Utilities.SeparatingEdgeCut G pair.1 pair.2) ∧ sigma pair.1 ≠ sigma pair.2}

@[simp]

theorem Utilities.mem_separatingBadPairs_iff (G : CFGraph) (sigma : firingScript G) (pair : G.V × G.V) : pair ∈ separatingBadPairs G sigma ↔ Nonempty (SeparatingEdgeCut G pair.1 pair.2) ∧ sigma pair.1 ≠ sigma pair.2

theorem Utilities.exists_separating_normalization (G : CFGraph) (sigma : firingScript G) : ∃ (normalized : firingScript G), (∀ {x y : G.V} (cut : SeparatingEdgeCut G x y), normalized x = normalized y) ∧ fossilPushforward G ((prin G) normalized) = fossilPushforward G ((prin G) sigma)

Repeatedly applying the one-side constant correction produces a script whose values agree across every separating edge. The corrections never destroy an equality already achieved, because separating cuts do not cross; therefore the finite set of bad endpoint pairs strictly shrinks.

theorem Utilities.exists_fossilScript_pushforward_prin (G : CFGraph) (hConnected : graphConnected G) (sigma : firingScript G) : ∃ (tau : firingScript (fossil G)), fossilPushforward G ((prin G) sigma) = (prin (fossil G)) tau

On a connected graph, every source firing script can be normalized along separating-edge cuts so that it is constant on fossil fibres. Pushing its principal divisor then gives the principal divisor of the descended script.

theorem Utilities.linear_equiv_fossilPushforward (G : CFGraph) (hConnected : graphConnected G) {D E : CFDiv G} (h : linearEquiv G D E) : linearEquiv (fossil G) (fossilPushforward G D) (fossilPushforward G E)

Linear equivalence descends to the fossil.

theorem Utilities.linear_equiv_fossil_iff (G : CFGraph) (hConnected : graphConnected G) (D E : CFDiv G) : linearEquiv G D E ↔ linearEquiv (fossil G) (fossilPushforward G D) (fossilPushforward G E)

On a connected graph, the fossil pushforward identifies divisor classes exactly.

theorem Utilities.effective_fossilLift (G : CFGraph) {D : CFDiv (fossil G)} (hD : effective D) : effective (fossilLift G D)

Lifting an effective fossil divisor at chosen representatives remains effective.

theorem Utilities.winnable_fossil_iff (G : CFGraph) (hConnected : graphConnected G) (D : CFDiv G) : winnable G D ↔ winnable (fossil G) (fossilPushforward G D)

Winnability is invariant under passage to the fossil.

theorem Utilities.rank_geq_fossil_iff (G : CFGraph) (hConnected : graphConnected G) (D : CFDiv G) (k : ℤ) : rankGeq G D k ↔ rankGeq (fossil G) (fossilPushforward G D) k

Every rank inequality is invariant under passage to the fossil.

theorem Utilities.rank_fossilPushforward (G : CFGraph) (hConnected : graphConnected G) (D : CFDiv G) : rank (fossil G) (fossilPushforward G D) = rank G D

Baker--Norine rank is unchanged by passing to the fossil.

theorem Utilities.BNExists_fossil_iff (G : CFGraph) (hConnected : graphConnected G) (r d : ℤ) : BNExists G r d ↔ BNExists (fossil G) r d

Brill--Noether existence is invariant under passage to the fossil.