Relabeling subdivided core graphs

This is the occurrence-sensitive symmetry interface for subdivision graphs. It transports a graph along a permutation of core vertices and edge slots, allowing each slot independently to be read in either direction. In particular, parallel core edges are never identified: unit steps are carried by an equivalence of their occurrences.

The data is intentionally stated for two possibly differently indexed core presentations. Thus it applies both to automorphisms of one presentation and to comparisons with another presentation having a different slot order.

structure Utilities.Certificate.SubdivisionGraph.Spec.Relabeling {n p n' p' : ℕ} (source : Spec n p) (target : Spec n' p') : Type

Slotwise relabeling data. reversed edge = true means that the target slot is read from the image of the source head to the image of the source tail.

• coreEquiv : Fin n ≃ Fin n'

  The bijection of core vertices in the subdivision relabeling.

• slotEquiv : Fin p ≃ Fin p'

  The bijection of core slots, required to preserve their subdivision lengths.

• reversed : Fin p → Bool

  The source-slot flags specifying which endpoint order is reversed by the relabeling.

• length_eq (edge : Fin p) : source.length edge = target.length (self.slotEquiv edge)
• tail_eq (edge : Fin p) : target.core.tail (self.slotEquiv edge) = if self.reversed edge = true then self.coreEquiv (source.core.head edge) else self.coreEquiv (source.core.tail edge)
• head_eq (edge : Fin p) : target.core.head (self.slotEquiv edge) = if self.reversed edge = true then self.coreEquiv (source.core.tail edge) else self.coreEquiv (source.core.head edge)

def Utilities.Certificate.SubdivisionGraph.Spec.positionEquiv {n p n' p' : ℕ} (source : Spec n p) (target : Spec n' p') (relabeling : source.Relabeling target) (edge : Fin p) : source.PathPosition edge ≃ target.PathPosition (relabeling.slotEquiv edge)

Equivalence of numerical positions on a matched edge slot.

Equations

• source.positionEquiv target relabeling edge = Equiv.trans (if relabeling.reversed edge = true then Fin.revPerm else Equiv.refl (Fin (source.length edge + 1))) (finCongr ⋯)

theorem Utilities.Certificate.SubdivisionGraph.Spec.positionEquiv_val {n p n' p' : ℕ} (source : Spec n p) (target : Spec n' p') (relabeling : source.Relabeling target) (edge : Fin p) (position : source.PathPosition edge) : ↑((source.positionEquiv target relabeling edge) position) = if relabeling.reversed edge = true then source.length edge - ↑position else ↑position

The numerical image of an offset. In a reversed slot this is L - k.

def Utilities.Certificate.SubdivisionGraph.Spec.interiorEquiv {n p n' p' : ℕ} (source : Spec n p) (target : Spec n' p') (relabeling : source.Relabeling target) (edge : Fin p) : Fin (source.length edge - 1) ≃ Fin (target.length (relabeling.slotEquiv edge) - 1)

Equivalence of interior coordinates on matched slots. A reversed slot sends interior coordinate j to L - 2 - j.

Equations

• source.interiorEquiv target relabeling edge = Equiv.trans (if relabeling.reversed edge = true then Fin.revPerm else Equiv.refl (Fin (source.length edge - 1))) (finCongr ⋯)

def Utilities.Certificate.SubdivisionGraph.Spec.stepOffsetEquiv {n p n' p' : ℕ} (source : Spec n p) (target : Spec n' p') (relabeling : source.Relabeling target) (edge : Fin p) : Fin (source.length edge) ≃ Fin (target.length (relabeling.slotEquiv edge))

Equivalence of unit-step offsets. A reversed slot sends step j to L - 1 - j.

Equations

• source.stepOffsetEquiv target relabeling edge = Equiv.trans (if relabeling.reversed edge = true then Fin.revPerm else Equiv.refl (Fin (source.length edge))) (finCongr ⋯)

def Utilities.Certificate.SubdivisionGraph.Spec.vertexEquiv {n p n' p' : ℕ} (source : Spec n p) (target : Spec n' p') (relabeling : source.Relabeling target) : source.Vertex ≃ target.Vertex

Vertex equivalence induced by a relabeling.

Equations

• source.vertexEquiv target relabeling = relabeling.coreEquiv.sumCongr (relabeling.slotEquiv.sigmaCongr fun (edge : Fin p) => source.interiorEquiv target relabeling edge)

