Controlled graph-contraction certificates

This is a deliberately one-way quotient interface. A certificate records a surjective vertex map whose inter-fibre edge multiplicities agree exactly with the target graph. Edges inside one fibre are intentionally unconstrained: they are the contracted edges and disappear from the quotient Laplacian.

The resulting pushforward transports explicit chip-firing witnesses from the source to the target. It does not assert that arbitrary divisor rank is preserved by contraction.

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

Passive data for a graph quotient/contraction. The validity predicate, rather than the data structure, records the quotient equations.

• vertexMap : G.V → H.V

  The proposed map from source vertices to quotient vertices; the separate validity predicate certifies the contraction equations.

def Utilities.Certificate.GraphContractionCertificate.precomposeLaplacianEquiv {G : CFGraph} {H : CFGraph} {G' : CFGraph} (c : GraphContractionCertificate G H) (equivalence : LaplacianEquiv G' G) : GraphContractionCertificate G' H

Reindex the source of a contraction certificate along a checked Laplacian-preserving relabeling. The quotient target is left unchanged.

This is a change of names on source vertices, not a rank-transport claim through a contraction.

Equations

• c.precomposeLaplacianEquiv equivalence = { vertexMap := c.vertexMap ∘ ⇑equivalence.toEquiv }

@[simp]

