One-edge subdivision refinement

An edge refinement replaces one ordered edge occurrence by two positive-length occurrences through a new bivalent core vertex. This file provides proof-carrying transport across that operation.

The fully proved part is deliberately occurrence-based:

• a bijection of subdivision vertices and a bijection of emitted unit steps, preserving each unordered endpoint pair, produce a LaplacianEquiv;
• the canonical split core and its positive-length SubdivisionGraph.Spec are constructed without collapsing parallel slots;
• the canonical split's vertex and unit-step equivalences, and the resulting canonicalSplitLaplacianEquiv, are constructed and checked internally;
• OneSplitData packages the corresponding finite bijections for an arbitrary endpoint-sorted presentation.

Matching such a presentation to its source remains an explicit data obligation rather than treating edge ordering as definitional equality.

Occurrence-preserving graph transport

def Utilities.Certificate.OneEdgeSplitRefinement.laplacianEquivOfUnorientedUnitSteps {n p n' p' : ℕ} (source : SubdivisionGraph.Spec n p) (target : SubdivisionGraph.Spec n' p') (vertexEquiv : source.Vertex ≃ target.Vertex) (stepEquiv : source.Step ≃ target.Step) (unitEdge_eq : ∀ (step : source.Step), target.unitEdge (stepEquiv step) = (vertexEquiv (source.unitEdge step).1, vertexEquiv (source.unitEdge step).2) ∨ target.unitEdge (stepEquiv step) = (vertexEquiv (source.unitEdge step).2, vertexEquiv (source.unitEdge step).1)) : LaplacianEquiv source.graph target.graph

A vertex equivalence and a bijection of emitted unit-step occurrences induce a LaplacianEquiv when each step preserves its unordered endpoints. The step equivalence, rather than an endpoint-pair map, retains parallel-edge multiplicity.

Equations

• Utilities.Certificate.OneEdgeSplitRefinement.laplacianEquivOfUnorientedUnitSteps source target vertexEquiv stepEquiv unitEdge_eq = { toEquiv := vertexEquiv, num_edges_eq := ⋯ }

def Utilities.Certificate.OneEdgeSplitRefinement.laplacianEquivOfUnitSteps {n p n' p' : ℕ} (source : SubdivisionGraph.Spec n p) (target : SubdivisionGraph.Spec n' p') (vertexEquiv : source.Vertex ≃ target.Vertex) (stepEquiv : source.Step ≃ target.Step) (unitEdge_eq : ∀ (step : source.Step), target.unitEdge (stepEquiv step) = (vertexEquiv (source.unitEdge step).1, vertexEquiv (source.unitEdge step).2)) : LaplacianEquiv source.graph target.graph

Ordered endpoint preservation is the special case with no reversed slots.

Equations

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

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

Composition of two Laplacian-preserving relabelings.

Equations

• Utilities.Certificate.OneEdgeSplitRefinement.laplacianEquivTrans first second = { toEquiv := first.toEquiv.trans second.toEquiv, num_edges_eq := ⋯ }

The canonical split core

def Utilities.Certificate.OneEdgeSplitRefinement.oldVertex {n p : ℕ} (_source : SubdivisionGraph.Spec n p) (vertex : Fin n) : Fin (n + 1)

Original vertices embed below the fresh last core vertex.

Equations

• Utilities.Certificate.OneEdgeSplitRefinement.oldVertex _source vertex = vertex.castSucc

def Utilities.Certificate.OneEdgeSplitRefinement.splitVertex {n p : ℕ} (_source : SubdivisionGraph.Spec n p) : Fin (n + 1)

The fresh bivalent vertex.

Equations

• Utilities.Certificate.OneEdgeSplitRefinement.splitVertex _source = Fin.last n

@[reducible, inline]

abbrev Utilities.Certificate.OneEdgeSplitRefinement.oldSlot {n p : ℕ} (_source : SubdivisionGraph.Spec n p) (edge : Fin p) : Fin (p + 1)

Original slots embed below the fresh last edge slot.

Equations

• Utilities.Certificate.OneEdgeSplitRefinement.oldSlot _source edge = edge.castSucc

@[reducible, inline]

abbrev Utilities.Certificate.OneEdgeSplitRefinement.secondSlot {n p : ℕ} (_source : SubdivisionGraph.Spec n p) : Fin (p + 1)

Slot occupied by the second half of the split edge.

Equations

• Utilities.Certificate.OneEdgeSplitRefinement.secondSlot _source = Fin.last p