def Utilities.Certificate.SubdivisionGraph.Spec.stepEquiv {n p n' p' : ℕ} (source : Spec n p) (target : Spec n' p') (relabeling : source.Relabeling target) : source.Step ≃ target.Step

Unit-step occurrence equivalence induced by a relabeling.

Equations

• source.stepEquiv target relabeling = relabeling.slotEquiv.sigmaCongr fun (edge : Fin p) => source.stepOffsetEquiv target relabeling edge

@[simp]

theorem Utilities.Certificate.SubdivisionGraph.Spec.vertexEquiv_coreVertex {n p n' p' : ℕ} (source : Spec n p) (target : Spec n' p') (relabeling : source.Relabeling target) (vertex : Fin n) : (source.vertexEquiv target relabeling) (source.coreVertex vertex) = target.coreVertex (relabeling.coreEquiv vertex)

@[simp]

theorem Utilities.Certificate.SubdivisionGraph.Spec.vertexEquiv_interiorVertex {n p n' p' : ℕ} (source : Spec n p) (target : Spec n' p') (relabeling : source.Relabeling target) (edge : Fin p) (offset : Fin (source.length edge - 1)) : (source.vertexEquiv target relabeling) (source.interiorVertex edge offset) = target.interiorVertex (relabeling.slotEquiv edge) ((source.interiorEquiv target relabeling edge) offset)

@[simp]

theorem Utilities.Certificate.SubdivisionGraph.Spec.stepEquiv_apply {n p n' p' : ℕ} (source : Spec n p) (target : Spec n' p') (relabeling : source.Relabeling target) (edge : Fin p) (offset : Fin (source.length edge)) : (source.stepEquiv target relabeling) ⟨edge, offset⟩ = ⟨relabeling.slotEquiv edge, (source.stepOffsetEquiv target relabeling edge) offset⟩

theorem Utilities.Certificate.SubdivisionGraph.Spec.pathVertex_positionEquiv {n p n' p' : ℕ} (source : Spec n p) (target : Spec n' p') (relabeling : source.Relabeling target) (edge : Fin p) (position : source.PathPosition edge) : target.pathVertex (relabeling.slotEquiv edge) ((source.positionEquiv target relabeling edge) position) = (source.vertexEquiv target relabeling) (source.pathVertex edge position)

Relabeling carries every named path position to the corresponding vertex of the matched target slot. This is the basic transport statement used for both core automorphisms and presentation changes.

theorem Utilities.Certificate.SubdivisionGraph.Spec.positionEquiv_stepLeft_of_not_reversed {n p n' p' : ℕ} (source : Spec n p) (target : Spec n' p') (relabeling : source.Relabeling target) (edge : Fin p) (offset : Fin (source.length edge)) (hReversed : relabeling.reversed edge = false) : (source.positionEquiv target relabeling edge) (source.stepLeftPosition edge offset) = target.stepLeftPosition (relabeling.slotEquiv edge) ((source.stepOffsetEquiv target relabeling edge) offset)

In an orientation-preserving slot, left unit-step endpoints retain their left position.

theorem Utilities.Certificate.SubdivisionGraph.Spec.positionEquiv_stepRight_of_not_reversed {n p n' p' : ℕ} (source : Spec n p) (target : Spec n' p') (relabeling : source.Relabeling target) (edge : Fin p) (offset : Fin (source.length edge)) (hReversed : relabeling.reversed edge = false) : (source.positionEquiv target relabeling edge) (source.stepRightPosition edge offset) = target.stepRightPosition (relabeling.slotEquiv edge) ((source.stepOffsetEquiv target relabeling edge) offset)

In an orientation-preserving slot, right unit-step endpoints retain their right position.

theorem Utilities.Certificate.SubdivisionGraph.Spec.positionEquiv_stepLeft_of_reversed {n p n' p' : ℕ} (source : Spec n p) (target : Spec n' p') (relabeling : source.Relabeling target) (edge : Fin p) (offset : Fin (source.length edge)) (hReversed : relabeling.reversed edge = true) : (source.positionEquiv target relabeling edge) (source.stepLeftPosition edge offset) = target.stepRightPosition (relabeling.slotEquiv edge) ((source.stepOffsetEquiv target relabeling edge) offset)

In a reversed slot, a source left unit-step endpoint becomes the target right endpoint.