theorem Utilities.Certificate.GraphContractionCertificate.precomposeLaplacianEquiv_vertexMap {G : CFGraph} {H : CFGraph} {G' : CFGraph} (c : GraphContractionCertificate G H) (equivalence : LaplacianEquiv G' G) (x : G'.V) : (c.precomposeLaplacianEquiv equivalence).vertexMap x = c.vertexMap (equivalence.toEquiv x)

def Utilities.Certificate.GraphContractionCertificate.postcomposeLaplacianEquiv {G : CFGraph} {H : CFGraph} {H' : CFGraph} (c : GraphContractionCertificate G H) (equivalence : LaplacianEquiv H H') : GraphContractionCertificate G H'

Reindex the target of a contraction certificate along a checked Laplacian-preserving relabeling. This only changes the names of quotient vertices; it is not a claim that rank descends through a contraction.

Equations

• c.postcomposeLaplacianEquiv equivalence = { vertexMap := ⇑equivalence.toEquiv ∘ c.vertexMap }

@[simp]

theorem Utilities.Certificate.GraphContractionCertificate.postcomposeLaplacianEquiv_vertexMap {G : CFGraph} {H : CFGraph} {H' : CFGraph} (c : GraphContractionCertificate G H) (equivalence : LaplacianEquiv H H') (x : G.V) : (c.postcomposeLaplacianEquiv equivalence).vertexMap x = equivalence.toEquiv (c.vertexMap x)

def Utilities.Certificate.GraphContractionCertificate.Valid {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) : Prop

The exact quotient condition. It is imposed only for distinct target vertices: source edges internal to one fibre are precisely the edges which are contracted, so no equation is required on the diagonal.

Equations

• c.Valid = (Function.Surjective c.vertexMap ∧ ∀ (a b : H.V), a ≠ b → numEdges H a b = ∑ x : G.V, ∑ y : G.V, if c.vertexMap x = a ∧ c.vertexMap y = b then numEdges G x y else 0)

theorem Utilities.Certificate.GraphContractionCertificate.valid_precomposeLaplacianEquiv {G : CFGraph} {H : CFGraph} {G' : CFGraph} (c : GraphContractionCertificate G H) (equivalence : LaplacianEquiv G' G) (hValid : c.Valid) : (c.precomposeLaplacianEquiv equivalence).Valid

Validity is invariant under a checked reindexing of the source graph. The proof uses the vertex equivalence twice to reindex the two source sums; edge multiplicities are then exactly LaplacianEquiv.num_edges_eq.

theorem Utilities.Certificate.GraphContractionCertificate.valid_postcomposeLaplacianEquiv {G : CFGraph} {H : CFGraph} {H' : CFGraph} (c : GraphContractionCertificate G H) (equivalence : LaplacianEquiv H H') (hValid : c.Valid) : (c.postcomposeLaplacianEquiv equivalence).Valid

Validity is invariant under a checked relabeling of the quotient target. The source fibres are unchanged; the proof only rewrites their two target labels through the vertex equivalence.

def Utilities.Certificate.GraphContractionCertificate.check {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) : Bool

Boolean replay of the finite quotient conditions.

Equations

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

@[simp]

theorem Utilities.Certificate.GraphContractionCertificate.check_eq_true_iff {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) : c.check = true ↔ c.Valid

def Utilities.Certificate.GraphContractionCertificate.pushDiv {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (D : CFDiv G) : CFDiv H

Push a divisor forward by summing it over fibres.

Equations

• c.pushDiv D b = ∑ x : G.V, if c.vertexMap x = b then D x else 0

def Utilities.Certificate.GraphContractionCertificate.pullScript {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (tau : firingScript H) : firingScript G

Pull a firing script back by composition with the quotient map.

Equations

• c.pullScript tau x = tau (c.vertexMap x)

@[simp]

theorem Utilities.Certificate.GraphContractionCertificate.pushDiv_apply {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (D : CFDiv G) (b : H.V) : c.pushDiv D b = ∑ x : G.V, if c.vertexMap x = b then D x else 0

@[simp]

theorem Utilities.Certificate.GraphContractionCertificate.pullScript_apply {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (tau : firingScript H) (x : G.V) : c.pullScript tau x = tau (c.vertexMap x)

@[simp]

theorem Utilities.Certificate.GraphContractionCertificate.pushDiv_zero {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) : c.pushDiv 0 = 0

@[simp]

theorem Utilities.Certificate.GraphContractionCertificate.pushDiv_add {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (D E : CFDiv G) : c.pushDiv (D + E) = c.pushDiv D + c.pushDiv E

@[simp]

theorem Utilities.Certificate.GraphContractionCertificate.pushDiv_sub {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (D E : CFDiv G) : c.pushDiv (D - E) = c.pushDiv D - c.pushDiv E

@[simp]

theorem Utilities.Certificate.GraphContractionCertificate.pushDiv_one_chip {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (x : G.V) : c.pushDiv (oneChip x) = oneChip (c.vertexMap x)

Fibre summation sends one chip to the one chip at its image.

theorem Utilities.Certificate.GraphContractionCertificate.effective_pushDiv {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) {D : CFDiv G} (hD : effective D) : effective (c.pushDiv D)

Fibre summation preserves effectivity.

@[simp]

theorem Utilities.Certificate.GraphContractionCertificate.deg_pushDiv {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (D : CFDiv G) : CFDiv.degree (c.pushDiv D) = CFDiv.degree D

Fibre summation preserves total degree.

theorem Utilities.Certificate.GraphContractionCertificate.pushDiv_prin_pullScript {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hValid : c.Valid) (tau : firingScript H) : c.pushDiv ((prin G) (c.pullScript tau)) = (prin H) tau

The quotient Laplacian identity. Only pulled-back scripts are claimed to commute with contraction; this is the precise amount of compatibility needed to push explicit reachability certificates forward.

def Utilities.Certificate.GraphContractionCertificate.PushableWinnable {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (X : CFDiv G) : Prop

An explicit source winnability witness whose script is pulled back from the target. This is the reusable certificate-level notion: it is stronger than merely being winnable on G, and therefore has a sound quotient image.

Equations

• c.PushableWinnable X = ∃ (tau : firingScript H), effective (X + (prin G) (c.pullScript tau))

theorem Utilities.Certificate.GraphContractionCertificate.winnable_pushDiv_of_pushableWinnable {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hValid : c.Valid) {X : CFDiv G} (hX : c.PushableWinnable X) : winnable H (c.pushDiv X)

A pulled-back source witness pushes to an ordinary winnability witness on the quotient.

def Utilities.Certificate.GraphContractionCertificate.PushableReaches {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (D : CFDiv G) (x : G.V) : Prop

The source divisor reaches x by a script that descends to the quotient. The definition deliberately retains the source representative: different vertices of one contracted fibre may have different source witnesses.

Equations

• c.PushableReaches D x = c.PushableWinnable (D - oneChip x)

def Utilities.Certificate.GraphContractionCertificate.PushableReachabilityAtRepresentatives {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (D : CFDiv G) : Prop

A fibre-wise certificate: every chosen target fibre has one source representative with a pushable removed-chip witness. This is the minimal condition needed for rank one on the quotient.

Equations

• c.PushableReachabilityAtRepresentatives D = ∀ (b : H.V), ∃ (x : G.V), c.vertexMap x = b ∧ c.PushableReaches D x

def Utilities.Certificate.GraphContractionCertificate.FibreConstantPushableReachability {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (D : CFDiv G) : Prop

A stronger, fibre-constant form useful when certificates are generated by one rule per target fibre rather than by a selected representative.

Equations

• c.FibreConstantPushableReachability D = ∀ (b : H.V) (x : G.V), c.vertexMap x = b → c.PushableReaches D x

theorem Utilities.Certificate.GraphContractionCertificate.pushableReachabilityAtRepresentatives_of_fibreConstant {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hValid : c.Valid) (D : CFDiv G) (hFibre : c.FibreConstantPushableReachability D) : c.PushableReachabilityAtRepresentatives D

theorem Utilities.Certificate.GraphContractionCertificate.reaches_pushDiv_of_pushableReaches {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hValid : c.Valid) {D : CFDiv G} {x : G.V} (hReach : c.PushableReaches D x) : StrongSeparator.Reaches H (c.pushDiv D) (c.vertexMap x)

A pushable removed-chip witness at x proves reachability at its quotient vertex.

theorem Utilities.Certificate.GraphContractionCertificate.reaches_all_pushDiv_of_pushableRepresentatives {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hValid : c.Valid) {D : CFDiv G} (hReach : c.PushableReachabilityAtRepresentatives D) (b : H.V) : StrongSeparator.Reaches H (c.pushDiv D) b

Reachability at representatives gives reachability at every target vertex after contraction.

theorem Utilities.Certificate.GraphContractionCertificate.rank_ge_one_of_reaches_all {K : CFGraph} {D : CFDiv K} (hReach : ∀ (q : K.V), StrongSeparator.Reaches K D q) : rank K D ≥ 1

Reaching every vertex is exactly the rank-one test, spelled out here so the contraction interface has no hidden dependence on a rank-preservation claim.

theorem Utilities.Certificate.GraphContractionCertificate.rank_ge_one_pushDiv_of_pushableRepresentatives {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hValid : c.Valid) {D : CFDiv G} (hReach : c.PushableReachabilityAtRepresentatives D) : rank H (c.pushDiv D) ≥ 1

Rank one on the quotient from pushable source reachability at target representatives.

theorem Utilities.Certificate.GraphContractionCertificate.bnExists_pushDiv_of_pushableRepresentatives {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hValid : c.Valid) (D : CFDiv G) (d : ℤ) (hDegree : CFDiv.degree D = d) (hReach : c.PushableReachabilityAtRepresentatives D) : BNExists H 1 d

A compact one-way Brill--Noether package for quotient certificates.

theorem Utilities.Certificate.GraphContractionCertificate.graphConnected {G : CFGraph} {H : CFGraph} (c : GraphContractionCertificate G H) (hValid : c.Valid) (hConnected : _root_.graphConnected G) : _root_.graphConnected H

A valid surjective contraction carries connected graphs to connected graphs. The proof pulls a target cut back to the full preimage cut in the source; a source crossing edge contributes a positive summand to the exact off-diagonal fibre-multiplicity equation.