def Utilities.Certificate.OneEdgeSplitRefinement.splitCore {n p : ℕ} (source : SubdivisionGraph.Spec n p) (split : Fin p) : ExplicitPotential.Core (n + 1) (p + 1)

Replace the named occurrence by a path through the fresh vertex. All other occurrences retain their old slots, including parallel copies.

Equations

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

def Utilities.Certificate.OneEdgeSplitRefinement.splitLength {n p : ℕ} (source : SubdivisionGraph.Spec n p) (split : Fin p) (first second : ℕ) : Fin (p + 1) → ℕ

The first half remains in the old slot and the second half occupies the new last slot.

Equations

• Utilities.Certificate.OneEdgeSplitRefinement.splitLength source split first second i = Fin.lastCases second (fun (edge : Fin p) => if edge = split then first else source.length edge) i

@[simp]

theorem Utilities.Certificate.OneEdgeSplitRefinement.splitCore_tail_old {n p : ℕ} (source : SubdivisionGraph.Spec n p) (split edge : Fin p) : (splitCore source split).tail (oldSlot source edge) = oldVertex source (source.core.tail edge)

@[simp]

theorem Utilities.Certificate.OneEdgeSplitRefinement.splitCore_tail_second {n p : ℕ} (source : SubdivisionGraph.Spec n p) (split : Fin p) : (splitCore source split).tail (secondSlot source) = splitVertex source

@[simp]

theorem Utilities.Certificate.OneEdgeSplitRefinement.splitCore_head_old {n p : ℕ} (source : SubdivisionGraph.Spec n p) (split edge : Fin p) : (splitCore source split).head (oldSlot source edge) = if edge = split then splitVertex source else oldVertex source (source.core.head edge)

@[simp]

theorem Utilities.Certificate.OneEdgeSplitRefinement.splitCore_head_second {n p : ℕ} (source : SubdivisionGraph.Spec n p) (split : Fin p) : (splitCore source split).head (secondSlot source) = oldVertex source (source.core.head split)

@[simp]

theorem Utilities.Certificate.OneEdgeSplitRefinement.splitLength_old {n p : ℕ} (source : SubdivisionGraph.Spec n p) (split : Fin p) (first second : ℕ) (edge : Fin p) : splitLength source split first second (oldSlot source edge) = if edge = split then first else source.length edge

@[simp]

theorem Utilities.Certificate.OneEdgeSplitRefinement.splitLength_second {n p : ℕ} (source : SubdivisionGraph.Spec n p) (split : Fin p) (first second : ℕ) : splitLength source split first second (secondSlot source) = second

def Utilities.Certificate.OneEdgeSplitRefinement.splitSpec {n p : ℕ} (source : SubdivisionGraph.Spec n p) (split : Fin p) (first second : ℕ) (hFirst : 0 < first) (hSecond : 0 < second) : SubdivisionGraph.Spec (n + 1) (p + 1)

Positive-length subdivision specification on the canonical split core.

Equations

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

Proof-carrying normalization of refinements

structure Utilities.Certificate.OneEdgeSplitRefinement.OneSplitData {n p : ℕ} (source : SubdivisionGraph.Spec n p) (expanded : SubdivisionGraph.Spec (n + 1) (p + 1)) : Type

Data required to connect one fixed edge refinement to its source subdivision. stepEquiv is an equivalence of occurrences, so sorted parallel slots remain distinct; unitEdge_eq permits endpoint orientation to reverse.

• splitEdge : Fin p

  The source edge divided into two positive segments in the expanded presentation.

• firstLength : ℕ

  The positive first-segment length in the one-edge split.

• secondLength : ℕ

  The positive second-segment length, whose sum with the first equals the original edge length.

• firstLength_pos : 0 < self.firstLength
• secondLength_pos : 0 < self.secondLength
• length_sum : source.length self.splitEdge = self.firstLength + self.secondLength
• vertexEquiv : source.Vertex ≃ expanded.Vertex

  The bijection between source and expanded subdivision vertices.

• stepEquiv : source.Step ≃ expanded.Step

  The bijection of unit-edge occurrences, required to match endpoints under vertexEquiv up to reversal.

• unitEdge_eq (step : source.Step) : expanded.unitEdge (self.stepEquiv step) = (self.vertexEquiv (source.unitEdge step).1, self.vertexEquiv (source.unitEdge step).2) ∨ expanded.unitEdge (self.stepEquiv step) = (self.vertexEquiv (source.unitEdge step).2, self.vertexEquiv (source.unitEdge step).1)

