Encoded size of constraint graphs

The encoding charges unary vertex identifiers and each constraint descriptor, including the frames around the endpoint pairs and the edge list. Well-formed graphs therefore have encoded size bounded by their vertex and edge counts together with the descriptor lengths.

Main results

• Cslib.PCP.Encoded.Edge.length_encoding: exact size of one encoded edge.
• Cslib.PCP.Encoded.Graph.length_encoding: exact size of the whole encoded graph.
• Cslib.PCP.Encoded.Graph.WellFormed.length_encoding_le: cardinality and descriptor-size bound.

References

• I. Dinur, The PCP theorem by gap amplification

theorem Cslib.PCP.Encoded.Edge.length_encoding {C : Type} (enc : C ↪ List Bool) (edge : Edge C) : ((encoding enc) edge).length = 2 * edge.src + 2 * edge.dst + (enc edge.constraint).length + 2

Both unary endpoints are framed; the final descriptor is stored without another inner frame.

theorem Cslib.PCP.Encoded.Graph.length_encoding {C : Type} (enc : C ↪ List Bool) (g : Graph C) : ((encoding enc) g).length = 2 * g.vertices + 1 + (List.map (fun (edge : Edge C) => 4 * edge.src + 4 * edge.dst + 2 * (enc edge.constraint).length + 5) g.edges).sum

Each edge receives an outer list frame, and the declared vertex count its own unary frame.

theorem Cslib.PCP.Encoded.Graph.WellFormed.length_encoding_le {C : Type} (enc : C ↪ List Bool) {g : Graph C} (hg : g.WellFormed) (bound : ℕ) (hbound : ∀ edge ∈ g.edges, (enc edge.constraint).length ≤ bound) : ((encoding enc) g).length ≤ 2 * g.vertices + 1 + g.edges.length * (8 * g.vertices + 2 * bound + 5)

Endpoint bounds give a full encoded-size bound for arbitrary bounded descriptors.