Executable preprocessing of constraint graphs

The program degree-reduces an explicit edge list, adds the edges of the numerical graph family on its numbered half-edges, and adds one self-loop per half-edge. Original constraints remain oriented; cloud constraints check equality; the added family edges and loops always accept.

The efficiency certificate is uniform in the input graph. Its numerical rotation hypothesis covers the runtime graph size, vertex, and edge label jointly. The value and satisfiability proofs reuse the existing degree-reduction argument and exact laws for appending trivial edges.

Main definitions

• Cslib.PCP.Encoded.Graph.rotationEdges: enumerate the numerical family's directed edges.
• Cslib.PCP.Encoded.Graph.preprocess: the complete executable preprocessing program.
• Cslib.PCP.Encoded.Graph.preprocessExpanders: the exact-numbering spectral contract.

Main results

• Cslib.PCP.Encoded.Graph.isPolyTime_preprocess: machine-backed efficiency of the full program.
• Cslib.PCP.Encoded.Graph.toGraph_preprocess: exact agreement with regular preprocessing.
• Cslib.PCP.Encoded.Graph.wellFormed_preprocess: all output endpoints are in range.
• Cslib.PCP.Encoded.Graph.unsatVal_preprocess: adding family edges and loops halves the degree-reduced graph's value.
• Cslib.PCP.Encoded.Graph.le_unsatVal_preprocess: the existing Dinur gap bound for the program.

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.rotationEdges {D : Type} (rotate : ℕ × ℕ × D → ℕ × D) (labels : List D) (vertices : ℕ) : List (ℕ × ℕ)

Enumerate every outgoing edge of a numerical rotation, retaining its starting vertex. The rotation's return label is not needed when enumerating constraint-graph edges.

def Cslib.PCP.Encoded.Graph.preprocess {C D : Type} (fallback truth : C) (rotate : ℕ × ℕ × D → ℕ × D) (labels : List D) (g : Graph C) : Graph (Option (Bool × C))

Degree reduction, addition of the numerical family's edges, and one self-loop per vertex.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_rotationEdges {D : Type} {labelEncoding : D ↪ List Bool} (rotate : ℕ × ℕ × D → ℕ × D) (labels : List D) (hrotate : Turing.MultiTapeTM.ComputableTidilyInPolyTime rotate (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary labelEncoding)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary labelEncoding)) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (rotationEdges rotate labels) Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary))

Enumerating all edges charges the runtime vertex count and every rotation call.

theorem Cslib.PCP.Encoded.Graph.isPolyTime_preprocess {C D : Type} {enc : C ↪ List Bool} {labelEncoding : D ↪ List Bool} (fallback truth : C) (rotate : ℕ × ℕ × D → ℕ × D) (labels : List D) (hrotate : Turing.MultiTapeTM.ComputableTidilyInPolyTime rotate (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary labelEncoding)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary labelEncoding)) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (preprocess fallback truth rotate labels) (encoding enc) (encoding (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBool enc)))

The full preprocessing program is polynomial-time, including enumeration, copying, all edge checks used by cloud search, and materializing every intermediate graph.

@[simp]

theorem Cslib.PCP.Encoded.Graph.length_rotationEdges {D : Type} (rotate : ℕ × ℕ × D → ℕ × D) (labels : List D) (vertices : ℕ) : (rotationEdges rotate labels vertices).length = vertices * labels.length

There is one enumerated edge per vertex and supplied edge label.

@[simp]

theorem Cslib.PCP.Encoded.Graph.vertices_preprocess {C D : Type} (fallback truth : C) (rotate : ℕ × ℕ × D → ℕ × D) (labels : List D) (g : Graph C) : (preprocess fallback truth rotate labels g).vertices = 2 * g.edges.length

The output has two vertices per input edge.

theorem Cslib.PCP.Encoded.Graph.length_edges_preprocess {C D : Type} (fallback truth : C) (rotate : ℕ × ℕ × D → ℕ × D) (labels : List D) (g : Graph C) : (preprocess fallback truth rotate labels g).edges.length = 2 * g.edges.length * (2 + 2 * labels.length)

There are 2 + 2 |labels| outgoing darts per half-edge in the construction.