def Utilities.Certificate.OneEdgeSplitRefinement.OneSplitData.laplacianEquiv {n p : ℕ} {source : SubdivisionGraph.Spec n p} {expanded : SubdivisionGraph.Spec (n + 1) (p + 1)} (data : OneSplitData source expanded) : LaplacianEquiv source.graph expanded.graph

A checked one-split normalization preserves the chip-firing Laplacian.

Equations

• data.laplacianEquiv = Utilities.Certificate.OneEdgeSplitRefinement.laplacianEquivOfUnorientedUnitSteps source expanded data.vertexEquiv data.stepEquiv ⋯

@[simp]

theorem Utilities.Certificate.OneEdgeSplitRefinement.OneSplitData.num_edges_eq {n p : ℕ} {source : SubdivisionGraph.Spec n p} {expanded : SubdivisionGraph.Spec (n + 1) (p + 1)} (data : OneSplitData source expanded) (x y : source.Vertex) : numEdges expanded.graph (data.vertexEquiv x) (data.vertexEquiv y) = numEdges source.graph x y

theorem Utilities.Certificate.OneEdgeSplitRefinement.OneSplitData.card_edges_eq {n p : ℕ} {source : SubdivisionGraph.Spec n p} {expanded : SubdivisionGraph.Spec (n + 1) (p + 1)} (data : OneSplitData source expanded) : expanded.graph.edges.card = source.graph.edges.card

Exact edge count, obtained from the occurrence bijection itself.

theorem Utilities.Certificate.OneEdgeSplitRefinement.OneSplitData.bnExists_iff {n p : ℕ} {source : SubdivisionGraph.Spec n p} {expanded : SubdivisionGraph.Spec (n + 1) (p + 1)} (data : OneSplitData source expanded) (r d : ℤ) : BNExists source.graph r d ↔ BNExists expanded.graph r d

theorem Utilities.Certificate.OneEdgeSplitRefinement.OneSplitData.transmissionExistence_iff {n p : ℕ} {source : SubdivisionGraph.Spec n p} {expanded : SubdivisionGraph.Spec (n + 1) (p + 1)} (data : OneSplitData source expanded) (u v : source.Vertex) : TransmissionExistence expanded.graph (data.vertexEquiv u) (data.vertexEquiv v) ↔ TransmissionExistence source.graph u v

A checked one-edge refinement preserves the full finite-length transmission-existence problem after carrying both marks through the checked vertex equivalence. This is stronger than bnExists_iff: it transports all ASP witnesses at once, not only their Grassmannian consequences.

Canonical split of a subdivision occurrence

def Utilities.Certificate.OneEdgeSplitRefinement.canonicalSplitVertexMap {n p : ℕ} (source : SubdivisionGraph.Spec n p) (split : Fin p) (first second : ℕ) (hFirst : 0 < first) (hSecond : 0 < second) (hLength : source.length split = first + second) : source.Vertex → (splitSpec source split first second hFirst hSecond).Vertex

The vertex map for the canonical split. On the selected subdivided path, the new core vertex occupies path position first; all other positions keep their evident old-slot names.

Equations

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

def Utilities.Certificate.OneEdgeSplitRefinement.canonicalSplitVertexMapInv {n p : ℕ} (source : SubdivisionGraph.Spec n p) (split : Fin p) (first second : ℕ) (hFirst : 0 < first) (hSecond : 0 < second) (hLength : source.length split = first + second) : (splitSpec source split first second hFirst hSecond).Vertex → source.Vertex

The inverse of canonicalSplitVertexMap, written by cases on the fresh core vertex and fresh edge slot.

Equations

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

def Utilities.Certificate.OneEdgeSplitRefinement.canonicalSplitVertexEquiv {n p : ℕ} (source : SubdivisionGraph.Spec n p) (split : Fin p) (first second : ℕ) (hFirst : 0 < first) (hSecond : 0 < second) (hLength : source.length split = first + second) : source.Vertex ≃ (splitSpec source split first second hFirst hSecond).Vertex

The canonical split preserves the underlying subdivision vertex set up to the explicit reclassification of the chosen path's position first as a fresh core vertex.

Equations

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

Canonical occurrence refinement

def Utilities.Certificate.OneEdgeSplitRefinement.canonicalSplitStepMap {n p : ℕ} (source : SubdivisionGraph.Spec n p) (split : Fin p) (first second : ℕ) (hFirst : 0 < first) (hSecond : 0 < second) (hLength : source.length split = first + second) : source.Step → (splitSpec source split first second hFirst hSecond).Step

