Vertex relabeling and the handshake identity for pseudocores

Three ingredients, all generic in the vertex count:

• Pseudocore.relabel — transport of a pseudocore along a vertex permutation, with well-formedness, connectedness, valence, and edge-count preservation;
• Pseudocore.sum_valence_eq — the handshake identity Σ valence = 2 · edgeCount for well-formed pseudocores, which pins an arbitrary valid pseudocore's valence vector to a partition-of-six degree sequence;
• Pseudocore.exists_monotone_relabel — every pseudocore admits a relabeling with monotone valences (Tuple.sort), which is what reduces the classifier to one generated tree per sorted degree sequence.

def Utilities.Certificate.GenusFourPseudocore.Pseudocore.relabel {n : ℕ} (core : Pseudocore n) (σ : Equiv.Perm (Fin n)) : Pseudocore n

Transport of a pseudocore along a vertex permutation: vertex v of the relabeled pseudocore carries the data of vertex σ v.

Equations

• core.relabel σ = { loops := fun (v : Fin n) => core.loops (σ v), multiplicity := fun (v w : Fin n) => core.multiplicity (σ v) (σ w) }

@[simp]

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.relabel_loops {n : ℕ} (core : Pseudocore n) (σ : Equiv.Perm (Fin n)) (v : Fin n) : (core.relabel σ).loops v = core.loops (σ v)

@[simp]

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.relabel_multiplicity {n : ℕ} (core : Pseudocore n) (σ : Equiv.Perm (Fin n)) (v w : Fin n) : (core.relabel σ).multiplicity v w = core.multiplicity (σ v) (σ w)

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.valence_relabel {n : ℕ} (core : Pseudocore n) (σ : Equiv.Perm (Fin n)) (v : Fin n) : (core.relabel σ).valence v = core.valence (σ v)

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.matrixWellFormed_relabel {n : ℕ} (core : Pseudocore n) (σ : Equiv.Perm (Fin n)) (hWellFormed : core.MatrixWellFormed) : (core.relabel σ).MatrixWellFormed

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.connected_relabel {n : ℕ} (core : Pseudocore n) (σ : Equiv.Perm (Fin n)) (hConnected : core.Connected) : (core.relabel σ).Connected

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.double_nonloopEdgeCount {n : ℕ} (core : Pseudocore n) (hWellFormed : core.MatrixWellFormed) : 2 * core.nonloopEdgeCount = ∑ v : Fin n, ∑ w : Fin n, core.multiplicity v w

The doubling identity behind the handshake: the full matrix sum of a well-formed pseudocore is twice its strict-upper-triangle sum.

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.sum_valence_eq {n : ℕ} (core : Pseudocore n) (hWellFormed : core.MatrixWellFormed) : ∑ v : Fin n, core.valence v = 2 * core.edgeCount

The handshake identity. A well-formed pseudocore's total valence is twice its edge count.

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.loopCount_relabel {n : ℕ} (core : Pseudocore n) (σ : Equiv.Perm (Fin n)) : (core.relabel σ).loopCount = core.loopCount

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.nonloopEdgeCount_relabel {n : ℕ} (core : Pseudocore n) (σ : Equiv.Perm (Fin n)) (hWellFormed : core.MatrixWellFormed) : (core.relabel σ).nonloopEdgeCount = core.nonloopEdgeCount

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.edgeCount_relabel {n : ℕ} (core : Pseudocore n) (σ : Equiv.Perm (Fin n)) (hWellFormed : core.MatrixWellFormed) : (core.relabel σ).edgeCount = core.edgeCount

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.stable_relabel {n : ℕ} (core : Pseudocore n) (σ : Equiv.Perm (Fin n)) (hStable : core.Stable) : (core.relabel σ).Stable

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.validAt_relabel {n : ℕ} (core : Pseudocore n) (σ : Equiv.Perm (Fin n)) {g : ℕ} (hValid : core.ValidAt g) : (core.relabel σ).ValidAt g

theorem Utilities.Certificate.GenusFourPseudocore.Pseudocore.exists_monotone_relabel {n : ℕ} (core : Pseudocore n) : ∃ (σ : Equiv.Perm (Fin n)), Monotone (core.relabel σ).valence

Every pseudocore admits a relabeling with monotone valences.