def Cslib.PCP.Encoded.Graph.halfEdgeEquiv (edges : ℕ) : Fin edges × Bool ≃ Fin (2 * edges)

Consecutive half-edge numbers identify the actual vertex set with Fin (2 |E|).

@[simp]

theorem Cslib.PCP.Encoded.Graph.halfEdgeEquiv_val (edges : ℕ) (p : Fin edges × Bool) : ↑((halfEdgeEquiv edges) p) = halfEdgeNumber (↑p.1, p.2)

The vertex equivalence uses the executable half-edge numbering.

def Cslib.PCP.Encoded.Graph.halfEdgeFamily {C D : Type} (g : Graph C) (family : (n : ℕ) → RotationMap (Fin n) D) : RotationMap (Fin g.edges.length × Bool) D

Interpret the numerical family on the half-edges using their explicit numbering.

def Cslib.PCP.Encoded.Graph.regularPreprocess {C α D : Type} (g : Graph C) (eval : C → α → α → Bool) (fallback : C) (family : (n : ℕ) → RotationMap (Fin n) D) : RegularConstraintGraph (Fin g.edges.length × Bool) (((Unit ⊕ D) ⊕ D) ⊕ Unit) α

The mathematical preprocessing pipeline with exactly the computed cloud and global numberings. It uses the existing degree reduction, expanderization, and loop operations.

def Cslib.PCP.Encoded.Graph.preprocessExpanders {C α D : Type} [Fintype D] (g : Graph C) (eval : C → α → α → Bool) (fallback : C) (family : (n : ℕ) → RotationMap (Fin n) D) (μ : ℝ) (hgap : ∀ (n : ℕ), (family n).spectralExpansion ≤ μ) : (g.toGraph eval).PreprocessExpanders D μ

A uniform spectral bound supplies the mathematical preprocessing contract with exactly the cloud and half-edge numberings computed by the program.

theorem Cslib.PCP.Encoded.Graph.spectralExpansion_regularPreprocess_le {C α D : Type} [Fintype D] (g : Graph C) (eval : C → α → α → Bool) (fallback : C) (family : (n : ℕ) → RotationMap (Fin n) D) (μ : ℝ) (hgap : ∀ (n : ℕ), (family n).spectralExpansion ≤ μ) : (g.regularPreprocess eval fallback family).graph.spectralExpansion ≤ 1 - (1 - μ) * ↑(Fintype.card D) / (2 * ↑(Fintype.card D) + 2)

The interpreted program inherits the preprocessing spectral bound with its actual numbering.

theorem Cslib.PCP.Encoded.Graph.wellFormed_preprocess {C D : Type} (g : Graph C) (fallback truth : C) (family : (n : ℕ) → RotationMap (Fin n) D) (rotate : ℕ × ℕ × D → ℕ × D) (hrotate : ∀ (n : ℕ) (v : Fin n) (d : D), rotate (n, ↑v, d) = (↑((family n).rot (v, d)).1, ((family n).rot (v, d)).2)) (labels : List D) : (preprocess fallback truth rotate labels g).WellFormed

All endpoints in the materialized preprocessing result are in range.

theorem Cslib.PCP.Encoded.Graph.toGraph_preprocess {C α D : Type} (g : Graph C) (eval : C → α → α → Bool) (fallback truth : C) (family : (n : ℕ) → RotationMap (Fin n) D) (rotate : ℕ × ℕ × D → ℕ × D) (hrotate : ∀ (n : ℕ) (v : Fin n) (d : D), rotate (n, ↑v, d) = (↑((family n).rot (v, d)).1, ((family n).rot (v, d)).2)) [DecidableEq α] (htruth : ∀ (a b : α), eval truth a b = true) (labels : List D) (hlabels : labels.Nodup) (hmem : ∀ (d : D), d ∈ labels) : ∃ (e : Fin (preprocess fallback truth rotate labels g).edges.length ≃ (Fin g.edges.length × Bool) × (((Unit ⊕ D) ⊕ D) ⊕ Unit)), (preprocess fallback truth rotate labels g).toGraph (degreeReduceEval eval) = ((g.regularPreprocess eval fallback family).toConstraintGraph.map fun (p : Fin g.edges.length × Bool) => halfEdgeNumber (↑p.1, p.2)).comap ⇑e

