Canonical three-way ports for finite graph incidences

Each listed edge contributes its two endpoint occurrences in order. An incidence is assigned the number of preceding equal vertex labels, reduced modulo three. When every vertex occurs at most three times, reduction does nothing and every incidence of that vertex gets a distinct port. Parallel listed edges remain distinct; a loop contributes two incidences.

Main definitions

• Cslib.Complexity.Graph.incidenceVertices: finite list of endpoint occurrences.
• Cslib.Complexity.Graph.incidencePort: canonical three-way port of an occurrence.
• Cslib.Complexity.Graph.canonicalPorts: finite edge-indexed port table.

Main results

• Cslib.Complexity.Graph.incidencePort_injective: equal vertex/port pairs identify incidences whenever endpoint occurrence counts are at most three.

def Cslib.Complexity.Graph.incidenceVertices (G : Graph) : List ℕ

Endpoints of all listed edges, counting edge occurrences rather than simple-graph degree.

@[simp]

theorem Cslib.Complexity.Graph.incidenceVertices_length (G : Graph) : G.incidenceVertices.length = 2 * G.edges.length

Number of endpoint occurrences is twice the edge-list length.

theorem Cslib.Complexity.Graph.getD_incidenceVertices_even (G : Graph) (i : ℕ) : G.incidenceVertices.getD (2 * i) 0 = (G.edges.getD i (0, 0)).1

The even endpoint occurrence is the first endpoint of the corresponding listed edge.

theorem Cslib.Complexity.Graph.getD_incidenceVertices_odd (G : Graph) (i : ℕ) : G.incidenceVertices.getD (2 * i + 1) 0 = (G.edges.getD i (0, 0)).2

The odd endpoint occurrence is the second endpoint of the corresponding listed edge.

def Cslib.Complexity.Graph.incidencePort (G : Graph) (k : ℕ) : Fin 3

Executable port assignment; under the degree hypothesis the remainder is the rank itself.

def Cslib.Complexity.Graph.canonicalPorts (G : Graph) : List (Fin 3 × Fin 3)

The edge-indexed finite table of canonical port pairs.

@[simp]

theorem Cslib.Complexity.Graph.canonicalPorts_length (G : Graph) : G.canonicalPorts.length = G.edges.length

One canonical port pair per listed edge.

theorem Cslib.Complexity.Graph.getD_canonicalPorts (G : Graph) {i : ℕ} (hi : i < G.edges.length) : G.canonicalPorts.getD i (0, 0) = (G.incidencePort (2 * i), G.incidencePort (2 * i + 1))

Reading the canonical table at an existing edge returns its two incidence ports.

theorem Cslib.Complexity.Graph.incidencePort_val (G : Graph) (hdeg : ∀ (v : ℕ), List.count v G.incidenceVertices ≤ 3) {k : ℕ} (hk : k < G.incidenceVertices.length) : ↑(G.incidencePort k) = List.count G.incidenceVertices[k] (List.take k G.incidenceVertices)

For graphs with at most three incidences per vertex, no remainder reduction occurs.

theorem Cslib.Complexity.Graph.incidencePort_injective (G : Graph) (hdeg : ∀ (v : ℕ), List.count v G.incidenceVertices ≤ 3) {i j : ℕ} (hi : i < G.incidenceVertices.length) (hj : j < G.incidenceVertices.length) (hv : G.incidenceVertices[i] = G.incidenceVertices[j]) (hp : G.incidencePort i = G.incidencePort j) : i = j

Equal vertex labels and canonical ports identify endpoint occurrences when all incidence counts are at most three.

def Cslib.Complexity.Graph.edgeEndpoint (G : Graph) (i : ℕ) (side : Bool) : ℕ

Endpoint label of a listed edge occurrence; false means first, true second.

theorem Cslib.Complexity.Graph.getD_incidenceVertices_endpoint (G : Graph) (i : ℕ) (side : Bool) : G.incidenceVertices.getD (2 * i + side.toNat) 0 = G.edgeEndpoint i side

The endpoint occurrence index agrees with the finite flattened endpoint list.

theorem Cslib.Complexity.Graph.endpoint_index_lt (G : Graph) {i : ℕ} (hi : i < G.edges.length) (side : Bool) : 2 * i + side.toNat < G.incidenceVertices.length

A listed endpoint occurrence lies in the endpoint list's index range.

theorem Cslib.Complexity.Graph.endpoint_port_injective (G : Graph) (hdeg : ∀ (v : ℕ), List.count v G.incidenceVertices ≤ 3) {i j : ℕ} (hi : i < G.edges.length) (hj : j < G.edges.length) (left right : Bool) (hv : G.edgeEndpoint i left = G.edgeEndpoint j right) (hp : G.incidencePort (2 * i + left.toNat) = G.incidencePort (2 * j + right.toNat)) : i = j ∧ left = right

Vertex and canonical port determine both the edge occurrence and which end it is.

def Cslib.Complexity.Graph.portAt (ports : List (Fin 3 × Fin 3)) (i : ℕ) (side : Bool) : Fin 3

Reading a finite port table at one end of an edge occurrence.

theorem Cslib.Complexity.Graph.portAt_canonicalPorts (G : Graph) {i : ℕ} (hi : i < G.edges.length) (side : Bool) : portAt G.canonicalPorts i side = G.incidencePort (2 * i + side.toNat)

The canonical table reads the corresponding incidence's occurrence-rank port.

theorem Cslib.Complexity.Graph.edgeEndpoint_mem (G : Graph) (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) {i : ℕ} (hi : i < G.edges.length) (side : Bool) : G.edgeEndpoint i side ∈ G.vertices

Every indexed endpoint of a graph with declared endpoints is declared.

theorem Cslib.Complexity.Graph.canonical_index_port_ne (G : Graph) (hG : ∀ edge ∈ G.edges, edge.1 ∈ G.vertices ∧ edge.2 ∈ G.vertices) (hdeg : ∀ (v : ℕ), List.count v G.incidenceVertices ≤ 3) {i j : ℕ} (hi : i < G.edges.length) (hj : j < G.edges.length) (hij : i ≠ j) (left right : Bool) : (List.idxOf (G.edgeEndpoint i left) G.vertices, portAt G.canonicalPorts i left) ≠ (List.idxOf (G.edgeEndpoint j right) G.vertices, portAt G.canonicalPorts j right)

Canonical vertex-position/port pairs are distinct at every pair of different listed edges.