The occurrence map for the canonical split. A unit step before the new core vertex remains in the old slot; every later step is moved to the new second slot. Thus this is a reclassification of the same unit-edge path, not an edge contraction or a change of the discrete graph.

Equations

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

def Utilities.Certificate.OneEdgeSplitRefinement.canonicalSplitStepMapInv {n p : ℕ} (source : SubdivisionGraph.Spec n p) (split : Fin p) (first second : ℕ) (hFirst : 0 < first) (hSecond : 0 < second) (hLength : source.length split = first + second) : (splitSpec source split first second hFirst hSecond).Step → source.Step

Inverse occurrence map for canonicalSplitStepMap.

Equations

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

def Utilities.Certificate.OneEdgeSplitRefinement.canonicalSplitStepEquiv {n p : ℕ} (source : SubdivisionGraph.Spec n p) (split : Fin p) (first second : ℕ) (hFirst : 0 < first) (hSecond : 0 < second) (hLength : source.length split = first + second) : source.Step ≃ (splitSpec source split first second hFirst hSecond).Step

The unit-step occurrences of a subdivision are unchanged when one path is canonically split at a positive interior position.

Equations

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

Compatibility of the canonical vertex and step maps

@[simp]

theorem Utilities.Certificate.OneEdgeSplitRefinement.canonicalSplitVertexEquiv_core {n p : ℕ} (source : SubdivisionGraph.Spec n p) (split : Fin p) (first second : ℕ) (hFirst : 0 < first) (hSecond : 0 < second) (hLength : source.length split = first + second) (vertex : Fin n) : (canonicalSplitVertexEquiv source split first second hFirst hSecond hLength) (source.coreVertex vertex) = (splitSpec source split first second hFirst hSecond).coreVertex (oldVertex source vertex)

On old core vertices the canonical vertex equivalence is the evident inclusion into the enlarged core.

@[simp]

theorem Utilities.Certificate.OneEdgeSplitRefinement.canonicalSplitVertexEquiv_oldInterior {n p : ℕ} (source : SubdivisionGraph.Spec n p) (split edge : Fin p) (first second : ℕ) (hFirst : 0 < first) (hSecond : 0 < second) (hLength : source.length split = first + second) (hEdge : edge ≠ split) (offset : Fin (source.length edge - 1)) : (canonicalSplitVertexEquiv source split first second hFirst hSecond hLength) (source.interiorVertex edge offset) = (splitSpec source split first second hFirst hSecond).interiorVertex (oldSlot source edge) ⟨↑offset, ⋯⟩

An interior point in an unsplit slot keeps both its slot and coordinate.

@[simp]

theorem Utilities.Certificate.OneEdgeSplitRefinement.canonicalSplitVertexEquiv_splitInterior_before {n p : ℕ} (source : SubdivisionGraph.Spec n p) (split : Fin p) (first second : ℕ) (hFirst : 0 < first) (hSecond : 0 < second) (hLength : source.length split = first + second) (offset : Fin (source.length split - 1)) (hBefore : ↑offset + 1 < first) : (canonicalSplitVertexEquiv source split first second hFirst hSecond hLength) (source.interiorVertex split offset) = (splitSpec source split first second hFirst hSecond).interiorVertex (oldSlot source split) ⟨↑offset, ⋯⟩

A selected-slot interior point strictly before the split remains in the first (old) slot.

@[simp]

theorem Utilities.Certificate.OneEdgeSplitRefinement.canonicalSplitVertexEquiv_splitInterior_at {n p : ℕ} (source : SubdivisionGraph.Spec n p) (split : Fin p) (first second : ℕ) (hFirst : 0 < first) (hSecond : 0 < second) (hLength : source.length split = first + second) (offset : Fin (source.length split - 1)) (hAt : ↑offset + 1 = first) : (canonicalSplitVertexEquiv source split first second hFirst hSecond hLength) (source.interiorVertex split offset) = (splitSpec source split first second hFirst hSecond).coreVertex (splitVertex source)

The old interior position at the split becomes the fresh core vertex.

@[simp]

theorem Utilities.Certificate.OneEdgeSplitRefinement.canonicalSplitVertexEquiv_splitInterior_after {n p : ℕ} (source : SubdivisionGraph.Spec n p) (split : Fin p) (first second : ℕ) (hFirst : 0 < first) (hSecond : 0 < second) (hLength : source.length split = first + second) (offset : Fin (source.length split - 1)) (hAfter : first < ↑offset + 1) : (canonicalSplitVertexEquiv source split first second hFirst hSecond hLength) (source.interiorVertex split offset) = (splitSpec source split first second hFirst hSecond).interiorVertex (secondSlot source) ⟨↑offset - first, ⋯⟩