theorem Utilities.Certificate.SubdivisionGraph.Spec.positionEquiv_stepRight_of_reversed {n p n' p' : ℕ} (source : Spec n p) (target : Spec n' p') (relabeling : source.Relabeling target) (edge : Fin p) (offset : Fin (source.length edge)) (hReversed : relabeling.reversed edge = true) : (source.positionEquiv target relabeling edge) (source.stepRightPosition edge offset) = target.stepLeftPosition (relabeling.slotEquiv edge) ((source.stepOffsetEquiv target relabeling edge) offset)

In a reversed slot, a source right unit-step endpoint becomes the target left endpoint.

theorem Utilities.Certificate.SubdivisionGraph.Spec.unitEdge_stepEquiv {n p n' p' : ℕ} (source : Spec n p) (target : Spec n' p') (relabeling : source.Relabeling target) (step : source.Step) : target.unitEdge ((source.stepEquiv target relabeling) step) = ((source.vertexEquiv target relabeling) (source.unitEdge step).1, (source.vertexEquiv target relabeling) (source.unitEdge step).2) ∨ target.unitEdge ((source.stepEquiv target relabeling) step) = ((source.vertexEquiv target relabeling) (source.unitEdge step).2, (source.vertexEquiv target relabeling) (source.unitEdge step).1)

Every unit-step occurrence has the same unordered endpoints after a relabeling. This retains parallel-edge multiplicities slot by slot.

def Utilities.Certificate.SubdivisionGraph.Spec.laplacianEquiv {n p n' p' : ℕ} (source : Spec n p) (target : Spec n' p') (relabeling : source.Relabeling target) : LaplacianEquiv source.graph target.graph

The resulting vertex equivalence is a graph isomorphism in the precise Laplacian sense used by the certificate checker.

Equations

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

def Utilities.Certificate.SubdivisionGraph.Spec.graphIso {n p n' p' : ℕ} (source : Spec n p) (target : Spec n' p') (relabeling : source.Relabeling target) : CFGraphIso source.graph target.graph

The same relabeling packaged for the older, transmission-facing graph isomorphism API. It has exactly the same finite multiplicity content as laplacianEquiv.

Equations

• source.graphIso target relabeling = { vertexEquiv := source.vertexEquiv target relabeling, map_num_edges := ⋯ }

theorem Utilities.Certificate.SubdivisionGraph.Spec.transmissionExistence_iff {n p n' p' : ℕ} (source : Spec n p) (target : Spec n' p') (relabeling : source.Relabeling target) (u v : source.Vertex) : TransmissionExistence target.graph ((source.vertexEquiv target relabeling) u) ((source.vertexEquiv target relabeling) v) ↔ TransmissionExistence source.graph u v

Full finite-length transmission existence is invariant under a checked slotwise relabeling of a subdivision presentation. In particular, a transmission certificate can be reused after independently permuting and reversing parallel edge occurrences.

Reindexing a specification along index equivalences

def Utilities.Certificate.SubdivisionGraph.coreReindex {n p n' p' : ℕ} (core : ExplicitPotential.Core n p) (vertexEquiv : Fin n ≃ Fin n') (slotEquiv : Fin p ≃ Fin p') : ExplicitPotential.Core n' p'

Rename the vertices and edge slots of an ordered core.

Equations

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

def Utilities.Certificate.SubdivisionGraph.specReindex {n p n' p' : ℕ} (spec : Spec n p) (vertexEquiv : Fin n ≃ Fin n') (slotEquiv : Fin p ≃ Fin p') (hn : 0 < n') : Spec n' p'

Rename the vertices and edge slots of a subdivision specification.

Equations

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

def Utilities.Certificate.SubdivisionGraph.specReindexRelabeling {n p n' p' : ℕ} (spec : Spec n p) (vertexEquiv : Fin n ≃ Fin n') (slotEquiv : Fin p ≃ Fin p') (hn : 0 < n') : spec.Relabeling (specReindex spec vertexEquiv slotEquiv hn)

Reindexing is a relabeling, hence preserves the subdivided graph.

Equations

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

theorem Utilities.Certificate.SubdivisionGraph.laplacianEquiv_specReindex {n p n' p' : ℕ} (spec : Spec n p) (vertexEquiv : Fin n ≃ Fin n') (slotEquiv : Fin p ≃ Fin p') (hn : 0 < n') : Nonempty (LaplacianEquiv spec.graph (specReindex spec vertexEquiv slotEquiv hn).graph)