Enumerating half-edges and vertex clouds

Degree reduction replaces a vertex by its incident half-edges. The executable enumeration uses edge indices and Boolean endpoint tags, including both ends of a loop and every parallel edge. cloudEquiv proves that this enumeration is exactly the cloud in the existing mathematical degree-reduction construction. Its inverse is list search, not a choice of a finite enumeration.

Main definitions

• Cslib.PCP.Encoded.Graph.halfEdges: the ordered half-edges of an edge list.
• Cslib.PCP.Encoded.Graph.endpoint: read the endpoint of a numbered half-edge.
• Cslib.PCP.Encoded.Graph.cloud: enumerate the half-edges incident to a vertex.
• Cslib.PCP.Encoded.Graph.cloudEquiv: identify this enumeration with the mathematical cloud.

Main results

• Cslib.PCP.Encoded.Graph.mem_cloud_iff: the enumeration includes exactly incident half-edges.
• Cslib.PCP.Encoded.Graph.nodup_cloud: each half-edge occurs once.
• Cslib.PCP.Encoded.Graph.isPolyTime_cloud: enumeration, scanning and endpoint lookup are uniformly polynomial-time in the encoded graph and vertex.

References

• I. Dinur, The PCP theorem by gap amplification
• I. Dinur, The PCP theorem by gap amplification, ECCC TR05-046, revision 1

def Cslib.PCP.Encoded.Graph.halfEdges {C : Type} (g : Graph C) : List (ℕ × Bool)

The ordered half-edges: first and second endpoint of every edge, retaining multiplicities of the edges. The two ends of a loop remain distinct half-edges.

def Cslib.PCP.Encoded.Graph.endpoint {C : Type} (fallback : C) (g : Graph C) (p : ℕ × Bool) : ℕ

Read the first endpoint for false and the second endpoint for true. Out-of-range edge indices return vertex zero.

def Cslib.PCP.Encoded.Graph.cloud {C : Type} (fallback : C) (g : Graph C) (vertex : ℕ) : List (ℕ × Bool)

Enumerate the half-edges incident to a vertex in edge-list order.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_halfEdges {C Input : Type} {input : Input ↪ List Bool} {enc : C ↪ List Bool} {graph : Input → Graph C} (hgraph : Turing.MultiTapeTM.ComputableTidilyInPolyTime graph input (encoding enc)) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => (graph x).halfEdges) input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool))

Enumerating both ends of every edge is polynomial-time.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_endpoint {C Input : Type} {input : Input ↪ List Bool} {enc : C ↪ List Bool} {graph : Input → Graph C} {halfEdge : Input → ℕ × Bool} (hgraph : Turing.MultiTapeTM.ComputableTidilyInPolyTime graph input (encoding enc)) (hhalfEdge : Turing.MultiTapeTM.ComputableTidilyInPolyTime halfEdge input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool)) (fallback : C) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => endpoint fallback (graph x) (halfEdge x)) input Turing.MultiTapeTM.encUnary

Endpoint lookup is uniform in the graph and the half-edge.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_cloud {C Input : Type} {input : Input ↪ List Bool} {enc : C ↪ List Bool} {graph : Input → Graph C} {vertex : Input → ℕ} (hgraph : Turing.MultiTapeTM.ComputableTidilyInPolyTime graph input (encoding enc)) (hvertex : Turing.MultiTapeTM.ComputableTidilyInPolyTime vertex input Turing.MultiTapeTM.encUnary) (fallback : C) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : Input) => cloud fallback (graph x) (vertex x)) input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool))

Cloud enumeration charges each endpoint lookup and the entire filtered output.

@[simp]

theorem Cslib.PCP.Encoded.Graph.length_halfEdges {C : Type} (g : Graph C) : g.halfEdges.length = 2 * g.edges.length

Every edge contributes exactly two half-edges.

@[simp]

theorem Cslib.PCP.Encoded.Graph.mem_halfEdges_iff {C : Type} (g : Graph C) (p : ℕ × Bool) : p ∈ g.halfEdges ↔ p.1 < g.edges.length

A numbered half-edge exists exactly when its edge index exists.

theorem Cslib.PCP.Encoded.Graph.nodup_halfEdges {C : Type} (g : Graph C) : g.halfEdges.Nodup

Both ends of every edge have distinct names, even for loops and parallel edges.

def Cslib.PCP.Encoded.Graph.halfEdgesEnumeration {C : Type} (g : Graph C) : g.halfEdges.Enumeration fun (p : Fin g.edges.length × Bool) => (↑p.1, p.2)

Half-edge positions retain the original edge order, with its two ends adjacent.

@[simp]

theorem Cslib.PCP.Encoded.Graph.mem_cloud_iff {C : Type} (g : Graph C) (fallback : C) (vertex : ℕ) (p : ℕ × Bool) : p ∈ cloud fallback g vertex ↔ p.1 < g.edges.length ∧ endpoint fallback g p = vertex

Cloud membership means that the edge exists and the selected endpoint is the vertex.

theorem Cslib.PCP.Encoded.Graph.nodup_cloud {C : Type} (g : Graph C) (fallback : C) (vertex : ℕ) : (cloud fallback g vertex).Nodup

A cloud has no repeated half-edge.

theorem Cslib.PCP.Encoded.Graph.length_cloud_le {C : Type} (g : Graph C) (fallback : C) (vertex : ℕ) : (cloud fallback g vertex).length ≤ 2 * g.edges.length

Every cloud has at most two half-edges per original edge.

theorem Cslib.PCP.Encoded.Graph.endpoint_eq {C α : Type} (g : Graph C) (eval : C → α → α → Bool) (fallback : C) (p : Fin g.edges.length × Bool) : endpoint fallback g (↑p.1, p.2) = (g.toGraph eval).endpoint p

Endpoint lookup agrees with the mathematical graph on existing edges.

def Cslib.PCP.Encoded.Graph.cloudEquiv {C α : Type} (g : Graph C) (eval : C → α → α → Bool) (fallback : C) (vertex : ℕ) : Fin (cloud fallback g vertex).length ≃ (g.toGraph eval).Cloud vertex

The computed cloud list is precisely the mathematical cloud, with an explicit inverse which searches the ordered half-edge list.

theorem Cslib.PCP.Encoded.Graph.cloudEquiv_apply {C α : Type} (g : Graph C) (eval : C → α → α → Bool) (fallback : C) (vertex : ℕ) (i : Fin (cloud fallback g vertex).length) : (↑(↑((g.cloudEquiv eval fallback vertex) i)).1, (↑((g.cloudEquiv eval fallback vertex) i)).2) = (cloud fallback g vertex).get i

The forward cloud identification reads the selected list entry.

theorem Cslib.PCP.Encoded.Graph.cloudEquiv_symm_apply {C α : Type} (g : Graph C) (eval : C → α → α → Bool) (fallback : C) (vertex : ℕ) (p : (g.toGraph eval).Cloud vertex) : ↑((g.cloudEquiv eval fallback vertex).symm p) = List.idxOf (↑(↑p).1, (↑p).2) (cloud fallback g vertex)

The inverse cloud identification is the ordinary index-of operation.