A selected-slot interior point strictly after the split moves to the second slot, with its coordinate shifted by first.

theorem Utilities.Certificate.OneEdgeSplitRefinement.canonicalSplitVertexEquiv_pathVertex_old {n p : ℕ} (source : SubdivisionGraph.Spec n p) (split edge : Fin p) (first second : ℕ) (hFirst : 0 < first) (hSecond : 0 < second) (hLength : source.length split = first + second) (hEdge : edge ≠ split) (position : source.PathPosition edge) : (canonicalSplitVertexEquiv source split first second hFirst hSecond hLength) (source.pathVertex edge position) = (splitSpec source split first second hFirst hSecond).pathVertex (oldSlot source edge) ⟨↑position, ⋯⟩

Along an unsplit core slot, the canonical vertex equivalence agrees with the literal numerical path position.

theorem Utilities.Certificate.OneEdgeSplitRefinement.canonicalSplitVertexEquiv_pathVertex_split_first {n p : ℕ} (source : SubdivisionGraph.Spec n p) (split : Fin p) (first second : ℕ) (hFirst : 0 < first) (hSecond : 0 < second) (hLength : source.length split = first + second) (position : source.PathPosition split) (hLe : ↑position ≤ first) : (canonicalSplitVertexEquiv source split first second hFirst hSecond hLength) (source.pathVertex split position) = (splitSpec source split first second hFirst hSecond).pathVertex (oldSlot source split) ⟨↑position, ⋯⟩

On the first segment of the selected slot, numerical path positions are unchanged. The common endpoint at first is the fresh core vertex.

theorem Utilities.Certificate.OneEdgeSplitRefinement.canonicalSplitVertexEquiv_pathVertex_at_split {n p : ℕ} (source : SubdivisionGraph.Spec n p) (split : Fin p) (first second : ℕ) (hFirst : 0 < first) (hSecond : 0 < second) (hLength : source.length split = first + second) : (canonicalSplitVertexEquiv source split first second hFirst hSecond hLength) (source.pathVertex split ⟨first, ⋯⟩) = (splitSpec source split first second hFirst hSecond).coreVertex (splitVertex source)

The point at which a slot is split is carried to the fresh bivalent core vertex. This proof-term-stable endpoint form is the one used by generated multi-split certificates.

theorem Utilities.Certificate.OneEdgeSplitRefinement.canonicalSplit_unitEdge_eq {n p : ℕ} (source : SubdivisionGraph.Spec n p) (split : Fin p) (first second : ℕ) (hFirst : 0 < first) (hSecond : 0 < second) (hLength : source.length split = first + second) (step : source.Step) : (splitSpec source split first second hFirst hSecond).unitEdge ((canonicalSplitStepEquiv source split first second hFirst hSecond hLength) step) = ((canonicalSplitVertexEquiv source split first second hFirst hSecond hLength) (source.unitEdge step).1, (canonicalSplitVertexEquiv source split first second hFirst hSecond hLength) (source.unitEdge step).2)

Each emitted unit step has exactly the same ordered endpoints after the canonical split. Unlike a slotwise relabeling, no orientation reversal is needed: only the slot containing a position changes.

def Utilities.Certificate.OneEdgeSplitRefinement.canonicalSplitLaplacianEquiv {n p : ℕ} (source : SubdivisionGraph.Spec n p) (split : Fin p) (first second : ℕ) (hFirst : 0 < first) (hSecond : 0 < second) (hLength : source.length split = first + second) : LaplacianEquiv source.graph (splitSpec source split first second hFirst hSecond).graph

Splitting one positive-length slot through a new bivalent core vertex preserves the subdivision graph in the Laplacian sense used by certificate checking.

Equations

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

Identity refinement

def Utilities.Certificate.OneEdgeSplitRefinement.identityLaplacianEquiv {n p : ℕ} (source : SubdivisionGraph.Spec n p) : LaplacianEquiv source.graph source.graph

The identity refinement uses the reflexive vertex and occurrence bijections.

Equations

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

@[simp]

theorem Utilities.Certificate.OneEdgeSplitRefinement.identity_num_edges {n p : ℕ} (source : SubdivisionGraph.Spec n p) (x y : source.Vertex) : numEdges source.graph ((identityLaplacianEquiv source).toEquiv x) ((identityLaplacianEquiv source).toEquiv y) = numEdges source.graph x y