The executable preprocessing program is the existing mathematical construction, using the same cloud and half-edge numberings. The edge equivalence enumerates each mathematical dart once.

theorem Cslib.PCP.Encoded.Graph.unsatVal_preprocess {C α D : Type} (g : Graph C) (eval : C → α → α → Bool) (fallback truth : C) (rotate : ℕ × ℕ × D → ℕ × D) [DecidableEq α] [Nonempty α] (htruth : ∀ (a b : α), eval truth a b = true) (labels : List D) : ((preprocess fallback truth rotate labels g).toGraph (degreeReduceEval eval)).unsatVal = ((degreeReduce fallback rotate labels g).toGraph (degreeReduceEval eval)).unsatVal / 2

The final two steps halve the degree-reduced value, including for the empty graph.

theorem Cslib.PCP.Encoded.Graph.unsatVal_preprocess_eq {C α D : Type} (g : Graph C) (eval : C → α → α → Bool) (fallback truth : C) (family : (n : ℕ) → RotationMap (Fin n) D) (rotate : ℕ × ℕ × D → ℕ × D) (hrotate : ∀ (n : ℕ) (v : Fin n) (d : D), rotate (n, ↑v, d) = (↑((family n).rot (v, d)).1, ((family n).rot (v, d)).2)) [DecidableEq α] [Nonempty α] (htruth : ∀ (a b : α), eval truth a b = true) [Fintype D] (labels : List D) (hlabels : labels.Nodup) (hmem : ∀ (d : D), d ∈ labels) : ((preprocess fallback truth rotate labels g).toGraph (degreeReduceEval eval)).unsatVal = (g.regularPreprocess eval fallback family).toConstraintGraph.unsatVal

The computed graph has exactly the value of the regular preprocessing construction.

theorem Cslib.PCP.Encoded.Graph.le_unsatVal_preprocess {C α D : Type} (g : Graph C) (eval : C → α → α → Bool) (fallback truth : C) (family : (n : ℕ) → RotationMap (Fin n) D) (rotate : ℕ × ℕ × D → ℕ × D) (hrotate : ∀ (n : ℕ) (v : Fin n) (d : D), rotate (n, ↑v, d) = (↑((family n).rot (v, d)).1, ((family n).rot (v, d)).2)) [DecidableEq α] [Nonempty α] (htruth : ∀ (a b : α), eval truth a b = true) [Fintype D] (labels : List D) (hlabels : labels.Nodup) (hmem : ∀ (d : D), d ∈ labels) (μ : ℝ) (hgap : ∀ (n : ℕ), (family n).spectralExpansion ≤ μ) : min 1 ((1 - μ) * ↑(Fintype.card D)) / (4 * (1 + ↑(Fintype.card D))) * (g.toGraph eval).unsatVal ≤ ((preprocess fallback truth rotate labels g).toGraph (degreeReduceEval eval)).unsatVal

The existing Dinur gap estimate applies to the exact executable preprocessing output.

theorem Cslib.PCP.Encoded.Graph.satisfiable_preprocess_iff {C α D : Type} (g : Graph C) (eval : C → α → α → Bool) (fallback truth : C) (family : (n : ℕ) → RotationMap (Fin n) D) (rotate : ℕ × ℕ × D → ℕ × D) (hrotate : ∀ (n : ℕ) (v : Fin n) (d : D), rotate (n, ↑v, d) = (↑((family n).rot (v, d)).1, ((family n).rot (v, d)).2)) [DecidableEq α] [Nonempty α] (htruth : ∀ (a b : α), eval truth a b = true) [Fintype D] [Nonempty D] (labels : List D) (hlabels : labels.Nodup) (hmem : ∀ (d : D), d ∈ labels) (μ : ℝ) (hgap : ∀ (n : ℕ), (family n).spectralExpansion ≤ μ) (hμ : μ < 1) : ((preprocess fallback truth rotate labels g).toGraph (degreeReduceEval eval)).Satisfiable ↔ (g.toGraph eval).Satisfiable

Efficient preprocessing preserves satisfiability whenever the supplied clouds expand.